Installation des printers de nombres pour constr_expr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3268 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 200 insertions, 78 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index bf91dc37b..cc68038e7 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -10,7 +10,7 @@
 
 (* This file to allow writing (3) for (S (S (S O))) 
    and still write (S y) for (S y) *)
-
+(*
 open Pcoq
 open Pp
 open Util
@@ -21,9 +21,6 @@ open Coqlib
 open Termast
 open Extend
 
-let ast_O = ast_of_ref glob_O
-let ast_S = ast_of_ref glob_S
-  
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 let nat_of_int n dloc =
   let ast_O = set_loc dloc ast_O in
@@ -104,18 +101,25 @@ let _ =
     [None, None,
      [[Gramext.Stoken ("INT", "")],
       Gramext.action pat_nat_of_string]]
+*)
 
-
-(**********************************************************************)
-(* Parsing *)
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-
+(*i*)
 open Rawterm
 open Libnames
 open Bignat
+open Coqlib
 open Symbols
+open Pp
+open Util
+open Names
+(*i*)
 
-let nat_of_int dloc = function
+(**********************************************************************)
+(* Parsing via scopes *)
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+
+let nat_of_int dloc n =
+  match n with
   | POS n ->
       if less_than (of_string "5000") n & Options.is_verbose () then begin
 	warning ("You may experiment stack overflow and segmentation fault\
@@ -124,19 +128,19 @@ let nat_of_int dloc = function
       end;
       let ref_O = RRef (dloc, glob_O) in
       let ref_S = RRef (dloc, glob_S) in
-      let rec mk_nat n =
+      let rec mk_nat acc n =
 	if is_nonzero n then 
-	  RApp (dloc,ref_S, [mk_nat (sub_1 n)])
+	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
 	else 
-	  ref_O
+	  acc
       in 
-      mk_nat n
+      mk_nat ref_O n
   | NEG n ->
       user_err_loc (dloc, "nat_of_int",
         str "Cannot interpret a negative number as a natural number")
 
-
-let pat_nat_of_int dloc n name = match n with
+let pat_nat_of_int dloc n name =
+  match n with
   | POS n -> 
       let rec mk_nat n name =
 	if is_nonzero n then 
@@ -149,12 +153,52 @@ let pat_nat_of_int dloc n name = match n with
       user_err_loc (dloc, "pat_nat_of_int",
         str "Cannot interpret a negative number as a natural number")
 
-let _ = 
+(***********************************************************************)
+(* Printing via scopes *)
+
+exception Non_closed_number
+
+let rec int_of_nat = function
+  | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
+  | RRef (_,z) when z = glob_O -> zero
+  | _ -> raise Non_closed_number
+	  
+let uninterp_nat p =
+  try 
+    Some (POS (int_of_nat p))
+  with
+    Non_closed_number -> None
+
+let rec int_of_nat_pattern = function
+  | PatCstr (_,s,[a],_) when ConstructRef s = glob_S ->
+      add_1 (int_of_nat_pattern a)
+  | PatCstr (_,z,[],_) when ConstructRef z = glob_O -> zero
+  | _ -> raise Non_closed_number
+	  
+let uninterp_nat_pattern p =
+  try 
+    Some (POS (int_of_nat_pattern p))
+  with
+    Non_closed_number -> None
+
+(***********************************************************************)
+(* Declare the primitive parsers and printers *)
+
+let _ =
   Symbols.declare_numeral_interpreter "nat_scope"
+    ["Coq";"Init";"Peano"]
     (nat_of_int,Some pat_nat_of_int)
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
 
 (***********************************************************************)
-(* Printing *)
+(* Old ast printing *)
+
+open Coqast
+open Ast
+open Termast
+
+let ast_O = ast_of_ref glob_O
+let ast_S = ast_of_ref glob_S
 
 exception Non_closed_number
 
@@ -179,4 +223,3 @@ let _ =
 
 let _ = 
   Esyntax.declare_primitive_printer "nat_printer_O" "nat_scope" nat_printer_O
-
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index e39b8125c..f7156d46d 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -16,6 +16,10 @@ open Extend
 open Topconstr
 open Libnames
 
+(**********************************************************************)
+(* Parsing with Grammar                                               *)
+(**********************************************************************)
+
 let get_r_sign loc =
   let mkid id =
     mkRefC (Qualid (loc,Libnames.make_short_qualid id))
@@ -34,7 +38,6 @@ let get_r_sign_ast loc =
     mkid (id_of_string "Rplus"), 
     mkid (id_of_string "NRplus")))
 
-(* Parsing via Grammar *)
 let r_of_int n dloc =
   let (a0,a1,plus,_) = get_r_sign dloc in
   let rec mk_r n =
@@ -58,7 +61,9 @@ let _ =
      [[Gramext.Stoken ("INT", "")],
       Gramext.action r_of_string]]
 
-(** pp **)
+(**********************************************************************)
+(* Old ast printing                                                   *)
+(**********************************************************************)
 
 exception Non_closed_number
 
@@ -97,7 +102,7 @@ let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
 let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
 
 (**********************************************************************)
-(* Parsing via scopes                                                 *)
+(* Parsing Z via scopes                                               *)
 (**********************************************************************)
 
 open Libnames
@@ -135,24 +140,42 @@ let r_of_posint dloc n =
   else
     RRef (dloc, glob_R0)
 
-let check_required_module loc d =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-  if not (Library.library_is_loaded dir) then
-    user_err_loc (loc,"z_of_int",
-    str ("Cannot interpret numbers in Z without requiring first module "
-    ^(list_last d)))
-
 let r_of_int dloc z =
-  check_required_module dloc ["Coq";"Reals";"Rsyntax"];
   match z with
   | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
   | POS n -> r_of_posint dloc n 
 
-let _ = Symbols.declare_numeral_interpreter "R_scope" (r_of_int,None)
+(**********************************************************************)
+(* Printing R via scopes                                              *)
+(**********************************************************************)
+
+let rec bignat_of_r = function
+  | RApp (_,RRef (_,p), [RRef (_,o); a]) when p = glob_Rplus & o = glob_R1
+      -> add_1 (bignat_of_r a)
+  | RRef (_,a) when a = glob_R1 -> Bignat.one
+  | RRef (_,a) when a = glob_R0 -> Bignat.zero
+  | _ -> raise Non_closed_number
+
+let bigint_of_r = function
+  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
+  | a -> POS (bignat_of_r a)
+
+let uninterp_r p =
+  try
+    Some (bigint_of_r p)
+  with Non_closed_number ->
+    None
+
+let _ = Symbols.declare_numeral_interpreter "R_scope"
+  ["Coq";"Reals";"Rsyntax"]
+  (r_of_int,None)
+  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
+    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_R1)],
+    uninterp_r,
+    None)
 
 (***********************************************************************)
-(* Printers *)
+(* Old ast printers via scope *)
 
 exception Non_closed_number
 
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 7b3c3e391..a3adabd62 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -17,6 +17,10 @@ open Ast
 open Extend
 open Topconstr
 open Libnames
+open Bignat
+
+(**********************************************************************)
+(* Parsing via Grammar *)
 
 let get_z_sign loc =
   let mkid id =
@@ -29,8 +33,6 @@ let get_z_sign loc =
     mkid (id_of_string "POS"),
     mkid (id_of_string "NEG")))
 
-open Bignat
-
 let pos_of_bignat xI xO xH x =
   let rec pos_of x =
     match div2_with_rest x with
@@ -50,7 +52,29 @@ let z_of_string pos_or_neg s dloc =
       mkAppC (aNEG, [pos_of_bignat xI xO xH v])
   else 
     aZERO
-      
+
+(* Declare the primitive parser with Grammar and without the scope mechanism *)
+open Pcoq
+
+let number = create_constr_entry (get_univ "znatural") "number" 
+
+let negnumber = create_constr_entry (get_univ "znatural") "negnumber"
+ 
+let _ =
+  Gram.extend number None
+    [None, None,
+     [[Gramext.Stoken ("INT", "")],
+      Gramext.action (z_of_string true)]]
+    
+let _ =
+  Gram.extend negnumber None
+    [None, None,
+     [[Gramext.Stoken ("INT", "")],
+      Gramext.action (z_of_string false)]]
+
+(**********************************************************************)
+(* Old ast printing *)
+
 exception Non_closed_number
 
 let get_z_sign_ast loc =
@@ -114,27 +138,8 @@ let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false))
 let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))
 let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
 
-(* Declare the primitive parser with Grammar and without the scope mechanism *)
-open Pcoq
-
-let number = create_constr_entry (get_univ "znatural") "number" 
-
-let negnumber = create_constr_entry (get_univ "znatural") "negnumber"
- 
-let _ =
-  Gram.extend number None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action (z_of_string true)]]
-    
-let _ =
-  Gram.extend negnumber None
-    [None, None,
-     [[Gramext.Stoken ("INT", "")],
-      Gramext.action (z_of_string false)]]
-
 (**********************************************************************)
-(* Parsing via scopes                                                 *)
+(* Parsing positive via scopes                                        *)
 (**********************************************************************)
 
 open Libnames
@@ -145,12 +150,6 @@ let fast_integer_module = make_dir ["Coq";"ZArith";"fast_integer"]
 (* TODO: temporary hack *)
 let make_path dir id = Libnames.encode_kn dir id
 
-let z_path = make_path fast_integer_module (id_of_string "Z")
-let glob_z = IndRef (z_path,0)
-let glob_ZERO = ConstructRef ((z_path,0),1)
-let glob_POS = ConstructRef ((z_path,0),2)
-let glob_NEG = ConstructRef ((z_path,0),3)
-
 let positive_path = make_path fast_integer_module (id_of_string "positive")
 let glob_xI = ConstructRef ((positive_path,0),1)
 let glob_xO = ConstructRef ((positive_path,0),2)
@@ -168,35 +167,92 @@ let pos_of_bignat dloc x =
   in 
   pos_of x
 
-let z_of_string2 dloc pos_or_neg n = 
+let interp_positive dloc = function
+  | POS n -> pos_of_bignat dloc n
+  | NEG n ->
+      user_err_loc (dloc, "interp_positive",
+        str "No negative number in type \"positive\"!")
+
+(**********************************************************************)
+(* Printing positive via scopes                                       *)
+(**********************************************************************)
+
+let rec bignat_of_pos = function
+  | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
+  | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | RRef (_, a) when a = glob_xH -> Bignat.one
+  | _ -> raise Non_closed_number
+
+let uninterp_positive p =
+  try 
+    Some (POS (bignat_of_pos p))
+  with Non_closed_number -> 
+    None
+
+(***********************************************************************)
+(* Declaring interpreters and uninterpreters for positive *)
+(***********************************************************************)
+
+let _ = Symbols.declare_numeral_interpreter "positive_scope"
+  ["Coq";"ZArith";"Zsyntax"]
+  (interp_positive,None)
+  ([RRef (dummy_loc, glob_xI); 
+    RRef (dummy_loc, glob_xO); 
+    RRef (dummy_loc, glob_xH)],
+   uninterp_positive,
+   None)
+
+(**********************************************************************)
+(* Parsing Z via scopes                                               *)
+(**********************************************************************)
+
+let z_path = make_path fast_integer_module (id_of_string "Z")
+let glob_z = IndRef (z_path,0)
+let glob_ZERO = ConstructRef ((z_path,0),1)
+let glob_POS = ConstructRef ((z_path,0),2)
+let glob_NEG = ConstructRef ((z_path,0),3)
+
+let z_of_posint dloc pos_or_neg n = 
   if is_nonzero n then
     let sgn = if pos_or_neg then glob_POS else glob_NEG in
     RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
   else 
     RRef (dloc, glob_ZERO)
 
-let check_required_module loc d =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-  if not (Library.library_is_loaded dir) then
-    user_err_loc (loc,"z_of_int",
-    str ("Cannot interpret numbers in Z without requiring first module "
-    ^(list_last d)))
-
 let z_of_int dloc z =
-  check_required_module dloc ["Coq";"ZArith";"Zsyntax"];
   match z with
-  | POS n -> z_of_string2 dloc true n 
-  | NEG n -> z_of_string2 dloc false n 
+  | POS n -> z_of_posint dloc true n 
+  | NEG n -> z_of_posint dloc false n 
 
-let _ = Symbols.declare_numeral_interpreter "Z_scope" (z_of_int,None)
+(**********************************************************************)
+(* Printing Z via scopes                                              *)
+(**********************************************************************)
 
-(***********************************************************************)
-(* Printer for positive *)
+let bigint_of_z = function
+  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> POS (bignat_of_pos a)
+  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> NEG (bignat_of_pos a)
+  | RRef (_, a) when a = glob_ZERO -> POS (Bignat.zero)
+  | _ -> raise Non_closed_number
 
+let uninterp_z p =
+  try
+    Some (bigint_of_z p)
+  with Non_closed_number -> None
 
 (***********************************************************************)
-(* Printers *)
+(* Declaring interpreters and uninterpreters for Z *)
+
+let _ = Symbols.declare_numeral_interpreter "Z_scope"
+  ["Coq";"ZArith";"Zsyntax"]
+  (z_of_int,None)
+  ([RRef (dummy_loc, glob_ZERO); 
+    RRef (dummy_loc, glob_POS); 
+    RRef (dummy_loc, glob_NEG)],
+  uninterp_z,
+  None)
+   
+(***********************************************************************)
+(* Old ast Printers *)
 
 exception Non_closed_number