summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorWei Tang <i@null.tl>2015-09-09 14:59:40 +0800
committerWei Tang <i@null.tl>2015-09-09 14:59:40 +0800
commit107eb12a399fda9b448f16d8cfb1281bcca19bd0 (patch)
treef7193e339e7e06318c2726a53a8e8f9577deb46a
parentfd39eb74fd1a53bf1bbb212ce7e36001ff241fb3 (diff)
downloadmm-107eb12a399fda9b448f16d8cfb1281bcca19bd0.tar.gz
mm-107eb12a399fda9b448f16d8cfb1281bcca19bd0.tar.bz2
fix disj: incorrect implementation of predicatifyo
-rw-r--r--mm.rkt41
1 files changed, 22 insertions, 19 deletions
diff --git a/mm.rkt b/mm.rkt
index 586aeba..d9bd725 100644
--- a/mm.rkt
+++ b/mm.rkt
@@ -323,18 +323,17 @@
'(_.0))
(define predicatifyo
- (lambda (s pattern-assoc parent fresh-next fresh-next-out
- substitution out)
- (fresh (tmp)
- (runo* out pattern-assoc parent
- fresh-next fresh-next-out tmp)
+ (lambda (s pattern-assoc parent fresh-next fresh-next-out substitution)
+ (fresh (tmp predicate)
+ (predicateo predicate pattern-assoc)
(conde
((varo s)
- (unifyo out s tmp substitution))
+ (unifyo predicate s tmp substitution))
((not-varo s)
- (predicateo s pattern-assoc)
- (== out s)
- (== tmp substitution))))))
+ (== predicate s)
+ (== tmp substitution)))
+ (runo* predicate pattern-assoc parent
+ fresh-next fresh-next-out tmp))))
(define runo*
(lambda (predicate pattern-assoc parent fresh-next fresh-next-out
@@ -343,18 +342,22 @@
((fresh (s1 s2)
(== `(== ,s1 ,s2) predicate)
(unifyo s1 s2 parent out)))
- ((fresh (s1 s2 o1 o2 t1 t2)
+ ((fresh (s1 s2 out1 out2 fresh-next-out1 fresh-next-out2)
(== `(disj ,s1 ,s2) predicate)
+ (predicatifyo s1 pattern-assoc parent fresh-next
+ fresh-next-out1 out1)
+ (predicatifyo s2 pattern-assoc parent fresh-next
+ fresh-next-out2 out2)
(conde
- ((predicatifyo s1 pattern-assoc parent fresh-next
- fresh-next-out t1 o1))
- ((predicatifyo s2 pattern-assoc parent fresh-next
- fresh-next-out t2 o2)))
- (conde
- ((== t1 #f) (== t2 #f) (== out #f))
- ((=/= t1 #f) (== t2 #f) (== out t1))
- ((== t1 #f) (=/= t2 #f) (== out t2))
- ((=/= t1 #f) (=/= t2 #f) (conde ((== out t1)) ((== out t2)))))))
+ ((== out1 #f) (== out2 #f)
+ (== out #f) (== fresh-next-out fresh-next))
+ ((=/= out1 #f) (== out2 #f)
+ (== out out1) (== fresh-next-out fresh-next-out1))
+ ((== out1 #f) (=/= out2 #f)
+ (== out out2) (== fresh-next-out fresh-next-out2))
+ ((=/= out1 #f) (=/= out2 #f)
+ (conde ((== out out1) (== fresh-next-out fresh-next-out1))
+ ((== out out2) (== fresh-next-out fresh-next-out2)))))))
((fresh (s1 s2 o1 o2 fresh-next-tmp tmp)
(== `(conj ,s1 ,s2) predicate)
(predicatifyo s1 pattern-assoc parent fresh-next