diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt index 67d3cde8eb..102f38ca1f 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt @@ -39,6 +39,13 @@ many1/e list/e vec/e + + cantor-vec/e + cantor-list/e + + box-vec/e + box-list/e + traverse/e hash-traverse/e @@ -836,25 +843,23 @@ (define (many1/e e) (except/e (many/e e) '())) +(define (cantor-vec/e . es) + (map/e list->vector + vector->list + (apply cantor-list/e es))) + ;; vec/e : listof (enum any) -> enum (vectorof any) -(define (vec/e . es) - (define all-inf? - (for/and ([e (in-list es)]) - (infinite? (size e)))) - (cond [(not all-inf?) - (map/e list->vector - vector->list - (list/e es))] - [else - (define k (length es)) - (define dec (cantor-untuple k)) - (define enc (cantor-tuple es)) - (enum +inf.0 dec enc)])) +(define vec/e cantor-vec/e) + +(define (box-vec/e . es) + (map/e list->vector + vector->list + (apply box-list/e es))) (define (cantor-untuple k) ;; Paul Tarau Deriving a Fast Inverse of the Generalized Cantor N-tupling Bijection (λ (n) - (apply vector (inc-set->list (combinatorial-number-decode k n))))) + (inc-set->list (combinatorial-number-decode k n)))) (define (combinatorial-number-decode k n) (define (loop k n acc) @@ -874,15 +879,13 @@ (loop k2 n2 (cons d acc))])) (loop k n '())) -(define (cantor-tuple es) - (λ (vec-xs) - (unless ((vector-length vec-xs) . = . (length es)) - (error 'bad-vector))68 - (define xs (vector->list vec-xs)) - (define is (map decode es xs)) +(define (cantor-tuple k) + (λ (xs) + (unless ((length xs) . = . k) + (error 'bad-length-cantor-tuple)) ;; Section 6 of Tarau Cantor n-tupling inverse (define sums - (list->inc-set is)) + (list->inc-set xs)) (for/sum ([sum_i (in-list sums)] [n (in-naturals)]) (binomial sum_i (add1 n))))) @@ -927,6 +930,49 @@ (cons left right)) (cons/e (list/e left) (list/e right)))])) +(define/contract (all-infinite? es) + ((listof enum?) . -> . boolean?) + (for/and ([e (in-list es)]) + (infinite? (size e)))) + +;; Fair tupling via generalized cantor n-tupling +;; ordering is monotonic in the sum of the elements of the list +(define (cantor-list/e . es) + (define all-inf? (all-infinite? es)) + (cond [(not all-inf?) + ;; TODO: improve mixed finite/infinite + (list/e es)] + [else + (define k (length es)) + (define dec + (compose + (λ (xs) (map decode es xs)) + (cantor-untuple k))) + (define enc + (compose + (cantor-tuple k) + (λ (xs) (map encode es xs)))) + (enum +inf.0 dec enc)])) + +;; Fair tupling via generalized +;; ordering is monotonic in the max of the elements of the list +(define (box-list/e . es) + (define all-inf? (all-infinite? es)) + (cond [(not all-inf?) (list/e es)] + [else + (define k (length es)) + (define dec (box-untuple k)) + (define enc (box-tuple k)) + (enum +inf.0 dec enc)])) + +(define (box-untuple k) + (λ (xs) + (error 'unimpl))) + +(define (box-tuple k) + (λ (n) + (error 'unimpl))) + (define (nats+/e n) (map/e (λ (k) (+ k n)) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt index bc4cc5b564..9bfb857634 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt @@ -268,23 +268,27 @@ [expected (list->set approx)]) (equal? actual expected))) (test-begin - (define n*n (vec/e nats/e nats/e)) - (check-range? n*n 0 1 '(#(0 0))) - (check-range? n*n 1 3 '(#(0 1) #(1 0))) - (check-range? n*n 3 6 '(#(0 2) #(1 1) #(2 0))) - (check-range? n*n 6 10 '(#(0 3) #(1 2) #(2 1) #(3 0))) - (check-range? n*n 10 15 '(#(0 4) #(1 3) #(2 2) #(3 1) #(4 0)))) + (define n*n (cantor-list/e nats/e nats/e)) + (check-range? n*n 0 1 '((0 0))) + (check-range? n*n 1 3 '((0 1) (1 0))) + (check-range? n*n 3 6 '((0 2) (1 1) (2 0))) + (check-range? n*n 6 10 '((0 3) (1 2) (2 1) (3 0))) + (check-range? n*n 10 15 '((0 4) (1 3) (2 2) (3 1) (4 0)))) (test-begin - (define n*n*n (vec/e nats/e nats/e nats/e)) - (define n*n*n*n (vec/e nats/e nats/e nats/e nats/e)) + (define n*n*n (cantor-list/e nats/e nats/e nats/e)) + (define n*n*n*n (cantor-list/e nats/e nats/e nats/e nats/e)) - (check-range? n*n*n 0 1 '(#(0 0 0))) - (check-range? n*n*n 1 4 '(#(0 0 1) #(0 1 0) #(1 0 0))) - (check-range? n*n*n 4 10 '(#(0 0 2) #(1 1 0) #(0 1 1) #(1 0 1) #(0 2 0) #(2 0 0))) - (check-range? n*n*n 10 20 '(#(0 0 3) #(0 3 0) #(3 0 0) - #(0 1 2) #(1 0 2) #(0 2 1) #(1 2 0) #(2 0 1) #(2 1 0) - #(1 1 1)))) + (check-range? n*n*n 0 1 '((0 0 0))) + (check-range? n*n*n 1 4 '((0 0 1) (0 1 0) (1 0 0))) + (check-range? n*n*n 4 10 '((0 0 2) (1 1 0) (0 1 1) (1 0 1) (0 2 0) (2 0 0))) + (check-range? n*n*n 10 20 '((0 0 3) (0 3 0) (3 0 0) + (0 1 2) (1 0 2) (0 2 1) (1 2 0) (2 0 1) (2 1 0) + (1 1 1)))) + +(test-begin + (check-bijection? (cantor-vec/e string/e nats/e real/e)) + (check-bijection? (cantor-list/e string/e nats/e real/e))) ;; helper (test-begin