From 8e367fb9bbcf5097466dc0e2f8c8544547e51079 Mon Sep 17 00:00:00 2001 From: Max New Date: Sun, 10 Nov 2013 17:51:46 -0600 Subject: [PATCH] Add redex support for mismatch repeat patterns --- .../redex-lib/redex/private/enum.rkt | 29 +++++-- .../redex-lib/redex/private/enumerator.rkt | 2 +- .../redex-lib/redex/private/env.rkt | 82 +++++++++++++++---- .../redex/private/preprocess-pat.rkt | 6 +- .../redex-test/redex/tests/enum-test.rkt | 7 +- 5 files changed, 96 insertions(+), 30 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index 665d253260..634b3ff835 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -30,6 +30,7 @@ (struct lang-enum (enums unused-var/e)) (struct repeat (n terms) #:transparent) (struct name-ref (name) #:transparent) +(struct misname-ref (name tag) #:transparent) (struct nrep-ref (name subpat) #:transparent) (struct decomp (ctx term) #:transparent) (struct hide-hole (term) #:transparent) @@ -121,8 +122,8 @@ (hash-ref nt-enums id)] [`(name ,n ,pat) (const/e (name-ref n))] - [`(mismatch-name ,n ,pat) - (unimplemented "mismatch-name")] + [`(mismatch-name ,n ,tag) + (const/e (misname-ref n tag))] [`(in-hole ,p1 ,p2) (map/e decomp (match-lambda @@ -160,9 +161,20 @@ (loop pat)) (define/match (env/e nv l-enums unused/e) - [((env names nreps) _ _) + [((env names misnames nreps) _ _) (define (val/e p) (pat-refs/e p l-enums unused/e)) + + (define/match (misvals/e p-ts) + [((cons p ts)) + (define p/e (val/e p)) + (fold-enum (λ (ts-excepts tag) + (define excepts + (map cdr ts-excepts)) + (cons/e (const/e tag) + (apply except/e p/e excepts))) + (set->list ts))]) + (define/match (reprec/e nv-t) [((cons nv tpats)) (define tpats/e @@ -172,15 +184,19 @@ tpats/e))]) (define names-env (hash-traverse/e val/e names)) + + (define misnames-env + (hash-traverse/e misvals/e misnames)) (define nreps-env (hash-traverse/e reprec/e nreps)) (map/e t-env (match-lambda - [(t-env names nreps) - (values names nreps)]) + [(t-env names misnames nreps) + (values names misnames nreps)]) names-env + misnames-env nreps-env)]) ;; to-term : (ann-pat t-env pat-with-refs) -> redex term @@ -209,6 +225,9 @@ [(name-ref n) (λ (nv) (t-env-name-ref nv n))] + [(misname-ref n tag) + (λ (nv) + ((refs-to-fn (t-env-misname-ref nv n tag)) nv))] [(list subrefpats ...) (compose append* diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt index f77561b683..0783db2fd3 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt @@ -99,7 +99,7 @@ (loop (+ i 1) seen))))) (λ (x) (encode e x)))) -;; except/e : enum a, a -> enum a +;; except/e : (enum a) a* -> (enum a) ;; Everything inside e MUST be in the enumerator or you will get a redex-error (define (except/e e . excepts) (define (except1/e x e) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt index 5f51894046..c4ba10af4c 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt @@ -2,14 +2,17 @@ (require/typed "error.rkt" [redex-error (Symbol String Any * -> Nothing)]) +(require racket/set) (provide (struct-out env) empty-env add-name + add-mismatch pure-nrep env-union (struct-out t-env) t-env-name-ref + t-env-misname-ref t-env-nrep-ref) ;; For now, accept any pattern @@ -20,24 +23,43 @@ (define-type Tag Integer) (define-type (Tagged a) (HashTable Tag a)) -(struct: env ([names : (HashTable Symbol Pattern)] - [nreps : (HashTable Symbol (Pairof Env (Tagged Pattern)))]) +(struct: env ([names : (HashTable Symbol Pattern)] + [misnames : (HashTable Symbol (Pairof Pattern (Setof Tag)))] + [nreps : (HashTable Symbol (Pairof Env (Tagged Pattern)))]) #:transparent) -(struct: t-env ([names : (HashTable Symbol Term)] - [nreps : (HashTable Symbol (Listof (Pairof TEnv (Tagged Term))))]) +(struct: t-env ([names : (HashTable Symbol Term)] + [misnames : (HashTable Symbol (Listof (Pairof Tag Term)))] + [nreps : (HashTable Symbol (Listof (Pairof TEnv (Tagged Term))))]) #:transparent) (: empty-env : Env) (define empty-env - (env (hash) (hash))) + (env (hash) (hash) (hash))) + +(: empty-t-env : TEnv) +(define empty-t-env + (t-env (hash) (hash) (hash))) (: add-name : Env Symbol Pattern -> Env) (define/match (add-name e n p) - [((env names nreps) _ _) + [((env names misnames nreps) _ _) (define (default) p) (define update identity) - (env (hash-update names n update default) nreps)]) + (env (hash-update names n update default) misnames nreps)]) + +(: add-mismatch : Env Symbol Pattern Tag -> Env) +(define/match (add-mismatch e n p t) + [((env names misnames nreps) _ _ _) + (: default : -> (Pairof Pattern (Setof Tag))) + (define (default) (cons p (set t))) + (: update : (Pairof Pattern (Setof Tag)) -> (Pairof Pattern (Setof Tag))) + (define/match (update p-ts) + [((cons p ts)) + (cons p (set-add ts t))]) + (env names + (hash-update misnames n update default) + nreps)]) (: pure-nrep : Symbol Env Tag Pattern -> Env) (define (pure-nrep n repnv tag pat) @@ -49,29 +71,53 @@ (hash-set (ann (hash) (Tagged Pattern)) tag pat)))) - (env (hash) - nreps)) + (env (hash) (hash) nreps)) -(: t-env-name-ref : TEnv Symbol -> Pattern) +(: t-env-name-ref : TEnv Symbol -> Term) (define/match (t-env-name-ref e n) - [((t-env names _) _) + [((t-env names _ _) _) (hash-ref names n (thunk (redex-error 't-env-name-ref "name not found: ~s" n)))]) +(: t-env-misname-ref : TEnv Symbol Tag -> Term) +(define/match (t-env-misname-ref te m tag) + [((t-env _ misnames _) _ _) + (define tagged-terms + (hash-ref misnames m (thunk (redex-error 't-env-misname-ref "mismatch name not found: ~s" m)))) + (define maybe-term + (assoc tag tagged-terms)) + (cond [maybe-term (cdr maybe-term)] + [else (redex-error 't-env-misname-ref "mismatch name tag not found: ~s" tag)])]) + (: t-env-nrep-ref : TEnv Symbol -> (Listof (Pairof TEnv Term))) (define/match (t-env-nrep-ref nv n) - [((t-env _ nreps) n) + [((t-env _ _ nreps) n) (hash-ref nreps n (thunk (redex-error 't-env-nrep-ref "repeat not found: ~s" n)))]) (: env-union : Env Env -> Env) (define/match (env-union e1 e2) - [((env ns1 rs1) (env ns2 rs2)) + [((env ns1 ms1 rs1) (env ns2 ms2 rs2)) (define names-union (hash-union ns1 ns2 - (λ (_ v1 v2) v1))) - (: combo : Symbol (Pairof Env (Tagged Pattern)) (Pairof Env (Tagged Pattern)) -> (Pairof Env (Tagged Pattern))) - (define/match (combo _ e-t1 e-t2) + (λ (_ v1 v2) + (unless (equal? v1 v2) + (redex-error 'generate-term-#:ith "named patterns must be the same pattern")) + v1))) + + (: mis-combo : Symbol (Pairof Pattern (Setof Tag)) (Pairof Pattern (Setof Tag)) -> (Pairof Pattern (Setof Tag))) + (define/match (mis-combo k pts1 pts2) + [(_ (cons p1 ts1) (cons p2 ts2)) + (unless (equal? p1 p2) + (redex-error 'generate-term-#:ith "mismatch named patterns must be the same pattern")) + (cons p1 (set-union ts1 ts2))]) + + (: misnames-union : (HashTable Symbol (Pairof Pattern (Setof Tag)))) + (define misnames-union + (hash-union ms1 ms2 mis-combo)) + + (: nrep-combo : Symbol (Pairof Env (Tagged Pattern)) (Pairof Env (Tagged Pattern)) -> (Pairof Env (Tagged Pattern))) + (define/match (nrep-combo _ e-t1 e-t2) [(_ (cons nv1 t1) (cons nv2 t2)) (cons (env-union nv1 nv2) (hash-union t1 t2 @@ -80,8 +126,8 @@ "2 tags should never collide, but these did: ~s, ~s with tag: ~s in envs ~s and ~s" _1 _2 t e1 e2))))]) (define nreps-union - (hash-union rs1 rs2 combo)) - (env names-union nreps-union)]) + (hash-union rs1 rs2 nrep-combo)) + (env names-union misnames-union nreps-union)]) (: key-set : (All (k v) (HashTable k v) -> (Setof k))) (define (key-set m) 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 f124778982..d815369c0d 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt @@ -28,8 +28,10 @@ (ann-pat (add-name subenv n subpat) `(name ,n ,new-subpat))] [`(mismatch-name ,n ,subpat) - ;; TODO - (unimplemented "mismatch-name")] + (match-define (ann-pat subenv new-subpat) (walk subpat)) + (define tag (get-and-inc!)) + (ann-pat (add-mismatch subenv n subpat tag) + `(mismatch-name ,n ,tag))] [`(in-hole ,p1 ,p2) (match-define (ann-pat subenv1 newsub1) (walk p1)) 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 a6f4aa269c..28118be448 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt @@ -100,11 +100,10 @@ (p (number_!_1 number_!_1)) (n (p_!_1 p_!_1)) (x number)) -;; Mismatch isn't working for now, will come back to this. -;; (try-it 100 M m) -;; (try-it 100 M n) -;; (try-it 100 M p) +(try-it 100 M m) +(try-it 100 M n) +(try-it 100 M p) ;; test variable filtering (define-language Vars