don't use disunify* to check disequations, since at this point they are fully instantiated

This commit is contained in:
Burke Fetscher 2012-11-01 11:51:09 -05:00
parent e6ab32593e
commit 6be405975e
2 changed files with 18 additions and 6 deletions

View File

@ -84,7 +84,7 @@
(set! sym-index 0)
(define rhs-term (pat->term/term-e rhs term-e eqs lang))
(define lhs-term (pat->term/term-e lhs term-e eqs lang))
(disunify* lhs-term rhs-term (make-hash) lang))
(not (equal? rhs-term lhs-term)))
(define (pat->term/term-e t term-e actual-e lang)
(call/ec
@ -100,7 +100,7 @@
[`(cstr (,nts ...) ,pat)
(recur pat)]
[`(list ,ps ...)
`(list ,@(for/list ([p ps]) (recur p)))]
(for/list ([p ps]) (recur p))]
[`(nt ,_)
(fail (not-ground))]
[`(,stuff ...) ;; here it's a fully instanatiated list

View File

@ -11,17 +11,21 @@
(let ()
(define-language L0)
(test-equal (check-dq `a `a (make-hash) L0 (hash))
#f)
(test-equal (check-dq `a `b (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a) `(list a) (make-hash) L0 (hash))
#f)
(test-equal (check-dq `(list a) `(list b) (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a) `(list any) (make-hash) L0 (hash))
(test-equal (check-dq `(list number) `(list variable) (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a) `(list number) (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a) `(list variable-not-otherwise-mentioned) (make-hash) L0 (hash))
(test-equal (check-dq `(list 2) `(list variable-not-otherwise-mentioned) (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a b) `(list a any) (make-hash) L0 (hash))
(test-equal (check-dq `(list a b) `(list a number) (make-hash) L0 (hash))
#t)
(test-equal (check-dq `(list a b) `(list a b) (make-hash) L0 (hash))
#f)
@ -30,7 +34,15 @@
(make-hash)
L0
(hash (lvar 'a) 'number))
#f))
#f)
(test-equal (check-dq `(name a ,(bound))
`(name b ,(bound))
(make-hash (list (cons (lvar 'a) '(1 2 3))
(cons (lvar 'b) '(1 2 3))))
L0
(hash (lvar 'a) 'any (lvar 'b) 'any))
#f)
)
(let ()