Better syntax support

Clojure syntax-quote leaves much to be desired when doing the symbolic manipulations that are common with the nominal functionality of core.logic. For example consider the following alphaProlog fragment program for describing the operational semantics of the pi-calculus:

step (tau P) tau_a P.
step (sum (P, Q)) A (P') :- step P A P'.
step (sum (P, Q)) A (Q') :- step Q A Q'.
step (par (P, Q)) A (par (P', Q)) :- step P A P'.
step (par (P, Q)) A (par (P, Q')) :- step Q A Q'.
step (par (ina,P)) tau_a P.
step (par (P,ina)) tau_a P.
step (par (P,Q)) tau_a (res (n\par(P',Q'))) 
	:- step' P (n\in_a(X,n)) (n\P'), step' Q (n\out_a(X,n)) (n\Q').
step (par (P,Q)) tau_a (res (n\par(P',Q'))) 
	:- step' P (n\out_a(X,n)) (n\P'), step' Q (n\in_a(X,n)) (n\Q').

step (res (n\P)) A (res (n\P')) :- step P A P', n # A.
step (out (X, Y, P)) (out_a (X, Y)) P.
step (par (P,Q)) tau_a (par (P'',Q'))  :- 
	step' P (y\in_a(X,Y)) (y\P'), 
	step Q (out_a(X,Z)) Q', 
	rename (y\P',Z,P'').
step (par (P,Q)) tau_a (par (P',Q''))  :- 
	step' Q (y\in_a(X,y)) (y\Q'), 
	step P (out_a(X,Z)) P', 
	rename (y\Q',Z,Q'').

step (rep P) A P' :- step (par (P, (rep P))) A P'.

Nada Amin's translation to core.logic currently looks like the following

(defn stepo [p a q]
  (conde
    [(== `(~'tau ~q) p)
     (== a 'tau_a)]
    [(fresh [p1 p2]
       (== `(~'sum ~p1 ~p2) p)
       (stepo p1 a q))]
    [(fresh [p1 p2]
       (== `(~'sum ~p1 ~p2) p)
       (stepo p2 a q))]
    [(fresh [p1 p2 q1]
       (== `(~'par ~p1 ~p2) p)
       (== `(~'par ~q1 ~p2) q)
       (stepo p1 a q1))]
    [(fresh [p1 p2 q2]
       (== `(~'par ~p1 ~p2) p)
       (== `(~'par ~p1 ~q2) q)
       (stepo p2 a q2))]
    [(== `(~'par ~'ina ~q) p)
     (== a 'tau_a)]
    [(== `(~'par ~q ~'ina) p)
     (== a 'tau_a)]
    [(fresh [p1 p2 q1 q2 x]
       (nom/fresh [n]
         (== `(~'par ~p1 ~p2) p)
         (== a 'tau_a)
         (== `(~'res ~(nom/tie n `(~'par ~q1 ~q2))) q)
         (b-stepo p1 (nom/tie n `(~'in_a ~x ~n)) (nom/tie n q1))
         (b-stepo p2 (nom/tie n `(~'out_a ~x ~n)) (nom/tie n q2))))]
    [(fresh [p1 p2 q1 q2 x]
       (nom/fresh [n]
         (== `(~'par ~p1 ~p2) p)
         (== a 'tau_a)
         (== `(~'res ~(nom/tie n `(~'par ~q1 ~q2))) q)
         (b-stepo p1 (nom/tie n `(~'out_a ~x ~n)) (nom/tie n q1))
         (b-stepo p2 (nom/tie n `(~'in_a ~x ~n)) (nom/tie n q2))))]
    [(fresh [p0 q0]
       (nom/fresh [n]
         (== `(~'res ~(nom/tie n p0)) p)
         (== `(~'res ~(nom/tie n q0)) q)
         (stepo p0 a q0)
         (nom/hash n a)))]
    [(fresh [x y]
       (== `(~'out ~x ~y ~q) p)
       (== a `(~'out_a ~x ~y)))]
    [(fresh [p1 p2 q1 q2 r1 x y z]
       (nom/fresh [y]
         (== `(~'par ~p1 ~p2) p)
         (== a 'tau_a)
         (== `(~'par ~r1 ~q1) q)
         (b-stepo p1 (nom/tie y `(~'in_a ~x ~y)) (nom/tie y q1))
         (stepo p2 `(~'out_a ~x ~z) q2)
         (renameo y z q1 r1)))]
    [(fresh [p1 p2 q1 q2 r2 x z]
       (nom/fresh [y]
         (== `(~'par ~p1 ~p2) p)
         (== a 'tau_a)
         (== `(~'par ~q1 ~r2) q)
         (b-stepo p2 (nom/tie y `(~'in_a ~x ~y)) (nom/tie y q2))
         (stepo p1 `(~'out_a ~x ~z) q1)
         (renameo y z q2 r2)))]))

This can be clean up with the defne pattern matching syntax but it is not enough. Something which could take it further would be support for a letsyn macro which supports some of the same behavior as defne. In order for this to really work for letfn and defne should support simple extensible parsing.

A cleaned up pi-calculus step relation might look something like the following:

(defne stepo [p a q]
  (['(tau ~q) 'tau_a _])
  (['(sum ~p1 ~p2)] (stepo p1 a q))
  (['(par ~p1 ~p2)] (stepo p2 a q))
  (['(par ~p1 ~p2) _ '(par ~q1 ~p2)] (stepo p1 a q1))
  (['(par ~p1 ~p2) _ '(par ~p1 ~q2)] (stepo p2 a q2))
  (['(par ina ~q) 'tau_a _])
  (['(par ~q ina) 'tau_a _])
  (['(par ~p1 ~p2) 'tau_a '(res (nom/tie n (par ~q1 ~q2)))]
     (letsyn [t0 (nom/tie n (in_a ~x ~n))
              t1 (nom/tie n ~q1)
              t2 (nom/tie n (out_a ~x ~n))
              t3 (nom/tie n ~q2)]
       (stepo' p1 t0 t1)
       (stepo' p2 t2 t3)))
  (['(par ~p1 ~p2) 'tau_a '(res (nom/tie ~(nom n) (par ~q1 ~q2)))]
     (letsyn [t0 (nom/tie n (out_a ~x ~n))
              t1 (nom/tie n ~q1)
              t2 (nom/tie n (in_a ~x ~n))
              t3 (nom/tie n ~q2)]
       (stepo' p1 t0 t1)
       (stepo' p2 t2 t3)))
  (['(res (nom/tie n p0)) _ '(res (nom/tie n q0))]
     (stepo p0 a q0)
     (nom/hash n a))
  (['(out ~x ~y ~q) '(out_a ~x ~y) _])
  (['(par ~p1 ~p2) 'tau_a '(par ~r1 ~q1)]
     (letsyn [t0 (nom/tie y (in_a ~x ~y))
              t1 (nomt/tie y ~q1)
              t2 (out_a ~x ~z)]
       (stepo' p1 t0 t1)
       (stepo p2 t2 q2)
       (renameo y z q1 r1)))
  (['(par ~p1 ~p2) 'tau_a '(par ~q1 ~r2)]
     (letsyn [t0 (nom/tie y (in_a ~x ~y))
              t1 (nom/tie y ~q2)
              t2 (out_a ~x ~z)]
       (stepo' p2 t0 t1)
       (stepo p1 t2 q1)
       (renameo y z q2 r2))))

This begins to approach the brevity and clarity of the alphaProlog implementation.