Merge PR #11650: Set Printing Parens

Reviewed-by: ejgallego

16 files changed, 92 insertions, 24 deletions

diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst
new file mode 100644
index 0000000000..5e2da594c6
--- /dev/null
+++ b/doc/changelog/03-notations/11650-parensNew.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  added option Set Printing Parentheses to print parentheses even when implied by associativity or precedence.
+  (`#11650 <https://github.com/coq/coq/pull/11650>`_,
+  by Hugo Herbelin and Abhishek Anand).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8bfcab0f4e..c568f13c12 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -396,6 +396,11 @@ Displaying information about notations
    Controls whether to use notations for printing terms wherever possible.
    Default is on.
 
+.. flag:: Printing Parentheses
+
+   If on, parentheses are printed even if implied by associativity and precedence
+   Default is off.
+
 .. seealso::
 
    :flag:`Printing All`
diff --git a/ide/coq.ml b/ide/coq.ml
index 0c6aef0305..5b66cb745e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -558,6 +558,7 @@ struct
     { opts = [raw_matching]; init = true;
       label = "Display raw _matching expressions" };
     { opts = [notations]; init = true; label = "Display _notations" };
+    { opts = [notations]; init = true; label = "Display _parentheses" };
     { opts = [all_basic]; init = false;
       label = "Display _all basic low-level contents" };
     { opts = [existential]; init = false;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index f22821c6ea..e9ff1bbba1 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -79,6 +79,7 @@ let init () =
 \n    <menuitem action='Display coercions' />\
 \n    <menuitem action='Display raw matching expressions' />\
 \n    <menuitem action='Display notations' />\
+\n    <menuitem action='Display parentheses' />\
 \n    <menuitem action='Display all basic low-level contents' />\
 \n    <menuitem action='Display existential variable instances' />\
 \n    <menuitem action='Display universe levels' />\
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 60036ef876..9eb0b972b6 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -49,6 +49,7 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Matching"];
   ["Printing";"Synth"];
   ["Printing";"Notations"];
+  ["Printing";"Parentheses"];
   ["Printing";"All"];
   ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4ec9f17c71..44aacd62d8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -57,6 +57,10 @@ let print_implicits_defensive = ref true
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
+(* This forces printing of parentheses even when
+   it is implied by associativity/precedence *)
+let print_parentheses = Notation_ops.print_parentheses
+
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index fa263cbeb7..0eca287c1d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -53,6 +53,7 @@ val print_implicits_defensive : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
+val print_parentheses : bool ref
 val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 59a58d643c..8f47e9276b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -258,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x =
 (******************************************************************************)
 (* Translating a glob_constr into a notation, interpreting recursive patterns *)
 
+let print_parentheses = ref false
+
 type found_variables = {
     vars : Id.t list;
     recursive_term_vars : (Id.t * Id.t) list;
@@ -1092,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
       let rest = Id.List.assoc ldots_var terms in
       let t = Id.List.assoc y terms in
       let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
+      if !print_parentheses && not (List.is_empty acc) then raise No_match;
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 2ab8b620df..0ef51b65a2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -61,6 +61,8 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
 
 exception No_match
 
+val print_parentheses : bool ref
+
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
       ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
       ('a cases_pattern_disjunction_g * extended_subscopes) list *
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 393ab8a302..bb6693a239 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -38,9 +38,9 @@ let ppcmd_of_cut = function
   | PpBrk(n1,n2) -> brk(n1,n2)
 
 type unparsing =
-  | UnpMetaVar of entry_relative_level
+  | UnpMetaVar of entry_relative_level * Extend.side option
   | UnpBinderMetaVar of entry_relative_level
-  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
@@ -50,9 +50,9 @@ type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
-  | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
   | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
-  | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2
   | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
   | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 346fc83f5f..18e48942c6 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -30,9 +30,9 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of entry_relative_level
+  | UnpMetaVar of entry_relative_level * Extend.side option
   | UnpBinderMetaVar of entry_relative_level
-  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c2d760ae08..59972f8bdb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -85,6 +85,7 @@ let tag_var = tag Tag.variable
     let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in
     let pop r = let a = List.hd !r in r := List.tl !r; a in
     let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in
+    let parens = !Constrextern.print_parentheses in
     (* Warning:
        The following function enforces a very precise order of
        evaluation of sub-components.
@@ -92,19 +93,19 @@ let tag_var = tag Tag.variable
     let rec aux = function
       | [] ->
         mt ()
-      | UnpMetaVar prec as unp :: l ->
+      | UnpMetaVar (prec, side) as unp :: l ->
         let c = pop env in
         let pp2 = aux l in
-        let pp1 = pr prec c in
+        let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in
         return unp pp1 pp2
       | UnpBinderMetaVar prec as unp :: l ->
         let c = pop bl in
         let pp2 = aux l in
         let pp1 = pr_patt prec c in
         return unp pp1 pp2
-      | UnpListMetaVar (prec, sl) as unp :: l ->
+      | UnpListMetaVar (prec, sl, side) as unp :: l ->
         let cl = pop envlist in
-        let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in
+        let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens && side <> None then LevelLe 0 else prec)) cl in
         let pp2 = aux l in
         return unp pp1 pp2
       | UnpBinderListMetaVar (isopen, sl) as unp :: l ->
diff --git a/test-suite/output/PrintingParentheses.out b/test-suite/output/PrintingParentheses.out
new file mode 100644
index 0000000000..a5874f09a7
--- /dev/null
+++ b/test-suite/output/PrintingParentheses.out
@@ -0,0 +1,28 @@
+((1 + (2 * 3), 4), 5)
+     : (nat * nat) * nat
+mult_n_Sm = 
+fun n m : nat =>
+nat_ind (fun n0 : nat => ((n0 * m) + n0) = (n0 * (S m))) eq_refl
+  (fun (p : nat) (H : ((p * m) + p) = (p * (S m))) =>
+   let n0 := p * (S m) in
+   match H in (_ = y) return (((m + (p * m)) + (S p)) = (S (m + y))) with
+   | eq_refl =>
+       eq_ind (S ((m + (p * m)) + p))
+         (fun n1 : nat => n1 = (S (m + ((p * m) + p))))
+         (eq_S ((m + (p * m)) + p) (m + ((p * m) + p))
+            (nat_ind
+               (fun n1 : nat => ((n1 + (p * m)) + p) = (n1 + ((p * m) + p)))
+               eq_refl
+               (fun (n1 : nat)
+                  (H0 : ((n1 + (p * m)) + p) = (n1 + ((p * m) + p))) =>
+                f_equal_nat nat S ((n1 + (p * m)) + p) 
+                  (n1 + ((p * m) + p)) H0) m)) ((m + (p * m)) + (S p))
+         (plus_n_Sm (m + (p * m)) p)
+   end) n
+     : forall n m : nat, ((n * m) + n) = (n * (S m))
+
+Arguments mult_n_Sm (_ _)%nat_scope
+1 :: (2 :: [3; 4])
+     : list nat
+{0 = 1} + {2 <= (4 + 5)}
+     : Set
diff --git a/test-suite/output/PrintingParentheses.v b/test-suite/output/PrintingParentheses.v
new file mode 100644
index 0000000000..190e122e2f
--- /dev/null
+++ b/test-suite/output/PrintingParentheses.v
@@ -0,0 +1,10 @@
+Set Printing Parentheses.
+
+Check (1+2*3,4,5).
+Print mult_n_Sm.
+
+Require Import List.
+Import ListNotations.
+Check [1;2;3;4].
+
+Check {0=1}+{2<=4+5}.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index afff0347f5..3937f887ad 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -294,15 +294,15 @@ let precedence_of_position_and_level from_level = function
      | RightA, Right -> LevelLe n
      | LeftA, Left -> LevelLe n
      | LeftA, Right -> LevelLt n
-     | NonA, _ -> LevelLt n)
-  | NumLevel n, _ -> LevelLe n
-  | NextLevel, _ -> LevelLt from_level
-  | DefaultLevel, _ -> LevelSome
+     | NonA, _ -> LevelLt n), Some b
+  | NumLevel n, _ -> LevelLe n, None
+  | NextLevel, _ -> LevelLt from_level, None
+  | DefaultLevel, _ -> LevelSome, None
 
 (** Computing precedences of subentries for parsing *)
 let precedence_of_entry_type (from_custom,from_level) = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
-    precedence_of_position_and_level from_level x
+    fst (precedence_of_position_and_level from_level x)
   | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
   | ETConstr (custom,_,(NextLevel,_)) ->
     user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
@@ -323,9 +323,9 @@ let unparsing_precedence_of_entry_type from_level = function
     (* Precedence of printing for a custom entry is managed using
        explicit insertion of entry coercions at the time of building
        a [constr_expr] *)
-    LevelSome
-  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
-  | _ -> LevelSome (* should not matter *)
+    LevelSome, None
+  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0), None
+  | _ -> LevelSome, None (* should not matter *)
 
 (* Some breaking examples *)
 (* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -392,10 +392,10 @@ let check_open_binder isopen sl m =
 
 let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
-  let prec = unparsing_precedence_of_entry_type from x in
+  let prec,side = unparsing_precedence_of_entry_type from x in
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
-     UnpMetaVar prec
+     UnpMetaVar (prec,side)
   | ETPattern _ ->
      UnpBinderMetaVar prec
   | ETIdent ->
@@ -446,14 +446,14 @@ let make_hunks etyps symbols from_level =
     | SProdList (m,sl) :: prods ->
         let i = index_id m vars in
         let typ = List.nth typs (i-1) in
-        let prec = unparsing_precedence_of_entry_type from_level typ in
+        let prec,side = unparsing_precedence_of_entry_type from_level typ in
         let sl' =
           (* If no separator: add a break *)
           if List.is_empty sl then add_break 1 []
           (* We add NonTerminal for simulation but remove it afterwards *)
           else make true sl in
         let hunk = match typ with
-          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
+          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl',side)
           | ETBinder isopen ->
               check_open_binder isopen sl m;
               UnpBinderListMetaVar (isopen,List.map snd sl')
@@ -589,13 +589,13 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
   | SProdList (m,sl) :: symbs, fmt when has_ldots fmt ->
       let i = index_id m vars in
       let typ = List.nth typs (i-1) in
-      let prec = unparsing_precedence_of_entry_type from_level typ in
+      let prec,side = unparsing_precedence_of_entry_type from_level typ in
       let loc_slfmt,rfmt = read_recursive_format sl fmt in
       let sl, slfmt = aux (sl,loc_slfmt) in
       if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
       let symbs, l = aux (symbs,rfmt) in
       let hunk = match typ with
-        | ETConstr _ -> UnpListMetaVar (prec,slfmt)
+        | ETConstr _ -> UnpListMetaVar (prec,slfmt,side)
         | ETBinder isopen ->
             check_open_binder isopen sl m;
             UnpBinderListMetaVar (isopen,slfmt)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63fc587f71..2eb1aa39b0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1282,6 +1282,13 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
+      optkey   = ["Printing";"Parentheses"];
+      optread  = (fun () -> !Constrextern.print_parentheses);
+      optwrite = (fun b ->  Constrextern.print_parentheses := b) }
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
       optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Detyping.print_evar_arguments);
       optwrite = (:=) Detyping.print_evar_arguments }