Very experimental commit: the type of the source is now required in LetIns

[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 e2f5fd36324ba017a59c6509f0b4bdf7f14f87a1..e402f4db214433ce174396929744ba8a4042d2cf 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -80,7 +80,25 @@ let reset_defaults () =
   true_URIs_ref := default_true_URIs;
   false_URIs_ref := default_false_URIs;
   absurd_URIs_ref := default_absurd_URIs
+;;
+
+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 () =
@@ -200,6 +218,14 @@ 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
@@ -207,3 +233,11 @@ let build_nat n =
     | 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
+