Add "if <term> is <pattern> then _ else _" syntax

.gitlab-ci.yml

@@ -1218,12 +1218,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

@@ -89,7 +89,6 @@ CI_TARGETS= \
     ci-oddorder \
     ci-paco \
     ci-parsec \
-    ci-perennial \
     ci-quickchick_test \
     ci-refman \
     ci-rewriter \
@@ -231,8 +230,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

@@ -120,8 +120,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
 
@@ -437,16 +436,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/21609-proux01-if-is.sh

@@ -0,0 +1,3 @@
+overlay bedrock2 https://github.com/proux01/bedrock2 rocq21478 21609
+overlay itree https://github.com/proux01/InteractionTrees rocq21478 21609
+overlay unimath https://github.com/proux01/UniMath rocq21478 21609

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

@@ -0,0 +1,7 @@
+- **Added:**
+  new syntactic sugar `if g is c then t else e`
+  and `if g isn't c then t else e` for `match g with c => t | _ => e end`
+  and `match g with c => e | _ => t end` respectively. This adds the
+  new reserved keywords `is` and `isn't`
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  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 return then where with
+    fix for forall fun if in is isn't let match 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,14 @@ 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 @term isn't @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 +81,10 @@ 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` and `if g isn't c then t else e`
+syntaxes are syntactic sugar for `match g with c => t | _ => e end`
+and `match g with c => e | _ => t end` respectively.
+
 .. _irrefutable-patterns:
 
 Irrefutable patterns: the destructuring let variants

doc/tools/docgram/common.edit_mlg

@@ -264,6 +264,8 @@ binder_constr: [
 | 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_if "if" term200 "isn't" 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

@@ -163,10 +163,20 @@ binder_constr: [
 | "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
+| "if" term200 "isn't" if_dthen if_else
 | "fix" fix_decls
 | "cofix" cofix_decls
 ]
 
+if_dthen: [
+| pattern200 OPT [ "in" pattern200 ] OPT case_type "then" lconstr
+]
+
+if_else: [
+| "else" lconstr
+]
+
 arg: [
 | test_lpar_id_coloneq "(" identref ":=" lconstr ")"
 | test_lpar_nat_coloneq "(" natural ":=" lconstr ")"

doc/tools/docgram/orderedGrammar

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

parsing/g_constr.mlg

@@ -303,9 +303,25 @@ 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 (MatchStyle, rt, [c, na, t], [b1; b2]) }
+      | "if"; c = term LEVEL "200"; "isn't"; db1 = if_dthen; b2 = if_else ->
+        { let b1, (na, t), rt = db1 in
+          let b1, b2 = let open CAst in
+            let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
+            (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) in
+          CAst.make ~loc @@ CCases (MatchStyle, 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) } ] ]
   ;
+  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) } ]];
   arg:
     [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
       | test_lpar_nat_coloneq; "("; n = natural; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByPos n)) }

plugins/ssr/ssrvernac.mlg

@@ -44,17 +44,15 @@ IGNORE KEYWORDS
 
 (* global syntactic changes and vernacular commands *)
 
-(** Alternative notations for "match" and anonymous arguments. *)(* ************)
+(** Alternative notations for anonymous arguments. *)(* ************)
 
 (* Syntax:                                                        *)
-(*  if <term> is <pattern> then ... else ...                      *)
-(*  if <term> is <pattern> [in ..] return ... then ... else ...   *)
 (*  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' *)
@@ -65,9 +63,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
@@ -76,7 +71,6 @@ let aliasvar = function
 let mk_cnotype mp = aliasvar mp, None
 let mk_ctype mp t = aliasvar mp, Some t
 let mk_rtype t = Some t
-let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt
 let mk_let ?loc rt ct mp c1 =
   CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)])
 let mk_pat c (na, t) = (c, na, t)
@@ -87,25 +81,8 @@ GRAMMAR EXTEND Gram
   GLOBAL: binder_constr;
   ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
   ssr_mpat: [[ p = pattern -> { [[p]] } ]];
-  ssr_dpat: [
-    [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
-    | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt }
-    | mp = ssr_mpat -> { mp, no_ct, no_rt }
-  ] ];
-  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]];
-  ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
-  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
   binder_constr: TOP [
-    [ "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 ->
-      { 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
-        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
-      in
-      CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
-    | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
+    [ "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
       { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 }
     | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr;
       rt = ssr_rtype; "in"; c1 = lconstr ->

test-suite/bugs/bug_16975.v

@@ -43,8 +43,8 @@ Notation "X ≃ Y" := (weq X%type Y%type) : type_scope.
 
 Definition pr1weq {X Y : Type} := pr1 : X ≃ Y -> (X -> Y).
 Coercion pr1weq : weq >-> Funclass.
-Definition make_weq {X Y : Type} (f : X -> Y) (is: isweq f) : X ≃ Y.
-exact (tpair (λ f : X -> Y, isweq f) f is).
+Definition make_weq {X Y : Type} (f : X -> Y) (isf: isweq f) : X ≃ Y.
+exact (tpair (λ f : X -> Y, isweq f) f isf).
 Defined.
 
 Theorem twooutof3c {X Y Z : Type} (f : X -> Y) (g : Y -> Z)

test-suite/bugs/bug_3374.v

@@ -24,7 +24,7 @@ Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd
 Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y )
   := forall x x' x0 x0' : X , R x x' ->  R x0 x0' ->  paths ( f x x0 ) ( f x' x0' ) .
 Axiom setquotuniv : forall  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y .
-Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R )
+Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( isf : iscomprelfun2 R f ) ( c c0 : setquot R )
 : Y .
 Proof.
   intros .

test-suite/bugs/bug_3375.v

@@ -8,7 +8,7 @@ Definition UU := Set.
 Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
 Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
 Definition hProp := sigT (fun X : Type => admit).
-Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp.
+Axiom hProppair : forall ( X : UU ) ( _ : admit ), hProp.
 Definition hProptoType := @projT1 _ _ : hProp -> Type .
 Coercion hProptoType: hProp >-> Sortclass.
 Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).

test-suite/bugs/bug_6661.v

@@ -123,10 +123,10 @@ Defined.
 
 Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr.
 
-Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
+Lemma proofirrelevancecontr {X : UU} (isc : iscontr X) (x x' : X) : x = x'.
 Proof.
   intros.
-  induction is as [y fe].
+  induction isc as [y fe].
   exact (fe x @ !(fe x')).
 Defined.
 
@@ -214,10 +214,10 @@ Section isweqcontrtounit.
   (* Constraint uu0 < i. *)
 
   (* Without this constraint, we get i = uu0 in the next definition *)
-  Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
+  Lemma isweqcontrtounit@{} {T : Type@{i}} (isc : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
   Proof.
     intros. intro y. induction y.
-    induction is as [c h].
+    induction isc as [c h].
     split with (hfiberpair@{i i i} _ c (idpath tt)).
     intros ha.
     induction ha as [x e].

test-suite/output/PrintGrammar.out

@@ -19,6 +19,8 @@ Entry binder_constr is
     LEVEL "200"
   | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":=";
     term LEVEL "200"; "in"; term LEVEL "200"
+  | "if"; term LEVEL "200"; "is"; if_dthen; if_else
+  | "if"; term LEVEL "200"; "isn't"; if_dthen; if_else
   | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else";
     term LEVEL "200"
   | "fix"; fix_decls

test-suite/output/PrintGrammarConstr.out

@@ -10,6 +10,8 @@ Entry binder_constr is
     LEVEL "200"
   | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":=";
     term LEVEL "200"; "in"; term LEVEL "200"
+  | "if"; term LEVEL "200"; "is"; if_dthen; if_else
+  | "if"; term LEVEL "200"; "isn't"; if_dthen; if_else
   | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else";
     term LEVEL "200"
   | "fix"; fix_decls

test-suite/output/PrintKeywords.out

@@ -81,6 +81,8 @@ forall
 fun
 if
 in
+is
+isn't
 let
 match
 return

test-suite/output/PrintNotation.out

@@ -166,9 +166,9 @@ Notation "{ ' _ : _ & _ }" at level 0 with arguments strict pattern
 at level 0, constr, constr, no associativity.
 Notation "{ ' _ : _ & _ & _ }" at level 0 with arguments strict pattern
 at level 0, constr, constr, constr, no associativity.
-Notation "if _ is _ then _ else _" at level 200 with arguments constr,
-pattern at level 100 at level 100, constr, constr at next level,
-no associativity.
+Notation "if _ is _ then _ else _" at level 200 with arguments constr
+at level 200, pattern at level 100 at level 100, constr at level 200, constr
+at level 200, no associativity.
 Notation "_ -> _" at level 99 with arguments constr at next level, constr
 at level 200, no associativity.
 Notation "_ <-> _" at level 95 with arguments constr at next level, constr
@@ -263,9 +263,9 @@ Notation "{ ' _ : _ & _ }" at level 0 with arguments strict pattern
 at level 0, constr, constr, no associativity.
 Notation "{ ' _ : _ & _ & _ }" at level 0 with arguments strict pattern
 at level 0, constr, constr, constr, no associativity.
-Notation "if _ is _ then _ else _" at level 200 with arguments constr,
-pattern at level 100 at level 100, constr, constr at next level,
-no associativity.
+Notation "if _ is _ then _ else _" at level 200 with arguments constr
+at level 200, pattern at level 100 at level 100, constr at level 200, constr
+at level 200, no associativity.
 Notation "{{ _ }}" in Foo at level 0 with arguments custom Foo,
 no associativity.
 Notation "{{ _ }}" in Foo at level 0 with arguments custom Foo,

test-suite/success/ltac.v

@@ -202,12 +202,12 @@ Abort.
 
 (* Utilisation de let rec sans arguments *)
 
-Ltac is :=
+Ltac rec_intros :=
   let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
   i.
 
 Goal True -> True -> True.
-is.
+rec_intros.
 exact I.
 Abort.
 

test-suite/success/telescope_canonical.v

@@ -1,9 +1,9 @@
-Structure Inner := mkI { is :> Type }.
+Structure Inner := mkI { ins :> Type }.
 Structure Outer := mkO { os :> Inner }.
 Canonical Structure natInner := mkI nat.
 Canonical Structure natOuter := mkO natInner.
 Definition hidden_nat := nat.
-Axiom P : forall S : Outer, is (os S) -> Prop.
+Axiom P : forall S : Outer, ins (os S) -> Prop.
 Lemma test1 (n : hidden_nat) : P _ n.
 Admitted.