diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index f4765beb24..c976981957 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -362,7 +362,7 @@ [`any (sum/e any/e - (listof/e any/e))] + (many/e any/e))] [`number num/e] [`string string/e] [`natural natural/e] @@ -416,11 +416,13 @@ (λ (rep) (cons (repeat-n rep) (repeat-terms rep))) - (dep/e - nats - (λ (n) - (list/e - (build-list n (const (loop pat)))))))] + (sum/e + (const/e (cons 0 '())) + (dep/e + (nats+/e 1) + (λ (n) + (list/e + (build-list n (const (loop pat))))))))] [`(repeat ,pat ,name #f) (error 'unimplemented "named-repeat")] [`(repeat ,pat #f ,mismatch) @@ -459,7 +461,7 @@ (map/e list->string string->list - (listof/e char/e))) + (many/e char/e))) (define integer/e #; ;; Simple "turn down the volume" list @@ -479,16 +481,10 @@ (from-list/e '(#t #f))) (define var/e - #; ;; "turn down the volume" variables - (from-list/e '(x y z)) (map/e - (compose string->symbol list->string list) - (λ (sym) - (let ([chars (string->list (symbol->string sym))]) - (match chars - [`(,c) c] - [_ (error "not an enumerated variable name")]))) - char/e)) + (compose string->symbol list->string) + (compose string->list symbol->string) + (many1/e char/e))) (define any/e (sum/e num/e diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt index ecfcb40f1a..4f514a182d 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt @@ -15,13 +15,16 @@ sum/e prod/e dep/e - dep2/e ;; doesn't require size + dep2/e ;; requires size (eventually should replace dep/e with this) map/e filter/e ;; very bad, only use for small enums except/e thunk/e - listof/e + many/e + many1/e list/e + traverse/e + fail/e to-list @@ -160,6 +163,7 @@ ;; from-list/e :: Listof a -> Gen a ;; input list should not contain duplicates +;; equality on eq? (define (from-list/e l) (if (empty? l) empty/e @@ -337,6 +341,8 @@ (define (traverse/e f xs) (list/e (map f xs))) +;; sequence/e : listof (enum a) -> enum (listof a) + ;; the nth triangle number (define (tri n) (/ (* n (+ n 1)) @@ -478,73 +484,106 @@ #f] [else (bin-search 0 (- size 1))]))) -;; dep2 : enum a (a -> enum b) -> enum (a,b) -(define (dep2/e e f) - (cond [(= 0 (size e)) empty/e] - [(not (infinite? (size (f (decode e 0))))) - ;; memoize tab : boxof (hash nat -o> (nat . nat)) - ;; maps an index into the dep/e to the 2 indices that we need - (let ([tab (box (hash))]) - (enum (if (infinite? (size e)) - +inf.f - (foldl + 0 (map (compose size f) (to-list e)))) - (λ (n) ;; n -> axb - (call-with-values - (λ () - (letrec - ;; go : nat -> nat nat - ([go - (λ (n) - (cond [(hash-has-key? (unbox tab) n) - (let ([ij (hash-ref (unbox tab) n)]) - (values (car ij) (cdr ij)))] - [(= n 0) ;; find the first element - (find 0 0 0)] - [else ;; recur - (call-with-values - (λ () (go (- n 1))) - (λ (ai bi) - (find ai (- n bi 1) n)))]))] - ;; find : nat nat nat -> nat - [find - ;; start is our starting eindex - ;; seen is how many we've already seen - (λ (start seen n) - (let loop ([ai start] - [seen seen]) - (let* ([a (decode e ai)] - [bs (f a)]) - (cond [(< (- n seen) - (size bs)) - (let ([bi (- n seen)]) - (begin - (set-box! tab - (hash-set (unbox tab) - n - (cons ai bi))) - (values ai bi)))] - [else - (loop (+ ai 1) - (+ seen (size bs)))]))))]) - (go n))) - (λ (ai bi) - (let ([a (decode e ai)]) - (cons a - (decode (f a) bi)))))) - ;; todo: memoize encode - (λ (ab) ;; axb -> n - (let ([ai (encode e (car ab))]) - (+ (let loop ([i 0] - [sum 0]) - (if (>= i ai) - sum - (loop (+ i 1) - (+ sum - (size (f (decode e i))))))) - (encode (f (car ab)) - (cdr ab)))))))] - [else ;; both infinite, same as prod/e - (dep/e e f)])) +;; dep2 : natural (enum a) (a -> enum b) -> enum (a,b) +(define (dep2/e n e f) + (define (search-size sizes n) + (define (loop cur) + (let* ([lastSize (gvector-ref sizes (- cur 1))] + [e2 (f (decode e cur))] + [s (+ lastSize (size e2))]) + (gvector-add! sizes s) + (if (> s n) + cur + (loop (+ cur 1))))) + (loop (gvector-count sizes))) + ;; fill-table - find sizes[n], filling the table as it goes + ;; assumption: n >= (gvector-count sizes) + (define (fill-table sizes n) + (let loop ([cur (gvector-count sizes)]) + (let* ([prevSize (gvector-ref sizes (- cur 1))] + [curE (f (decode e cur))] + [s (+ prevSize (size curE))]) + (gvector-add! sizes s) + (if (= cur n) + s + (loop (+ cur 1)))))) + (if (= 0 (size e)) + empty/e + (cond + [(not (infinite? n)) + ;; memo table caches the size of the dependent enumerators + ;; sizes[n] = # of terms with left side index <= n + ;; sizes : gvector int + (let* ([first (size (f (decode e 0)))] + [sizes (gvector first)]) + (enum (if (infinite? (size e)) + +inf.f + (foldl + (λ (curSize acc) + (let ([sum (+ curSize acc)]) + (gvector-add! sizes sum) + sum)) + first (map (compose size f) (cdr (to-list e))))) + (λ (n) + (let* ([ind (or (find-size sizes n) + (search-size sizes n))] + [l (if (= ind 0) + 0 + (gvector-ref sizes (- ind 1)))] + [m (- n l)] + [x (decode e ind)] + [e2 (f x)] + [y (decode e2 m)]) + (cons x y))) + (λ (ab) + (let* ([a (car ab)] + [b (cdr ab)] + [ai (encode e a)] + [ei (f a)] + [nextSize (size ei)] + [sizeUpTo (if (= ai 0) + 0 + (or (gvector-ref sizes (- ai 1) #f) + (let ([sizeUp + (fill-table sizes (- ai 1))]) + (begin0 + sizeUp + (gvector-add! sizes + (+ nextSize + sizeUp))))))]) + (+ sizeUpTo + (encode ei b))))))] + [(not (infinite? (size e))) + (enum +inf.f + (λ (n) + (call-with-values + (λ () + (quotient/remainder n (size e))) + (λ (q r) + (cons (decode e r) + (decode (f (decode e r)) q))))) + (λ (ab) + (+ (* (size e) (encode (f (car ab)) (cdr ab))) + (encode e (car ab)))))] + [else ;; both infinite, same as prod/e + (enum +inf.f + (λ (n) + (let* ([k (floor-untri n)] + [t (tri k)] + [l (- n t)] + [m (- k l)] + [a (decode e l)]) + (cons a + (decode (f a) m)))) + (λ (xs) ;; bijection from nxn -> n, inverse of previous + ;; (n,m) -> (n+m)(n+m+1)/2 + n + (unless (pair? xs) + (error "not a pair")) + (let ([l (encode e (car xs))] + [m (encode (f (car xs)) (cdr xs))]) + (+ (/ (* (+ l m) (+ l m 1)) + 2) + l))))]))) ;; fold-enum : ((listof a), b -> enum a), (listof b) -> enum (listof a) (define (fold-enum f l) @@ -606,16 +645,25 @@ (λ (x) (encode (thunk) x)))) -;; listof/e : enum a -> enum (listof a) -(define (listof/e e) - (thunk/e - (if (= 0 (size e)) - 0 - +inf.f) - (λ () - (sum/e - (const/e '()) - (prod/e e (listof/e e)))))) +;; many/e : enum a -> enum (listof a) +;; or : enum a, #:length natural -> enum (listof a) +(define many/e + (case-lambda + [(e) + (thunk/e + (if (= 0 (size e)) + 0 + +inf.f) + (λ () + (sum/e + (const/e '()) + (prod/e e (many/e e)))))] + [(e n) + (list/e (build-list n (const e)))])) + +;; many1/e : enum a -> enum (nonempty listof a) +(define (many1/e e) + (prod/e e (many/e e))) ;; list/e : listof (enum any) -> enum (listof any) (define (list/e es) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt index 2f6c73eb6a..20f9e2d740 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt @@ -1,6 +1,7 @@ #lang racket/base (require rackunit redex) + (define-language Base (x a b c) (y d e f)) @@ -172,9 +173,9 @@ ;; you also must enumerate all variables that are at that ;; depth, in this way named vals and named repeats are similar - (dep/e (vals/e ((iterate 1 (curry listof/e + (dep/e (vals/e ((iterate 1 (curry many/e len2)) nats) - ((iterate 1 (curry listof/e + ((iterate 1 (curry many/e len2)) (enum y))) (λ (len1s ys) (dep/e diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt index fe8b2f648d..f5c842e5c9 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt @@ -33,6 +33,16 @@ (try-it 250 Λc e) (try-it 24 Λc x) +;; De Bruijn for performance comparison +(define-language DBλc + (e (e e) + (λ e) + x) + (x natural)) + +(try-it 500 DBλc e) + + ;; Name test (define-language Named (n (number_1 number_1)))