Experimental support for Russell (coercions moving inside lambda & pattern

[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..50c3bd208d2b1c4465b0da542a9ecdbe8a72f803 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -24,13 +24,36 @@
  *)
 
 (* $Id$ *)
-(*
-module NCicIndexable : Discrimination_tree.Indexable
-with type input = NCic.term and type constant_name = NUri.uri = struct
+
+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 TermListOT : Set.OrderedType with type t = NCic.term list =
+ struct
+   type t = NCic.term list
+   let compare = Pervasives.compare
+ end
+
+module TermListSet : Set.S with type elt = NCic.term list =
+ Set.Make(TermListOT)
+
+
+module NCicIndexable : Indexable
+with type input = NCic.term 
+and type constant_name = NReference.reference = struct
+
+type input = NCic.term
+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 -> "?"
@@ -39,13 +62,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? *)
@@ -53,16 +78,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
 ;;
@@ -71,6 +96,4 @@ let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
 end
 
-module DiscriminationTree = 
-  Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-  *)
+module DiscriminationTree = Make(NCicIndexable)(TermSet)