Merge PR #13840: [notation] option to fine tune printing of literals

Reviewed-by: SkySkimmer
Ack-by: jfehrle

8 files changed, 123 insertions, 11 deletions

diff --git a/doc/changelog/03-notations/13840-print-prim.rst b/doc/changelog/03-notations/13840-print-prim.rst
new file mode 100644
index 0000000000..d6e3184662
--- /dev/null
+++ b/doc/changelog/03-notations/13840-print-prim.rst
@@ -0,0 +1,11 @@
+- **Changed:**
+  Flag :flag:`Printing Notations` no longer controls
+  whether strings and numbers are printed raw
+  (`#13840 <https://github.com/coq/coq/pull/13840>`_,
+  by Enrico Tassi).
+
+- **Added:**
+  Flag :flag:`Printing Raw Literals` to control whether
+  strings and numbers are printed raw.
+  (`#13840 <https://github.com/coq/coq/pull/13840>`_,
+  by Enrico Tassi).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 557ef10555..453e878a5d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -442,6 +442,12 @@ Displaying information about notations
    Controls whether to use notations for printing terms wherever possible.
    Default is on.
 
+.. flag:: Printing Raw Literals
+
+   Controls whether to use string and number notations for printing terms
+   wherever possible (see :ref:`string-notations`).
+   Default is off.
+
 .. flag:: Printing Parentheses
 
    If on, parentheses are printed even if implied by associativity and precedence
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4fb7861ca6..3cabf52197 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -64,7 +64,7 @@ let print_parentheses = Notation_ops.print_parentheses
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
 
-(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
+(* This suppresses printing of notations *)
 let print_no_symbol = ref false
 
 (* This tells to skip types if a variable has this type by default *)
@@ -74,6 +74,9 @@ let print_use_implicit_types =
     ~key:["Printing";"Use";"Implicit";"Types"]
     ~value:true
 
+(* Print primitive tokens, like strings *)
+let print_raw_literal = ref false
+
 (**********************************************************************)
 
 let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
@@ -434,7 +437,7 @@ let extern_record_pattern cstrsp args =
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
-    if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
+    if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
     let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
@@ -853,6 +856,7 @@ let same_binder_type ty nal c =
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token (custom,scopes) r =
+   if !print_raw_literal then raise No_match;
    let (n,key) = uninterp_prim_token r scopes in
    match availability_of_entry_coercion custom InConstrEntrySomeLevel with
    | None -> raise No_match
@@ -1261,11 +1265,12 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   make ?loc (pll,extern inctx scopes vars c)
 
 and extern_notations inctx scopes vars nargs t =
-  if !Flags.raw_print || !print_no_symbol then raise No_match;
+  if !Flags.raw_print then raise No_match;
   try extern_possible_prim_token scopes t
   with No_match ->
-  let t = flatten_application t in
-  extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+    if !print_no_symbol then raise No_match;
+    let t = flatten_application t in
+    extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
 
 and extern_notation inctx (custom,scopes as allscopes) vars t rules =
   match rules with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 298b52f0be..bb49c8697d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -60,6 +60,7 @@ val print_parentheses : bool ref
 val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
+val print_raw_literal : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 60213cab0c..cc9e745f6b 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -6,7 +6,7 @@
      : nat * nat * (nat * nat)
 (0, 2, (2, 2))
      : nat * nat * (nat * nat)
-pair (pair O (S (S O))) (pair (S (S O)) O)
+pair (pair 0 2) (pair 2 0)
      : prod (prod nat nat) (prod nat nat)
 << 0, 2, 4 >>
      : nat * nat * nat * (nat * (nat * nat))
@@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O)
      : nat * nat * nat * (nat * (nat * nat))
 (0, 2, 4, (0, (2, 4)))
      : nat * nat * nat * (nat * (nat * nat))
-pair (pair (pair O (S (S O))) (S (S (S (S O)))))
-  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+pair (pair (pair 0 2) 4) (pair 4 (pair 2 0))
      : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
 ETA x y : nat, Nat.add
      : nat -> nat -> nat
@@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t
      : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) *
        (nat * nat * nat)
 pair
-  (pair
-     (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O)))
-     (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O)))
+  (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0)))
+  (pair (pair 0 1) 2)
      : prod
          (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out
new file mode 100644
index 0000000000..afe9b25442
--- /dev/null
+++ b/test-suite/output/primitive_tokens.out
@@ -0,0 +1,61 @@
+"foo"
+     : string
+1234
+     : nat
+Nat.add 1 2
+     : nat
+match "a" with
+| "a" => true
+| _ => false
+end
+     : bool
+match 1 with
+| 1 => true
+| _ => false
+end
+     : bool
+{| field := 7 |}
+     : test
+String (Ascii.Ascii false true true false false true true false)
+  (String (Ascii.Ascii true true true true false true true false)
+     (String (Ascii.Ascii true true true true false true true false)
+        EmptyString))
+     : string
+S
+  (S
+     (S
+        (S
+           (S
+              (S
+                 (S
+                    (S
+                       (S
+                          (S
+                             (S
+                                (S
+                                   (S
+                                      (S
+                                         (S
+                                            (S
+                                               (S
+                                                 (S
+                                                 (S (S (S (S (S (S ...)))))))))))))))))))))))
+     : nat
+Nat.add (S O) (S (S O))
+     : nat
+match
+  String (Ascii.Ascii true false false false false true true false)
+    EmptyString
+with
+| String (Ascii.Ascii true false false false false true true false)
+  EmptyString => true
+| _ => false
+end
+     : bool
+match S O with
+| S O => true
+| _ => false
+end
+     : bool
+{| field := S (S (S (S (S (S (S O)))))) |}
+     : test
diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v
new file mode 100644
index 0000000000..3207e5983f
--- /dev/null
+++ b/test-suite/output/primitive_tokens.v
@@ -0,0 +1,23 @@
+Require Import String.
+
+Record test := { field : nat }.
+
+Open Scope string_scope.
+
+Unset Printing Notations.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
+
+Set Printing Raw Literals.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 38ca836b32..e8d84a67a3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1568,6 +1568,13 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
+      optkey   = ["Printing";"Raw";"Literals"];
+      optread  = (fun () -> !Constrextern.print_raw_literal);
+      optwrite = (fun b ->  Constrextern.print_raw_literal := b) }
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
       optkey   = ["Printing";"All"];
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }