X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FlibraryObjects.ml;h=579c21eede3a9f2f2e44023d180377fcf2282341;hb=63f876b112e1be016e8063e6a00ec47f841ee615;hp=7a4112ad5a67350a9110b54d1cc4516fd848a451;hpb=9e4b17bfecb0cc4f16e5fa36f5377f7ae9fb0911;p=helm.git

diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml
index 7a4112ad5..579c21eed 100644
--- a/components/cic/libraryObjects.ml
+++ b/components/cic/libraryObjects.ml
@@ -55,17 +55,25 @@ let insert_unique e extract l =
 
 let set_default what l =
   match what,l with
-    "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
+  "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
+              eq_ind_r_URI;eq_rec_URI;eq_rec_r_URI;eq_rect_URI;
+              eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] ->
       eq_URIs_ref :=
-       insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
-        (fun x,_,_,_,_ -> x) !eq_URIs_ref
+       insert_unique
+         (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
+          eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI,
+          eq_rect_r_URI,eq_f_URI,eq_f_sym_URI)
+        (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref
   | "true",[true_URI] ->
       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
   | "false",[false_URI] ->
       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 what)
+  | _,l -> 
+      raise 
+        (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
+;;
 
 let reset_defaults () =
   eq_URIs_ref := default_eq_URIs;
@@ -73,14 +81,14 @@ let reset_defaults () =
   false_URIs_ref := default_false_URIs;
   absurd_URIs_ref := default_absurd_URIs
 
-(**** LOOKUP FUNCTIONS ****)
 
+(**** LOOKUP FUNCTIONS ****)
 let eq_URI () =
- try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ 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
+ List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
 
 let is_eq_refl_URI uri =
   let urieq = UriManager.strip_xpointer uri in
@@ -89,39 +97,97 @@ let is_eq_refl_URI uri =
 ;;
 
 let is_eq_ind_URI uri =
- List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
-
+ 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
+ List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
+let is_eq_rec_URI uri =
+ List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref
+let is_eq_rec_r_URI uri =
+ List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref
+let is_eq_rect_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref
+let is_eq_rect_r_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref
 let is_trans_eq_URI uri = 
- List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
+ 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
+ List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+let is_eq_f_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
+let is_eq_f_sym_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 
+let in_eq_URIs uri =  
+  is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri || 
+  is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri ||
+  is_eq_rect_URI uri || is_eq_rect_r_URI uri ||
+  is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri ||
+  is_eq_f_sym_URI uri
+
+
+ 
 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 trans_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 eq_ind_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 eq_ind_r_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 eq_rec_URI ~eq:uri =
+ try
+  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 eq_rec_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 (UriManager.string_of_uri uri))
+
+let eq_rect_URI ~eq:uri =
+ try
+  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 eq_rect_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 (UriManager.string_of_uri uri))
+
+let eq_f_URI ~eq:uri =
+ try
+  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 eq_f_sym_URI ~eq:uri =
+ try
+  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 eq_URI_of_eq_f_URI eq_f_URI = 
+  try
+  let x,_,_,_,_,_,_,_,_,_,_ = 
+    List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref 
+  in x
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
+ 
 let true_URI () =
  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 let false_URI () =