Handle all variable pats in pattern unification.
This commit is contained in:
Burke Fetscher
parent
8e0dc29c1d
commit
37ced9609c
|
|
@ -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)]
|
||||
|
|
|
|||
|
|
@ -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)))]
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user