Redex: parameterized disequations
refactor the pattern unifier and tests to handle disequations with parameters correctly
This commit is contained in:
Burke Fetscher
parent
564d244039
commit
bdf1866e80
|
|
@ -23,7 +23,10 @@
|
|||
pat*-clause-p?s
|
||||
bind-names
|
||||
remove-empty-dqs
|
||||
unif-fail)
|
||||
unif-fail
|
||||
dq)
|
||||
|
||||
;(require racket/trace)
|
||||
;;
|
||||
;; atom := `any | `number | `string | `integer | `boolean | `real | `variable | `variable-not-otherwise-mentioned
|
||||
;; var := symbol?
|
||||
|
|
@ -49,6 +52,7 @@
|
|||
(struct p*e (p e) #:transparent)
|
||||
|
||||
(struct env (eqs dqs) #:transparent)
|
||||
(struct dq (params dq) #:transparent)
|
||||
(define empty-env (env (hash) '()))
|
||||
|
||||
(struct unif-fail () #:transparent)
|
||||
|
|
@ -162,7 +166,7 @@
|
|||
(list->dq-pairs dq-sides/id)))]
|
||||
[found-dqs
|
||||
(for/list ([pdq found-pre-dqs])
|
||||
(disunify* (first pdq) (second pdq) (hash-copy static-eqs) L))])
|
||||
(disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
|
||||
(and (for/and ([d found-dqs]) d)
|
||||
(let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
|
||||
[new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
|
||||
|
|
@ -181,7 +185,7 @@
|
|||
(list->dq-pairs (cdr dq-sides)))]))
|
||||
|
||||
;; pat pat env lang -> (or/c env #f)
|
||||
(define (disunify t u e L)
|
||||
(define (disunify params t u e L)
|
||||
;(-> pat? pat? env/c any/c (or/c env/c #f))
|
||||
(parameterize ([new-eqs (make-hash)])
|
||||
(define eqs (hash-copy (env-eqs e)))
|
||||
|
|
@ -192,7 +196,7 @@
|
|||
e]
|
||||
[else
|
||||
(define bn-eqs (hash-copy eqs))
|
||||
(define new-dq (disunify* t* u* eqs L))
|
||||
(define new-dq (disunify* params t* u* eqs L))
|
||||
(match new-dq
|
||||
[#f #f]
|
||||
[#t
|
||||
|
|
@ -230,11 +234,11 @@
|
|||
;; simplified - first element in lhs of all inequations is a var not occuring in lhs of eqns
|
||||
(define (check-and-resimplify eqs dqs L)
|
||||
(define-values (dqs-notok dqs-ok)
|
||||
(partition (λ (dq)
|
||||
(partition (λ (a-dq)
|
||||
(hash-has-key?
|
||||
eqs
|
||||
(lvar (match dq
|
||||
[`((list (name ,v1 ,(bound)) ,vs ...) (list ,t1 ,ts ...))
|
||||
(lvar (match a-dq
|
||||
[(dq ps `((list (name ,v1 ,(bound)) ,vs ...) (list ,t1 ,ts ...)))
|
||||
v1]))))
|
||||
(remove-empty-dqs dqs)))
|
||||
(let loop ([ok dqs-ok]
|
||||
|
|
@ -244,23 +248,52 @@
|
|||
ok]
|
||||
[else
|
||||
(match notok
|
||||
[`((,vars-p* ,term-p*) ,rest ...)
|
||||
(let ([new-dq (disunify* vars-p* term-p* (hash-copy eqs) L)])
|
||||
[`(,(dq ps `(,vars-p* ,term-p*)) ,rest ...)
|
||||
(let ([new-dq (disunify* ps vars-p* term-p* (hash-copy eqs) L)])
|
||||
(and new-dq
|
||||
(match new-dq
|
||||
[#t (loop ok rest)]
|
||||
[`((list)(list)) (loop ok rest)]
|
||||
#;[`((list)(list)) (loop ok rest)]
|
||||
[else (loop (cons new-dq ok) rest)])))])])))
|
||||
|
||||
;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*)
|
||||
(define (disunify* u* t* eqs L)
|
||||
(define (disunify* params u* t* eqs L)
|
||||
(parameterize ([new-eqs (make-hash)])
|
||||
(let ([res (unify* u* t* eqs L)])
|
||||
(cond
|
||||
[(unif-fail? res) #t]
|
||||
[(empty? (hash-keys (new-eqs))) #f]
|
||||
[else
|
||||
(extend-dq (new-eqs) base-dq)]))))
|
||||
(define-values (new-ps new-dq)
|
||||
(param-elim params (extend-dq (new-eqs) base-dq)))
|
||||
(match new-dq
|
||||
[`((list) (list))
|
||||
#f]
|
||||
[else
|
||||
(dq new-ps new-dq)])
|
||||
#;(extend-dq (new-eqs) base-dq)]))))
|
||||
|
||||
(define (param-elim params unquantified-dq)
|
||||
(let loop ([dq-rest unquantified-dq]
|
||||
[ps params]
|
||||
[new-dq-l '()]
|
||||
[new-dq-r '()])
|
||||
;(printf "~s ~s ~s ~s\n" dq-rest ps new-dq-l new-dq-r)
|
||||
(match dq-rest
|
||||
['((list) (list))
|
||||
(values ps `((list ,@new-dq-l) (list ,@new-dq-r)))]
|
||||
[`((list (name ,v1,(bound)) ,vs ...) (list ,t1 ,ts ...))
|
||||
(cond
|
||||
[(member v1 params)
|
||||
(loop `((list ,@vs) (list ,@ts))
|
||||
(remove v1 ps)
|
||||
new-dq-l
|
||||
new-dq-r)]
|
||||
[else
|
||||
(loop `((list ,@vs) (list ,@ts))
|
||||
ps
|
||||
(cons `(name ,v1 ,(bound)) new-dq-l)
|
||||
(cons t1 new-dq-r))])])))
|
||||
|
||||
|
||||
;; the "root" pats will be pats without names,
|
||||
|
|
@ -609,6 +642,7 @@
|
|||
(values (lvar id) res)]))
|
||||
|
||||
|
||||
;(trace disunify*)
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -59,28 +59,30 @@
|
|||
(env-dqs e-right))))
|
||||
|
||||
(define (dqs->dqset dqs)
|
||||
(for/set ([dq (in-list dqs)])
|
||||
(for/fold ([dq-pairs (set)])
|
||||
([ls (first dq)]
|
||||
[rs (second dq)])
|
||||
(set-add dq-pairs (cons ls rs)))))
|
||||
(for/set ([the-dq (in-list dqs)])
|
||||
(match the-dq
|
||||
[(dq ps dq-e)
|
||||
(for/fold ([dq-pairs (set)])
|
||||
([ls (first dq-e)]
|
||||
[rs (second dq-e)])
|
||||
(set-add dq-pairs (cons ls rs)))])))
|
||||
|
||||
(check-equal? (dqs->dqset `(((list (name a ,(bound))
|
||||
(name b ,(bound)))
|
||||
(list a-cant-be
|
||||
b-cant-be))))
|
||||
(check-equal? (dqs->dqset (list (dq '() `((list (name a ,(bound))
|
||||
(name b ,(bound)))
|
||||
(list a-cant-be
|
||||
b-cant-be)))))
|
||||
(set (set (cons 'list 'list)
|
||||
(cons `(name a ,(bound)) 'a-cant-be)
|
||||
(cons `(name b ,(bound)) 'b-cant-be))))
|
||||
|
||||
(check-equal? (dqs->dqset `(((list (name a ,(bound))
|
||||
(name b ,(bound)))
|
||||
(list a-cant-be
|
||||
b-cant-be))
|
||||
((list (name c ,(bound))
|
||||
(name d ,(bound)))
|
||||
(list c-cant-be
|
||||
d-cant-be))))
|
||||
(check-equal? (dqs->dqset `(,(dq '() `((list (name a ,(bound))
|
||||
(name b ,(bound)))
|
||||
(list a-cant-be
|
||||
b-cant-be)))
|
||||
,(dq '() `((list (name c ,(bound))
|
||||
(name d ,(bound)))
|
||||
(list c-cant-be
|
||||
d-cant-be)))))
|
||||
(set (set (cons 'list 'list)
|
||||
(cons `(name c ,(bound)) 'c-cant-be)
|
||||
(cons `(name d ,(bound)) 'd-cant-be))
|
||||
|
|
@ -873,42 +875,45 @@
|
|||
;; TODO tests on the dqs here are currently order-dependent
|
||||
|
||||
(check-false
|
||||
(disunify* `(list (name x_1 ,(bound)))
|
||||
(disunify* '()
|
||||
`(list (name x_1 ,(bound)))
|
||||
`(list (name x_2 ,(bound)))
|
||||
(make-hash `((,(lvar 'x_1) . a)
|
||||
(,(lvar 'x_2) . a)))
|
||||
L0))
|
||||
(check-not-false
|
||||
(disunify* `(list (name x_1 ,(bound)))
|
||||
(disunify* '()
|
||||
`(list (name x_1 ,(bound)))
|
||||
`(list (name x_2 ,(bound)))
|
||||
(make-hash `((,(lvar 'x_1) . (nt x))
|
||||
(,(lvar 'x_2) . a)))
|
||||
L0))
|
||||
(check-not-false
|
||||
(disunify* `(list (name x_1 ,(bound)))
|
||||
(disunify* '()
|
||||
`(list (name x_1 ,(bound)))
|
||||
`(list (name x_2 ,(bound)))
|
||||
(make-hash `((,(lvar 'x_1) . (nt x))
|
||||
(,(lvar 'x_2) . (nt x))))
|
||||
L0))
|
||||
(check-false
|
||||
(disunify* 'a '(cstr (s) a) (make-hash) L0))
|
||||
(disunify* '() 'a '(cstr (s) a) (make-hash) L0))
|
||||
(check-false
|
||||
(let ([h (make-hash (list (cons (lvar 'a2) 'a)))])
|
||||
(disunify* `(name a2 ,(bound)) '(cstr (s) a) h L0)))
|
||||
(disunify* '() `(name a2 ,(bound)) '(cstr (s) a) h L0)))
|
||||
(check-false
|
||||
(let ([h (make-hash (list (cons (lvar 'a2) 'a)
|
||||
(cons (lvar 's6) '(cstr (s) a))))])
|
||||
(disunify* `(name a2 ,(bound)) `(name s6 ,(bound)) h L0)))
|
||||
(disunify* '() `(name a2 ,(bound)) `(name s6 ,(bound)) h L0)))
|
||||
|
||||
(define (make-eqs eqs)
|
||||
(for/hash ([eq eqs])
|
||||
(values (car eq) (cdr eq))))
|
||||
|
||||
(define (make-dqs dqs)
|
||||
(for/list ([dq dqs])
|
||||
(list (car dq) (cdr dq))))
|
||||
(for/list ([the-dq dqs])
|
||||
(dq '() (list (car the-dq) (cdr the-dq)))))
|
||||
|
||||
(define-syntax (test-disunify stx)
|
||||
(define-syntax (test-disunify/no-params stx)
|
||||
(syntax-case stx ()
|
||||
[(_ t u eqs dqs eqs′ dqs′)
|
||||
(quasisyntax/loc stx
|
||||
|
|
@ -916,7 +921,7 @@
|
|||
[eqs-out (make-eqs eqs′)]
|
||||
[dqs-in (check-and-resimplify eqs-in (make-dqs dqs) L0)]
|
||||
[dqs-out (make-dqs dqs′)]
|
||||
[res (disunify t u (env eqs-in dqs-in) L0)])
|
||||
[res (disunify '() t u (env eqs-in dqs-in) L0)])
|
||||
#,(syntax/loc stx
|
||||
(check-not-false
|
||||
(env-equal?
|
||||
|
|
@ -926,7 +931,7 @@
|
|||
(quasisyntax/loc stx
|
||||
(let* ([eqs-in (make-eqs eqs)]
|
||||
[dqs-in (check-and-resimplify eqs (make-dqs dqs) L0)]
|
||||
[res (disunify t u (env eqs-in dqs-in) L0)])
|
||||
[res (disunify '() t u (env eqs-in dqs-in) L0)])
|
||||
(if true/false
|
||||
#,(syntax/loc stx (check-not-false res))
|
||||
#,(syntax/loc stx (check-false res)))))]))
|
||||
|
|
@ -953,33 +958,33 @@
|
|||
(check-not-false res)
|
||||
(check-false res))))]))
|
||||
|
||||
(test-disunify 1 2 '() '() '() '())
|
||||
(test-disunify '(list 1 2) '(list 1 3) '() '() '() '())
|
||||
(test-disunify `(list (name x any) (name y any)) `(list 1)
|
||||
(test-disunify/no-params 1 2 '() '() '() '())
|
||||
(test-disunify/no-params '(list 1 2) '(list 1 3) '() '() '() '())
|
||||
(test-disunify/no-params `(list (name x any) (name y any)) `(list 1)
|
||||
`((,(lvar 'x) . any)
|
||||
(,(lvar 'y) . any))
|
||||
'()
|
||||
`((,(lvar 'x) . any)
|
||||
(,(lvar 'y) . any))
|
||||
'())
|
||||
(test-disunify `(name x any) 4
|
||||
(test-disunify/no-params `(name x any) 4
|
||||
`((,(lvar 'x) . ,(lvar 'y))
|
||||
(,(lvar 'y) . 3))
|
||||
'()
|
||||
`((,(lvar 'x) . ,(lvar 'y))
|
||||
(,(lvar 'y) . 3))
|
||||
'())
|
||||
(test-disunify `(name x any) 1
|
||||
(test-disunify/no-params `(name x any) 1
|
||||
`((,(lvar 'x) . 1)) '() #f)
|
||||
(test-disunify 1 `(name x any)
|
||||
(test-disunify/no-params 1 `(name x any)
|
||||
'() '() `((,(lvar 'x) . any))
|
||||
`(((list (name x ,(bound))) . (list 1))))
|
||||
(test-disunify `(name x any) 3
|
||||
(test-disunify/no-params `(name x any) 3
|
||||
`((,(lvar 'x) . ,(lvar 'y))
|
||||
(,(lvar 'y) . 3))
|
||||
'() #f)
|
||||
;; does violate the occurs check (stolen from Colmerauer '84)
|
||||
(test-disunify 1 `(name z any)
|
||||
(test-disunify/no-params 1 `(name z any)
|
||||
`((,(lvar 'x) . ,(lvar 'y))
|
||||
(,(lvar 'y) . (list (name y ,(bound)) (name z ,(bound))))
|
||||
(,(lvar 'z) . any))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user