;; lib/minikanren/peano.sx — Peano-encoded natural-number relations.
;;
;; Same encoding as `lengtho`: zero is the keyword `:z`; successors are
;; `(:s n)`. So 3 = `(:s (:s (:s :z)))`. `(:z)` and `(:s ...)` are normal
;; SX values that unify positionally — no special primitives needed.
;;
;; Peano arithmetic is the canonical miniKanren way to test addition /
;; multiplication / less-than relationally without an FD constraint store.
;; (CLP(FD) integers come in Phase 6.)

(define zeroo (fn (n) (== n :z)))

(define succ-of (fn (n m) (== m (list :s n))))

(define
  pluso
  (fn
    (a b c)
    (conde
      ((== a :z) (== b c))
      ((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (pluso a-1 b c-1))))))

(define minuso (fn (a b c) (pluso b c a)))

(define lteo (fn (a b) (fresh (k) (pluso a k b))))

(define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b))))

(define
  eveno
  (fn
    (n)
    (conde
      ((== n :z))
      ((fresh (m) (== n (list :s (list :s m))) (eveno m))))))

(define
  oddo
  (fn
    (n)
    (conde
      ((== n (list :s :z)))
      ((fresh (m) (== n (list :s (list :s m))) (oddo m))))))

(define
  *o
  (fn
    (a b c)
    (conde
      ((== a :z) (== c :z))
      ((fresh (a-1 ab-1) (== a (list :s a-1)) (*o a-1 b ab-1) (pluso b ab-1 c))))))