From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 14 May 2009 13:43:55 +0000 (+0000)
Subject: - libraryObjects: new default "natural numbers" with the uri of nat.
X-Git-Tag: make_still_working~3979
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68dbcd02022874a025a9444aa1125b0458816fbb;p=helm.git

- libraryObjects: new default "natural numbers" with the uri of nat.
alias num "natural number" uses this one instead of the hardcoded uri (removed)
also destroy_nat (moved to termAcicContent) looks at this default
---

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index c350f38c4..fb8909152 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -28,6 +28,7 @@
 open Printf
 
 module Ast = CicNotationPt
+module Obj = LibraryObjects
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -70,6 +71,21 @@ let constructor_of_inductive_type uri i j =
 let left_params_no_of_inductive_type uri =
    snd (get_types uri)
 
+let destroy_nat annterm =
+  let is_zero = function
+    | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
+    | _ -> false
+  in
+  let is_succ = function
+    | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
+    | _ -> false
+  in
+  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 ast_of_acic0 ~output_type term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
@@ -124,7 +140,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
-       (match LibraryObjects.destroy_nat t with
+       (match destroy_nat t with
        | Some n -> idref aid (Ast.Num (string_of_int n, -1))
        | None ->
            let deannot_he = Deannotate.deannotate_term he in
diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 0364803c7..a397de41e 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t =
          | v when H.is_proof c v && H.is_atomic v          ->
 	    let x = S.subst v t in
 	    opt_proof g (info st "Optimizer: remove 5") true c x 
-	 | v                                               ->
+(*	 | v when t = C.Rel 1                              ->
+	    g (info st "Optimizer: remove 6") v 
+*)	 | v                                               ->
 	    g st (C.LetIn (name, v, w, t))
       in
       if es then opt_term g st es c v else g st v
diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index e402f4db2..c523a60de 100644
--- 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
diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli
index b4e19dff8..248893002 100644
--- a/helm/software/components/cic/libraryObjects.mli
+++ b/helm/software/components/cic/libraryObjects.mli
@@ -66,6 +66,5 @@ val false_URI : unit -> UriManager.uri option
 val true_URI : unit -> UriManager.uri option
 val absurd_URI : unit -> UriManager.uri option
 
-val build_nat : int -> Cic.term
-val destroy_nat : Cic.annterm -> int option
-
+val nat_URI : unit -> UriManager.uri option
+val is_nat_URI : UriManager.uri -> bool
diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 06099dcfe..c41a9aab0 100644
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -25,10 +25,31 @@
 
 (* $Id$ *)
 
+module C   = Cic
+module Obj = LibraryObjects
+module DT  = DisambiguateTypes
+
+let error msg =
+   raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
+
+let build_nat o s str =
+   let n = int_of_string str in
+   if n < 0 then error (str ^ " is not a valid natural number number") else
+   let rec aux n = if n = 0 then o () else s (aux (pred n)) in
+   aux n
+
+let interp_natural_number num =
+   let nat_URI = match Obj.nat_URI () with
+      | Some uri -> uri
+      | None     -> error "no default natural numbers"
+   in
+   let o () = C.MutConstruct (nat_URI,0,1,[]) in
+   let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in
+   build_nat o s num
+
 let _ =
   DisambiguateChoices.add_num_choice
-    ("natural number",
-      `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num)));
+    ("natural number", `Num_interp interp_natural_number);
   DisambiguateChoices.add_num_choice
     ("Coq natural number",
       `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
@@ -39,8 +60,8 @@ let _ =
     ("binary positive number",
       `Num_interp (fun num ->
         let num = int_of_string num in
-        if num = 0 then
-          raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
+        if num = 0 then 
+          error "0 is not a valid positive number"
         else
           HelmLibraryObjects.build_bin_pos num));
   DisambiguateChoices.add_num_choice
diff --git a/helm/software/matita/library/nat/nat.ma b/helm/software/matita/library/nat/nat.ma
index 5e3e769ec..83b489f06 100644
--- a/helm/software/matita/library/nat/nat.ma
+++ b/helm/software/matita/library/nat/nat.ma
@@ -19,6 +19,9 @@ inductive nat : Set \def
   | S : nat \to nat.
 
 interpretation "Natural numbers" 'N = nat.
+
+default "natural numbers" cic:/matita/nat/nat/nat.ind.
+
 alias num (instance 0) = "natural number".
 
 definition pred: nat \to nat \def