- libraryObjects: new default "natural numbers" with the uri of nat.

[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 e402f4db214433ce174396929744ba8a4042d2cf..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 ****)
@@ -70,6 +72,8 @@ let set_default what l =
       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"))
@@ -79,25 +83,29 @@ 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
 ;;
 
 let stack = ref [];;
 
 let push () =
-  stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref)::!stack;
+  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)::tl ->
+  | (eq,t,f,a,n)::tl ->
       stack := tl;
       eq_URIs_ref := eq;
       true_URIs_ref := t;
       false_URIs_ref := f;
-      absurd_URIs_ref := a
+      absurd_URIs_ref := a;
+      nat_URIs_ref := n
 ;;
 
 (**** LOOKUP FUNCTIONS ****)
@@ -213,31 +221,7 @@ let false_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