diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt index 863518d737..b40dc94566 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt @@ -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) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt index a67f97cb84..b90f4e6c64 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/env.rkt @@ -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))) 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 3d2b789a8f..d572542613 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/preprocess-pat.rkt @@ -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)) 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 1cb31c2d23..59a34d20f8 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt @@ -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