feat: add support for match in iprop(...)

Iris/Iris/BI/Notation.lean

@@ -1,16 +1,18 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
+Authors: Lars König, Alex Keizer
 -/
 module
 
 public meta import Lean.PrettyPrinter.Delaborator
 
+meta import Lean.Parser.Term
+
 public meta section
 
 namespace Iris.BI
-open Lean Lean.Macro
+open Lean Lean.Macro Lean.Parser.Term
 
 -- define `iprop` embedding in `term`
 syntax:max "iprop(" term ")" : term
@@ -27,6 +29,13 @@ macro_rules
   | `(iprop(if $c then $t else $e)) => ``(if $c then iprop($t) else iprop($e))
   | `(iprop(($P : $t)))             => ``((iprop($P) : $t))
   | `(iprop(fun $xs* => $P))        => ``(fun $xs* => iprop($P))
+  -- `iprop(match …)` expansion wraps the rhs of each match arm in `iprop(…)`
+  | `(iprop(match $[$g:generalizingParam]? $[$m:motive]? $[$x:matchDiscr],* with
+              $[$alts:matchAlt]*)) => do
+        let alts ← alts.mapM <| fun
+          | `(matchAltExpr| | $[$lhs]|* => $rhs) => `(matchAltExpr| | $[$lhs]|* => iprop($rhs))
+          | _ => throwUnsupported
+        `(match $[$g:generalizingParam]? $[$m:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*)
 
 macro:max "iprop(" P:term " : " t:term ")" : term => `((iprop($P) : $t))
 
@@ -47,6 +56,18 @@ partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m T
     let e ← unpackIprop e
     `(if $c then $t else $e)
   | `(($P : $t))             => do ``(($(← unpackIprop P) : $t))
+  | `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) => do
+      -- The following type ascriptions look redundant, but, without them, the ``(match ...)`
+      -- syntax quotation below fails with an error about types containing metavariables.
+      let g : Option (TSyntax ``generalizingParam) := g
+      let mot : Option (TSyntax ``motive) := mot
+      let alts ← Array.mapM (as := alts) (m:=m) <| fun
+        | `(matchAltExpr| | $[$lhs]|* => $rhs) => do
+            let rhs ← unpackIprop rhs
+            `(matchAltExpr| | $[$lhs]|* => $rhs)
+        | alt => return ⟨alt⟩
+      `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*)
+  -- Fallback case
   | `($t)                    => `($t:term)
 
 end Iris.BI

Iris/Iris/Tests/Notation.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
+Authors: Lars König, Alex Keizer
 -/
 module
 
@@ -110,9 +110,39 @@ variable [BIBase PROP] (P Q R : PROP) (Ψ : Nat → PROP) (Φ : Nat → Nat →
 
 /-- info: if p = true then iprop(□ P) else P : PROP -/
 #guard_msgs in #check iprop(if p then □ P else P)
+/-- info: iprop((if p = true then □ P else P) ∗ Q) : PROP -/
+#guard_msgs in #check iprop((if p then □ P else P) ∗ Q)
 /-- info: iprop(□ P) : PROP -/
 #guard_msgs in #check iprop((□ P : PROP))
 
+/--
+info: match p with
+| true => Ψ 1
+| false => iprop(False) : PROP
+-/
+#guard_msgs in #check iprop(match p with
+  | true => term(Ψ 1)
+  | false => False)
+
+/--
+info: iprop(□
+    match p with
+    | true => Ψ 1
+    | false => False) : PROP
+-/
+#guard_msgs in #check iprop(□ match p with
+  | true => term(Ψ 1)
+  | false => False)
+
+/--
+info: match true with
+| true => iprop(P ∗ Q)
+| false => iprop(P ∗ Q) : PROP
+-/
+#guard_msgs in #check iprop(match (generalizing := false) (motive := Bool → PROP) true with
+  | true | false => P ∗ Q
+)
+
 /-! ## Derived Connectives -/
 
 /-- info: ⊢ P : Prop -/