From 37ced9609c2579b07dce7658299cbecfdf6d7c91 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Wed, 4 Sep 2013 15:33:08 -0500 Subject: [PATCH] Handle all variable pats in pattern unification. --- .../redex-lib/redex/private/pat-unify.rkt | 143 ++++++++++++------ .../redex-test/redex/tests/unify-tests.rkt | 48 +++++- 2 files changed, 142 insertions(+), 49 deletions(-) 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 770d9bd29d..732bee917d 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt @@ -4,6 +4,7 @@ racket/contract racket/set racket/match + racket/function "match-a-pattern.rkt" "matcher.rkt" "lang-struct.rkt" @@ -95,8 +96,8 @@ [`real #t] [`boolean #t] [`variable #t] - [`(variable-except ,vars ...) #f] - [`(variable-prefix ,pfx) #f] + [`(variable-except ,vars ...) #t] + [`(variable-prefix ,pfx) #t] [`variable-not-otherwise-mentioned #t] [`hole #f] [`(nt ,(? n-t? n)) @@ -168,9 +169,7 @@ (not-failed? u*) (unify* t* u* eqs L))) (and/fail (not-failed? res) - (let* ([static-eqs (hash/mut->imm (let ([ans eqs]) - ;(printf "1.1\n") - ans))] + (let* ([static-eqs (hash/mut->imm eqs)] [found-pre-dqs (apply set-union (set) (for/list ([dq-sides/id (hash-values (dqs-found))]) @@ -391,53 +390,93 @@ (define t (resolve t0 e)) (define u (resolve u0 e)) #2dmatch - ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═══════════╦═══════════╦═════════╦══════════╦══════════════╦═════════════╗ - ║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? vnom?) ║ `variable ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║ - ║ ║ ,u-name ║ ,name-u ║ (,nts1 ...) ║ ║ ║ ║ ,us ...) ║ ║ ║ ║ ║ ║ ║ - ║ t ║ ,u-pat) ║ ,(bound)) ║ ,p1) ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ - ╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═══════════╩═══════════╩═════════╩══════════╩══════════════╩═════════════╣ - ║`(mismatch-name ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '())))) ║ - ║ ,t-name ║ (unify* t-pat u e L) ║ - ║ ,t-pat) ║ ║ - ╠═════════════════╬═════════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ - ║`(name ,name-t ║ ║ (instantiate* name-t u e L) ║ - ║ ,(bound)) ║ ║ ║ - ╠═════════════════╣ ╚═════════════╦═══════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ - ║`(cstr ║ ║(u*-2cstrs ║ (u*-1cstr nts2 p2 u e L) ║ - ║ (,nts2 ...) ║ ║ nts1 p1 ║ ║ - ║ ,p2) ║ ║ nts2 p2 e L) ║ ║ - ╠═════════════════╣ ╚═══════════════╬═══════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ - ║ `(nt ,n-t) ║ ║(u*-2nts ║ (u*-1nt n-t u e L) ║ - ║ ║ ║ n-t n-u ║ ║ - ║ ║ ║ e L) ║ ║ - ╠═════════════════╣ ╚═══════════╬════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ - ║ `any ║ ║ u ║ - ║ ║ ║ ║ - ╠═════════════════╣ ╚══════╦════════════╦══════════════════════════════════════════════════════════════════════════╦═════════════╣ - ║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║ - ║ ║ ║ t u) ║ ║ ║ - ╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║ - ║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║ - ║ ║ ║ ts us e L) ║ ║(u*-matches? ║ - ╠═════════════════╣ ╚══════════════╬═══════════╦═══════════╗ ║ t u ║ - ║ (? vnom?) ║ ║ t ║ t ║ ║ e L) ║ - ╠═════════════════╣ ╚═══════════╬═══════════╣ ║ ║ - ║ `variable ║ ║ t ║ ║ ║ - ╠═════════════════╣ ╚═══════════╬═════════╗ ║ ║ - ║ `string ║ (unify* u t e L) ║ t ║ ║ ║ - ╠═════════════════╣ ╚═════════╬══════════╗ ║ ║ - ║ `boolean ║ ║ t ║ ║ ║ - ╠═════════════════╣ ╚══════════╬══════════════╣ ║ - ║ (? base-ty?) ║ ║ t ║ ║ - ╠═════════════════╣ ╚══════════════╬═════════════╣ - ║ (? not-pair?) ║ ║(and/fail ║ - ║ ║ ║ (equal? t u)║ - ║ ║ ║ t) ║ - ╚═════════════════╩══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝) + ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═════════════════╦═════════╦══════════╦══════════════╦═════════════╗ + ║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? pvar?) ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║ + ║ ║ ,u-name ║ ,name-u ║ (,nts1 ...) ║ ║ ║ ║ ,us ...) ║ ║ ║ ║ ║ ║ + ║ t ║ ,u-pat) ║ ,(bound)) ║ ,p1) ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ + ╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═════════════════╩═════════╩══════════╩══════════════╩═════════════╣ + ║`(mismatch-name ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '())))) ║ + ║ ,t-name ║ (unify* t-pat u e L) ║ + ║ ,t-pat) ║ ║ + ╠═════════════════╬═════════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ + ║`(name ,name-t ║ ║ (instantiate* name-t u e L) ║ + ║ ,(bound)) ║ ║ ║ + ╠═════════════════╣ ╚═════════════╦═══════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ + ║`(cstr ║ ║(u*-2cstrs ║ (u*-1cstr nts2 p2 u e L) ║ + ║ (,nts2 ...) ║ ║ nts1 p1 ║ ║ + ║ ,p2) ║ ║ nts2 p2 e L) ║ ║ + ╠═════════════════╣ ╚═══════════════╬═══════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════╣ + ║ `(nt ,n-t) ║ ║(u*-2nts ║ (u*-1nt n-t u e L) ║ + ║ ║ ║ n-t n-u ║ ║ + ║ ║ ║ e L) ║ ║ + ╠═════════════════╣ ╚═══════════╬══════════════════════════════════════════════════════════════════════════════════════════════════════╣ + ║ `any ║ ║ u ║ + ║ ║ ║ ║ + ╠═════════════════╣ ╚══════╦════════════╦════════════════════════════════════════════════════════════════════╦═════════════╣ + ║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║ + ║ ║ ║ t u) ║ ║ ║ + ╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║ + ║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║ + ║ ║ ║ ts us e L) ║ ║(u*-matches? ║ + ╠═════════════════╣ ╚══════════════╬═════════════════╗ ║ t u ║ + ║ (? pvar?) ║ ║(u*-2pvars u t L)║ ║ e L) ║ + ╠═════════════════╣ ╚═════════════════╬═════════╗ ║ ║ + ║ `string ║ (unify* u t e L) ║ t ║ ║ ║ + ╠═════════════════╣ ╚═════════╬══════════╗ ║ ║ + ║ `boolean ║ ║ t ║ ║ ║ + ╠═════════════════╣ ╚══════════╬══════════════╣ ║ + ║ (? base-ty?) ║ ║ t ║ ║ + ╠═════════════════╣ ╚══════════════╬═════════════╣ + ║ (? not-pair?) ║ ║(and/fail ║ + ║ ║ ║ (equal? t u)║ + ║ ║ ║ t) ║ + ╚═════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝) +(define (pvar? x) (or (vnom? x) + (var-pref? x) + (var-exc? x) + (equal? 'variable x))) (define (vnom? x) (equal? x 'variable-not-otherwise-mentioned)) +(define (var-pref? x) (match x + [`(variable-prefix ,p) #t] + [_ #f])) +(define (var-exc? x) (match x + [`(variable-except ,p ...) #t] + [_ #f])) (define (not-pair? x) (not (pair? x))) +(define (u*-2pvars v1 v2 L) + #2dmatch + ╔════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╗ + ║ v1 ║`(variable-prefix ,p1) ║ `(variable-except ,e1 ... ) ║ (? vnom?) ║ `variable ║ + ║ v2 ║ ║ ║ ║ ║ + ╠════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╣ + ║ ║ (cond ║ (and/fail ║(u*-2pvars ║ ║ + ║ `(variable-prefix ,p2) ║ [(sym-pref? p1 p2) ║ (andmap ║ v2 ║ ║ + ║ ║ `(variable-prefix ,p2)]║ (curry sym-pref? p2) ║ `(variable-except ║ ║ + ║ ║ [(sym-pref? p2 p1) ║ e1) ║ ,@(compiled-lang-literals L)) ║ ║ + ║ ║ `(variable-prefix ,p1)]║ v2) ║ L) ║ ║ + ║ ║ [else (unif-fail)]) ║ ║ ║ ║ + ╠════════════════════════╬══════════════════════════╬════════════════════════════════╣ ║ ║ + ║ ║ ║ `(variable-except ║ ║ ║ + ║ `(variable-except ║ ║ ,@(de-dupe/sorted ║ ║ v2 ║ + ║ ,e2 ...) ║ ║ (merge/sorted e1 e2))) ║ ║ ║ + ║ ║ ║ ║ ║ ║ + ╠════════════════════════╣ ╚════════════════════════════════╬═══════════════════════════════╣ ║ + ║ ║ ║ ║ ║ + ║ (? vnom?) ║ ║ v1 ║ ║ + ║ ║ ║ ║ ║ + ╠════════════════════════╣ (u*-2pvars v2 v1 L) ╚═══════════════════════════════╣ ║ + ║ ║ ║ ║ + ║ `variable ║ ║ ║ + ║ ║ ║ ║ + ╚════════════════════════╩═══════════════════════════════════════════════════════════════════════════════════════════╩════════════════╝) + +(define (sym-pref? sp s) + (regexp-match + (string-append "^" (symbol->string sp) ".*$") + (symbol->string s))) + (define (u*-2cstrs nts1 p1 nts2 p2 e L) (let ([res (unify* p1 p2 e L)] [new-nts (merge-ids/sorted nts1 nts2 L)]) @@ -507,6 +546,14 @@ (and/fail (not (memq s (compiled-lang-literals L))) (not (base-ty? s)) s)] + [(`(variable-except ,ss ...) (? symbol? s)) + (and/fail (not (memq s ss)) + u)] + [(`(variable-prefix ,pref) (? symbol? s)) + (and/fail (regexp-match + (regexp (string-append "^" (symbol->string pref) ".*$")) + (symbol->string s)) + u)] [(`variable (? symbol? s)) (and/fail (not (base-ty? s)) s)] diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt index d4b116f889..0026de67aa 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt @@ -360,7 +360,6 @@ #'(unify-all/results lhs eqs ([rhs res eqs] ...))])) - (unify-all/results/no-bindings 'any (hash) (['any 'any] @@ -497,6 +496,47 @@ ['(nt e) '(cstr (e) any)] ['variable 'variable] ['variable-not-otherwise-mentioned 'variable-not-otherwise-mentioned])) + +(unify-all/results/no-bindings + '(variable-except a) (hash) + ([5 #f] + ['any '(variable-except a)] + ['number #f] + ['integer #f] + ['natural #f] + ['real #f] + ['string #f] + ['boolean #f] + ['(list 1 2 3) #f] + ['b 'b] + ['a #f] + ['(mismatch-name y b) 'b] + ['(nt e) '(cstr (e) (variable-except a))] + ['variable '(variable-except a)] + ['variable-not-otherwise-mentioned '(variable-except a)] + ['(variable-except b) '(variable-except a b)] + ['(variable-prefix a) '(variable-prefix a)])) + +(unify-all/results/no-bindings + '(variable-prefix a) (hash) + ([5 #f] + ['any '(variable-prefix a)] + ['number #f] + ['integer #f] + ['natural #f] + ['real #f] + ['string #f] + ['boolean #f] + ['(list 1 2 3) #f] + ['b #f] + ['a 'a] + ['aa 'aa] + ['(mismatch-name y b) #f] + ['(nt e) '(cstr (e) (variable-prefix a))] + ['variable '(variable-prefix a)] + ['variable-not-otherwise-mentioned '(variable-prefix a)] + ['(variable-prefix a) '(variable-prefix a)] + ['(variable-prefix b) #f])) @@ -537,6 +577,10 @@ ['variable `(cstr (e q) variable) (make-hash)] ['variable-not-otherwise-mentioned `(cstr (e q) variable-not-otherwise-mentioned) (make-hash)] + ['(variable-except a) + `(cstr (e q) (variable-except a)) (make-hash)] + ['(variable-prefix a) + `(cstr (e q) (variable-prefix a)) (make-hash)] ['(list 1 2 3) '(cstr (e q) (list 1 2 3)) (make-hash)] [5 '(cstr (e q) 5) (make-hash)] @@ -555,6 +599,8 @@ ['boolean `(name x ,(bound)) (make-hash `((,(lvar 'x) . boolean)))] ['variable `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable)))] ['variable-not-otherwise-mentioned `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable-not-otherwise-mentioned)))] + ['(variable-except a) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (variable-except a))))] + ['(variable-prefix a) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (variable-prefix a))))] ['(cstr (n) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (n) any))))] ['(list 1 2) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (list 1 2))))] ['(mismatch-name z any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . any)))]