we rewrite the paramodulation code!

[helm.git] / helm / software / components / ng_paramodulation / index.ml

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
new file mode 100644 (file)
index 0000000..123c516
--- /dev/null
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -0,0 +1,78 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+module type Comparable =
+  sig
+    type t
+    val is_eq : t -> t -> bool
+  end
+
+module C : Comparable =
+  struct 
+    type t = NCic.term
+    let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
+  end
+
+  (*
+module C : Comparable =
+  struct 
+    type t = Cic.term
+    let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
+  end
+*)
+
+open Discrimination_tree
+
+module ClauseOT : Set.OrderedType 
+                with type t = Terms.direction * C.t Terms.unit_clause = 
+ struct 
+  type t = Terms.direction * C.t Terms.unit_clause
+  let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) = 
+          Pervasives.compare (d1,id1) (d2,id2)
+ end
+
+module ClauseSet = Set.Make(ClauseOT)
+
+module FotermIndexable : Indexable
+with type input = C.t Terms.foterm and 
+     type constant_name = C.t = struct
+
+type input = C.t Terms.foterm
+type constant_name = C.t
+
+let path_string_of =
+  let rec aux arity = function
+    | Terms.Leaf a -> [Constant (a, arity)]
+    | Terms.Var i -> assert (arity = 0); [Variable]
+    | Terms.Node (Terms.Var _::_) -> assert false
+    | Terms.Node ([] | [ _ ] ) -> assert false
+    | Terms.Node (Terms.Node _::_) -> assert false
+    | Terms.Node (hd::tl) ->
+        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+  in 
+    aux 0
+;;
+
+let compare e1 e2 = 
+  match e1,e2 with 
+  | Constant (a1,ar1), Constant (a2,ar2) ->
+      if C.is_eq a1 a2 then Pervasives.compare ar1 ar2
+      else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *)
+  | _ -> Pervasives.compare e1 e2
+;;
+
+let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
+
+end
+
+module DiscriminationTree = Make(FotermIndexable)(ClauseSet)