playing with termito rewriting in clojure

ex.clj

(ns rewrite.ex
  (:require [clojure.core.logic :refer [defnc fnc]]
            [termito.core :refer [defrules simplify simplify-one]]))

(defnc numberc [x]
  (number? x))

(defrules bad
  [:dog :cat]
  [:cat :dog])


(defrules n-rule
  [(n 0)
   :zero]
  [(n (s ?x))
   (s (n ?x))]
  [(n ?n)
   :when [?n ~numberc]
   :with [?n1 [?n] ~dec]
   (n (n ?n1))])

;; sum [m_,0] := m;
;; sum [m_,s[n_]] := s[sum[m,n]];
(defrules s-rule
  [(+ ?x 0)
   ?x]
  [(+ ?x (s ?y))
   (s (+ ?x ?y))])

(def rules (concat bad
                   n-rule
                   s-rule))


(comment
  (simplify '(n) rules)
  ;; (n)

  (simplify '(n 0) rules)
  ;; :zero

  (simplify '(n 5) rules)
  ;; (n (n (n (n (n :zero)))))

  (simplify '(+ (s (s 0)) (s (s (s (s 0))))) s-rule)
  ;; (s (s (s (s (s (s 0))))))

  (simplify '(dog cat) s-rule)
  ;; (dog cat)

  )