(**** TABLES ****)
-let default_eq_URIs =
- [HelmLibraryObjects.Logic.eq_URI,
- HelmLibraryObjects.Logic.sym_eq_URI,
- HelmLibraryObjects.Logic.trans_eq_URI,
- HelmLibraryObjects.Logic.eq_ind_URI,
- HelmLibraryObjects.Logic.eq_ind_r_URI];;
-
-let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
-let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
-let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
+let default_eq_URIs = []
+let default_true_URIs = []
+let default_false_URIs = []
+let default_absurd_URIs = []
(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
-let eq_URIs_ref =
- ref [HelmLibraryObjects.Logic.eq_URI,
- HelmLibraryObjects.Logic.sym_eq_URI,
- HelmLibraryObjects.Logic.trans_eq_URI,
- HelmLibraryObjects.Logic.eq_ind_URI,
- HelmLibraryObjects.Logic.eq_ind_r_URI];;
+let eq_URIs_ref = ref default_eq_URIs;;
-let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI]
-let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI]
-let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
+let true_URIs_ref = ref default_true_URIs
+let false_URIs_ref = ref default_false_URIs
+let absurd_URIs_ref = ref default_absurd_URIs
(**** SET_DEFAULT ****)
(**** LOOKUP FUNCTIONS ****)
-let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
+let eq_URI () =
+ try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ with Failure "hd" -> None
let is_eq_URI uri =
List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
+let is_eq_refl_URI uri =
+ let urieq = UriManager.strip_xpointer uri in
+ is_eq_URI urieq &&
+ not (UriManager.eq urieq uri)
+;;
+
let is_eq_ind_URI uri =
List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
let is_sym_eq_URI uri =
List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+let eq_refl_URI ~eq:uri =
+ let uri = UriManager.strip_xpointer uri in
+ UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
+
let sym_eq_URI ~eq:uri =
try
let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
-let true_URI () = List.hd !true_URIs_ref
-let false_URI () = List.hd !false_URIs_ref
-let absurd_URI () = List.hd !absurd_URIs_ref
+let true_URI () =
+ try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
+let false_URI () =
+ try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
+let absurd_URI () =
+ try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None