Created
April 1, 2017 19:39
-
-
Save moxaj/da60985e609916361a550a5f130df11f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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))))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment