assoco.clj

gistfile1.clj

(ns clojure.core.logic.assoco
  (:refer-clojure :exclude [== reify inc not])
  (:use [clojure.core.logic minikanren prelude match disequality]))

;; defining assoc as a pure relation
;; a good example of the non-overlapping
;; clauses property. A given map can match
;; only one of the these clauses.

(defne assoco [m k v o]
  ([[] _ _ [[k v]]])
  ([[[k v] . _] _ _ m])
  ([[[k ?v]] _ _ [[k v]]]
     (!= ?v v))
  ([[[k ?v] . ?r] _ _ [[k v] . ?r]]
     (!= ?r ()) (!= ?v v) (!= m o))
  ([[[?j ?v]] _ _ [[?j ?v] [k v]]]
     (!= ?j k))
  ([[[?j ?u] . ?r] _ _ [[?j ?u] . ?o]]
     (!= ?r ()) (!= ?j k) (!= m o)
     (assoco ?r k v ?o)))

(comment
  ;; add k v pair to map
  ;; ------------------------------
  (run* [q]
    (assoco [] :a 1 q))
  ;; [[:a 1]]

  (run* [q]
    (assoco [[:a 1]] :a 1 q))
  ;; [[:a 1]]

  (run* [q]
    (assoco [[:a 1]] :a 2 q))
  ;; (([:a 2]))

  (run* [q]
    (assoco [[:a 1]] :b 2 q))
  ;; (([:a 1] [:b 2]))

  ;; infer k v
  ;; ------------------------------
  (run* [q]
    (exist [k v]
     (assoco [[:a 1]] k v
             [[:a 1] [:b 2]])
     (== q [k v])))
  ;; ([:b 2])

  ;; infer original map
  ;; ------------------------------
  (run* [q]
    (assoco q :a 1 [[:a 1]]))
  ;; ([] ([:a 1]) ([:a _.0]))  

  ;; keys must be unique
  ;; ------------------------------
  (run* [q]
    (assoco q :a 2
            [[:a 1] [:a 2]]))
  ;; ()

  ;; prevent contradiction
  ;; -----------------------------
  (run* [q]
    (assoco q :a 1 q)
    (assoco q :a 2 q))
  ;; ()

  (run* [q]
    (exist [k v]
     (assoco [[:a 1] [:b 1]] k v
             [[:a 1] [:b 1]])
     (== q k)))
  ;; (:a)
  ;; we can't use assoco to enumerate keys
  ;; because our code imposes so many
  ;; constraints in order to be strongly
  ;; terminating
)

(defn assoco* [m k v o]
  (fn [s]
    (let [f (fn [x]
              (let [x (walk s x)]
                (if (lvar? x) x (sort-by first (seq x)))))
          m (f m)
          o (f o)]
      ((assoco m k v o) s))))

(comment
  ;; assoco* deals w/ order
  ;; ------------------------------
  (run* [q]
    (exist [k v]
     (assoco* [[:a 1]] k v
              [[:b 2] [:a 1]])
     (== q [k v])))
  ;; ([:b 2])
  ;; this is because our maps are ordered
 )

(defne keyso [m k]
  ([[[k _] . _]])
  ([[[_ _] . ?r]]
     (keyso ?r k)))

(defne valso [m v]
  ([[[_ v] . _]])
  ([[[_ _] . ?r]]
     (valso ?r v)))

(defne containso [m k]
  ([[[k _] . _] _])
  ([[[?k _] . ?r] _]
     (!= ?k k)
     (containso ?r k)))

(defne findo [m k o]
  ([[[k ?v] . _] _ [k ?v]])
  ([[[?k _] . ?r] _ _]
     (!= k ?k)
     (findo ?r k o)))

(comment
   (run* [q]
     (containso [[:a 1]] :a))
   ;; (_.0)

   (run* [q]
     (findo [[:a 1] [:b 2]] :b q))
   ;; ([:b 2])

   (run* [q]
     (keyso [[:a 1] [:b 2]] q))
   ;; (:a :b)

   (run* [q]
     (valso [[:a 1] [:b 2]] q))
   ;; (1 2)
 )