1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* path indexing implementation *)
28 (* position of the subterm, subterm (Appl are not stored...) *)
34 type path_string_elem = Index of int | Term of Cic.term;;
35 type path_string = path_string_elem list;;
38 let rec path_strings_of_term index =
39 let module C = Cic in function
40 | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
42 let p = if index > 0 then [Index index; Term hd] else [Term hd] in
46 let rr = path_strings_of_term i t in
47 (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
51 | term -> [ [Index index; Term term] ]
55 let string_of_path_string ps =
61 | Index i -> "Index " ^ (string_of_int i)
62 | Term t -> "Term " ^ (CicPp.ppterm t)
69 module OrderedPathStringElement = struct
70 type t = path_string_elem
74 | Index i, Index j -> Pervasives.compare i j
75 | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
76 | Index _, Term _ -> -1
77 | Term _, Index _ -> 1
80 module PSMap = Map.Make(OrderedPathStringElement);;
82 module PSTrie = Trie.Make(PSMap);;
86 let empty = PSTrie.empty
87 let arities = Hashtbl.create 0
89 let index trie term info =
90 let ps = path_strings_of_term 0 term in
93 let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in
94 let trie = PSTrie.add ps (A.add info ps_set) trie in
97 let remove_index trie term info=
98 let ps = path_strings_of_term 0 term in
102 let ps_set = A.remove info (PSTrie.find ps trie) in
103 if A.is_empty ps_set then
104 PSTrie.remove ps trie
106 PSTrie.add ps ps_set trie
107 with Not_found -> trie) trie ps
110 let in_index trie term test =
111 let ps = path_strings_of_term 0 term in
114 let set = PSTrie.find ps trie in
123 let head_of_term = function
124 | Cic.Appl (hd::tl) -> hd
129 let subterm_at_pos index term =
135 (try List.nth l index with Failure _ -> raise Not_found)
136 | _ -> raise Not_found
140 let rec retrieve_generalizations trie term =
142 | PSTrie.Node (value, map) ->
145 | Cic.Meta _ -> A.empty
147 let hd_term = head_of_term term in
149 let n = PSMap.find (Term hd_term) map in
151 | PSTrie.Node (Some s, _) -> s
152 | PSTrie.Node (None, m) ->
158 let t = subterm_at_pos i term in
159 let s = retrieve_generalizations v t in
166 List.fold_left (fun r s -> A.inter r s) hd tl
172 let n = PSMap.find (Term (Cic.Implicit None)) map in
174 | PSTrie.Node (Some s, _) -> A.union res s
181 let rec retrieve_unifiables trie term =
183 | PSTrie.Node (value, map) ->
188 (fun ps v res -> A.union res v)
189 (PSTrie.Node (None, map))
192 let hd_term = head_of_term term in
194 let n = PSMap.find (Term hd_term) map in
196 | PSTrie.Node (Some v, _) -> v
197 | PSTrie.Node (None, m) ->
203 let t = subterm_at_pos i term in
204 let s = retrieve_unifiables v t in
211 List.fold_left (fun r s -> A.inter r s) hd tl
217 let n = PSMap.find (Term (Cic.Implicit None)) map in
219 | PSTrie.Node (Some s, _) -> A.union res s