:shift-occurrence-backward/:shift-occurrence-forward

src/nal/deriver.clj

@@ -4,23 +4,9 @@
     [nal.deriver.key-path :refer [mall-paths all-paths path mpath-invariants]]
     [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)))))
-(def mchild? (memoize child?))
-
-(defn remove-children [paths]
-  (reduce #(remove (partial mchild? %2) %1) paths paths))
-
 (defn get-matcher [rules p1 p2]
   (let [matchers (->> (mall-paths p1 p2)
                       (filter rules)
-                      remove-children
                       (select-keys rules)
                       (map (fn [el] (:matcher (second el)))))]
     (case (count matchers)

src/nal/deriver/key_path.clj

@@ -35,6 +35,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/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

@@ -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,36 +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)
-      (and (= :shift-occurrence-forward type) ('#{=|> ==>} arg2))
-      `(let [:t-occurrence (+ :t-occurrence ~arg1)]
-         ~conclusion)
-      (= :shift-occurrence-forward type)
-      `(let [:t-occurrence (+ (~(if (= arg2 'pred-impl) `+ `-)
-                                :t-occurrence ~dur)
-                              ~arg1)]
-         ~conclusion)
-      (and (= :shift-occurrence-backward type) ('#{=|> ==>} arg2))
-      `(let [:t-occurrence (if (and (coll? ~arg1) (= 'seq-conj (first ~arg1)))
-                             (+ :t-occurrence (last ~arg1))
-                             :t-occurrence)]
-         ~conclusion)
-      (= :shift-occurrence-backward type)
-      `(let [:t-occurrence (if (and (coll? ~arg1) (= 'seq-conj (first ~arg1)))
-                             (+ (~(if (= arg2 'pred-impl) `+ `-)
-                                  :t-occurrence ~dur)
-                                ~arg1)
-                             (~(if (= arg2 'pred-impl) `+ `-)
-                               :t-occurrence ~dur))]
-         ~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/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)

test/nal/test/core.clj

@@ -22,10 +22,31 @@
        :truth     [1 0.9]
        :occurrence 0}]
 
-    '({:statement [--> a1 [ext-image m _ a2 a3]]
-       :truth     [1 0.9]
-       :task-type :judgement
-       :occurrence 1})
+    '({:occurrence 1
+       :statement  [&| a1 [--> [* a1 a2 a3] m]]
+       :task-type  :judgement
+       :truth      [1.0
+                    0.81]}
+       {:occurrence 1
+        :statement  [--> a1 [ext-image m _ a2 a3]]
+        :task-type  :judgement
+        :truth      [1
+                     0.9]}
+       {:occurrence 1
+        :statement  [<|> a1 [--> [* a1 a2 a3] m]]
+        :task-type  :judgement
+        :truth      [1.0
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> [--> [* a1 a2 a3] m] a1]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> a1 [--> [* a1 a2 a3] m]]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]})
     '[{:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
        :task-type :judgement
@@ -60,9 +81,28 @@
        :truth     [1 0.9]
        :occurrence 0}]
 
-    '({:statement a1 :truth [1 0.44751381215469616]
-       :task-type :judgement
-       :occurrence 1})
+    '({:occurrence 1
+       :statement  [&| a1 [conj a1 a2 a3]]
+       :task-type  :judgement
+       :truth      [1.0 0.81]}
+       {:occurrence 1
+        :statement  [<|> a1 [conj a1 a2 a3]]
+        :task-type  :judgement
+        :truth      [1.0 0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> [conj a1 a2 a3] a1]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> a1 [conj a1 a2 a3]]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  a1
+        :task-type  :judgement
+        :truth      [1 0.44751381215469616]})
     '[{:statement [conj a1 a2 a3]
        :truth     [1 0.9]
        :task-type :judgement