diff --git a/collects/redex/private/enum.rkt b/collects/redex/private/enum.rkt index 396521d10f..1b568ba79f 100644 --- a/collects/redex/private/enum.rkt +++ b/collects/redex/private/enum.rkt @@ -274,114 +274,21 @@ (define pat/enum-with-names (case-lambda [(pat nt-enums named-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-mentioned")] ;; error - [`hole - (const/enum 'hole)] - [`(nt ,id) - (hash-ref nt-enums id)] - [`(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) ;; loses bijection - (plug-hole (car t1-t2) - (cdr t1-t2))) - (λ (plugged) - (cons 'hole plugged)) - (prod/enum - (loop p1) - (loop p2)))] - [`(hide-hole ,p) - (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 - (λ (x) (list x)) - car - (loop sub-pat))])) - sub-pats)))] - [(? (compose not pair?)) - (const/enum pat)]))] + (pat/enum-with-names-with + pat + named-terms + (λ (nt) + (hash-ref nt-enums nt)))] [(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)]) + (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 id))) + (cond [(cdr (assoc rhs (hash-ref rec-nt-terms nt))) (thunk/enum +inf.f (λ () @@ -392,60 +299,85 @@ (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)]))])) + rhss)))))])) + +(define (pat/enum-with-names-with pat named-terms f) + (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 ...) + (apply except/enum var/enum s)] + [`(variable-prefix ,s) + ;; todo + (error/enum 'unimplemented "var-prefix")] + [`variable-not-otherwise-mentioned + (error/enum 'unimplemented "var-not-mentioned")] ;; error + [`hole + (const/enum 'hole)] + [`(nt ,id) + (f id)] + [`(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) ;; loses bijection + (plug-hole (car t1-t2) + (cdr t1-t2))) + (λ (plugged) + (cons 'hole plugged)) + (prod/enum + (loop p1) + (loop p2)))] + [`(hide-hole ,p) + (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 + car + (loop sub-pat))])) + sub-pats)))] + [(? (compose not pair?)) + (const/enum pat)]))) (define (flatten-1 xs) (append-map diff --git a/collects/redex/private/enumerator.rkt b/collects/redex/private/enumerator.rkt index 4bc8a3d14f..a63d2d0ee8 100644 --- a/collects/redex/private/enumerator.rkt +++ b/collects/redex/private/enumerator.rkt @@ -80,20 +80,28 @@ (λ (x) (encode e x)))) ;; except/enum : enum a, a -> enum a -(define (except/enum e a) - (unless (> (size e) 0) - (error 'empty-enum)) - (let ([m (encode e a)]) - (enum (- (size e) 1) - (λ (n) - (if (< n m) - (decode e n) - (decode e (+ n 1)))) - (λ (x) - (let ([n (encode e x)]) - (cond [(< n m) n] - [(> n m) (- n 1)] - [else (error 'excepted)])))))) +(define except/enum + (case-lambda + [(e) e] + [(e a . rest) + (let ([excepted + (begin + (unless (> (size e) 0) + (error 'empty-enum)) + (with-handlers ([exn:fail? (λ (_) + (apply except/enum e rest))]) + (let ([m (encode e a)]) + (enum (- (size e) 1) + (λ (n) + (if (< n m) + (decode e n) + (decode e (+ n 1)))) + (λ (x) + (let ([n (encode e x)]) + (cond [(< n m) n] + [(> n m) (- n 1)] + [else (error 'excepted)])))))))]) + (apply except/enum excepted rest))])) ;; to-list : enum a -> listof a ;; better be finite @@ -869,4 +877,13 @@ (check-equal? (to-list (up-to 3)) '(0 1 2 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))) diff --git a/collects/redex/tests/enum-test.rkt b/collects/redex/tests/enum-test.rkt index cfa4b2510d..d227af70c7 100644 --- a/collects/redex/tests/enum-test.rkt +++ b/collects/redex/tests/enum-test.rkt @@ -24,7 +24,7 @@ (e (e e) (λ (x) e) x) - (x variable)) + (x (variable-except λ))) ;; slow: fix dep/enum (try-it 250 Λc e) @@ -36,3 +36,8 @@ ;; Very slow, to be fixed (try-it 100 Named n) + +(define-language not-SKI + (x (variable-except s k i))) + +(try-it 21 not-SKI x)