suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Get unnamed and named terms working with new env

Browse Source 
Also separate 2set into separate typed module.
This commit is contained in:
Max New 2013-10-15 00:14:38 -05:00
parent 5d5522ad4c
commit 153a488309
7 changed files with 286 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
pkgs/redex-pkgs/redex-lib/redex/private/2set.rkt Normal file
View File

@ -0,0 +1,38 @@
#lang typed/racket/base
(require racket/match
racket/set)
(provide 2Setof
(rename-out [mk-2set 2set]
[2set-set1 2set-ones]
[2set-set2 2set-manys])
2set-add
2set-union)
(define-type (2Setof A) (2set A))
(struct: (A) 2set ([set1 : (Setof A)]
[set2 : (Setof A)]))
(: mk-2set : (All (a) (a * -> (2Setof a))))
(define (mk-2set . xs)
(for/fold ([acc (2set (ann (set) (Setof a))
(ann (set) (Setof a)))])
([x (in-list xs)])
(2set-add acc x)))
(: 2set-add : (All (a) ((2Setof a) a * -> (2Setof a))))
(define (2set-add ts . xs)
(for/fold ([acc ts])
([x (in-list xs)])
(match-define (2set ones manys) acc)
(cond [(set-member? ones x)
(2set ones (set-add manys x))]
[else (2set (set-add ones x) manys)])))
(: 2set-union : (All (a) ((2Setof a) (2Setof a) -> (2Setof a))))
(define/match (2set-union ts1 ts2)
[((2set s11 s12) (2set s21 s22))
(define common (set-intersect s11 s21))
(2set (set-union s11 s21)
(set-union s12 s22 common))])

122
pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
View File

@ -6,6 +6,7 @@
racket/set
"enumerator.rkt"
"env.rkt"
"lang-struct.rkt"
"match-a-pattern.rkt"
"preprocess-pat.rkt"
@ -45,14 +46,12 @@
(except/e var/e
(used-vars lang)))
(define (enumerate-lang cur-lang enum-f)
(for-each
(λ (nt)
(hash-set! l-enums
(for ([nt (in-list cur-lang)])
(hash-set! l-enums
(nt-name nt)
(with-handlers ([exn:fail? fail/e])
(enum-f (nt-rhs nt)
l-enums))))
cur-lang))
l-enums)))))
(let-values ([(fin-lang rec-lang)
(sep-lang lang)])
(enumerate-lang fin-lang
@ -68,8 +67,7 @@
(define (pat-enumerator l-enum pat)
(map/e
to-term
;;identity
fill-refs
(λ (_)
(error 'pat-enum "Enumerator is not a bijection"))
(pat/e pat
@ -78,19 +76,88 @@
(define (enumerate-rhss rhss l-enums unused/e)
(apply sum/e
(map
(λ (rhs)
(pat/e (rhs-pattern rhs)
l-enums
unused/e))
rhss)))
(for/list ([production (in-list rhss)])
(pat/e (rhs-pattern production)
l-enums
unused/e))))
(define (pat/e pat l-enums unused/e)
(define processed (preprocess pat))
(enum-names processed
(sep-names processed)
l-enums
unused/e))
(match-define (ann-pat nv pp-pat) (preprocess pat))
(map/e
(λ (e-p)
(ann-pat (car e-p) (cdr e-p)))
(λ (ap)
(cons (ann-pat-ann ap)
(ann-pat-pat ap)))
(cons/e (env/e nv l-enums unused/e)
(pat-refs/e pp-pat l-enums unused/e))))
(define (pat-refs/e pat nt-enums unused/e)
(define (loop pat)
(match-a-pattern
pat
[`any (sum/e any/e (many/e any/e))]
[`number num/e]
[`string string/e]
[`natural natural/e]
[`integer integer/e]
[`real real/e]
[`boolean bool/e]
[`variable var/e]
[`(variable-except ,s ...)
(except/e var/e s)]
[`(variable-prefix ,s)
;; todo
(error 'unimplemented "var-prefix")]
[`variable-not-otherwise-mentioned
unused/e]
[`hole
(const/e the-hole)]
[`(nt ,id)
(hash-ref nt-enums id)]
[`(name ,n ,pat)
(const/e (name-ref n))]
[`(mismatch-name ,n ,pat)
(const/e (mismatch-ref n))]
[`(in-hole ,p1 ,p2) ;; untested
(map/e
(λ (ts)
(decomposition (car ts)
(cdr ts)))
(λ (decomp)
(cons (decomposition-ctx decomp)
(decomposition-term decomp)))
(cons/e
(loop p1)
(loop p2)))]
[`(hide-hole ,p)
(loop p)]
[`(side-condition ,p ,g ,e)
(unsupported pat)]
[`(cross ,s)
(unsupported pat)]
[`(list ,sub-pats ...)
;; enum-list
(list/e
(for/list ([sub-pat (in-list sub-pats)])
(match sub-pat
[`(repeat ,pat ,n ,m)
(error 'unimplemented "repeats")]
[else (loop sub-pat)])))]
[(? (compose not pair?))
(const/e pat)]))
(loop pat))
(define (env/e nv l-enums unused/e)
(define names (env-names nv))
(define (val/e p)
(pat/e p l-enums unused/e))
(define names-env
(hash-traverse/e val/e names))
(map/e
env
env-names
names-env))
(define (map-nt-rhs-pat f nonterminal)
(nt (nt-name nonterminal)
@ -409,7 +476,7 @@
[`hole
(const/e the-hole)]
[`(nt ,id)
(hash-ref nt-enums id)]
(fill-refs (hash-ref nt-enums id))]
[`(name ,n ,pat)
(const/e (name-ref n))]
[`(mismatch-name ,n ,pat)
@ -422,7 +489,7 @@
(λ (decomp)
(cons (decomposition-ctx decomp)
(decomposition-term decomp)))
(prod/e
(cons/e
(loop p1)
(loop p2)))]
[`(hide-hole ,p)
@ -521,6 +588,21 @@
bool/e
var/e))
;; fill-refs : (ann-pat env pat-with-refs) -> redex term
(define/match (fill-refs ap)
[((ann-pat nv term))
(define (rec term)
(cond [(ann-pat? term)
(fill-refs term)]
[(name-ref? term)
(fill-refs (env-name-ref nv (name-ref-name term)))]
[(decomposition? term)
(error 'unsupported "in-hole")]
[(list? term)
(map rec term)]
[else term]))
(rec term)])
;; to-term : augmented term -> redex term
(define (to-term aug)
(cond [(named? aug)

38
pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt
View File

@ -14,7 +14,7 @@
const/e
from-list/e
sum/e
prod/e
cons/e
dep/e
dep2/e ;; requires size (eventually should replace dep/e with this)
map/e
@ -25,6 +25,7 @@
many1/e
list/e
traverse/e
hash-traverse/e
fail/e
@ -288,8 +289,8 @@
l))) ;; (n,m) -> (n+m)(n+m+1)/2 + n
))
;; prod/e : enum a, enum b -> enum (a,b)
(define prod/e
;; cons/e : enum a, enum b -> enum (cons a b)
(define cons/e
(case-lambda
[(e) e]
[(e1 e2)
@ -365,14 +366,29 @@
2)
l))))])]
[(a b c . rest)
(prod/e a (apply prod/e b c rest))]))
(cons/e a (apply cons/e b c rest))]))
;; Traversal (maybe come up with a better name
;; traverse/e : (a -> enum b), (listof a) -> enum (listof b)
(define (traverse/e f xs)
(list/e (map f xs)))
;; sequence/e : listof (enum a) -> enum (listof a)
;; Hash Traversal
;; hash-traverse/e : (a -> enum b), (hash[k] -o> a) -> enum (hash[k] -o> b)
(define (hash-traverse/e f ht)
;; as-list : listof (cons k a)
(define as-list (hash->list ht))
;; on-cdr : (cons k a) -> enum (cons k b)
(define/match (on-cdr pr)
[((cons k v))
(cons/e (const/e k)
(f v))])
;; enum (listof (cons k b))
(define assoc/e
(traverse/e on-cdr as-list))
(map/e make-immutable-hash
hash->list
assoc/e))
;; the nth triangle number
(define (tri n)
@ -471,7 +487,7 @@
(λ (ab)
(+ (* (size e) (encode (f (car ab)) (cdr ab)))
(encode e (car ab)))))]
[else ;; both infinite, same as prod/e
[else ;; both infinite, same as cons/e
(enum +inf.f
(λ (n)
(let* ([k (floor-untri n)]
@ -596,7 +612,7 @@
(λ (ab)
(+ (* (size e) (encode (f (car ab)) (cdr ab)))
(encode e (car ab)))))]
[else ;; both infinite, same as prod/e
[else ;; both infinite, same as cons/e
(enum +inf.f
(λ (n)
(let* ([k (floor-untri n)]
@ -693,17 +709,19 @@
(λ ()
(sum/e
(const/e '())
(prod/e e (many/e e)))))]
(cons/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)))
(cons/e e (many/e e)))
;; list/e : listof (enum any) -> enum (listof any)
(define (list/e es)
(apply prod/e (append es `(,(const/e '())))))
(foldr cons/e
(const/e '())
es))
(define (nats+/e n)
(map/e (λ (k)

48
pkgs/redex-pkgs/redex-lib/redex/private/env.rkt Normal file
View File

@ -0,0 +1,48 @@
#lang typed/racket
(provide env
env?
empty-env
add-name
env-name-ref
env-union
env-names)
;; For now, accept any pattern
(define-type Pattern Any)
(define-type Tag Number)
(define-type Env env)
(struct: env ([names : (HashTable Symbol Pattern)])
#:transparent)
(: empty-env : Env)
(define empty-env
(env (hash)))
(: add-name : Env Symbol Pattern -> Env)
(define/match (add-name e n p)
[((env names) _ _)
(define (default) p)
(define update identity)
(env (hash-update names n update default))])
(: env-name-ref : Env Symbol -> Pattern)
(define/match (env-name-ref e n)
[((env names) _)
(hash-ref names n (λ () (error (format "env-name-ref: name not found: ~s" n))))])
(: env-union : Env Env -> Env)
(define/match (env-union e1 e2)
[((env ns1) (env ns2))
(define ks1 (list->set (hash-keys ns1)))
(define ks2 (list->set (hash-keys ns2)))
;; For some reason in-set is not typed so I can't use it
(env (for/hash: : (HashTable Symbol Pattern)
([k : Symbol (set-union ks1 ks2)])
(: ref-default : (HashTable Symbol Pattern) -> Pattern)
(define (ref-default ns)
(hash-ref ns k (thunk #f)))
(match-define p1 (ref-default ns1))
(match-define p2 (ref-default ns2))
(values k (or p1 p2))))])

87
pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt
View File

@ -2,37 +2,63 @@
(require racket/match
racket/set
"2set.rkt"
"env.rkt"
"match-a-pattern.rkt")
(provide preprocess)
;; A set that knows if an element has been added more than once
(struct 2set (set1 set2))
(define 2set-empty (2set (set) (set)))
(define (2set-add ts . xs)
(foldr (λ (x ts)
(match ts
[(2set s1 s2)
(if (set-member? s1 x)
(2set s1 (set-add s2 x))
(2set (set-add s1 x) s2))]))
ts
xs))
(define/match (2set-union ts1 ts2)
[((2set s11 s12) (2set s21 s22))
(define common (set-intersect s11 s21))
(2set (set-union s11 s21)
(set-union s12 s22 common))])
(provide preprocess
(struct-out ann-pat))
;; preprocess : pat -> (ann-pat env pat)
(define (preprocess pat)
(remove-names pat))
(build-env (remove-names pat)))
;; This function returns an env containing all top-level name references, i.e., the ones that need to be enumerated doing anything
(define (build-env pat)
(define (walk pat)
(match-a-pattern/single-base-case pat
[`(name ,n ,subpat)
(match-define (ann-pat subenv _) (walk subpat))
(ann-pat (add-name subenv n subpat)
pat)]
[`(mismatch-name ,n ,subpat)
;; TODO
(error 'unimplemented)]
[`(in-hole ,p1 ,p2)
(match-define (ann-pat subenv1 _)
(walk p1))
(match-define (ann-pat subenv2 _)
(walk p2))
(ann-pat (env-union subenv1 subenv2) pat)]
[`(hide-hole ,p)
(match-define (ann-pat subenv _)
(walk p))
(ann-pat subenv pat)]
[`(side-condition ,p ,c ,s)
(error 'unsupported "side condition is not supported.")]
[`(list ,sub-pats ...)
(define ann-sub-pats
(for/list ([sub-pat (in-list sub-pats)])
(match sub-pat
[`(repeat ,p ,n ,m)
(error 'unimplemented)]
[_ (walk sub-pat)])))
(define list-env
(for/fold ([accenv empty-env])
([sub-apat (in-list ann-sub-pats)])
(match sub-apat
[(ann-pat subenv _)
(env-union subenv accenv)])))
(ann-pat list-env pat)]
[_ (pure-ann-pat pat)]))
(walk pat))
(define (remove-names pat)
(match-define (2set names 2names) (find-names pat))
(define names-2set (find-names pat))
(define names (2set-ones names-2set))
(define 2names (2set-manys names-2set))
(define badnames (set-subtract names 2names))
(define (strip-named name subpat con)
(define sub-stripped (strip subpat))
@ -85,10 +111,17 @@
(find-names p)]
[`(list ,sub-pats ...)
(foldr 2set-union
2set-empty
(2set)
(map (match-lambda
[`(repeat ,p ,n ,m)
(2set-add (find-names p) n m)]
[sub-pat (find-names sub-pat)])
sub-pats))]
[_ 2set-empty]))
[_ (2set)]))
;; Patterns annotated with variable/name/repeat information
(struct ann-pat (ann pat)
#:transparent)
(define (pure-ann-pat pat)
(ann-pat empty-env pat))

5
pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt
View File

@ -16,6 +16,10 @@
(generate-term l p #:i-th i))
(error 'bad-term "line ~a: i=~a" line i)))))))]))
(define-language Nats
(n natural))
(try-it 100 Nats n)
;; Repeat test
(define-language Rep
(r (variable variable ...)))
@ -29,7 +33,6 @@
x)
(x (variable-except λ)))
;; slow: fix dep/enum
(try-it 250 Λc e)
(try-it 24 Λc x)

12
pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt
View File

@ -132,12 +132,12 @@
(check-equal? (encode odd-or-even 3) 3)
(check-bijection? odd-or-even)))
;; prod/e tests
(define bool*bool (prod/e bools/e bools/e))
(define 1*b (prod/e (const/e 1) bools/e))
(define bool*nats (prod/e bools/e nats))
(define nats*bool (prod/e nats bools/e))
(define nats*nats (prod/e nats nats))
;; cons/e tests
(define bool*bool (cons/e bools/e bools/e))
(define 1*b (cons/e (const/e 1) bools/e))
(define bool*nats (cons/e bools/e nats))
(define nats*bool (cons/e nats bools/e))
(define nats*nats (cons/e nats nats))
(define ns-equal? (λ (ns ms)
(and (= (car ns)
(car ms))