X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2Fdiscrimination_tree.ml;h=546f4a34fce9f01b2fcca86ff0148af5ee6ee045;hb=a957099550619f87a58be467b9b11f2ad6501378;hp=b2906e1c9c741d774b0492790a62861f9a5aae82;hpb=218a5af368cb7ea58c59cad2e7c8ef1f733792c2;p=helm.git

diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml
index b2906e1c9..546f4a34f 100644
--- a/components/cic/discrimination_tree.ml
+++ b/components/cic/discrimination_tree.ml
@@ -30,8 +30,8 @@ module DiscriminationTreeIndexing =
     struct
 
       type path_string_elem = 
-        | Function | Constant of UriManager.uri 
-        | Bound of int | Variable | Proposition | Datatype ;;
+        | Constant of UriManager.uri 
+        | Bound of int | Variable | Proposition | Datatype | Dead;;
       type path_string = path_string_elem list;;
 
 
@@ -39,28 +39,34 @@ module DiscriminationTreeIndexing =
        * "functions" *)
       
       let ppelem = function
-        | Function -> "Fun"
         | Constant uri -> UriManager.name_of_uri uri
         | Bound i -> string_of_int i
         | Variable -> "?"
         | Proposition -> "Prop"
         | Datatype -> "Type"
+        | Dead -> "DEAD"
       ;;
       let pppath l = String.concat "::" (List.map ppelem l) ;;
       let elem_of_cic = function
-        | Cic.Meta _ -> Variable
-        | Cic.Lambda _ -> Function
+        | Cic.Meta _ | Cic.Implicit _ -> Variable
         | Cic.Rel i -> Bound i
         | Cic.Sort (Cic.Prop) -> Proposition
         | Cic.Sort _ -> Datatype
-        | term ->
-            try Constant (CicUtil.uri_of_term term)
-            with Invalid_argument _ -> Variable (* HACK! *)
+        | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
+            (try Constant (CicUtil.uri_of_term t)
+            with Invalid_argument _ -> assert false)
+        | Cic.Appl _ -> 
+            assert false (* should not happen *)
+        | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
+        | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> 
+            HLog.debug "FIXME: the trie receives an invalid term";
+            Dead
+            (* assert false universe.ml removes these *)
       ;;
       let path_string_of_term arities =
 	let set_arity arities k n = 
 	  (assert (k<>Variable || n=0);
-	  (k,n)::(List.remove_assoc k arities))
+          if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
         in
         let rec aux arities = function
           | Cic.Appl ((hd::tl) as l) ->