1. New paramodulation function

[helm.git] / helm / software / components / ng_refiner / nDiscriminationTree.ml

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index d3a334a591db27453e13a2bd678a00ae63f83495..fff8b67699c6d5388dfa811995d30a686a5aff84 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -24,10 +24,22 @@
  *)
 
 (* $Id$ *)
-(*
-module NCicIndexable : Discrimination_tree.Indexable
+
+open Discrimination_tree
+
+module TermOT : Set.OrderedType with type t = NCic.term = struct 
+  type t = NCic.term 
+  let compare = Pervasives.compare 
+end
+
+module TermSet = Set.Make(TermOT)
+
+module NCicIndexable : Indexable
 with type input = NCic.term and type constant_name = NUri.uri = struct
 
+type input = NCic.term
+type constant_name = NUri.uri
+
 let ppelem = function
   | Constant (uri,arity) -> 
       "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
@@ -39,13 +51,15 @@ let ppelem = function
   | Dead -> "Dead"
 ;;
 
-let path_string_of =
-  let rec aux arity = function
+let path_string_of t =
+  let rec aux arity depth = function
     | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
     | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
     | NCic.Appl [] -> assert false
+    | NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
     | NCic.Appl (hd::tl) ->
-        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+       aux (List.length tl) depth hd @ 
+       List.flatten (List.map (aux 0 (depth+1)) tl)
     | NCic.Lambda _ | NCic.Prod _ -> [Variable]
         (* I think we should CicSubstitution.subst Implicit t *)
     | NCic.LetIn _ -> [Variable] (* z-reduce? *)
@@ -56,7 +70,7 @@ let path_string_of =
     | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
     | NCic.Match _ -> [Dead]
   in 
-    aux 0
+  aux 0 0 t
 ;;
 
 let compare e1 e2 =
@@ -71,6 +85,4 @@ let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
 end
 
-module DiscriminationTree = 
-  Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-  *)
+module DiscriminationTree = Make(NCicIndexable)(TermSet)