Automatisation de l'utilisation de token primitifs dans les motifs de filtrage

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

3 files changed, 15 insertions, 71 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 073a689167..9bf6de0f50 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -51,19 +51,6 @@ let nat_of_int dloc n =
       user_err_loc (dloc, "nat_of_int",
         str "Cannot interpret a negative number as a number of type nat")
 
-let pat_nat_of_int dloc n name =
-  if is_pos_or_zero n then
-      let rec mk_nat n name =
-	if n <> zero then 
-	  PatCstr (dloc,path_of_S,[mk_nat (sub_1 n) Anonymous],name)
-	else 
-	  PatCstr (dloc,path_of_O,[],name)
-      in 
-      mk_nat n name
-  else
-      user_err_loc (dloc, "pat_nat_of_int",
-        str "Unable to interpret a negative number in type nat")
-
 (************************************************************************)
 (* Printing via scopes *)
 
@@ -80,24 +67,11 @@ let uninterp_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 (int_of_nat_pattern p)
-  with
-    Non_closed_number -> None
-
 (************************************************************************)
 (* Declare the primitive parsers and printers *)
 
 let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (glob_nat,["Coq";"Init";"Datatypes"])
-    (nat_of_int,Some pat_nat_of_int)
-    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], 
-     uninterp_nat, Some uninterp_nat_pattern)
+    nat_of_int
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true)
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index fb5be28968..3cfa3f1040 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -111,8 +111,9 @@ let uninterp_r p =
 
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (glob_R,["Coq";"Reals";"Rdefinitions"])
-  (r_of_int,None)
+  r_of_int
   ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
-    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
+    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);
+    RRef(dummy_loc,glob_R1)],
     uninterp_r,
-    None)
+    false)
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 9f4bba335b..c4983c7cda 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -60,19 +60,6 @@ let interp_positive dloc n =
   if is_strictly_pos n then pos_of_bignat dloc n
   else error_non_positive dloc
 
-let rec pat_pos_of_bignat dloc x name =
-  match div2_with_rest x with
-    | (q,false) -> 
-        PatCstr (dloc,path_of_xO,[pat_pos_of_bignat dloc q Anonymous],name)
-    | (q,true) when q <> zero -> 
-        PatCstr (dloc,path_of_xI,[pat_pos_of_bignat dloc q Anonymous],name)
-    | (q,true) ->
-        PatCstr (dloc,path_of_xH,[],name)
-
-let pat_interp_positive dloc n =
-  if is_strictly_pos n then pat_pos_of_bignat dloc n else
-    error_non_positive dloc
-
 (**********************************************************************)
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
@@ -95,12 +82,12 @@ let uninterp_positive p =
 
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (glob_positive,positive_module)
-  (interp_positive,Some pat_interp_positive)
-  ([RRef (dummy_loc, glob_xI); 
+  interp_positive
+  ([RRef (dummy_loc, glob_xI);
     RRef (dummy_loc, glob_xO); 
     RRef (dummy_loc, glob_xH)],
    uninterp_positive,
-   None)
+   true)
 
 (**********************************************************************)
 (* Parsing N via scopes                                               *)
@@ -114,7 +101,7 @@ let path_of_Npos = ((n_path,0),2)
 let glob_N0 = ConstructRef path_of_N0
 let glob_Npos = ConstructRef path_of_Npos
 
-let n_of_posint dloc pos_or_neg n = 
+let n_of_binnat dloc pos_or_neg n = 
   if n <> zero then
     RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
   else 
@@ -124,17 +111,7 @@ let error_negative dloc =
   user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"")
 
 let n_of_int dloc n =
-  if is_pos_or_zero n then n_of_posint dloc true n
-  else error_negative dloc
-
-let pat_n_of_binnat dloc n name = 
-  if n <> zero then
-    PatCstr (dloc, path_of_Npos, [pat_pos_of_bignat dloc n Anonymous], name)
-  else 
-    PatCstr (dloc, path_of_N0, [], name)
-
-let pat_n_of_int dloc n name =
-  if is_pos_or_zero n then pat_n_of_binnat dloc n name
+  if is_pos_or_zero n then n_of_binnat dloc true n
   else error_negative dloc
 
 (**********************************************************************)
@@ -155,11 +132,11 @@ let uninterp_n p =
 
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (glob_n,binnat_module)
-  (n_of_int,Some pat_n_of_int)
+  n_of_int
   ([RRef (dummy_loc, glob_N0); 
     RRef (dummy_loc, glob_Npos)],
   uninterp_n,
-  None)
+  true)
    
 (**********************************************************************)
 (* Parsing Z via scopes                                               *)
@@ -183,14 +160,6 @@ let z_of_int dloc n =
   else 
     RRef (dloc, glob_ZERO)
 
-let pat_z_of_int dloc n name = 
-  if n <> zero then
-    let sgn,n =
-      if is_pos_or_zero n then path_of_POS, n else path_of_NEG, Bigint.neg n in
-    PatCstr (dloc, sgn, [pat_pos_of_bignat dloc n Anonymous], name)
-  else 
-    PatCstr (dloc, path_of_ZERO, [], name)
-
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
@@ -211,9 +180,9 @@ let uninterp_z p =
 
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (glob_z,fast_integer_module)
-  (z_of_int,Some pat_z_of_int)
+  z_of_int
   ([RRef (dummy_loc, glob_ZERO); 
     RRef (dummy_loc, glob_POS); 
     RRef (dummy_loc, glob_NEG)],
   uninterp_z,
-  None)
+  true)