From 3926a91fb2136a70755e16cfba865c28c874dbfb Mon Sep 17 00:00:00 2001
From: Roman Volosovskyi <rasom@ukr.net>
Date: Thu, 10 Mar 2016 18:15:45 +0200
Subject: [PATCH] :measure-time

---
 src/nal/core.clj                  |  1 +
 src/nal/deriver/matching.clj      | 23 +++++++++++----------
 src/nal/deriver/preconditions.clj | 14 +++++++++++++
 src/nal/deriver/rules.clj         | 33 ++++++++++++++++---------------
 src/nal/rules.clj                 |  2 +-
 5 files changed, 46 insertions(+), 27 deletions(-)

diff --git a/src/nal/core.clj b/src/nal/core.clj
index 6ae41dc..863be38 100644
--- a/src/nal/core.clj
+++ b/src/nal/core.clj
@@ -15,6 +15,7 @@
 (comment
   :seq-interval-from-premises                               ;post
   :shift-occurrence-forward                                 ;pre
+  :shift-occurrence-backward                                 ;pre
   :measure-time                                             ;pre
   :concurrent
   :linkage-temporal)
diff --git a/src/nal/deriver/matching.clj b/src/nal/deriver/matching.clj
index 8d7bb94..adf812d 100644
--- a/src/nal/deriver/matching.clj
+++ b/src/nal/deriver/matching.clj
@@ -76,17 +76,20 @@
   [pattern rules task-type]
   (let [t1 (gensym) t2 (gensym)
         task (gensym) belief (gensym)
+        t-occurence (gensym) b-occurence (gensym)
         truth-kw (if (= :goal task-type) :desire :truth)]
-    `(fn [{p1# :statement ~t1 ~truth-kw :as ~task}
-          {p2# :statement ~t2 :truth :as ~belief}]
-       (match [p1# p2#] ~(quote-operators pattern)
-         ~(traverse {:t1        t1
-                     :t2        t2
-                     :task      task
-                     :belief    belief
-                     :task-type task-type}
-                    rules)
-         :else nil))))
+    (walk `(fn [{p1# :statement ~t1 ~truth-kw :t-occurence :occurence :as ~task}
+                {p2# :statement ~t2 :truth :b-occurence :occurence :as ~belief}]
+             (match [p1# p2#] ~(quote-operators pattern)
+               ~(traverse {:t1        t1
+                           :t2        t2
+                           :task      task
+                           :belief    belief
+                           :task-type task-type}
+                          rules)
+               :else nil))
+      (= :el :t-occurence) t-occurence
+      (= :el :b-occurence) b-occurence)))
 
 (defn find-and-replace-symbols
   "Replaces all terms in statemnt to placeholders that will be used in pattern
diff --git a/src/nal/deriver/preconditions.clj b/src/nal/deriver/preconditions.clj
index fe8bb11..9ac10e8 100644
--- a/src/nal/deriver/preconditions.clj
+++ b/src/nal/deriver/preconditions.clj
@@ -81,6 +81,12 @@
 (defmethod compound-precondition :not-set?
   [[_ arg]]
   [`(or (not (coll? ~arg)) (not (sets (first ~arg))))])
+
+(defmethod compound-precondition :measure-time
+  [_]
+  [`(not= :eternal :t-occurence)
+   `(not= :eternal :b-occurence)])
+
 ;-------------------------------------------------------------------------------
 (defmulti precondition-transformation (fn [arg1 _] (first arg1)))
 
@@ -113,6 +119,14 @@
   [[_ p1 p2 p3] conclusion]
   `(substitute ~p1 ~p2 ~p3 ~conclusion))
 
+(defmethod precondition-transformation :measure-time
+  [[_ arg] conclusion]
+  (let [mt (gensym)]
+    (walk `(let [k# 1 ~arg (- :t-occurence :b-occurence)]
+             ~(walk conclusion
+                (= :el arg) [:interval arg]))
+      (= :el arg) mt)))
+
 (defn check-precondition
   [conclusion precondition]
   (if (seq? precondition)
diff --git a/src/nal/deriver/rules.clj b/src/nal/deriver/rules.clj
index c02ce31..c272d6e 100644
--- a/src/nal/deriver/rules.clj
+++ b/src/nal/deriver/rules.clj
@@ -121,19 +121,20 @@
   "Define rules. Rules must be #R statements."
   ;TODO exception on duplication of the rule
   [name & rules]
-  `(let [rules# (rules->> (quote ~rules)
-                          contains-list? generate-all-lists
-                          contains-list? generate-all-lists
-                          identity rule
-                          order-for-all-same? generate-all-orders
-                          allow-swapping? swap
-                          allow-backward? expand-backward-rules)
-         judgement-rules# (check-duplication (filter judgement? rules#))
-         question-rules# (check-duplication (filter question? rules#))
-         goal-rules# (check-duplication (filter goal? rules#))]
-     (println "Q rules:" (count question-rules#))
-     (println "J rules:" (count judgement-rules#))
-     (println "G rules:" (count goal-rules#))
-     (def ~name {:judgement (rules-map judgement-rules# :judgement)
-                 :question  (rules-map question-rules# :question)
-                 :goal      (rules-map goal-rules# :goal)})))
+  `(time
+     (let [rules# (rules->> (quote ~rules)
+                            contains-list? generate-all-lists
+                            contains-list? generate-all-lists
+                            identity rule
+                            order-for-all-same? generate-all-orders
+                            allow-swapping? swap
+                            allow-backward? expand-backward-rules)
+           judgement-rules# (check-duplication (filter judgement? rules#))
+           question-rules# (check-duplication (filter question? rules#))
+           goal-rules# (check-duplication (filter goal? rules#))]
+       (println "Q rules:" (count question-rules#))
+       (println "J rules:" (count judgement-rules#))
+       (println "G rules:" (count goal-rules#))
+       (def ~name {:judgement (rules-map judgement-rules# :judgement)
+                   :question  (rules-map question-rules# :question)
+                   :goal      (rules-map goal-rules# :goal)}))))
diff --git a/src/nal/rules.clj b/src/nal/rules.clj
index 67cf739..cb2249c 100644
--- a/src/nal/rules.clj
+++ b/src/nal/rules.clj
@@ -326,7 +326,7 @@
                               (&& (#Y --> S) (#Y --> P)) :post (:t/intersection))
      :pre ((:!= S P)) ]
 
-  #_#R[(M --> S) (M --> P) |- (((&/ ($X --> P) I) =/> ($X --> S))  :post (:t/induction :linkage-temporal)
+  #R[(M --> S) (M --> P) |- (((&/ ($X --> P) I) =/> ($X --> S))  :post (:t/induction :linkage-temporal)
                               (($X --> S) =\> (&/ ($X --> P) I)) :post (:t/abduction :linkage-temporal)
                               ((&/ ($X --> P) I) </> ($X --> S)) :post (:t/comparison :linkage-temporal)
                               (&/ (#Y --> P) I (#Y --> S)) :post (:t/intersection :linkage-temporal))