X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;fp=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;h=9470e1bdec34d17edde11a06eb51b252dbbe21b9;hb=969fb8763a6d4afb88aef1eaa4a4d1ce7d626264;hp=8753782d47e577a5bf64bc896d3e1776dcd962bf;hpb=7e0973fe9cb31ea68d8a046766f64fc978fbcdf6;p=helm.git diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 8753782d4..9470e1bde 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -16,6 +16,11 @@ let rec path_string_of_term = function ;; +let string_of_path_string ps = + String.concat "." (List.map CicPp.ppterm ps) +;; + + module OrderedPathStringElement = struct type t = path_string_elem @@ -25,9 +30,22 @@ end module PSMap = Map.Make(OrderedPathStringElement);; +module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + + let compare = Pervasives.compare +end + +module PosEqSet = Set.Make(OrderedPosEquality);; + + +module DiscriminationTree = Trie.Make(PSMap);; + + +(* module DiscriminationTree = struct type key = path_string - type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t) + type t = Node of PosEqSet.t option * (t PSMap.t) let empty = Node (None, PSMap.empty) @@ -56,10 +74,11 @@ module DiscriminationTree = struct let rec remove l t = match (l, t) with | [], Node (_, m) -> Node (None, m) - | x::r, Node (v, m) -> + | x::r, Node (v, m) -> try let t' = remove r (PSMap.find x m) in - Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m) + let m' = if t' = empty then PSMap.remove x m else PSMap.add x t' m in + Node (v, m') with Not_found -> t @@ -73,18 +92,55 @@ module DiscriminationTree = struct traverse [] t acc end +*) + +let string_of_discrimination_tree tree = + let rec to_string level = function + | DiscriminationTree.Node (value, map) -> + let s = + match value with + | Some v -> + (String.make (2 * level) ' ') ^ + "{" ^ (String.concat "; " + (List.map + (fun (p, e) -> + "(" ^ (Utils.string_of_pos p) ^ ", " ^ + (Inference.string_of_equality e) ^ ")") + (PosEqSet.elements v))) ^ "}" + | None -> "" + in + let rest = + String.concat "\n" + (PSMap.fold + (fun k v s -> + let ks = CicPp.ppterm k in + let rs = to_string (level+1) v in + ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) + map []) + in + s ^ rest + in + to_string 0 tree +;; let index tree equality = let _, (_, l, r, ordering), _, _ = equality in let psl = path_string_of_term l and psr = path_string_of_term r in + let index pos tree ps = + let ps_set = + try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in + let tree = + DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in + tree + in match ordering with - | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree - | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree + | Utils.Gt -> index Utils.Left tree psl + | Utils.Lt -> index Utils.Right tree psr | _ -> - let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in - DiscriminationTree.add psr (Utils.Right, equality) tree + let tree = index Utils.Left tree psl in + index Utils.Right tree psr ;; @@ -92,12 +148,23 @@ let remove_index tree equality = let _, (_, l, r, ordering), _, _ = equality in let psl = path_string_of_term l and psr = path_string_of_term r in + let remove_index pos tree ps = + try + let ps_set = + PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in + if PosEqSet.is_empty ps_set then + DiscriminationTree.remove ps tree + else + DiscriminationTree.add ps ps_set tree + with Not_found -> + tree + in match ordering with - | Utils.Gt -> DiscriminationTree.remove psl tree - | Utils.Lt -> DiscriminationTree.remove psr tree + | Utils.Gt -> remove_index Utils.Left tree psl + | Utils.Lt -> remove_index Utils.Right tree psr | _ -> - let tree = DiscriminationTree.remove psl tree in - DiscriminationTree.remove psr tree + let tree = remove_index Utils.Left tree psl in + remove_index Utils.Right tree psr ;; @@ -107,8 +174,11 @@ let in_index tree equality = and psr = path_string_of_term r in let meta_convertibility = Inference.meta_convertibility_eq equality in let ok ps = - try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq - with Not_found -> false + try + let set = DiscriminationTree.find ps tree in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + with Not_found -> + false in (ok psl) || (ok psr) ;; @@ -116,6 +186,7 @@ let in_index tree equality = let head_of_term = function | Cic.Appl (hd::tl) -> hd +(* | Cic.Meta _ -> Cic.Implicit None *) | term -> term ;; @@ -131,18 +202,6 @@ let rec subterm_at_pos pos term = ;; -let next_t pos term = - let t = subterm_at_pos pos term in - try - let t2 = subterm_at_pos [1] t in - pos @ [1] - with Not_found -> - match pos with - | [] -> [1] - | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] -;; - - let rec after_t pos term = let pos' = match pos with @@ -160,24 +219,44 @@ let rec after_t pos term = ;; +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 term = - let rec retrieve tree term pos = + let rec retrieve tree term pos = match tree with - | DiscriminationTree.Node (value, map) -> + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> let res = try let hd_term = head_of_term (subterm_at_pos pos term) in let n = PSMap.find hd_term map in match n with - | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) -> - retrieve n term (next_t pos term) + let newpos = try next_t pos term with Not_found -> [] in + retrieve n term newpos with Not_found -> - [] + PosEqSet.empty in try let n = PSMap.find (Cic.Implicit None) map in - res @ (retrieve n term (after_t pos term)) + let newpos = try after_t pos term with _ -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res + | _ -> res + else + PosEqSet.union res (retrieve n term newpos) with Not_found -> res in @@ -209,30 +288,43 @@ let jump_list = function let retrieve_unifiables tree term = let rec retrieve tree term pos = match tree with - | DiscriminationTree.Node (value, map) -> - let res = - try - match subterm_at_pos pos term with - | Cic.Meta _ -> - List.concat - (List.map - (fun t -> retrieve t term (next_t pos term)) - (jump_list tree)) - | subterm -> + | 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 -> PosEqSet.empty + | Some (Cic.Meta _) -> + let newpos = try next_t pos term with Not_found -> [] in + let jl = jump_list tree in + List.fold_left + (fun r s -> PosEqSet.union r s) + PosEqSet.empty + (List.map (fun t -> retrieve t term newpos) jl) + | Some subterm -> + let res = + try let hd_term = head_of_term subterm in let n = PSMap.find hd_term map in match n with - | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) -> retrieve n term (next_t pos term) - with Not_found -> - [] - in - try - let n = PSMap.find (Cic.Implicit None) map in - res @ (retrieve n term (after_t pos term)) - with Not_found -> - res + with Not_found -> + PosEqSet.empty + in + try + let n = PSMap.find (Cic.Implicit None) map in + let newpos = try after_t pos term with _ -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res + | _ -> res + else + PosEqSet.union res (retrieve n term newpos) + with Not_found -> + res in retrieve tree term [] ;;