From 1f0a2f70c4621c33abba597ce420121b66feefae Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 20 Dec 2023 11:40:27 +0000 Subject: [PATCH] fix: do not introduced additional `let`s that block match generalization --- Qq/Match.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Qq/Match.lean b/Qq/Match.lean index 78c871e..3ca0b2d 100644 --- a/Qq/Match.lean +++ b/Qq/Match.lean @@ -257,14 +257,14 @@ macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in scoped macro "comefrom" n:ident "do" b:doSeq : doElem => `(doElem| assert! (_comefrom $n do $b)) -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 : TSyntax `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 @@ -335,11 +335,11 @@ private partial def floatExprAntiquot (depth : Nat) : Term → StateT (Array (TS | 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)) => @@ -351,7 +351,7 @@ macro_rules 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))) + `(doSeqItem| do assert! (_qq_match $pat ← $rhs | $alt))) `(doElem| do $(lifts.push t):doSeqItem*)