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).

:F