Redex enum supports var-except.

Also reduces code duplication in Redex enum.
This commit is contained in:
Max New 2013-05-14 13:10:21 -05:00
parent 857cdfce64
commit c0f45d7d99
3 changed files with 128 additions and 174 deletions

View File

@ -274,6 +274,34 @@
(define pat/enum-with-names (define pat/enum-with-names
(case-lambda (case-lambda
[(pat nt-enums named-terms) [(pat nt-enums named-terms)
(pat/enum-with-names-with
pat
named-terms
(λ (nt)
(hash-ref nt-enums nt)))]
[(pat nts named-terms rec-nt-terms)
(pat/enum-with-names-with
pat
named-terms
(λ (nt)
(let ([rhss (lookup nts nt)])
(apply sum/enum
(map
(λ (rhs)
(cond [(cdr (assoc rhs (hash-ref rec-nt-terms nt)))
(thunk/enum
+inf.f
(λ ()
(rec-pat/enum (rhs-pattern rhs)
nts
rec-nt-terms)))]
[else
(rec-pat/enum (rhs-pattern rhs)
nts
rec-nt-terms)]))
rhss)))))]))
(define (pat/enum-with-names-with pat named-terms f)
(let loop ([pat pat]) (let loop ([pat pat])
(match-a-pattern (match-a-pattern
pat pat
@ -289,8 +317,7 @@
[`boolean bool/enum] [`boolean bool/enum]
[`variable var/enum] [`variable var/enum]
[`(variable-except ,s ...) [`(variable-except ,s ...)
;; todo (apply except/enum var/enum s)]
(error/enum 'unimplemented "var-except")]
[`(variable-prefix ,s) [`(variable-prefix ,s)
;; todo ;; todo
(error/enum 'unimplemented "var-prefix")] (error/enum 'unimplemented "var-prefix")]
@ -299,7 +326,7 @@
[`hole [`hole
(const/enum 'hole)] (const/enum 'hole)]
[`(nt ,id) [`(nt ,id)
(hash-ref nt-enums id)] (f id)]
[`(name ,name ,pat) [`(name ,name ,pat)
(const/enum (hash-ref named-terms name))] (const/enum (hash-ref named-terms name))]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
@ -345,107 +372,12 @@
[`(repeat ,pat #f ,mismatch) [`(repeat ,pat #f ,mismatch)
(error/enum 'unimplemented "mismatch-repeat")] (error/enum 'unimplemented "mismatch-repeat")]
[else (map/enum [else (map/enum
(λ (x) (list x)) list
car car
(loop sub-pat))])) (loop sub-pat))]))
sub-pats)))] sub-pats)))]
[(? (compose not pair?)) [(? (compose not pair?))
(const/enum pat)]))] (const/enum pat)])))
[(pat nts named-terms rec-nt-terms)
(let loop ([pat pat])
(match-a-pattern
pat
[`any
(sum/enum
any/enum
(listof/enum any/enum))]
[`number num/enum]
[`string string/enum]
[`natural natural/enum]
[`integer integer/enum]
[`real real/enum]
[`boolean bool/enum]
[`variable var/enum]
[`(variable-except ,s ...)
;; todo
(error/enum 'unimplemented "var except")]
[`(variable-prefix ,s)
;; todo
(error/enum 'unimplemented "var prefix")]
[`variable-not-otherwise-mentioned
(error/enum 'unimplemented "var not otherwise mentioned")]
[`hole
(const/enum 'hole)]
[`(nt ,id)
(let ([rhss (lookup nts id)])
(apply sum/enum
(map
(λ (rhs)
(cond [(cdr (assoc rhs (hash-ref rec-nt-terms id)))
(thunk/enum
+inf.f
(λ ()
(rec-pat/enum (rhs-pattern rhs)
nts
rec-nt-terms)))]
[else
(rec-pat/enum (rhs-pattern rhs)
nts
rec-nt-terms)]))
rhss)))]
[`(name ,name ,pat)
(const/enum (hash-ref named-terms name))]
[`(mismatch-name ,name ,pat)
(error/enum 'unimplemented "mismatch-name")]
[`(in-hole ,p1 ,p2) ;; untested
(map/enum
(λ (t1-t2)
(decomposition (car t1-t2)
(cdr t1-t2)))
(λ (decomp)
(cons (decomposition-ctx decomp)
(decomposition-term decomp)))
(prod/enum
(loop p1)
(loop p2)))]
[`(hide-hole ,p)
;; todo
(loop p)]
[`(side-condition ,p ,g ,e)
(unsupported/enum pat)]
[`(cross ,s)
(unsupported/enum pat)]
[`(list ,sub-pats ...)
;; enum-list
(map/enum
flatten-1
identity
(list/enum
(map
(λ (sub-pat)
(match sub-pat
[`(repeat ,pat #f #f)
(map/enum
cdr
(λ (ts)
(cons (length ts)
ts))
(dep/enum
nats
(λ (n)
(list/enum
(build-list n (const (loop pat)))))))]
[`(repeat ,pat ,name #f)
(error/enum 'unimplemented "named-repeat")]
[`(repeat ,pat #f ,mismatch)
(error/enum 'unimplemented "mismatch-repeat")]
[else (map/enum
list
cdr
(loop sub-pat))]))
sub-pats)))]
[(? (compose not pair?))
(const/enum pat)]))]))
(define (flatten-1 xs) (define (flatten-1 xs)
(append-map (append-map

View File

@ -80,9 +80,16 @@
(λ (x) (encode e x)))) (λ (x) (encode e x))))
;; except/enum : enum a, a -> enum a ;; except/enum : enum a, a -> enum a
(define (except/enum e a) (define except/enum
(case-lambda
[(e) e]
[(e a . rest)
(let ([excepted
(begin
(unless (> (size e) 0) (unless (> (size e) 0)
(error 'empty-enum)) (error 'empty-enum))
(with-handlers ([exn:fail? (λ (_)
(apply except/enum e rest))])
(let ([m (encode e a)]) (let ([m (encode e a)])
(enum (- (size e) 1) (enum (- (size e) 1)
(λ (n) (λ (n)
@ -93,7 +100,8 @@
(let ([n (encode e x)]) (let ([n (encode e x)])
(cond [(< n m) n] (cond [(< n m) n]
[(> n m) (- n 1)] [(> n m) (- n 1)]
[else (error 'excepted)])))))) [else (error 'excepted)])))))))])
(apply except/enum excepted rest))]))
;; to-list : enum a -> listof a ;; to-list : enum a -> listof a
;; better be finite ;; better be finite
@ -869,4 +877,13 @@
(check-equal? (to-list (up-to 3)) (check-equal? (to-list (up-to 3))
'(0 1 2 3)) '(0 1 2 3))
(check-equal? (foldl-enum cons '() (up-to 3)) (check-equal? (foldl-enum cons '() (up-to 3))
'(3 2 1 0)))) '(3 2 1 0)))
;; except/enum test
(define not-3 (except/enum nats 3))
(test-begin
(check-equal? (decode not-3 0) 0)
(check-equal? (decode not-3 3) 4))
(define not-a (except/enum nats 'a))
(test-begin
(check-equal? (decode not-a 0) 0)))

View File

@ -24,7 +24,7 @@
(e (e e) (e (e e)
(λ (x) e) (λ (x) e)
x) x)
(x variable)) (x (variable-except λ)))
;; slow: fix dep/enum ;; slow: fix dep/enum
(try-it 250 Λc e) (try-it 250 Λc e)
@ -36,3 +36,8 @@
;; Very slow, to be fixed ;; Very slow, to be fixed
(try-it 100 Named n) (try-it 100 Named n)
(define-language not-SKI
(x (variable-except s k i)))
(try-it 21 not-SKI x)