                    (fresh [~@(rest var-vec)]
                      ~@clauses)))))
 
-
-;; ## Reificiation
-
-;; In miniKanren, reification refers to extracting the desired values
-;; from the stream of states you get as a result of executing a goal.
-(defn reify-name [n]
-  (symbol (str "_." n)))
-
-(defn reify-s [v s]
-  (reify-s* (walk v s) s))
-
-
-(extend-protocol IReifySubstitution
-  LVar
-  (reify-s* [v s] (let [n (reify-name (count s))]
-                    (assoc s v n)))
-
-  Object
-  (reify-s* [v s] s))
-
-
-(defn walk* [v s]
-  (let [v' (walk v s)]
-    (deep-walk v' s)))
-
-(extend-protocol IDeepWalk
-  LVar
-  (deep-walk [v s] v)
-
-  Object
-  (deep-walk [v s] v))
-
-
-(defn reify-state-first-var [st]
-  (let [v (walk* (lvar 0) (.s st))]
-    (walk* v (reify-s v {}))))
-
-(defn reify-state-lvar [st lv]
-  (let [v (walk* lv (.s st))]
-    (walk* v (reify-s v {}))))
-
-
-;;; run interface
-
 (defn call-empty-state [g]
   (g empty-state))
 

       (cons (.head $') (stream-to-seq (.next $')))))))


;; ## Goals

;; A *state* is a record containing a substitution map *s* and the id
;; of the next unbound logic variable *c*.

;; This is a logic programming system embedded in Clojure. It's made
;; of a few simple pieces, some surprising in their depth; we'll
;; examine them each in turn, then put them together and show how to
;; do some logic programming with the result.
;;
;; ## Audience
;;
;; This literate program is written for any Clojure programmer who
;; wants to know more about logic programming. You don't need a
;; particularly deep knowledge of logic programming going into this,
;; but it may help to have gone through a tutorial or two so you can
;; recognize the end when we get there.
;;
;; ## Overview
;;
;; We'll start by defining [*logic variables*](#lvars) (*lvars*) and
;; [*substition maps*](#substitutions). An lvar is a variable which
;; gets a value through an entry in the subsitution map. We then
;; define a [*walk*](#walk) function to get the value of an lvar out
;; of an existing substitution map.
;;
;; With those in place, we can define the [*unifier*](#unification), a
;; way to declare that two terms (which may include lvars) must be
;; equal and to compute what substitution map must be used to make
;; them equal.
;;
;; We then take a left turn into the most remarkable poart of
;; miniKanren, its definition of [*lazy streams*](#streams). These are
;; unordered streams that can be composed together in a fair way: no
;; one stream will monopolize all computing resources, instead
;; interleaving its computation and its results with other streams it
;; has been combined with.
;;
;; The above are the primitive elements; we can use them to start to
;; define the actual logic interpreter.  We begin with a definition of
;; [*interpreter state*](#goals), (which contains the current
;; substitution map and some other book-keeping information).
;;
;; Then we can create [*goal*](#goals) functions, which take a
;; prexisting interpreter state and return a stream of possible
;; interpreter states which meet the goal's constraints.  Several
;; useful *goal constructors* are defined: *===* (unify), *ldisj*
;; (logical or), *lconj* (logical and), *call-fresh* (call a function
;; with a newly allocated lvar) and some extended utilities.
;;
;; To translate streams of interpreter states (the output of each goal
;; function) to something more useful, we implement a
;; [*reify*](#reify) function that extract the desired information
;; from each state.
;;
;; Finally, we put the pieces together to define the
;; [programmer interface](#programmerInterface): the *run* and *run**
;; macros, *conde* and *fresh*, which will be familiar to any core.logic
;; or minikanren programmer.
;;
;; ### Extensibility
;;
;; We use Clojure's protocols in defining many of the above functions, in a bid
;; to make the core logic system extensible to new data structures. (this is
;; similar to core.logic) By way of example, and also to be able to do some
;; useful logic programming, extend the core to support sequences.
;;
;; First we have to define a custom linked-list type. Clojure doesn't
;; support 'improper lists', which are very useful for this
;; application.  We then extend the unifier and the reifier to support
;; this type and define the basic miniKanren sequence goals using it.
;; (*conso*, *firsto*, *resto*, *emptyo*)

(ns micro-logic.core
  (:require [micro-logic.protocols :refer :all]))


;; ## <a name="lvars"></a>Logic Variables
;;
;; Logic variables (lvars for short) are the unknown items that will
;; be given a value by the unifier. Each of them has an id (*c*); this
