From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Oct 2009 21:38:41 +0000 (+0000)
Subject: the trie indexes terms up to 10 nested applications and skips applications with more... 
X-Git-Tag: make_still_working~3261
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e0e2b06cfc3fb3116e1fce632d9897fdbac9895;p=helm.git

the trie indexes terms up to 10 nested applications and skips applications with more then 50 arguments
---

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index bd64cfe5d..fff8b6769 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -51,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? *)
@@ -68,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 =