From aa1144602bbf07aa8df4ffb9ce18df3c6499e689 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 2 Apr 2026 11:40:44 +0200 Subject: [PATCH] feat: add `letConfig` syntax to `do` block `let`/`have` parsers (#13250) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR extends the `doLet`, `doLetElse`, `doLetArrow`, and `doHave` parsers to accept `letConfig` (e.g. `(eq := h)`, `+nondep`, `+usedOnly`, `+zeta`), matching the syntax of term-level `let`/`have`. The elaborators are adjusted to handle the shifted syntax indices but do not yet process the configuration; that will be done in a follow-up PR after stage0 is updated, allowing the use of proper quotation patterns. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/BuiltinDo/Let.lean | 30 +++++++++++++--- src/Lean/Elab/Do/InferControlInfo.lean | 20 +++++++++-- src/Lean/Elab/Do/Legacy.lean | 47 ++++++++++++++++---------- src/Lean/Parser/Do.lean | 8 ++--- 4 files changed, 77 insertions(+), 28 deletions(-) diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean index 3103df4a81..231d11cc67 100644 --- a/src/Lean/Elab/BuiltinDo/Let.lean +++ b/src/Lean/Elab/BuiltinDo/Let.lean @@ -168,12 +168,25 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do elabDoElem (← `(doElem| $pattern:term := $x)) dec | _ => throwUnsupportedSyntax +/-- Backward-compatible index for `doLet`/`doLetArrow`/`doLetElse`: if `letConfig` is present at +index 2, the decl is at index 3; otherwise (old-shape syntax from stage0 macros), it's at index 2. -/ +private def doLetDeclIdx (stx : Syntax) : Nat := + if stx[2].isOfKind ``Parser.Term.letConfig then 3 else 2 + +/-- Backward-compatible index for `doHave`: if `letConfig` is present at +index 1, the decl is at index 2; otherwise (old-shape syntax), it's at index 1. -/ +private def doHaveDeclIdx (stx : Syntax) : Nat := + if stx[1].isOfKind ``Parser.Term.letConfig then 2 else 1 + @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do - let `(doLet| let $[mut%$mutTk?]? $decl:letDecl) := stx | throwUnsupportedSyntax + -- "let " >> optional "mut " >> letConfig >> letDecl + let mutTk? := stx.raw[1].getOptional? + let decl : TSyntax ``letDecl := ⟨stx.raw[doLetDeclIdx stx.raw]⟩ elabDoLetOrReassign (.let mutTk?) decl dec @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do - let `(doHave| have $decl:letDecl) := stx | throwUnsupportedSyntax + -- "have" >> letConfig >> letDecl + let decl : TSyntax ``letDecl := ⟨stx.raw[doHaveDeclIdx stx.raw]⟩ elabDoLetOrReassign .have decl dec @[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do @@ -199,7 +212,14 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do | _ => throwUnsupportedSyntax @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do - let `(doLetElse| let $[mut%$mutTk?]? $pattern := $rhs | $otherwise $(body?)?) := stx | throwUnsupportedSyntax + -- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> + -- (checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent) + let mutTk? := stx.raw[1].getOptional? + let offset := doLetDeclIdx stx.raw -- 3 if letConfig present, 2 otherwise + let pattern : Term := ⟨stx.raw[offset]⟩ + let rhs : Term := ⟨stx.raw[offset + 2]⟩ + let otherwise : TSyntax ``doSeqIndent := ⟨stx.raw[offset + 4]⟩ + let body? := stx.raw[offset + 5].getOptional?.map fun s => (⟨s⟩ : TSyntax ``doSeqIndent) let letOrReassign := LetOrReassign.let mutTk? let vars ← getPatternVarsEx pattern letOrReassign.checkMutVars vars @@ -211,7 +231,9 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec @[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do - let `(doLetArrow| let $[mut%$mutTk?]? $decl) := stx | throwUnsupportedSyntax + -- "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl) + let mutTk? := stx.raw[1].getOptional? + let decl : TSyntax [``doIdDecl, ``doPatDecl] := ⟨stx.raw[doLetDeclIdx stx.raw]⟩ elabDoArrow (.let mutTk?) decl dec @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean index 3f21e05566..2b568677bc 100644 --- a/src/Lean/Elab/Do/InferControlInfo.lean +++ b/src/Lean/Elab/Do/InferControlInfo.lean @@ -169,15 +169,29 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do let bodyInfo ← match body? with | none => pure {} | some body => ofSeq ⟨body⟩ return otherwiseInfo.alternative bodyInfo | _ => - let handlers := controlInfoElemAttribute.getEntries (← getEnv) stx.raw.getKind + -- Backward compat: quotation patterns above may fail for doLet/doHave/doLetElse/doLetArrow + -- when the parser shape includes letConfig (not present in stage0 quotations). + let kind := stx.raw.getKind + if kind == ``Parser.Term.doLet || kind == ``Parser.Term.doHave || kind == ``Parser.Term.doLetRec then + return .pure + if kind == ``Parser.Term.doLetElse then + let offset := if stx.raw[2].isOfKind ``Parser.Term.letConfig then 3 else 2 + let otherwise? := stx.raw[offset + 4].getOptional?.map (⟨·⟩ : _ → TSyntax ``doSeqIndent) + let body? := stx.raw[offset + 5].getOptional?.map (⟨·⟩ : _ → TSyntax ``doSeqIndent) + return ← ofLetOrReassign #[] none otherwise? body? + if kind == ``Parser.Term.doLetArrow then + let declIdx := if stx.raw[2].isOfKind ``Parser.Term.letConfig then 3 else 2 + let decl : TSyntax [``doIdDecl, ``doPatDecl] := ⟨stx.raw[declIdx]⟩ + return ← ofLetOrReassignArrow false decl + let handlers := controlInfoElemAttribute.getEntries (← getEnv) kind for handler in handlers do let res ← catchInternalId unsupportedSyntaxExceptionId (some <$> handler.value stx) (fun _ => pure none) if let some info := res then return info throwError - "No `ControlInfo` inference handler found for `{stx.raw.getKind}` in syntax {indentD stx}\n\ - Register a handler with `@[doElem_control_info {stx.raw.getKind}]`." + "No `ControlInfo` inference handler found for `{kind}` in syntax {indentD stx}\n\ + Register a handler with `@[doElem_control_info {kind}]`." partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDecl, ``doPatDecl]) : TermElabM ControlInfo := do match decl with diff --git a/src/Lean/Elab/Do/Legacy.lean b/src/Lean/Elab/Do/Legacy.lean index 90a7ceb6d1..bb74224c74 100644 --- a/src/Lean/Elab/Do/Legacy.lean +++ b/src/Lean/Elab/Do/Legacy.lean @@ -36,6 +36,18 @@ private def getDoSeq (doStx : Syntax) : Syntax := def elabLiftMethod : TermElab := fun stx _ => throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression" +/-- Backward-compatible index for `doLet`/`doLetArrow`/`doLetElse`: if `letConfig` is present at +index 2, the decl is at index 3; otherwise (old-shape syntax from stage0 quotations), it's at +index 2. -/ +private def doLetDeclIdx (stx : Syntax) : Nat := + if stx[2].isOfKind ``Parser.Term.letConfig then 3 else 2 + +/-- Backward-compatible index for `doHave`: if `letConfig` is present at +index 1, the decl is at index 2; otherwise (old-shape syntax from stage0 quotations), it's at +index 1. -/ +private def doHaveDeclIdx (stx : Syntax) : Nat := + if stx[1].isOfKind ``Parser.Term.letConfig then 2 else 1 + /-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind. -/ private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool := k == ``Parser.Term.do || @@ -76,9 +88,9 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool := else if k == ``Parser.Term.let then letDeclHasBinders stx[1] else if k == ``Parser.Term.doLet then - letDeclHasBinders stx[2] + letDeclHasBinders stx[doLetDeclIdx stx] else if k == ``Parser.Term.doLetArrow then - letDeclArgHasBinders stx[2] + letDeclArgHasBinders stx[doLetDeclIdx stx] else false @@ -701,12 +713,12 @@ def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do throwError "unexpected kind of let declaration" def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) := - -- leading_parser "let " >> optional "mut " >> letDecl - getLetDeclVars doLet[2] + -- leading_parser "let " >> optional "mut " >> letConfig >> letDecl + getLetDeclVars doLet[doLetDeclIdx doLet] def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := - -- leading_parser "have" >> letDecl - getLetDeclVars doHave[1] + -- leading_parser "have" >> letConfig >> letDecl + getLetDeclVars doHave[doHaveDeclIdx doHave] def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do -- letRecDecls is an array of `(group (optional attributes >> letDecl))` @@ -727,9 +739,9 @@ def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do let pattern := doPatDecl[0] getPatternVarsEx pattern --- leading_parser "let " >> optional "mut " >> (doIdDecl <|> doPatDecl) +-- leading_parser "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl) def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do - let decl := doLetArrow[2] + let decl := doLetArrow[doLetDeclIdx doLetArrow] if decl.getKind == ``Parser.Term.doIdDecl then return #[getDoIdDeclVar decl] else if decl.getKind == ``Parser.Term.doPatDecl then @@ -1060,14 +1072,14 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFreshMacroScope do let kind := decl.getKind if kind == ``Parser.Term.doLet then - let letDecl := decl[2] + let letDecl := decl[doLetDeclIdx decl] `(let $letDecl:letDecl; $k) else if kind == ``Parser.Term.doLetRec then let letRecToken := decl[0] let letRecDecls := decl[1] return mkNode ``Parser.Term.letrec #[letRecToken, letRecDecls, mkNullNode, k] else if kind == ``Parser.Term.doLetArrow then - let arg := decl[2] + let arg := decl[doLetDeclIdx decl] if arg.getKind == ``Parser.Term.doIdDecl then let id := arg[0] let type := expandOptType id arg[1] @@ -1415,7 +1427,7 @@ mutual /-- Generate `CodeBlock` for `doLetArrow; doElems` `doLetArrow` is of the form ``` - "let " >> optional "mut " >> (doIdDecl <|> doPatDecl) + "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl) ``` where ``` @@ -1424,7 +1436,7 @@ mutual ``` -/ partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do - let decl := doLetArrow[2] + let decl := doLetArrow[doLetDeclIdx doLetArrow] if decl.getKind == ``Parser.Term.doIdDecl then let y := decl[0] checkNotShadowingMutable #[y] @@ -1475,11 +1487,12 @@ mutual throwError "unexpected kind of `do` declaration" partial def doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock := do - -- "let " >> optional "mut " >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq - let pattern := doLetElse[2] - let val := doLetElse[4] - let elseSeq := doLetElse[6] - let bodySeq := doLetElse[7][0] + -- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq + let offset := doLetDeclIdx doLetElse + let pattern := doLetElse[offset] + let val := doLetElse[offset + 2] + let elseSeq := doLetElse[offset + 4] + let bodySeq := doLetElse[offset + 5][0] let contSeq ← if isMutableLet doLetElse then let vars ← (← getPatternVarsEx pattern).mapM fun var => `(doElem| let mut $var := $var) pure (vars ++ (getDoSeqElems bodySeq).toArray) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 390ecc02c7..1c81eb498c 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -67,9 +67,9 @@ def notFollowedByRedefinedTermToken := "token at 'do' element" @[builtin_doElem_parser] def doLet := leading_parser - "let " >> optional "mut " >> letDecl + "let " >> optional "mut " >> letConfig >> letDecl @[builtin_doElem_parser] def doLetElse := leading_parser withPosition <| - "let " >> optional "mut " >> termParser >> " := " >> termParser >> + "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> (checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent) @[builtin_doElem_parser] def doLetExpr := leading_parser withPosition <| @@ -89,7 +89,7 @@ def doPatDecl := leading_parser atomic (termParser >> optType >> ppSpace >> leftArrow) >> doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent)) @[builtin_doElem_parser] def doLetArrow := leading_parser withPosition <| - "let " >> optional "mut " >> (doIdDecl <|> doPatDecl) + "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl) /- We use `letIdDeclNoBinders` to define `doReassign`. @@ -114,7 +114,7 @@ def letIdDeclNoBinders := leading_parser @[builtin_doElem_parser] def doReassignArrow := leading_parser notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl) @[builtin_doElem_parser] def doHave := leading_parser - "have" >> Term.letDecl + "have" >> Term.letConfig >> Term.letDecl /- In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as