Merge remote-tracking branch 'origin/master' into eric-wieser/fix-return

Qq/Match.lean

@@ -234,9 +234,9 @@ scoped elab "_qq_match" pat:term " ← " e:term " | " alt:term " in " body:term
   makeMatchCode q($inst2) inst oldPatVarDecls argLvlExpr argTyExpr synthed q($e') alt expectedType fun expectedType =>
     return Quoted.unsafeMk (← elabTerm body expectedType)
 
-scoped syntax "_qq_match" term " ← " term " | " doSeq : term
+scoped syntax "_qq_match" term " := " term " | " doSeq : term
 macro_rules
-  | `(assert! (_qq_match $pat ← $e | $alt); $x) => `(_qq_match $pat ← $e | (do $alt) in $x)
+  | `(assert! (_qq_match $pat := $e | $alt); $x) => `(_qq_match $pat ← $e | (do $alt) in $x)
 
 partial def isIrrefutablePattern : Term → Bool
   | `(($stx)) => isIrrefutablePattern stx
@@ -246,14 +246,14 @@ partial def isIrrefutablePattern : Term → Bool
   | `(true) => false | `(false) => false -- TODO properly
   | stx => stx.1.isIdent
 
-def mkLetDoSeqItem [Monad m] [MonadQuotation m] (pat : Term) (rhs : TSyntax `doElem) (alt : TSyntax ``doSeq) : m (List (TSyntax ``doSeqItem)) := do
+def mkLetDoSeqItem [Monad m] [MonadQuotation m] (pat : Term) (rhs : Term) (alt : TSyntax ``doSeq) : m (List (TSyntax ``doSeqItem)) := do
   match pat with
     | `(_) => return []
     | _ =>
       if isIrrefutablePattern pat then
-        return [← `(doSeqItem| let $pat:term ← $rhs)]
+        return [← `(doSeqItem| let $pat:term := $rhs)]
       else
-        return [← `(doSeqItem| let $pat:term ← $rhs | $alt)]
+        return [← `(doSeqItem| let $pat:term := $rhs | $alt)]
 
 end Impl
 
@@ -288,7 +288,7 @@ private partial def floatLevelAntiquot (stx : Syntax.Level) : StateT (Array (TSy
   if stx.1.isAntiquot && !stx.1.isEscapedAntiquot then
     if !stx.1.getAntiquotTerm.isIdent then
       withFreshMacroScope do
-        push <|<- `(doSeqItem| let u : Level := $(⟨stx.1.getAntiquotTerm⟩))
+        push <| ← `(doSeqItem| let u : Level := $(⟨stx.1.getAntiquotTerm⟩))
         `(level| u)
     else
       pure stx
@@ -316,32 +316,24 @@ private partial def floatExprAntiquot (depth : Nat) : Term → StateT (Array (TS
               return ⟨addSyntaxDollar id⟩
           | none => pure ()
         withFreshMacroScope do
-          push <|<- `(doSeqItem| let a : Quoted _ := $term)
+          push <| ← `(doSeqItem| let a : Quoted _ := $term)
           return ⟨addSyntaxDollar (← `(a))⟩
     else
       match stx with
       | ⟨.node i k args⟩ => return ⟨.node i k (← args.mapM (floatExprAntiquot depth ⟨·⟩))⟩
       | stx => return stx
 
 macro_rules
-  | `(doElem| let $pat:term ← $_) => do
+  | `(doElem| let $pat:term := $_) => do
     if !hasQMatch pat then Macro.throwUnsupported
     Macro.throwError "let-bindings with ~q(.) require an explicit alternative"
 
-  | `(doElem| let $pat:term ← $rhs:doElem | $alt:doSeq) => do
+  | `(doElem| let $pat:term := $rhs:term | $alt:doSeq) => do
     if !hasQMatch pat then Macro.throwUnsupported
     match pat with
       | `(~q($pat)) =>
         let (pat, lifts) ← floatExprAntiquot 0 pat #[]
-
-        let mut t ← (do
-          match rhs with
-            | `(doElem| $id:ident $rhs:term) =>
-              if id.getId.eraseMacroScopes == `pure then -- TODO: super hacky
-                return ← `(doSeqItem| assert! (_qq_match $pat ← $rhs | $alt))
-            | _ => pure ()
-          `(doSeqItem| do let rhs ← $rhs; assert! (_qq_match $pat ← rhs | $alt)))
-
+        let t ← `(doSeqItem| do assert! (_qq_match $pat := $rhs | $alt))
         `(doElem| do $(lifts.push t):doSeqItem*)
 
       | _ =>
@@ -355,16 +347,13 @@ macro_rules
 
   | `(doElem| match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     if !patss.any (·.any (hasQMatch ·)) then Macro.throwUnsupported
-    let discrs ← discrs.mapM fun d => withFreshMacroScope do
-      pure (← `(x), ← `(doSeqItem| let x := $d:term))
-    let mut items := discrs.map (·.2)
-    let discrs := discrs.map (·.1)
+    let mut items := #[]
     let mut alt : TSyntax `doElem ← `(doElem| throwError "nonexhaustive match")
     for pats in patss.reverse, rhs in rhss.reverse do
       let mut subItems : Array (TSyntax ``doSeqItem) := #[]
       for discr in discrs, pat in pats do
         subItems :=
-          subItems ++ (← mkLetDoSeqItem pat (← `(doElem| pure $discr:term)) (←`(doSeq|$alt:doElem)))
+          subItems ++ (← mkLetDoSeqItem pat discr (←`(doSeq|$alt:doElem)))
       subItems := subItems.push (←`(doSeqItem|do $rhs))
       alt ← `(doElem| do $subItems:doSeqItem*)
     items := items.push (←`(doSeqItem|$alt:doElem))

examples/matching.lean

@@ -117,3 +117,10 @@ def foo_if_let2 (T : Q(Type)) : MetaM Nat := do
 #eval do guard <| (←foo_if_let2 q(Nat)) == 1
 
 end test_return
+def pairLit (u : Lean.Level) (α : Q(Type u)) (a : Q($α)) : MetaM Q($α × $α) := do
+  match u, α, a with
+  | 0, ~q(Nat), n => return q(($n, $n))
+  | 0, ~q(Int), z => return q(($z, $z))
+  | _, _, _ => failure
+
+#eval show MetaM Unit from do guard <| (←pairLit _ _ q(2)) == q((2, 2))

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.6.0-rc1