From 153a488309c5c557cd8de7a0d910771d778e0441 Mon Sep 17 00:00:00 2001 From: Max New Date: Tue, 15 Oct 2013 00:14:38 -0500 Subject: [PATCH] Get unnamed and named terms working with new env Also separate 2set into separate typed module. --- .../redex-lib/redex/private/2set.rkt | 38 ++++++ .../redex-lib/redex/private/enum.rkt | 122 +++++++++++++++--- .../redex-lib/redex/private/enumerator.rkt | 38 ++++-- .../redex-lib/redex/private/env.rkt | 48 +++++++ .../redex/private/preprocess-pat.rkt | 87 +++++++++---- .../redex-test/redex/tests/enum-test.rkt | 5 +- .../redex/tests/enumerator-test.rkt | 12 +- 7 files changed, 286 insertions(+), 64 deletions(-) create mode 100644 pkgs/redex-pkgs/redex-lib/redex/private/2set.rkt create mode 100644 pkgs/redex-pkgs/redex-lib/redex/private/env.rkt diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/2set.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/2set.rkt new file mode 100644 index 0000000000..40853b6ca6 --- /dev/null +++ b/pkgs/redex-pkgs/redex-lib/redex/private/2set.rkt @@ -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))]) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index 81f10394f0..06c0e101af 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -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) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt index 179c2ae97f..9b90eaa4e5 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt @@ -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) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt new file mode 100644 index 0000000000..a67f97cb84 --- /dev/null +++ b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt @@ -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))))]) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt index 8a06b1208a..768fe27377 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt @@ -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)) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt index 1de8a12751..1cb31c2d23 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt @@ -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) 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 ce4ebb0ae0..6459e5e102 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt @@ -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))