From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 7 Jun 2005 06:44:39 +0000 (+0000)
Subject: My two pennies.
X-Git-Tag: PRE_INDEX_1~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5462948747cca234512fd998678cb9315785d68c;p=helm.git

My two pennies.
---

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
new file mode 100644
index 000000000..8ed8f49a1
--- /dev/null
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -0,0 +1,40 @@
+(* type naif_indexing =
+    (Cic.term * ((bool * Inference.equality) list)) list 
+;; *)
+
+type pos = Left | Right 
+;;
+
+let head_of_term =
+  function 
+    | Cic.Appl hd::tl -> hd
+    | t -> t
+;;
+
+let index table eq =
+  let (_,(_,l,r,ordering),_,_) = eq in
+  let hl = head_of_term l in
+  let hr = head_of_term r in
+  let index x pos = 
+    let x_entry = 
+      try Hashtbl.find table x
+      with Not_found -> [] in
+      Hashtbl.replace table x (pos,eq)::x_entry in
+  (match ordering with
+    | Utils.Gt -> 
+	index hl Left
+    | Utils.Lt -> 
+	index hr Right
+    | _ -> index hl Left;
+	index hr Right);
+  table
+;;
+
+let demodulate_term env table cmp term =
+  let hd_term = head_of_term term in
+  let candidates = Hashtbl.find table hd_term in
+  
+    
+    
+      
+