From: Enrico Tassi Date: Fri, 19 Sep 2008 08:11:53 +0000 (+0000) Subject: Revised discrimination tree implementation: X-Git-Tag: make_still_working~4762 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=059b7545a49e50bf6204997027f7bda375af819c;p=helm.git Revised discrimination tree implementation: - code size reduced, looking for unifiables or generalizations is almost the same and do not internally work with the query term, but its path representation that is now decorated with arieties to recover the tree structure when needed (jump to the sibling...) - works with partial instantiation (no more global ariety list, but local to application heads). Stupid example: query: fold plus [] 0 = 0 ==?== tree: fold ? [] 0 = 0 since the 2nd arg is ? we skip the query subterm rooted in plus, but if plus is considered of ariety 2, we fail unifiing the following terms (we skip [] and 0 reaching the second 0 that is unified with [] and fails). - term -> path string function fixed to clen up the input term, no more "FIXME: the trie received invalid term". Here there is room for improvements especially on beta redexes and terms beginning with an abstraction, but we need the substitutions operation, we should move the file elsewhere - Big change: - if the query term is a meta, then the whole content of the tree is returned - in paramodulation this is dangerous, thus we added a small check in the paramodulation code (eq_indexing) instead of making the discrimination tree behave in a nasty way - the new implementation returns the same set of candidates on all test TPTP/Veloci and library/ (except for the aforementioned corner case). --- diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index f5d614630..cb3a7d745 100644 --- a/helm/software/components/cic/discrimination_tree.ml +++ b/helm/software/components/cic/discrimination_tree.ml @@ -25,67 +25,69 @@ (* $Id$ *) -module DiscriminationTreeIndexing = - functor (A:Set.S) -> - struct +type path_string_elem = + | Constant of UriManager.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 +;; - type path_string_elem = - | Constant of UriManager.uri - | Bound of int | Variable | Proposition | Datatype | Dead;; - type path_string = path_string_elem list;; +type path = path_string_elem list;; + +let ppelem = function + | Constant (uri,arity) -> + "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")" + | Bound (i,arity) -> + "("^string_of_int i ^ "," ^ string_of_int arity^")" + | Variable -> "?" + | Proposition -> "Prop" + | Datatype -> "Type" + | Dead -> "Dead" +;; +let path_string_of_term_with_jl = + let rec aux arity = function + | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable] + | Cic.Appl (Cic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *) + | Cic.Appl [] -> assert false + | Cic.Appl (hd::tl) -> + aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) + | Cic.Cast (t,_) -> aux arity t + | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable] + (* I think we should CicSubstitution.subst Implicit t *) + | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *) + | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable] + | Cic.Rel i -> [Bound (i, arity)] + | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition] + | Cic.Sort _ -> assert (arity=0); [Datatype] + | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t -> + [Constant (CicUtil.uri_of_term t, arity)] + | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead] + in + aux 0 +;; - (* needed by the retrieve_* functions, to know the arities of the - * "functions" *) - - let ppelem = function - | 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 _ | Cic.Implicit _ -> Variable - | Cic.Rel i -> Bound i - | Cic.Sort (Cic.Prop) -> Proposition - | Cic.Sort _ -> Datatype - | 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); - 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) -> - 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 -> UriManager.compare u1 u2 - | e1,e2 -> Pervasives.compare e1 e2 - ;; +let compare_elem e1 e2 = + match e1,e2 with + | Constant (u1,a1),Constant (u2,a2) -> + let x = UriManager.compare u1 u2 in + if x = 0 then Pervasives.compare a1 a2 else x + | e1,e2 -> Pervasives.compare 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 @@ -98,212 +100,89 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; - type t = A.t DiscriminationTree.t * (path_string_elem*int) list - let empty = DiscriminationTree.empty, [] ;; + type t = A.t DiscriminationTree.t - let iter (dt, _ ) f = - DiscriminationTree.iter (fun _ x -> f x) dt - ;; + let empty = DiscriminationTree.empty;; + + let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;; - let index (tree,arity) term info = - let arity,ps = path_string_of_term arity term in + 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 - let tree = DiscriminationTree.add ps (A.add info ps_set) tree in - tree,arity + try DiscriminationTree.find ps tree with Not_found -> A.empty + in + DiscriminationTree.add ps (A.add info ps_set) tree ;; - let remove_index (tree,arity) term info = - let arity,ps = path_string_of_term arity term in + 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,arity - else - DiscriminationTree.add ps ps_set tree,arity - with Not_found -> - tree,arity + 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,arity) term test = - let arity,ps = path_string_of_term arity term in + 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 - ;; - - let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | term -> term - ;; - - let rec skip_prods = function - | Cic.Prod (_,_,t) -> skip_prods t - | term -> term - ;; - - let rec subterm_at_pos pos term = - match pos with - | [] -> term - | index::pos -> - match term with - | Cic.Appl l -> - (try subterm_at_pos pos (List.nth l index) - with Failure _ -> raise Not_found) - | _ -> raise Not_found + with Not_found -> false ;; - - let rec after_t pos term = - let pos' = - match pos with - | [] -> raise Not_found - | pos -> - List.fold_right - (fun i r -> if r = [] then [i+1] else i::r) pos [] - in - try - ignore(subterm_at_pos pos' term ); pos' - with Not_found -> - let pos, _ = - List.fold_right - (fun i (r, b) -> if b then (i::r, true) else (r, true)) - pos ([], false) - in - after_t pos term + (* 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 ;; - - let next_t pos term = - let t = subterm_at_pos pos term in - try - let _ = subterm_at_pos [1] t in - pos @ [1] - with Not_found -> - match pos with - | [] -> [1] - | pos -> after_t pos term - ;; - - let retrieve_generalizations (tree,arity) term = - let term = skip_prods term in - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let res = - let hd_term = - elem_of_cic (head_of_term (subterm_at_pos pos term)) - in - if hd_term = Variable then A.empty else - try - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - let newpos = - try next_t pos term - with Not_found -> [] - in - retrieve n term newpos - with Not_found -> - A.empty - in - try - let n = PSMap.find Variable map in - let newpos = try after_t pos term with Not_found -> [-1] in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> A.union s res - | _ -> res - else - A.union res (retrieve n term newpos) - with Not_found -> - res + (* 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 (value, map) -> + let rec get n = function DiscriminationTree.Node (v, 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 - retrieve tree term [] + PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map [] ;; - - let jump_list arities = function - | DiscriminationTree.Node (value, map) -> - let rec get n tree = - match tree with - | DiscriminationTree.Node (v, m) -> - if n = 0 then - [tree] - else - PSMap.fold - (fun k v res -> - let a = - try List.assoc k arities - with Not_found -> 0 - in - (get (n-1 + a) v) @ res) m [] - in - PSMap.fold - (fun k v res -> - let arity = - try - List.assoc k arities - with Not_found -> 0 in - (get arity 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 (_, map), 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_unifiables (tree,arities) term = - let term = skip_prods term in - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let subterm = - try Some (subterm_at_pos pos term) with Not_found -> None - in - match subterm with - | None -> A.empty - | Some (Cic.Meta _) -> - let newpos = try next_t pos term with Not_found -> [] in - let jl = jump_list arities tree in - List.fold_left - (fun r s -> A.union r s) - A.empty - (List.map (fun t -> retrieve t term newpos) jl) - | Some subterm -> - let res = - let hd_term = elem_of_cic (head_of_term subterm) in - if hd_term = Variable then - A.empty else - try - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - retrieve n term (next_t pos term) - with Not_found -> - A.empty - in - try - let n = PSMap.find Variable map in - let newpos = - try after_t pos term - with Not_found -> [-1] - in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> - A.union s res - | _ -> res - else - A.union res (retrieve n term newpos) - with Not_found -> - res - in - retrieve tree term [] + let retrieve_generalizations tree term = retrieve false tree term;; + let retrieve_unifiables tree term = retrieve true tree term;; end ;; diff --git a/helm/software/components/cic/discrimination_tree.mli b/helm/software/components/cic/discrimination_tree.mli index 94c51ec57..1b3ab8be5 100644 --- a/helm/software/components/cic/discrimination_tree.mli +++ b/helm/software/components/cic/discrimination_tree.mli @@ -23,12 +23,16 @@ * http://cs.unibo.it/helm/. *) +type path + +val string_of_path : path -> string + module DiscriminationTreeIndexing : functor (A : Set.S) -> sig type t - val iter : t -> (A.t -> unit) -> unit + val iter : t -> (path -> A.t -> unit) -> unit val empty : t val index : t -> Cic.term -> A.elt -> t diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.ml b/helm/software/components/tactics/paramodulation/equality_indexing.ml index 01fecc0ed..f24ff1de1 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.ml +++ b/helm/software/components/tactics/paramodulation/equality_indexing.ml @@ -36,7 +36,7 @@ module type EqualityIndex = val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t val in_index : t -> Equality.equality -> bool - val iter : t -> (PosEqSet.t -> unit) -> unit + val iter : t -> (Discrimination_tree.path -> PosEqSet.t -> unit) -> unit end module DT = diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.mli b/helm/software/components/tactics/paramodulation/equality_indexing.mli index 9fd06f3ff..31b5e26d1 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.mli +++ b/helm/software/components/tactics/paramodulation/equality_indexing.mli @@ -34,7 +34,7 @@ module type EqualityIndex = val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t val in_index : t -> Equality.equality -> bool - val iter : t -> (PosEqSet.t -> unit) -> unit + val iter : t -> (Discrimination_tree.path -> PosEqSet.t -> unit) -> unit end module DT : EqualityIndex diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 89bb0462b..9c471d3b3 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -441,7 +441,7 @@ let subsumption_aux_all use_unification env table target = in let leftr = match left with - | Cic.Meta _ when not use_unification -> [] + | Cic.Meta _ (*when not use_unification*) -> [] | _ -> let leftc = get_candidates predicate table left in find_all_matches ~unif_fun @@ -449,7 +449,7 @@ let subsumption_aux_all use_unification env table target = in let rightr = match right with - | Cic.Meta _ when not use_unification -> [] + | Cic.Meta _ (*when not use_unification*) -> [] | _ -> let rightc = get_candidates predicate table right in find_all_matches ~unif_fun