X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=bd64cfe5d5a036b2ad0e69e0356c52a2718384af;hb=e869500069d11aadd7bbe8afddcdd9044d0b56a7;hp=fb9b4c021335b08188a39257d109294957cf4ebd;hpb=40a37ee02e437c28828ee1d8249d43e847b0b0cd;p=helm.git

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index fb9b4c021..bd64cfe5d 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -25,22 +25,20 @@
 
 (* $Id$ *)
 
-type path_string_elem = 
-  | Constant of NUri.uri * int (* name, arity *)
-  | Bound of int * int (* rel, arity *)
-  | Variable (* arity is 0 *)
-  | Proposition (* arity is 0 *) 
-  | Datatype (* arity is 0 *) 
-  | Dead (* arity is 0 *) 
-;;  
-      
-let arity_of = function
-  | Constant (_,a) 
-  | Bound (_,a) -> a
-  | _ -> 0 
-;;
+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)
 
-type path = path_string_elem list;;
+module NCicIndexable : Indexable
+with type input = NCic.term and type constant_name = NUri.uri = struct
+
+type input = NCic.term
+type constant_name = NUri.uri
 
 let ppelem = function
   | Constant (uri,arity) -> 
@@ -53,7 +51,7 @@ let ppelem = function
   | Dead -> "Dead"
 ;;
 
-let path_string_of_term_with_jl =
+let path_string_of =
   let rec aux arity = function
     | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
     | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
@@ -73,7 +71,7 @@ let path_string_of_term_with_jl =
     aux 0
 ;;
 
-let compare_elem e1 e2 =
+let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NUri.compare u1 u2 in
@@ -83,104 +81,6 @@ let compare_elem e1 e2 =
 
 let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
-module DiscriminationTreeIndexing =  
-  functor (A:Set.S) -> 
-    struct
-
-      module OrderedPathStringElement = struct
-        type t = path_string_elem
-        let compare = compare_elem
-      end
-
-      module PSMap = Map.Make(OrderedPathStringElement);;
-
-      type key = PSMap.key
-
-      module DiscriminationTree = Trie.Make(PSMap);;
-
-      type t = A.t DiscriminationTree.t
-
-      let empty = DiscriminationTree.empty;;
-
-      let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
-
-      let index tree term info =
-        let ps = path_string_of_term_with_jl term in
-        let ps_set =
-          try DiscriminationTree.find ps tree with Not_found -> A.empty 
-        in
-        DiscriminationTree.add ps (A.add info ps_set) tree
-      ;;
-
-      let remove_index tree term info =
-        let ps = path_string_of_term_with_jl term in
-        try
-          let ps_set = A.remove info (DiscriminationTree.find ps tree) in
-          if A.is_empty ps_set then DiscriminationTree.remove ps tree
-          else DiscriminationTree.add ps ps_set tree
-        with Not_found -> tree
-      ;;
-
-      let in_index tree term test =
-        let ps = path_string_of_term_with_jl term in
-        try
-          let ps_set = DiscriminationTree.find ps tree in
-          A.exists test ps_set
-        with Not_found -> false
-      ;;
-
-      (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is 
-         (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
-         skip all its progeny, thus you want to reach t.
-      
-         You need to skip as many elements as the sum of all arieties contained
-          in the progeny of f.
-      
-         The input ariety is the one of f while the path is x.g....t  
-         Should be the equivalent of after_t in the literature (handbook A.R.)
-       *)
-      let rec skip arity path =
-        if arity = 0 then path else match path with 
-        | [] -> assert false 
-        | m::tl -> skip (arity-1+arity_of m) tl
-      ;;
-
-      (* the equivalent of skip, but on the index, thus the list of trees
-         that are rooted just after the term represented by the tree root
-         are returned (we are skipping the root) *)
-      let skip_root = function DiscriminationTree.Node (_, map) ->
-        let rec get n = function DiscriminationTree.Node (_, m) as tree ->
-           if n = 0 then [tree] else 
-           PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
-        in
-          PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
-      ;;
-
-      let retrieve unif tree term =
-        let path = path_string_of_term_with_jl term in
-        let rec retrieve path tree =
-          match tree, path with
-          | DiscriminationTree.Node (Some s, _), [] -> s
-          | DiscriminationTree.Node (None, _), [] -> A.empty 
-          | DiscriminationTree.Node _, Variable::path when unif ->
-              List.fold_left A.union A.empty
-                (List.map (retrieve path) (skip_root tree))
-          | DiscriminationTree.Node (_, map), node::path ->
-              A.union
-                 (if not unif && node = Variable then A.empty else
-                  try retrieve path (PSMap.find node map)
-                  with Not_found -> A.empty)
-                 (try
-                    match PSMap.find Variable map,skip (arity_of node) path with
-                    | DiscriminationTree.Node (Some s, _), [] -> s
-                    | n, path -> retrieve path n
-                  with Not_found -> A.empty)
-       in
-        retrieve path tree
-      ;;
-
-      let retrieve_generalizations tree term = retrieve false tree term;;
-      let retrieve_unifiables tree term = retrieve true tree term;;
-  end
-;;
+end
 
+module DiscriminationTree = Make(NCicIndexable)(TermSet)