Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

added new version of miniKanren relational parser, where the empty se…

…t is represented as failure
  • Loading branch information...
commit 48b2ad0bae4cb1743349d13d05553f579516e1df 1 parent 7a674b6
William Byrd authored
View
543 mK-empty-set-as-failure/mk-lexer.scm
@@ -0,0 +1,543 @@
+; William E. Byrd's miniKanren version of (a subset) of Matt Might's code for
+; a Scheme lexer, based on derivative parsing of regexp.
+
+; Matt's original code can be found at
+; http://matt.might.net/articles/nonblocking-lexing-toolkit-based-on-regex-derivatives/
+
+; This file requires the miniKanren version of Matt Might's code for derivative
+; parsing of regexp.
+
+;;; ! BUG shown in maino-3b: matching isn't necessarily greedy
+;;; In other words, Kleene star and Kleene plus don't have 'maximum munch' semantics:
+;;; http://en.wikipedia.org/wiki/Maximal_munch
+;;; Indeed, this is a problem pointed out by Oleg when not using committed choice.
+;;; What is the right way to solve this problem? I smell constraints for the character
+;;; classes--maybe constraints would help with maximum munch as well. Oleg seems skeptical
+;;; that constraints will help. This is an interesting problem!
+
+(load "mk-rd.scm")
+
+;;; Regular language convenience operators
+
+; Exactly n repetitions
+; n must be a Peano numeral: z, (s z), (s (s z)), etc.
+(define (n-repso n pat out)
+ (fresh ()
+ (conde
+ [(== 'z n) (== regex-BLANK out)]
+ [(fresh (n-1 res)
+ (== `(s ,n-1) n)
+ (n-repso n-1 pat res)
+ (seqo pat res out))])))
+
+; Kleene plus: one or more repetitions
+; (not to be mistaken with the relational arithmetic pluso!)
+(define (pluso pat out)
+ (fresh (res)
+ (repo pat res)
+ (seqo pat res out)))
+
+; Option: zero or one instances
+(define (optiono pat out)
+ (fresh ()
+ (alto regex-BLANK pat out)))
+
+
+;;; letters: a-d (to make the branching factor tolerable)
+(define alphas '(alt
+ (alt a b)
+ (alt c d)))
+
+;;; special characters: _, ?, #, and \ (to make the branching factor tolerable)
+(define specials '(alt
+ (alt _ ?)
+ (alt hash slash)))
+
+;;; whitespace: ' ' and '\n' (to make the branching factor tolerable)
+(define white-space '(alt space newline))
+
+(define parens '(alt left-paren right-paren))
+
+; Match any character
+; Here we represent characters as symbols.
+;;; WEB: I don't think I can just use a fresh logic variable
+;;; to represent AnyChar, for the same reason that _ is tricky in miniKanren.
+;;; Basically, the question is how should this program behave:
+;;;
+;;; (run* (q)
+;;; (fresh (x out)
+;;; (any-charo x)
+;;; (repo x out)
+;;; (== `(,x ,out) q)))
+;;;
+;;; I assume the correct interpretation is [a-zA-Z0-0]*
+;;; In other words, this regex should match 'abc', not just 'aaa'.
+;;; Yet, the definition of any-charo below would only match 'aaa'.
+;;;
+;;; This feels like a scoping issue. Could nominal logic resolve this problem?
+;;;
+;;;(define (any-charo x) (symbolo x))
+(define any-char `(alt (alt ,alphas ,specials) (alt ,white-space ,parens)))
+
+;;; Scheme lexer
+
+; abbreviations
+
+;;; Scheme literal character: #\\ ~ AnyChar
+(define ch `(seq (seq hash slash) (seq slash ,alphas)))
+
+;;; (simplified) Scheme identifier:
+;;; (('a' thru 'd') ||
+;;; oneOf("_?%"))+
+;;;
+;;; The resulting regex is quite large. Tempting to use a
+;;; higher-order representation using a conde. Not sure if this will
+;;; run into the _-style problem described above.
+(define id
+ (let ((pat `(alt ,alphas ,specials)))
+ `(seq ,pat (rep ,pat))))
+
+;;; ** all of these character classes smell like constraints **
+
+(define (appendo l s out)
+ (conde
+ [(== '() l) (== s out)]
+ [(fresh (a d res)
+ (== `(,a . ,d) l)
+ (== `(,a . ,res) out)
+ (appendo d s res))]))
+
+;;; the main lexer loop
+(define (maino chars tokens)
+ (conde
+ [(== '() chars) (== '() tokens)]
+ [(fresh (a d pat prefix suffix tok res)
+ (== `(,a . ,d) chars)
+ (emito pat chars prefix suffix tok)
+ (appendo tok res tokens)
+ (maino suffix res))]))
+
+;;; *** fascinating! This appears, at first glance, to be a counter
+;;; example to Will's Law: that simpler goals that have finitely many
+;;; answers should come first in a conde. However, Will's Law stil
+;;; holds, since the paren cases can actually diverge. Still, the
+;;; useful ordering seems counter intuitive!
+(define (emito pat chars prefix suffix tok)
+ (fresh ()
+ (conde
+;;; I don't think I need the END pattern.
+ [(== id pat) (== `((SymbolToken ,prefix)) tok)]
+ [(== ch pat) (== `((CharToken ,prefix)) tok)]
+ [(== white-space pat) (== '() tok)]
+ [(== 'left-paren pat) (== '((PuncToken left-paren)) tok)]
+ [(== 'right-paren pat) (== '((PuncToken right-paren)) tok)])
+ (regex-matcho pat prefix #t)
+ (appendo prefix suffix chars)))
+
+;;; tests
+
+(check-expect "n-repso-1"
+ (run 10 (q)
+ (fresh (n pat out)
+ (n-repso n pat out)
+ (== `(,n ,pat ,out) q)))
+ '((z _.0 #t) ; is this true, even if _.0 is #f?
+ ((s z) #f #f)
+ ((s z) #t #t)
+ (((s z) _.0 _.0) (=/= ((_.0 . #f)) ((_.0 . #t))))
+ ((s (s z)) #f #f)
+ ((s (s z)) #t #t)
+ (((s (s z)) _.0 (seq _.0 _.0)) (=/= ((_.0 . #f)) ((_.0 . #t))))
+ ((s (s (s z))) #f #f)
+ ((s (s (s z))) #t #t)
+ (((s (s (s z))) _.0 (seq _.0 (seq _.0 _.0))) (=/= ((_.0 . #f)) ((_.0 . #t))))))
+
+(check-expect "pluso-1"
+ (run* (q)
+ (fresh (pat out)
+ (pluso pat out)
+ (== `(,pat ,out) q)))
+ '((#f #f)
+ ((_.0 (seq _.0 (rep _.0))) (sym _.0))
+ (#t #t)
+ ((rep _.0) (seq (rep _.0) (rep _.0)))
+ ((seq _.0 _.1) (seq (seq _.0 _.1) (rep (seq _.0 _.1))))
+ ((alt _.0 _.1) (seq (alt _.0 _.1) (rep (alt _.0 _.1))))))
+
+(check-expect "optiono-1"
+ (run* (q)
+ (fresh (pat out)
+ (optiono pat out)
+ (== `(,pat ,out) q)))
+ '((#t #t)
+ (#f #t)
+ ((_.0 (alt #t _.0)) (=/= ((_.0 . #f)) ((_.0 . #t))))))
+
+; run 5 appears to diverge
+(check-expect "alphas-1"
+ (run 4 (q)
+ (regex-matcho alphas q regex-BLANK))
+ '((a) (b) (c) (d)))
+
+(check-expect "specials-1"
+ (run 4 (q)
+ (regex-matcho specials q regex-BLANK))
+ '((_) (?) (hash) (slash)))
+
+(check-expect "white-space-1"
+ (run 2 (q)
+ (regex-matcho white-space q regex-BLANK))
+ '((space) (newline)))
+
+(check-expect "parens-1"
+ (run 2 (q)
+ (regex-matcho parens q regex-BLANK))
+ '((left-paren) (right-paren)))
+
+(check-expect "any-char-1"
+ (run 5 (q)
+ (regex-matcho any-char q regex-BLANK))
+ '((a) (b) (c) (d) (_)))
+
+(check-expect "ch-1"
+ (run 4 (q)
+ (regex-matcho ch q regex-BLANK))
+ '((hash slash slash a)
+ (hash slash slash b)
+ (hash slash slash c)
+ (hash slash slash d)))
+
+(check-expect "id-1"
+ (run 20 (q)
+ (regex-matcho id q regex-BLANK))
+ '((a)
+ (b)
+ (a a)
+ (a b)
+ (c)
+ (b a)
+ (a a a)
+ (a c)
+ (b b)
+ (a a b)
+ (d)
+ (a d)
+ (c a)
+ (b a a)
+ (a a a a)
+ (b c)
+ (a a c)
+ (a _)
+ (a b a)
+ (c b)))
+
+(check-expect "rep-any-char-1"
+ (run 10 (q)
+ (regex-matcho `(rep ,any-char) q regex-BLANK))
+ '(() (a) (b) (a a) (c) (a b) (b a) (d) (a a a) (a c)))
+
+(check-expect "pluso-any-char-1"
+ (run 10 (q)
+ (fresh (pat)
+ (pluso any-char pat)
+ (regex-matcho pat q regex-BLANK)))
+ '((a) (b) (a a) (a b) (c) (b a) (a a a) (a c) (b b) (a a b)))
+
+(check-expect "appemdo-1"
+ (run* (q)
+ (appendo '(a b c) '(d e) q))
+ '((a b c d e)))
+
+(check-expect "emito-1"
+ (run 10 (q)
+ (fresh (pat chars prefix suffix tok)
+ (emito pat chars prefix suffix tok)
+ (== `(,pat ,chars ,prefix ,suffix ,tok) q)))
+ '((left-paren
+ (left-paren . _.0)
+ (left-paren)
+ _.0
+ ((PuncToken left-paren)))
+ (right-paren
+ (right-paren . _.0)
+ (right-paren)
+ _.0
+ ((PuncToken right-paren)))
+ ((alt space newline) (space . _.0) (space) _.0 ())
+ ((alt space newline) (newline . _.0) (newline) _.0 ())
+ ((seq (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))
+ (rep (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))))
+ (a . _.0)
+ (a)
+ _.0
+ ((SymbolToken (a))))
+ ((seq (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))
+ (rep (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))))
+ (b . _.0)
+ (b)
+ _.0
+ ((SymbolToken (b))))
+ ((seq (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))
+ (rep (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))))
+ (a a . _.0)
+ (a a)
+ _.0
+ ((SymbolToken (a a))))
+ ((seq (seq hash slash)
+ (seq slash (alt (alt a b) (alt c d))))
+ (hash slash slash a . _.0) ; !!!!!! WTF!? sweet
+ (hash slash slash a)
+ _.0
+ ((CharToken (hash slash slash a))))
+ ((seq (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))
+ (rep (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))))
+ (a b . _.0)
+ (a b)
+ _.0
+ ((SymbolToken (a b))))
+ ((seq (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))
+ (rep (alt (alt (alt a b) (alt c d))
+ (alt (alt _ ?) (alt hash slash)))))
+ (c . _.0)
+ (c)
+ _.0
+ ((SymbolToken (c))))))
+
+(check-expect "maino-1"
+ (run 50 (q)
+ (fresh (chars tokens)
+ (maino chars tokens)
+ (== `(,chars ,tokens) q)))
+ '((() ())
+ ((left-paren) ((PuncToken left-paren)))
+ ((right-paren) ((PuncToken right-paren)))
+ ((space) ())
+ ((left-paren left-paren)
+ ((PuncToken left-paren) (PuncToken left-paren)))
+ ((left-paren right-paren)
+ ((PuncToken left-paren) (PuncToken right-paren)))
+ ((right-paren left-paren)
+ ((PuncToken right-paren) (PuncToken left-paren)))
+ ((right-paren right-paren)
+ ((PuncToken right-paren) (PuncToken right-paren)))
+ ((left-paren space) ((PuncToken left-paren)))
+ ((left-paren left-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((newline) ())
+ ((left-paren left-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((space left-paren) ((PuncToken left-paren)))
+ ((left-paren right-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((space right-paren) ((PuncToken right-paren)))
+ ((left-paren right-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken right-paren)))
+ ((right-paren space) ((PuncToken right-paren)))
+ ((right-paren left-paren left-paren)
+ ((PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((right-paren left-paren right-paren)
+ ((PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((left-paren left-paren space)
+ ((PuncToken left-paren) (PuncToken left-paren)))
+ ((left-paren left-paren left-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((left-paren newline) ((PuncToken left-paren)))
+ ((left-paren left-paren left-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((right-paren right-paren left-paren)
+ ((PuncToken right-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((left-paren space left-paren)
+ ((PuncToken left-paren) (PuncToken left-paren)))
+ ((newline left-paren) ((PuncToken left-paren)))
+ ((right-paren right-paren right-paren)
+ ((PuncToken right-paren)
+ (PuncToken right-paren)
+ (PuncToken right-paren)))
+ ((left-paren left-paren right-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((left-paren space right-paren)
+ ((PuncToken left-paren) (PuncToken right-paren)))
+ ((newline right-paren) ((PuncToken right-paren)))
+ ((left-paren left-paren right-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken right-paren)))
+ ((space space) ())
+ ((left-paren right-paren space)
+ ((PuncToken left-paren) (PuncToken right-paren)))
+ ((space left-paren left-paren)
+ ((PuncToken left-paren) (PuncToken left-paren)))
+ ((left-paren right-paren left-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((right-paren left-paren space)
+ ((PuncToken right-paren) (PuncToken left-paren)))
+ ((space left-paren right-paren)
+ ((PuncToken left-paren) (PuncToken right-paren)))
+ ((left-paren right-paren left-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((right-paren left-paren left-paren left-paren)
+ ((PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((left-paren left-paren left-paren space)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((right-paren newline) ((PuncToken right-paren)))
+ ((right-paren left-paren left-paren right-paren)
+ ((PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((left-paren left-paren left-paren left-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((left-paren left-paren newline)
+ ((PuncToken left-paren) (PuncToken left-paren)))
+ ((left-paren left-paren left-paren left-paren right-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((space right-paren left-paren)
+ ((PuncToken right-paren) (PuncToken left-paren)))
+ ((left-paren right-paren right-paren left-paren)
+ ((PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((right-paren space left-paren)
+ ((PuncToken right-paren) (PuncToken left-paren)))
+ ((right-paren left-paren right-paren left-paren)
+ ((PuncToken right-paren)
+ (PuncToken left-paren)
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((left-paren left-paren space left-paren)
+ ((PuncToken left-paren)
+ (PuncToken left-paren)
+ (PuncToken left-paren)))))
+
+(check-expect "maino-2"
+ (run 9 (q)
+ (fresh (chars tokens x y z* rest)
+ (maino chars tokens)
+ (== `((SymbolToken (,x ,y . ,z*)) . ,rest) tokens)
+ (== `(,chars ,tokens) q)))
+ '(((a a) ((SymbolToken (a a))))
+ ((a a left-paren)
+ ((SymbolToken (a a)) (PuncToken left-paren)))
+ ((a a right-paren)
+ ((SymbolToken (a a)) (PuncToken right-paren)))
+ ((a a space) ((SymbolToken (a a))))
+ ((a a left-paren left-paren)
+ ((SymbolToken (a a))
+ (PuncToken left-paren)
+ (PuncToken left-paren)))
+ ((a a left-paren right-paren)
+ ((SymbolToken (a a))
+ (PuncToken left-paren)
+ (PuncToken right-paren)))
+ ((a a right-paren left-paren)
+ ((SymbolToken (a a))
+ (PuncToken right-paren)
+ (PuncToken left-paren)))
+ ((a a right-paren right-paren)
+ ((SymbolToken (a a))
+ (PuncToken right-paren)
+ (PuncToken right-paren)))
+ ((a a left-paren space)
+ ((SymbolToken (a a)) (PuncToken left-paren)))))
+
+(check-expect "maino-3"
+ (run 1 (q)
+ (maino '(left-paren a b right-paren) q))
+ '(((PuncToken left-paren)
+ (SymbolToken (a))
+ (SymbolToken (b))
+ (PuncToken right-paren))))
+
+;;; Bug! The matching isn't always greedy.
+(check-expect "maino-3b"
+ (run 2 (q)
+ (maino '(a a) q))
+ '(((SymbolToken (a)) (SymbolToken (a)))
+ ((SymbolToken (a a)))))
+
+;; this takes too long to run
+;(check-expect "maino-4"
+; (run 1 (q)
+; (maino '(left-paren a b c c a space c a space right-paren) q))
+; '???)
+
+(check-expect "maino-5"
+ (run 1 (q)
+ (maino q '((PuncToken left-paren))))
+ '((left-paren)))
+
+(check-expect "maino-6"
+ (run 1 (q)
+ (maino q '((PuncToken left-paren)
+ (SymbolToken (a)))))
+ '((left-paren a)))
+
+;;; too slow to run
+;(check-expect "maino-9"
+; (run 1 (q)
+; (maino q '((PuncToken left-paren)
+; (SymbolToken (a))
+; (SymbolToken (b)))))
+; '???)
+
+;;; too slow
+;(check-expect "maino-10"
+; (run 1 (q)
+; (maino q '((PuncToken left-paren)
+; (SymbolToken (a))
+; (SymbolToken (b))
+; (PuncToken right-paren))))
+; '???)
View
612 mK-empty-set-as-failure/mk-rd.scm
@@ -0,0 +1,612 @@
+; William E. Byrd's miniKanren version of Matt Might's code for derivative
+; parsing of regexp.
+
+; Matt's original Scheme code can be found at
+; http://matt.might.net/articles/implementation-of-regular-expression-matching-in-scheme-with-derivatives/
+
+; This file requires core miniKanren (conde, ==, fresh) plus =/= and symbolo.
+
+; In theory, tabling will allow this code to parse CFG's (or at least
+; be something close to parsing CFG's).
+
+;;; This version models the 'empty set' regex as failure. As a result, the
+;;; miniKanren translations of 'regex-matcho' and 'deltao' merely succeed or fail
+;;; rather than unifying with an 'out' variable.
+;;;
+;;; Oleg insists all true predicates succeed or fail rather than
+;;; having an out variable. It is a matter of perspective whether
+;;; regex-matcho is a predicate, or rather is returning the empty
+;;; string or the empty set. Although it is probably a matter of
+;;; perspective whether the empty set should be a regex.
+;;;
+;;; We lose the flexibility of generating regex that don't match a
+;;; string, or strings that don't match a regex. The advantage
+;;; (hopefully) is that the code will be greatly simplified.
+
+;;; Open issue:
+;;;
+;;; To what extent should constraints be used to enforce terms are in proper, normalized form?
+;;; The relational arithmetic system assumes that the user will never instantiate terms incorrectly.
+;;; Probably we should just have enough of a constraint to ensure illegal terms are instantiated when
+;;; running backwards.
+;;;
+;;; For example, consider this answer in test 12:
+;;;
+;;; ((alt (rep (seq _.0 _.1)) _.2) (=/= ((_.0 . #t)) ((_.1 . #t))))
+;;;
+;;; the (=/= ((_.0 . #t)) ((_.1 . #t))) constraints aren't sufficient.
+;;; For example, _.0 could become instantiated to (rep (rep EPSILON)),
+;;; which isn't in normal form. So perhaps those two constraints
+;;; aren't very useful. Need to think this through carefully.
+;;;
+;;; Another approach would be to add constraints to miniKanren for the
+;;; different types of regex terms; the constraints would ensure the
+;;; terms are never instantiated incorrectly. Would need rep, alt,
+;;; and seq constraints.
+
+(load "mk.scm")
+
+; <regex> ::=
+; | EPSILON ; Empty/blank pattern (same as #t)
+; | '<symbol> ; Symbol
+; | (alt <regex> <regex>) ; Alternation
+; | (seq <regex> <regex>) ; Sequence
+; | (rep <regex>) ; Repetition
+
+
+;; Special regular expression.
+(define EPSILON #t) ; the empty string
+
+;; Simplifying regex constructors.
+(define (valid-seqo exp)
+ (fresh (pat1 pat2)
+ (== `(seq ,pat1 ,pat2) exp)
+ (=/= EPSILON pat1)
+ (=/= EPSILON pat2)))
+
+(define (seqo pat1 pat2 out)
+ (conde
+ [(== EPSILON pat1) (== pat2 out)]
+ [(== EPSILON pat2) (== pat1 out) (=/= EPSILON pat1)]
+ [(=/= EPSILON pat1) (=/= EPSILON pat2) (== `(seq ,pat1 ,pat2) out)]))
+
+(define (valid-alto exp)
+ (fresh (pat1 pat2)
+ (== `(alt ,pat1 ,pat2) exp)
+ (=/= pat1 pat2)))
+
+(define (alto pat1 pat2 out)
+ (conde
+ [(== pat1 pat2) (== pat1 out)]
+ [(=/= pat1 pat2) (== `(alt ,pat1 ,pat2) out)]))
+
+(define (valid-repo exp)
+ (fresh (pat)
+ (== `(rep ,pat) exp)
+ (=/= EPSILON pat)
+ (conde
+ ((symbolo pat))
+ ((fresh (re1 re2)
+ (== `(seq ,re1 ,re2) pat)
+ (valid-seqo pat)))
+ ((fresh (re1 re2)
+ (== `(alt ,re1 ,re2) pat)
+ (valid-alto pat))))))
+
+(define (repo pat out)
+ (conde
+ [(== EPSILON pat)
+ (== EPSILON out)]
+ [(conde
+ ((symbolo pat) (== `(rep ,pat) out))
+ ((fresh (re1 re2)
+ (conde
+ ((== `(rep ,re1) pat)
+ ; remove nested reps
+ (== pat out))
+ ((== `(seq ,re1 ,re2) pat)
+ (== `(rep ,pat) out)
+ (valid-seqo pat))
+ ((== `(alt ,re1 ,re2) pat)
+ (== `(rep ,pat) out)
+ (valid-alto pat))))))]))
+
+;; Matching functions.
+
+; deltao : regex
+(define (deltao re)
+ (conde
+ [(== EPSILON re)]
+ [(fresh (re1)
+ (== `(rep ,re1) re)
+ (valid-repo re))]
+ [(fresh (re1 re2)
+ (== `(alt ,re1 ,re2) re)
+ (valid-alto re)
+ (conde
+ ((deltao re1))
+ ((not-deltao re1) (deltao re2))))]
+ [(fresh (re1 re2)
+ (== `(seq ,re1 ,re2) re)
+ (valid-seqo re)
+ (deltao re1)
+ (deltao re2))]))
+
+(define (not-deltao re)
+ (conde
+ [(symbolo re)]
+ [(fresh (re1 re2)
+ (== `(seq ,re1 ,re2) re)
+ (valid-seqo re)
+ (conde
+ ((not-deltao re1))
+ ((deltao re1) (not-deltao re2))))]
+ [(fresh (re1 re2)
+ (== `(alt ,re1 ,re2) re)
+ (valid-alto re)
+ (not-deltao re1)
+ (not-deltao re2))]))
+
+; d/dco : regex regex-atom regex
+(define (d/dco re c out)
+ (fresh ()
+ (symbolo c)
+ (conde
+ [(== c re)
+ (== EPSILON out)]
+ [(fresh (re1 res1)
+ (== `(rep ,re1) re)
+ (valid-repo re)
+ (seqo res1 re out)
+ (d/dco re1 c res1))]
+ [(fresh (re1 re2 res1 res2)
+ (== `(alt ,re1 ,re2) re)
+ (valid-alto re)
+ (conde
+ ((no-d/dco re2 c)
+ (d/dco re1 c out))
+ ((no-d/dco re1 c)
+ (d/dco re2 c out))
+ ((alto res1 res2 out)
+ (d/dco re1 c res1)
+ (d/dco re2 c res2))))]
+ [(fresh (re1 re2 res1 res2 res3)
+ (== `(seq ,re1 ,re2) re)
+ (valid-seqo re)
+ (seqo res1 re2 res2)
+ (conde
+ ((== res2 out) (not-deltao re1))
+ ((alto res2 res3 out)
+ (deltao re1)
+ (d/dco re2 c res3)))
+ (d/dco re1 c res1))])))
+
+(define (no-d/dco re c)
+ (fresh ()
+ (symbolo c)
+ (conde
+ [(== EPSILON re)]
+ [(symbolo re) (=/= c re)]
+ [(fresh (re1 res1)
+ (== `(rep ,re1) re)
+ (valid-repo re)
+ (no-d/dco re c))]
+ [(fresh (re1 re2 res1 res2 res3)
+ (== `(seq ,re1 ,re2) re)
+ (valid-seqo re)
+ (conde
+ ((not-deltao re1))
+ ((deltao re1) (no-d/dco re2 c)))
+ (no-d/dco re1 c))]
+ [(fresh (re1 re2 res1 res2)
+ (== `(alt ,re1 ,re2) re)
+ (valid-alto re)
+ (no-d/dco re1 c)
+ (no-d/dco re2 c))])))
+
+; regex-matcho : regex list
+(define (regex-matcho pattern data)
+ (conde
+ [(== '() data) (deltao pattern)]
+ [(fresh (a d res)
+ (== `(,a . ,d) data)
+ (d/dco pattern a res)
+ (regex-matcho res d))]))
+
+;; Tests.
+(define-syntax check-expect
+ (syntax-rules ()
+ [(_ name check expect)
+ (begin
+ (display "testing ")
+ (display name)
+ (display "...")
+ (newline)
+ (if (not (equal? check expect))
+ (begin (display "check-expect failed for test ")
+ (display name)
+ (newline)
+ (display "got: ")
+ (newline)
+ (display check)
+ (newline)
+ (display "expected: ")
+ (newline)
+ (display expect)
+ (newline)
+ (newline))))]))
+
+;;; new tests
+
+(check-expect "2"
+ (run* (q) (repo EPSILON q))
+ '(#t))
+
+(check-expect "3"
+ (run* (q) (repo 'foo q))
+ '((rep foo)))
+
+(check-expect "3-b"
+ (run* (q)
+ (fresh (res)
+ (repo 'foo res)
+ (repo res q)))
+ '((rep foo)))
+
+(check-expect "3-c"
+ (run* (q)
+ (fresh (res)
+ (repo EPSILON res)
+ (repo res q)))
+ '(#t))
+
+(check-expect "6"
+ (run* (q) (alto 'foo 'bar q))
+ '((alt foo bar)))
+
+(check-expect "6-b"
+ (run* (q) (alto 'foo EPSILON q))
+ '((alt foo #t)))
+
+(check-expect "6-c"
+ (run* (q) (alto EPSILON 'foo q))
+ '((alt #t foo)))
+
+(check-expect "9"
+ (run* (q) (seqo EPSILON 'foo q))
+ '(foo))
+
+(check-expect "10"
+ (run* (q) (seqo 'foo EPSILON q))
+ '(foo))
+
+(check-expect "11"
+ (run* (q) (seqo 'foo 'bar q))
+ '((seq foo bar)))
+
+(check-expect "12"
+ (run 10 (q) (deltao q))
+ '(#t
+ ((rep _.0) (sym _.0))
+ ((rep (seq _.0 _.1)) (=/= ((_.0 . #t)) ((_.1 . #t))))
+ ((rep (alt _.0 _.1)) (=/= ((_.0 . _.1))))
+ ((alt #t _.0) (=/= ((_.0 . #t))))
+ ((alt _.0 #t) (sym _.0))
+ ((alt (rep _.0) _.1) (=/= ((_.1 rep _.0))) (sym _.0))
+ ((seq (rep _.0) (rep _.1)) (sym _.0 _.1))
+ ((alt _.0 (rep _.1)) (sym _.0 _.1))
+ ((alt (rep (seq _.0 _.1)) _.2) (=/= ((_.0 . #t)) ((_.1 . #t))))))
+
+(check-expect "12-b"
+ (run 10 (q) (not-deltao q))
+ '((_.0 (sym _.0))
+ ((seq _.0 _.1) (=/= ((_.1 . #t))) (sym _.0))
+ ((alt _.0 _.1) (=/= ((_.0 . _.1))) (sym _.0 _.1))
+ ((seq (rep _.0) _.1) (sym _.0 _.1))
+ ((seq (seq _.0 _.1) _.2)
+ (=/= ((_.1 . #t)) ((_.2 . #t)))
+ (sym _.0))
+ ((alt _.0 (seq _.1 _.2)) (=/= ((_.2 . #t))) (sym _.0 _.1))
+ ((alt (seq _.0 _.1) _.2) (=/= ((_.1 . #t))) (sym _.0 _.2))
+ ((seq (alt _.0 _.1) _.2)
+ (=/= ((_.0 . _.1)) ((_.2 . #t)))
+ (sym _.0 _.1))
+ ((alt _.0 (alt _.1 _.2))
+ (=/= ((_.1 . _.2)))
+ (sym _.0 _.1 _.2))
+ ((alt (alt _.0 _.1) _.2)
+ (=/= ((_.0 . _.1)))
+ (sym _.0 _.1 _.2))))
+
+(check-expect "13"
+ (run 10 (q)
+ (fresh (re c out)
+ (d/dco re c out)
+ (== `(,re ,c ,out) q)))
+ '(((_.0 _.0 #t) (sym _.0))
+ (((rep _.0) _.0 (rep _.0)) (sym _.0))
+ (((seq _.0 _.1) _.0 _.1) (=/= ((_.1 . #t))) (sym _.0))
+ (((alt _.0 #t) _.0 #t) (sym _.0))
+ (((alt _.0 _.1) _.0 #t) (=/= ((_.0 . _.1))) (sym _.0 _.1))
+ (((alt #t _.0) _.0 #t) (sym _.0))
+ (((rep (alt _.0 #t)) _.0 (rep (alt _.0 #t))) (sym _.0))
+ (((rep (alt _.0 _.1)) _.0 (rep (alt _.0 _.1))) (=/= ((_.0 . _.1))) (sym _.0 _.1))
+ (((rep (alt #t _.0)) _.0 (rep (alt #t _.0))) (sym _.0))
+ (((alt _.0 _.1) _.1 #t) (=/= ((_.0 . _.1))) (sym _.0 _.1))))
+
+(check-expect "14"
+ (run* (q) (regex-matcho '(seq foo (rep bar))
+ '(foo bar bar bar)))
+ '(_.0))
+
+(check-expect "14-b"
+ (run* (q) (regex-matcho '(seq foo (rep bar))
+ '(foo)))
+ '(_.0))
+
+(check-expect "14-c"
+ (run* (q) (d/dco '(seq foo (rep bar)) 'foo q))
+ '((rep bar)))
+
+(check-expect "14-d"
+ (run* (q) (valid-seqo '(seq foo (rep bar))))
+ '(_.0))
+
+(check-expect "14-e"
+ (run* (q) (d/dco 'foo 'foo q))
+ '(#t))
+
+(check-expect "14-f"
+ (run* (q) (d/dco '(rep bar) 'foo q))
+ '())
+
+(check-expect "15"
+ (run* (q) (regex-matcho '(seq foo (rep bar))
+ '(foo bar baz bar bar)))
+ '())
+
+(check-expect "16"
+ (run* (q) (regex-matcho '(seq foo (rep (alt bar baz)))
+ '(foo bar baz bar bar)))
+ '(_.0))
+
+;;; generate regex patterns that match the input string (!)
+;;; (seq foo (rep bar)) was the original regex
+;;; The #t's in the answer represent epsilons. This seems to be okay, actually!
+;;; The run expression can produce equivalent regex's; for example,
+;;; (rep (alt foo bar))
+;;; and
+;;; (rep (alt bar foo))
+;;; Is there a canonical representation of regex's that would avoid these
+;;; essentially duplicate answers?
+
+;;; WEB wow--these answers are very different from the previous answers in the naive mk translation.
+(check-expect "20"
+ (run 30 (q) (regex-matcho q '(foo bar bar bar)))
+ '((seq foo (rep bar)) (seq foo (seq bar (rep bar))) (seq foo (seq bar (seq bar bar))) (seq foo (seq bar (seq bar (rep bar)))) ((seq foo (seq bar (seq bar (seq bar (rep _.0))))) (sym _.0)) (rep (alt foo bar)) (seq foo (seq bar (seq bar (alt bar #t)))) ((seq foo (seq bar (seq bar (seq bar (rep (seq _.0 _.1)))))) (=/= ((_.0 . #t)) ((_.1 . #t)))) ((seq foo (seq bar (seq bar (seq bar (rep (alt _.0 _.1)))))) (=/= ((_.0 . _.1)))) ((seq foo (seq bar (seq bar (seq bar (alt #t _.0))))) (=/= ((_.0 . #t)))) ((seq foo (seq bar (seq bar (seq bar (alt _.0 #t))))) (sym _.0)) (seq foo (rep (alt bar #t))) ((seq foo (seq bar (seq bar (seq bar (alt (rep _.0) _.1))))) (=/= ((_.1 rep _.0))) (sym _.0)) ((seq foo (seq bar (seq bar (alt bar _.0)))) (=/= ((_.0 . bar))) (sym _.0)) ((seq foo (seq bar (seq bar (seq bar (seq (rep _.0) (rep _.1)))))) (sym _.0 _.1)) (seq foo (seq bar (seq bar (alt #t bar)))) (seq foo (seq bar (rep (alt bar #t)))) ((seq foo (seq bar (seq bar (seq bar (alt _.0 (rep _.1)))))) (sym _.0 _.1)) ((seq foo (seq bar (seq bar (seq bar (alt (rep (seq _.0 _.1)) _.2))))) (=/= ((_.0 . #t)) ((_.1 . #t)))) ((seq foo (rep (alt bar _.0))) (=/= ((_.0 . bar))) (sym _.0)) ((seq foo (seq bar (seq bar (seq bar (alt (rep (alt _.0 _.1)) _.2))))) (=/= ((_.0 . _.1)))) ((seq foo (seq bar (seq bar (seq bar (seq (rep _.0) (rep (seq _.1 _.2))))))) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) ((seq foo (seq bar (seq bar (seq bar (alt (alt #t _.0) _.1))))) (=/= ((_.0 . #t)))) ((seq foo (seq bar (seq bar (seq bar (seq (rep _.0) (rep (alt _.1 _.2))))))) (=/= ((_.1 . _.2))) (sym _.0)) ((seq foo (seq bar (seq bar (seq bar (seq (rep _.0) (alt #t _.1)))))) (=/= ((_.1 . #t))) (sym _.0)) (seq foo (seq bar (seq bar (rep (alt bar #t))))) ((seq foo (seq bar (seq bar (seq bar (alt (seq _.0 _.1) #t))))) (=/= ((_.1 . #t))) (sym _.0)) ((seq foo (seq bar (seq bar (seq bar (seq (rep (seq _.0 _.1)) (rep _.2)))))) (=/= ((_.0 . #t)) ((_.1 . #t))) (sym _.2)) (rep (alt bar foo)) (seq foo (rep (alt #t bar))))
+
+;;; old answers from naive mk translation
+
+ ;; '((seq foo (rep bar)) ; jackpot!
+ ;; (rep (alt foo bar))
+ ;; (rep (alt bar foo)) ; equivalent to a previous regex
+ ;; (seq foo (rep (alt #t bar)))
+ ;; (seq foo (alt #t (rep bar)))
+ ;; (alt #t (seq foo (rep bar)))
+ ;; (seq foo (rep (alt bar #t)))
+ ;; (seq (rep foo) (rep bar))
+ ;; (rep (alt foo (rep bar)))
+ ;; (seq foo (alt foo (rep bar)))
+ ;; (rep (seq foo (rep bar)))
+ ;; (alt foo (seq foo (rep bar)))
+ ;; (seq foo (rep (alt #t (rep bar))))
+ ;; (seq foo (seq bar (rep bar)))
+ ;; ((seq foo (rep (alt bar _.0))) (=/= ((_.0 . bar)) ((_.0 . foo))) (sym _.0))
+ ;; ((seq foo (rep (alt _.0 bar))) (=/= ((_.0 . bar)) ((_.0 . foo))) (sym _.0))
+ ;; ((seq foo (rep (seq bar (rep _.0)))) (=/= ((_.0 . bar)) ((_.0 . foo))) (sym _.0))
+ ;; (seq foo (rep (seq bar (rep bar))))
+ ;; (seq (alt #t foo) (rep bar))
+ ;; (seq foo (rep (seq bar (rep foo))))
+ ;; (seq foo (alt (rep bar) #t))
+ ;; (rep (alt (rep bar) foo))
+ ;; (seq foo (seq (rep bar) bar))
+ ;; ((seq foo (rep (seq (rep _.0) bar))) (=/= ((_.0 . bar)) ((_.0 . foo))) (sym _.0))
+ ;; (rep (alt #t (alt foo bar)))
+ ;; (seq foo (rep (seq (rep bar) bar)))
+ ;; ((seq foo (alt _.0 (rep bar))) (=/= ((_.0 . bar)) ((_.0 . foo))) (sym _.0))
+ ;; (seq foo (alt bar (rep bar)))
+ ;; (alt #t (rep (alt foo bar)))
+ ;; (rep (alt foo (alt #t bar))))
+
+ )
+
+(check-expect "20-ab"
+;;; takes around 10 seconds to generate 10,0000 answers under Petite
+;;; Here's the 1,000th answer
+ (car (reverse (run 1000 (q) (regex-matcho q '(foo bar bar bar)))))
+ '((seq foo (seq bar (seq (seq bar bar) (alt (alt (rep (alt _.0 _.1)) _.2) _.3))))
+ (=/= ((_.0 . _.1)))))
+
+(check-expect "20-a"
+ (run 1 (q) (regex-matcho '(alt #t (seq foo (rep bar))) '(foo bar bar bar)))
+ '(_.0))
+
+(check-expect "20-aa"
+ (run 1 (q) (regex-matcho '(alt (seq foo (rep bar)) #t) '(foo bar bar bar)))
+ '(_.0))
+
+(check-expect "20-c"
+ (run 1 (q) (d/dco '(alt #t (seq foo (rep bar))) 'foo q))
+ '((rep bar)))
+
+(check-expect "20-cc"
+ (run 1 (q) (d/dco '(alt (seq foo (rep bar)) #t) 'foo q))
+ '((rep bar)))
+
+(check-expect "20-c1"
+ (run 1 (q) (d/dco '#t 'foo q))
+ '())
+
+(check-expect "20-c2"
+ (run 1 (q) (d/dco '(seq foo (rep bar)) 'foo q))
+ '((rep bar)))
+
+(check-expect "20-d"
+ (run 1 (q) (d/dco '(alt (seq foo (rep bar)) #t) 'foo q))
+ '((rep bar)))
+
+(check-expect "20-e"
+ ;;; illegal alt with duplicate patterns
+ (run 1 (q) (d/dco '(alt (seq foo (rep bar)) (seq foo (rep bar))) 'foo q))
+ '())
+
+(check-expect "20-z"
+ (run 1 (q) (fresh (e1 e2) (regex-matcho q '(foo bar bar bar)) (== `(alt ,e1 ,e2) q)))
+ '((alt (seq foo (rep bar)) #t)))
+
+;;; look for the literal match regex
+;;; easy version
+(check-expect "21"
+ (run 1 (q)
+ (== `(seq foo (seq bar bar)) q)
+ (regex-matcho q
+ '(foo bar bar)))
+ '((seq foo (seq bar bar))))
+
+;;; look for the literal match regex
+;;; hard version (generate and test)
+(check-expect "22"
+ (run 1 (q)
+ (regex-matcho q
+ '(foo bar bar))
+ (== `(seq foo (seq bar bar)) q))
+ '((seq foo (seq bar bar))))
+
+;;; look for the literal match regex (longer)
+;;; easy version
+(check-expect "23"
+ (run 1 (q)
+ (== `(seq foo (seq bar (seq bar bar))) q)
+ (regex-matcho q
+ '(foo bar bar bar)))
+ '((seq foo (seq bar (seq bar bar)))))
+
+;;; look for the literal match regex (longer)
+;;; hard version (generate and test)
+(check-expect "24"
+ (run 1 (q)
+ (regex-matcho q
+ '(foo bar bar bar))
+ (== `(seq foo (seq bar (seq bar bar))) q))
+ '((seq foo (seq bar (seq bar bar)))))
+
+;;; generate regex, and data that matches.
+(check-expect "25"
+ (run 30 (q)
+ (fresh (regex data)
+ (regex-matcho regex
+ data)
+ (== `(,regex ,data) q)))
+ '((#t ()) (((rep _.0) ()) (sym _.0)) ((_.0 (_.0)) (sym _.0)) (((rep (seq _.0 _.1)) ()) (=/= ((_.0 . #t)) ((_.1 . #t)))) (((rep (alt _.0 _.1)) ()) (=/= ((_.0 . _.1)))) (((alt #t _.0) ()) (=/= ((_.0 . #t)))) (((alt _.0 #t) ()) (sym _.0)) (((alt (rep _.0) _.1) ()) (=/= ((_.1 rep _.0))) (sym _.0)) (((seq (rep _.0) (rep _.1)) ()) (sym _.0 _.1)) (((rep _.0) (_.0)) (sym _.0)) (((alt _.0 (rep _.1)) ()) (sym _.0 _.1)) (((alt (rep (seq _.0 _.1)) _.2) ()) (=/= ((_.0 . #t)) ((_.1 . #t)))) (((alt (rep (alt _.0 _.1)) _.2) ()) (=/= ((_.0 . _.1)))) (((seq (rep _.0) (rep (seq _.1 _.2))) ()) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) (((alt (alt #t _.0) _.1) ()) (=/= ((_.0 . #t)))) (((seq (rep _.0) (rep (alt _.1 _.2))) ()) (=/= ((_.1 . _.2))) (sym _.0)) (((seq (rep _.0) (alt #t _.1)) ()) (=/= ((_.1 . #t))) (sym _.0)) (((rep _.0) (_.0 _.0)) (sym _.0)) (((alt (seq _.0 _.1) #t) ()) (=/= ((_.1 . #t))) (sym _.0)) (((seq (rep (seq _.0 _.1)) (rep _.2)) ()) (=/= ((_.0 . #t)) ((_.1 . #t))) (sym _.2)) (((alt (alt _.0 #t) _.1) ()) (sym _.0)) (((alt (alt _.0 _.1) #t) ()) (=/= ((_.0 . _.1))) (sym _.0 _.1)) (((alt _.0 #t) (_.0)) (sym _.0)) (((seq (rep _.0) (alt _.1 #t)) ()) (sym _.0 _.1)) (((seq _.0 (rep _.1)) (_.0)) (sym _.0 _.1)) (((alt _.0 (rep (seq _.1 _.2))) ()) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) (((rep _.0) (_.0 _.0 _.0)) (sym _.0)) (((alt _.0 (rep (alt _.1 _.2))) ()) (=/= ((_.1 . _.2))) (sym _.0)) (((seq _.0 _.1) (_.0 _.1)) (sym _.0 _.1)) (((seq (rep (alt _.0 _.1)) (rep _.2)) ()) (=/= ((_.0 . _.1))) (sym _.2))))
+
+;;; generate regexs, and *non-empty* data, that match
+;;; This test was *extremely* slow under the naive miniKanren translation: even run 3 took a while.
+;;; Now run 1000 takes 4.5 seconds under Petite.
+(check-expect "27"
+ (run 20 (q)
+ (fresh (regex data)
+ (=/= '() data)
+ (regex-matcho regex
+ data)
+ (== `(,regex ,data) q)))
+ '(((_.0 (_.0)) (sym _.0)) (((rep _.0) (_.0)) (sym _.0)) (((rep _.0) (_.0 _.0)) (sym _.0)) (((alt _.0 #t) (_.0)) (sym _.0)) (((seq _.0 (rep _.1)) (_.0)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0)) (sym _.0)) (((seq _.0 _.1) (_.0 _.1)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (rep (seq _.1 _.2))) (_.0)) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) (((seq _.0 (rep (alt _.1 _.2))) (_.0)) (=/= ((_.1 . _.2))) (sym _.0)) (((seq _.0 (alt #t _.1)) (_.0)) (=/= ((_.1 . #t))) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((alt _.0 _.1) (_.0)) (=/= ((_.0 . _.1))) (sym _.0 _.1)) (((seq _.0 (alt _.1 #t)) (_.0)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((alt #t _.0) (_.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (alt (rep _.1) _.2)) (_.0)) (=/= ((_.2 rep _.1))) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0))))
+
+;;; generate regexs, and *non-null* data
+;;; This test was problematic under the naive mk translation.
+(check-expect "28"
+ (run 30 (q)
+ (fresh (regex data)
+ (=/= '() data)
+ (regex-matcho regex
+ data)
+ (== `(,regex ,data) q)))
+ '(((_.0 (_.0)) (sym _.0)) (((rep _.0) (_.0)) (sym _.0)) (((rep _.0) (_.0 _.0)) (sym _.0)) (((alt _.0 #t) (_.0)) (sym _.0)) (((seq _.0 (rep _.1)) (_.0)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0)) (sym _.0)) (((seq _.0 _.1) (_.0 _.1)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (rep (seq _.1 _.2))) (_.0)) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) (((seq _.0 (rep (alt _.1 _.2))) (_.0)) (=/= ((_.1 . _.2))) (sym _.0)) (((seq _.0 (alt #t _.1)) (_.0)) (=/= ((_.1 . #t))) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((alt _.0 _.1) (_.0)) (=/= ((_.0 . _.1))) (sym _.0 _.1)) (((seq _.0 (alt _.1 #t)) (_.0)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((alt #t _.0) (_.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (alt (rep _.1) _.2)) (_.0)) (=/= ((_.2 rep _.1))) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (seq (rep _.1) (rep _.2))) (_.0)) (sym _.0 _.1 _.2)) (((seq _.0 (rep _.1)) (_.0 _.1)) (sym _.0 _.1)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((rep (alt _.0 #t)) (_.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0)) (((seq _.0 (alt _.1 (rep _.2))) (_.0)) (sym _.0 _.1 _.2)) (((seq _.0 (alt (rep (seq _.1 _.2)) _.3)) (_.0)) (=/= ((_.1 . #t)) ((_.2 . #t))) (sym _.0)) (((rep _.0) (_.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0 _.0)) (sym _.0))))
+
+(check-expect "28-b"
+ (run 10 (q)
+ (fresh (a b c d regex data)
+ (== `(,a ,b ,b ,c ,c ,d) data)
+ (=/= a b)
+ (=/= b c)
+ (=/= c d)
+ (=/= d a)
+ (regex-matcho regex
+ data)
+ (== `(,regex ,data) q)))
+ '((((rep (alt _.0 _.1)) (_.0 _.1 _.1 _.0 _.0 _.1)) (=/= ((_.0 . _.1))) (sym _.0 _.1)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 _.3))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0))) (sym _.0 _.1 _.2 _.3)) (((seq _.0 (rep (alt _.1 _.2))) (_.0 _.1 _.1 _.2 _.2 _.1)) (=/= ((_.0 . _.1)) ((_.1 . _.2))) (sym _.0 _.1 _.2)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 (rep _.3)))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0))) (sym _.0 _.1 _.2 _.3)) (((rep (alt _.0 _.1)) (_.1 _.0 _.0 _.1 _.1 _.0)) (=/= ((_.1 . _.0))) (sym _.0 _.1)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 (seq _.3 (rep _.4))))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0))) (sym _.0 _.1 _.2 _.3 _.4)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 (alt _.3 #t)))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0))) (sym _.0 _.1 _.2 _.3)) (((seq _.0 (seq _.1 (rep (alt _.1 _.2)))) (_.0 _.1 _.1 _.2 _.2 _.1)) (=/= ((_.0 . _.1)) ((_.1 . _.2))) (sym _.0 _.1 _.2)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 (seq _.3 (rep (seq _.4 _.5)))))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0)) ((_.4 . #t)) ((_.5 . #t))) (sym _.0 _.1 _.2 _.3)) (((seq _.0 (seq _.1 (seq _.1 (seq _.2 (seq _.2 (seq _.3 (rep (alt _.4 _.5)))))))) (_.0 _.1 _.1 _.2 _.2 _.3)) (=/= ((_.0 . _.1)) ((_.1 . _.2)) ((_.2 . _.3)) ((_.3 . _.0)) ((_.4 . _.5))) (sym _.0 _.1 _.2 _.3))))
+
+(check-expect "29a"
+ (run 10 (q)
+ (fresh (regex data)
+ (== '(rep #t) regex)
+ (=/= '() data)
+ (regex-matcho regex data)
+ (== `(,regex ,data) q)))
+ '())
+
+(check-expect "29b"
+ (run 10 (q)
+ (fresh (regex data out)
+ (== '(rep #t) regex)
+ (regex-matcho regex data)))
+ '())
+
+(check-expect "29f"
+ (run 10 (q)
+ (fresh (regex data out)
+ (== '(seq #t #t) regex)
+ (regex-matcho regex data)))
+ '())
+
+(check-expect "29z"
+ (run* (q)
+ (fresh (regex data)
+ (== #t regex)
+ (=/= '() data)
+ (regex-matcho regex data)
+ (== `(,regex ,data) q)))
+ '())
+
+(check-expect "30"
+ (run* (q) (repo EPSILON q))
+ '(#t))
+
+;;; original tests
+
+(check-expect "31"
+ (run* (q) (d/dco 'baz 'f q))
+ '())
+
+(check-expect "32"
+ (run* (q) (d/dco '(seq foo barn) 'foo q))
+ '(barn))
+
+(check-expect "33"
+ (run* (q) (d/dco '(alt (seq foo bar) (seq foo (rep baz))) 'foo q))
+ '((alt bar (rep baz))))
+
+(check-expect "34"
+ (run* (q) (regex-matcho '(seq foo (rep bar))
+ '(foo bar bar bar)))
+ '(_.0))
+
+(check-expect "35"
+ (run* (q) (regex-matcho '(seq foo (rep bar))
+ '(foo bar baz bar bar)))
+ '())
+
+(check-expect "36"
+ (run* (q) (regex-matcho '(seq foo (rep (alt bar baz)))
+ '(foo bar baz bar bar)))
+ '(_.0))
+
View
649 mK-empty-set-as-failure/mk.scm
@@ -0,0 +1,649 @@
+;;; miniKanren with =/=, symbolo, numbero, and noo (A new goal) (noo
+;;; 'clasure x). not-in is gone; there are fewer uses of 'sym; and
+;;; no uses of 'num (except when creating numbero.)
+
+(define-syntax test-check
+ (syntax-rules ()
+ ((_ title tested-expression expected-result)
+ (begin
+ (printf "Testing ~s\n" title)
+ (let* ((expected expected-result)
+ (produced tested-expression))
+ (or (equal? expected produced)
+ (errorf 'test-check
+ "Failed: ~a~%Expected: ~a~%Computed: ~a~%"
+ 'tested-expression expected produced)))))))
+
+(define a->s (lambda (a) (car a)))
+(define a->c* (lambda (a) (cadr a)))
+(define a->t (lambda (a) (caddr a)))
+
+(define-syntax lambdag@
+ (syntax-rules (:)
+ ((_ (a) e) (lambda (a) e))
+ ((_ (a : s c* t) e)
+ (lambda (a)
+ (let ((s (a->s a)) (c* (a->c* a)) (t (a->t a)))
+ e)))))
+
+(define mzero (lambda () #f))
+(define unit (lambdag@ (a) a))
+(define choice (lambda (a f) (cons a f)))
+(define-syntax lambdaf@
+ (syntax-rules () ((_ () e) (lambda () e))))
+
+(define-syntax inc
+ (syntax-rules () ((_ e) (lambdaf@ () e))))
+
+(define empty-f (lambdaf@ () (mzero)))
+
+(define-syntax case-inf
+ (syntax-rules ()
+ ((_ e (() e0) ((f^) e1) ((a^) e2) ((a f) e3))
+ (let ((a-inf e))
+ (cond
+ ((not a-inf) e0)
+ ((procedure? a-inf) (let ((f^ a-inf)) e1))
+ ((not (and (pair? a-inf)
+ (procedure? (cdr a-inf))))
+ (let ((a^ a-inf)) e2))
+ (else (let ((a (car a-inf)) (f (cdr a-inf)))
+ e3)))))))
+(define take
+ (lambda (n f)
+ (cond
+ ((and n (zero? n)) '())
+ (else
+ (case-inf (f)
+ (() '())
+ ((f) (take n f))
+ ((a) (cons a '()))
+ ((a f) (cons a (take (and n (- n 1)) f))))))))
+
+(define empty-a '(() () ()))
+
+(define-syntax run
+ (syntax-rules ()
+ ((_ n (x) g0 g ...)
+ (take n
+ (lambdaf@ ()
+ ((fresh (x) g0 g ...
+ (lambdag@ (final-a)
+ (choice ((reify x) final-a) empty-f)))
+ empty-a))))))
+
+(define-syntax run*
+ (syntax-rules ()
+ ((_ (x) g ...) (run #f (x) g ...))))
+
+(define-syntax fresh
+ (syntax-rules ()
+ ((_ (x ...) g0 g ...)
+ (lambdag@ (a)
+ (inc
+ (let ((x (var 'x)) ...)
+ (bind* (g0 a) g ...)))))))
+
+(define-syntax bind*
+ (syntax-rules ()
+ ((_ e) e)
+ ((_ e g0 g ...) (bind* (bind e g0) g ...))))
+
+(define bind
+ (lambda (a-inf g)
+ (case-inf a-inf
+ (() (mzero))
+ ((f) (inc (bind (f) g)))
+ ((a) (g a))
+ ((a f) (mplus (g a) (lambdaf@ () (bind (f) g)))))))
+
+(define mplus
+ (lambda (a-inf f)
+ (case-inf a-inf
+ (() (f))
+ ((f^) (inc (mplus (f) f^)))
+ ((a) (choice a f))
+ ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))))))
+
+(define-syntax conde
+ (syntax-rules ()
+ ((_ (g0 g ...) (g1 g^ ...) ...)
+ (lambdag@ (a)
+ (inc
+ (mplus*
+ (bind* (g0 a) g ...)
+ (bind* (g1 a) g^ ...) ...))))))
+
+(define-syntax mplus*
+ (syntax-rules ()
+ ((_ e) e)
+ ((_ e0 e ...) (mplus e0
+ (lambdaf@ () (mplus* e ...))))))
+
+(define pr-t->tag
+ (lambda (pr-t)
+ (car (rhs pr-t))))
+
+(define pr-t->pred
+ (lambda (pr-t)
+ (cdr (rhs pr-t))))
+
+(define noo
+ (lambda (tag u)
+ (let ((pred (lambda (x) (not (eq? x tag)))))
+ (lambdag@ (a : s c* t)
+ (noo-aux tag u pred a s c* t)))))
+
+(define noo-aux
+ (lambda (tag u pred a s c* t)
+ (let ((u (if (var? u) (walk u s) u)))
+ (cond
+ ((pair? u)
+ (cond
+ ((pred u)
+ (let ((a (noo-aux tag (car u) pred a s c* t)))
+ (and a
+ ((lambdag@ (a : s c* t)
+ (noo-aux tag (cdr u) pred a s c* t))
+ a))))
+ (else (mzero))))
+ ((not (var? u))
+ (cond
+ ((pred u) (unit a))
+ (else (mzero))))
+ ((ext-t u tag pred s t) =>
+ (lambda (t0)
+ (cond
+ ((not (eq? t0 t))
+ (let ((t^ (list (car t0))))
+ (let ((c* (subsume t^ c*)))
+ (unit (subsume-t s c* t0)))))
+ (else (unit a)))))
+ (else (mzero))))))
+
+(define make-flat-tag
+ (lambda (tag pred)
+ (lambda (u)
+ (lambdag@ (a : s c* t)
+ (let ((u (if (var? u) (walk u s) u)))
+ (cond
+ ((not (var? u))
+ (cond
+ ((pred u) (unit a))
+ (else (mzero))))
+ ((ext-t u tag pred s t) =>
+ (lambda (t0)
+ (cond
+ ((not (eq? t0 t))
+ (let ((t^ (list (car t0))))
+ (let ((c* (subsume t^ c*)))
+ (unit (subsume-t s c* t0)))))
+ (else (unit a)))))
+ (else (mzero))))))))
+
+(define deep-tag?
+ (lambda (tag)
+ (not (or (eq? tag 'sym) (eq? tag 'num)))))
+
+;;; We can extend t with a deep tag provided
+;;; It is not in a singleton c of c* with the same
+;;; tag. That would mean lifting an innocent
+;;; constraint to an overarching constraint,
+;;; would be wrong. So, no change to c* or t.
+;;; in that case.
+
+(define ext-t
+ (lambda (x tag pred s t^)
+ (let ((x (walk x s)))
+ (let loop ((t t^))
+ (cond
+ ((null? t) (cons `(,x . (,tag . ,pred)) t^))
+ ((not (eq? (walk (lhs (car t)) s) x)) (loop (cdr t)))
+ ((eq? (pr-t->tag (car t)) tag) t^)
+ ((works-together? (pr-t->tag (car t)) tag)
+ (loop (cdr t)))
+ (else #f))))))
+
+(define works-together?
+ (lambda (t1 t2)
+ (or (deep-tag? t1) (deep-tag? t2))))
+
+(define subsume-t
+ (lambda (s c* t)
+ (let loop
+ ((x* (rem-dups (map lhs t)))
+ (c* c*)
+ (t t))
+ (cond
+ ((null? x*) `(,s ,c* ,t))
+ (else
+ (let ((c*/t (subsume-c*/t (car x*) s c* t)))
+ (loop (cdr x*) (car c*/t) (cdr c*/t))))))))
+
+(define rem-dups
+ (lambda (vars)
+ (cond
+ ((null? vars) '())
+ ((memq (car vars) (cdr vars))
+ (rem-dups (cdr vars)))
+ (else (cons (car vars) (rem-dups (cdr vars)))))))
+
+(define have-flat-tag?
+ (lambda (pred x)
+ (lambda (pr-t)
+ (let ((tag (pr-t->tag pr-t)))
+ (and
+ (not (deep-tag? tag))
+ (eq? (lhs pr-t) x)
+ (pred tag))))))
+
+(define subsume-c*/t
+ (lambda (x s c* t)
+ (cond
+ ((exists (have-flat-tag? (lambda (u) (eq? u 'sym)) x) t)
+ (subsumed-from-t-to-c* x s c* t '()))
+ ((exists (have-flat-tag? (lambda (u) (not (eq? u 'sym))) x) t)
+ `(,c* . ,(drop-from-t x t)))
+ (else `(,c* . ,t)))))
+
+(define drop-from-t
+ (lambda (x t)
+ (remp (lambda (pr-t)
+ (and
+ (eq? (lhs pr-t) x)
+ (deep-tag? (pr-t->tag pr-t))))
+ t)))
+
+(define subsumed-from-t-to-c*
+ (lambda (x s c* t t^)
+ (cond
+ ((null? t) `(,c* . ,t^))
+ (else
+ (let ((pr-t (car t)))
+ (let ((tag (pr-t->tag pr-t))
+ (y (lhs pr-t)))
+ (cond
+ ((and (eq? y x) (deep-tag? tag))
+ (subsumed-from-t-to-c* x s
+ (new-c* x tag c* s)
+ (cdr t)
+ t^))
+ (else
+ (subsumed-from-t-to-c* x s
+ c*
+ (cdr t)
+ (cons (car t) t^))))))))))
+
+(define new-c*
+ (lambda (x tag c* s)
+ (cond
+ ((exists
+ (lambda (c)
+ (and (null? (cdr c))
+ (eq? (walk (lhs (car c)) s) x)
+ (eq? (rhs (car c)) tag)))
+ c*)
+ c*)
+ (else (cons `((,x . ,tag)) c*)))))
+
+;;; End reading here.
+
+(define subsume
+ (lambda (t c*)
+ (remp (lambda (c)
+ (exists (subsumed-pr? t) c))
+ c*)))
+
+(define subsumed-pr?
+ (lambda (t)
+ (lambda (pr-c)
+ (let ((u (rhs pr-c)))
+ (and (not (var? u))
+ (let ((x (lhs pr-c)))
+ (let ((pr-t (assq x t)))
+ (and pr-t
+ (let ((tag (pr-t->tag pr-t)))
+ (cond
+ ((and (deep-tag? tag) (eq? tag u)))
+ ((not ((pr-t->pred pr-t) u)))
+ (else #f)))))))))))
+
+(define booleano
+ (lambda (x)
+ (conde
+ ((== #f x))
+ ((== #t x)))))
+
+(define symbolo (make-flat-tag 'sym symbol?))
+
+(define numbero (make-flat-tag 'num number?))
+
+(define =/=
+ (lambda (u v)
+ (lambdag@ (a : s c* t)
+ (cond
+ ((unify u v s) =>
+ (lambda (s0)
+ (cond
+ ((eq? s0 s) (mzero))
+ (else
+ (let ((p* (list (prefix-s s0 s))))
+ (let ((p* (subsume t p*)))
+ (let ((c* (append p* c*)))
+ (unit `(,s ,c* ,t)))))))))
+ (else (unit a))))))
+
+(define prefix-s
+ (lambda (s0 s)
+ (cond
+ ((eq? s0 s) '())
+ (else (cons (car s0)
+ (prefix-s (cdr s0) s))))))
+
+(define ==
+ (lambda (u v)
+ (lambdag@ (a : s c* t)
+ (cond
+ ((unify u v s) =>
+ (lambda (s0)
+ (cond
+ ((eq? s0 s) (unit a))
+ ((verify-c* c* s0) =>
+ (lambda (c*)
+ (cond
+ ((verify-t t s0) =>
+ (lambda (t)
+ (let ((c* (subsume t c*)))
+ (unit (subsume-t s0 c* t)))))
+ (else (mzero)))))
+ (else (mzero)))))
+ (else (mzero))))))
+
+(define verify-c*
+ (lambda (c* s)
+ (cond
+ ((null? c*) '())
+ ((verify-c* (cdr c*) s) =>
+ (lambda (c0*)
+ (let ((c (car c*)))
+ (cond
+ ((verify-c*-aux c c0* s))
+ (else (mzero))))))
+ (else #f))))
+
+(define verify-c*-aux
+ (lambda (c c0* s)
+ (cond
+ ((unify* c s) =>
+ (lambda (s0)
+ (and (not (eq? s0 s))
+ (cons (prefix-s s0 s) c0*))))
+ (else c0*))))
+
+(define verify-t
+ (lambda (t s)
+ (cond
+ ((null? t) '())
+ ((verify-t (cdr t) s) =>
+ (letrec ((rec
+ (lambda (u)
+ (let ((u (if (var? u) (walk u s) u)))
+ (let ((tag (pr-t->tag (car t)))
+ (pred (pr-t->pred (car t))))
+ (lambda (t0)
+ (cond
+ ((var? u)
+ (ext-t u tag pred s t0))
+ ((pair? u)
+ (if (deep-tag? tag)
+ (cond
+ (((rec (car u)) t0) =>
+ (rec (cdr u)))
+ (else #f))
+ (and (pred u) t0)))
+ (else (and (pred u) t0)))))))))
+ (rec (lhs (car t)))))
+ (else #f))))
+
+(define succeed (== #f #f))
+
+(define fail (== #f #t))
+
+(define var (lambda (dummy) (vector dummy)))
+(define var? (lambda (x) (vector? x)))
+(define lhs (lambda (pr) (car pr)))
+(define rhs (lambda (pr) (cdr pr)))
+
+(define walk
+ (lambda (x s)
+ (let ((a (assq x s)))
+ (cond
+ (a (let ((u (rhs a)))
+ (if (var? u) (walk u s) u)))
+ (else x)))))
+
+(define walk*
+ (lambda (v s)
+ (let ((v (if (var? v) (walk v s) v)))
+ (cond
+ ((var? v) v)
+ ((pair? v)
+ (cons (walk* (car v) s) (walk* (cdr v) s)))
+ (else v)))))
+
+(define unify
+ (lambda (u v s)
+ (let ((u (if (var? u) (walk u s) u))
+ (v (if (var? v) (walk v s) v)))
+ (cond
+ ((and (pair? u) (pair? v))
+ (let ((s (unify (car u) (car v) s)))
+ (and s
+ (unify (cdr u) (cdr v) s))))
+ (else (unify-nonpair u v s))))))
+
+(define unify-nonpair
+ (lambda (u v s)
+ (cond
+ ((eq? u v) s)
+ ((var? u)
+ (and (or (not (pair? v)) (valid? u v s))
+ (cons `(,u . ,v) s)))
+ ((var? v)
+ (and (or (not (pair? u)) (valid? v u s))
+ (cons `(,v . ,u) s)))
+ ((equal? u v) s)
+ (else #f))))
+
+(define valid?
+ (lambda (x v s)
+ (not (occurs-check x v s))))
+
+(define occurs-check
+ (lambda (x v s)
+ (let ((v (if (var? v) (walk v s) v)))
+ (cond
+ ((var? v) (eq? v x))
+ ((pair? v)
+ (or (occurs-check x (car v) s)
+ (occurs-check x (cdr v) s)))
+ (else #f)))))
+
+(define reify-s
+ (lambda (v)
+ (let reify-s ((v v) (r '()))
+ (let ((v (if (var? v) (walk v r) v)))
+ (cond
+ ((var? v)
+ (let ((n (length r)))
+ (let ((name (reify-name n)))
+ (cons `(,v . ,name) r))))
+ ((pair? v)
+ (let ((r (reify-s (car v) r)))
+ (reify-s (cdr v) r)))
+ (else r))))))
+
+(define reify-name
+ (lambda (n)
+ (string->symbol
+ (string-append "_" "." (number->string n)))))
+
+(define reify
+ (lambda (x)
+ (lambdag@ (a : s c* t)
+ (let ((v (walk* x s)))
+ (let ((r (reify-s v)))
+ (reify-aux r v
+ (let ((c* (remp
+ (lambda (c)
+ (anyvar? c r))
+ c*)))
+ (rem-subsumed c*))
+ (remp
+ (lambda (pr)
+ (var? (walk (lhs pr) r)))
+ t)))))))
+
+(define reify-aux
+ (lambda (r v c* t)
+ (let ((v (walk* v r))
+ (c* (walk* c* r))
+ (t (walk* t r)))
+ (let ((c* (sorter (map sorter c*)))
+ (p* (sorter
+ (map sort-t-vars
+ (partition* t)))))
+ (cond
+ ((and (null? c*) (null? p*)) v)
+ ((null? c*) `(,v . ,p*))
+ (else `(,v (=/= . ,c*) . ,p*)))))))
+
+(define sorter
+ (lambda (ls)
+ (sort lex<=? ls)))
+
+(define sort-t-vars
+ (lambda (pr-t)
+ (let ((tag (car pr-t))
+ (x* (sorter (cdr pr-t))))
+ (let ((reified-tag (tag->reified-tag tag)))
+ `(,reified-tag . ,x*)))))
+
+(define tag->reified-tag
+ (lambda (tag)
+ (if (deep-tag? tag)
+ (string->symbol
+ (string-append "no-"
+ (symbol->string tag)))
+ tag)))
+
+(define lex<=?
+ (lambda (x y)
+ (string<=? (datum->string x) (datum->string y))))
+
+(define datum->string
+ (lambda (x)
+ (call-with-string-output-port
+ (lambda (p) (display x p)))))
+
+(define anyvar?
+ (lambda (c r)
+ (cond
+ ((pair? c)
+ (or (anyvar? (car c) r)
+ (anyvar? (cdr c) r)))
+ (else (and (var? c) (var? (walk c r)))))))
+
+(define rem-subsumed
+ (lambda (c*)
+ (let rem-subsumed ((c* c*) (c^* '()))
+ (cond
+ ((null? c*) c^*)
+ ((or (subsumed? (car c*) (cdr c*))
+ (subsumed? (car c*) c^*))
+ (rem-subsumed (cdr c*) c^*))
+ (else (rem-subsumed (cdr c*)
+ (cons (car c*) c^*)))))))
+
+(define unify*
+ (lambda (c s)
+ (unify (map lhs c) (map rhs c) s)))
+
+(define subsumed?
+ (lambda (c c*)
+ (cond
+ ((null? c*) #f)
+ (else
+ (let ((c^ (unify* (car c*) c)))
+ (or
+ (and c^ (eq? c^ c))
+ (subsumed? c (cdr c*))))))))
+
+(define part
+ (lambda (tag t x* y*)
+ (cond
+ ((null? t)
+ (cons `(,tag . ,x*) (partition* y*)))
+ ((eq? (pr-t->tag (car t)) tag)
+ (let ((x (lhs (car t))))
+ (let ((x* (cond
+ ((memq x x*) x*)
+ (else (cons x x*)))))
+ (part tag (cdr t) x* y*))))
+ (else
+ (let ((y* (cons (car t) y*)))
+ (part tag (cdr t) x* y*))))))
+
+(define partition*
+ (lambda (t)
+ (cond
+ ((null? t) '())
+ (else
+ (part (pr-t->tag (car t)) t '() '())))))
+
+(define-syntax project
+ (syntax-rules ()
+ ((_ (x ...) g g* ...)
+ (lambdag@ (a : s c* t)
+ (let ((x (walk* x s)) ...)
+ ((fresh () g g* ...) a))))))
+
+(define-syntax conda
+ (syntax-rules ()
+ ((_ (g0 g ...) (g1 g^ ...) ...)
+ (lambdag@ (a)
+ (inc
+ (ifa ((g0 a) g ...)
+ ((g1 a) g^ ...) ...))))))
+
+(define-syntax ifa
+ (syntax-rules ()
+ ((_) (mzero))
+ ((_ (e g ...) b ...)
+ (let loop ((a-inf e))
+ (case-inf a-inf
+ (() (ifa b ...))
+ ((f) (inc (loop (f))))
+ ((a) (bind* a-inf g ...))
+ ((a f) (bind* a-inf g ...)))))))
+
+(define-syntax condu
+ (syntax-rules ()
+ ((_ (g0 g ...) (g1 g^ ...) ...)
+ (lambdag@ (a)
+ (inc
+ (ifu ((g0 a) g ...)
+ ((g1 a) g^ ...) ...))))))
+
+(define-syntax ifu
+ (syntax-rules ()
+ ((_) (mzero))
+ ((_ (e g ...) b ...)
+ (let loop ((a-inf e))
+ (case-inf a-inf
+ (() (ifu b ...))
+ ((f) (inc (loop (f))))
+ ((a) (bind* a-inf g ...))
+ ((a f) (bind* (unit a) g ...)))))))
+
+(define onceo (lambda (g) (condu (g))))
View
1  miniKanren-version/mk-rd.scm
@@ -667,3 +667,4 @@
'(foo bar baz bar bar)
q))
`(,regex-BLANK))
+
Please sign in to comment.
Something went wrong with that request. Please try again.