From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 17 Sep 2008 10:22:57 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4777
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=348e5e6b9765c760159107a0fdb102c3eff42cd9;p=helm.git

...
---

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index 1089474e4..c4fd43ad2 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -11,65 +11,87 @@
 
 (* $Id$ *)
 
+type path_string_elem = 
+  | Constant of NUri.uri 
+  | Bound of int 
+  | Variable 
+  | Proposition 
+  | Datatype 
+  | Dead of NCic.term 
+;;
+
+type path_string = path_string_elem list;;
+
+let ppelem = function
+  | Constant uri -> NUri.name_of_uri uri
+  | Bound i -> string_of_int i
+  | Variable -> "?"
+  | Proposition -> "Prop"
+  | Datatype -> "Type"
+  | Dead t -> 
+      "DEAD("^NCicPp.ppterm ~context:[] ~subst:[] ~metasenv:[] t^")"
+;;
+
+let pp_path_string l = String.concat "::" (List.map ppelem l) ;;
+
+let elem_of_cic = function
+  | NCic.Meta _ | NCic.Implicit _ -> Variable
+  | NCic.Rel i -> Bound i
+  | NCic.Sort (NCic.Prop) -> Proposition
+  | NCic.Sort _ -> Datatype
+  | NCic.Const (NReference.Ref (u,_)) -> Constant u
+  | NCic.Appl _ -> assert false (* should not happen *)
+  | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ as t -> 
+      prerr_endline 
+        "FIXME: the discrimination tree receives an invalid term";
+      Dead t
+;;
+
+let path_string_of_term arities =
+  let set_arity arities k n = 
+    (assert (k<>Variable || n=0);
+    match k with 
+    | Dead _ -> arities 
+    | _ -> 
+       (* here we override, but partial instantiation may trick us *)
+       (k,n)::(List.remove_assoc k arities))
+  in
+  let rec aux arities = function
+    | NCic.Appl ((hd::tl) as l) ->
+        let arities = 
+          set_arity arities (elem_of_cic hd) (List.length tl) 
+        in
+        List.fold_left 
+  	(fun (arities,path) t -> 
+  	   let arities,tpath = aux arities t in
+  	     arities,path@tpath)
+  	(arities,[]) l
+    | t -> arities, [elem_of_cic t]
+  in 
+    aux arities
+;;
+
+let compare_elem e1 e2 =
+  match e1,e2 with
+  | Constant u1,Constant u2 -> NUri.compare u1 u2
+  | e1,e2 -> Pervasives.compare e1 e2
+;;
+
+let head_of_term = function
+  | NCic.Appl (hd::tl) -> hd
+  | term -> term
+;;
+
+let rec skip_prods = function
+  | NCic.Prod (_,_,t) -> skip_prods t
+  | term -> term
+;;
+
+
 module DiscriminationTreeIndexing =  
   functor (A:Set.S) -> 
     struct
 
-      type path_string_elem = 
-        | Constant of NUri.uri 
-        | Bound of int | Variable | Proposition | Datatype | Dead;;
-      type path_string = path_string_elem list;;
-
-
-      (* needed by the retrieve_* functions, to know the arities of the
-       * "functions" *)
-      
-      let ppelem = function
-        | Constant uri -> NUri.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
-        | NCic.Meta _ | NCic.Implicit _ -> Variable
-        | NCic.Rel i -> Bound i
-        | NCic.Sort (NCic.Prop) -> Proposition
-        | NCic.Sort _ -> Datatype
-        | NCic.Const (NReference.Ref (u,_)) -> Constant u
-        | NCic.Appl _ -> 
-            assert false (* should not happen *)
-        | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ -> 
-            prerr_endline "FIXME: the discrimination tree 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);
-          if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
-        in
-        let rec aux arities = function
-          | NCic.Appl ((hd::tl) as l) ->
-              let arities = 
-		set_arity arities (elem_of_cic hd) (List.length tl) in
-	      List.fold_left 
-		(fun (arities,path) t -> 
-		   let arities,tpath = aux arities t in
-		     arities,path@tpath)
-		(arities,[]) l
-          | t -> arities, [elem_of_cic t]
-        in 
-          aux arities
-      ;;
-      let compare_elem e1 e2 =
-        match e1,e2 with
-        | Constant u1,Constant u2 -> assert false (*NUri.compare u1 u2*)
-        | e1,e2 -> Pervasives.compare e1 e2
-      ;;
-
       module OrderedPathStringElement = struct
         type t = path_string_elem
         let compare = compare_elem
@@ -82,10 +104,11 @@ module DiscriminationTreeIndexing =
       module DiscriminationTree = Trie.Make(PSMap);;
 
       type t = A.t DiscriminationTree.t * (path_string_elem*int) list
+
       let empty = DiscriminationTree.empty, [] ;;
 
       let iter (dt, _ ) f =
-        DiscriminationTree.iter (fun _ x -> f x) dt
+        DiscriminationTree.iter (fun y x -> f y  x) dt
       ;;
 
       let index (tree,arity) term info =
@@ -118,16 +141,6 @@ module DiscriminationTreeIndexing =
           false
       ;;
 
-      let head_of_term = function
-        | NCic.Appl (hd::tl) -> hd
-        | term -> term
-      ;;
-
-      let rec skip_prods = function
-        | NCic.Prod (_,_,t) -> skip_prods t
-        | term -> term
-      ;;
-
       let rec subterm_at_pos pos term =
         match pos with
           | [] -> term
diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
index a146c4b73..04f8c6907 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -12,12 +12,16 @@
 
 (* $Id$ *)
 
+type path_string
+
+val pp_path_string : path_string -> string
+
 module DiscriminationTreeIndexing :
   functor (A : Set.S) ->
     sig
 
       type t 
-      val iter : t -> (A.t -> unit) -> unit
+      val iter : t -> (path_string -> A.t -> unit) -> unit
 
       val empty : t
       val index : t -> NCic.term -> A.elt -> t