Memoized redex dependent enumeration.
This commit is contained in:
Max New
Robby Findler
parent
88c5cf6f0e
commit
72544723b5
|
|
@ -1,7 +1,8 @@
|
||||||
#lang racket/base
|
#lang racket/base
|
||||||
(require racket/math
|
(require racket/math
|
||||||
racket/list
|
racket/list
|
||||||
racket/function)
|
racket/function
|
||||||
|
data/gvector)
|
||||||
|
|
||||||
(provide enum
|
(provide enum
|
||||||
enum?
|
enum?
|
||||||
|
|
@ -369,66 +370,130 @@
|
||||||
1))
|
1))
|
||||||
2)))
|
2)))
|
||||||
|
|
||||||
|
;; dep/enum : enum a (a -> enum b) -> enum (a, b)
|
||||||
;; dep/enum : enum a (a -> enum b) -> enum (a,b)
|
|
||||||
(define (dep/enum e f)
|
(define (dep/enum e f)
|
||||||
(cond [(= 0 (size e)) empty/enum]
|
(define (search-size sizes n)
|
||||||
[(not (infinite? (size (f (decode e 0)))))
|
(define (loop cur)
|
||||||
(enum (if (infinite? (size e))
|
(let* ([lastSize (gvector-ref sizes (- cur 1))]
|
||||||
+inf.f
|
[e2 (f (decode e cur))]
|
||||||
(foldl + 0 (map (compose size f) (to-list e))))
|
[s (+ lastSize (size e2))])
|
||||||
(λ (n) ;; n -> axb
|
(gvector-add! sizes s)
|
||||||
(let loop ([ei 0]
|
(if (> s n)
|
||||||
[seen 0])
|
cur
|
||||||
(let* ([a (decode e ei)]
|
(loop (+ cur 1)))))
|
||||||
[e2 (f a)])
|
(loop (gvector-count sizes)))
|
||||||
(if (< (- n seen)
|
;; fill-table - find sizes[n], filling the table as it goes
|
||||||
(size e2))
|
;; assumption: n >= (gvector-count sizes)
|
||||||
(cons a (decode e2 (- n seen)))
|
(define (fill-table sizes n)
|
||||||
(loop (+ ei 1)
|
(let loop ([cur (gvector-count sizes)])
|
||||||
(+ seen (size e2)))))))
|
(let* ([prevSize (gvector-ref sizes (- cur 1))]
|
||||||
(λ (ab) ;; axb -> n
|
[curE (f (decode e cur))]
|
||||||
(let ([ai (encode e (car ab))])
|
[s (+ prevSize (size curE))])
|
||||||
(+ (let loop ([i 0]
|
(gvector-add! sizes s)
|
||||||
[sum 0])
|
(if (= cur n)
|
||||||
(if (>= i ai)
|
s
|
||||||
sum
|
(loop (+ cur 1))))))
|
||||||
(loop (+ i 1)
|
(if (= 0 (size e))
|
||||||
(+ sum
|
empty/enum
|
||||||
(size (f (decode e i)))))))
|
(let ([first (size (f (decode e 0)))])
|
||||||
(encode (f (car ab))
|
(cond
|
||||||
(cdr ab))))))]
|
[(not (infinite? first))
|
||||||
[(not (infinite? (size e)))
|
;; memo table caches the size of the dependent enumerators
|
||||||
(enum +inf.f
|
;; sizes[n] = # of terms with left side index <= n
|
||||||
(λ (n)
|
;; sizes : gvector int
|
||||||
(call-with-values
|
(let ([sizes (gvector first)])
|
||||||
(λ ()
|
(enum (if (infinite? (size e))
|
||||||
(quotient/remainder n (size e)))
|
+inf.f
|
||||||
(λ (q r)
|
(foldl
|
||||||
(cons (decode e r)
|
(λ (curSize acc)
|
||||||
(decode (f (decode e r)) q)))))
|
(let ([sum (+ curSize acc)])
|
||||||
(λ (ab)
|
(gvector-add! sizes sum)
|
||||||
(+ (* (size e) (encode (f (car ab)) (cdr ab)))
|
sum))
|
||||||
(encode e (car ab)))))]
|
first (map (compose size f) (cdr (to-list e)))))
|
||||||
[else ;; both infinite, same as prod/enum
|
(λ (n)
|
||||||
(enum +inf.f
|
(let* ([ind (or (find-size sizes n)
|
||||||
(λ (n)
|
(search-size sizes n))]
|
||||||
(let* ([k (floor-untri n)]
|
[l (if (= ind 0)
|
||||||
[t (tri k)]
|
0
|
||||||
[l (- n t)]
|
(gvector-ref sizes (- ind 1)))]
|
||||||
[m (- k l)]
|
[m (- n l)]
|
||||||
[a (decode e l)])
|
[x (decode e ind)]
|
||||||
(cons a
|
[e2 (f x)]
|
||||||
(decode (f a) m))))
|
[y (decode e2 m)])
|
||||||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
(cons x y)))
|
||||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
(λ (ab)
|
||||||
(unless (pair? xs)
|
(let* ([a (car ab)]
|
||||||
(error "not a pair"))
|
[b (cdr ab)]
|
||||||
(let ([l (encode e (car xs))]
|
[ai (encode e a)]
|
||||||
[m (encode (f (car xs)) (cdr xs))])
|
[ei (f a)]
|
||||||
(+ (/ (* (+ l m) (+ l m 1))
|
[nextSize (size ei)]
|
||||||
2)
|
[sizeUpTo (if (= ai 0)
|
||||||
l))))]))
|
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/enum
|
||||||
|
(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))))]))))
|
||||||
|
|
||||||
|
;; find-size : gvector int, int -> either int #f
|
||||||
|
;; binary search for the index of the smallest element of vec greater
|
||||||
|
;; than n or #f if no such element exists
|
||||||
|
(define (find-size vec n)
|
||||||
|
(define (bin-search min max)
|
||||||
|
(cond [(= min max) min]
|
||||||
|
[(= (- max min) 1)
|
||||||
|
(cond [(> (gvector-ref vec min) n)
|
||||||
|
min]
|
||||||
|
[else max])]
|
||||||
|
[else
|
||||||
|
(let ([mid (quotient (+ max min)
|
||||||
|
2)])
|
||||||
|
(cond [(> (gvector-ref vec mid) n)
|
||||||
|
(bin-search min mid)]
|
||||||
|
[else
|
||||||
|
(bin-search mid max)]))]))
|
||||||
|
(let ([size (gvector-count vec)])
|
||||||
|
(cond [(or (= size 0)
|
||||||
|
(<= (gvector-ref vec (- size 1))
|
||||||
|
n))
|
||||||
|
#f]
|
||||||
|
[else (bin-search 0 (- size 1))])))
|
||||||
|
|
||||||
;; dep2 : enum a (a -> enum b) -> enum (a,b)
|
;; dep2 : enum a (a -> enum b) -> enum (a,b)
|
||||||
(define (dep2/enum e f)
|
(define (dep2/enum e f)
|
||||||
|
|
@ -836,15 +901,25 @@
|
||||||
|
|
||||||
(check-bijection? nats-up))
|
(check-bijection? nats-up))
|
||||||
|
|
||||||
;; dep2/enum tests
|
;; find-size tests
|
||||||
|
(check-equal? (find-size (gvector) 5) #f)
|
||||||
|
(check-equal? (find-size (gvector 5) 4) 0)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 0) 0)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 1) 1)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 4) 1)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 5) 2)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 6) 2)
|
||||||
|
(check-equal? (find-size (gvector 1 5 7) 7) #f)
|
||||||
|
|
||||||
|
;; depend/enum tests
|
||||||
;; same as dep unless the right side is finite
|
;; same as dep unless the right side is finite
|
||||||
(define 3-up-2
|
(define 3-up-2
|
||||||
(dep2/enum
|
(dep/enum
|
||||||
(from-list/enum '(0 1 2))
|
(from-list/enum '(0 1 2))
|
||||||
up-to))
|
up-to))
|
||||||
|
|
||||||
(define nats-to-2
|
(define nats-to-2
|
||||||
(dep2/enum nats up-to))
|
(dep/enum nats up-to))
|
||||||
|
|
||||||
|
|
||||||
(test-begin
|
(test-begin
|
||||||
|
|
@ -855,18 +930,28 @@
|
||||||
(check-equal? (decode 3-up-2 3) (cons 2 0))
|
(check-equal? (decode 3-up-2 3) (cons 2 0))
|
||||||
(check-equal? (decode 3-up-2 4) (cons 2 1))
|
(check-equal? (decode 3-up-2 4) (cons 2 1))
|
||||||
(check-equal? (decode 3-up-2 5) (cons 2 2))
|
(check-equal? (decode 3-up-2 5) (cons 2 2))
|
||||||
(check-bijection? 3-up-2)
|
|
||||||
|
(check-equal? (encode 3-up-2 (cons 0 0)) 0)
|
||||||
|
(check-equal? (encode 3-up-2 (cons 1 0)) 1)
|
||||||
|
(check-equal? (encode 3-up-2 (cons 1 1)) 2)
|
||||||
|
(check-equal? (encode 3-up-2 (cons 2 0)) 3)
|
||||||
|
|
||||||
(check-equal? (size nats-to-2) +inf.f)
|
(check-equal? (size nats-to-2) +inf.f)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 0 0)) 0)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 1 0)) 1)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 1 1)) 2)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 2 0)) 3)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 2 1)) 4)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 2 2)) 5)
|
||||||
|
(check-equal? (encode nats-to-2 (cons 3 0)) 6)
|
||||||
|
|
||||||
(check-equal? (decode nats-to-2 0) (cons 0 0))
|
(check-equal? (decode nats-to-2 0) (cons 0 0))
|
||||||
(check-equal? (decode nats-to-2 1) (cons 1 0))
|
(check-equal? (decode nats-to-2 1) (cons 1 0))
|
||||||
(check-equal? (decode nats-to-2 2) (cons 1 1))
|
(check-equal? (decode nats-to-2 2) (cons 1 1))
|
||||||
(check-equal? (decode nats-to-2 3) (cons 2 0))
|
(check-equal? (decode nats-to-2 3) (cons 2 0))
|
||||||
(check-equal? (decode nats-to-2 4) (cons 2 1))
|
(check-equal? (decode nats-to-2 4) (cons 2 1))
|
||||||
(check-equal? (decode nats-to-2 5) (cons 2 2))
|
(check-equal? (decode nats-to-2 5) (cons 2 2))
|
||||||
(check-equal? (decode nats-to-2 6) (cons 3 0))
|
(check-equal? (decode nats-to-2 6) (cons 3 0)))
|
||||||
(check-bijection? nats-to-2)
|
|
||||||
)
|
|
||||||
|
|
||||||
;; take/enum test
|
;; take/enum test
|
||||||
(define to-2 (up-to 2))
|
(define to-2 (up-to 2))
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user