Printing for if <term> is <pattern> then _ else _ syntax

.gitlab-ci.yml

@@ -1229,12 +1229,6 @@ plugin:ci-paramcoq:
   - build:edge+flambda
   - library:ci-stdlib+flambda
 
-plugin:ci-perennial:
-  extends: .ci-template-flambda
-  needs:
-  - build:edge+flambda
-  - library:ci-stdlib+flambda
-
 plugin:plugin-tutorial:
   stage: build-0
   interruptible: true

Makefile.ci

@@ -164,8 +164,6 @@ ci-compcert: ci-menhir ci-flocq
 
 ci-paramcoq: ci-stdlib
 
-ci-perennial: ci-stdlib
-
 ci-aac_tactics: ci-stdlib
 ci-relation_algebra: ci-aac_tactics ci-mathcomp
 

dev/ci/ci-basic-overlay.sh

@@ -123,8 +123,7 @@ project corn "https://github.com/coq-community/corn" "master"
 # NB: stdpp and Iris refs are gotten from the opam files in the Iris and
 # iris_examples repos respectively. So just getting a fix landed in stdpp or
 # Iris is not enough. Ping @RalfJung and @robbertkrebbers if you need the
-# versions of stdpp or Iris to be bumped. Perennial also has its own pinned
-# versions of stdpp and Iris; ping @tchajed and @zeldovich to get that bumped.
+# versions of stdpp or Iris to be bumped.
 project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" ""
 # Contact @RalfJung, @robbertkrebbers on github
 
@@ -440,16 +439,6 @@ project argosy "https://github.com/mit-pdos/argosy" "master"
 project atbr "https://github.com/coq-community/atbr" "master"
 # Contact @palmskog, @tchajed on github
 
-########################################################################
-# perennial
-########################################################################
-project perennial "https://github.com/mit-pdos/perennial" "coq/tested"
-# Contact @upamanyus, @tchajed on github
-# PRs to fix Perennial failures should be submitted against the Perennial
-# `master` branch. `coq/tested` is automatically updated every night to the
-# `master` branch if CI on `master` is green. This is to avoid breaking Coq CI
-# when Perennial CI breaks.
-
 ########################################################################
 # metarocq
 ########################################################################

dev/ci/user-overlays/22124-proux01-if-printing.sh

@@ -0,0 +1,2 @@
+overlay hott https://github.com/proux01/HoTT rocq22124 22124
+overlay mtac2 https://github.com/proux01/Mtac2 rocq22124 22124

doc/changelog/02-specification-language/21611-if-is.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  new syntactic sugar `if g is c then t else e`
+  for `match g with c => t | _ => e end`. This adds the
+  new reserved keyword `is`
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  by Pierre Roux).

doc/changelog/02-specification-language/22124-if-printing-Removed.rst

@@ -0,0 +1,4 @@
+- **Removed:**
+  table ``Printing If``
+  (`#22124 <https://github.com/rocq-prover/rocq/pull/22124>`_,
+  by Pierre Roux).

doc/sphinx/language/core/basic.rst

@@ -189,7 +189,7 @@ Keywords
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
     SProp Set Theorem Type Variable as at cofix else end
-    fix for forall fun if in let match of return then where with
+    fix for forall fun if in is let match of return then where with
 
   The following are keywords defined in notations or plugins loaded in the :term:`prelude`::
 

doc/sphinx/language/extensions/match.rst

@@ -34,10 +34,13 @@ is often not successful and prints the expanded form.
 Pattern-matching on boolean values: the if expression
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. insertprodn term_if term_if
+.. insertprodn term_if if_else
 
 .. prodn::
    term_if ::= if @term {? {? as @name } return @term100 } then @term else @term
+   | if @term is @if_dthen @if_else
+   if_dthen ::= @pattern {? in @pattern } {? return @term100 } then @term
+   if_else ::= else @term
 
 For inductive types with exactly two constructors and for pattern matching
 expressions that do not depend on the arguments of the constructors, it is possible
@@ -77,6 +80,9 @@ and :n:`@ident__2`, the following terms are equal:
 Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is
 declared as such (see :ref:`controlling-match-pp`).
 
+The `if g is c then t else e` syntax is syntactic sugar for `match g
+with c => t | _ => e end`.
+
 .. _irrefutable-patterns:
 
 Irrefutable patterns: the destructuring let variants
@@ -313,19 +319,6 @@ written using the :ref:`let-tuple syntax <let-tuple>`.
    Use the :cmd:`Add` and :cmd:`Remove` commands to update this set.
 
 
-Printing matching on booleans
-+++++++++++++++++++++++++++++
-
-If an inductive type is isomorphic to the boolean type, pattern matching
-can be written using ``if`` … ``then`` … ``else`` ….  This table controls
-which types are written this way:
-
-.. table:: Printing If @qualid
-
-   This :term:`table` specifies a set of qualids for which pattern matching is displayed using
-   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add` and :cmd:`Remove`
-   commands to update this set.
-
 This example emphasizes what the printing settings offer.
 
 .. example::
@@ -355,7 +348,7 @@ Printing regular match syntax
 
    When enabled, this flag makes printing avoid the alternate case
    analysis syntaxes (with :ref:`if <if-then-else>` and :ref:`let
-   <irrefutable-patterns>`), overriding :table:`Printing If` and
+   <irrefutable-patterns>`), overriding
    :table:`Printing Let` and disregarding the syntax used to input the
    case analysis (so e.g. `let 'tt := tt in tt` will be printed using `match`).
 

doc/tools/docgram/common.edit_mlg

@@ -264,6 +264,7 @@ term10: [
 | MOVETO term_forall_or_fun "fun" open_binders "=>" term200
 | MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200
 | MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200
+| MOVETO term_if "if" term200 "is" if_dthen if_else
 | MOVETO term_fix "let" "fix" fix_decl "in" term200
 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200

doc/tools/docgram/fullGrammar

@@ -109,6 +109,7 @@ term10: [
 | "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
 | "let" "'" pattern200 OPT [ "in" pattern200 ] ":=" term200 OPT case_type "in" term200
 | "if" term200 as_return_type "then" term200 "else" term200
+| "if" term200 "is" if_dthen if_else
 | "fix" fix_decls
 | "cofix" cofix_decls
 | term9
@@ -145,6 +146,14 @@ term0: [
 | "ltac" ":" "(" Pltac.ltac_expr ")"
 ]
 
+if_dthen: [
+| pattern200 OPT [ "in" pattern200 ] OPT case_type "then" lconstr
+]
+
+if_else: [
+| "else" lconstr
+]
+
 array_elems: [
 | LIST0 lconstr SEP ";"
 ]

doc/tools/docgram/orderedGrammar

@@ -369,6 +369,15 @@ cofix_body: [
 
 term_if: [
 | "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+| "if" term "is" if_dthen if_else
+]
+
+if_dthen: [
+| pattern OPT [ "in" pattern ] OPT ( "return" term100 ) "then" term
+]
+
+if_else: [
+| "else" term
 ]
 
 term_let: [

ide/rocqide/rocq_commands.ml

@@ -15,7 +15,6 @@ let commands = [
    "Add Field";
    "Add Morphism";
    "Add Printing Constructor";
-   "Add Printing If";
    "Add Printing Let";
    "Add Printing Record";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
@@ -94,7 +93,6 @@ let commands = [
    "Record";
    "Remark";
    "Remove Printing Constructor";
-   "Remove Printing If";
    "Remove Printing Let";
    "Remove Printing Record";
    "Require";
@@ -128,7 +126,6 @@ let commands = [
      "Syntactic Definition";
      "Syntax";];
   [
-   "Test Printing If";
    "Test Printing Let";
    "Test Printing Synth";
    "Test Printing Wildcard";
@@ -194,7 +191,6 @@ let state_preserving = [
   "Print Scopes.";
   "Print Section";
 
-  "Print Table Printing If.";
   "Print Table Printing Let.";
   "Print Tables.";
   "Print Term";
@@ -219,7 +215,6 @@ let state_preserving = [
   "Show Proof";
   "Show Tree";
 
-  "Test Printing If";
   "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";

parsing/g_constr.mlg

@@ -247,6 +247,9 @@ GRAMMAR EXTEND Gram
         "then"; b1 = term LEVEL "200";
         "else"; b2 = term LEVEL "200" ->
         { CAst.make ~loc @@ CIf (c, po, b1, b2) }
+      | "if"; c = term LEVEL "200"; "is"; db1 = if_dthen; b2 = if_else ->
+        { let b1, (na, t), rt = db1 in
+          CAst.make ~loc @@ CCases (IfStyle, rt, [c, na, t], [b1; b2]) }
       | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ]
     | "9"
@@ -288,6 +291,15 @@ GRAMMAR EXTEND Gram
       | "`("; c = term LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, c) } ] ]
   ;
+  if_dthen:
+    [ [ mp = pattern; t = OPT ["in"; t = pattern -> { t } ]; rt = OPT case_type; "then"; c = lconstr ->
+        { let ct = match t, rt with None, None -> None | _ -> aliasvar mp in
+          (CAst.make ~loc ([[mp]], c)), (ct, t), rt } ]]
+  ;
+  if_else:
+    [ [ mp = [ "else" -> { CAst.make ~loc @@ CPatAtom None } ]; c = lconstr ->
+        { CAst.make ~loc ([[mp]], c) } ]]
+  ;
   array_elems:
     [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]]
   ;

plugins/ssr/ssrvernac.mlg

@@ -43,15 +43,15 @@ IGNORE KEYWORDS
 
 (* global syntactic changes and vernacular commands *)
 
-(** Alternative notations for "match" and anonymous arguments. *)(* ************)
+(** Alternative notations for anonymous arguments. *)(* ************)
 
 (* Syntax:                                                        *)
 (*  let: <pattern> := <term> in ...                               *)
 (*  let: <pattern> [in ...] := <term> return ... in ...           *)
 (* The scope of a top-level 'as' in the pattern extends over the  *)
-(* 'return' type (dependent if/let).                              *)
+(* 'return' type (dependent let).                              *)
 (* Note that the optional "in ..." appears next to the <pattern>  *)
-(* rather than the <term> in then "let:" syntax. The alternative  *)
+(* rather than the <term> in the "let:" syntax. The alternative   *)
 (* would lead to ambiguities in, e.g.,                            *)
 (* let: p1 := (*v---INNER LET:---v *)                             *)
 (*   let: p2 := let: p3 := e3 in k return t in k2 in k1 return t' *)
@@ -62,9 +62,6 @@ IGNORE KEYWORDS
 (* display style -- why aren't these strings?); also, the v8.1    *)
 (* pretty-printer only allows extension hooks for printing        *)
 (* integer or string literals.                                    *)
-(*   Also note that in the v8 grammar "is" needs to be a keyword; *)
-(* as this can't be done from an ML extension file, the new       *)
-(* syntax will only work when ssreflect.v is imported.            *)
 
 let no_ct = None, None and no_rt = None
 let aliasvar = function

plugins/ssrrewrite/ssrrewrite.mlg

@@ -127,9 +127,7 @@ GRAMMAR EXTEND Gram
   ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
   ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
   term: LEVEL "10" [
-    [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
-      { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
-    | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
+    [ "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
       { let b1, ct, rt = db1 in
       let b1, b2 = let open CAst in
         let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in

pretyping/detyping.ml

@@ -222,39 +222,17 @@ let encode_inductive env r =
 
 (* Parameterization of the translation from constr to ast      *)
 
-(* Tables for Cases printing under a "if" form, a "let" form,  *)
-
-let has_two_constructors lc =
-  Int.equal (Array.length lc) 2 (* & lc.(0) = 0 & lc.(1) = 0 *)
+(* Table for Cases printing under a "let" form,  *)
 
 let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 
-let encode_bool env ({CAst.loc} as r) =
-  let (x,lc) = encode_inductive env r in
-  if not (has_two_constructors lc) then
-    user_err ?loc
-      (str "This type has not exactly two constructors.");
-  x
-
 let encode_tuple env ({CAst.loc} as r) =
   let (x,lc) = encode_inductive env r in
   if not (isomorphic_to_tuple lc) then
     user_err ?loc
       (str "This type cannot be seen as a tuple type.");
   x
 
-module PrintingCasesIf =
-  PrintingFlags.PrintingInductiveMake (struct
-    let encode = encode_bool
-    let field = "If"
-    let title = "Types leading to pretty-printing of Cases using a `if' form:"
-    let member_message s b =
-      str "Cases on elements of " ++ s ++
-      str
-        (if b then " are printed using a `if' form"
-         else " are not printed using a `if' form")
-  end)
-
 module PrintingCasesLet =
   PrintingFlags.PrintingInductiveMake (struct
     let encode = encode_tuple
@@ -268,7 +246,6 @@ module PrintingCasesLet =
          else " are not printed using a `let' form")
   end)
 
-module PrintingIf  = Goptions.MakeRefTable(PrintingCasesIf)
 module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
 
 (** univ and sort detyping *)
@@ -616,6 +593,9 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
       n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
+  let ci_bool =
+    match Rocqlib.lib_ref_opt "core.bool.type" with None -> false
+    | Some bool -> GlobRef.CanOrd.equal (IndRef ci.ci_ind) bool in
   let tag =
     let tag = ci.ci_pp_info.style in
     if flags.flg.always_regular_match_style then
@@ -624,7 +604,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
       tag
     else if PrintingLet.active ci.ci_ind then
       LetStyle
-    else if PrintingIf.active ci.ci_ind then
+    else if ci_bool then
       IfStyle
     else
       tag
@@ -641,7 +621,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
     let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
     GLetTuple (nal,(alias,pred),tomatch,d)
   | IfStyle, None ->
-      if Array.for_all (fun br -> is_nondep_branch sigma br) bl then
+      if ci_bool && Array.for_all (fun br -> is_nondep_branch sigma br) bl then
         let map i br =
           let ctx, body = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
           EConstr.it_mkLambda_or_LetIn body ctx
@@ -653,7 +633,11 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
         GIf (tomatch,(alias,pred), nondepbrs.(0), nondepbrs.(1))
       else
         let eqnl = detype_eqns constructs (ci, univs, params, bl) in
-        GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+        if Array.length bl = 2 && is_nondep_branch sigma bl.(0)
+           && not (is_nondep_branch sigma bl.(1)) then
+          GCases (tag,pred,[tomatch,(alias,aliastyp)],List.rev eqnl)
+        else
+          GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
       let eqnl = detype_eqns constructs (ci, univs, params, bl) in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)