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/.
28 (* path indexing implementation *)
30 (* position of the subterm, subterm (Appl are not stored...) *)
36 type path_string_elem = Index of int | Term of Cic.term;;
37 type path_string = path_string_elem list;;
40 let rec path_strings_of_term index =
41 let module C = Cic in function
42 | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
44 let p = if index > 0 then [Index index; Term hd] else [Term hd] in
48 let rr = path_strings_of_term i t in
49 (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
53 | term -> [ [Index index; Term term] ]
57 let string_of_path_string ps =
63 | Index i -> "Index " ^ (string_of_int i)
64 | Term t -> "Term " ^ (CicPp.ppterm t)
71 module OrderedPathStringElement = struct
72 type t = path_string_elem
76 | Index i, Index j -> Pervasives.compare i j
77 | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
78 | Index _, Term _ -> -1
79 | Term _, Index _ -> 1
82 module PSMap = Map.Make(OrderedPathStringElement);;
84 module PSTrie = Trie.Make(PSMap);;
88 let empty = PSTrie.empty
89 let arities = Hashtbl.create 0
91 let index trie term info =
92 let ps = path_strings_of_term 0 term in
95 let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in
96 let trie = PSTrie.add ps (A.add info ps_set) trie in
99 let remove_index trie term info=
100 let ps = path_strings_of_term 0 term in
104 let ps_set = A.remove info (PSTrie.find ps trie) in
105 if A.is_empty ps_set then
106 PSTrie.remove ps trie
108 PSTrie.add ps ps_set trie
109 with Not_found -> trie) trie ps
112 let in_index trie term test =
113 let ps = path_strings_of_term 0 term in
116 let set = PSTrie.find ps trie in
125 let head_of_term = function
126 | Cic.Appl (hd::tl) -> hd
131 let subterm_at_pos index term =
137 (try List.nth l index with Failure _ -> raise Not_found)
138 | _ -> raise Not_found
142 let rec retrieve_generalizations trie term =
144 | PSTrie.Node (value, map) ->
147 | Cic.Meta _ -> A.empty
149 let hd_term = head_of_term term in
151 let n = PSMap.find (Term hd_term) map in
153 | PSTrie.Node (Some s, _) -> s
154 | PSTrie.Node (None, m) ->
160 let t = subterm_at_pos i term in
161 let s = retrieve_generalizations v t in
168 List.fold_left (fun r s -> A.inter r s) hd tl
174 let n = PSMap.find (Term (Cic.Implicit None)) map in
176 | PSTrie.Node (Some s, _) -> A.union res s
183 let rec retrieve_unifiables trie term =
185 | PSTrie.Node (value, map) ->
190 (fun ps v res -> A.union res v)
191 (PSTrie.Node (None, map))
194 let hd_term = head_of_term term in
196 let n = PSMap.find (Term hd_term) map in
198 | PSTrie.Node (Some v, _) -> v
199 | PSTrie.Node (None, m) ->
205 let t = subterm_at_pos i term in
206 let s = retrieve_unifiables v t in
213 List.fold_left (fun r s -> A.inter r s) hd tl
219 let n = PSMap.find (Term (Cic.Implicit None)) map in
221 | PSTrie.Node (Some s, _) -> A.union res s