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