parameter sintax added to axiom statement

[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..c523a60de259589772165f0e8765e4468932363c 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -31,6 +31,7 @@ let default_eq_URIs = []
 let default_true_URIs = []
 let default_false_URIs = []
 let default_absurd_URIs = []
+let default_nat_URIs = []
 
 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
 let eq_URIs_ref = ref default_eq_URIs;;
@@ -38,6 +39,7 @@ let eq_URIs_ref = ref default_eq_URIs;;
 let true_URIs_ref = ref default_true_URIs
 let false_URIs_ref = ref default_false_URIs
 let absurd_URIs_ref = ref default_absurd_URIs
+let nat_URIs_ref = ref default_nat_URIs
 
 
 (**** SET_DEFAULT ****)
@@ -55,32 +57,64 @@ 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)
+  | "natural numbers",[nat_URI] ->
+      nat_URIs_ref := insert_unique nat_URI (fun x -> x) !nat_URIs_ref
+  | _,l -> 
+      raise 
+        (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
+;;
 
 let reset_defaults () =
   eq_URIs_ref := default_eq_URIs;
   true_URIs_ref := default_true_URIs;
   false_URIs_ref := default_false_URIs;
-  absurd_URIs_ref := default_absurd_URIs
+  absurd_URIs_ref := default_absurd_URIs;
+  nat_URIs_ref := default_nat_URIs
+;;
 
-(**** LOOKUP FUNCTIONS ****)
+let stack = ref [];;
+
+let push () =
+  stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref,
+            !nat_URIs_ref
+          )::!stack;
+  reset_defaults ()
+;;
 
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP in libraryObjects.ml")
+  | (eq,t,f,a,n)::tl ->
+      stack := tl;
+      eq_URIs_ref := eq;
+      true_URIs_ref := t;
+      false_URIs_ref := f;
+      absurd_URIs_ref := a;
+      nat_URIs_ref := n
+;;
+
+(**** 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,42 +123,105 @@ 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 () =
  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
+
+let nat_URI () =
+ try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None
+let is_nat_URI uri =
+ List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref