New demodulation tactics (mostly for debugging purposes).

[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 bd64cfe5d5a036b2ad0e69e0356c52a2718384af..2bae037c1b10438068ca7e1b7ade09144a20e953 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -35,14 +35,15 @@ end
 module TermSet = Set.Make(TermOT)
 
 module NCicIndexable : Indexable
-with type input = NCic.term and type constant_name = NUri.uri = struct
+with type input = NCic.term 
+and type constant_name = NReference.reference = struct
 
 type input = NCic.term
-type constant_name = NUri.uri
+type constant_name = NReference.reference
 
 let ppelem = function
-  | Constant (uri,arity) -> 
-      "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
+  | Constant (ref,arity) -> 
+      "("^NReference.string_of_reference ref ^ "," ^ string_of_int arity^")"
   | Bound (i,arity) -> 
       "("^string_of_int i ^ "," ^ string_of_int arity^")"
   | Variable -> "?"
@@ -51,13 +52,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? *)
@@ -65,16 +68,16 @@ let path_string_of =
     | NCic.Rel i -> [Bound (i, arity)]
     | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
     | NCic.Sort _ -> assert (arity=0); [Datatype]
-    | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+    | NCic.Const (u) -> [Constant (u, arity)]
     | NCic.Match _ -> [Dead]
   in 
-    aux 0
+  aux 0 0 t
 ;;
 
 let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
-       let x = NUri.compare u1 u2 in
+       let x = NReference.compare u1 u2 in
        if x = 0 then Pervasives.compare a1 a2 else x
   | e1,e2 -> Pervasives.compare e1 e2
 ;;