Have cons/e use list/e and make explicit when using finite cons/e
Also add to-stream and make cons/e tests less specific
This commit is contained in:
Max New
Robby Findler
parent
f309685999
commit
7032acc066
|
|
@ -6,6 +6,7 @@
|
|||
racket/math
|
||||
racket/match
|
||||
racket/promise
|
||||
racket/stream
|
||||
racket/vector
|
||||
|
||||
data/gvector
|
||||
|
|
@ -55,6 +56,7 @@
|
|||
|
||||
approximate
|
||||
to-list
|
||||
to-stream
|
||||
take/e
|
||||
fold-enum
|
||||
|
||||
|
|
@ -148,6 +150,15 @@
|
|||
e
|
||||
excepts))
|
||||
|
||||
(define (to-stream e)
|
||||
(define (loop n)
|
||||
(cond [(n . >= . (size e))
|
||||
empty-stream]
|
||||
[else
|
||||
(stream-cons (decode e n)
|
||||
(loop (add1 n)))]))
|
||||
(loop 0))
|
||||
|
||||
(define (approximate e n)
|
||||
(for/list ([i (in-range n)])
|
||||
(decode e i)))
|
||||
|
|
@ -241,6 +252,11 @@
|
|||
y))
|
||||
(foldl exact-min-2 +inf.0 xs))
|
||||
|
||||
(struct fin-layer
|
||||
(bound ;; nat
|
||||
enums) ;; Vectorof (Enum a, list-index)
|
||||
#:transparent)
|
||||
|
||||
(struct upper-bound
|
||||
(total-bound ;; Nat
|
||||
individual-bound ;; Nat
|
||||
|
|
@ -248,8 +264,19 @@
|
|||
)
|
||||
#:transparent)
|
||||
|
||||
;; layers : Listof Enum -> Listof Upper-Bound
|
||||
(define (mk-layers es)
|
||||
; scanl :: (a -> b -> b) -> b -> [a] -> [b]
|
||||
(define (scanl f base xs)
|
||||
(let loop ([cur base]
|
||||
[xs xs]
|
||||
[acc '()])
|
||||
(match xs
|
||||
['() (cons base (reverse acc))]
|
||||
[(cons x xs)
|
||||
(define step (f x cur))
|
||||
(loop step xs (cons step acc))])))
|
||||
|
||||
(define/contract (mk-fin-layers es)
|
||||
((listof enum?) . -> . (listof fin-layer?))
|
||||
(define (loop eis prev)
|
||||
(define non-emptys (filter (negate (compose empty/e? car)) eis))
|
||||
(match non-emptys
|
||||
|
|
@ -263,18 +290,7 @@
|
|||
(filter not-min-size? non-emptys))
|
||||
(define veis
|
||||
(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 veis))))
|
||||
(define cur-layer
|
||||
(upper-bound total-bound
|
||||
min-size
|
||||
veis))
|
||||
(define cur-layer (fin-layer min-size veis))
|
||||
(define remaining-layers
|
||||
(loop leftover cur-layer))
|
||||
(cons cur-layer
|
||||
|
|
@ -283,9 +299,40 @@
|
|||
(for/list [(i (in-naturals))
|
||||
(e (in-list es))]
|
||||
(cons e i)))
|
||||
(apply vector
|
||||
(loop eis
|
||||
(upper-bound 0 0 eis))))
|
||||
(loop eis (fin-layer 0 eis)))
|
||||
|
||||
;; layers : Listof Enum -> Listof Upper-Bound
|
||||
(define/contract (disj-sum-layers es)
|
||||
((listof enum?) . -> . (vectorof upper-bound?))
|
||||
(define fin-layers (mk-fin-layers es))
|
||||
(define/contract (loop fin-layers prev)
|
||||
(-> (listof fin-layer?)
|
||||
upper-bound?
|
||||
(listof upper-bound?))
|
||||
(match fin-layers
|
||||
['() '()]
|
||||
[(cons (fin-layer cur-bound eis) rest-fin-layers)
|
||||
(match-define (upper-bound prev-tb
|
||||
prev-ib
|
||||
_)
|
||||
prev)
|
||||
(define min-size cur-bound)
|
||||
(define diff-min-size
|
||||
(min-size . - . prev-ib))
|
||||
(define total-bound
|
||||
(prev-tb . + . (diff-min-size . * . (vector-length eis))))
|
||||
(define cur-layer
|
||||
(upper-bound total-bound
|
||||
cur-bound
|
||||
eis))
|
||||
(define rest-layers (loop rest-fin-layers cur-layer))
|
||||
(cons cur-layer
|
||||
rest-layers)]))
|
||||
(define eis
|
||||
(for/list [(i (in-naturals))
|
||||
(e (in-list es))]
|
||||
(cons e i)))
|
||||
(apply vector (loop fin-layers (upper-bound 0 0 eis))))
|
||||
|
||||
;; find-layer : Nat, Nonempty-Listof Upper-bound -> Upper-bound, Upper-bound
|
||||
;; Given an index, find the first layer
|
||||
|
|
@ -347,7 +394,7 @@
|
|||
;; fairly interleave a list of enumerations
|
||||
(define (disj-sum/e . e-ps)
|
||||
(define layers
|
||||
(mk-layers (map car e-ps)))
|
||||
(disj-sum-layers (map car e-ps)))
|
||||
(define (empty-e-p? e-p)
|
||||
(= 0 (size (car e-p))))
|
||||
(match (filter (negate empty-e-p?) e-ps)
|
||||
|
|
@ -357,8 +404,8 @@
|
|||
(define (dec i)
|
||||
(define-values (prev-up-bound cur-up-bound)
|
||||
(find-dec-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)
|
||||
(match-define (upper-bound so-far prev-ib _) 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))
|
||||
|
|
@ -410,54 +457,48 @@
|
|||
[(cons x '()) x]
|
||||
[(cons x xs) (f x (foldr1 f xs))]))
|
||||
|
||||
(define (fin-cons/e e1 e2)
|
||||
(define s1 (enum-size e1))
|
||||
(define s2 (enum-size e2))
|
||||
(define size (* s1 s2))
|
||||
(cond [(zero? size) empty/e]
|
||||
[(or (not (infinite? s1))
|
||||
(not (infinite? s2)))
|
||||
(define fst-finite? (not (infinite? s1)))
|
||||
(define fin-size
|
||||
(cond [fst-finite? s1]
|
||||
[else s2]))
|
||||
(define (dec n)
|
||||
(define-values (q r)
|
||||
(quotient/remainder n fin-size))
|
||||
(define-values (n1 n2)
|
||||
(if fst-finite?
|
||||
(values r q)
|
||||
(values q r)))
|
||||
(cons (decode e1 n1)
|
||||
(decode e2 n2)))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define n1 (encode e1 x1))
|
||||
(define n2 (encode e2 x2))
|
||||
(define-values (q r)
|
||||
(if fst-finite?
|
||||
(values n2 n1)
|
||||
(values n1 n2)))
|
||||
(+ (* fin-size q)
|
||||
r)])
|
||||
(enum size dec enc)]
|
||||
[else
|
||||
(redex-error 'internal "fin-cons/e should only be called on finite enumerations")]))
|
||||
|
||||
;; cons/e : enum a, enum b ... -> enum (cons a b ...)
|
||||
(define (cons/e e . es)
|
||||
(define (cons/e2 e1 e2)
|
||||
(define s1 (enum-size e1))
|
||||
(define s2 (enum-size e2))
|
||||
(define size (* s1 s2))
|
||||
(cond [(zero? size) empty/e]
|
||||
[(or (not (infinite? s1))
|
||||
(not (infinite? s2)))
|
||||
(define fst-finite? (not (infinite? s1)))
|
||||
(define fin-size
|
||||
(cond [fst-finite? s1]
|
||||
[else s2]))
|
||||
(define (dec n)
|
||||
(define-values (q r)
|
||||
(quotient/remainder n fin-size))
|
||||
(define x1 (decode e1 (if fst-finite? r q)))
|
||||
(define x2 (decode e2 (if fst-finite? q r)))
|
||||
(cons x1 x2))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define n1 (encode e1 x1))
|
||||
(define n2 (encode e2 x2))
|
||||
(define q (if fst-finite? n2 n1))
|
||||
(define r (if fst-finite? n1 n2))
|
||||
(+ (* fin-size q)
|
||||
r)])
|
||||
(enum size dec enc)]
|
||||
[else
|
||||
;; based on http://en.wikipedia.org/wiki/Pairing_function
|
||||
(define (dec n)
|
||||
(define k (floor-untri n))
|
||||
(define t (tri k))
|
||||
(define l (- n t))
|
||||
(define m (- k l))
|
||||
(define x1 (decode e1 l))
|
||||
(define x2 (decode e2 m))
|
||||
(cons x1 x2))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define l (encode e1 x1))
|
||||
(define m (encode e2 x2))
|
||||
(+ (/ (* (+ l m)
|
||||
(+ l m 1))
|
||||
2)
|
||||
l)])
|
||||
(enum size dec enc)]))
|
||||
(foldr1 cons/e2 (cons e es)))
|
||||
(define (cons/e e1 e2)
|
||||
(map/e (λ (x)
|
||||
(cons (first x)
|
||||
(second x)))
|
||||
(λ (x-y)
|
||||
(list (car x-y) (cdr x-y)))
|
||||
(list/e e1 e2)))
|
||||
|
||||
(define (elegant-cons/e e1 e2)
|
||||
(define s1 (size e1))
|
||||
|
|
@ -504,8 +545,9 @@
|
|||
;; on-cdr : (cons k a) -> enum (cons k b)
|
||||
(define/match (on-cdr pr)
|
||||
[((cons k v))
|
||||
(cons/e (const/e k)
|
||||
(f v))])
|
||||
(map/e (λ (x) (cons k x))
|
||||
cdr
|
||||
(f v))])
|
||||
;; enum (listof (cons k b))
|
||||
(define assoc/e
|
||||
(traverse/e on-cdr as-list))
|
||||
|
|
@ -833,7 +875,7 @@
|
|||
+inf.0))
|
||||
(fix/e fix-size
|
||||
(λ (self)
|
||||
(disj-sum/e (cons (const/e '()) null?)
|
||||
(disj-sum/e (cons (fin/e '()) null?)
|
||||
(cons (cons/e e self) pair?))))]
|
||||
[(e n)
|
||||
(apply list/e (build-list n (const e)))]))
|
||||
|
|
@ -977,6 +1019,7 @@
|
|||
rest
|
||||
(cons (car fins) acc))])]))])
|
||||
(define (deconstruct xs)
|
||||
|
||||
(let loop ([xs xs]
|
||||
[inf-acc '()]
|
||||
[fin-acc '()]
|
||||
|
|
@ -997,8 +1040,8 @@
|
|||
rest-inf?s)])])))
|
||||
(map/e reconstruct
|
||||
deconstruct
|
||||
(cons/e (apply list/e inf-es)
|
||||
(apply list/e fin-es)))]))
|
||||
(fin-cons/e (apply list/e inf-es)
|
||||
(apply list/e fin-es)))]))
|
||||
|
||||
(define (nested-cons-list/e . es)
|
||||
(define l (length es))
|
||||
|
|
@ -1009,7 +1052,7 @@
|
|||
(λ (lst)
|
||||
(define-values (left right) (split-at lst split-point))
|
||||
(cons left right))
|
||||
(cons/e (apply list/e left) (apply list/e right))))
|
||||
(fin-cons/e (apply list/e left) (apply list/e right))))
|
||||
|
||||
|
||||
(define (all-infinite? es)
|
||||
|
|
@ -1078,8 +1121,8 @@
|
|||
(define first-not-max/e
|
||||
(match bound
|
||||
[0 empty/e]
|
||||
[_ (cons/e (take/e nat/e bound)
|
||||
smallers/e)]))
|
||||
[_ (fin-cons/e (take/e nat/e bound)
|
||||
smallers/e)]))
|
||||
(define (first-max? l)
|
||||
((first l) . = . bound))
|
||||
(disj-append/e (cons first-not-max/e (negate first-max?))
|
||||
|
|
|
|||
|
|
@ -5,10 +5,6 @@
|
|||
redex/private/enumerator
|
||||
(submod redex/private/enumerator test))
|
||||
|
||||
;; basic enums
|
||||
(define bools/e
|
||||
(from-list/e (list #t #f)))
|
||||
|
||||
;; const/e tests
|
||||
(let ([e (const/e 17)])
|
||||
(test-begin
|
||||
|
|
@ -83,14 +79,14 @@
|
|||
|
||||
(test-begin
|
||||
(define bool-or-num
|
||||
(disj-sum/e (cons bools/e boolean?)
|
||||
(disj-sum/e (cons bool/e boolean?)
|
||||
(cons (from-list/e '(0 1 2 3)) number?)))
|
||||
(define bool-or-nat
|
||||
(disj-sum/e (cons bools/e boolean?)
|
||||
(disj-sum/e (cons bool/e boolean?)
|
||||
(cons nat/e number?)))
|
||||
(define nat-or-bool
|
||||
(disj-sum/e (cons nat/e number?)
|
||||
(cons bools/e boolean?)))
|
||||
(cons bool/e boolean?)))
|
||||
(define odd-or-even
|
||||
(disj-sum/e (cons evens/e even?)
|
||||
(cons odds/e odd?)))
|
||||
|
|
@ -161,10 +157,10 @@
|
|||
|
||||
(test-begin
|
||||
(define bool-or-num
|
||||
(disj-append/e (cons bools/e boolean?)
|
||||
(disj-append/e (cons bool/e boolean?)
|
||||
(cons (from-list/e '(0 1 2 3)) number?)))
|
||||
(define bool-or-nat
|
||||
(disj-append/e (cons bools/e boolean?)
|
||||
(disj-append/e (cons bool/e boolean?)
|
||||
(cons nat/e number?)))
|
||||
(check-equal? (size bool-or-num) 6)
|
||||
|
||||
|
|
@ -188,11 +184,11 @@
|
|||
(check-bijection? bool-or-nat))
|
||||
|
||||
;; cons/e tests
|
||||
(define bool*bool (cons/e bools/e bools/e))
|
||||
(define 1*b (cons/e (const/e 1) bools/e))
|
||||
(define b*1 (cons/e bools/e (const/e 1)))
|
||||
(define bool*nats (cons/e bools/e nat/e))
|
||||
(define nats*bool (cons/e nat/e bools/e))
|
||||
(define bool*bool (cons/e bool/e bool/e))
|
||||
(define 1*b (cons/e (const/e 1) bool/e))
|
||||
(define b*1 (cons/e bool/e (const/e 1)))
|
||||
(define bool*nats (cons/e bool/e nat/e))
|
||||
(define nats*bool (cons/e nat/e bool/e))
|
||||
(define nats*nats (cons/e nat/e nat/e))
|
||||
(define ns-equal? (λ (ns ms)
|
||||
(and (= (car ns)
|
||||
|
|
@ -211,55 +207,17 @@
|
|||
(check-bijection? 1*b)
|
||||
(check-bijection? b*1)
|
||||
(check-equal? (size bool*bool) 4)
|
||||
(check-equal? (decode bool*bool 0)
|
||||
(cons #t #t))
|
||||
(check-equal? (decode bool*bool 1)
|
||||
(cons #f #t))
|
||||
(check-equal? (decode bool*bool 2)
|
||||
(cons #t #f))
|
||||
(check-equal? (decode bool*bool 3)
|
||||
(cons #f #f))
|
||||
(check-bijection? bool*bool)
|
||||
|
||||
(check-equal? (size bool*nats) +inf.0)
|
||||
(check-equal? (decode bool*nats 0)
|
||||
(cons #t 0))
|
||||
(check-equal? (decode bool*nats 1)
|
||||
(cons #f 0))
|
||||
(check-equal? (decode bool*nats 2)
|
||||
(cons #t 1))
|
||||
(check-equal? (decode bool*nats 3)
|
||||
(cons #f 1))
|
||||
(check-bijection? bool*nats)
|
||||
|
||||
(check-equal? (size nats*bool) +inf.0)
|
||||
(check-equal? (decode nats*bool 0)
|
||||
(cons 0 #t))
|
||||
(check-equal? (decode nats*bool 1)
|
||||
(cons 0 #f))
|
||||
(check-equal? (decode nats*bool 2)
|
||||
(cons 1 #t))
|
||||
(check-equal? (decode nats*bool 3)
|
||||
(cons 1 #f))
|
||||
(check-bijection? nats*bool)
|
||||
|
||||
(check-equal? (size nats*nats) +inf.0)
|
||||
(check ns-equal?
|
||||
(decode nats*nats 0)
|
||||
(cons 0 0))
|
||||
(check ns-equal?
|
||||
(decode nats*nats 1)
|
||||
(cons 0 1))
|
||||
(check ns-equal?
|
||||
(decode nats*nats 2)
|
||||
(cons 1 0))
|
||||
(check ns-equal?
|
||||
(decode nats*nats 3)
|
||||
(cons 0 2))
|
||||
(check ns-equal?
|
||||
(decode nats*nats 4)
|
||||
(cons 1 1))
|
||||
(check-bijection? nats*nats))
|
||||
(check-bijection? nats*nats)
|
||||
(check-bijection? (list/e integer/e integer/e)))
|
||||
|
||||
|
||||
;; fair product tests
|
||||
(define-simple-check (check-range? e l u approx)
|
||||
|
|
@ -323,9 +281,55 @@
|
|||
(check-equal? (list->inc-set '(2 0 1 2)) '(2 3 5 8))
|
||||
(check-equal? (inc-set->list '(2 3 5 8)) '(2 0 1 2)))
|
||||
|
||||
(define (below/e n)
|
||||
(take/e nat/e n))
|
||||
|
||||
;; mixed finite/infinite list/e tests
|
||||
(test-begin
|
||||
|
||||
(check-equal?
|
||||
(to-list (list/e (below/e 3) (below/e 3) (below/e 3)))
|
||||
(to-list (take/e (list/e nat/e nat/e nat/e) 27)))
|
||||
|
||||
(define n*2 (list/e nat/e (below/e 2)))
|
||||
(check-range? n*2 0 1 '((0 0)))
|
||||
(check-range? n*2 1 3 '((0 1) (1 0) (1 1)))
|
||||
(check-range? n*2 3 5 '((2 0) (2 1)))
|
||||
(check-range? n*2 5 7 '((3 0) (3 1)))
|
||||
|
||||
(define n*1*2 (list/e nat/e (below/e 1) (below/e 2)))
|
||||
(check-range? n*1*2 0 1 '((0 0 0)))
|
||||
(check-range? n*1*2 1 4 '((0 0 1) (1 0 0) (1 0 1)))
|
||||
(check-range? n*1*2 4 6 '((2 0 0) (2 0 1)))
|
||||
(check-range? n*1*2 4 6 '((3 0 0) (3 0 1)))
|
||||
|
||||
(define n*2*4 (list/e nat/e (below/e 2) (below/e 4)))
|
||||
(check-range? n*2*4 0 1 '((0 0 0)))
|
||||
(check-range? n*2*4 1 8 '((0 0 1) (0 1 1) (0 1 0)
|
||||
(1 0 0) (1 0 1) (1 1 0) (1 1 1)))
|
||||
(check-range? n*2*4 8 18 ;; (8 previous . + . (2 magnitude of exhausted enums
|
||||
;; . * . (9 3^(number left) . - . 4 2^(number left)))
|
||||
|
||||
'((0 0 2) (0 1 2)
|
||||
(1 0 2) (1 1 2)
|
||||
(2 0 0) (2 1 0)
|
||||
(2 0 1) (2 1 1)
|
||||
(2 0 2) (2 1 2)))
|
||||
(check-range? n*2*4 18 32 ;; 18 + (2 * (4^2 - 3^2))
|
||||
'((0 0 3) (0 1 3)
|
||||
(1 0 3) (1 1 3)
|
||||
(2 0 3) (2 1 3)
|
||||
(3 0 0) (3 1 0)
|
||||
(3 0 1) (3 1 1)
|
||||
(3 0 2) (3 1 2)
|
||||
(3 0 3) (3 1 3)))
|
||||
(check-range? n*2*4 32 38
|
||||
'((4 0 0) (4 0 1) (4 0 2) (4 0 3)
|
||||
(4 1 0) (4 1 1) (4 1 2) (4 1 3)))
|
||||
(check-range? n*2*4 38 46
|
||||
'((5 0 0) (5 0 1) (5 0 2) (5 0 3)
|
||||
(5 1 0) (5 1 1) (5 1 2) (5 1 3)))
|
||||
|
||||
(check-bijection? (list/e bool/e (cons/e bool/e bool/e) (fin/e 'foo 'bar 'baz)))
|
||||
(check-bijection? (list/e nat/e string/e (many/e bool/e)))
|
||||
(check-bijection? (list/e bool/e nat/e int/e string/e (cons/e bool/e bool/e))))
|
||||
|
|
@ -344,8 +348,7 @@
|
|||
|
||||
;; dep/e tests
|
||||
(define (up-to n)
|
||||
(take/e nat/e (+ n 1)))
|
||||
|
||||
(below/e (add1 n)))
|
||||
(define 3-up
|
||||
(dep/e
|
||||
(from-list/e '(0 1 2))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user