acl2s.clj

(ns acl2s.core
  (:require [clojure.walk :as walk]))

(def replacements
  {'nat   `(fn [x#] (and (integer? x#) (<= 0 x#)))
   'plus  `+
   'minus `-})

(defn replace-symbols* [expr]
  (if-not (list? expr)
    expr
    (let [[expr & exprs] expr]
      `(~(replacements expr expr) ~@exprs))))

(defn replace-symbols [expr]
  (walk/postwalk replace-symbols* expr))

(defmacro defunc [name args & {:keys [input-test output-test body]}]
  `(defn ~name ~args
     (if ~(replace-symbols input-test)
       ~(replace-symbols body))))

(comment
  (macroexpand
    '(defunc foobar [x]
       :input-test (nat x)
       :body       (plus x (minus x x)))))