Merge pull request 0xc1c4da#2 from jarradh/deriver

Update Deriver

project.clj

@@ -15,6 +15,7 @@
             [jonase/eastwood "0.2.3"]
             [lein-kibit "0.1.2"]
             [cider/cider-nrepl "0.11.0-SNAPSHOT"]]
+  :eastwood {:exclude-namespaces [nal.rules]}
   :target-path "target/%s"
   :repl-options {:init-ns          narjure.repl
                  :nrepl-middleware [narjure.repl/narsese-handler]}

src/nal/deriver.clj

@@ -1,36 +1,22 @@
 (ns nal.deriver
   (:require
     [nal.deriver.utils :refer [walk]]
-    [nal.deriver.key-path :refer [mall-paths all-paths path mpath-invariants]]
+    [nal.deriver.key-path :refer [mall-paths all-paths mpath-invariants
+                                  path-with-max-level]]
     [nal.deriver.rules :refer [rule]]))
 
-;!s.contains("task(") && !s.contains("measure_time(") && !s.contains("Structural") && !s.contains("Identity") && !s.contains("Negation")
-(defn child? [parent child]
-  (when-not (= child parent)
-    (let [[f _ l] child
-          [pf _ pl] parent
-          fp-inv (set (mpath-invariants pf))
-          fl-inv (set (mpath-invariants pl))]
-      (and (fp-inv f) (fl-inv l)))))
-
-(defn remove-children [paths]
-  (reduce #(remove (partial child? %2) %1) paths paths))
-
 (defn get-matcher [rules p1 p2]
-  (let [paths (->> (mall-paths p1 p2)
-                   (filter rules)
-                   remove-children)
-        matchers (->> (filter rules paths)
+  (let [matchers (->> (mall-paths p1 p2)
+                      (filter rules)
                       (select-keys rules)
-                      vals
-                      (map :matcher))]
+                      (map (fn [el] (:matcher (second el)))))]
     (case (count matchers)
       0 (constantly [])
       1 (first matchers)
       (fn [t1 t2] (mapcat #(% t1 t2) matchers)))))
 
 (def mget-matcher (memoize get-matcher))
-(def mpath (memoize path))
+(def mpath (memoize path-with-max-level))
 (defn generate-conclusions
   [rules {p1 :statement :as t1} {p2 :statement :as t2}]
   (let [matcher (mget-matcher rules (mpath p1) (mpath p2))]

src/nal/deriver/key_path.clj

@@ -8,6 +8,18 @@
       (conj (map path tail) fst))
     :any))
 
+(defn path-with-max-level
+  ([statement] (path-with-max-level 0 statement))
+  ([level statement]
+   (if (coll? statement)
+     (let [[fst & tail] statement]
+       (cons fst
+             (if (> 1 level)
+               (let [next-level (if (= 'conj fst) level (inc level))]
+                 (map #(path-with-max-level next-level %) tail))
+               (repeat (count tail) :any))))
+     :any)))
+
 (defn rule-path
   "Generates detailed pattern for the rule."
   [p1 p2]
@@ -35,6 +47,7 @@
 
 (def mpath-invariants (memoize path-invariants))
 
+;(all-paths 'Y '(==> (seq-conj X A1 A2 A3) B))
 (defn all-paths
   "Generates all pathes for pair of premises."
   [p1 p2]

src/nal/deriver/list_expansion.clj

@@ -2,6 +2,8 @@
   (:require [nal.deriver.utils :refer [walk]]
             [clojure.string :as s]))
 
+(def max-elements-in-list 7)
+
 (defn get-list
   "Finds the first :list element in the rule."
   [prefix statement]
@@ -49,7 +51,7 @@
               (if-let [from-name (get-list ":from" st)]
                 (expand-:from-element st from-name l-name %)
                 [st]))
-            (range 1 6))))
+            (range 1 (inc max-elements-in-list)))))
 
 (defn contains-list?
   "Checks if rule contains any :list element."

src/nal/deriver/matching.clj

@@ -8,7 +8,7 @@
     [nal.deriver
      [set-functions :refer [f-map not-empty-diff? not-empty-inter?]]
      [substitution :refer [munification-map substitute]]
-     [preconditions :refer [sets compound-precondition shift-transformation
+     [preconditions :refer [sets compound-precondition conclusion-transformation
                             implications-and-equivalences get-terms abs
                             preconditions-transformations]]
      [normalization :refer [commutative-ops sort-commutative reducible-ops]
@@ -23,7 +23,8 @@
     `sort-commutative `n/reduce-ext-inter `n/reduce-symilarity `complement
     `n/reduce-int-dif `n/reduce-and `n/reduce-ext-dif `n/reduce-image
     `n/reduce-int-inter `n/reduce-neg `n/reduce-or `nil? `not `or `abs
-    `implications-and-equivalences `get-terms `empty? `intersection})
+    `implications-and-equivalences `get-terms `empty? `intersection
+    `n/reduce-seq-conj})
 
 (defn quote-operators
   [statement]
@@ -53,7 +54,7 @@
                      :goal (assoc conclusion :desire (list df t1 t2))
                      conclusion)]
     (if sc
-      (shift-transformation sc conclusion)
+      (conclusion-transformation sc conclusion)
       conclusion)))
 
 (defn traverse-node

src/nal/deriver/normalization.clj

@@ -85,7 +85,7 @@
     [_ ['ext-inter & l1] l2] (union 'ext-inter l1 [l2])
     [_ l1 ['ext-inter & l2]] (union 'ext-inter [l1] l2)
     [_ ['int-set & l1] ['int-set & l2]] (union 'int-set l1 l2)
-    [_ ['ext-set & l1] ['ext-set & l2]] (union 'ext-set l1 l2)
+    ;[_ ['ext-set & l1] ['ext-set & l2]] (union 'ext-set l1 l2)
     :else st))
 
 (defn reduce-int-inter
@@ -156,6 +156,14 @@
     ['conj t1 t2] (if (= t1 t2) t1 st)
     :else st))
 
+(defn reduce-seq-conj
+  [st]
+  (let [cnt (count st)]
+    (cond
+      (= 3 cnt) (second st)
+      (odd? cnt) (vec (butlast st))
+      :else st)))
+
 (def reducible-ops
   {'ext-inter `reduce-ext-inter
    '|         `reduce-int-inter

src/nal/deriver/preconditions.clj

@@ -1,12 +1,13 @@
 (ns nal.deriver.preconditions
   (:require [nal.deriver.set-functions
              :refer [f-map not-empty-diff? not-empty-inter?]]
-            [nal.deriver.substitution :refer [munification-map]]
             [nal.deriver.utils :refer [walk]]
             [nal.deriver.substitution :refer [substitute munification-map]]
             [nal.deriver.terms-permutation :refer [implications equivalences]]
             [clojure.set :refer [union intersection]]
-            [narjure.defaults :refer [duration]]))
+            [narjure.defaults :refer [duration]]
+            [clojure.core.match :as m]
+            [nal.deriver.normalization :refer [reduce-seq-conj]]))
 
 (defn abs [^long n] (Math/abs n))
 
@@ -144,22 +145,57 @@
   [conclusion preconditions]
   (reduce check-precondition conclusion preconditions))
 
-(defn shift-transformation
-  [[type arg1 [_ arg2]] conclusion]
-  (let [dur (if (= :shift-occurrence-forward type)
-              duration
-              (- duration))]
-    (cond
-      (and (= :unused arg1) ('#{=|> ==>} arg2)) conclusion
-      (and (= :unused arg1) (not ('#{=|> ==>} arg2)))
-      `(let [:t-occurrence (~(if (= arg2 'pred-impl) `+ `-)
-                            :t-occurrence ~dur)]
-         ~conclusion)
-      ('#{=|> ==>} arg2)
-      `(let [:t-occurrence (+ :t-occurrence ~arg1)]
-         ~conclusion)
-      :default
-      `(let [:t-occurrence (+ (~(if (= arg2 'pred-impl) `+ `-)
-                               :t-occurrence ~dur)
-                              ~arg1)]
-         ~conclusion))))
+;-------------------------------------------------------------------------------
+(defmulti conclusion-transformation (fn [arg1 _] (first arg1)))
+
+(defn shift-forward-let
+  ([sym conclusion] (shift-forward-let sym nil conclusion nil))
+  ([sym op conclusion duration]
+   `(let [interval# ~sym
+          ~@(if duration
+              `[:t-occurrence (~op :t-occurrence ~duration)]
+              [])
+          :t-occurrence (if interval# (+ :t-occurrence interval#)
+                                      :t-occurrence)]
+      ~conclusion)))
+
+(defmethod conclusion-transformation :shift-occurrence-forward
+  [args concl]
+  (m/match (mapv #(if (and (coll? %) (= 'quote (first %)))
+                   (second %) %) (rest args))
+    [(:or '=|> '==>)] concl
+    ['pred-impl] `(let [:t-occurrence (+ :t-occurrence ~duration)] ~concl)
+    ['retro-impl] `(let [:t-occurrence (- :t-occurrence ~duration)] ~concl)
+    [sym (:or '=|> '==>)] (shift-forward-let sym concl)
+    [sym 'pred-impl] (shift-forward-let sym `+ concl duration)
+    [sym 'retro-impl] (shift-forward-let sym `- concl duration)))
+
+(defn backward-interval-check [sym]
+  `(and (coll? ~sym) (= (first ~sym) (quote ~'seq-conj))
+        (let [cnt# (count ~sym)]
+          (and (odd? cnt#) (get-in ~sym [(dec cnt#) 1])))))
+
+(defn shift-backward-let
+  ([sym conclusion] (shift-backward-let sym nil conclusion nil))
+  ([sym op conclusion duration]
+   `(let [interval# ~(backward-interval-check sym)
+          ~@(if duration
+              `[:t-occurrence (~op :t-occurrence ~duration)]
+              [])
+          :t-occurrence (if interval# (+ :t-occurrence interval#)
+                                      :t-occurrence)]
+      (if interval#
+        (update ~conclusion :statement reduce-seq-conj)
+        ~conclusion))))
+
+(defmethod conclusion-transformation :shift-occurrence-backward
+  [args concl]
+  (let [duration (- duration)]
+    (m/match (mapv #(if (and (coll? %) (= 'quote (first %)))
+                     (second %) %) (rest args))
+      [(:or '=|> '==>)] concl
+      ['pred-impl] `(let [:t-occurrence (+ :t-occurrence ~duration)] ~concl)
+      ['retro-impl] `(let [:t-occurrence (- :t-occurrence ~duration)] ~concl)
+      [sym (:or '=|> '==>)] (shift-backward-let sym concl)
+      [sym 'pred-impl] (shift-backward-let sym `+ concl duration)
+      [sym 'retro-impl] (shift-backward-let sym `- concl duration))))

src/nal/deriver/rules.clj

@@ -2,7 +2,7 @@
   (:require [clojure.string :as s]
             [clojure.set :refer [map-invert]]
             [nal.deriver
-             [key-path :refer [rule-path all-paths path-invariants]]
+             [key-path :refer [rule-path all-paths path-invariants path]]
              [utils :refer [walk]]
              [list-expansion :refer [contains-list? generate-all-lists]]
              [premises-swapping :refer [allow-swapping? swap]]
@@ -81,7 +81,7 @@
   of rules that matches [[--> [- :any :any] :any] :and [--> [:any :any]]] path."
   [ac [k {:keys [all starts-with]}]]
   (let [rules (mapcat :rules (vals (select-keys ac all)))]
-    (-> ac
+    ac #_(-> ac
         (update-in [k :rules] concat rules)
         (update-in [k :rules] set))))
 
@@ -92,7 +92,7 @@
   (-> ac
       (update-in [full-path :rules] conj rule)
       (assoc-in [full-path :pattern] [p1 p2])
-      (assoc-in [full-path :all] (all-paths p1 p2))
+      (assoc-in [full-path :all] (all-paths (path p1) (path p2)))
       (assoc-in [full-path :starts-with] (set (path-invariants p1)))
       (assoc-in [full-path :end-with] (set (path-invariants p2)))))
 

src/nal/deriver/substitution.clj

@@ -3,20 +3,20 @@
             [clojure.core.unify :as u]
             [clojure.string :as s]))
 
-(def vars-map {"$" 'ind-var "#" 'dep-var})
-
 (defn replace-vars
   "Defn replaces var-elements from statemts by placeholders for unification."
   [var-type statement]
   (walk statement
-    (and (coll? el) (= var-type (first el)))
-    (->> el second (str "?") symbol)))
+    (and (coll? :el) (= var-type (first :el)))
+    (->> :el second (str "?") symbol)))
 
 (defn unification-map
   "Returns map of inified elements from both collections."
   [var-symbol p2 p3]
-  (let [var-type (vars-map var-symbol)]
-    (u/unify (replace-vars var-type p2) p3)))
+  (let [var-type (if (= var-symbol "$")
+                   'ind-var
+                   'dep-var)]
+    ((u/make-occurs-unify-fn #(and (coll? %) (= var-type (first %)))) p2 p3)))
 
 (def munification-map (memoize unification-map))
 
@@ -35,7 +35,5 @@
   "Unifies p2 and p3, then replaces elements from the unification map
   inside the conclusion."
   [var-symbol p2 p3 conclusion]
-  (let [var-type (vars-map var-symbol)
-        u-map (munification-map var-symbol p2 p3)
-        u-map (replace-placeholders var-type u-map)]
+  (let [u-map (munification-map var-symbol p2 p3)]
     (walk conclusion (u-map el) (u-map el))))

src/nal/deriver/utils.clj

@@ -11,7 +11,7 @@
   "Macro that helps to replace elements during walk. The first argument
   is collection, rest of the arguments are cond-like
   expressions. Default result of cond is element itself.
-  el is reserved name for current element of collection."
+  el (optionally :el) is reserved name for current element of collection."
   [coll & conditions]
   (let [el (gensym)
         replace-el (fn [coll]

src/nal/rules.clj

@@ -261,10 +261,10 @@
 
   ; conditional syllogism
   ; If after M P usually happens and M happens it means P is expected to happen
-  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
-  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward :unused ==>))]
-  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward :unused <=>))]
-  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
+  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward ==>))]
+  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward ==>))]
+  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward <=>))]
+  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward ==>))]
 
   ; conjunction decompose
   #R[(&& :list/A) Ai |- Ai :pre (:contains? (:list/A) Ai) :post (:t/structural-deduction :d/structural-strong)]
@@ -371,11 +371,11 @@
 
 
   ; independent variable elimination
-  #R[B (A ==> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused ==>))]
-  #R[B (C ==> A) |- C :post (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused ==>))]
+  #R[B (A ==> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward ==>))]
+  #R[B (C ==> A) |- C :post (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward C ==>))]
 
-  #R[B (A <=> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused <=>))]
-  #R[B (C <=> A) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused <=>))]
+  #R[B (A <=> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward <=>))]
+  #R[B (C <=> A) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward <=>))]
 
   ; second level variable handling rules
   ; second level variable elimination (termlink level2 growth needed in order for these rules to work)
@@ -390,7 +390,7 @@
 
   ; NAL7 specific inference
   ; Reasoning about temporal statements. those are using the ==> relation because relation in time is a relation of the truth between statements.
-#R[X ((&/ K (:interval I)) ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))]
+  #R[X ((&/ K (:interval I)) ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))]
   #_#R[X (XI ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" XI (&/ X :interval)) (:shift-occurrence-forward XI ==>))]
   #_#R[X (BI ==> Y) |- BI :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" Y X) (:shift-occurrence-backward BI ==>))]