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

Add redex support for mismatch repeat patterns

Browse Source
This commit is contained in:
Max New 2013-11-10 17:51:46 -06:00
parent aba0880dda
commit 8e367fb9bb
5 changed files with 96 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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*

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

@ -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)

82
pkgs/redex-pkgs/redex-lib/redex/private/env.rkt
View File

@ -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)

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

@ -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))

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

@ -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