From 0b663736fb297c405a0fd65f1b7f1a07ebde3112 Mon Sep 17 00:00:00 2001 From: Max New Date: Mon, 18 Nov 2013 20:13:44 -0600 Subject: [PATCH] Add redex enum support for cross patterns --- .../redex-lib/redex/private/enum.rkt | 110 +++++++++++------- .../redex-lib/redex/private/matcher.rkt | 7 +- .../redex-lib/redex/private/pat-unify.rkt | 11 +- .../redex/private/preprocess-lang.rkt | 45 +++---- .../redex-test/redex/tests/enum-test.rkt | 17 +++ 5 files changed, 119 insertions(+), 71 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index 1154e5611a..58f5f145ad 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -5,6 +5,7 @@ racket/list racket/math racket/match + racket/promise racket/set "enumerator.rkt" @@ -17,7 +18,7 @@ (provide (contract-out - [lang-enumerators (-> (listof nt?) lang-enum?)] + [lang-enumerators (-> (listof nt?) (promise/c (listof nt?)) lang-enum?)] [pat-enumerator (-> lang-enum? any/c ;; pattern enum?)] @@ -25,7 +26,10 @@ [lang-enum? (-> any/c boolean?)] [enum? (-> any/c boolean?)])) -(struct lang-enum (enums unused-var/e)) +;; nt-enums : hash[sym -o> enum] +;; cc-enums : promise/c (hash[sym -o> enum]) +;; unused-var/e : enum +(struct lang-enum (nt-enums delayed-cc-enums unused-var/e)) (struct repeat (n terms) #:transparent) (struct name-ref (name) #:transparent) (struct misname-ref (name tag) #:transparent) @@ -36,59 +40,64 @@ ;; Top level exports (define enum-ith decode) -(define (lang-enumerators lang) - (define l-enums (make-hash)) +(define (lang-enumerators lang cc-lang) + (define (make-lang-table! ht lang) + (define (enumerate-lang! cur-lang enum-f) + (for ([nt (in-list cur-lang)]) + (hash-set! ht + (nt-name nt) + (with-handlers ([exn:fail:redex? fail/e]) + (enum-f (nt-rhs nt) + nt-enums))))) + (define-values (fin-lang rec-lang) (sep-lang lang)) + (enumerate-lang! fin-lang + (λ (rhs enums) + (enumerate-rhss rhs l-enum))) + (enumerate-lang! rec-lang + (λ (rhs enums) + (thunk/e +inf.f + (λ () + (enumerate-rhss rhs l-enum))))) + ht) + (define nt-enums (make-hash)) + (define cc-enums (delay (make-hash))) (define unused-var/e (apply except/e var/e (used-vars lang))) - (define (enumerate-lang! cur-lang enum-f) - (for ([nt (in-list cur-lang)]) - (hash-set! l-enums - (nt-name nt) - (with-handlers ([exn:fail:redex? fail/e]) - (enum-f (nt-rhs nt) - l-enums))))) - (define-values (fin-lang rec-lang) (sep-lang lang)) - (enumerate-lang! fin-lang - (λ (rhs enums) - (enumerate-rhss rhs enums unused-var/e))) - (enumerate-lang! rec-lang - (λ (rhs enums) - (thunk/e +inf.f - (λ () - (enumerate-rhss rhs enums unused-var/e))))) + (define l-enum + (lang-enum nt-enums cc-enums unused-var/e)) + + (make-lang-table! nt-enums lang) + (define filled-cc-enums + (delay (make-lang-table! (force cc-enums) (force cc-lang)))) - (lang-enum l-enums unused-var/e)) + (struct-copy lang-enum l-enum [delayed-cc-enums filled-cc-enums])) (define (pat-enumerator l-enum pat) (map/e to-term (λ (_) (redex-error 'pat-enum "Enumerator is not a bijection")) - (pat/e pat - (lang-enum-enums l-enum) - (lang-enum-unused-var/e l-enum)))) + (pat/e pat l-enum))) -(define (enumerate-rhss rhss l-enums unused/e) +(define (enumerate-rhss rhss l-enum) (apply sum/e (for/list ([production (in-list rhss)]) - (pat/e (rhs-pattern production) - l-enums - unused/e)))) + (pat/e (rhs-pattern production) l-enum)))) -(define (pat/e pat l-enums unused/e) +(define (pat/e pat l-enum) (match-define (ann-pat nv pp-pat) (preprocess pat)) (map/e ann-pat (λ (ap) (values (ann-pat-ann ap) (ann-pat-pat ap))) - (env/e nv l-enums unused/e) - (pat-refs/e pp-pat l-enums unused/e))) + (env/e nv l-enum) + (pat-refs/e pp-pat l-enum))) ;; (: pat-refs/e : Pat (HashTable Symbol (Enum Pat)) (Enum Symbol) -> Enum RefPat) -(define (pat-refs/e pat nt-enums unused/e) +(define (pat-refs/e pat l-enum) (define (loop pat) (match-a-pattern pat @@ -105,10 +114,10 @@ [`(variable-prefix ,s) (var-prefix/e s)] [`variable-not-otherwise-mentioned - unused/e] + (lang-enum-unused-var/e l-enum)] [`hole (const/e the-hole)] [`(nt ,id) - (hash-ref nt-enums id)] + (lang-enum-get-nt-enum l-enum id)] [`(name ,n ,pat) (const/e (name-ref n))] [`(mismatch-name ,n ,tag) @@ -129,7 +138,7 @@ [`(side-condition ,p ,g ,e) (unsupported pat)] [`(cross ,s) - (unsupported pat)] + (lang-enum-get-cross-enum l-enum s)] [`(list ,sub-pats ...) (list/e (for/list ([sub-pat (in-list sub-pats)]) @@ -151,10 +160,10 @@ (const/e pat)])) (loop pat)) -(define/match (env/e nv l-enums unused/e) - [((env names misnames nreps) _ _) +(define/match (env/e nv l-enum) + [((env names misnames nreps) _) (define (val/e p) - (pat-refs/e p l-enums unused/e)) + (pat-refs/e p l-enum)) (define/match (misvals/e p-ts) [((cons p ts)) @@ -171,7 +180,7 @@ (define tpats/e (hash-traverse/e val/e tpats)) (many/e - (cons/e (env/e nv l-enums unused/e) + (cons/e (env/e nv l-enum) tpats/e))]) (define names-env (hash-traverse/e val/e names)) @@ -193,15 +202,14 @@ ;; to-term : (ann-pat t-env pat-with-refs) -> redex term (define/match (to-term ap) [((ann-pat nv term)) - ((refs-to-fn term) nv)]) + (strip-hide-holes ((refs-to-fn term) nv))]) ;; refs-to-fn : RefPat -> (TEnv -> Term) (define (refs-to-fn refpat) (match refpat - [(ann-pat _ _) - (define term - (to-term refpat)) - (λ (_) term)] + [(ann-pat nv term) + (λ (_) + ((refs-to-fn term) nv))] [(decomp ctx-refs termpat-refs) (define ctx-fn (refs-to-fn ctx-refs)) (define term-fn (refs-to-fn termpat-refs)) @@ -237,6 +245,12 @@ [_ (sequence-fn (list (refs-to-fn subrefpat)))]))))] [else (λ (_) refpat)])) +(define (strip-hide-holes term) + (match term + [(hide-hole t) (strip-hide-holes t)] + [(list ts ...) (map strip-hide-holes ts)] + [_ term])) + (define (plug-hole ctx term) (define (plug ctx) (match ctx @@ -255,3 +269,11 @@ (λ (x) (for/list ([f (in-list fs)]) (f x)))) + +;; lang-enum-get-nt-enum : lang-enum Symbol -> Enum +(define (lang-enum-get-nt-enum l-enum s) + (hash-ref (lang-enum-nt-enums l-enum) s)) + +;; lang-enum-get-cross-enum : lang-enum Symbol -> Enum +(define (lang-enum-get-cross-enum l-enum s) + (hash-ref (force (lang-enum-delayed-cc-enums l-enum)) s)) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/matcher.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/matcher.rkt index ad6fe0254b..adcb675bec 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/matcher.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/matcher.rkt @@ -163,7 +163,7 @@ See match-a-pattern.rkt for more details literals nt-map collapsible-nts - (lang-enumerators lang))] + #f)] [non-list-nt-table (build-non-list-nt-label lang)] [list-nt-table (build-list-nt-label lang)] [do-compilation @@ -209,7 +209,10 @@ See match-a-pattern.rkt for more details (do-compilation across-ht across-list-ht compatible-context-language) compatible-context-language))) (do-compilation clang-ht clang-list-ht lang) - (struct-copy compiled-lang clang [delayed-cclang compatible-context-language]))) + (define enumerators + (lang-enumerators lang compatible-context-language)) + (struct-copy compiled-lang clang [delayed-cclang compatible-context-language] + [enum-table enumerators]))) ;; mk-uf-sets : (listof (listof sym)) -> (hash[symbol -o> uf-set?]) ;; in the result hash, each nt maps to a uf-set that represents diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt index b7d6971377..fce052f819 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt @@ -1,10 +1,11 @@ #lang unstable/2d racket/base -(require racket/list - racket/contract - racket/set - racket/match +(require racket/contract racket/function + racket/list + racket/match + racket/promise + racket/set "match-a-pattern.rkt" "matcher.rkt" "lang-struct.rkt" @@ -849,7 +850,7 @@ (define empty-lang (compiled-lang #f #f #f #f #f #f #f #f #f #f '() #f (hash) - (lang-enumerators '()))) + (lang-enumerators '() (delay '())))) (define unique-name-nums (make-parameter 0)) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt index 39a6e2f012..6b098c2214 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-lang.rkt @@ -24,10 +24,10 @@ ;; sorts rhs's so that recursive ones go last (define (sep-lang lang) (define (filter-edges edges lang) - (for/fold ([ht (hash)]) + (for/fold ([filtered (hash)]) ([nt (in-list lang)]) (define name (nt-name nt)) - (hash-set ht name (hash-ref edges name)))) + (hash-set filtered name (hash-ref edges name)))) (define edges (find-edges lang)) (define cyclic-nts (find-cycles edges)) (define-values (cyclic non-cyclic) @@ -55,10 +55,22 @@ (λ (rhs) (let loop ([pat (rhs-pattern rhs)] [s (set)]) - (match-a-pattern/single-base-case + (match-a-pattern pat - - [`(name ,name ,pat) + [`any s] + [`number s] + [`string s] + [`natural s] + [`integer s] + [`real s] + [`boolean s] + [`variable s] + [`(variable-except ,var ...) s] + [`(variable-prefix ,var) s] + [`variable-not-otherwise-mentioned s] + [`hole s] + [`(nt ,id) (set-add s id)] + [`(name ,var ,pat) (loop pat s)] [`(mismatch-name ,name ,pat) (loop pat s)] @@ -66,7 +78,8 @@ (set-union (loop p1 s) (loop p2 s))] [`(hide-hole ,p) (loop p s)] - [`(side-condition ,p ,_ ,_) (loop p s)] + [`(side-condition ,p ,_1 ,_2) (loop p s)] + [`(cross ,id) (set-add s id)] [`(list ,sub-pats ...) (fold-map/set (λ (sub-pat) @@ -75,11 +88,7 @@ (loop pat s)] [else (loop sub-pat s)])) sub-pats)] - [_ (match pat - [`(nt ,id) - (set-add s id)] - [_ s]) - ]))) + [(? (compose not pair?)) s]))) (nt-rhs nt)))) (hash) lang)) @@ -96,8 +105,7 @@ (λ (next) (rec next (set-add seen cur))) - (set->list (hash-ref edges - cur)))])) + (set->list (hash-ref edges cur (set))))])) (set-add s v) s)) (set) @@ -120,8 +128,7 @@ [`(variable-prefix ,s) #f] [`variable-not-otherwise-mentioned #f] [`hole #f] - [`(nt ,id) - (set-member? recs id)] + [`(nt ,id) (set-member? recs id)] [`(name ,name ,pat) (rec pat)] [`(mismatch-name ,name ,pat) @@ -130,9 +137,8 @@ (or (rec p1) (rec p2))] [`(hide-hole ,p) (rec p)] - ;; not sure about these 2, but they are unsupported by enum anyway - [`(side-condition ,p ,g ,e) #f] - [`(cross ,s) #f] + [`(side-condition ,p ,g ,e) #f] + [`(cross ,s) (set-member? recs s)] [`(list ,sub-pats ...) (ormap (λ (sub-pat) (match sub-pat @@ -220,7 +226,6 @@ ;; directly-used-nts : pat -> (setof symbol) (define (directly-used-nts pat) (match-a-pattern/single-base-case pat - [`(name ,n ,p) (directly-used-nts p)] [`(mismatch-name ,n ,p) @@ -243,6 +248,7 @@ sub-pats)] [_ (match pat [`(nt ,id) (set id)] + [`(cross ,id) (set id)] [_ (set)])])) ;; used-vars : lang -> (listof symbol) @@ -274,7 +280,6 @@ (set-union (loop p1) (loop p2))] [`(hide-hole ,p) (loop p)] - ;; not sure about these 2, but they are unsupported by enum anyway [`(side-condition ,p ,g ,e) (set)] [`(cross ,s) (set)] [`(list ,sub-pats ...) 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 6e27e92c86..8f08eb1f04 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt @@ -155,3 +155,20 @@ (try-it 4 Holes ctx) (try-it 100 Holes i) (try-it 100 Holes i2) +(try-it 1 Holes hole) +(try-it 100 Holes (in-hole hole number)) + +;; Cross test +(define-language CrossLang + (e (e e) + (λ (x) e) + x) + (x variable-not-otherwise-mentioned)) + +(try-it 100 CrossLang e) +(try-it 100 CrossLang x) +(try-it 100 CrossLang (cross e)) +(try-it 1 CrossLang (cross x)) +(try-it 100 CrossLang (in-hole (cross x) e)) +(try-it 100 CrossLang (in-hole (cross e) x)) +