matitaprover

[helm.git] / helm / software / components / cic / libraryObjects.ml

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index 7a4112ad5a67350a9110b54d1cc4516fd848a451..dc36636fe816d4629d6f9f08c4cfb1207ee1c8e5 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -55,17 +55,23 @@ 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_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_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;
@@ -76,11 +82,11 @@ let reset_defaults () =
 (**** 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 +95,63 @@ 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_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 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_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 () =