Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de chaîne de caractères tel que "foo"

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

4 files changed, 22 insertions, 16 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 37dc007ee0..336f741aec 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -70,7 +70,7 @@ let make_constr_action
 	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CNumeral (dummy_loc,v)) :: env) tl)
+	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:constr_expr list) ->
           let dummyid = Ident (dummy_loc,id_of_string "") in
@@ -96,7 +96,7 @@ let make_cases_pattern_action
 	  make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CPatNumeral (dummy_loc,v)) :: env) tl)
+	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
           let dummyid = Ident (dummy_loc,id_of_string "") in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1f84221113..6208952d32 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -180,7 +180,7 @@ GEXTEND Gram
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
-              CNumeral(_,z) when Bigint.is_pos_or_zero z ->
+              CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",[c])
             | _ -> c) ] ]
   ;
@@ -218,8 +218,9 @@ GEXTEND Gram
   ;
   atomic_constr:
     [ [ g=global -> CRef g
-      | s=sort -> CSort(loc,s)
-      | n=INT -> CNumeral (loc, Bigint.of_string n)
+      | s=sort -> CSort (loc,s)
+      | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
+      | s=string -> CPrim (loc, String s)
       | "_" -> CHole loc
       | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
@@ -294,10 +295,11 @@ GEXTEND Gram
       | "_" -> CPatAtom (loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
-              CPatNumeral(_,z) when Bigint.is_pos_or_zero z ->
+              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CPatNotation(loc,"( _ )",[p])
             | _ -> p)
-      | n = INT -> CPatNumeral (loc, Bigint.of_string n) ] ]
+      | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
+      | s = string -> CPatPrim (loc, String s) ] ]
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index d80cc5ec36..073a689167 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -99,4 +99,5 @@ 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, None)
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], 
+     uninterp_nat, Some uninterp_nat_pattern)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 36470c13dc..2f2f0773b4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -19,6 +19,7 @@ open Ppextend
 open Topconstr
 open Term
 open Pattern
+open Rawterm
 (*i*)
 
 let sep_p = fun _ -> str"."
@@ -54,6 +55,10 @@ let prec_less child (parent,assoc) =
       | Prec n -> child<=n
       | Any -> true
 
+let prec_of_prim_token = function
+  | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+  | String _ -> latom
+
 let env_assoc_value v env =
   try List.nth env (v-1)
   with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
@@ -104,8 +109,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-open Rawterm
-
 let pr_opt pr = function
   | None -> mt ()
   | Some x -> spc() ++ pr x
@@ -157,6 +160,10 @@ let pr_or_var pr = function
   | Genarg.ArgArg x -> pr x
   | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
 
+let pr_prim_token = function
+  | Numeral n -> Bigint.pr_bigint n
+  | String s -> qs s
+
 let las = lapp
 let lpator = 100
 
@@ -174,7 +181,7 @@ let rec pr_patt sep inh p =
   | CPatNotation (_,"( _ )",[p]) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
   | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
-  | CPatNumeral (_,i) -> Bigint.pr_bigint i, latom
+  | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
   let loc = cases_pattern_loc p in
@@ -566,9 +573,7 @@ let rec pr sep inherited a =
   | CNotation (_,"( _ )",[t]) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
-  | CNumeral (_,p) ->
-      Bigint.pr_bigint p, 
-      (if Bigint.is_pos_or_zero p then lposint else lnegint)
+  | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
   | CDynamic _ -> str "<dynamic>", latom
   in
@@ -666,8 +671,6 @@ let pr_unfold_occ pr_ref = function
 
 let pr_qualid qid = str (string_of_qualid qid)
 
-open Rawterm
-
 let pr_arg pr x = spc () ++ pr x
 
 let pr_red_flag pr r =