From ccd9b2f2d87345e8ec9f40d40b0a3e9c4fbf9d76 Mon Sep 17 00:00:00 2001 From: Max New Date: Tue, 4 Mar 2014 00:47:23 -0600 Subject: [PATCH] Start fair interleaving for Redex enumeration (decode) Also remove dead code and split disj-sum/e #:append to separate function --- .../redex-lib/redex/private/enum.rkt | 2 +- .../redex-lib/redex/private/enumerator.rkt | 283 ++++++++---------- .../redex/tests/enumerator-test.rkt | 102 +++---- 3 files changed, 168 insertions(+), 219 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index 53560eedae..c58ee7abef 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -94,7 +94,7 @@ production-term e) (λ (nd-x) (= i (production-n nd-x))))) - (apply disj-sum/e #:alternate? #t + (apply disj-sum/e (for/list ([i (in-naturals)] [production (in-list rhss)]) (with-index i diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt index 98e25b595a..a77e84134c 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt @@ -20,8 +20,8 @@ empty/e const/e from-list/e - sum/e disj-sum/e + disj-append/e cons/e dep/e dep2/e ;; requires size (eventually should replace dep/e with this) @@ -212,148 +212,123 @@ (- (* 2 n) 1) (* 2 (abs n)))))) -;; sum :: enum a, enum b -> enum (U a b) -(define sum/e - (case-lambda - [(e) e] - [(e1 e2) - ;; Sum two enumerators of different sizes - (define (sum-uneven less/e more/e) - ;; interleave until less/e is exhausted - ;; pairsdone is 1+ the highest index using less/e - (let* ([less-size (size less/e)] - [pairsdone (* 2 less-size)]) - (enum (+ less-size (size more/e)) - (λ (n) - (if (< n pairsdone) - (let-values ([(q r) (quotient/remainder n 2)]) - ;; Always put e1 first though! - (decode (match r - [0 e1] - [1 e2]) - q)) - (decode more/e (- n less-size)))) - (λ (x) - (with-handlers - ([exn:fail? - (λ (_) - (let ([i (encode more/e x)]) - (if (< i less-size) - (+ (* 2 i) 1) - (+ (- i less-size) pairsdone))))]) - (* 2 (encode less/e x))))))) - (let* ([s1 (size e1)] - [s2 (size e2)]) - (cond - [(= 0 s1) e2] - [(= 0 s2) e1] - [(< s1 s2) - (sum-uneven e1 e2)] - [(< s2 s1) - (sum-uneven e2 e1)] - [else ;; both the same length, interleave them - (enum (+ s1 s2) - (λ (n) - (if (even? n) - ((enum-from e1) (/ n 2)) - ((enum-from e2) (/ (- n 1) 2)))) - (λ (x) - (with-handlers ([exn:fail? - (λ (_) - (+ (* ((enum-to e2) x) 2) - 1))]) - (* ((enum-to e1) x) 2))))]))] - [(a b c . rest) - ;; map-pairs : (a, a -> b), (a -> b), listof a -> listof b - ;; apply the function to every pair, applying f to the first element of an odd length list - (define (map-pairs f d l) - (define (map-pairs/even l) - (match l - ['() '()] - [`(,x ,y ,rest ...) - (cons (f x y) - (map-pairs f d rest))])) - (if (even? (length l)) - (map-pairs/even l) - (cons (d (car l)) - (map-pairs/even (cdr l))))) - (apply sum/e (map-pairs sum/e identity (list* a b c rest)))])) +(define (empty/e? e) + (= 0 (size e))) -(define (disj-sum/e #:alternate? [alternate? #f] #:append? [append? #f] e-p . e-ps) - (define/match (disj-sum2/e e-p1 e-p2) +(define (exact-min . xs) + (define (exact-min-2 x y) + (if (x . <= . y) + x + y)) + (foldl exact-min-2 +inf.0 xs)) + +(struct upper-bound + (total-bound ;; Nat + individual-bound ;; Nat + enumerators ;; Vectorof (Enum a) + ) + #:transparent) + +;; layers : Listof Enum -> Listof Upper-Bound +(define/contract (mk-layers es [prev (upper-bound 0 0 (vector es))]) + ((listof enum?) . -> . (listof upper-bound?)) + (define non-emptys (filter (negate empty/e?) es)) + (match non-emptys + ['() '()] + [_ + (define min-size + (apply exact-min (map size non-emptys))) + (define (not-min-size? e) + (not (= (size e) min-size))) + (define leftover + (filter not-min-size? non-emptys)) + (define ves + (apply vector non-emptys)) + (match-define (upper-bound prev-tb + prev-ib + prev-es) + prev) + (define diff-min-size + (min-size . - . prev-ib)) + (define total-bound + (prev-tb . + . (diff-min-size . * . (vector-length ves)))) + (define cur-layer + (upper-bound total-bound + min-size + ves)) + (define remaining-layers + (mk-layers leftover cur-layer)) + (cons cur-layer + remaining-layers)])) + +;; find-layer : Nat, Nonempty-Listof Upper-bound -> Upper-bound, Upper-bound +;; Given an index, find the first layer +(define/contract (find-layer i layers) + (natural-number/c (listof upper-bound?) . -> . (values upper-bound? upper-bound?)) + (define (loop prev ls) + (match ls + ['() (error "internal error in find-layer: index out of range")] + [(cons (and ub (upper-bound tb ib es)) + tl) + (cond [(i . < . tb) (values prev ub)] + [else (loop ub tl)])])) + (loop (upper-bound 0 0 (vector)) + layers)) + +;; fairly interleave a list of enumerations +(define (disj-sum/e . e-ps) + (define layers + (mk-layers (map car e-ps))) + (define (empty-e-p? e-p) + (= 0 (size (car e-p)))) + (match (filter (negate empty-e-p?) e-ps) + ['() empty/e] + [`(,e-p) (car e-p)] + [_ + (define (dec i) + (define-values (prev-up-bound cur-up-bound) + (find-layer i layers)) + (match-define (upper-bound so-far prev-ib es1) prev-up-bound) + (match-define (upper-bound ctb cib es) cur-up-bound) + (define this-i (i . - . so-far)) + (define len (vector-length es)) + (define-values (q r) (quotient/remainder this-i len)) + (define this-e (vector-ref es r)) + (decode this-e (+ q prev-ib))) + (define (enc x) + 0 + ;; (error 'todo) + ) + (enum (apply + (map (compose size car) e-ps)) + dec + enc)])) + +;; Like disj-sum/e, but sequences the enumerations instead of interleaving +(define (disj-append/e e-p . e-ps) + (define/match (disj-append2/e e-p1 e-p2) [((cons e1 1?) (cons e2 2?)) - (define (alternate-uneven less/e less? more/e more? #:less-first? less-first?) - (define-values (first/e second/e) - (if less-first? - (values less/e more/e) - (values more/e less/e))) - ;; interleave until less/e is exhausted - ;; pairsdone is 1+ the highest index using less/e - (define less-size (size less/e)) - (define pairsdone (* 2 less-size)) - (define (from-nat n) - (cond [(< n pairsdone) - (define-values (q r) (quotient/remainder n 2)) - ;; Always put e1 first though! - (decode (match r - [0 first/e] - [1 second/e]) - q)] - [else (decode more/e (- n less-size))])) - (define (to-nat x) - (cond [(less? x) - (+ (* 2 (encode less/e x)) - (if less-first? 0 1))] - [(more? x) - (define i (encode more/e x)) - (if (< i less-size) - (+ (* 2 i) - (if less-first? 1 0)) - (+ (- i less-size) pairsdone))] - [else (redex-error 'encode "bad term")])) - (enum (+ less-size (size more/e)) - from-nat - to-nat)) (define s1 (size e1)) (define s2 (size e2)) - (cond [(not (xor alternate? append?)) - (redex-error 'disj-sum/e "Conflicting options chosen, must pick exactly one of #:alternate? or #:append?")] - [alternate? - (cond [(= 0 s1) e2] - [(= 0 s2) e1] - [(< s1 s2) (alternate-uneven e1 1? e2 2? #:less-first? #t)] - [(< s2 s1) (alternate-uneven e2 2? e1 1? #:less-first? #f)] - [else ;; both the same length, interleave them - (define (from-nats n) - (cond [(even? n) (decode e1 (/ n 2))] - [else (decode e2 (/ (- n 1) 2))])) - (define (to-nats x) - (cond [(1? x) (* (encode e1 x) 2)] - [(2? x) (+ 1 (* (encode e2 x) 2))] - [else (redex-error 'encode "bad term")])) - (enum (+ s1 s2) from-nats to-nats)])] - [append? - (define (from-nat n) - (cond [(< n s1) (decode e1 n)] - [else (decode e2 (- n s1))])) - (define (to-nat x) - (cond [(1? x) (encode e1 x)] - [(2? x) (+ (encode e2 x) s1)] - [else (redex-error 'encode "bad term")])) - (enum (+ s1 s2) from-nat to-nat)] - [(nor alternate? append?) - (redex-error 'disj-sum/e "Must specify either #:alternate? or #:append?")])]) + (when (infinite? s1) + (error "Only the last enum in a call to disj-append/e can be infinite.")) + (define (from-nat n) + (cond [(< n s1) (decode e1 n)] + [else (decode e2 (- n s1))])) + (define (to-nat x) + (cond [(1? x) (encode e1 x)] + [(2? x) (+ (encode e2 x) s1)] + [else (redex-error 'encode "bad term")])) + (enum (+ s1 s2) from-nat to-nat)]) (car - (foldr (λ (e-p1 e-p2) + (foldr1 (λ (e-p1 e-p2) (match* (e-p1 e-p2) [((cons e1 1?) (cons e2 2?)) - (cons (disj-sum2/e e-p1 - (cons e2 (negate 1?))) + (cons (disj-append2/e e-p1 + (cons e2 (negate 1?))) (λ (x) (or (1? x) (2? x))))])) - (cons empty/e (λ (_) #f)) - (cons e-p e-ps)))) + (cons e-p e-ps)))) (define (foldr1 f l) (match l @@ -753,8 +728,7 @@ +inf.0)) (fix/e fix-size (λ (self) - (disj-sum/e #:alternate? #t - (cons (const/e '()) null?) + (disj-sum/e (cons (const/e '()) null?) (cons (cons/e e self) pair?))))] [(e n) (list/e (build-list n (const e)))])) @@ -828,13 +802,12 @@ (map/e integer->char char->integer - (disj-sum/e #:append? #t - low/e-p - up/e-p - bottom/e-p - mid/e-p - above1/e-p - above2/e-p))) + (disj-append/e low/e-p + up/e-p + bottom/e-p + mid/e-p + above1/e-p + above2/e-p))) (define string/e (map/e @@ -848,8 +821,7 @@ nats/e)) (define integer/e - (disj-sum/e #:alternate? #t - (cons (const/e 0) zero?) + (disj-sum/e (cons (const/e 0) zero?) (cons from-1/e (λ (n) (> n 0))) (cons (map/e - - from-1/e) (λ (n) (< n 0))))) @@ -871,13 +843,11 @@ (nor (infinite? n) (nan? n)))))) (define float/e - (disj-sum/e #:append? #t - weird-flonums/e-p - normal-flonums/e-p)) + (disj-append/e weird-flonums/e-p + normal-flonums/e-p)) (define real/e - (disj-sum/e #:alternate? #t - (cons integer/e exact-integer?) + (disj-sum/e (cons integer/e exact-integer?) (cons float/e flonum?))) (define non-real/e @@ -886,11 +856,14 @@ (values (real-part z) (imag-part z))) real/e - (except/e real/e 0 0.0))) + (except/e real/e + 0 + ;; TODO: revert this when encode works + ;; 0.0 + ))) (define num/e - (disj-sum/e #:alternate? #t - (cons real/e real?) + (disj-sum/e (cons real/e real?) (cons non-real/e complex?))) (define bool/e @@ -903,8 +876,7 @@ (many/e char/e))) (define base/e - (disj-sum/e #:alternate? #t - (cons (const/e '()) null?) + (disj-sum/e (cons (const/e '()) null?) (cons num/e number?) (cons string/e string?) (cons bool/e boolean?) @@ -913,8 +885,7 @@ (define any/e (fix/e +inf.0 (λ (any/e) - (disj-sum/e #:alternate? #t - (cons base/e (negate pair?)) + (disj-sum/e (cons base/e (negate pair?)) (cons (cons/e any/e any/e) pair?))))) (define (var-prefix/e s) (define as-str (symbol->string s)) 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 fc5975703b..f9359f2468 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt @@ -61,7 +61,6 @@ (check-bijection? ints/e)) ; -1 -> 2, -3 -> 4 ;; sum tests - (define evens/e (enum +inf.0 (λ (n) @@ -82,69 +81,22 @@ (/ (- n 1) 2) (error 'odd))))) -(test-begin - (let ([bool-or-num (sum/e bools/e - (from-list/e '(0 1 2 3)))] - [bool-or-nat (sum/e bools/e - nats/e)] - [nat-or-bool (sum/e nats/e - bools/e)] - [odd-or-even (sum/e evens/e - odds/e)]) - (check-equal? (size bool-or-num) 6) - - (check-equal? (decode bool-or-num 0) #t) - (check-equal? (decode bool-or-num 1) 0) - (check-equal? (decode bool-or-num 2) #f) - (check-equal? (decode bool-or-num 3) 1) - (check-equal? (decode bool-or-num 4) 2) - (check-equal? (decode bool-or-num 5) 3) - - (check-exn exn:fail? - (λ () - (decode bool-or-num 6))) - (check-bijection? bool-or-num) - - (check-equal? (size bool-or-nat) - +inf.0) - (check-equal? (decode bool-or-nat 0) #t) - (check-equal? (decode bool-or-nat 1) 0) - (check-bijection? bool-or-nat) - - (check-equal? (size odd-or-even) - +inf.0) - (check-equal? (decode odd-or-even 0) 0) - (check-equal? (decode odd-or-even 1) 1) - (check-equal? (decode odd-or-even 2) 2) - (check-exn exn:fail? - (λ () - (decode odd-or-even -1))) - (check-equal? (encode odd-or-even 0) 0) - (check-equal? (encode odd-or-even 1) 1) - (check-equal? (encode odd-or-even 2) 2) - (check-equal? (encode odd-or-even 3) 3) - (check-bijection? odd-or-even) - ;; Known bug, won't fix because I'm getting rid of sum/e anyway - ;; (check-bijection? nat-or-bool) - )) - (test-begin (define bool-or-num - (disj-sum/e #:alternate? #t - (cons bools/e boolean?) + (disj-sum/e (cons bools/e boolean?) (cons (from-list/e '(0 1 2 3)) number?))) (define bool-or-nat - (disj-sum/e #:alternate? #t - (cons bools/e boolean?) + (disj-sum/e (cons bools/e boolean?) (cons nats/e number?))) (define nat-or-bool - (disj-sum/e #:alternate? #t - (cons nats/e number?) + (disj-sum/e (cons nats/e number?) (cons bools/e boolean?))) (define odd-or-even - (disj-sum/e #:alternate? #t - (cons evens/e even?) + (disj-sum/e (cons evens/e even?) (cons odds/e odd?))) + + + (check-equal? (size bool-or-num) 6) (check-equal? (decode bool-or-num 0) #t) @@ -179,17 +131,42 @@ (check-equal? (encode odd-or-even 3) 3) (check-bijection? odd-or-even) - (check-bijection? nat-or-bool)) + (check-bijection? nat-or-bool) + + (define multi-layered + (disj-sum/e (cons (take/e string/e 5) string?) + (cons (from-list/e '(a b c d)) symbol?) + (cons nats/e number?) + (cons bool/e boolean?) + (cons (many/e bool/e) list?))) + + (define (test-multi-layered i x) + (check-equal? (decode multi-layered i) x)) + (map test-multi-layered + (for/list ([i (in-range 31)]) + i) + ;; Please don't reformat this! + '("" a 0 #t () + "a" b 1 #f (#t) + "b" c 2 (#f) + "c" d 3 (#t #t) + "d" 4 (#f #t) + 5 (#t #f) + 6 (#f #f) + 7 (#t #t #t) + 8 (#f #t #t) + 9 (#t #f #t))) + + (check-bijection? multi-layered) + ) (test-begin (define bool-or-num - (disj-sum/e #:append? #t - (cons bools/e boolean?) - (cons (from-list/e '(0 1 2 3)) number?))) + (disj-append/e (cons bools/e boolean?) + (cons (from-list/e '(0 1 2 3)) number?))) (define bool-or-nat - (disj-sum/e #:append? #t - (cons bools/e boolean?) - (cons nats/e number?))) + (disj-append/e (cons bools/e boolean?) + (cons nats/e number?))) (check-equal? (size bool-or-num) 6) (check-equal? (decode bool-or-num 0) #t) @@ -442,3 +419,4 @@ (define natss (many/e nats/e)) (check-bijection? natss) +