Using unification to write readable macros

In my core.contracts code I've experimented with using unification to aide read and re-readability in my macros. Often I've found that I'll hit a wall when returning to a macro that I wrote long ago. A mass of documentation often helps, but I wanted something more. I think I've found it... or at least the beginnings of 'it'. Observe the following macro:

(defn- build-contract-body
 [[args cnstr descr :as V]]
 (unify/subst 
 '(?PARMS
 (let [ret ?PRE-CHECK]
 ?POST-CHECK))

 {'?ARGS args
 '?F 'f
 '?PARMS (vec (list* 'f args))
 '?MSG descr
 '?PRE-CHECK (build-condition-body {:pre (:pre cnstr)} '(apply ?F ?ARGS) "Pre-condition failure: ")
 '?POST-CHECK (build-condition-body {:post (:post cnstr)} 'ret "Post-condition failure: ")}))

This macro builds a datastructure that corresponds to a function body useful for tracking pre and post condition constraint failures. You'll see that the meat of the macro is simply:

'(?PARMS
 (let [ret ?PRE-CHECK]
 ?POST-CHECK))

My approach uses unification (subst from the core.unify library) to fill in the body variables ?PARMs, ?PRE-CHECK and ?POST-CHECK with further data structures. Specifically, the structures to fill are provided in a bindings map to subst and built directly or via another macro shown below:

(defn- build-condition-body
 [constraint-map body prefix-msg]
 (unify/subst
 '(try
 ((fn []
 ?CNSTR
 ?BODY))
 (catch AssertionError ae
 (throw (AssertionError. (str ?PREFIX ?MSG \newline (.getMessage ae))))))

 {'?CNSTR constraint-map
 '?PREFIX prefix-msg
 '?BODY body}))

Using this method allows me to effectively draw a picture of the data structure representing a function body and fill in the required values via variable substitution. I need to explore this deeper, but I like the initial findings.

It's a poor man's RHS of a define-syntax (maybe).