Fix redex repeat enum bug.
Also small api change, variable enumeration change (again) and more experimentation with a sound dep/e.
This commit is contained in:
Max New
parent
3899da968d
commit
1574d5c9c6
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user