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 is nearly twice as much code as the equivalent alphaProlog!

While it can be partially cleaned up with the defne pattern matching sugar, something more is necessray. We should perhaps provide a letsyn macro which delivers the intelligent handling of unquoted vars. Both 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.