Implement 1-level named repeats with named patterns inside.
This commit is contained in:
Max New
parent
5fbcc62e9a
commit
3b64ee8c81
|
|
@ -34,6 +34,7 @@
|
|||
|
||||
(struct name-ref (name) #:transparent)
|
||||
(struct mismatch-ref (name) #:transparent)
|
||||
(struct nrep-ref (name subpat) #:transparent)
|
||||
|
||||
(struct named-pats (names map) #:transparent
|
||||
) ;; listof symbol and hash symbol -o> (or named, mismatched, named-repeat, mismatch-repeat)
|
||||
|
|
@ -84,14 +85,14 @@
|
|||
(define (pat/e pat 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)))
|
||||
ann-pat
|
||||
(λ (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))))
|
||||
(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)))
|
||||
|
||||
;; (: pat-refs/e : Pat (HashTable Symbol (Enum Pat)) (Enum Symbol) -> Enum RefPat)
|
||||
(define (pat-refs/e pat nt-enums unused/e)
|
||||
(define (loop pat)
|
||||
(match-a-pattern
|
||||
|
|
@ -118,46 +119,59 @@
|
|||
[`(name ,n ,pat)
|
||||
(const/e (name-ref n))]
|
||||
[`(mismatch-name ,n ,pat)
|
||||
(const/e (mismatch-ref n))]
|
||||
(unimplemented "mismatch-name")]
|
||||
[`(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)))]
|
||||
(unsupported pat)]
|
||||
[`(hide-hole ,p)
|
||||
(loop p)]
|
||||
(unsupported pat)]
|
||||
[`(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 #f #f)
|
||||
(map/e
|
||||
(λ (ts)
|
||||
(repeat (length ts)
|
||||
ts))
|
||||
(λ (rep)
|
||||
(repeat-terms rep))
|
||||
(many/e (loop pat)))]
|
||||
[`(repeat ,tag ,n #f)
|
||||
(const/e (nrep-ref n tag))]
|
||||
[`(repeat ,pat ,n ,m)
|
||||
(error 'unimplemented "repeats")]
|
||||
(unimplemented "mismatch 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/match (env/e nv l-enums unused/e)
|
||||
[((env names nreps) _ _)
|
||||
(define (val/e p)
|
||||
(pat-refs/e p l-enums unused/e))
|
||||
(define/match (reprec/e nv-t)
|
||||
[((cons nv tpats))
|
||||
(define tpats/e
|
||||
(hash-traverse/e val/e tpats))
|
||||
(many/e
|
||||
(cons/e (env/e nv l-enums unused/e)
|
||||
tpats/e))])
|
||||
(define names-env
|
||||
(hash-traverse/e val/e names))
|
||||
|
||||
(define nreps-env
|
||||
(hash-traverse/e reprec/e nreps))
|
||||
(map/e
|
||||
t-env
|
||||
(match-lambda
|
||||
[(t-env names nreps)
|
||||
(values names nreps)])
|
||||
names-env
|
||||
nreps-env)])
|
||||
|
||||
(define (map-nt-rhs-pat f nonterminal)
|
||||
(nt (nt-name nonterminal)
|
||||
|
|
@ -586,24 +600,44 @@
|
|||
bool/e
|
||||
var/e))
|
||||
|
||||
;; fill-refs : (ann-pat env pat-with-refs) -> redex term
|
||||
;; fill-refs : (ann-pat t-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)
|
||||
(append*
|
||||
(for/list ([sub-term (in-list term)])
|
||||
(cond [(repeat? sub-term)
|
||||
(map rec (repeat-terms sub-term))]
|
||||
[else (list (rec sub-term))])))]
|
||||
[else term]))
|
||||
(rec term)])
|
||||
((refs-to-fn term) nv)])
|
||||
|
||||
;; refs-to-fn : RefPat -> (TEnv -> Term)
|
||||
(define (refs-to-fn refpat)
|
||||
(match refpat
|
||||
[(ann-pat _ _)
|
||||
(define term
|
||||
(fill-refs refpat))
|
||||
(λ (_) term)]
|
||||
[(name-ref n)
|
||||
(λ (nv)
|
||||
(t-env-name-ref nv n))]
|
||||
[(list subrefpats ...)
|
||||
(compose
|
||||
append*
|
||||
(sequence-fn
|
||||
(for/list ([subrefpat (in-list subrefpats)])
|
||||
(match subrefpat
|
||||
[(repeat _ subs)
|
||||
(sequence-fn (map refs-to-fn subs))]
|
||||
[(nrep-ref n tag)
|
||||
(λ (nv)
|
||||
(define env-ts (t-env-nrep-ref nv n))
|
||||
(for/list ([nv-t (in-list env-ts)])
|
||||
(match nv-t
|
||||
[(cons nv tterms)
|
||||
((refs-to-fn (hash-ref tterms tag)) nv)])))]
|
||||
[_ (sequence-fn (list (refs-to-fn subrefpat)))]))))]
|
||||
[else (λ (_) refpat)]))
|
||||
|
||||
;; (: sequence-fn : (All (a b) (Listof (a -> b)) -> (a -> (Listof b))))
|
||||
(define (sequence-fn fs)
|
||||
(λ (x)
|
||||
(for/list ([f (in-list fs)])
|
||||
(f x))))
|
||||
|
||||
;; to-term : augmented term -> redex term
|
||||
(define (to-term aug)
|
||||
|
|
|
|||
|
|
@ -1,48 +1,103 @@
|
|||
#lang typed/racket
|
||||
|
||||
(provide env
|
||||
env?
|
||||
(provide (struct-out env)
|
||||
empty-env
|
||||
add-name
|
||||
env-name-ref
|
||||
add-nrep
|
||||
env-union
|
||||
env-names)
|
||||
(struct-out t-env)
|
||||
t-env-name-ref
|
||||
t-env-nrep-ref)
|
||||
|
||||
;; For now, accept any pattern
|
||||
(define-type Pattern Any)
|
||||
(define-type Tag Number)
|
||||
(define-type Term Any)
|
||||
(define-type Env env)
|
||||
(define-type TEnv t-env)
|
||||
(define-type Tag Integer)
|
||||
(define-type (Tagged a) (HashTable Tag a))
|
||||
|
||||
(struct: env ([names : (HashTable Symbol Pattern)])
|
||||
(struct: env ([names : (HashTable Symbol Pattern)]
|
||||
[nreps : (HashTable Symbol (Pairof Env (Tagged Pattern)))])
|
||||
#:transparent)
|
||||
|
||||
(struct: t-env ([names : (HashTable Symbol Term)]
|
||||
[nreps : (HashTable Symbol (Listof (Pairof TEnv (Tagged Term))))])
|
||||
#:transparent)
|
||||
|
||||
(: empty-env : Env)
|
||||
(define empty-env
|
||||
(env (hash)))
|
||||
(env (hash) (hash)))
|
||||
|
||||
(: add-name : Env Symbol Pattern -> Env)
|
||||
(define/match (add-name e n p)
|
||||
[((env names) _ _)
|
||||
[((env names nreps) _ _)
|
||||
(define (default) p)
|
||||
(define update identity)
|
||||
(env (hash-update names n update default))])
|
||||
(env (hash-update names n update default) nreps)])
|
||||
|
||||
(: 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))))])
|
||||
(: add-nrep : Env Symbol Env Tag Pattern -> Env)
|
||||
(define/match (add-nrep e n repnv tag pat)
|
||||
[((env names nreps) _ _ _ _)
|
||||
(: update-nreps : (Pairof Env (Tagged Pattern)) -> (Pairof Env (Tagged Pattern)))
|
||||
(define/match (update-nreps e-t)
|
||||
[((cons nv tagged))
|
||||
(cons (env-union nv repnv)
|
||||
(hash-set tagged tag pat))])
|
||||
(: default : (-> (Pairof Env (Tagged Pattern))))
|
||||
(define (default)
|
||||
(: tagged : (Tagged Pattern))
|
||||
(define tagged (hash-set (ann (hash) (Tagged Pattern))
|
||||
tag pat))
|
||||
(cons repnv tagged))
|
||||
(env names
|
||||
(hash-update nreps n update-nreps default
|
||||
))])
|
||||
|
||||
(: t-env-name-ref : TEnv Symbol -> Pattern)
|
||||
(define/match (t-env-name-ref e n)
|
||||
[((t-env names _) _)
|
||||
(hash-ref names n (thunk (error (format "t-env-name-ref: name not found: ~s" n))))])
|
||||
|
||||
(: t-env-nrep-ref : TEnv Symbol -> (Listof (Pairof TEnv Term)))
|
||||
(define/match (t-env-nrep-ref nv n)
|
||||
[((t-env _ nreps) n)
|
||||
(hash-ref nreps n (thunk (error (format "t-env-nrep-ref: repeat 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))))])
|
||||
[((env ns1 rs1) (env ns2 rs2))
|
||||
|
||||
(define names-union
|
||||
(hash-union ns1
|
||||
ns2
|
||||
(λ (v1 v2) v1)))
|
||||
(: combo : (Pairof Env (Tagged Pattern)) (Pairof Env (Tagged Pattern)) -> (Pairof Env (Tagged Pattern)))
|
||||
(define/match (combo e-t1 e-t2)
|
||||
[((cons nv1 t1) (cons nv2 t2))
|
||||
(cons (env-union nv1 nv2)
|
||||
(hash-union t1 t2 (λ (_1 _2) (error "2 tags should never collide"))))])
|
||||
(define nreps-union
|
||||
(hash-union rs1 rs2 combo))
|
||||
(env names-union nreps-union)])
|
||||
|
||||
(: key-set : (All (k v) (HashTable k v) -> (Setof k)))
|
||||
(define (key-set m)
|
||||
(list->set (hash-keys m)))
|
||||
|
||||
(: hash-union : (All (k v) (HashTable k v) (HashTable k v) (v v -> v) -> (HashTable k v)))
|
||||
(define (hash-union m1 m2 combo)
|
||||
(: ks1 : (Setof k))
|
||||
(: ks2 : (Setof k))
|
||||
(define ks1 (key-set m1))
|
||||
(define ks2 (key-set m2))
|
||||
;; TODO: in-set should be typed in HEAD, fix this after rebasing.
|
||||
(for/hash: : (HashTable k v)
|
||||
([k : k (set-union ks1 ks2)])
|
||||
(define v1 (hash-ref m1 k (thunk #f)))
|
||||
(define v2 (hash-ref m2 k (thunk #f)))
|
||||
(define v
|
||||
(cond [(and v1 v2)
|
||||
(combo v1 v2)]
|
||||
[else (or v1 v2 (error "absurd"))]))
|
||||
(values k v)))
|
||||
|
|
|
|||
|
|
@ -17,25 +17,30 @@
|
|||
|
||||
;; 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 counter 0)
|
||||
(define (get-and-inc!)
|
||||
(begin0 counter
|
||||
(set! counter (add1 counter))))
|
||||
(define (walk pat)
|
||||
(match-a-pattern/single-base-case pat
|
||||
[`(name ,n ,subpat)
|
||||
(match-define (ann-pat subenv _) (walk subpat))
|
||||
(match-define (ann-pat subenv new-subpat) (walk subpat))
|
||||
(ann-pat (add-name subenv n subpat)
|
||||
pat)]
|
||||
`(name ,n ,new-subpat))]
|
||||
[`(mismatch-name ,n ,subpat)
|
||||
;; TODO
|
||||
(unimplemented "mismatch-name")]
|
||||
[`(in-hole ,p1 ,p2)
|
||||
(match-define (ann-pat subenv1 _)
|
||||
(match-define (ann-pat subenv1 newsub1)
|
||||
(walk p1))
|
||||
(match-define (ann-pat subenv2 _)
|
||||
(match-define (ann-pat subenv2 newsub2)
|
||||
(walk p2))
|
||||
(ann-pat (env-union subenv1 subenv2) pat)]
|
||||
(ann-pat (env-union subenv1 subenv2)
|
||||
`(in-hole ,newsub1 ,newsub2))]
|
||||
[`(hide-hole ,p)
|
||||
(match-define (ann-pat subenv _)
|
||||
(match-define (ann-pat subenv newsub)
|
||||
(walk p))
|
||||
(ann-pat subenv pat)]
|
||||
(ann-pat subenv `(hide-hole ,newsub))]
|
||||
[`(side-condition ,p ,c ,s)
|
||||
(error 'unsupported "side condition is not supported.")]
|
||||
[`(list ,sub-pats ...)
|
||||
|
|
@ -44,19 +49,27 @@
|
|||
(match sub-pat
|
||||
[`(repeat ,p #f #f)
|
||||
(ann-pat empty-env sub-pat)]
|
||||
[`(repeat ,p ,n #f)
|
||||
(match-define (ann-pat subenv _)
|
||||
(walk p))
|
||||
(define tag (get-and-inc!))
|
||||
(ann-pat (add-nrep empty-env n subenv tag p)
|
||||
`(repeat ,tag ,n #f))]
|
||||
[`(repeat ,p ,n ,m)
|
||||
(unimplemented "named repeat")]
|
||||
(unimplemented (format "mismatch repeat (..._!_): ~s ~s" n m))]
|
||||
[_ (walk sub-pat)])))
|
||||
|
||||
(define list-env
|
||||
(for/fold ([accenv empty-env])
|
||||
([sub-apat (in-list ann-sub-pats)])
|
||||
([sub-apat (in-list ann-sub-pats)])
|
||||
(match sub-apat
|
||||
[(ann-pat subenv _)
|
||||
(env-union subenv accenv)])))
|
||||
(ann-pat list-env pat)]
|
||||
(ann-pat list-env (cons 'list (map ann-pat-pat ann-sub-pats)))]
|
||||
[_ (pure-ann-pat pat)]))
|
||||
(walk pat))
|
||||
(define res
|
||||
(walk pat))
|
||||
res)
|
||||
|
||||
(define (remove-names pat)
|
||||
(define names-2set (find-names pat))
|
||||
|
|
|
|||
|
|
@ -11,10 +11,10 @@
|
|||
(for ([i (in-range N)])
|
||||
(check-not-exn
|
||||
(λ ()
|
||||
(unless (redex-match
|
||||
l p
|
||||
(generate-term l p #:i-th i))
|
||||
(error 'bad-term "line ~a: i=~a" line i)))))))]))
|
||||
(define term
|
||||
(generate-term l p #:i-th i))
|
||||
(unless (redex-match l p term)
|
||||
(error 'bad-term (format "line ~a: i=~a" line i))))))))]))
|
||||
|
||||
(define-language Nats
|
||||
(n natural))
|
||||
|
|
@ -99,11 +99,13 @@
|
|||
(try-it 20 VarMentioned var)
|
||||
|
||||
(define-language NRep
|
||||
(v (natural ..._1 natural ..._1))
|
||||
(v2 (v ..._1 v ..._2 v ..._1 v ..._2)))
|
||||
(v (natural ..._1 natural ..._1))
|
||||
(v2 (v ..._1 v ..._2 v ..._1 v ..._2))
|
||||
(v3 (natural_1 ..._1 natural_1 ..._1)))
|
||||
|
||||
(try-it 100 NRep v)
|
||||
(try-it 100 NRep v2)
|
||||
(try-it 100 NRep v3)
|
||||
|
||||
;; Test production sort
|
||||
(define-language rec
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user