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://helm.cs.unibo.it/
30 let default_eq_URIs = []
31 let default_true_URIs = []
32 let default_false_URIs = []
33 let default_absurd_URIs = []
34 let default_nat_URIs = []
36 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
37 let eq_URIs_ref = ref default_eq_URIs;;
39 let true_URIs_ref = ref default_true_URIs
40 let false_URIs_ref = ref default_false_URIs
41 let absurd_URIs_ref = ref default_absurd_URIs
42 let nat_URIs_ref = ref default_nat_URIs
45 (**** SET_DEFAULT ****)
47 exception NotRecognized of string;;
49 (* insert an element in front of the list, removing from the list all the
50 previous elements with the same key associated *)
51 let insert_unique e extract l =
52 let uri = extract e in
54 List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l
58 let set_default what l =
60 "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
61 eq_ind_r_URI;eq_rec_URI;eq_rec_r_URI;eq_rect_URI;
62 eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] ->
65 (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
66 eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI,
67 eq_rect_r_URI,eq_f_URI,eq_f_sym_URI)
68 (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref
69 | "true",[true_URI] ->
70 true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
71 | "false",[false_URI] ->
72 false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
73 | "absurd",[absurd_URI] ->
74 absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
75 | "natural numbers",[nat_URI] ->
76 nat_URIs_ref := insert_unique nat_URI (fun x -> x) !nat_URIs_ref
79 (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
82 let reset_defaults () =
83 eq_URIs_ref := default_eq_URIs;
84 true_URIs_ref := default_true_URIs;
85 false_URIs_ref := default_false_URIs;
86 absurd_URIs_ref := default_absurd_URIs;
87 nat_URIs_ref := default_nat_URIs
93 stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref,
101 | [] -> raise (Failure "Unable to POP in libraryObjects.ml")
102 | (eq,t,f,a,n)::tl ->
107 absurd_URIs_ref := a;
111 (**** LOOKUP FUNCTIONS ****)
113 try let eq,_,_,_,_,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
114 with Failure "hd" -> None
117 List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
119 let is_eq_refl_URI uri =
120 let urieq = UriManager.strip_xpointer uri in
122 not (UriManager.eq urieq uri)
125 let is_eq_ind_URI uri =
126 List.exists (fun (_,_,_,eq_ind,_,_,_,_,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
127 let is_eq_ind_r_URI uri =
128 List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
129 let is_eq_rec_URI uri =
130 List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref
131 let is_eq_rec_r_URI uri =
132 List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref
133 let is_eq_rect_URI uri =
134 List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref
135 let is_eq_rect_r_URI uri =
136 List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref
137 let is_trans_eq_URI uri =
138 List.exists (fun (_,_,trans_eq,_,_,_,_,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
139 let is_sym_eq_URI uri =
140 List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
141 let is_eq_f_URI uri =
142 List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
143 let is_eq_f_sym_URI uri =
144 List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
147 is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri ||
148 is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri ||
149 is_eq_rect_URI uri || is_eq_rect_r_URI uri ||
150 is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri ||
155 let eq_refl_URI ~eq:uri =
156 let uri = UriManager.strip_xpointer uri in
157 UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
159 let sym_eq_URI ~eq:uri =
161 let _,x,_,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
162 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
164 let trans_eq_URI ~eq:uri =
166 let _,_,x,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
167 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
169 let eq_ind_URI ~eq:uri =
171 let _,_,_,x,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
172 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
174 let eq_ind_r_URI ~eq:uri =
176 let _,_,_,_,x,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
177 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
179 let eq_rec_URI ~eq:uri =
181 let _,_,_,_,_,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
182 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
184 let eq_rec_r_URI ~eq:uri =
186 let _,_,_,_,_,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
187 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
189 let eq_rect_URI ~eq:uri =
191 let _,_,_,_,_,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
192 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
194 let eq_rect_r_URI ~eq:uri =
196 let _,_,_,_,_,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
197 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
199 let eq_f_URI ~eq:uri =
201 let _,_,_,_,_,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
202 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
204 let eq_f_sym_URI ~eq:uri =
206 let _,_,_,_,_,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
207 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
210 let eq_URI_of_eq_f_URI eq_f_URI =
212 let x,_,_,_,_,_,_,_,_,_,_ =
213 List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref
215 with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
218 try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
220 try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
222 try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
225 try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None
227 List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref