summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorWei Tang <i@null.tl>2015-09-09 14:10:09 +0800
committerWei Tang <i@null.tl>2015-09-09 14:10:09 +0800
commitfd39eb74fd1a53bf1bbb212ce7e36001ff241fb3 (patch)
tree5cdedf8ceb54ab9d92806ecec9fa0610ca68962b
parent0272856fd59cc370243daa5aa0cf7dee38491da5 (diff)
downloadmm-fd39eb74fd1a53bf1bbb212ce7e36001ff241fb3.tar.gz
mm-fd39eb74fd1a53bf1bbb212ce7e36001ff241fb3.tar.bz2
check predicate for patterns
-rw-r--r--mm.rkt32
1 files changed, 32 insertions, 0 deletions
diff --git a/mm.rkt b/mm.rkt
index 2c19ed9..586aeba 100644
--- a/mm.rkt
+++ b/mm.rkt
@@ -274,6 +274,7 @@
(=/= 'fresh selbri)
(lookupo selbri pattern-assoc pattern)
(patterno pv pp pattern)
+ (predicateo pp pattern-assoc)
(zipo pv args a-params)
(appendo a-params params combined-params)
(applyo pp pattern-assoc combined-params fresh-next fresh-next-out out))))))
@@ -291,6 +292,36 @@
(== `(,out ,fresh-next-out) q)))
'(((== (variable (fresh)) 1) (fresh fresh))))
+(define predicateo
+ (lambda (p pattern-assoc)
+ (conde
+ ((fresh (s1 s2)
+ (== `(== ,s1 ,s2) p)))
+ ((fresh (selbri s1 s2)
+ (== `(,selbri ,s1 ,s2) p)
+ (conde
+ ((== 'disj selbri))
+ ((== 'conj selbri)))
+ (conde
+ ((varo s1))
+ ((predicateo s1 pattern-assoc)))
+ (conde
+ ((varo s2))
+ ((predicateo s2 pattern-assoc)))))
+ ((fresh (selbri args pattern pv pp a-params)
+ (== `(,selbri . ,args) p)
+ (lookupo selbri pattern-assoc pattern)
+ (patterno pv pp pattern)
+ (predicateo pp pattern-assoc)
+ (zipo pv args a-params)
+ (=/= selbri '==)
+ (=/= selbri 'conj)
+ (=/= selbri 'disj))))))
+
+(check-expect
+ (run* (q) (predicateo '(== 1 1) '()))
+ '(_.0))
+
(define predicatifyo
(lambda (s pattern-assoc parent fresh-next fresh-next-out
substitution out)
@@ -301,6 +332,7 @@
((varo s)
(unifyo out s tmp substitution))
((not-varo s)
+ (predicateo s pattern-assoc)
(== out s)
(== tmp substitution))))))