X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fpath_indexing.ml;h=06da404abeaa102d87f5c670e608c878fecf7455;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=87e917fff79b5c176401225a1cc757f20f64967c;hpb=b9599336a7e5b19b3cf37d73a9d14f9899e2b82f;p=helm.git diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml index 87e917fff..06da404ab 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/paramodulation/path_indexing.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/. + *) + (* path indexing implementation *) (* position of the subterm, subterm (Appl are not stored...) *) @@ -49,8 +74,6 @@ end module PSMap = Map.Make(OrderedPathStringElement);; -(* module PSTrie = Trie.Make(PathStringElementMap);; *) - module OrderedPosEquality = struct type t = Utils.pos * Inference.equality @@ -59,70 +82,17 @@ end module PosEqSet = Set.Make(OrderedPosEquality);; -(* - * Trie: maps over lists. - * Copyright (C) 2000 Jean-Christophe FILLIATRE - *) -module PSTrie = struct - type key = path_string - type t = Node of PosEqSet.t 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 -end +module PSTrie = Trie.Make(PSMap);; let index trie equality = - let _, (_, l, r, ordering), _, _ = equality in + let _, _, (_, l, r, ordering), _, _ = equality in let psl = path_strings_of_term 0 l and psr = path_strings_of_term 0 r in let index pos trie ps = let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in -(* if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *) -(* Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *) -(* (Inference.string_of_equality equality); *) trie in match ordering with @@ -135,7 +105,7 @@ let index trie equality = let remove_index trie equality = - let _, (_, l, r, ordering), _, _ = equality in + let _, _, (_, l, r, ordering), _, _ = equality in let psl = path_strings_of_term 0 l and psr = path_strings_of_term 0 r in let remove_index pos trie ps = @@ -146,10 +116,7 @@ let remove_index trie equality = else PSTrie.add ps ps_set trie with Not_found -> -(* Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *) -(* (Inference.string_of_equality equality); *) trie -(* raise Not_found *) in match ordering with | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl @@ -160,6 +127,22 @@ let remove_index trie equality = ;; +let in_index trie equality = + let _, _, (_, l, r, ordering), _, _ = equality in + let psl = path_strings_of_term 0 l + and psr = path_strings_of_term 0 r in + let meta_convertibility = Inference.meta_convertibility_eq equality in + let ok ps = + try + let set = PSTrie.find ps trie in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + with Not_found -> + false + in + (List.exists ok psl) || (List.exists ok psr) +;; + + let head_of_term = function | Cic.Appl (hd::tl) -> hd | term -> term @@ -251,16 +234,6 @@ let rec retrieve_unifiables trie term = List.fold_left (fun r s -> PosEqSet.inter r s) hd tl | _ -> PosEqSet.empty with Not_found -> -(* Printf.printf "Not_found: %s, term was: %s\n" *) -(* (CicPp.ppterm hd_term) (CicPp.ppterm term); *) -(* Printf.printf "map is:\n %s\n\n" *) -(* (String.concat "\n" *) -(* (PSMap.fold *) -(* (fun k v l -> *) -(* match k with *) -(* | Index i -> ("Index " ^ (string_of_int i))::l *) -(* | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *) -(* map [])); *) PosEqSet.empty in try @@ -273,6 +246,12 @@ let rec retrieve_unifiables trie term = ;; +let retrieve_all trie term = + PSTrie.fold + (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty +;; + + let string_of_pstrie trie = let rec to_string level = function | PSTrie.Node (v, map) ->