From 974970b91996a4caae7af96b85acde33254cdfc9 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 May 2012 22:24:08 +0000
Subject: [PATCH] Orientation of equalities is now displayed.

---
 .../grafite_engine/grafiteEngine.ml           | 34 +++++++++++++++----
 matita/components/ng_paramodulation/pp.ml     | 14 ++++----
 matita/components/ng_paramodulation/pp.mli    |  2 ++
 3 files changed, 37 insertions(+), 13 deletions(-)

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b6f5b14e6..bd0fd6cea 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -275,25 +275,47 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
    NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
-let index_eq uri status =
+(*
+module EmptyC = 
+  struct
+    let metasenv = []
+    let subst = []
+    let context = []
+  end
+*)
+
+let index_eq print uri (status:#NCic.status) =
   let eq_status = status#eq_cache in
-  let eq_status = NCicParamod.index_obj status eq_status uri in
-    status#set_eq_cache eq_status
+  let eq_status,clause = NCicParamod.index_obj status eq_status uri in
+  if print then
+   ((*let module NCicBlob =
+    struct
+     include NCicBlob.NCicBlob(EmptyC)
+     let pp t = status#ppterm ~metasenv:[] ~subst:[] ~context:[] t
+    end in
+   let module Pp = Pp.Pp(NCicBlob) in*)
+   (match clause with
+     | Some (*clause*) (_,Terms.Equation (_,_,_,o),_,_) ->
+        HLog.debug ("Indexed with orientation: " ^ Pp.string_of_comparison o);
+        (*HLog.debug ("Indexed as:" ^ Pp.pp_unit_clause clause)*)
+     | _ -> HLog.debug "Not indexed (i.e. pruned)")) ;
+  status#set_eq_cache eq_status
 ;;
 
 let record_index_eq =
  let basic_index_eq uri
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
    ~alias_only status
-   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
-     status
+   = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status 
+     else
+      status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
 
 let index_eq_for_auto status uri =
  if NnAuto.is_a_fact_obj status uri then
-   let newstatus = index_eq uri status in
+   let newstatus = index_eq true uri status in
      if newstatus#eq_cache == status#eq_cache then status 
      else
        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
diff --git a/matita/components/ng_paramodulation/pp.ml b/matita/components/ng_paramodulation/pp.ml
index ddf5726c4..64af9ab17 100644
--- a/matita/components/ng_paramodulation/pp.ml
+++ b/matita/components/ng_paramodulation/pp.ml
@@ -11,6 +11,13 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+let string_of_comparison = function
+  | Terms.Lt -> "=<="
+  | Terms.Gt -> "=>="
+  | Terms.Eq -> "==="
+  | Terms.Incomparable -> "=?="
+  | Terms.Invertible -> "=<->="
+
 module Pp (B : Terms.Blob) = struct
 
 (* Main pretty printing functions *)
@@ -80,13 +87,6 @@ let pp_proof bag ~formatter:f p =
     Format.fprintf f "@]"
 ;;
 
-let string_of_comparison = function
-  | Terms.Lt -> "=<="
-  | Terms.Gt -> "=>="
-  | Terms.Eq -> "==="
-  | Terms.Incomparable -> "=?="
-  | Terms.Invertible -> "=<->="
-
 let pp_unit_clause ~formatter:f c =
   let (id, l, vars, proof) = c in
     Format.fprintf f "Id : %3d, " id ;
diff --git a/matita/components/ng_paramodulation/pp.mli b/matita/components/ng_paramodulation/pp.mli
index 767c87e0b..7ed129275 100644
--- a/matita/components/ng_paramodulation/pp.mli
+++ b/matita/components/ng_paramodulation/pp.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val string_of_comparison: Terms.comparison -> string
+
 module Pp (B : Terms.Blob) : 
   sig
 
-- 
2.39.2