max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-11 09:39:40 -08:00
parent 164577d94e
commit 55c5234100
36 changed files with 815 additions and 2067 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/Lean/Attributes.lean generated
View file

@ -182,11 +182,11 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
Helper methods for decoding the parameters of builtin attributes that are defined before `Lean.Parser`.
We have the following ones:
```
@[builtinAttrParser] def simple := parser! ident >> optional ident >> optional priorityParser
@[builtinAttrParser] def simple := leading_parser ident >> optional ident >> optional priorityParser
/- We can't use `simple` for `class`, `instance`, `export` and `macro` because they are keywords. -/
@[builtinAttrParser] def «class» := parser! "class"
@[builtinAttrParser] def «instance» := parser! "instance" >> optional priorityParser
@[builtinAttrParser] def «macro» := parser! "macro " >> ident
@[builtinAttrParser] def «class» := leading_parser "class"
@[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser
@[builtinAttrParser] def «macro» := leading_parser "macro " >> ident
```
Note that we need the parsers for `class`, `instance`, and `macros` because they are keywords.
-/

4
stage0/src/Lean/Compiler/ExternAttr.lean generated
View file

@ -36,8 +36,8 @@ structure ExternAttrData where
entries : List ExternEntry
deriving Inhabited
-- def externEntry := parser! optional ident >> optional (nonReservedSymbol "inline ") >> strLit
-- @[builtinAttrParser] def extern := parser! nonReservedSymbol "extern " >> optional numLit >> many externEntry
-- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit
-- @[builtinAttrParser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry
private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
let arity? := if stx[1].isNone then none else some <| stx[1][0].isNatLit?.getD 0
let entriesStx := stx[2].getArgs

2
stage0/src/Lean/Elab/App.lean generated
View file

@ -890,7 +890,7 @@ partial def expandApp (stx : Syntax) (pattern := false) : TermElabM (Syntax × A
(args, false)
let (namedArgs, args) ← args.foldlM (init := (#[], #[])) fun (namedArgs, args) stx => do
if stx.getKind == `Lean.Parser.Term.namedArgument then
-- tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
-- trailing_tparser try ("(" >> ident >> " := ") >> termParser >> ")"
let name := stx[1].getId.eraseMacroScopes
let val := stx[3]
let namedArgs ← addNamedArg namedArgs { ref := stx, name := name, val := Arg.stx val }

6
stage0/src/Lean/Elab/Attributes.lean generated
View file

@ -27,7 +27,7 @@ instance : Inhabited Attribute where
/-
```
attrKind := parser! optional («scoped» <|> «local»)
attrKind := leading_parser optional («scoped» <|> «local»)
```
-/
def toAttributeKind [Monad m] [MonadResolveName m] [MonadError m] (attrKindStx : Syntax) : m AttributeKind := do
@ -44,7 +44,7 @@ def mkAttrKindGlobal : Syntax :=
Syntax.node `Lean.Parser.Term.attrKind #[mkNullNode]
def elabAttr {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] (attrInstance : Syntax) : m Attribute := do
/- attrInstance := ppGroup $ parser! attrKind >> attrParser -/
/- attrInstance := ppGroup $ leading_parser attrKind >> attrParser -/
let attrKind ← toAttributeKind attrInstance[0]
let attr := attrInstance[1]
let attr ← liftMacroM <| expandMacros attr
@ -67,7 +67,7 @@ def elabAttrs {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [Mo
attrs := attrs.push (← elabAttr attr)
return attrs
-- parser! "@[" >> sepBy1 attrInstance ", " >> "]"
-- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
def elabDeclAttrs {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] (stx : Syntax) : m (Array Attribute) :=
elabAttrs stx[1].getSepArgs

8
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -73,8 +73,8 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
/-
Expand `optional (binderTactic <|> binderDefault)`
def binderTactic := parser! " := " >> " by " >> tacticParser
def binderDefault := parser! " := " >> termParser
def binderTactic := leading_parser " := " >> " by " >> tacticParser
def binderDefault := leading_parser " := " >> termParser
-/
private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax := do
if optBinderModifier.isNone then
@ -103,7 +103,7 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
/-
Recall that
```
def typeSpec := parser! " : " >> termParser
def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
```
-/
@ -244,7 +244,7 @@ private partial def getFunBinderIds? (stx : Syntax) : OptionT TermElabM (Array S
Auxiliary function for expanding `fun` notation binders. Recall that `fun` parser is defined as
```
def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
parser! unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser
leading_parser unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser
```
to allow notation such as `fun (a, b) => a + b`, where `(a, b)` should be treated as a pattern.
The result is a pair `(explicitBinders, newBody)`, where `explicitBinders` is syntax of the form

18
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -58,7 +58,7 @@ open Meta
private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
let (some declName) ← getDeclName?
| throwError "invalid `parser!` macro, it must be used in definitions"
| throwError "invalid `leading_parser` macro, it must be used in definitions"
match extractMacroScopes declName with
| { name := Name.str _ s _, scopes := scps, .. } =>
let kind := quote declName
@ -70,13 +70,7 @@ private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax :
else
-- if the parser decl is hidden by hygiene, it doesn't make sense to provide an antiquotation kind
`(OrElse.orElse (Lean.Parser.mkAntiquot $s none) $p)
| _ => throwError "invalid `parser!` macro, unexpected declaration name"
@[builtinTermElab «parser!»] def elabParserMacro : TermElab :=
adaptExpander fun stx => match stx with
| `(parser! $e) => elabParserMacroAux (quote Parser.maxPrec) e
| `(parser! : $prec $e) => elabParserMacroAux prec e
| _ => throwUnsupportedSyntax
| _ => throwError "invalid `leading_parser` macro, unexpected declaration name"
@[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab :=
adaptExpander fun stx => match stx with
@ -88,13 +82,7 @@ private def elabTParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax
let declName? ← getDeclName?
match declName? with
| some declName => let kind := quote declName; `(Lean.Parser.trailingNode $kind $prec $e)
| none => throwError "invalid `tparser!` macro, it must be used in definitions"
@[builtinTermElab «tparser!»] def elabTParserMacro : TermElab :=
adaptExpander fun stx => match stx with
| `(tparser! $e) => elabTParserMacroAux (quote Parser.maxPrec) e
| `(tparser! : $prec $e) => elabTParserMacroAux prec e
| _ => throwUnsupportedSyntax
| none => throwError "invalid `trailing_parser` macro, it must be used in definitions"
@[builtinTermElab «trailing_parser»] def elabTrailingParserMacro : TermElab :=
adaptExpander fun stx => match stx with

2
stage0/src/Lean/Elab/DeclModifiers.lean generated
View file

@ -146,7 +146,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
/-
`declId` is of the form
```
parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
```
but we also accept a single identifier to users to make macro writing more convenient .
-/

2
stage0/src/Lean/Elab/DeclUtil.lean generated
View file

@ -39,7 +39,7 @@ namespace Elab
def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
-- many Term.bracketedBinder >> Term.optType
let binders := stx[0]
let optType := stx[1] -- optional (parser! " : " >> termParser)
let optType := stx[1] -- optional (leading_parser " : " >> termParser)
if optType.isNone then
(binders, none)
else

12
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -55,7 +55,7 @@ def expandDeclNamespace? (stx : Syntax) : Option (Name × Syntax) :=
none
def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-- parser! "axiom " >> declId >> declSig
-- leading_parser "axiom " >> declId >> declSig
let declId := stx[1]
let (binders, typeStx) := expandDeclSig stx[2]
let scopeLevelNames ← getLevelNames
@ -87,8 +87,8 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
/-
parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
leading_parser "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
-/
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
checkValidInductiveModifier modifiers
@ -97,7 +97,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
addDeclarationRanges declName decl
let ctors ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
-- def ctor := leading_parser " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
let ctorModifiers ← elabModifiers ctor[1]
if ctorModifiers.isPrivate && modifiers.isPrivate then
throwError "invalid 'private' constructor in a 'private' inductive datatype"
@ -256,7 +256,7 @@ def elabMutual : CommandElab := fun stx => do
else
throwError "invalid mutual block"
/- parser! "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
/- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
@[builtinCommandElab «attribute»] def elabAttr : CommandElab := fun stx => do
let mut attrInsts := #[]
let mut toErase := #[]
@ -265,7 +265,7 @@ def elabMutual : CommandElab := fun stx => do
let attrName := attrKindStx[1].getId.eraseMacroScopes
unless isAttribute (← getEnv) attrName do
throwError! "unknown attribute [{attrName}]"
toErase := toErase.push attrName
toErase := toErase.push attrName
else
attrInsts := attrInsts.push attrKindStx
let attrs ← elabAttrs attrInsts

12
stage0/src/Lean/Elab/DefView.lean generated
View file

@ -47,7 +47,7 @@ namespace Command
open Meta
def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
-- parser! "abbrev " >> declId >> optDeclSig >> declVal
-- leading_parser "abbrev " >> declId >> optDeclSig >> declVal
let (binders, type) := expandOptDeclSig (stx.getArg 2)
let modifiers := modifiers.addAttribute { name := `inline }
let modifiers := modifiers.addAttribute { name := `reducible }
@ -55,13 +55,13 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
-- parser! "def " >> declId >> optDeclSig >> declVal
-- leading_parser "def " >> declId >> optDeclSig >> declVal
let (binders, type) := expandOptDeclSig (stx.getArg 2)
{ ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
-- parser! "theorem " >> declId >> declSig >> declVal
-- leading_parser "theorem " >> declId >> declSig >> declVal
let (binders, type) := expandDeclSig (stx.getArg 2)
{ ref := stx, kind := DefKind.theorem, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 }
@ -125,7 +125,7 @@ partial def main (type : Syntax) : CommandElabM Name := do
end MkInstanceName
def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- parser! "constant " >> declId >> declSig >> optional declValSimple
-- leading_parser "constant " >> declId >> declSig >> optional declValSimple
let (binders, type) := expandDeclSig (stx.getArg 2)
let val ← match (stx.getArg 3).getOptional? with
| some val => pure val
@ -138,7 +138,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
}
def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- parser! Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
-- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
let attrKind ← toAttributeKind stx[0]
let prio ← liftMacroM <| expandOptNamedPrio stx[2]
let attrStx ← `(attr| instance $(quote prio):numLit)
@ -155,7 +155,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
}
def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
-- parser! "example " >> declSig >> declVal
-- leading_parser "example " >> declSig >> declVal
let (binders, type) := expandDeclSig (stx.getArg 1)
let id := mkIdentFrom stx `_example
let declId := Syntax.node ``Parser.Command.declId #[id, mkNullNode]

2
stage0/src/Lean/Elab/Deriving/Basic.lean generated
View file

@ -45,7 +45,7 @@ structure DerivingClassView where
ref : Syntax
className : Name
/- parser! optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -/
/- leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -/
def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
if optDeriving.isNone then
return #[]

26
stage0/src/Lean/Elab/Do.lean generated
View file

@ -559,12 +559,12 @@ def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Name) := do
throwError "unexpected kind of let declaration"
def getDoLetVars (doLet : Syntax) : TermElabM (Array Name) :=
-- parser! "let " >> optional "mut " >> letDecl
-- leading_parser "let " >> optional "mut " >> letDecl
getLetDeclVars doLet[2]
def getDoHaveVar (doHave : Syntax) : Name :=
/-
`parser! "have " >> Term.haveDecl`
`leading_parser "have " >> Term.haveDecl`
where
```
haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@ -597,7 +597,7 @@ def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Name) := do
let pattern := doPatDecl[0]
getPatternVarsEx pattern
-- parser! "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
-- leading_parser "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Name) := do
let decl := doLetArrow[2]
if decl.getKind == `Lean.Parser.Term.doIdDecl then
@ -921,10 +921,10 @@ def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFr
def reassignToTerm (reassign : Syntax) (k : Syntax) : MacroM Syntax := withRef reassign <| withFreshMacroScope do
let kind := reassign.getKind
if kind == `Lean.Parser.Term.doReassign then
-- doReassign := parser! (letIdDecl <|> letPatDecl)
-- doReassign := leading_parser (letIdDecl <|> letPatDecl)
let arg := reassign[0]
if arg.getKind == `Lean.Parser.Term.letIdDecl then
-- letIdDecl := parser! ident >> many (ppSpace >> bracketedBinder) >> optType >> " := " >> termParser
-- letIdDecl := leading_parser ident >> many (ppSpace >> bracketedBinder) >> optType >> " := " >> termParser
let x := arg[0]
let val := arg[4]
let newVal ← `(ensureTypeOf! $x $(quote "invalid reassignment, value") $val)
@ -1207,8 +1207,8 @@ mutual
```
where
```
def doIdDecl := parser! ident >> optType >> leftArrow >> doElemParser
def doPatDecl := parser! termParser >> leftArrow >> doElemParser >> optional (" | " >> doElemParser)
def doIdDecl := leading_parser ident >> optType >> leftArrow >> doElemParser
def doPatDecl := leading_parser termParser >> leftArrow >> doElemParser >> optional (" | " >> doElemParser)
```
-/
partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
@ -1304,8 +1304,8 @@ mutual
/- Generate `CodeBlock` for `doFor; doElems`
`doFor` is of the form
```
def doForDecl := parser! termParser >> " in " >> withForbidden "do" termParser
def doFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
```
-/
partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
@ -1391,10 +1391,10 @@ mutual
/--
Generate `CodeBlock` for `doTry; doElems`
```
def doTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
def doCatch := parser! "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
def doCatchMatch := parser! "catch " >> doMatchAlts
def doFinally := parser! "finally " >> doSeq
def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
def doCatch := leading_parser "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser "catch " >> doMatchAlts
def doFinally := leading_parser "finally " >> doSeq
```
-/
partial def doTryToCode (doTry : Syntax) (doElems: List Syntax) : M CodeBlock := do

18
stage0/src/Lean/Elab/Match.lean generated
View file

@ -16,9 +16,9 @@ open Lean.Parser.Term
/- This modules assumes "match"-expressions use the following syntax.
```lean
def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
def matchDiscr := leading_parser optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
def «match» := leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
```
-/
@ -304,7 +304,7 @@ partial def collect (stx : Syntax) : M Syntax := do
else if k == `Lean.Parser.Term.structInst then
/-
```
parser! "{" >> optional (atomic (termParser >> " with "))
leading_parser "{" >> optional (atomic (termParser >> " with "))
>> manyIndent (group (structInstField >> optional ", "))
>> optional ".."
>> optional (" : " >> termParser)
@ -317,7 +317,7 @@ partial def collect (stx : Syntax) : M Syntax := do
let fields ← args[2].getArgs.mapM fun p => do
-- p is of the form (group (structInstField >> optional ", "))
let field := p[0]
-- parser! structInstLVal >> " := " >> termParser
-- leading_parser structInstLVal >> " := " >> termParser
let newVal ← collect field[2]
let field := field.setArg 2 newVal
pure <| field.setArg 0 field
@ -353,7 +353,7 @@ partial def collect (stx : Syntax) : M Syntax := do
processCtor stx[0]
else if k == `Lean.Parser.Term.namedPattern then
/- Recall that
def namedPattern := check... >> tparser! "@" >> termParser -/
def namedPattern := check... >> trailing_parser "@" >> termParser -/
let id := stx[0]
discard <| processVar id
let pat := stx[2]
@ -820,7 +820,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
pure (matchStx.setArg 1 discrs)
| discr :: discrs =>
-- Recall that
-- matchDiscr := parser! optional (ident >> ":") >> termParser
-- matchDiscr := leading_parser optional (ident >> ":") >> termParser
let term := discr[1]
match (← isLocalIdent? term) with
| some _ => loop discrs (discrsNew.push discr)
@ -894,7 +894,7 @@ private def waitExpectedTypeAndDiscrs (matchStx : Syntax) (expectedType? : Optio
/-
```
parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
```
Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
-/
@ -918,7 +918,7 @@ where
isAtomicIdent (stx : Syntax) : Bool :=
stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
-- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
-- leading_parser "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
match stx with
| `(match $discr:term with | $y:ident => $rhs:term) =>
@ -940,7 +940,7 @@ where
builtin_initialize
registerTraceClass `Elab.match
-- parser!:leadPrec "nomatch " >> termParser
-- leading_parser:leadPrec "nomatch " >> termParser
@[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? =>
match stx with
| `(nomatch $discrExpr) => do

4
stage0/src/Lean/Elab/MutualDef.lean generated
View file

@ -154,8 +154,8 @@ private def expandWhereDeclsAsStructInst : Macro
/-
Recall that
```
def declValSimple := parser! " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := parser! Term.matchAltsWhereDecls
def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
```
-/

14
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -86,7 +86,7 @@ private def getStructSource (stx : Syntax) : TermElabM Source :=
/-
We say a `{ ... }` notation is a `modifyOp` if it contains only one
```
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
-/
private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
@ -95,8 +95,8 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
let arg := p[0]
/- Remark: the syntax for `structInstField` is
```
def structInstLVal := parser! (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstField := parser! structInstLVal >> " := " >> termParser
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstField := leading_parser structInstLVal >> " := " >> termParser
```
-/
let lval := arg[0]
@ -255,9 +255,9 @@ instance : ToString (Field Struct) := ⟨toString ∘ format⟩
/-
Recall that `structInstField` elements have the form
```
def structInstField := parser! structInstLVal >> " := " >> termParser
def structInstLVal := parser! (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstField := leading_parser structInstLVal >> " := " >> termParser
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
-/
-- Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName`
@ -293,7 +293,7 @@ private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : Except String Struct := do
/- Recall that `stx` is of the form
```
parser! "{" >> optional (atomic (termParser >> " with "))
leading_parser "{" >> optional (atomic (termParser >> " with "))
>> manyIndent (group (structInstField >> optional ", "))
>> optional ".."
>> optional (" : " >> termParser)

26
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -18,7 +18,7 @@ open Meta
/- Recall that the `structure command syntax is
```
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
```
-/
@ -96,7 +96,7 @@ private def defaultCtorName := `mk
/-
The structure constructor syntax is
```
parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
leading_parser try (declModifiers >> ident >> optional inferMod >> " :: ")
```
-/
private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM StructCtorView := do
@ -141,11 +141,11 @@ def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
/-
```
def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := parser! atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structFields := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
```
-/
private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) :=
@ -180,7 +180,7 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
let optBinderDefault := fieldBinder[5]
if optBinderDefault.isNone then none
else
-- binderDefault := parser! " := " >> termParser
-- binderDefault := leading_parser " := " >> termParser
some optBinderDefault[0][1]
let idents := fieldBinder[2].getArgs
idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
@ -527,15 +527,15 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
addDefaults lctx defaultAuxDecls
/-
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields >> optDeriving
leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields >> optDeriving
where
def «extends» := parser! " extends " >> sepBy1 termParser ", "
def typeSpec := parser! " : " >> termParser
def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
def structCtor := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
def structFields := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
def structCtor := leading_parser try (declModifiers >> ident >> optional inferMod >> " :: ")
-/
def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do

10
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -9,7 +9,7 @@ import Lean.Parser.Syntax
namespace Lean.Elab.Term
/-
Expand `optional «precedence»` where
«precedence» := parser! " : " >> precedenceParser -/
«precedence» := leading_parser " : " >> precedenceParser -/
def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) :=
if stx.isNone then
return none
@ -284,7 +284,7 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
kind == `Lean.Parser.Syntax.atom
/-
def «syntax» := parser! attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
def «syntax» := leading_parser attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
-/
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
let env ← getEnv
@ -329,7 +329,7 @@ def «syntax» := parser! attrKind >> "syntax " >> optPrecedence >> optName
withMacroExpansion stx d <| elabCommand d
/-
def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
-/
@[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do
let declName := stx[1]
@ -541,7 +541,7 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do
mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]
/- «macro» := parser! suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/
/- «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/
def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
let attrKind := stx[0]
let prec := stx[2].getOptional?
@ -592,7 +592,7 @@ builtin_initialize
/-
def elabTail := try (" : " >> ident) >> darrow >> termParser
def «elab» := parser! suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
def «elab» := leading_parser suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
-/
def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
let ref := stx

6
stage0/src/Lean/Elab/Tactic/Induction.lean generated
View file

@ -243,7 +243,7 @@ end ElimApp
Recall that
```
generalizingVars := optional (" generalizing " >> many1 ident)
«induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> optional inductionAlts
«induction» := leading_parser nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> optional inductionAlts
```
`stx` is syntax for `induction`. -/
private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
@ -343,7 +343,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
appendGoals result.others.toList
-- Recall that
-- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
-- majorPremise := leading_parser optional (try (ident >> " : ")) >> termParser
private def getTargetHypothesisName? (target : Syntax) : Option Name :=
if target[0].isNone then
none
@ -377,7 +377,7 @@ def elabTargets (targets : Array Syntax) : TacticM (Array Expr) :=
builtin_initialize registerTraceClass `Elab.cases
@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focus do
-- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
-- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
let targets ← elabTargets stx[1].getSepArgs
let optInductionAlts := stx[3]
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts

2
stage0/src/Lean/Elab/Tactic/Injection.lean generated
View file

@ -19,7 +19,7 @@ private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Uni
Meta.throwTacticEx `injection mvarId m!"too many identifiers provided, unused: {unusedIds}"
@[builtinTactic «injection»] def evalInjection : Tactic := fun stx => do
-- parser! nonReservedSymbol "injection " >> termParser >> withIds
-- leading_parser nonReservedSymbol "injection " >> termParser >> withIds
let fvarId ← elabAsFVar stx[1]
let ids := getInjectionNewIds stx[2]
liftMetaTactic fun mvarId => do

8
stage0/src/Lean/Elab/Tactic/Location.lean generated
View file

@ -13,10 +13,10 @@ inductive Location where
/-
Recall that
```
def locationWildcard := parser! "*"
def locationTarget := parser! unicodeSymbol "⊢" "|-"
def locationHyp := parser! many1 ident
def location := parser! "at " >> (locationWildcard <|> locationTarget <|> locationHyp)
def locationWildcard := leading_parser "*"
def locationTarget := leading_parser unicodeSymbol "⊢" "|-"
def locationHyp := leading_parser many1 ident
def location := leading_parser "at " >> (locationWildcard <|> locationTarget <|> locationHyp)
```
-/
def expandLocation (stx : Syntax) : Location :=

4
stage0/src/Lean/Elab/Tactic/Rewrite.lean generated
View file

@ -75,8 +75,8 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
/-
```
def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser
def «rewrite» := parser! "rewrite" >> rwRule >> optional location
def rwRule := leading_parser optional (unicodeSymbol "←" "<-") >> termParser
def «rewrite» := leading_parser "rewrite" >> rwRule >> optional location
```
-/
@[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic :=

2
stage0/src/Lean/Meta/RecursorInfo.lean generated
View file

@ -238,7 +238,7 @@ private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) :
| _ => throwError! "invalid user defined recursor '{declName}', type of the major premise must be of the form (I ...), where I is a constant"
/-
@[builtinAttrParser] def «recursor» := parser! "recursor " >> numLit
@[builtinAttrParser] def «recursor» := leading_parser "recursor " >> numLit
-/
def Attribute.Recursor.getMajorPos (stx : Syntax) : AttrM Nat := do
if stx.getKind == `Lean.Parser.Attr.recursor then

18
stage0/src/Lean/Parser/Attr.lean generated
View file

@ -32,19 +32,19 @@ end Priority
namespace Attr
@[builtinAttrParser] def simple := parser! ident >> optional (priorityParser <|> ident)
@[builtinAttrParser] def simple := leading_parser ident >> optional (priorityParser <|> ident)
/- Remark, We can't use `simple` for `class`, `instance`, `export`, and `macro` because they are keywords. -/
@[builtinAttrParser] def «macro» := parser! "macro " >> ident
@[builtinAttrParser] def «export» := parser! "export " >> ident
@[builtinAttrParser] def «macro» := leading_parser "macro " >> ident
@[builtinAttrParser] def «export» := leading_parser "export " >> ident
/- We don't use `simple` for recursor because the argument is not a priority-/
@[builtinAttrParser] def recursor := parser! nonReservedSymbol "recursor " >> numLit
@[builtinAttrParser] def «class» := parser! "class"
@[builtinAttrParser] def «instance» := parser! "instance" >> optional priorityParser
@[builtinAttrParser] def defaultInstance := parser! nonReservedSymbol "defaultInstance " >> optional priorityParser
@[builtinAttrParser] def recursor := leading_parser nonReservedSymbol "recursor " >> numLit
@[builtinAttrParser] def «class» := leading_parser "class"
@[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser
@[builtinAttrParser] def defaultInstance := leading_parser nonReservedSymbol "defaultInstance " >> optional priorityParser
def externEntry := parser! optional ident >> optional (nonReservedSymbol "inline ") >> strLit
@[builtinAttrParser] def extern := parser! nonReservedSymbol "extern " >> optional numLit >> many externEntry
def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit
@[builtinAttrParser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry
end Attr

2
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -28,7 +28,7 @@ constructing and deconstructing countless monadic return values. Instead of expl
push (zero or more of) them onto a syntax stack inside the linear state. Chaining parsers via `>>` accumulates their
output on the stack. Combinators such as `node` then pop off all syntax objects produced during their invocation and
wrap them in a single `Syntax.node` object that is again pushed on this stack. Instead of calling `node` directly, we
usually use the macro `parser! p`, which unfolds to `node k p` where the new syntax node kind `k` is the name of the
usually use the macro `leading_parser p`, which unfolds to `node k p` where the new syntax node kind `k` is the name of the
declaration being defined.
The lack of a dedicated lexer ensures we can modify and replace the lexical grammar at any point, and simplifies

154
stage0/src/Lean/Parser/Command.lean generated
View file

@ -15,110 +15,110 @@ namespace Parser
Multiple command will be put in a `null node, but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator). -/
-- TODO: use two separate quotation parsers with parser priorities instead
@[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")"
@[builtinTermParser] def Term.quot := leading_parser "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")"
namespace Command
def namedPrio := parser! (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")")
def namedPrio := leading_parser (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")")
def optNamedPrio := optional namedPrio
def «private» := parser! "private "
def «protected» := parser! "protected "
def «private» := leading_parser "private "
def «protected» := leading_parser "protected "
def visibility := «private» <|> «protected»
def «noncomputable» := parser! "noncomputable "
def «unsafe» := parser! "unsafe "
def «partial» := parser! "partial "
def declModifiers (inline : Bool) := parser! optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
def declId := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := parser! many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := parser! many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := parser! " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := parser! Term.matchAltsWhereDecls
def «noncomputable» := leading_parser "noncomputable "
def «unsafe» := leading_parser "unsafe "
def «partial» := leading_parser "partial "
def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
def declId := leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
def «abbrev» := parser! "abbrev " >> declId >> optDeclSig >> declVal
def «def» := parser! "def " >> declId >> optDeclSig >> declVal
def «theorem» := parser! "theorem " >> declId >> declSig >> declVal
def «constant» := parser! "constant " >> declId >> declSig >> optional declValSimple
def «instance» := parser! Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
def «axiom» := parser! "axiom " >> declId >> declSig
def «example» := parser! "example " >> declSig >> declVal
def inferMod := parser! atomic (symbol "{" >> "}")
def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
def optDeriving := parser! optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def classInductive := parser! atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := parser! atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structFields := parser! manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structCtor := parser! atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
def structureTk := parser! "structure "
def classTk := parser! "class "
def «extends» := parser! " extends " >> sepBy1 termParser ", "
def «structure» := parser!
def «abbrev» := leading_parser "abbrev " >> declId >> optDeclSig >> declVal
def «def» := leading_parser "def " >> declId >> optDeclSig >> declVal
def «theorem» := leading_parser "theorem " >> declId >> declSig >> declVal
def «constant» := leading_parser "constant " >> declId >> declSig >> optional declValSimple
def «instance» := leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
def «axiom» := leading_parser "axiom " >> declId >> declSig
def «example» := leading_parser "example " >> declSig >> declVal
def inferMod := leading_parser atomic (symbol "{" >> "}")
def ctor := leading_parser "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
def optDeriving := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
def «inductive» := leading_parser "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def classInductive := leading_parser atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structFields := leading_parser manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structCtor := leading_parser atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
def structureTk := leading_parser "structure "
def classTk := leading_parser "class "
def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
def «structure» := leading_parser
(structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType
>> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
>> optDeriving
@[builtinCommandParser] def declaration := parser!
@[builtinCommandParser] def declaration := leading_parser
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
@[builtinCommandParser] def «deriving» := parser! "deriving " >> "instance " >> sepBy1 ident ", " >> " for " >> sepBy1 ident ", "
@[builtinCommandParser] def «section» := parser! "section " >> optional ident
@[builtinCommandParser] def «namespace» := parser! "namespace " >> ident
@[builtinCommandParser] def «end» := parser! "end " >> optional ident
@[builtinCommandParser] def «variable» := parser! "variable" >> many1 Term.bracketedBinder
@[builtinCommandParser] def «universe» := parser! "universe " >> ident
@[builtinCommandParser] def «universes» := parser! "universes " >> many1 ident
@[builtinCommandParser] def check := parser! "#check " >> termParser
@[builtinCommandParser] def check_failure := parser! "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtinCommandParser] def reduce := parser! "#reduce " >> termParser
@[builtinCommandParser] def eval := parser! "#eval " >> termParser
@[builtinCommandParser] def synth := parser! "#synth " >> termParser
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def print := parser! "#print " >> (ident <|> strLit)
@[builtinCommandParser] def printAxioms := parser! "#print " >> nonReservedSymbol "axioms " >> ident
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
@[builtinCommandParser] def «deriving» := leading_parser "deriving " >> "instance " >> sepBy1 ident ", " >> " for " >> sepBy1 ident ", "
@[builtinCommandParser] def «section» := leading_parser "section " >> optional ident
@[builtinCommandParser] def «namespace» := leading_parser "namespace " >> ident
@[builtinCommandParser] def «end» := leading_parser "end " >> optional ident
@[builtinCommandParser] def «variable» := leading_parser "variable" >> many1 Term.bracketedBinder
@[builtinCommandParser] def «universe» := leading_parser "universe " >> ident
@[builtinCommandParser] def «universes» := leading_parser "universes " >> many1 ident
@[builtinCommandParser] def check := leading_parser "#check " >> termParser
@[builtinCommandParser] def check_failure := leading_parser "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtinCommandParser] def reduce := leading_parser "#reduce " >> termParser
@[builtinCommandParser] def eval := leading_parser "#eval " >> termParser
@[builtinCommandParser] def synth := leading_parser "#synth " >> termParser
@[builtinCommandParser] def exit := leading_parser "#exit"
@[builtinCommandParser] def print := leading_parser "#print " >> (ident <|> strLit)
@[builtinCommandParser] def printAxioms := leading_parser "#print " >> nonReservedSymbol "axioms " >> ident
@[builtinCommandParser] def «resolve_name» := leading_parser "#resolve_name " >> ident
@[builtinCommandParser] def «init_quot» := leading_parser "init_quot"
def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> ppSpace >> optionValue
def eraseAttr := parser! "-" >> ident
@[builtinCommandParser] def «attribute» := parser! "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := parser! atomic (ident >> "hiding") >> many1 ident
def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
def openRenaming := parser! atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := parser! atomic (ident >> "(") >> many1 ident >> ")"
def openSimple := parser! many1 ident
@[builtinCommandParser] def «set_option» := leading_parser "set_option " >> ident >> ppSpace >> optionValue
def eraseAttr := leading_parser "-" >> ident
@[builtinCommandParser] def «attribute» := leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := leading_parser "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := leading_parser atomic (ident >> "hiding") >> many1 ident
def openRenamingItem := leading_parser ident >> unicodeSymbol "→" "->" >> ident
def openRenaming := leading_parser atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := leading_parser atomic (ident >> "(") >> many1 ident >> ")"
def openSimple := leading_parser many1 ident
def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple
@[builtinCommandParser] def «open» := parser! "open " >> openDecl
@[builtinCommandParser] def «open» := leading_parser "open " >> openDecl
@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end")
@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «builtin_initialize» := parser! "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end")
@[builtinCommandParser] def «initialize» := leading_parser "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «builtin_initialize» := leading_parser "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «in» := tparser! " in " >> commandParser
@[builtinCommandParser] def «in» := trailing_parser " in " >> commandParser
@[runBuiltinParserAttributeHooks] abbrev declModifiersF := declModifiers false
@[runBuiltinParserAttributeHooks] abbrev declModifiersT := declModifiers true
builtin_initialize
registerParserAlias! "declModifiers" declModifiersF
registerParserAlias! "nestedDeclModifiers" declModifiersT
registerParserAlias! "declId" declId
registerParserAlias! "declSig" declSig
registerParserAlias! "optDeclSig" optDeclSig
registerParserAlias! "openDecl" openDecl
register_parser_alias "declModifiers" declModifiersF
register_parser_alias "nestedDeclModifiers" declModifiersT
register_parser_alias "declId" declId
register_parser_alias "declSig" declSig
register_parser_alias "optDeclSig" optDeclSig
register_parser_alias "openDecl" openDecl
end Command
namespace Term
@[builtinTermParser] def «open» := parser!:leadPrec "open " >> Command.openDecl >> " in " >> termParser
@[builtinTermParser] def «set_option» := parser!:leadPrec "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
@[builtinTermParser] def «open» := leading_parser:leadPrec "open " >> Command.openDecl >> " in " >> termParser
@[builtinTermParser] def «set_option» := leading_parser:leadPrec "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> termParser
end Term
namespace Tactic
@[builtinTacticParser] def «open» := parser!:leadPrec "open " >> Command.openDecl >> " in " >> tacticSeq
@[builtinTacticParser] def «set_option» := parser!:leadPrec "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
@[builtinTacticParser] def «open» := leading_parser:leadPrec "open " >> Command.openDecl >> " in " >> tacticSeq
@[builtinTacticParser] def «set_option» := leading_parser:leadPrec "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
end Tactic
end Parser

76
stage0/src/Lean/Parser/Do.lean generated
View file

@ -16,11 +16,11 @@ builtin_initialize registerBuiltinDynamicParserAttribute `doElemParser `doElem
namespace Term
def leftArrow : Parser := unicodeSymbol " ← " " <- "
@[builtinTermParser] def liftMethod := parser!:minPrec leftArrow >> termParser
@[builtinTermParser] def liftMethod := leading_parser:minPrec leftArrow >> termParser
def doSeqItem := parser! ppLine >> doElemParser >> optional "; "
def doSeqIndent := parser! many1Indent doSeqItem
def doSeqBracketed := parser! "{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
def doSeqItem := leading_parser ppLine >> doElemParser >> optional "; "
def doSeqIndent := leading_parser many1Indent doSeqItem
def doSeqBracketed := leading_parser "{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
def termBeforeDo := withForbidden "do" termParser
@ -28,28 +28,28 @@ def termBeforeDo := withForbidden "do" termParser
attribute [runBuiltinParserAttributeHooks] doSeq termBeforeDo
builtin_initialize
registerParserAlias! "doSeq" doSeq
registerParserAlias! "termBeforeDo" termBeforeDo
register_parser_alias "doSeq" doSeq
register_parser_alias "termBeforeDo" termBeforeDo
def notFollowedByRedefinedTermToken :=
-- Remark: we don't currently support `open` and `set_option` in `do`-blocks, but we include them in the following list to fix the ambiguity
-- "open" command following `do`-block. If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
@[builtinDoElemParser] def doLet := parser! "let " >> optional "mut " >> letDecl
@[builtinDoElemParser] def doLet := leading_parser "let " >> optional "mut " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := parser! atomic (ident >> optType >> leftArrow) >> doElemParser
def doPatDecl := parser! atomic (termParser >> leftArrow) >> doElemParser >> optional (checkColGt >> " | " >> doElemParser)
@[builtinDoElemParser] def doLetArrow := parser! withPosition ("let " >> optional "mut " >> (doIdDecl <|> doPatDecl))
@[builtinDoElemParser] def doLetRec := leading_parser group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := leading_parser atomic (ident >> optType >> leftArrow) >> doElemParser
def doPatDecl := leading_parser atomic (termParser >> leftArrow) >> doElemParser >> optional (checkColGt >> " | " >> doElemParser)
@[builtinDoElemParser] def doLetArrow := leading_parser withPosition ("let " >> optional "mut " >> (doIdDecl <|> doPatDecl))
-- We use `letIdDeclNoBinders` to define `doReassign`.
-- Motivation: we do not reassign functions, and avoid parser conflict
def letIdDeclNoBinders := node `Lean.Parser.Term.letIdDecl $ atomic (ident >> pushNone >> optType >> " := ") >> termParser
@[builtinDoElemParser] def doReassign := parser! notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl)
@[builtinDoElemParser] def doHave := parser! "have " >> Term.haveDecl
@[builtinDoElemParser] def doReassign := leading_parser notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtinDoElemParser] def doReassignArrow := leading_parser notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl)
@[builtinDoElemParser] def doHave := leading_parser "have " >> Term.haveDecl
/-
In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as
```
@ -81,32 +81,32 @@ else if c_2 then
-/
def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if ")))
-- ensure `if $e then ...` still binds to `e:term`
def doIfLetPure := parser! " := " >> termParser
def doIfLetBind := parser! " ← " >> termParser
def doIfLetPure := leading_parser " := " >> termParser
def doIfLetBind := leading_parser " ← " >> termParser
def doIfLet := nodeWithAntiquot "doIfLet" `Lean.Parser.Term.doIfLet <| "let " >> termParser >> (doIfLetPure <|> doIfLetBind)
def doIfProp := nodeWithAntiquot "doIfProp" `Lean.Parser.Term.doIfProp <| optIdent >> termParser
def doIfCond := withAntiquot (mkAntiquot "doIfCond" none (anonymous := false)) <| doIfLet <|> doIfProp
@[builtinDoElemParser] def doIf := parser! withPosition $
@[builtinDoElemParser] def doIf := leading_parser withPosition $
"if " >> doIfCond >> " then " >> doSeq
>> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> doIfCond >> " then " >> doSeq))
>> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
@[builtinDoElemParser] def doUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq
def doForDecl := parser! termParser >> " in " >> withForbidden "do" termParser
@[builtinDoElemParser] def doFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtinDoElemParser] def doUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
@[builtinDoElemParser] def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doMatchAlts := matchAlts (rhsParser := doSeq)
@[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
@[builtinDoElemParser] def doMatch := leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
def doCatch := parser! atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatchMatch := parser! "catch " >> doMatchAlts
def doFinally := parser! "finally " >> doSeq
@[builtinDoElemParser] def doTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
def doCatch := leading_parser atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser "catch " >> doMatchAlts
def doFinally := leading_parser "finally " >> doSeq
@[builtinDoElemParser] def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
@[builtinDoElemParser] def doBreak := parser! "break"
@[builtinDoElemParser] def doContinue := parser! "continue"
@[builtinDoElemParser] def doReturn := parser!:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtinDoElemParser] def doDbgTrace := parser!:leadPrec "dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)
@[builtinDoElemParser] def doAssert := parser!:leadPrec "assert! " >> termParser
@[builtinDoElemParser] def doBreak := leading_parser "break"
@[builtinDoElemParser] def doContinue := leading_parser "continue"
@[builtinDoElemParser] def doReturn := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtinDoElemParser] def doDbgTrace := leading_parser:leadPrec "dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)
@[builtinDoElemParser] def doAssert := leading_parser:leadPrec "assert! " >> termParser
/-
We use `notFollowedBy` to avoid counterintuitive behavior. For example, the `if`-term parser
@ -114,18 +114,18 @@ doesn't enforce indentation restrictions, but we don't want it to be used when `
Note that parser priorities would not solve this problem since the `doIf` parser is failing while the `if`
parser is succeeding.
-/
@[builtinDoElemParser] def doExpr := parser! notFollowedByRedefinedTermToken >> termParser
@[builtinDoElemParser] def doNested := parser! "do " >> doSeq
@[builtinDoElemParser] def doExpr := leading_parser notFollowedByRedefinedTermToken >> termParser
@[builtinDoElemParser] def doNested := leading_parser "do " >> doSeq
@[builtinTermParser] def «do» := parser!:maxPrec "do " >> doSeq
@[builtinTermParser] def «do» := leading_parser:maxPrec "do " >> doSeq
@[builtinTermParser] def doElem.quot : Parser := parser! "`(doElem|" >> toggleInsideQuot doElemParser >> ")"
@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> toggleInsideQuot doElemParser >> ")"
/- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
@[builtinTermParser] def termUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtinTermParser] def termFor := parser! "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtinTermParser] def termTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
@[builtinTermParser] def termReturn := parser!:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtinTermParser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtinTermParser] def termFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtinTermParser] def termTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
@[builtinTermParser] def termReturn := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
end Term
end Parser

16
stage0/src/Lean/Parser/Extra.lean generated
View file

@ -98,19 +98,19 @@ namespace Parser
attribute [runBuiltinParserAttributeHooks]
ppHardSpace ppSpace ppLine ppGroup ppIndent ppDedent
macro "registerParserAlias!" aliasName:strLit declName:ident : term =>
macro "register_parser_alias" aliasName:strLit declName:ident : term =>
`(do Parser.registerAlias $aliasName $declName
PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
builtin_initialize
registerParserAlias! "group" group
registerParserAlias! "ppHardSpace" ppHardSpace
registerParserAlias! "ppSpace" ppSpace
registerParserAlias! "ppLine" ppLine
registerParserAlias! "ppGroup" ppGroup
registerParserAlias! "ppIndent" ppIndent
registerParserAlias! "ppDedent" ppDedent
register_parser_alias "group" group
register_parser_alias "ppHardSpace" ppHardSpace
register_parser_alias "ppSpace" ppSpace
register_parser_alias "ppLine" ppLine
register_parser_alias "ppGroup" ppGroup
register_parser_alias "ppIndent" ppIndent
register_parser_alias "ppDedent" ppDedent
end Parser

10
stage0/src/Lean/Parser/Level.lean generated
View file

@ -16,13 +16,13 @@ builtin_initialize
namespace Level
@[builtinLevelParser] def paren := parser! "(" >> levelParser >> ")"
@[builtinLevelParser] def max := parser! nonReservedSymbol "max" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtinLevelParser] def imax := parser! nonReservedSymbol "imax" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtinLevelParser] def hole := parser! "_"
@[builtinLevelParser] def paren := leading_parser "(" >> levelParser >> ")"
@[builtinLevelParser] def max := leading_parser nonReservedSymbol "max" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtinLevelParser] def imax := leading_parser nonReservedSymbol "imax" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtinLevelParser] def hole := leading_parser "_"
@[builtinLevelParser] def num := checkPrec maxPrec >> numLit
@[builtinLevelParser] def ident := checkPrec maxPrec >> Parser.ident
@[builtinLevelParser] def addLit := tparser!:65 " + " >> numLit
@[builtinLevelParser] def addLit := trailing_parser:65 " + " >> numLit
end Level

8
stage0/src/Lean/Parser/Module.lean generated
View file

@ -10,15 +10,15 @@ namespace Lean
namespace Parser
namespace Module
def «prelude» := parser! "prelude"
def «import» := parser! "import " >> optional "runtime" >> ident
def header := parser! optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine
def «prelude» := leading_parser "prelude"
def «import» := leading_parser "import " >> optional "runtime" >> ident
def header := leading_parser optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine
/--
Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. -/
@[runBuiltinParserAttributeHooks]
def module := parser! header >> many (commandParser >> ppLine >> ppLine)
def module := leading_parser header >> many (commandParser >> ppLine >> ppLine)
def updateTokens (c : ParserContext) : ParserContext :=
{ c with

60
stage0/src/Lean/Parser/Syntax.lean generated
View file

@ -23,70 +23,70 @@ builtin_initialize
@[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
categoryParser `stx rbp
def «precedence» := parser! ":" >> precedenceParser maxPrec
def «precedence» := leading_parser ":" >> precedenceParser maxPrec
def optPrecedence := optional (atomic «precedence»)
namespace Syntax
@[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence
@[builtinSyntaxParser] def unary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def binary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def sepBy := parser! "sepBy(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtinSyntaxParser] def sepBy1 := parser! "sepBy1(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtinSyntaxParser] def atom := parser! strLit
@[builtinSyntaxParser] def nonReserved := parser! "&" >> strLit
@[builtinSyntaxParser] def paren := leading_parser "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := leading_parser ident >> optPrecedence
@[builtinSyntaxParser] def unary := leading_parser ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def binary := leading_parser ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def sepBy := leading_parser "sepBy(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtinSyntaxParser] def sepBy1 := leading_parser "sepBy1(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtinSyntaxParser] def atom := leading_parser strLit
@[builtinSyntaxParser] def nonReserved := leading_parser "&" >> strLit
end Syntax
namespace Term
@[builtinTermParser] def stx.quot : Parser := parser! "`(stx|" >> toggleInsideQuot syntaxParser >> ")"
@[builtinTermParser] def prec.quot : Parser := parser! "`(prec|" >> toggleInsideQuot precedenceParser >> ")"
@[builtinTermParser] def prio.quot : Parser := parser! "`(prio|" >> toggleInsideQuot priorityParser >> ")"
@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|" >> toggleInsideQuot syntaxParser >> ")"
@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|" >> toggleInsideQuot precedenceParser >> ")"
@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|" >> toggleInsideQuot priorityParser >> ")"
end Term
namespace Command
def namedName := parser! (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")")
def namedName := leading_parser (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")")
def optNamedName := optional namedName
def «prefix» := parser! "prefix"
def «infix» := parser! "infix"
def «infixl» := parser! "infixl"
def «infixr» := parser! "infixr"
def «postfix» := parser! "postfix"
def «prefix» := leading_parser "prefix"
def «infix» := leading_parser "infix"
def «infixl» := leading_parser "infixl"
def «infixr» := leading_parser "infixr"
def «postfix» := leading_parser "postfix"
def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
@[builtinCommandParser] def «mixfix» := parser! Term.attrKind >> mixfixKind >> optPrecedence >> optNamedName >> optNamedPrio >> ppSpace >> strLit >> darrow >> termParser
@[builtinCommandParser] def «mixfix» := leading_parser Term.attrKind >> mixfixKind >> optPrecedence >> optNamedName >> optNamedPrio >> ppSpace >> strLit >> darrow >> termParser
-- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
-- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
def identPrec := parser! ident >> optPrecedence
def identPrec := leading_parser ident >> optPrecedence
def optKind : Parser := optional ("[" >> ident >> "]")
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := parser! Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := parser! Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArgSymbol := parser! strLit >> optional (atomic <| checkNoWsBefore >> "%" >> checkNoWsBefore >> ident)
@[builtinCommandParser] def «notation» := leading_parser Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident
def macroArgSimple := leading_parser ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArgSymbol := leading_parser strLit >> optional (atomic <| checkNoWsBefore >> "%" >> checkNoWsBefore >> ident)
def macroArg := macroArgSymbol <|> atomic macroArgSimple
def macroHead := macroArg
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
@[builtinCommandParser] def «macro» := parser! suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
@[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
@[builtinCommandParser] def «elab_rules» := parser! suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
@[builtinCommandParser] def «elab_rules» := leading_parser suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
def elabHead := macroHead
def elabArg := macroArg
def elabTail := atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
@[builtinCommandParser] def «elab» := parser! suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
@[builtinCommandParser] def «elab» := leading_parser suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
end Command

14
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -10,21 +10,21 @@ namespace Parser
namespace Tactic
builtin_initialize
registerParserAlias! "tacticSeq" tacticSeq
register_parser_alias "tacticSeq" tacticSeq
@[builtinTacticParser] def «unknown» := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtinTacticParser] def «unknown» := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
/- Auxiliary parser for expanding `match` tactic -/
@[builtinTacticParser] def eraseAuxDiscrs := parser!:maxPrec "eraseAuxDiscrs!"
@[builtinTacticParser] def eraseAuxDiscrs := leading_parser:maxPrec "eraseAuxDiscrs!"
def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq
def matchAlts := Term.matchAlts (rhsParser := matchRhs)
@[builtinTacticParser] def «match» := parser!:leadPrec "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def introMatch := parser! nonReservedSymbol "intro " >> matchAlts
@[builtinTacticParser] def «match» := leading_parser:leadPrec "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def introMatch := leading_parser nonReservedSymbol "intro " >> matchAlts
@[builtinTacticParser] def decide := parser! nonReservedSymbol "decide"
@[builtinTacticParser] def nativeDecide := parser! nonReservedSymbol "nativeDecide"
@[builtinTacticParser] def decide := leading_parser nonReservedSymbol "decide"
@[builtinTacticParser] def nativeDecide := leading_parser nonReservedSymbol "nativeDecide"
end Tactic
end Parser

200
stage0/src/Lean/Parser/Term.lean generated
View file

@ -16,7 +16,7 @@ def commentBody : Parser :=
@[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
@[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
def docComment := parser! ppDedent $ "/--" >> commentBody >> ppLine
def docComment := leading_parser ppDedent $ "/--" >> commentBody >> ppLine
end Command
builtin_initialize
@ -29,9 +29,9 @@ builtin_initialize
namespace Tactic
def tacticSeq1Indented : Parser :=
parser! many1Indent (group (ppLine >> tacticParser >> optional ";"))
leading_parser many1Indent (group (ppLine >> tacticParser >> optional ";"))
def tacticSeqBracketed : Parser :=
parser! "{" >> many (group (ppLine >> tacticParser >> optional ";")) >> ppDedent (ppLine >> "}")
leading_parser "{" >> many (group (ppLine >> tacticParser >> optional ";")) >> ppDedent (ppLine >> "}")
def tacticSeq :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq (tacticSeqBracketed <|> tacticSeq1Indented)
@ -47,7 +47,7 @@ namespace Term
/- Built-in parsers -/
@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.tacticSeq
@[builtinTermParser] def byTactic := leading_parser:leadPrec "by " >> Tactic.tacticSeq
def optSemicolon (p : Parser) : Parser := ppDedent $ optional ";" >> ppLine >> p
@ -57,46 +57,46 @@ def optSemicolon (p : Parser) : Parser := ppDedent $ optional ";" >> ppLine >> p
@[builtinTermParser] def scientific : Parser := checkPrec maxPrec >> scientificLit
@[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
@[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit
@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtinTermParser] def prop := parser! "Prop"
@[builtinTermParser] def hole := parser! "_"
@[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole)
@[builtinTermParser] def «sorry» := parser! "sorry"
@[builtinTermParser] def cdot := parser! symbol "·" <|> "."
@[builtinTermParser] def emptyC := parser! "∅" <|> (symbol "{" >> "}")
def typeAscription := parser! " : " >> termParser
def tupleTail := parser! ", " >> sepBy1 termParser ", "
@[builtinTermParser] def type := leading_parser "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtinTermParser] def sort := leading_parser "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtinTermParser] def prop := leading_parser "Prop"
@[builtinTermParser] def hole := leading_parser "_"
@[builtinTermParser] def syntheticHole := leading_parser "?" >> (ident <|> hole)
@[builtinTermParser] def «sorry» := leading_parser "sorry"
@[builtinTermParser] def cdot := leading_parser symbol "·" <|> "."
@[builtinTermParser] def emptyC := leading_parser "∅" <|> (symbol "{" >> "}")
def typeAscription := leading_parser " : " >> termParser
def tupleTail := leading_parser ", " >> sepBy1 termParser ", "
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@[builtinTermParser] def paren := parser! "(" >> ppDedent (withoutPosition (withoutForbidden (optional (termParser >> parenSpecial)))) >> ")"
@[builtinTermParser] def anonymousCtor := parser! "⟨" >> sepBy termParser ", " >> "⟩"
@[builtinTermParser] def paren := leading_parser "(" >> ppDedent (withoutPosition (withoutForbidden (optional (termParser >> parenSpecial)))) >> ")"
@[builtinTermParser] def anonymousCtor := leading_parser "⟨" >> sepBy termParser ", " >> "⟩"
def optIdent : Parser := optional (atomic (ident >> " : "))
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
def fromTerm := leading_parser " from " >> termParser
def haveAssign := leading_parser " := " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@[builtinTermParser] def «have» := parser!:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
@[builtinTermParser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
def sufficesDecl := optIdent >> termParser >> (fromTerm <|> byTactic)
@[builtinTermParser] def «suffices» := parser!:leadPrec withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := parser! (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := ppGroup $ parser! structInstLVal >> " := " >> termParser
def optEllipsis := parser! optional ".."
@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (atomic (termParser >> " with "))
@[builtinTermParser] def «suffices» := leading_parser:leadPrec withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
@[builtinTermParser] def «show» := leading_parser:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
def structInstLVal := leading_parser (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := ppGroup $ leading_parser structInstLVal >> " := " >> termParser
def optEllipsis := leading_parser optional ".."
@[builtinTermParser] def structInst := leading_parser "{" >> ppHardSpace >> optional (atomic (termParser >> " with "))
>> manyIndent (group (structInstField >> optional ", "))
>> optEllipsis
>> optional (" : " >> termParser) >> " }"
def typeSpec := parser! " : " >> termParser
def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
@[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec
@[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
@[builtinTermParser] def explicit := leading_parser "@" >> termParser maxPrec
@[builtinTermParser] def inaccessible := leading_parser ".(" >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := parser! atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
def binderDefault := parser! " := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
def instBinder := ppGroup $ parser! "[" >> optIdent >> termParser >> "]"
def binderTactic := leading_parser atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
def binderDefault := leading_parser " := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ leading_parser "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := ppGroup $ leading_parser "{" >> many1 binderIdent >> binderType requireType >> "}"
def instBinder := ppGroup $ leading_parser "[" >> optIdent >> termParser >> "]"
def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" none (anonymous := false)) <|
explicitBinder requireType <|> implicitBinder requireType <|> instBinder
@ -109,17 +109,17 @@ def implicitShortBinder := node `Lean.Parser.Term.implicitBinder $ "{" >> many1
def depArrowShortPrefix := try (implicitShortBinder >> unicodeSymbol " → " " -> ")
def depArrowLongPrefix := bracketedBinder true >> unicodeSymbol " → " " -> "
def depArrowPrefix := depArrowShortPrefix <|> depArrowLongPrefix
@[builtinTermParser] def depArrow := parser! depArrowPrefix >> termParser
@[builtinTermParser] def depArrow := leading_parser depArrowPrefix >> termParser
```
Note that no changes in the elaborator are needed.
We decided to not use it because terms such as `{α} → α → α` may look too cryptic.
Note that we did not add a `explicitShortBinder` parser since `(α) → α → α` is really cryptic as a short for `(α : Type) → α → α`.
-/
@[builtinTermParser] def depArrow := parser!:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
@[builtinTermParser] def depArrow := leading_parser:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
def simpleBinder := parser! many1 binderIdent >> optType
def simpleBinder := leading_parser many1 binderIdent >> optType
@[builtinTermParser]
def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
def matchAlt (rhsParser : Parser := termParser) : Parser :=
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
@ -130,29 +130,27 @@ def matchAlt (rhsParser : Parser := termParser) : Parser :=
def matchAltExpr := matchAlt
def matchAlts (rhsParser : Parser := termParser) : Parser :=
parser! ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
leading_parser ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
def matchDiscr := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser
@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
def funSimpleBinder := atomic (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
-- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
@[builtinTermParser] def «fun» := leading_parser:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def «leading_parser» := parser!:leadPrec "leading_parser " >> optExprPrecedence >> termParser
@[builtinTermParser] def «trailing_parser» := parser!:leadPrec "trailing_parser " >> optExprPrecedence >> termParser
@[builtinTermParser] def «leading_parser» := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> termParser
@[builtinTermParser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> termParser
@[builtinTermParser] def borrowed := parser! "@&" >> termParser leadPrec
@[builtinTermParser] def quotedName := parser! nameLit
@[builtinTermParser] def doubleQuotedName := parser! "`" >> checkNoWsBefore >> nameLit
@[builtinTermParser] def borrowed := leading_parser "@&" >> termParser leadPrec
@[builtinTermParser] def quotedName := leading_parser nameLit
@[builtinTermParser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> nameLit
def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" `Lean.Parser.Term.simpleBinder (anonymous := true)
(many1 binderIdent >> pushNone)
@ -164,96 +162,96 @@ def letPatDecl := nodeWithAntiquot "letPatDecl" `Lean.Parser.Term.letPatDecl
def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
def «scoped» := parser! "scoped "
def «local» := parser! "local "
def attrKind := parser! optional («scoped» <|> «local»)
def attrInstance := ppGroup $ parser! attrKind >> attrParser
@[builtinTermParser] def «let» := leading_parser:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let!» := leading_parser:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let*» := leading_parser:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
def «scoped» := leading_parser "scoped "
def «local» := leading_parser "local "
def attrKind := leading_parser optional («scoped» <|> «local»)
def attrInstance := ppGroup $ leading_parser attrKind >> attrParser
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecl := parser! optional Command.docComment >> optional «attributes» >> letDecl
def attributes := leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecl := leading_parser optional Command.docComment >> optional «attributes» >> letDecl
def letRecDecls := sepBy1 letRecDecl ", "
@[builtinTermParser]
def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
def «letrec» := leading_parser:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
@[runBuiltinParserAttributeHooks]
def whereDecls := parser! "where " >> many1Indent (group (letRecDecl >> optional ";"))
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
@[runBuiltinParserAttributeHooks]
def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def noindex := parser! "noindex!" >> termParser maxPrec
@[builtinTermParser] def noindex := leading_parser "noindex!" >> termParser maxPrec
@[builtinTermParser] def binrel := parser! "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binrel := leading_parser "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := parser! "forIn! " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser "forIn! " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := parser! "ensureExpectedType! " >> strLit >> termParser maxPrec
@[builtinTermParser] def typeOf := leading_parser "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := leading_parser "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := leading_parser "ensureExpectedType! " >> strLit >> termParser maxPrec
def namedArgument := parser! atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := parser! ".."
@[builtinTermParser] def app := tparser!:(maxPrec-1) many1 $
def namedArgument := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := leading_parser ".."
@[builtinTermParser] def app := trailing_parser:(maxPrec-1) many1 $
checkWsBefore "expected space" >>
checkColGt "expected to be indented" >>
(namedArgument <|> ellipsis <|> termParser maxPrec)
@[builtinTermParser] def proj := tparser! checkNoWsBefore >> "." >> (fieldIdx <|> ident)
@[builtinTermParser] def arrayRef := tparser! checkNoWsBefore >> "[" >> termParser >>"]"
@[builtinTermParser] def arrow := tparser! checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@[builtinTermParser] def proj := trailing_parser checkNoWsBefore >> "." >> (fieldIdx <|> ident)
@[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
@[builtinTermParser] def arrow := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
def isIdent (stx : Syntax) : Bool :=
-- antiquotations should also be allowed where an identifier is expected
stx.isAntiquot || stx.isIdent
@[builtinTermParser] def explicitUniv : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtinTermParser] def namedPattern : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def pipeProj := tparser!:minPrec " |>. " >> (fieldIdx <|> ident)
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>. " >> (fieldIdx <|> ident)
@[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|" >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
def bracketedBinderF := bracketedBinder -- no default arg
@[builtinTermParser] def bracketedBinder.quot : Parser := parser! "`(bracketedBinder|" >> toggleInsideQuot (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := parser! "`(matchDiscr|" >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := parser! "`(attr|" >> toggleInsideQuot attrParser >> ")"
@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> toggleInsideQuot (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> toggleInsideQuot attrParser >> ")"
@[builtinTermParser] def panic := parser!:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace := parser!:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
@[builtinTermParser] def panic := leading_parser:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace := leading_parser:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtinTermParser] def assert := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
def macroArg := termParser maxPrec
def macroDollarArg := parser! "$" >> termParser 10
def macroDollarArg := leading_parser "$" >> termParser 10
def macroLastArg := macroDollarArg <|> macroArg
-- Macro for avoiding exponentially big terms when using `STWorld`
@[builtinTermParser] def stateRefT := parser! "StateRefT" >> macroArg >> macroLastArg
@[builtinTermParser] def stateRefT := leading_parser "StateRefT" >> macroArg >> macroLastArg
@[builtinTermParser] def dynamicQuot := parser! "`(" >> ident >> "|" >> toggleInsideQuot (parserOfStack 1) >> ")"
@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> toggleInsideQuot (parserOfStack 1) >> ")"
end Term
@[builtinTermParser default+1] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
@[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> toggleInsideQuot levelParser >> ")"
builtin_initialize
registerParserAlias! "letDecl" Term.letDecl
registerParserAlias! "haveDecl" Term.haveDecl
registerParserAlias! "sufficesDecl" Term.sufficesDecl
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
registerParserAlias! "matchDiscr" Term.matchDiscr
registerParserAlias! "bracketedBinder" Term.bracketedBinder
registerParserAlias! "attrKind" Term.attrKind
register_parser_alias "letDecl" Term.letDecl
register_parser_alias "haveDecl" Term.haveDecl
register_parser_alias "sufficesDecl" Term.sufficesDecl
register_parser_alias "letRecDecls" Term.letRecDecls
register_parser_alias "hole" Term.hole
register_parser_alias "syntheticHole" Term.syntheticHole
register_parser_alias "matchDiscr" Term.matchDiscr
register_parser_alias "bracketedBinder" Term.bracketedBinder
register_parser_alias "attrKind" Term.attrKind
end Parser
end Lean

4
stage0/src/Lean/ParserCompiler.lean generated
View file

@ -109,11 +109,11 @@ def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : B
let (Expr.const c' _ _) ← (compileParserExpr ctx (mkConst declName) (force := false)).run'
| unreachable!
-- We assume that for tagged parsers, the kind is equal to the declaration name. This is automatically true for parsers
-- using `parser!` or `syntax`.
-- using `leading_parser` or `syntax`.
let kind := declName
let attrName := if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name
-- Create syntax node for a simple attribute of the form
-- `def simple := parser! ident >> optional (ident <|> priorityParser)`
-- `def simple := leading_parser ident >> optional (ident <|> priorityParser)`
let stx := Syntax.node `Lean.Parser.Attr.simple #[
mkIdent attrName,
mkNullNode #[mkIdent kind]

368
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -16,7 +16,6 @@ extern "C" {
lean_object* l_Lean_mkCIdentFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_15956____closed__5;
lean_object* l_Lean_extractMacroScopes(lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabForall___spec__1___rarg(lean_object*);
@ -83,7 +82,6 @@ extern lean_object* l_instReprBool___closed__1;
lean_object* l_Lean_Elab_Term_expandHave___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_termS_x21_____closed__3;
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_expandAssert___closed__2;
lean_object* l_Lean_Elab_Term_expandEmptyC___closed__1;
lean_object* l_Lean_Elab_Term_elabParen___closed__3;
@ -117,7 +115,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserM
lean_object* l_Lean_Elab_Term_elabAnonymousCtor_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTrailingParserMacro___closed__1;
extern lean_object* l_Lean_Meta_assert___closed__1;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2;
lean_object* lean_string_utf8_byte_size(lean_object*);
extern lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__35;
@ -149,7 +146,6 @@ lean_object* l_Lean_Meta_DiscrTree_mkNoindexAnnotation(lean_object*);
lean_object* l_Lean_Elab_Term_elabParen___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabNoindex___closed__1;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_expandCDot___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTParserMacro(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_expandCDot___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabPanic___closed__10;
lean_object* l_Lean_Elab_Term_expandHave___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -175,7 +171,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserM
lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__1;
extern lean_object* l_Lean_setOptionFromString___closed__4;
@ -197,7 +192,6 @@ lean_object* l_Lean_Elab_Term_mkPairs_loop___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13868____closed__9;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__10;
lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_19491____closed__1;
lean_object* l_Lean_Elab_Term_expandHave_match__1(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1;
@ -222,7 +216,6 @@ lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__4;
lean_object* l_Lean_Elab_Term_expandHave___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux_match__2(lean_object*);
lean_object* l_Lean_Elab_Term_expandEmptyC___closed__6;
lean_object* l_Lean_Elab_Term_elabTParserMacro___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_expandSuffices(lean_object*);
lean_object* l_Lean_Elab_Term_elabNoindex(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabPanic___closed__5;
@ -262,6 +255,7 @@ lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__3;
lean_object* l___private_Init_Meta_0__Lean_quoteName(lean_object*);
lean_object* l_Lean_Syntax_mkStrLit(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTrailingParserMacro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1;
extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__1;
extern lean_object* l_Lean_instToExprUnit___lambda__1___closed__3;
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
@ -296,7 +290,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserM
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTrailingParserMacro(lean_object*);
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabStateRefT___lambda__2___closed__7;
lean_object* l_Lean_Elab_Term_expandSuffices___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabStateRefT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -321,7 +314,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_15956____closed__6;
extern lean_object* l_Lean_Syntax_mkApp___closed__1;
lean_object* l_Lean_Elab_Term_elabPanic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandSuffices___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTParserMacro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__3;
lean_object* l_Lean_Elab_Term_elabStateRefT___lambda__2___closed__3;
lean_object* l_Lean_Elab_Term_elabSorry___closed__1;
@ -331,7 +324,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParser
lean_object* l___regBuiltin_Lean_Elab_Term_expandShow(lean_object*);
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_932____closed__3;
extern lean_object* l_Lean_Elab_macroAttribute;
lean_object* l_Lean_Elab_Term_elabParserMacro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_main_module(lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__5;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28;
@ -368,12 +360,9 @@ extern lean_object* l_Lean_Parser_Term_panic___elambda__1___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__17;
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1;
extern lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_expandHave___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabParserMacro___closed__1;
extern lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabPanic___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -413,7 +402,6 @@ lean_object* l_Lean_Elab_Term_elabSubst___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTrailingParserMacro___closed__1;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__8;
lean_object* l_Lean_Elab_Term_elabPanic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1;
lean_object* l_Lean_Elab_Term_mkPairs(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__5;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_hasCDot_match__1(lean_object*);
@ -448,7 +436,6 @@ lean_object* l_Lean_Elab_Term_expandEmptyC(lean_object*, lean_object*, lean_obje
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__1;
lean_object* l_Lean_Elab_Term_expandHave_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabSorry___closed__6;
lean_object* l_Lean_Elab_Term_elabBorrowed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__6;
@ -468,7 +455,6 @@ lean_object* l_Lean_Elab_getRefPosition___at_Lean_Elab_Term_elabPanic___spec__1(
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_expandCDot_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33;
lean_object* l___regBuiltin_Lean_Elab_Term_elabBorrowed___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1;
lean_object* l_Lean_Meta_kabstract(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandHave___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_object*);
@ -3131,7 +3117,7 @@ static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Ter
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid `parser!` macro, it must be used in definitions");
x_1 = lean_mk_string("invalid `leading_parser` macro, it must be used in definitions");
return x_1;
}
}
@ -3159,7 +3145,7 @@ static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Ter
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid `parser!` macro, unexpected declaration name");
x_1 = lean_mk_string("invalid `leading_parser` macro, unexpected declaration name");
return x_1;
}
}
@ -4087,7 +4073,7 @@ lean_dec(x_4);
return x_10;
}
}
static lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -4096,173 +4082,17 @@ x_2 = l_Nat_repr(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_numLitKind;
x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1;
x_2 = l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1;
x_3 = lean_box(2);
x_4 = l_Lean_Syntax_mkLit(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; uint8_t x_10;
x_9 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2;
lean_inc(x_1);
x_10 = l_Lean_Syntax_isOfKind(x_1, x_9);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_2);
lean_dec(x_1);
x_11 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_27; uint8_t x_28;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
x_27 = l_Lean_nullKind___closed__2;
lean_inc(x_13);
x_28 = l_Lean_Syntax_isOfKind(x_13, x_27);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_box(0);
x_14 = x_29;
goto block_26;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_30 = l_Lean_Syntax_getArgs(x_13);
x_31 = lean_array_get_size(x_30);
lean_dec(x_30);
x_32 = lean_unsigned_to_nat(0u);
x_33 = lean_nat_dec_eq(x_31, x_32);
lean_dec(x_31);
if (x_33 == 0)
{
lean_object* x_34;
x_34 = lean_box(0);
x_14 = x_34;
goto block_26;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_13);
x_35 = lean_unsigned_to_nat(2u);
x_36 = l_Lean_Syntax_getArg(x_1, x_35);
lean_dec(x_1);
x_37 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2;
x_38 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux(x_37, x_36, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_38;
}
}
block_26:
{
lean_object* x_15; uint8_t x_16;
lean_dec(x_14);
x_15 = l_Lean_nullKind___closed__2;
lean_inc(x_13);
x_16 = l_Lean_Syntax_isOfKind(x_13, x_15);
if (x_16 == 0)
{
lean_object* x_17;
lean_dec(x_13);
lean_dec(x_2);
lean_dec(x_1);
x_17 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_18 = l_Lean_Syntax_getArgs(x_13);
x_19 = lean_array_get_size(x_18);
lean_dec(x_18);
x_20 = lean_unsigned_to_nat(2u);
x_21 = lean_nat_dec_eq(x_19, x_20);
lean_dec(x_19);
if (x_21 == 0)
{
lean_object* x_22;
lean_dec(x_13);
lean_dec(x_2);
lean_dec(x_1);
x_22 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = l_Lean_Syntax_getArg(x_13, x_12);
lean_dec(x_13);
x_24 = l_Lean_Syntax_getArg(x_1, x_20);
lean_dec(x_1);
x_25 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux(x_23, x_24, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_25;
}
}
}
}
}
}
static lean_object* _init_l_Lean_Elab_Term_elabParserMacro___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabParserMacro___lambda__1___boxed), 8, 0);
return x_1;
}
}
lean_object* l_Lean_Elab_Term_elabParserMacro(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_Elab_Term_elabParserMacro___closed__1;
x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Elab_Term_elabParserMacro___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabParserMacro), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -4316,7 +4146,7 @@ lean_dec(x_13);
x_35 = lean_unsigned_to_nat(2u);
x_36 = l_Lean_Syntax_getArg(x_1, x_35);
lean_dec(x_1);
x_37 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2;
x_37 = l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2;
x_38 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux(x_37, x_36, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_38;
}
@ -4454,7 +4284,7 @@ static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Ter
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid `tparser!` macro, it must be used in definitions");
x_1 = lean_mk_string("invalid `trailing_parser` macro, it must be used in definitions");
return x_1;
}
}
@ -4677,162 +4507,6 @@ lean_dec(x_4);
return x_10;
}
}
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; uint8_t x_10;
x_9 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
lean_inc(x_1);
x_10 = l_Lean_Syntax_isOfKind(x_1, x_9);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_2);
lean_dec(x_1);
x_11 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_27; uint8_t x_28;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
x_27 = l_Lean_nullKind___closed__2;
lean_inc(x_13);
x_28 = l_Lean_Syntax_isOfKind(x_13, x_27);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_box(0);
x_14 = x_29;
goto block_26;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_30 = l_Lean_Syntax_getArgs(x_13);
x_31 = lean_array_get_size(x_30);
lean_dec(x_30);
x_32 = lean_unsigned_to_nat(0u);
x_33 = lean_nat_dec_eq(x_31, x_32);
lean_dec(x_31);
if (x_33 == 0)
{
lean_object* x_34;
x_34 = lean_box(0);
x_14 = x_34;
goto block_26;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_13);
x_35 = lean_unsigned_to_nat(2u);
x_36 = l_Lean_Syntax_getArg(x_1, x_35);
lean_dec(x_1);
x_37 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2;
x_38 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux(x_37, x_36, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_38;
}
}
block_26:
{
lean_object* x_15; uint8_t x_16;
lean_dec(x_14);
x_15 = l_Lean_nullKind___closed__2;
lean_inc(x_13);
x_16 = l_Lean_Syntax_isOfKind(x_13, x_15);
if (x_16 == 0)
{
lean_object* x_17;
lean_dec(x_13);
lean_dec(x_2);
lean_dec(x_1);
x_17 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_18 = l_Lean_Syntax_getArgs(x_13);
x_19 = lean_array_get_size(x_18);
lean_dec(x_18);
x_20 = lean_unsigned_to_nat(2u);
x_21 = lean_nat_dec_eq(x_19, x_20);
lean_dec(x_19);
if (x_21 == 0)
{
lean_object* x_22;
lean_dec(x_13);
lean_dec(x_2);
lean_dec(x_1);
x_22 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___spec__1___rarg(x_8);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = l_Lean_Syntax_getArg(x_13, x_12);
lean_dec(x_13);
x_24 = l_Lean_Syntax_getArg(x_1, x_20);
lean_dec(x_1);
x_25 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux(x_23, x_24, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_25;
}
}
}
}
}
}
static lean_object* _init_l_Lean_Elab_Term_elabTParserMacro___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabTParserMacro___lambda__1___boxed), 8, 0);
return x_1;
}
}
lean_object* l_Lean_Elab_Term_elabTParserMacro(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_Elab_Term_elabTParserMacro___closed__1;
x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Elab_Term_elabTParserMacro___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabTParserMacro), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_elabTParserMacro(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabTrailingParserMacro___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -4886,7 +4560,7 @@ lean_dec(x_13);
x_35 = lean_unsigned_to_nat(2u);
x_36 = l_Lean_Syntax_getArg(x_1, x_35);
lean_dec(x_1);
x_37 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2;
x_37 = l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2;
x_38 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux(x_37, x_36, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
return x_38;
}
@ -11233,17 +10907,10 @@ l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___clo
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__38);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__39 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__39();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__39);
l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1);
l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2);
l_Lean_Elab_Term_elabParserMacro___closed__1 = _init_l_Lean_Elab_Term_elabParserMacro___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___closed__1);
l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1);
res = l___regBuiltin_Lean_Elab_Term_elabParserMacro(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1 = _init_l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__1);
l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2 = _init_l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_elabLeadingParserMacro___lambda__1___closed__2);
l_Lean_Elab_Term_elabLeadingParserMacro___closed__1 = _init_l_Lean_Elab_Term_elabLeadingParserMacro___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabLeadingParserMacro___closed__1);
l___regBuiltin_Lean_Elab_Term_elabLeadingParserMacro___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabLeadingParserMacro___closed__1();
@ -11271,13 +10938,6 @@ l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___cl
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__9);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__10 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__10();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__10);
l_Lean_Elab_Term_elabTParserMacro___closed__1 = _init_l_Lean_Elab_Term_elabTParserMacro___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabTParserMacro___closed__1);
l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1);
res = l___regBuiltin_Lean_Elab_Term_elabTParserMacro(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabTrailingParserMacro___closed__1 = _init_l_Lean_Elab_Term_elabTrailingParserMacro___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabTrailingParserMacro___closed__1);
l___regBuiltin_Lean_Elab_Term_elabTrailingParserMacro___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabTrailingParserMacro___closed__1();

124
stage0/stdlib/Lean/Parser/Extra.c generated
View file

@ -26,6 +26,7 @@ lean_object* l_Lean_Parser_charLit___closed__1;
lean_object* l_Lean_Parser_nonReservedSymbol_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_visitArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__4;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__1;
extern lean_object* l_Lean_scientificLitKind___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_categoryParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__26;
@ -64,6 +65,7 @@ lean_object* l_Lean_Parser_sepBy_formatter___boxed(lean_object*, lean_object*, l
lean_object* l_Lean_Parser_ppGroup___boxed(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__18;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__11;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__4;
lean_object* l_Lean_Parser_symbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_charLit;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__30;
@ -84,6 +86,7 @@ extern lean_object* l_Lean_identKind___closed__2;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__5;
lean_object* l_Lean_PrettyPrinter_Formatter_manyNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nameLit_formatter___closed__3;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__8;
extern lean_object* l_term___u2218_____closed__6;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__3;
lean_object* l_Lean_Parser_ident_formatter___closed__2;
@ -92,7 +95,6 @@ lean_object* l_Lean_Parser_many___closed__2;
lean_object* l_Lean_Parser_scientificLit;
lean_object* l_Lean_ppSpace_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__2;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__12;
lean_object* l_Lean_Parser_tokenWithAntiquotFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_orelse_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -109,7 +111,6 @@ lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__14;
lean_object* l_Lean_Parser_withAntiquotSpliceAndSuffix_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__22;
lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__1;
extern lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7;
lean_object* l_Lean_PrettyPrinter_Formatter_pushLine(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
@ -120,6 +121,7 @@ lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__18;
lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__8;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_nameLitNoAntiquot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__6;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_Parser_optional_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -130,6 +132,7 @@ lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__9;
lean_object* l_Lean_Parser_strLit_formatter___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__2;
lean_object* l_Lean_Parser_charLit___elambda__1___closed__1;
lean_object* l_Lean_Parser_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_numLit___closed__3;
@ -156,6 +159,7 @@ lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed_
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_unicodeSymbolNoAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__4;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__5;
lean_object* l_Lean_Parser_nodeWithAntiquot_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__18;
lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__4;
@ -214,13 +218,13 @@ lean_object* l_Lean_Parser_ppSpace_parenthesizer(lean_object*, lean_object*, lea
lean_object* l_Lean_Parser_ident___closed__2;
lean_object* l_Lean_Parser_sepByElemParser_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ppHardSpace_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__7;
extern lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__4;
lean_object* l_Lean_Parser_charLit_formatter___closed__2;
lean_object* l_Lean_Parser_mkAntiquotSplice_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_setExpected_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_strLitNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_strLit_parenthesizer___closed__2;
lean_object* l_Lean_Parser_termRegister__parser__alias______;
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__16;
extern lean_object* l_Lean_Parser_rawIdentNoAntiquot___closed__1;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__23;
@ -232,6 +236,7 @@ lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__22;
lean_object* l_Lean_Parser_charLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_numLitNoAntiquot___closed__1;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__13;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__9;
lean_object* l_Lean_Parser_scientificLit_formatter___closed__3;
lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
lean_object* l_Lean_Parser_scientificLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -288,7 +293,6 @@ lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg(lean_object*, uint8_t
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__19;
extern lean_object* l_Lean_Parser_parserAliasesRef;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__20;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__11;
lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__7;
lean_object* l_Lean_Parser_nameLit___closed__2;
@ -301,7 +305,6 @@ lean_object* l_Lean_Syntax_getId(lean_object*);
extern lean_object* l_termDepIfThenElse___closed__6;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__24;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_958____closed__6;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__3;
extern lean_object* l_Lean_charLitKind;
extern lean_object* l_Lean_Parser_maxPrec;
lean_object* l_Lean_Parser_strLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -326,7 +329,6 @@ lean_object* l_Lean_Parser_ppLine_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__7;
extern lean_object* l_Lean_Parser_charLitNoAntiquot___closed__1;
lean_object* l_Lean_Parser_antiquotExpr_parenthesizer___closed__1;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__6;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__25;
lean_object* l_Lean_Parser_nonReservedSymbol_parenthesizer___rarg___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer___boxed(lean_object*);
@ -362,7 +364,6 @@ lean_object* l_Lean_ppHardSpace_formatter___boxed(lean_object*, lean_object*, le
lean_object* l_Lean_Parser_many1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nameLit___elambda__1___closed__1;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__14;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21______;
lean_object* l_Lean_Parser_notSymbol(lean_object*);
lean_object* l_Lean_Parser_sepByElemParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind___closed__2;
@ -420,6 +421,7 @@ lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__13;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__12;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__12;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__31;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__10;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__10;
lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__7;
lean_object* l_Lean_Parser_nameLit_parenthesizer___closed__2;
@ -430,6 +432,7 @@ lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__23;
lean_object* l_Lean_Parser_charLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_charLit_parenthesizer___closed__2;
lean_object* l_Lean_Parser_charLit_formatter___closed__3;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__11;
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Int_instInhabitedInt___closed__1;
lean_object* l_Lean_Parser_notSymbol_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -437,7 +440,6 @@ extern lean_object* l_Lean_Syntax_mkAntiquotNode___closed__2;
lean_object* l_Lean_ppLine_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_optional___closed__2;
lean_object* l_Lean_Parser_many1Indent(lean_object*);
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__10;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__16;
lean_object* l_Lean_PrettyPrinter_Formatter_pushNone_formatter___boxed(lean_object*);
@ -481,9 +483,7 @@ lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__
lean_object* l_Lean_Parser_scientificLit_formatter___closed__1;
lean_object* l_Lean_Parser_symbol_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerAliasesRef;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__4;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__2;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__8;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquotSuffixSplice_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ppLine_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -503,7 +503,6 @@ extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_Pretty
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__4;
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__9;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__8;
lean_object* l_Lean_Parser_nameLit_formatter___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_nonReservedSymbolNoAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -519,6 +518,7 @@ lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__
lean_object* l_Lean_Parser_ident_parenthesizer___closed__1;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__11;
lean_object* l_Lean_Parser_optional___closed__4;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__3;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_strLitNoAntiquot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__1;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__19;
@ -543,6 +543,7 @@ lean_object* l_Lean_Parser_ident___closed__3;
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__17;
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__2;
lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__24;
lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__7;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__9;
lean_object* l_Lean_PrettyPrinter_Formatter_withAntiquotSuffixSplice_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ident_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -566,7 +567,6 @@ lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__17;
lean_object* l_Lean_Parser_strLit;
lean_object* l_Lean_Parser_many1(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_andthen_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termRegisterParserAlias_x21_________closed__5;
lean_object* l_Lean_Parser_scientificLit___closed__1;
lean_object* l_Lean_Parser_mkAntiquotSplice_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_identNoAntiquot___closed__2;
@ -3827,43 +3827,43 @@ x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
return x_7;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__1() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("termRegisterParserAlias!___");
x_1 = lean_mk_string("termRegister_parser_alias___");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__2() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__4;
x_2 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__1;
x_2 = l_Lean_Parser_termRegister__parser__alias_________closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__3() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("registerParserAlias!");
x_1 = lean_mk_string("register_parser_alias");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__4() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__3;
x_1 = l_Lean_Parser_termRegister__parser__alias_________closed__3;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__5() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -3873,23 +3873,23 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__6() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__5;
x_1 = l_Lean_Parser_termRegister__parser__alias_________closed__5;
x_2 = lean_alloc_ctor(8, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__7() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__4;
x_3 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__6;
x_2 = l_Lean_Parser_termRegister__parser__alias_________closed__4;
x_3 = l_Lean_Parser_termRegister__parser__alias_________closed__6;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3897,7 +3897,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__8() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -3907,23 +3907,23 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__9() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__8;
x_1 = l_Lean_Parser_termRegister__parser__alias_________closed__8;
x_2 = lean_alloc_ctor(8, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__10() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__7;
x_3 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__9;
x_2 = l_Lean_Parser_termRegister__parser__alias_________closed__7;
x_3 = l_Lean_Parser_termRegister__parser__alias_________closed__9;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3931,13 +3931,13 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__11() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias_________closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__2;
x_1 = l_Lean_Parser_termRegister__parser__alias_________closed__2;
x_2 = lean_unsigned_to_nat(1023u);
x_3 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__10;
x_3 = l_Lean_Parser_termRegister__parser__alias_________closed__10;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3945,11 +3945,11 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_termRegisterParserAlias_x21______() {
static lean_object* _init_l_Lean_Parser_termRegister__parser__alias______() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__11;
x_1 = l_Lean_Parser_termRegister__parser__alias_________closed__11;
return x_1;
}
}
@ -4248,7 +4248,7 @@ lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276_(lean_obje
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_termRegisterParserAlias_x21_________closed__2;
x_4 = l_Lean_Parser_termRegister__parser__alias_________closed__2;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
@ -6805,30 +6805,30 @@ l_Lean_Parser_ppLine = _init_l_Lean_Parser_ppLine();
lean_mark_persistent(l_Lean_Parser_ppLine);
l_Lean_ppLine_formatter___closed__1 = _init_l_Lean_ppLine_formatter___closed__1();
lean_mark_persistent(l_Lean_ppLine_formatter___closed__1);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__1 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__1();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__1);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__2 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__2();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__2);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__3 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__3();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__3);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__4 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__4();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__4);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__5 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__5();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__5);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__6 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__6();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__6);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__7 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__7();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__7);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__8 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__8();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__8);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__9 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__9();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__9);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__10 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__10();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__10);
l_Lean_Parser_termRegisterParserAlias_x21_________closed__11 = _init_l_Lean_Parser_termRegisterParserAlias_x21_________closed__11();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21_________closed__11);
l_Lean_Parser_termRegisterParserAlias_x21______ = _init_l_Lean_Parser_termRegisterParserAlias_x21______();
lean_mark_persistent(l_Lean_Parser_termRegisterParserAlias_x21______);
l_Lean_Parser_termRegister__parser__alias_________closed__1 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__1();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__1);
l_Lean_Parser_termRegister__parser__alias_________closed__2 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__2();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__2);
l_Lean_Parser_termRegister__parser__alias_________closed__3 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__3();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__3);
l_Lean_Parser_termRegister__parser__alias_________closed__4 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__4();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__4);
l_Lean_Parser_termRegister__parser__alias_________closed__5 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__5();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__5);
l_Lean_Parser_termRegister__parser__alias_________closed__6 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__6();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__6);
l_Lean_Parser_termRegister__parser__alias_________closed__7 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__7();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__7);
l_Lean_Parser_termRegister__parser__alias_________closed__8 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__8();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__8);
l_Lean_Parser_termRegister__parser__alias_________closed__9 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__9();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__9);
l_Lean_Parser_termRegister__parser__alias_________closed__10 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__10();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__10);
l_Lean_Parser_termRegister__parser__alias_________closed__11 = _init_l_Lean_Parser_termRegister__parser__alias_________closed__11();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias_________closed__11);
l_Lean_Parser_termRegister__parser__alias______ = _init_l_Lean_Parser_termRegister__parser__alias______();
lean_mark_persistent(l_Lean_Parser_termRegister__parser__alias______);
l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__1 = _init_l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__1();
lean_mark_persistent(l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__1);
l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__2 = _init_l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__2();

1632
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff