feat: add letConfig syntax to do block let/have parsers (#13250)
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 <noreply@anthropic.com>
This commit is contained in:
Sebastian Graf
GitHub
parent
ffc2c0ab1a
commit
aa1144602b
4 changed files with 77 additions and 28 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue