X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=7a4112ad5a67350a9110b54d1cc4516fd848a451;hb=50844b0116c863862434c7c673c5caaf6ff78cdf;hp=adbc219cc3fd72771b314a3e61eeea85a98cfc52;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index adbc219cc..7a4112ad5 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -27,33 +27,22 @@
 
 (**** 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 ****)
 
-exception NotRecognized;;
+exception NotRecognized of string;;
 
 (* insert an element in front of the list, removing from the list all the
    previous elements with the same key associated *)
@@ -76,7 +65,7 @@ let set_default what l =
       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
   | "absurd",[absurd_URI] ->
       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
-  | _,_ -> raise NotRecognized
+  | _,_ -> raise (NotRecognized what)
 
 let reset_defaults () =
   eq_URIs_ref := default_eq_URIs;
@@ -86,37 +75,56 @@ let reset_defaults () =
 
 (**** 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_eq_ind_r_URI uri =
  List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
-
+let is_trans_eq_URI uri = 
+ List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq 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
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let trans_eq_URI ~eq:uri =
  try
   let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_URI ~eq:uri =
  try
   let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_r_URI ~eq:uri =
  try
   let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
- with Not_found -> raise NotRecognized
-
-let true_URI () = List.hd !true_URIs_ref
-let false_URI () = List.hd !false_URIs_ref
-let absurd_URI () = List.hd !absurd_URIs_ref
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
+
+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