check in wg211 demo prep

demos/wg211/1-example.rkt

@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require "mk.rkt")
+
+(defrel (appendo l1 l2 l3)
+  (conde
+    [(== l1 '()) (== l2 l3)]
+    [(fresh (first rest res)
+       (== l1 (cons first rest))
+       (== l3 (cons first res))
+       (appendo rest l2 res))]))
+
+(run* (l1 l2)
+  (appendo l1 l2 (list 1 2 3 4)))

demos/wg211/2-example-core.rkt

@@ -0,0 +1,29 @@
+#lang racket/base
+
+(require "mk-core.rkt")
+
+(defrel (appendo l1 l2 l3)
+  (disj2
+   (conj2 (== l1 '()) (== l2 l3))
+   (fresh1 (first)
+     (fresh1 (rest)
+       (fresh1 (res)
+         (conj2
+          (conj2
+           (== l1 (cons first rest))
+           (== l3 (cons first res)))
+          (appendo rest l2 res)))))))
+
+(run 5 (q)
+  (fresh1 (l1)
+    (fresh1 (l2)
+      (conj2 (== q (cons l1 (cons l2 '())))
+             (appendo l1 l2 (cons 1 (cons 2 (cons 3 (cons 4 '())))))))))
+
+
+
+
+;; What if I make a grammar mistake?
+
+#;(run 1 (q)
+    (fresh1 (q) q))

demos/wg211/3-example-with-binding.rkt

@@ -0,0 +1,25 @@
+#lang racket/base
+
+(require "mk-with-binding.rkt")
+
+(defrel (appendo l1 l2 l3)
+  (disj2
+   (conj2 (== l1 '()) (== l2 l3))
+   (fresh1 (first)
+     (fresh1 (rest)
+       (fresh1 (res)
+         (conj2
+          (conj2
+           (== l1 (cons first rest))
+           (== l3 (cons first res)))
+          (appendo rest l2 res)))))))
+
+(run 5 (q)
+  (fresh1 (l1)
+    (fresh1 (l2)
+      (conj2 (== q (cons l1 (cons l2 '())))
+             (appendo l1 l2 (cons 1 (cons 2 (cons 3 (cons 4 '())))))))))
+
+
+;; DrRacket understands binding structure now,
+;; and unbound references are errors.

demos/wg211/4-example-with-sugar.rkt

@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require "mk-with-sugar.rkt")
+
+(defrel (appendo l1 l2 l3)
+  (conde
+    [(== l1 '()) (== l2 l3)]
+    [(fresh (first rest res)
+       (== l1 (cons first rest))
+       (== l3 (cons first res))
+       (appendo rest l2 res))]))
+
+(run* (l1 l2)
+  (appendo l1 l2 (list 1 2 3 4)))

demos/wg211/5-example-compiled.rkt

@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require "mk.rkt")
+
+(defrel (appendo l1 l2 l3)
+  (conde
+    [(== l1 '()) (== l2 l3)]
+    [(fresh (first rest res)
+       (== l1 (cons first rest))
+       (== l3 (cons first res))
+       (appendo rest l2 res))]))
+
+(run* (l1 l2)
+  (appendo l1 l2 (list 1 2 3 4)))

demos/wg211/6-example-with-check.rkt

@@ -0,0 +1,21 @@
+#lang racket/base
+
+(module def racket
+  (require "mk.rkt")
+  (provide appendo)
+
+  (defrel (appendo l1 l2 l3)
+    (conde
+      [(== l1 '()) (== l2 l3)]
+      [(fresh (first rest res)
+         (== l1 (cons first rest))
+         (== l3 (cons first res))
+         (appendo rest l2 res))])))
+
+(module use racket
+  (require "mk.rkt" (submod ".." def))
+
+  (run* (l1 l2)
+    (appendo l1 l2 (list 1 2 3 4))))  ;; What if I make an arity mistake?
+
+(require 'use)

demos/wg211/compile-with-check.rkt

@@ -0,0 +1,68 @@
+#lang racket
+
+(provide compile-defrel compile-run (for-syntax record-relation-arity!))
+
+(require
+  "runtime.rkt"
+  syntax-spec
+  (for-syntax syntax/parse (only-in ee-lib compiled-from)))
+
+;; New
+(begin-for-syntax
+  (define-persistent-symbol-table relation-arity)
+
+  (define (record-relation-arity! relname arity)
+    (symbol-table-set! relation-arity relname arity)))
+
+(define-syntax compile-defrel
+  (syntax-parser
+    [(_ name (x ...) g)
+     #'(lambda (x ...)
+         (lambda (s)
+           (lambda ()
+             (#%app (compile-goal g) s))))]))
+
+(define-syntax compile-run
+  (syntax-parser
+    [(_ n (q) g)
+     #'(let ([q (var 'q)])
+        (map (reify q)
+             (run-goal n (compile-goal g))))]))
+
+(define-syntax compile-goal
+  (syntax-parser
+    #:datum-literals (succeed fail == disj2 conj2 fresh1)
+    [(_ succeed)
+     #'succeed-rt]
+    [(_ fail)
+     #'fail-rt]
+    [(_ (== t1 t2))
+     #`(==-rt (compile-term t1) (compile-term t2))]
+    [(_ (disj2 g1 g2))
+     #`(disj2-rt (compile-goal g1) (compile-goal g2))]
+    [(_ (conj2 g1 g2))
+     #`(conj2-rt (compile-goal g1) (compile-goal g2))]
+    [(_ (fresh1 (x) b))
+     #`(call/fresh 'x (lambda (x) (compile-goal b)))]
+    [(_ (relname t ...))
+     (let ([actual (length (attribute t))]
+           [expected (symbol-table-ref relation-arity #'relname)])
+       (when (not (= actual expected ))
+         (raise-syntax-error
+          #f
+          (format "wrong number of arguments to relation; actual ~a, expected ~a" actual expected)
+          (compiled-from #'relname))))
+
+     #'(relname (compile-term t) ...)]))
+
+(define-syntax compile-term
+  (syntax-parser
+    #:datum-literals (quote cons)
+    [(_ n:number)
+     #''n]
+    [(_ x:id)
+     #'x]
+    [(_ (quote t))
+     #''t]
+    [(_ (cons t1 t2))
+     #`(cons (compile-term t1) (compile-term t2))]))

demos/wg211/compile.rkt

@@ -0,0 +1,53 @@
+#lang racket
+
+(provide compile-defrel compile-run)
+
+(require
+  "runtime.rkt"
+  syntax-spec
+  (for-syntax syntax/parse))
+
+(define-syntax compile-defrel
+  (syntax-parser
+    [(_ name (x ...) g)
+     #'(lambda (x ...)
+         (lambda (s)
+           (lambda ()
+             (#%app (compile-goal g) s))))]))
+
+(define-syntax compile-run
+  (syntax-parser
+    [(_ n (q) g)
+     #'(let ([q (var 'q)])
+        (map (reify q)
+             (run-goal n (compile-goal g))))]))
+
+(define-syntax compile-goal
+  (syntax-parser
+    #:datum-literals (succeed fail == disj2 conj2 fresh1)
+    [(_ succeed)
+     #'succeed-rt]
+    [(_ fail)
+     #'fail-rt]
+    [(_ (== t1 t2))
+     #`(==-rt (compile-term t1) (compile-term t2))]
+    [(_ (disj2 g1 g2))
+     #`(disj2-rt (compile-goal g1) (compile-goal g2))]
+    [(_ (conj2 g1 g2))
+     #`(conj2-rt (compile-goal g1) (compile-goal g2))]
+    [(_ (fresh1 (x) b))
+     #`(call/fresh 'x (lambda (x) (compile-goal b)))]
+    [(_ (relname t ...))      
+     #'(relname (compile-term t) ...)]))
+
+(define-syntax compile-term
+  (syntax-parser
+    #:datum-literals (quote cons)
+    [(_ n:number)
+     #''n]
+    [(_ x:id)
+     #'x]
+    [(_ (quote t))
+     #''t]
+    [(_ (cons t1 t2))
+     #`(cons (compile-term t1) (compile-term t2))]))

demos/wg211/complete.rkt

@@ -0,0 +1,127 @@
+#lang racket
+
+(provide (all-defined-out))
+
+(require syntax-spec
+         "compile.rkt"
+         (for-syntax syntax/parse))
+
+;;
+;; Core syntax
+;;
+
+(syntax-spec
+  (binding-class term-variable)
+  (binding-class relation-name)
+
+  (extension-class term-macro)
+  (extension-class goal-macro)
+
+  (nonterminal term
+    #:allow-extension term-macro
+
+    n:number
+    x:term-variable
+    ((~literal quote) ())
+    ((~literal cons) t1:term t2:term))
+
+  (nonterminal goal
+    #:description "miniKanren goal"
+    #:allow-extension goal-macro
+
+    succeed
+    fail
+
+    (== t1:term t2:term)
+
+    (disj2 g1:goal g2:goal)
+    (conj2 g1:goal g2:goal)
+
+    (fresh1 (x:term-variable) b:goal)
+    #:binding {(bind x) b}
+
+    (r:relation-name t:term ...+)))
+
+
+;;
+;; Interface macros
+;;
+
+(syntax-spec
+  (host-interface/definition
+    (core-defrel (name:relation-name x:term-variable ...) g:goal)
+    #:binding [(export name) {(bind x) g}]
+
+    #:lhs
+    [(record-relation-arity! #'name (length (attribute x)))
+     #'name]
+
+    #:rhs
+    [#'(compile-defrel (x ...) g)])
+
+  (host-interface/expression
+    (core-run n:expr q:term-variable g:goal)
+    #:binding {(bind q) g}
+    #'(compile-run n q g)))
+
+
+;;
+;; Surface syntax
+;;
+
+(define-syntax list
+  (term-macro
+   (syntax-rules ()
+     [(list) '()]
+     [(list a rest ...) (cons a (list rest ...))])))
+
+(define-syntax disj
+  (goal-macro
+   (syntax-rules ()
+     ((disj) fail)
+     ((disj g) g)
+     ((disj g0 g ...) (disj2 g0 (disj g ...))))))
+
+(define-syntax conj
+  (goal-macro
+   (syntax-rules ()
+     ((conj) succeed)
+     ((conj g) g)
+     ((conj g0 g ...) (conj2 g0 (conj g ...))))))
+
+(define-syntax fresh
+  (goal-macro
+   (syntax-rules ()
+     ((fresh () g ...) (conj g ...))
+     ((fresh (x0 x ...) g ...)
+      (fresh1 (x0)
+              (fresh (x ...)
+                g ...))))))
+
+(define-syntax conde
+  (goal-macro
+   (syntax-rules ()
+     ((conde (g ...) ...)
+      (disj (conj g ...) ...)))))
+
+
+;;
+;; Surface syntax for interface macros
+;;
+
+(define-syntax defrel
+  (syntax-rules ()
+    [(defrel (name x ...) g ...)
+     (core-defrel (name x ...) (conj g ...))]))
+
+(define-syntax run
+  (syntax-rules ()
+    [(run n (x0 x ...) g ...)
+     (run n q (fresh (x0 x ...)
+                (== (list x0 x ...) q) g ...))]
+    [(run n q g ...)
+     (core-run n q (conj g ...))]))
+
+(define-syntax run*
+  (syntax-rules ()
+    ((run* q g ...) (run #f q g ...))))