+(* 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...) *)
module PSMap = Map.Make(OrderedPathStringElement);;
-(* module PSTrie = Trie.Make(PathStringElementMap);; *)
-
module OrderedPosEquality = struct
type t = Utils.pos * Inference.equality
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
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 =
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
;;
+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
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
;;
+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) ->
projects / helm.git / blobdiff