My two pennies.

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
new file mode 100644 (file)
index 0000000..8ed8f49
--- /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
+  
+    
+    
+      
+