X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=fff8b67699c6d5388dfa811995d30a686a5aff84;hb=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;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..fff8b6769 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,13 +51,15 @@ let ppelem = function | Dead -> "Dead" ;; -let path_string_of_term_with_jl = - 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? *) @@ -70,10 +70,10 @@ let path_string_of_term_with_jl = | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)] | NCic.Match _ -> [Dead] in - aux 0 + aux 0 0 t ;; -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 +83,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)