 
 
 
-;; # Streams
+;; # <a name="streams"></a>Lazy Streams
 ;;
 ;; The lazy stream mechanism is one of the really interesting parts
 ;; about miniKanren. It's different from regular scheme linked lists

  nil
  (walk [u s] nil))

;; # Unification

(defn unify
  "Given two terms *u* and *v*, and an existing substitution map *s*,

;; 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
