Possible syntaxes for flexible unifier w/ multi-lvar constraints

gistfile1.clj

;;Support for simple constraints on lvars during unification was added in 76fd4d7c:
;;
;;    https://github.com/clojure/core.logic/commit/76fd4d7c155161d74ad5cd8d87955148eece1fe0
;;
;;but these constraints apply to a single lvar only.
;;The unifier could support more general constraints if it accepted an explicit predicate function.

;;For instance, given this `data-numeric?` predicate and `spec` data:

(defn data-numeric? [data dimension]
  (number? (-> data first dimension)))

(def spec {:data (repeatedly 10 #(hash-map :val (rand) :cat (rand-nth [:a :b :c])))
           :mapping {:y :val}})

;;I'd like a unifier call that has the same semantics as:

(run* [q]
      (fresh [data dim]
             (== spec {:data data :mapping {:y dim}})
             (project [data dim]
                      (== true (data-numeric? data dim)))
             (== q :success)))

;;A concise syntax is

(unifier1 spec
          '{:data ?data :mapping {:y ?dim}}
          '(data-numeric? ?data ?dim))

;;but that would require `unifier1` to
;; + prep all of its arguments together
;; + treat its third argument (or last, if more than 3 args) specially
;; + prep, project, and eval the predicate form, which feels gross.

;;We can avoid the last-argument issue via a dynamic var:

(binding [*unifier-constraints* '(data-numeric? ?data ?dim)]
  (unifier2 spec))

;;This maintains backwards compatibilty at the expense of being klunky (and suffers from the same prep+project+eval issue).

;;A more programmatically flexible syntax:

(unifier3 '[spec {:data ?data :mapping {:y ?dim}}
            :where
            [data-numeric? ?data ?dim]])

;;where everything before the `:where` is something to unify and everything after is a tuple of the form [predicate & lvar-arguments].
;;This syntax could be used with the existing unifier since the single-arity implementation is currently undefined.


;;Another option is to pass a map of constraints as the unifier's third arg:

(unifier4 spec '{:data ?data :mapping {:y ?dim}}
          {data-numeric? '[?data ?dim]
           '?dim keyword?})

;;the map can have entries (constraint-fn -> vector of args) for complex constraints of multiple lvars or (lvar symbol -> constraint-fn) for simple constraints on a single argument.
;;Since the constraint function is given grounded vals, this form could support "or" constraints via set literals.

(unifier4 m '{:a 1 :b ?b}
          '{?b #{1 5}})

;;succeeds for m equal to {:a 1 :b 1} OR {:a 1 :b 5}

;;In any of these syntaxes, I'm not sure if we can/want to support anonymous functions, or if in that case the user should just ball up and write a full run* form.

Ping: @swannodette.

@swannodette, here's the scaffold implementation you requested on IRC for the variable-arity unifier to accept an optional :where clause and constraint map in the last position.

(defn unify-with-constraint-map [terms m]
  (prn [terms m]))

(defn unifier
  [u w & ts]
  (let [[where constraint-map] (take-last 2 ts)]
    (if (= where :where)
      (unify-with-constraint-map
        (concat [u w] (drop-last 2 ts))
        constraint-map)
      (unify-with-constraint-map (concat [u w] ts) {}))))


(unifier :u :w 1 2 3 :where {:c :m})
;; => [(:u :w 1 2 3) {:c :m}]
(unifier :u :w :where {:c :m})
;; => [(:u :w) {:c :m}]
(unifier :u :w :z)
;; => [(:u :w :z) {}]