X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;h=d73eb9c3a2bac8f9cab0c8dfa767309c26c76981;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=8753782d47e577a5bf64bc896d3e1776dcd962bf;hpb=101ecc0bc98f6f979d08200ae562ce89bffc0670;p=helm.git diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 8753782d4..d73eb9c3a 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + type path_string_elem = Cic.term;; type path_string = path_string_elem list;; @@ -16,6 +41,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,90 +55,103 @@ end module PSMap = Map.Make(OrderedPathStringElement);; -module DiscriminationTree = struct - type key = path_string - type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t) - - let empty = Node (None, PSMap.empty) - - let rec find l t = - match (l, t) with - | [], Node (None, _) -> raise Not_found - | [], Node (Some v, _) -> v - | x::r, Node (_, m) -> find r (PSMap.find x m) - - let rec mem l t = - match (l, t) with - | [], Node (None, _) -> false - | [], Node (Some _, _) -> true - | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false - - let add l v t = - let rec ins = function - | [], Node (_, m) -> Node (Some v, m) - | x::r, Node (v, m) -> - let t' = try PSMap.find x m with Not_found -> empty in - let t'' = ins (r, t') in - Node (v, PSMap.add x t'' m) - in - ins (l, t) - - let rec remove l t = - match (l, t) with - | [], Node (_, m) -> Node (None, 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) - with Not_found -> - t - - let rec fold f t acc = - let rec traverse revp t acc = match t with - | Node (None, m) -> - PSMap.fold (fun x -> traverse (x::revp)) m acc - | Node (Some v, m) -> - f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc) - in - traverse [] t acc +module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare end +module PosEqSet = Set.Make(OrderedPosEquality);; + + +module DiscriminationTree = Trie.Make(PSMap);; + + +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 _, _, (_, 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 ;; let remove_index tree equality = - let _, (_, l, r, ordering), _, _ = equality in + 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 ;; let in_index tree equality = - let _, (_, l, r, ordering), _, _ = equality in + let _, _, (_, l, r, ordering), _, _ = equality in let psl = path_string_of_term l 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) ;; @@ -126,23 +169,12 @@ let rec subterm_at_pos pos term = | index::pos -> match term with | Cic.Appl l -> - (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found) + (try subterm_at_pos pos (List.nth l index) + with Failure _ -> raise Not_found) | _ -> raise Not_found ;; -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 +192,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 Not_found -> [-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 +261,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 Not_found -> [-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 [] ;;