logic.hy

(import [user-mu [*]])
(require user-mu)

;; Mostly translated from Scheme examples in "The Reasoned Schemer,"
;; by Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov.

(defn caro [p a]
  (fresh [d]
         (== (cons a d) p)))

(defn cdro [p d]
  (fresh [a]
         (== (cons a d) p)))

(defn conso [a d p]
  (== (cons a d) p))

(defn nullo [x]
  (== [] x))


;; (run 1 (fresh [q] (appendo/l [1 2] [3 4] q)))
;; => [[1, 2, 3, 4]]
;;
;; (ptake 1 (callgoal (fresh [q] (appendo/l [1 2] [3 4] q))))
;; => [[pmap({pset([2]): [2], pset([6]): [3, 4], pset([0]): (pset([1]) . pset([3])), pset([4]): 2, pset([1]): 1, pset([3]): (pset([4]) . pset([6])), pset([5]): []}) 7]]
;;
;; (run 6 (fresh [q a b] (== q [a b]) (appendo/l a b [1 2 3 4 5])))
;; (run* (fresh [q a b] (== q [a b]) (appendo/l a b [1 2 3 4 5])))
;; => [[[], [1 2 3 4 5]], [[1], [2 3 4 5]], [[1 2], [3 4 5]], [[1 2 3], [4 5]], [[1 2 3 4], [5]], [[1 2 3 4 5], []]]
;;
(defn appendo/l [l r out]
  "Just like `appendo`, but uses logic fns (conde, nullo, conso)"
  (conde
   ((nullo l) (== r out))
   ((fresh [a d res]
           (conso a d l)
           (conso a res out)
           (appendo/l d r res)))))

(defn pairo [p]
  (fresh [a d]
         (conso a d p)))

(defn unwrapo [x out]
  (conde
   [(== x out)]
   [(pairo x) (fresh [a]
                     (caro x a)
                     (unwrapo a out))]))

mu.hy

(import [pyrsistent [pmap
                     pset
                     PSet]]
        [types])

(defn list? [x]
  "Checks if this is a normal list"
  (instance? list x))

(defn seq? [x]
  "Checks for non-empty list"
  (and (list? x)
       (not (empty? x))))

(defn null? [c]
  (or (nil? c)
      (and (list? c)
           (empty? c))))

(defn pair? [c]
  (or (seq? c)
      (cons? c)))

(defn fn? [f]
  "Tests for a function"
  (instance? types.FunctionType f))


;; Variables "are represented as vectors that hold their variable index."
(defclass var [PSet]
  []
  (defn --new-- [self c]
    (.--new-- (super) self (pmap {c True})))

  (defn --str-- [self]
    (% "(var %s)" (first self)))
  
  (defn --repr-- [self]
    (str self)))

(defn var? [x]
  "Test if is logic var"
  (instance? var x))

;; State
(defn stor [&optional [m {}]]
  (pmap m))

(defn stor-get [s k]
  (.get s k))

(defn stor-contains? [s k]
  (.__contains__ s k))

(defn stor-assoc [s k v]
  "Associates key with value in a given state map, returning updated
   map"
  (.set s k v))

(defn stor-keys [s]
  (.keys s))

(defn num-stor-keys [s]
  (len (stor-keys s)))

(def empty-s (stor))
(def empty-state [empty-s 0])


;; walk
;;
;; (walk 1337 (pmap {}))
;; => 1337
;;
;; (walk (var 0) (pmap {}))
;; => pset([0])
;;
;; (walk (var 0) (pmap {(var 0) 1337}))
;; => 1337
;;
;; (walk (var 1) (pmap {(var 0) 1337 (var 1) (var 0)}))
;; => 1337
;;
(defn walk [u s]
  "Recursive lookup of logic var keys in a state map"
  (if (and (var? u) (stor-contains? s u))
    (walk (stor-get s u) s)
    u))

;; unify
;;
;; (unify 1337 1337 (pmap {}))
;; => pmap({})
;;
;; (unify 1337 1338 (pmap {}))
;; => False
;;
;; (unify [1 2 3] [1 2 3] (pmap {}))
;; => pmap({})
;;
;; (unify [1 2 3] [1 2 4] (pmap {}))
;; => False
;;
;; (unify [1 2 3] [1 2 3 4] (pmap {}))
;; => False
;;
;; (unify [1 2 3] [1 2 (var 0)] (pmap {}))
;; => pmap({pset([0]): 3})
;;
(defn unify [u1 v1 s1]
  "Unifies terms of the language by walking the state map for instances
   of logic variables

   - If two terms walk to the same variable the state map is returned.
   - When one of the terms walks to a variable, the state is extended.
   - If both walk to non-empty lists, the cars and then cdrs are are 
     unified recursively.
   - Non-variable, non-seqs unify if they are equal.
   - Otherwise unification fails and returns False."
  (let [u (walk u1 s1)
        v (walk v1 s1)
        s s1]
    (cond
     [(and (var? u) (var? v) (= u v)) s]

     [(var? u) (stor-assoc s u v)]
     [(var? v) (stor-assoc s v u)]

     [(and (pair? u) (pair? v))
      (let [s2 (unify (car u) (car v) s)]
        (and (coll? s2)
             (unify (cdr u) (cdr v) s2)))]
     
     [True (and (= u v) s)])))

;; empty result
(def mzero nil)

(defn unit [sc]
  "Lifts state into a stream"
  (cons sc mzero))

;; ==
;;
;; ((== 1 1) empty-state)
;; => ([pmap({}) 0])
;;
;; ((== 1 2) empty-state)
;; => nil
;;
(defn == [u v]
  "Takes two terms as args and returns a goal"
  (fn [[s c]]
    (let [s1 (unify u v s)]
      (if (coll? s1) (unit [s1 c]) mzero))))

;; ((callfresh (fn [q] (== q 5))) empty-state)
;; => ([pmap({pset([0]): 5}), 1])
;;
(defn callfresh [f]
  "Take a fn f with a goal body and returns a fn takes a state and
   applies the f to a newly created logic variable"
  (fn [[s c]]
    ((f (var c)) [s (inc c)])))


;; "or" and "and" | "and" and "or"

;; (mplus [1 2] [3 4])
;; => (1 2 3 . 4)
;;
(defn mplus [$1 $2]
  "Merges streams and applies some trampolining to avoid the depth
   first search that would be unfun for infinite streams"
  (cond
   [(null? $1) $2]

   [(fn? $1) (fn [] (mplus ($1) $2))]
   
   [True (cons (car $1) (mplus $2 (cdr $1)))]))

(defn bind [$ g]
  "Invokes a goal on each element of a stream and then either
   merges the results, or if results exhausted returns the empty
   stream"
  (cond
   [(null? $) mzero]
   
   [(fn? $) (fn [] (bind ($) g))]

   [True (mplus (g (car $)) (bind (cdr $) g))]))

;; ((callfresh (fn [q] (disj (== q 1) (== q 2)))) empty-state)
;; => ([pmap({pset([0]): 1}), 1] [pmap({pset([0]): 2}), 1])
;;
(defn disj [g1 g2]
  "Goal constructor like a logical `or`"
  (fn [sc] (mplus (g1 sc) (g2 sc))))

;; ((callfresh (fn [q] (conj (== q 1) (== q 1)))) empty-state)
;; => ([pmap({pset([0]): 1}), 1])
;;
(defn conj [g1 g2]
  "Goal constructor like a logical `and`"
  (fn [sc] (bind (g1 sc) g2)))

;; Works the same:
;; (callgoal (callfresh (fn [q] (conj (== q 1) (== q 1)))))
;; => ([pmap({pset([0]): 1}), 1])
;;
(defn callgoal [g]
  "Helper to which applies the given goal to the empty state"
  (g empty-state))


;; (callgoal (callfresh fives))
;; => RecursionError: maximum recursion depth exceeded
;; (defn fives [x]
;;   (disj (== x 5) (fn [sc] ((fives x) sc))))

;; Wrap the return in a closure:
;; (callgoal (callfresh fives))
;; => ([pmap({pset([0]): 5}), 1] <function fives.<locals>._hy_anon_fn_2.<locals>._hy_anon_fn_1 at 0x10a967048>)
(defn fives [x]
  "An infinite goal constructor of fives"
  (disj (== x 5) (fn [sc] (fn [] ((fives x) sc)))))

(defn sixes [x]
  "An infinite goal constructor of sixes"
  (disj (== x 6) (fn [sc] (fn [] ((sixes x) sc)))))

(defn pull [$]
  "Automatically invokes an immature stream, advancing the stream
   until it matures"
  (if (fn? $) (pull ($)) $))

;; (ptake 10 (callgoal (callfresh fives)))
;; => ([pmap({pset([0]): 5}) 1] ... x10
(defn ptake [n $1]
  "Invokes pull a given number of times to return the desired number
   of results from a stream"
  (if (zero? n) []
      (let [$ (pull $1)]
        (if (null? $) []
            (cons (car $)
                  (ptake (dec n) (cdr $)))))))

;; (ptake 10 (callgoal fives-and-sixes))
;; => ([pmap({pset([0]): 5}), 1] [pmap({pset([0]): 6}), 1] ...
;;    alternating ... x5 pairs
(def fives-and-sixes (callfresh (fn [x] (disj (fives x) (sixes x)))))

;; (callgoal a-and-b)
;; => ([pmap({pset([1]): 5, pset([0]): 7}) 2] [pmap({pset([1]): 6, pset([0]): 7}) 2])
(def a-and-b
  (conj
   (callfresh (fn [a] (== a 7)))
   (callfresh (fn [b] (disj (== b 5) (== b 6))))))

user_mu.hy

(import [mu [*]])

(defmacro/g! zzz [g]
  "The snooze macro"
  `(fn [g!sc] (fn [] (~g g!sc))))

;; (callgoal (callfresh sevens))
;; => ([pmap({pset([0]): 7}) 1] . <function sevens.<locals>._hy_anon_fn_2.<locals>._hy_anon_fn_1 at 0x10f59abf8>)
;;
(defn sevens [x]
  "An inifinte goal constructor of sevens, using the snooze macro"
  (disj (== x 7) (zzz (sevens x))))

(defmacro conj+ [&rest gs]
  (if (= (len gs) 1)
    `(zzz ~(car gs))
    `(conj (zzz ~(car gs)) (conj+ ~@(cdr gs)))))

(defmacro disj+ [g0 &rest gs]
  (if (> (len gs) 0)
    `(disj (zzz ~g0) (disj+ ~@gs))
    `(zzz ~g0)))

;; (run* (fresh [q x y] (== [x 5 y] q) (== [x y] [4 6])))
;; => [[4, 5, 6]]
;;
;; `fresh` is like *and*
(defmacro fresh [vars &rest body]
  "Used to declare an `and` relation"
  (if (empty? vars)
    `(conj+ ~@body)
    `(callfresh
      (fn [~(car vars)]
        (fresh ~(cdr vars) ~@body)))))

(defn walk* [v1 s]
  (let [v (walk v1 s)]
    (cond
     [(var? v) v]
     
     [(pair? v)
      (cons (walk* (car v) s)
            (walk* (cdr v) s))]

     [True v])))

(defn reify-s [v1 s]
  (let [v (walk v1 s)]
    (cond
     [(var? v)
      (let [n (reify-name (num-stor-keys s))]
        (stor-assoc s v n))]
     
     [(pair? v)
      (reify-s (cdr v) (reify-s (car v) s))]

     [True s])))

(defn reify-name [n]
  (HySymbol (+ "_." (str n))))

(defn reify-1st [[s c]]
  (walk* (var 0) s))

(defn reify-1st [[s c]]
  (let [v (walk* (var 0) s)]
    (walk* v (reify-s v empty-s))))

;; (list (map reify-1st (ptake 6 (callgoal (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5]))))))
;; => [[[], [1 2 3 4 5]], [[1], [2 3 4 5]], [[1 2], [3 4 5]], [[1 2 3], [4 5]], [[1 2 3 4], [5]], [[1 2 3 4 5], []]]
;;
;; (ptake 6 (callgoal (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5]))))
;; => [[pmap({pset([2]): [1, 2, 3, 4, 5], pset([1]): [], pset([0]): [pset([1]), pset([2])]}) 3], ... x6 states ... ]
(defn run [n g]
  (list (map reify-1st (ptake n (callgoal g)))))

;; (take-all (callgoal (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5]))))
;; => ... same as `ptake 6` ...
;;
(defn take-all [$1]
  "See also `ptake`, this consumes the entire stream"
  (let [$ (pull $1)]
    (if (null? $) [] (cons (car $) (take-all (cdr $))))))

;; (run* (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5])))
;; => [[[], [1 2 3 4 5]], [[1], [2 3 4 5]], [[1 2], [3 4 5]], [[1 2 3], [4 5]], [[1 2 3 4], [5]], [[1 2 3 4 5], []]]
;;
(defn run* [g]
  "See also `run`, this one provides all solutions"
  (list (map reify-1st (take-all (callgoal g)))))

;; (take-all (callgoal (fresh [q] (conde [(== q 5)] [(== q 6)]))))
;; => [[pmap({pset([0]): 5}) 1], [pmap({pset([0]): 6}) 1]]
;;
;; (run* (fresh [q] (conde [(== q 5)] [(== q 6)])))
;; => [5, 6]
;;
;; (run* (fresh [q x] (conde [(== q x) (== x 5)] [(== q 6)])))
;; => [5, 6]
;;
(defmacro conde [&rest gs]
  "Used to declare a series of `or` relations
   Each relation (clause) can contain one or many `and` goals"
  `(disj+ ~@(list (map (fn [l] `(conj+ ~@l)) gs))))

(defn appendo [l r out]
  (disj
   (conj (== l []) (== r out))
   (fresh [a d res]
          (== (cons a d) l)
          (== (cons a res) out)
          (appendo d r res))))

(defn appendo/e [l r out]
  "Just like `appendo`, but uses `conde`"
  (conde
   ((== [] l) (== r out))
   ((fresh [a d res]
           (== (cons a d) l)
           (== (cons a res) out)
           (appendo d r res)))))

;; (run 1 (fresh [q] (appendo [1 2] [3 4] q)))
;; => [[1, 2, 3, 4]]
;;
;; (ptake 1 (callgoal (fresh [q] (appendo [1 2] [3 4] q))))
;; => [[pmap({pset([2]): [2], pset([6]): [3, 4], pset([0]): (pset([1]) . pset([3])), pset([4]): 2, pset([1]): 1, pset([3]): (pset([4]) . pset([6])), pset([5]): []}) 7]]

;; (ptake 1 (callgoal (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5]))))
;; => [[pmap({pset([2]): [1, 2, 3, 4, 5], pset([1]): [], pset([0]): [pset([1]), pset([2])]}) 3]]
;;
;; (take-all (callgoal (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5]))))
;; => [[pmap({
;;            pset([0]): [pset([1]), pset([2])]
;;            pset([1]): [],
;;            pset([2]): [1, 2, 3, 4, 5],
;;           }) 3],
;;     [pmap({
;;            pset([0]): [pset([1]), pset([2])],
;;            pset([1]): (pset([3]) . pset([4])),
;;            pset([2]): [2, 3, 4, 5],
;;            pset([3]): 1,
;;            pset([4]): [],
;;            pset([5]): [2, 3, 4, 5]
;;           }) 6],
;;     [pmap({
;;            pset([0]): [pset([1]), pset([2])],
;;            pset([1]): (pset([3]) . pset([4])),
;;            pset([2]): [3, 4, 5],
;;            pset([3]): 1,
;;            pset([4]): (pset([6]) . pset([7])),
;;            pset([5]): [2, 3, 4, 5]
;;            pset([6]): 2,
;;            pset([7]): [],
;;            pset([8]): [3, 4, 5],
;;           }) 9],
;;     [pmap({
;;            pset([0]): [pset([1]), pset([2])],
;;            pset([1]): (pset([3]) . pset([4]))
;;            pset([2]): [4, 5],
;;            pset([3]): 1,
;;            pset([4]): (pset([6]) . pset([7])),
;;            pset([5]): [2, 3, 4, 5],
;;            pset([6]): 2,
;;            pset([7]): (pset([9]) . pset([10])),
;;            pset([8]): [3, 4, 5],
;;            pset([9]): 3,
;;            pset([10]): [],
;;            pset([11]): [4, 5],
;;           }) 12],
;;     [pmap({
;;            pset([0]): [pset([1]), pset([2])],
;;            pset([1]): (pset([3]) . pset([4]))
;;            pset([2]): [5],
;;            pset([3]): 1,
;;            pset([4]): (pset([6]) . pset([7])),
;;            pset([5]): [2, 3, 4, 5],
;;            pset([6]): 2,
;;            pset([7]): (pset([9]) . pset([10])),
;;            pset([8]): [3, 4, 5],
;;            pset([9]): 3,
;;            pset([10]): (pset([12]) . pset([13])),
;;            pset([11]): [4, 5],
;;            pset([12]): 4,
;;            pset([13]): [],
;;            pset([14]): [5],
;;           }) 15],
;;     [pmap({
;;            pset([0]): [pset([1]), pset([2])],
;;            pset([1]): (pset([3]) . pset([4]))
;;            pset([2]): [],
;;            pset([3]): 1,
;;            pset([4]): (pset([6]) . pset([7])),
;;            pset([5]): [2, 3, 4, 5],
;;            pset([6]): 2,
;;            pset([7]): (pset([9]) . pset([10])),
;;            pset([8]): [3, 4, 5],
;;            pset([9]): 3,
;;            pset([10]): (pset([12]) . pset([13])),
;;            pset([11]): [4, 5],
;;            pset([12]): 4,
;;            pset([13]): (pset([15]) . pset([16])),
;;            pset([14]): [5],
;;            pset([15]): 5,
;;            pset([16]): [],
;;            pset([17]): [],
;;           }) 18]]


;; (run 6 (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5])))
;; (run* (fresh [q a b] (== q [a b]) (appendo a b [1 2 3 4 5])))
;; => [[[], [1 2 3 4 5]], [[1], [2 3 4 5]], [[1 2], [3 4 5]], [[1 2 3], [4 5]], [[1 2 3 4], [5]], [[1 2 3 4 5], []]]


;; ground-appendo
;; SCHEME:
;; (test-check "ground appendo"
;;   (car ((ground-appendo empty-state)))
;;   '(((#(2) b) (#(1)) (#(0) . a)) . 3))
;;
;; (def ground-appendo (appendo ['a] ['b] ['a 'b]))
;; (take-all (callgoal ground-appendo))
;; => [[pmap({pset([2]): ['b'], pset([1]): [], pset([0]): 'a'}) 3]]