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 = []
35 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
36 let eq_URIs_ref = ref default_eq_URIs;;
38 let true_URIs_ref = ref default_true_URIs
39 let false_URIs_ref = ref default_false_URIs
40 let absurd_URIs_ref = ref default_absurd_URIs
43 (**** SET_DEFAULT ****)
45 exception NotRecognized of string;;
47 (* insert an element in front of the list, removing from the list all the
48 previous elements with the same key associated *)
49 let insert_unique e extract l =
50 let uri = extract e in
52 List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l
56 let set_default what l =
58 "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
59 eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] ->
62 (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
63 eq_ind_r_URI,eq_f_URI,eq_f_sym_URI)
64 (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref
65 | "true",[true_URI] ->
66 true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
67 | "false",[false_URI] ->
68 false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
69 | "absurd",[absurd_URI] ->
70 absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
73 (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
76 let reset_defaults () =
77 eq_URIs_ref := default_eq_URIs;
78 true_URIs_ref := default_true_URIs;
79 false_URIs_ref := default_false_URIs;
80 absurd_URIs_ref := default_absurd_URIs
82 (**** LOOKUP FUNCTIONS ****)
85 try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
86 with Failure "hd" -> None
89 List.exists (fun (eq,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
91 let is_eq_refl_URI uri =
92 let urieq = UriManager.strip_xpointer uri in
94 not (UriManager.eq urieq uri)
97 let is_eq_ind_URI uri =
98 List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
100 let is_eq_ind_r_URI uri =
101 List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
102 let is_trans_eq_URI uri =
103 List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
104 let is_sym_eq_URI uri =
105 List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
106 let is_eq_f_URI uri =
107 List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
108 let is_eq_f_sym_URI uri =
109 List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
113 let eq_refl_URI ~eq:uri =
114 let uri = UriManager.strip_xpointer uri in
115 UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
117 let sym_eq_URI ~eq:uri =
119 let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
120 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
122 let trans_eq_URI ~eq:uri =
124 let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
125 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
127 let eq_ind_URI ~eq:uri =
129 let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
130 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
132 let eq_ind_r_URI ~eq:uri =
134 let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
135 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
137 let eq_f_URI ~eq:uri =
139 let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
140 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
142 let eq_f_sym_URI ~eq:uri =
144 let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
145 with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
148 let eq_URI_of_eq_f_URI eq_f_URI =
151 List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref
153 with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
156 try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
158 try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
160 try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None