X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=e402f4db214433ce174396929744ba8a4042d2cf;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=7a4112ad5a67350a9110b54d1cc4516fd848a451;hpb=938823007263452cd877b06865a555e1f06c1ede;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index 7a4112ad5..e402f4db2 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -55,32 +55,58 @@ 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;
   true_URIs_ref := default_true_URIs;
   false_URIs_ref := default_false_URIs;
   absurd_URIs_ref := default_absurd_URIs
+;;
 
-(**** LOOKUP FUNCTIONS ****)
+let stack = ref [];;
+
+let push () =
+  stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref)::!stack;
+  reset_defaults ()
+;;
 
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP in libraryObjects.ml")
+  | (eq,t,f,a)::tl ->
+      stack := tl;
+      eq_URIs_ref := eq;
+      true_URIs_ref := t;
+      false_URIs_ref := f;
+      absurd_URIs_ref := a
+;;
+
+(**** 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 +115,129 @@ 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 = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
+
+let zero = Cic.MutConstruct (nat_URI,0,1,[])
+let succ = Cic.MutConstruct (nat_URI,0,2,[])
+
+let is_zero = function
+  | Cic.AMutConstruct (_, uri, 0, 1, _) when UriManager.eq uri nat_URI -> true
+  | _ -> false
+
+let is_succ = function
+  | Cic.AMutConstruct (_, uri, 0, 2, _) when UriManager.eq uri nat_URI -> true
+  | _ -> false
+
+let build_nat n =
+  if n < 0 then assert false;
+  let rec aux = function
+    | 0 -> zero
+    | n -> Cic.Appl [ succ; (aux (n - 1)) ]
+  in
+  aux n
+
+let destroy_nat annterm =
+  let rec aux acc = function
+    | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
+    | t when is_zero t -> Some acc
+    | _ -> None in
+  aux 0 annterm
+