Playing miniKanren!

miniKanren-test0.ss

; playing with miniKanren!

(load "mk.ss")
(load "mkextraforms.ss")
(load "mkprelude.ss")

; data Nat : Set where
(define nato
  (lambda (n)
    (conde [(zeroo n) succeed]    ; zero : Nat
           [else                  ; suc : Nat -> Nat
            (fresh (m)
                   (suco n m)
                   (nato m))])))

; representation of zero
(define zeroo
  (lambda (n) (== n '(zero))))

; representation of suc _
(define suco
  (lambda (n m)
    (conso 'suc m n)))

(define addo
  (lambda (n m k)
    (conde [(zeroo n) (== m k)]
           [else
            (fresh (n^ res)
                   (suco n n^)
                   (suco k res)
                   (addo n^ m res))])))

(define mulo
  (lambda (n m k)
    (conde [(zeroo n) (zeroo k)]
           [else
            (fresh (n^ res)
                   (suco n n^)
                   (addo m res k)
                   (mulo n^ m res))])))

(define test
  (lambda ()
    (for-each (lambda (u)
                (cond [(list? u) (pretty-print u)]
                      [else (display u) (newline)]))
              `("The first 5 natural number"
                ,(run 5 (n)
                      (nato n))
                "--"
                "2 + 3 = ?"
                ,(run* (r)
                       (addo '(suc suc zero) '(suc suc suc zero) r))
                "--"
                "2 + ? = 4, found 1 solution"
                ,(run* (x)
                       (addo '(suc suc zero) x '(suc suc suc suc zero)))
                "--"
                "2 + ? = 4, found all solution(s)"
                ,(run* (x)
                       (addo '(suc suc zero) x '(suc suc suc suc zero)))
                "--"
                "? + 2 = 4, found 1 solution"
                ,(run* (x)
                       (addo x '(suc suc zero) '(suc suc suc suc zero)))
                "--"
                "? + ? = 2, found 2 solutions."
                ,(run* (r)
                       (fresh (x y)
                              (addo x y '(suc suc zero))
                              (== `(,x ,y) r)))
                "--"
                "2 * 3 = ?"
                ,(run* (r)
                       (mulo `(suc suc zero) `(suc suc suc zero) r))
                "--"
                "x + ? = 4 where x >= 2; found 2 solutions."
                ,(run* (r)
                       (fresh (x y p q)
                              (addo x y '(suc suc suc suc zero))
                              (suco x p)
                              (suco p q)
                              (== `(,x ,y) r)))
                "--"
                "? + y = 4 where x >= 2; found 2 solutions."
                ,(run* (r)
                       (fresh (x y p q)
                              (addo x y '(suc suc suc suc zero))
                              (suco y p)
                              (suco p q)
                              (== `(,x ,y) r)))))))