nat in miniKanren

nat.rkt

#lang racket

(require "Racket-miniKanren/minikanren/mk.rkt")

(defrel (conso a d p)
  (== (cons a d) p))

(defrel (caro p a)
  (fresh (d)
    (conso a d p)))

(defrel (cdro p d)
  (fresh (a)
    (conso a d p)))

(define (build-nat n)
  (cond
    ((= n 0) 'O)
    (else (cons 'S (build-nat (- n 1))))))

(define (unbox-nat n)
  (cond
    ((eq? n 'O) 0)
    (else (+ 1 (unbox-nat (cdr n))))))

(defrel (succo a-1 a)
  (conso 'S a-1 a))

(defrel (zero?o n)
  (== n 'O))

(defrel (pos?o n)
  (fresh (n-1)
    (succo n-1 n)))


(defrel (+o a b c)
  (conde
   ((zero?o a) (== b c))
   ((pos?o a)
    (fresh (a-1 prev)
      (succo a-1 a)
      (succo prev c)
      (+o a-1 b prev)))))


(defrel (*o a b c)
  (conde
   ((zero?o a) (zero?o c))
   ((pos?o a) (zero?o b) (zero?o c))
   ((pos?o a) (pos?o b)
    (fresh (a-1 prev)
      (succo a-1 a)
      (+o b prev c)
      (*o a-1 b prev)))))

(map
 (λ (p)
   (cons (unbox-nat (car p))
         (unbox-nat (cadr p))))
 (run* (x y)
  (*o x y (build-nat 120))))