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 () =
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
| 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
+