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:
Mario Carneiro 2022-10-24 14:49:25 -04:00 • committed by Gabriel Ebner
parent 765ebcdbf0
commit 8b8fc64fa0
17 changed files with 5201 additions and 3747 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -324,7 +324,7 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do
let mvar ← instantiateMVars mvar
if !(← hasAssignableMVar mvar) then
/- The metavariable `mvar` may have been assinged when solving typing constraints.
/- The metavariable `mvar` may have been assigned when solving typing constraints.
This may happen when a local instance type depends on other local instances.
For example, in Mathlib, we have
```
@ -441,11 +441,11 @@ private def hasUnusedArguments : Expr → Bool
When we look for such an instance it is enough to look for an instance `c : C` and then return `fun _ => c`.
Tomas' approach makes sure that instance of a type like `a : A → C` never gets tabled/cached. More on that later.
At the core is the this methos. it takes an expression E and does two things:
At the core is this method. it takes an expression E and does two things:
The modification to TC resolution works this way: We are looking for an instance of `E`, if it is tabled
just get it as normal, but if not first remove all unused arguments producing `E'`. Now we look up the table again but
for `E'`. If it exists, use the transforme to create E. If it does not exists, create a new goal `E'`.
for `E'`. If it exists, use the transformer to create E. If it does not exists, create a new goal `E'`.
-/
private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM (Option (Expr × Expr)) :=
withMCtx mctx do

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

@ -40,6 +40,8 @@ builtin_initialize
register_parser_alias many1Indent
register_parser_alias optional { autoGroupArgs := false }
register_parser_alias withPosition { stackSz? := none }
register_parser_alias withoutPosition { stackSz? := none }
register_parser_alias withoutForbidden { stackSz? := none }
register_parser_alias (kind := interpolatedStrKind) interpolatedStr
register_parser_alias orelse
register_parser_alias andthen { stackSz? := none }

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

@ -10,40 +10,57 @@ namespace Lean
namespace Parser
/-- Syntax quotation for terms. -/
@[builtin_term_parser] def Term.quot := leading_parser "`(" >> incQuotDepth termParser >> ")"
@[builtin_term_parser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
@[builtin_term_parser] def Term.quot := leading_parser
"`(" >> withoutPosition (incQuotDepth termParser) >> ")"
@[builtin_term_parser] def Term.precheckedQuot := leading_parser
"`" >> Term.quot
namespace Command
/--
Syntax quotation for (sequences of) commands. The identical syntax for term quotations takes priority, so ambiguous quotations like
`` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
Multiple commands 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). -/
@[builtin_term_parser low] def quot := leading_parser "`(" >> incQuotDepth (many1Unbox commandParser) >> ")"
Syntax quotation for (sequences of) commands.
The identical syntax for term quotations takes priority,
so ambiguous quotations like `` `($x $y) `` will be parsed as an application,
not two commands. Use `` `($x:command $y:command) `` instead.
Multiple commands 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). -/
@[builtin_term_parser low] def quot := leading_parser
"`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
/-
A mutual block may be broken in different cliques, we identify them using an `ident` (an element of the clique)
We provide two kinds of hints to the termination checker:
1- A wellfounded relation (`p` is `termParser`)
2- A tactic for proving the recursive applications are "decreasing" (`p` is `tacticSeq`)
A mutual block may be broken in different cliques,
we identify them using an `ident` (an element of the clique).
We provide two kinds of hints to the termination checker:
1- A wellfounded relation (`p` is `termParser`)
2- A tactic for proving the recursive applications are "decreasing" (`p` is `tacticSeq`)
-/
def terminationHintMany (p : Parser) := leading_parser atomic (lookahead (ident >> " => ")) >> many1Indent (group (ppLine >> ident >> " => " >> p >> optional ";"))
def terminationHintMany (p : Parser) := leading_parser
atomic (lookahead (ident >> " => ")) >>
many1Indent (group (ppLine >> ident >> " => " >> p >> optional ";"))
def terminationHint1 (p : Parser) := leading_parser p
def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser
def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq
def terminationByCore := leading_parser
"termination_by' " >> terminationHint termParser
def decreasingBy := leading_parser
"decreasing_by " >> terminationHint Tactic.tacticSeq
def terminationByElement := leading_parser ppLine >> (ident <|> Term.hole) >> many (ident <|> Term.hole) >> " => " >> termParser >> optional ";"
def terminationBy := leading_parser ppLine >> "termination_by " >> many1Indent terminationByElement
def terminationByElement := leading_parser
ppLine >> (ident <|> Term.hole) >> many (ident <|> Term.hole) >>
" => " >> termParser >> optional ";"
def terminationBy := leading_parser
ppLine >> "termination_by " >> many1Indent terminationByElement
def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy
def terminationSuffix :=
optional (terminationBy <|> terminationByCore) >> optional decreasingBy
@[builtin_command_parser]
def moduleDoc := leading_parser ppDedent $ "/-!" >> commentBody >> ppLine
def moduleDoc := leading_parser ppDedent <|
"/-!" >> commentBody >> ppLine
def namedPrio := leading_parser (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")")
def namedPrio := leading_parser
atomic ("(" >> nonReservedSymbol "priority") >> " := " >> withoutPosition priorityParser >> ")"
def optNamedPrio := optional (ppSpace >> namedPrio)
def «private» := leading_parser "private "
@ -53,112 +70,208 @@ def «noncomputable» := leading_parser "noncomputable "
def «unsafe» := leading_parser "unsafe "
def «partial» := leading_parser "partial "
def «nonrec» := leading_parser "nonrec "
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» <|> «nonrec»)
def declId := leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := leading_parser " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def whereStructField := leading_parser Term.letDecl
def whereStructInst := leading_parser " where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >> optional Term.whereDecls
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» <|> «nonrec»)
def declId := leading_parser
ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := leading_parser
many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser
many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := leading_parser
" :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser
Term.matchAltsWhereDecls
def whereStructField := leading_parser
Term.letDecl
def whereStructInst := leading_parser
" where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
optional Term.whereDecls
/-
Remark: we should not use `Term.whereDecls` at `declVal` because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
Remark: we should not use `Term.whereDecls` at `declVal`
because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
Issue #753 showns an example that fails to be parsed when we used `Term.whereDecls`.
-/
def declVal := withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
declValSimple <|> declValEqns <|> whereStructInst
def «abbrev» := leading_parser "abbrev " >> declId >> ppIndent optDeclSig >> declVal
def optDefDeriving := optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
def «def» := leading_parser "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
def «theorem» := leading_parser "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
def «opaque» := leading_parser "opaque " >> declId >> ppIndent declSig >> optional declValSimple
/- As `declSig` starts with a space, "instance" does not need a trailing space if we put `ppSpace` in the optional fragments. -/
def «instance» := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
def «axiom» := leading_parser "axiom " >> declId >> ppIndent declSig
def declVal :=
withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
declValSimple <|> declValEqns <|> whereStructInst
def «abbrev» := leading_parser
"abbrev " >> declId >> ppIndent optDeclSig >> declVal
def optDefDeriving :=
optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
def «def» := leading_parser
"def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
def «theorem» := leading_parser
"theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
def «opaque» := leading_parser
"opaque " >> declId >> ppIndent declSig >> optional declValSimple
/- As `declSig` starts with a space, "instance" does not need a trailing space
if we put `ppSpace` in the optional fragments. -/
def «instance» := leading_parser
Term.attrKind >> "instance" >> optNamedPrio >>
optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
def «axiom» := leading_parser
"axiom " >> declId >> ppIndent declSig
/- As `declSig` starts with a space, "example" does not need a trailing space. -/
def «example» := leading_parser "example" >> ppIndent optDeclSig >> declVal
def ctor := leading_parser atomic (optional docComment >> "\n| ") >> ppGroup (declModifiers true >> rawIdent >> optDeclSig)
def «example» := leading_parser
"example" >> ppIndent optDeclSig >> declVal
def ctor := leading_parser
atomic (optional docComment >> "\n| ") >>
ppGroup (declModifiers true >> rawIdent >> optDeclSig)
def derivingClasses := sepBy1 (group (ident >> optional (" with " >> Term.structInst))) ", "
def optDeriving := leading_parser optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
def computedField := leading_parser declModifiers true >> ident >> " : " >> termParser >> Term.matchAlts
def computedFields := leading_parser "with" >> manyIndent (ppLine >> ppGroup computedField)
def optDeriving := leading_parser
optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
def computedField := leading_parser
declModifiers true >> ident >> " : " >> termParser >> Term.matchAlts
def computedFields := leading_parser
"with" >> manyIndent (ppLine >> ppGroup computedField)
/--
In Lean, every concrete type other than the universes and every type constructor other than dependent arrows is
an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the
type universes, dependent arrow types, and inductive types; everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructor. For example, `List α` is the list of elements of type `α`, and
is defined as follows
In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructor.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`, or an element `head : α` followed by a list `tail : List α`.
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
For more information about [inductive types](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html).
-/
def «inductive» := leading_parser "inductive " >> declId >> optDeclSig >> optional (symbol " :=" <|> " where") >>
def «inductive» := leading_parser
"inductive " >> declId >> optDeclSig >> optional (symbol " :=" <|> " where") >>
many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
def classInductive := leading_parser atomic (group (symbol "class " >> "inductive ")) >> declId >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >> many ctor >> optDeriving
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> ppIndent optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) >> ")"
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault)
def structFields := leading_parser manyIndent (ppLine >> checkColGe >> ppGroup (structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structCtor := leading_parser atomic (declModifiers true >> ident >> " :: ")
def structureTk := leading_parser "structure "
def classTk := leading_parser "class "
def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
def classInductive := leading_parser
atomic (group (symbol "class " >> "inductive ")) >>
declId >> ppIndent optDeclSig >>
optional (symbol " :=" <|> " where") >> many ctor >> optDeriving
def structExplicitBinder := leading_parser
atomic (declModifiers true >> "(") >>
withoutPosition (many1 ident >> ppIndent optDeclSig >>
optional (Term.binderTactic <|> Term.binderDefault)) >> ")"
def structImplicitBinder := leading_parser
atomic (declModifiers true >> "{") >> withoutPosition (many1 ident >> declSig) >> "}"
def structInstBinder := leading_parser
atomic (declModifiers true >> "[") >> withoutPosition (many1 ident >> declSig) >> "]"
def structSimpleBinder := leading_parser
atomic (declModifiers true >> ident) >> optDeclSig >>
optional (Term.binderTactic <|> Term.binderDefault)
def structFields := leading_parser
manyIndent <|
ppLine >> checkColGe >> ppGroup (
structExplicitBinder <|> structImplicitBinder <|>
structInstBinder <|> structSimpleBinder)
def structCtor := leading_parser
atomic (declModifiers true >> ident >> " :: ")
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 (ppSpace >> Term.bracketedBinder) >> optional «extends» >> Term.optType
>> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
>> optDeriving
(structureTk <|> classTk) >>
declId >> many (ppSpace >> Term.bracketedBinder) >>
optional «extends» >> Term.optType >>
optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >>
optDeriving
@[builtin_command_parser] def declaration := leading_parser
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
@[builtin_command_parser] def «deriving» := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
@[builtin_command_parser] def noncomputableSection := leading_parser "noncomputable " >> "section " >> optional ident
@[builtin_command_parser] def «section» := leading_parser "section " >> optional ident
@[builtin_command_parser] def «namespace» := leading_parser "namespace " >> ident
@[builtin_command_parser] def «end» := leading_parser "end " >> optional ident
@[builtin_command_parser] def «variable» := leading_parser "variable" >> many1 (ppSpace >> Term.bracketedBinder)
@[builtin_command_parser] def «universe» := leading_parser "universe " >> many1 ident
@[builtin_command_parser] def check := leading_parser "#check " >> termParser
@[builtin_command_parser] def check_failure := leading_parser "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtin_command_parser] def reduce := leading_parser "#reduce " >> termParser
@[builtin_command_parser] def eval := leading_parser "#eval " >> termParser
@[builtin_command_parser] def synth := leading_parser "#synth " >> termParser
@[builtin_command_parser] def exit := leading_parser "#exit"
@[builtin_command_parser] def print := leading_parser "#print " >> (ident <|> strLit)
@[builtin_command_parser] def printAxioms := leading_parser "#print " >> nonReservedSymbol "axioms " >> ident
@[builtin_command_parser] def «init_quot» := leading_parser "init_quot"
declModifiers false >>
(«abbrev» <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
«inductive» <|> classInductive <|> «structure»)
@[builtin_command_parser] def «deriving» := leading_parser
"deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
@[builtin_command_parser] def noncomputableSection := leading_parser
"noncomputable " >> "section " >> optional ident
@[builtin_command_parser] def «section» := leading_parser
"section " >> optional ident
@[builtin_command_parser] def «namespace» := leading_parser
"namespace " >> ident
@[builtin_command_parser] def «end» := leading_parser
"end " >> optional ident
@[builtin_command_parser] def «variable» := leading_parser
"variable" >> many1 (ppSpace >> Term.bracketedBinder)
@[builtin_command_parser] def «universe» := leading_parser
"universe " >> many1 ident
@[builtin_command_parser] def check := leading_parser
"#check " >> termParser
@[builtin_command_parser] def check_failure := leading_parser
"#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtin_command_parser] def reduce := leading_parser
"#reduce " >> termParser
@[builtin_command_parser] def eval := leading_parser
"#eval " >> termParser
@[builtin_command_parser] def synth := leading_parser
"#synth " >> termParser
@[builtin_command_parser] def exit := leading_parser
"#exit"
@[builtin_command_parser] def print := leading_parser
"#print " >> (ident <|> strLit)
@[builtin_command_parser] def printAxioms := leading_parser
"#print " >> nonReservedSymbol "axioms " >> ident
@[builtin_command_parser] def «init_quot» := leading_parser
"init_quot"
def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@[builtin_command_parser] def «set_option» := leading_parser "set_option " >> ident >> ppSpace >> optionValue
def eraseAttr := leading_parser "-" >> rawIdent
@[builtin_command_parser] def «attribute» := leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
@[builtin_command_parser] def «export» := leading_parser "export " >> ident >> " (" >> many1 ident >> ")"
@[builtin_command_parser] def «import» := leading_parser "import" -- not a real command, only for error messages
def openHiding := leading_parser atomic (ident >> "hiding") >> many1 (checkColGt >> ident)
def openRenamingItem := leading_parser ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident
def openRenaming := leading_parser atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := leading_parser atomic (ident >> " (") >> many1 ident >> ")"
def openSimple := leading_parser many1 (checkColGt >> ident)
def openScoped := leading_parser "scoped " >> many1 (checkColGt >> ident)
def openDecl := withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
@[builtin_command_parser] def «open» := leading_parser withPosition ("open " >> openDecl)
@[builtin_command_parser] def «set_option» := leading_parser
"set_option " >> ident >> ppSpace >> optionValue
def eraseAttr := leading_parser
"-" >> rawIdent
@[builtin_command_parser] def «attribute» := leading_parser
"attribute " >> "[" >>
withoutPosition (sepBy1 (eraseAttr <|> Term.attrInstance) ", ") >>
"] " >> many1 ident
@[builtin_command_parser] def «export» := leading_parser
"export " >> ident >> " (" >> many1 ident >> ")"
@[builtin_command_parser] def «import» := leading_parser
"import" -- not a real command, only for error messages
def openHiding := leading_parser
atomic (ident >> "hiding") >> many1 (checkColGt >> ident)
def openRenamingItem := leading_parser
ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident
def openRenaming := leading_parser
atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := leading_parser
atomic (ident >> " (") >> many1 ident >> ")"
def openSimple := leading_parser
many1 (checkColGt >> ident)
def openScoped := leading_parser
"scoped " >> many1 (checkColGt >> ident)
def openDecl :=
withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
@[builtin_command_parser] def «open» := leading_parser
withPosition ("open " >> openDecl)
@[builtin_command_parser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end") >> terminationSuffix
def initializeKeyword := leading_parser "initialize " <|> "builtin_initialize "
@[builtin_command_parser] def «initialize» := leading_parser declModifiers false >> initializeKeyword >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtin_command_parser] def «mutual» := leading_parser
"mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >>
ppDedent (ppLine >> "end") >> terminationSuffix
def initializeKeyword := leading_parser
"initialize " <|> "builtin_initialize "
@[builtin_command_parser] def «initialize» := leading_parser
declModifiers false >> initializeKeyword >>
optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtin_command_parser] def «in» := trailing_parser withOpen (" in " >> commandParser)
@[builtin_command_parser] def addDocString := leading_parser docComment >> "add_decl_doc" >> ident
@[builtin_command_parser] def addDocString := leading_parser
docComment >> "add_decl_doc" >> ident
/--
This is an auxiliary command for generation constructor injectivity theorems for inductive types defined at `Prelude.lean`.
This is an auxiliary command for generation constructor injectivity theorems for
inductive types defined at `Prelude.lean`.
It is meant for bootstrapping purposes only. -/
@[builtin_command_parser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident
@[builtin_command_parser] def genInjectiveTheorems := leading_parser
"gen_injective_theorems% " >> ident
@[run_builtin_parser_attribute_hooks] abbrev declModifiersF := declModifiers false
@[run_builtin_parser_attribute_hooks] abbrev declModifiersT := declModifiers true

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

@ -16,12 +16,18 @@ builtin_initialize registerBuiltinDynamicParserAttribute `doElem_parser `doElem
namespace Term
def leftArrow : Parser := unicodeSymbol "← " "<- "
@[builtin_term_parser] def liftMethod := leading_parser:minPrec leftArrow >> termParser
@[builtin_term_parser] def liftMethod := leading_parser:minPrec
leftArrow >> termParser
def doSeqItem := leading_parser ppLine >> doElemParser >> optional "; "
def doSeqIndent := leading_parser many1Indent doSeqItem
def doSeqBracketed := leading_parser "{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
def doSeq := withAntiquot (mkAntiquot "doSeq" `Lean.Parser.Term.doSeq (isPseudoKind := true)) <| doSeqBracketed <|> doSeqIndent
def doSeqItem := leading_parser
ppLine >> doElemParser >> optional "; "
def doSeqIndent := leading_parser
many1Indent doSeqItem
def doSeqBracketed := leading_parser
"{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
def doSeq :=
withAntiquot (mkAntiquot "doSeq" decl_name% (isPseudoKind := true)) <|
doSeqBracketed <|> doSeqIndent
def termBeforeDo := withForbidden "do" termParser
attribute [run_builtin_parser_attribute_hooks] doSeq termBeforeDo
@ -31,27 +37,45 @@ builtin_initialize
register_parser_alias 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" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
-- 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 where
-- an "open" command follows the `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" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
"token at 'do' element"
@[builtin_doElem_parser] def doLet := leading_parser "let " >> optional "mut " >> letDecl
@[builtin_doElem_parser] def doLetElse := leading_parser "let " >> optional "mut " >> termParser >> " := " >> termParser >> checkColGt >> " | " >> doElemParser
@[builtin_doElem_parser] def doLet := leading_parser
"let " >> optional "mut " >> letDecl
@[builtin_doElem_parser] def doLetElse := leading_parser
"let " >> optional "mut " >> termParser >> " := " >> termParser >>
checkColGt >> " | " >> doElemParser
@[builtin_doElem_parser] def doLetRec := leading_parser group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := leading_parser atomic (ident >> optType >> ppSpace >> leftArrow) >> doElemParser
def doPatDecl := leading_parser atomic (termParser >> ppSpace >> leftArrow) >> doElemParser >> optional (checkColGt >> " | " >> doElemParser)
@[builtin_doElem_parser] def doLetArrow := leading_parser withPosition ("let " >> optional "mut " >> (doIdDecl <|> doPatDecl))
@[builtin_doElem_parser] def doLetRec := leading_parser
group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := leading_parser
atomic (ident >> optType >> ppSpace >> leftArrow) >>
doElemParser
def doPatDecl := leading_parser
atomic (termParser >> ppSpace >> leftArrow) >>
doElemParser >> optional (checkColGt >> " | " >> doElemParser)
@[builtin_doElem_parser] 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
def letIdDeclNoBinders := node ``letIdDecl <|
atomic (ident >> pushNone >> optType >> " := ") >> termParser
@[builtin_doElem_parser] def doReassign := leading_parser notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtin_doElem_parser] def doReassignArrow := leading_parser notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl)
@[builtin_doElem_parser] def doHave := leading_parser "have " >> Term.haveDecl
@[builtin_doElem_parser] def doReassign := leading_parser
notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtin_doElem_parser] def doReassignArrow := leading_parser
notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl)
@[builtin_doElem_parser] 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
In `do` blocks, we support `if` without an `else`.
Thus, we use indentation to prevent examples such as
```
if c_1 then
if c_2 then
@ -83,73 +107,112 @@ def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if ")))
-- ensure `if $e then ...` still binds to `e:term`
def doIfLetPure := leading_parser " := " >> termParser
def doIfLetBind := leading_parser " ← " >> termParser
def doIfLet := leading_parser (withAnonymousAntiquot := false) "let " >> termParser >> (doIfLetPure <|> doIfLetBind)
def doIfProp := leading_parser (withAnonymousAntiquot := false) optIdent >> termParser
def doIfCond := withAntiquot (mkAntiquot "doIfCond" `Lean.Parser.Term.doIfCond (anonymous := false) (isPseudoKind := true)) <| doIfLet <|> doIfProp
@[builtin_doElem_parser] def doIf := leading_parser withPositionAfterLinebreak $
"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)
@[builtin_doElem_parser] def doUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
def doForDecl := leading_parser optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser
def doIfLet := leading_parser (withAnonymousAntiquot := false)
"let " >> termParser >> (doIfLetPure <|> doIfLetBind)
def doIfProp := leading_parser (withAnonymousAntiquot := false)
optIdent >> termParser
def doIfCond :=
withAntiquot (mkAntiquot "doIfCond" decl_name% (anonymous := false) (isPseudoKind := true)) <|
doIfLet <|> doIfProp
@[builtin_doElem_parser] def doIf := leading_parser withPositionAfterLinebreak <|
"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)
@[builtin_doElem_parser] def doUnless := leading_parser
"unless " >> withForbidden "do" termParser >> "do " >> doSeq
def doForDecl := leading_parser
optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser
/--
`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
-/
@[builtin_doElem_parser] def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtin_doElem_parser] def doFor := leading_parser
"for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
@[builtin_doElem_parser] def doMatch := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> optional Term.motive >> sepBy1 matchDiscr ", " >> " with " >> doMatchAlts
@[builtin_doElem_parser] def doMatch := leading_parser:leadPrec
"match " >> optional Term.generalizingParam >> optional Term.motive >>
sepBy1 matchDiscr ", " >> " with " >> doMatchAlts
def doCatch := leading_parser atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser "catch " >> doMatchAlts
def doFinally := leading_parser "finally " >> doSeq
@[builtin_doElem_parser] def doTry := leading_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
@[builtin_doElem_parser] def doTry := leading_parser
"try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
/-- `break` exits the surrounding `for` loop. -/
@[builtin_doElem_parser] def doBreak := leading_parser "break"
/-- `continue` skips to the next iteration of the surrounding `for` loop. -/
@[builtin_doElem_parser] def doContinue := leading_parser "continue"
/--
`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`, skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do` do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block is highlighted when hovering over `return`.
`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
-/
@[builtin_doElem_parser] def doReturn := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtin_doElem_parser] def doDbgTrace := leading_parser:leadPrec "dbg_trace " >> ((interpolatedStr termParser) <|> termParser)
@[builtin_doElem_parser] def doAssert := leading_parser:leadPrec "assert! " >> termParser
@[builtin_doElem_parser] def doReturn := leading_parser:leadPrec
withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtin_doElem_parser] def doDbgTrace := leading_parser:leadPrec
"dbg_trace " >> ((interpolatedStr termParser) <|> termParser)
@[builtin_doElem_parser] def doAssert := leading_parser:leadPrec
"assert! " >> termParser
/-
We use `notFollowedBy` to avoid counterintuitive behavior.
For example, the `if`-term parser
doesn't enforce indentation restrictions, but we don't want it to be used when `doIf` fails.
Note that parser priorities would not solve this problem since the `doIf` parser is failing while the `if`
parser is succeeding. The first `notFollowedBy` prevents this problem.
For example, the `if`-term parser doesn't enforce indentation restrictions,
but we don't want it to be used when `doIf` fails.
Note that parser priorities would not solve this problem
since the `doIf` parser is failing while the `if` parser is succeeding.
The first `notFollowedBy` prevents this problem.
Consider the `doElem` `x := (a, b⟩` it contains an error since we are using `⟩` instead of `)`. Thus, `doReassign` parser fails.
However, `doExpr` would succeed consuming just `x`, and cryptic error message is generated after that.
Consider the `doElem` `x := (a, b⟩`.
It contains an error since we are using `⟩` instead of `)`.
Thus, `doReassign` parser fails.
However, `doExpr` would succeed consuming just `x`,
and cryptic error message is generated after that.
The second `notFollowedBy` prevents this problem.
-/
@[builtin_doElem_parser] def doExpr := leading_parser notFollowedByRedefinedTermToken >> termParser >> notFollowedBy (symbol ":=" <|> symbol "←" <|> symbol "<-") "unexpected token after 'expr' in 'do' block"
@[builtin_doElem_parser] def doNested := leading_parser "do " >> doSeq
@[builtin_doElem_parser] def doExpr := leading_parser
notFollowedByRedefinedTermToken >> termParser >>
notFollowedBy (symbol ":=" <|> symbol "←" <|> symbol "<-")
"unexpected token after 'expr' in 'do' block"
@[builtin_doElem_parser] def doNested := leading_parser
"do " >> doSeq
@[builtin_term_parser] def «do» := leading_parser:argPrec ppAllowUngrouped >> "do " >> doSeq
@[builtin_term_parser] def «do» := leading_parser:argPrec
ppAllowUngrouped >> "do " >> doSeq
/- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
/-- `unless e do s` is a nicer way to write `if !e do s`. -/
@[builtin_term_parser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtin_term_parser] def termFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtin_term_parser] def termTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
/--
`return` used outside of `do` blocks creates an implicit block around it and thus is equivalent to `pure e`, but helps with
avoiding parentheses.
/-
macros for using `unless`, `for`, `try`, `return` as terms.
They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...`
-/
@[builtin_term_parser] def termReturn := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
/-- `unless e do s` is a nicer way to write `if !e do s`. -/
@[builtin_term_parser] def termUnless := leading_parser
"unless " >> withForbidden "do" termParser >> "do " >> doSeq
@[builtin_term_parser] def termFor := leading_parser
"for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
@[builtin_term_parser] def termTry := leading_parser
"try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
/--
`return` used outside of `do` blocks creates an implicit block around it
and thus is equivalent to `pure e`, but helps with avoiding parentheses.
-/
@[builtin_term_parser] def termReturn := leading_parser:leadPrec
withPosition ("return " >> optional (checkLineEq >> termParser))
end Term
end Parser

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

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

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

@ -22,26 +22,38 @@ builtin_initialize
@[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
categoryParser `stx rbp
def «precedence» := leading_parser ":" >> precedenceParser maxPrec
def «precedence» := leading_parser
":" >> precedenceParser maxPrec
def optPrecedence := optional (atomic «precedence»)
namespace Syntax
@[builtin_prec_parser] def numPrec := checkPrec maxPrec >> numLit
@[builtin_syntax_parser] def paren := leading_parser "(" >> many1 syntaxParser >> ")"
@[builtin_syntax_parser] def cat := leading_parser ident >> optPrecedence
@[builtin_syntax_parser] def unary := leading_parser ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
@[builtin_syntax_parser] def binary := leading_parser ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")"
@[builtin_syntax_parser] def sepBy := leading_parser "sepBy(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtin_syntax_parser] def sepBy1 := leading_parser "sepBy1(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")"
@[builtin_syntax_parser] def atom := leading_parser strLit
@[builtin_syntax_parser] def nonReserved := leading_parser "&" >> strLit
@[builtin_syntax_parser] def paren := leading_parser
"(" >> withoutPosition (many1 syntaxParser) >> ")"
@[builtin_syntax_parser] def cat := leading_parser
ident >> optPrecedence
@[builtin_syntax_parser] def unary := leading_parser
ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser) >> ")"
@[builtin_syntax_parser] def binary := leading_parser
ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser >> ", " >> many1 syntaxParser) >> ")"
@[builtin_syntax_parser] def sepBy := leading_parser
"sepBy(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >>
optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")"
@[builtin_syntax_parser] def sepBy1 := leading_parser
"sepBy1(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >>
optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")"
@[builtin_syntax_parser] def atom := leading_parser
strLit
@[builtin_syntax_parser] def nonReserved := leading_parser
"&" >> strLit
end Syntax
namespace Command
def namedName := leading_parser (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")")
def namedName := leading_parser
atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")"
def optNamedName := optional namedName
def «prefix» := leading_parser "prefix"
@ -50,7 +62,9 @@ def «infixl» := leading_parser "infixl"
def «infixr» := leading_parser "infixr"
def «postfix» := leading_parser "postfix"
def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
@[builtin_command_parser] def «mixfix» := leading_parser optional docComment >> optional Term.«attributes» >> Term.attrKind >> mixfixKind >> precedence >> optNamedName >> optNamedPrio >> ppSpace >> strLit >> darrow >> termParser
@[builtin_command_parser] def «mixfix» := leading_parser
optional docComment >> optional Term.«attributes» >> Term.attrKind >> mixfixKind >>
precedence >> 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 := leading_parser ident >> optPrecedence
@ -58,23 +72,37 @@ def identPrec := leading_parser ident >> optPrecedence
def optKind : Parser := optional ("(" >> nonReservedSymbol "kind" >> ":=" >> ident >> ")")
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtin_command_parser] def «notation» := leading_parser optional docComment >> optional Term.«attributes» >> Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtin_command_parser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> optional Term.«attributes» >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtin_command_parser] def «syntax» := leading_parser optional docComment >> optional Term.«attributes» >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtin_command_parser] def syntaxAbbrev := leading_parser optional docComment >> "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtin_command_parser] def «notation» := leading_parser
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtin_command_parser] def «macro_rules» := suppressInsideQuot <| leading_parser
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"macro_rules" >> optKind >> Term.matchAlts
@[builtin_command_parser] def «syntax» := leading_parser
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtin_command_parser] def syntaxAbbrev := leading_parser
optional docComment >> "syntax " >> ident >> " := " >> many1 syntaxParser
def catBehaviorBoth := leading_parser nonReservedSymbol "both"
def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
@[builtin_command_parser] def syntaxCat := leading_parser optional docComment >> "declare_syntax_cat " >> ident >> catBehavior
def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
@[builtin_command_parser] def syntaxCat := leading_parser
optional docComment >> "declare_syntax_cat " >> ident >> catBehavior
def macroArg := leading_parser
optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
def macroRhs : Parser := leading_parser withPosition termParser
def macroTail := leading_parser atomic (" : " >> ident) >> darrow >> macroRhs
@[builtin_command_parser] def «macro» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 macroArg >> macroTail)
@[builtin_command_parser] def «elab_rules» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts)
@[builtin_command_parser] def «macro» := leading_parser suppressInsideQuot <|
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"macro " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 macroArg >> macroTail
@[builtin_command_parser] def «elab_rules» := leading_parser suppressInsideQuot <|
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts
def elabArg := macroArg
def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> withPosition termParser
@[builtin_command_parser] def «elab» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 elabArg >> elabTail)
@[builtin_command_parser] def «elab» := leading_parser suppressInsideQuot <|
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"elab " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 elabArg >> elabTail
end Command

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

@ -18,7 +18,8 @@ to improve syntax error messages.
example : True := by foo -- unknown tactic
```
-/
@[builtin_tactic_parser] def «unknown» := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtin_tactic_parser] def «unknown» := leading_parser
withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtin_tactic_parser] def nestedTactic := tacticSeqBracketed
@ -38,7 +39,10 @@ example (n : Nat) : n = n := by
[tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html
-/
@[builtin_tactic_parser] def «match» := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> optional Term.motive >> sepBy1 Term.matchDiscr ", " >> " with " >> ppDedent matchAlts
@[builtin_tactic_parser] def «match» := leading_parser:leadPrec
"match " >> optional Term.generalizingParam >>
optional Term.motive >> sepBy1 Term.matchDiscr ", " >>
" with " >> ppDedent matchAlts
/--
The tactic
@ -57,7 +61,8 @@ match x with
That is, `intro` can be followed by match arms and it introduces the values while
doing a pattern match. This is equivalent to `fun` with match arms in term mode.
-/
@[builtin_tactic_parser] def introMatch := leading_parser nonReservedSymbol "intro " >> matchAlts
@[builtin_tactic_parser] def introMatch := leading_parser
nonReservedSymbol "intro " >> matchAlts
/-- `decide` will attempt to prove a goal of type `p` by synthesizing an instance
of `Decidable p` and then evaluating it to `isTrue ..`. Because this uses kernel
@ -67,7 +72,8 @@ by well founded recursion, since this requires reducing proofs.
example : 2 + 2 ≠ 5 := by decide
```
-/
@[builtin_tactic_parser] def decide := leading_parser nonReservedSymbol "decide"
@[builtin_tactic_parser] def decide := leading_parser
nonReservedSymbol "decide"
/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
@ -82,7 +88,8 @@ large computations this is one way to run external programs and trust the result
example : (List.range 1000).length = 1000 := by native_decide
```
-/
@[builtin_tactic_parser] def nativeDecide := leading_parser nonReservedSymbol "native_decide"
@[builtin_tactic_parser] def nativeDecide := leading_parser
nonReservedSymbol "native_decide"
end Tactic
end Parser

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

@ -13,10 +13,13 @@ namespace Command
def commentBody : Parser :=
{ fn := rawFn (finishCommentBlock 1) (trailingWs := true) }
@[combinator_parenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
@[combinator_formatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
@[combinator_parenthesizer commentBody]
def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
@[combinator_formatter commentBody]
def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
def docComment := leading_parser
ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
end Command
builtin_initialize
@ -43,14 +46,14 @@ builtin_initialize
register_parser_alias sepByIndentSemicolon
register_parser_alias sepBy1IndentSemicolon
def tacticSeq1Indented : Parser :=
leading_parser sepBy1IndentSemicolon tacticParser
def tacticSeq1Indented : Parser := leading_parser
sepBy1IndentSemicolon tacticParser
/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
It runs the tactics in sequence, and fails if the goal is not solved. -/
def tacticSeqBracketed : Parser :=
leading_parser "{" >> sepByIndentSemicolon tacticParser >> ppDedent (ppLine >> "}")
def tacticSeq :=
leading_parser tacticSeqBracketed <|> tacticSeq1Indented
def tacticSeqBracketed : Parser := leading_parser
"{" >> sepByIndentSemicolon tacticParser >> ppDedent (ppLine >> "}")
def tacticSeq := leading_parser
tacticSeqBracketed <|> tacticSeq1Indented
/- Raw sequence for quotation and grouping -/
def seq1 :=
@ -66,7 +69,8 @@ namespace Term
/-! # Built-in parsers -/
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
@[builtin_term_parser] def byTactic := leading_parser:leadPrec ppAllowUngrouped >> "by " >> Tactic.tacticSeq
@[builtin_term_parser] def byTactic := leading_parser:leadPrec
ppAllowUngrouped >> "by " >> Tactic.tacticSeq
/-
This is the same as `byTactic`, but it uses a different syntax kind. This is
@ -74,36 +78,53 @@ namespace Term
support arbitrary terms where `byTactic` is accepted. Mathport uses this to e.g.
safely find-replace `by exact $e` by `$e` in any context without causing
incorrect syntax when the full expression is `show $T by exact $e`. -/
def byTactic' := leading_parser "by " >> Tactic.tacticSeq
def byTactic' := leading_parser
"by " >> Tactic.tacticSeq
-- TODO: rename to e.g. `afterSemicolonOrLinebreak`
def optSemicolon (p : Parser) : Parser := ppDedent $ semicolonOrLinebreak >> ppLine >> p
def optSemicolon (p : Parser) : Parser :=
ppDedent $ semicolonOrLinebreak >> ppLine >> p
-- `checkPrec` necessary for the pretty printer
@[builtin_term_parser] def ident := checkPrec maxPrec >> Parser.ident
@[builtin_term_parser] def num : Parser := checkPrec maxPrec >> numLit
@[builtin_term_parser] def scientific : Parser := checkPrec maxPrec >> scientificLit
@[builtin_term_parser] def str : Parser := checkPrec maxPrec >> strLit
@[builtin_term_parser] def char : Parser := checkPrec maxPrec >> charLit
@[builtin_term_parser] def ident :=
checkPrec maxPrec >> Parser.ident
@[builtin_term_parser] def num : Parser :=
checkPrec maxPrec >> numLit
@[builtin_term_parser] def scientific : Parser :=
checkPrec maxPrec >> scientificLit
@[builtin_term_parser] def str : Parser :=
checkPrec maxPrec >> strLit
@[builtin_term_parser] def char : Parser :=
checkPrec maxPrec >> charLit
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
@[builtin_term_parser] def type := leading_parser "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtin_term_parser] def type := leading_parser
"Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
/-- A specific universe in Lean's infinite hierarchy of universes. -/
@[builtin_term_parser] def sort := leading_parser "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
@[builtin_term_parser] def sort := leading_parser
"Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
/-- The universe of propositions. `Prop ≡ Sort 0`. -/
@[builtin_term_parser] def prop := leading_parser "Prop"
@[builtin_term_parser] def prop := leading_parser
"Prop"
/-- A placeholder term, to be synthesized by unification. -/
@[builtin_term_parser] def hole := leading_parser "_"
@[builtin_term_parser] def syntheticHole := leading_parser "?" >> (ident <|> hole)
@[builtin_term_parser] def hole := leading_parser
"_"
@[builtin_term_parser] def syntheticHole := leading_parser
"?" >> (ident <|> hole)
/-- A temporary placeholder for a missing proof or value. -/
@[builtin_term_parser] def «sorry» := leading_parser "sorry"
@[builtin_term_parser] def «sorry» := leading_parser
"sorry"
/--
A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses.
For example, `(· + ·)` is equivalent to `fun x y => x + y`.
-/
@[builtin_term_parser] def cdot := leading_parser symbol "·" <|> "."
def typeAscription := leading_parser " : " >> termParser
def tupleTail := leading_parser ", " >> sepBy1 termParser ", "
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@[builtin_term_parser] def cdot := leading_parser
symbol "·" <|> "."
def typeAscription := leading_parser
" : " >> termParser
def tupleTail := leading_parser
", " >> sepBy1 termParser ", "
def parenSpecial : Parser :=
optional (tupleTail <|> typeAscription)
/--
Parentheses, used for
- Grouping expressions, e.g., `a * (b + c)`.
@ -116,7 +137,8 @@ Parentheses, used for
- `(f · a b)` is shorthand for `fun x => f x a b`
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
-/
@[builtin_term_parser] def paren := leading_parser "(" >> (withoutPosition (withoutForbidden (optional (ppDedentIfGrouped termParser >> parenSpecial)))) >> ")"
@[builtin_term_parser] def paren := leading_parser
"(" >> (withoutPosition (withoutForbidden (optional (ppDedentIfGrouped termParser >> parenSpecial)))) >> ")"
/--
The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
expected type is an inductive type with a single constructor `c`.
@ -124,18 +146,30 @@ If more terms are given than `c` has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
-/
@[builtin_term_parser] def anonymousCtor := leading_parser "⟨" >> sepBy termParser ", " >> "⟩"
def optIdent : Parser := optional (atomic (ident >> " : "))
def fromTerm := leading_parser "from " >> termParser
@[builtin_term_parser] def anonymousCtor := leading_parser
"⟨" >> sepBy termParser ", " >> "⟩"
def optIdent : Parser :=
optional (atomic (ident >> " : "))
def fromTerm := leading_parser
"from " >> termParser
def showRhs := fromTerm <|> byTactic'
def sufficesDecl := leading_parser optIdent >> termParser >> ppSpace >> showRhs
@[builtin_term_parser] def «suffices» := leading_parser:leadPrec withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
def sufficesDecl := leading_parser
optIdent >> termParser >> ppSpace >> showRhs
@[builtin_term_parser] def «suffices» := leading_parser:leadPrec
withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
@[builtin_term_parser] def «show» := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
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 structInstFieldAbbrev := leading_parser atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation") -- `x` is an abbreviation for `x := x`
def optEllipsis := leading_parser optional ".."
def structInstArrayRef := leading_parser
"[" >> withoutPosition termParser >>"]"
def structInstLVal := leading_parser
(ident <|> fieldIdx <|> structInstArrayRef) >>
many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := ppGroup $ leading_parser
structInstLVal >> " := " >> termParser
def structInstFieldAbbrev := leading_parser
-- `x` is an abbreviation for `x := x`
atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation")
def optEllipsis := leading_parser
optional ".."
/--
Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
@ -145,37 +179,60 @@ A *structure update* of an existing value can be given via `with`:
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
-/
@[builtin_term_parser] def structInst := leading_parser "{" >> ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with "))
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
>> optEllipsis
>> optional (" : " >> termParser) >> " }"
@[builtin_term_parser] def structInst := leading_parser
"{" >> withoutPosition (ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with "))
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
>> optEllipsis
>> optional (" : " >> termParser)) >> " }"
def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
/--
`@x` disables automatic insertion of implicit parameters of the constant `x`.
`@e` for any term `e` also disables the insertion of implicit lambdas at this position.
-/
@[builtin_term_parser] def explicit := leading_parser "@" >> termParser maxPrec
@[builtin_term_parser] def explicit := leading_parser
"@" >> termParser maxPrec
/--
`.(e)` marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type.
-/
@[builtin_term_parser] def inaccessible := leading_parser ".(" >> termParser >> ")"
@[builtin_term_parser] def inaccessible := leading_parser
".(" >> withoutPosition termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then node nullKind (" : " >> termParser) else optional (" : " >> 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) >> ")"
/-- Implicit binder. In regular applications without `@`, it is automatically inserted and solved by unification whenever all explicit parameters before it are specified. -/
def implicitBinder (requireType := false) := ppGroup $ leading_parser "{" >> many1 binderIdent >> binderType requireType >> "}"
def binderType (requireType := false) : Parser :=
if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := leading_parser
atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
def binderDefault := leading_parser
" := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ leading_parser
"(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
/--
Implicit binder. In regular applications without `@`, it is automatically inserted
and solved by unification whenever all explicit parameters before it are specified.
-/
def implicitBinder (requireType := false) := ppGroup $ leading_parser
"{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
/-- Strict-implicit binder. In contrast to `{ ... }` regular implicit binders, a strict-implicit binder is inserted automatically only when at least one subsequent explicit parameter is specified. -/
def strictImplicitBinder (requireType := false) := ppGroup $ leading_parser strictImplicitLeftBracket >> many1 binderIdent >> binderType requireType >> strictImplicitRightBracket
/-- Instance-implicit binder. In regular applications without `@`, it is automatically inserted and solved by typeclass inference of the specified class. -/
def instBinder := ppGroup $ leading_parser "[" >> optIdent >> termParser >> "]"
def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" `Lean.Parser.Term.bracketedBinder (isPseudoKind := true)) <|
explicitBinder requireType <|> strictImplicitBinder requireType <|> implicitBinder requireType <|> instBinder
/--
Strict-implicit binder. In contrast to `{ ... }` regular implicit binders,
a strict-implicit binder is inserted automatically only when at least one subsequent
explicit parameter is specified.
-/
def strictImplicitBinder (requireType := false) := ppGroup <| leading_parser
strictImplicitLeftBracket >> many1 binderIdent >>
binderType requireType >> strictImplicitRightBracket
/--
Instance-implicit binder. In regular applications without `@`, it is automatically inserted
and solved by typeclass inference of the specified class.
-/
def instBinder := ppGroup <| leading_parser
"[" >> withoutPosition (optIdent >> termParser) >> "]"
def bracketedBinder (requireType := false) :=
withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
explicitBinder requireType <|> strictImplicitBinder requireType <|>
implicitBinder requireType <|> instBinder
/-
It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
@ -192,14 +249,21 @@ 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) → α → α`.
-/
@[builtin_term_parser] def depArrow := leading_parser:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
@[builtin_term_parser] def depArrow := leading_parser:25
bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
@[builtin_term_parser]
def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >> optType >> ", " >> termParser
def «forall» := leading_parser:leadPrec
unicodeSymbol "∀" "forall" >>
many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
optType >> ", " >> termParser
def matchAlt (rhsParser : Parser := termParser) : Parser :=
leading_parser (withAnonymousAntiquot := false)
"| " >> ppIndent (sepBy1 (sepBy1 termParser ", ") "|" >> darrow >> checkColGe "alternative right-hand-side to start in a column greater than or equal to the corresponding '|'" >> rhsParser)
"| " >> ppIndent (
sepBy1 (sepBy1 termParser ", ") "|" >> darrow >>
checkColGe "alternative right-hand-side to start in a column greater than or equal to the corresponding '|'" >>
rhsParser)
/--
Useful for syntax quotations. Note that generic patterns such as `` `(matchAltExpr| | ... => $rhs) `` should also
work with other `rhsParser`s (of arity 1). -/
@ -211,13 +275,18 @@ instance : Coe (TSyntax ``matchAltExpr) (TSyntax ``matchAlt) where
def matchAlts (rhsParser : Parser := termParser) : Parser :=
leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
def matchDiscr := leading_parser optional (atomic (ident >> " : ")) >> termParser
def matchDiscr := leading_parser
optional (atomic (ident >> " : ")) >> termParser
def trueVal := leading_parser nonReservedSymbol "true"
def falseVal := leading_parser nonReservedSymbol "false"
def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "generalizing") >> " := " >> (trueVal <|> falseVal) >> ")" >> ppSpace
def generalizingParam := leading_parser
atomic ("(" >> nonReservedSymbol "generalizing") >> " := " >>
(trueVal <|> falseVal) >> ")" >> ppSpace
def motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> termParser >> ")" >> ppSpace
def motive := leading_parser
atomic ("(" >> nonReservedSymbol "motive" >> " := ") >>
withoutPosition termParser >> ")" >> ppSpace
/--
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
@ -249,7 +318,9 @@ syntax "c" (foo <|> "bar") ...
```
they are not.
-/
@[builtin_term_parser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts
@[builtin_term_parser] def «match» := leading_parser:leadPrec
"match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >>
" with " >> ppDedent matchAlts
/--
Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
@ -257,19 +328,34 @@ e.g. because it has no constructors.
-/
@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <| atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
def funStrictImplicitBinder := atomic (lookahead (strictImplicitLeftBracket >> many1 binderIdent >> (symbol " : " <|> strictImplicitRightBracket))) >> strictImplicitBinder
def funBinder : Parser := withAntiquot (mkAntiquot "funBinder" `Lean.Parser.Term.funBinder (isPseudoKind := true)) (funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> termParser maxPrec)
-- NOTE: we disable anonymous antiquotations to ensure that `fun $b => ...` remains a `term` antiquotation
def basicFun : Parser := leading_parser (withAnonymousAntiquot := false) ppGroup (many1 (ppSpace >> funBinder) >> optType >> " =>") >> ppSpace >> termParser
@[builtin_term_parser] def «fun» := leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
def funStrictImplicitBinder :=
atomic (lookahead (
strictImplicitLeftBracket >> many1 binderIdent >>
(symbol " : " <|> strictImplicitRightBracket))) >>
strictImplicitBinder
def funBinder : Parser :=
withAntiquot (mkAntiquot "funBinder" decl_name% (isPseudoKind := true)) <|
funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> termParser maxPrec
-- NOTE: we disable anonymous antiquotations to ensure that `fun $b => ...`
-- remains a `term` antiquotation
def basicFun : Parser := leading_parser (withAnonymousAntiquot := false)
ppGroup (many1 (ppSpace >> funBinder) >> optType >> " =>") >> ppSpace >> termParser
@[builtin_term_parser] def «fun» := leading_parser:maxPrec
ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "withAnonymousAntiquot" >> " := ") >> (trueVal <|> falseVal) >> ")" >> ppSpace
@[builtin_term_parser] def «leading_parser» := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> optional withAnonymousAntiquot >> termParser
@[builtin_term_parser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser
def withAnonymousAntiquot := leading_parser
atomic ("(" >> nonReservedSymbol "withAnonymousAntiquot" >> " := ") >>
(trueVal <|> falseVal) >> ")" >> ppSpace
@[builtin_term_parser] def «leading_parser» := leading_parser:leadPrec
"leading_parser " >> optExprPrecedence >> optional withAnonymousAntiquot >> termParser
@[builtin_term_parser] def «trailing_parser» := leading_parser:leadPrec
"trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser
@[builtin_term_parser] def borrowed := leading_parser "@& " >> termParser leadPrec
@[builtin_term_parser] def borrowed := leading_parser
"@& " >> termParser leadPrec
/-- A literal of type `Name`. -/
@[builtin_term_parser] def quotedName := leading_parser nameLit
/--
@ -278,28 +364,44 @@ existent in the current context, or else fails.
-/
-- use `rawCh` because ``"`" >> ident`` overlaps with `nameLit`, with the latter being preferred by the tokenizer
-- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
@[builtin_term_parser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
@[builtin_term_parser] def doubleQuotedName := leading_parser
"`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
def letIdBinder := withAntiquot (mkAntiquot "letIdBinder" `Lean.Parser.Term.letIdBinder (isPseudoKind := true)) (binderIdent <|> bracketedBinder)
def letIdBinder :=
withAntiquot (mkAntiquot "letIdBinder" decl_name% (isPseudoKind := true)) <|
binderIdent <|> bracketedBinder
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
def letIdLhs : Parser := ident >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> letIdBinder) >> optType
def letIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (letIdLhs >> " := ") >> termParser
def letPatDecl := leading_parser (withAnonymousAntiquot := false) atomic (termParser >> pushNone >> optType >> " := ") >> termParser
def letIdLhs : Parser :=
ident >> notFollowedBy (checkNoWsBefore "" >> "[")
"space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >>
many (ppSpace >> letIdBinder) >> optType
def letIdDecl := leading_parser (withAnonymousAntiquot := false)
atomic (letIdLhs >> " := ") >> termParser
def letPatDecl := leading_parser (withAnonymousAntiquot := false)
atomic (termParser >> pushNone >> optType >> " := ") >> termParser
/-
Remark: the following `(" := " <|> matchAlts)` is a hack we use to produce a better error message at `letDecl`.
Remark: the following `(" := " <|> matchAlts)` is a hack we use
to produce a better error message at `letDecl`.
Consider this following example
```
def myFun (n : Nat) : IO Nat :=
let q ← (10 : Nat)
n + q
```
Without the hack, we get the error `expected '|'` at `←`. Reason: at `letDecl`, we use the parser `(letIdDecl <|> letPatDecl <|> letEqnsDecl)`,
Without the hack, we get the error `expected '|'` at `←`. Reason: at `letDecl`,
we use the parser `(letIdDecl <|> letPatDecl <|> letEqnsDecl)`,
`letIdDecl` and `letEqnsDecl` have the same prefix `letIdLhs`, but `letIdDecl` uses `atomic`.
Note that the hack relies on the fact that the parser `":="` never succeeds at `(" := " <|> matchAlts)`. It is there just to make sure we produce the error `expected ':=' or '|'`
Note that the hack relies on the fact that the parser `":="` never succeeds
at `(" := " <|> matchAlts)`.
It is there just to make sure we produce the error `expected ':=' or '|'`
-/
def letEqnsDecl := leading_parser (withAnonymousAntiquot := false) letIdLhs >> (" := " <|> matchAlts)
-- Remark: we disable anonymous antiquotations here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := leading_parser (withAnonymousAntiquot := false) notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)
def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
letIdLhs >> (" := " <|> matchAlts)
-- Remark: we disable anonymous antiquotations here to make sure
-- anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := leading_parser (withAnonymousAntiquot := false)
notFollowedBy (nonReservedSymbol "rec") "rec" >>
(letIdDecl <|> letPatDecl <|> letEqnsDecl)
/--
`let` is used to declare a local definition. Example:
```
@ -307,103 +409,142 @@ let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare local functions too.
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
-/
@[builtin_term_parser] def «let» := leading_parser:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
@[builtin_term_parser] def «let» := leading_parser:leadPrec
withPosition ("let " >> letDecl) >> optSemicolon termParser
/--
`let_fun x := v; b` is syntax sugar for `(fun x => b) v`. It is very similar to `let x := v; b`, but they are not equivalent.
`let_fun x := v; b` is syntax sugar for `(fun x => b) v`.
It is very similar to `let x := v; b`, but they are not equivalent.
In `let_fun`, the value `v` has been abstracted away and cannot be accessed in `b`.
-/
@[builtin_term_parser] def «let_fun» := leading_parser:leadPrec withPosition ((symbol "let_fun " <|> "let_λ") >> letDecl) >> optSemicolon termParser
@[builtin_term_parser] def «let_fun» := leading_parser:leadPrec
withPosition ((symbol "let_fun " <|> "let_λ") >> letDecl) >> optSemicolon termParser
/--
`let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
-/
@[builtin_term_parser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
@[builtin_term_parser] def «let_delayed» := leading_parser:leadPrec
withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
/--
`let`-declaration that is only included in the elaborated term if variable is still there.
It is often used when building macros.
-/
@[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
@[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec
withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
/- like `let_fun` but with optional name -/
def haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
def haveIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (haveIdLhs >> " := ") >> termParser
def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false) haveIdLhs >> matchAlts
def haveDecl := leading_parser (withAnonymousAntiquot := false) haveIdDecl <|> letPatDecl <|> haveEqnsDecl
@[builtin_term_parser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
def haveIdDecl := leading_parser (withAnonymousAntiquot := false)
atomic (haveIdLhs >> " := ") >> termParser
def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)
haveIdLhs >> matchAlts
def haveDecl := leading_parser (withAnonymousAntiquot := false)
haveIdDecl <|> letPatDecl <|> haveEqnsDecl
@[builtin_term_parser] def «have» := leading_parser:leadPrec
withPosition ("have " >> haveDecl) >> 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 := leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecl := leading_parser optional Command.docComment >> optional «attributes» >> letDecl
def letRecDecls := leading_parser sepBy1 letRecDecl ", "
def attributes := leading_parser
"@[" >> withoutPosition (sepBy1 attrInstance ", ") >> "]"
def letRecDecl := leading_parser
optional Command.docComment >> optional «attributes» >> letDecl
def letRecDecls := leading_parser
sepBy1 letRecDecl ", "
@[builtin_term_parser]
def «letrec» := leading_parser:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
def «letrec» := leading_parser:leadPrec
withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >>
optSemicolon termParser
@[run_builtin_parser_attribute_hooks]
def whereDecls := leading_parser " where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
def whereDecls := leading_parser
" where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
@[run_builtin_parser_attribute_hooks]
def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
def matchAltsWhereDecls := leading_parser
matchAlts >> optional whereDecls
@[builtin_term_parser] def noindex := leading_parser "no_index " >> termParser maxPrec
@[builtin_term_parser] def noindex := leading_parser
"no_index " >> termParser maxPrec
@[builtin_term_parser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binrel := leading_parser
"binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
/-- Similar to `binrel`, but coerce `Prop` arguments into `Bool`. -/
@[builtin_term_parser] def binrel_no_prop := leading_parser "binrel_no_prop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binrel_no_prop := leading_parser
"binrel_no_prop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binop := leading_parser
"binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def binop_lazy := leading_parser
"binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def forInMacro' := leading_parser "for_in'% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def forInMacro := leading_parser
"for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtin_term_parser] def forInMacro' := leading_parser
"for_in'% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
/-- A macro which evaluates to the name of the currently elaborating declaration. -/
@[builtin_term_parser] def declName := leading_parser "decl_name%"
@[builtin_term_parser] def declName := leading_parser "decl_name%"
/--
* `with_decl_name% id e` elaborates `e` in a context while changing the effective
declaration name to `id`.
* `with_decl_name% ?id e` does the same, but resolves `id` as a new definition name
(appending the current namespaces).
-/
@[builtin_term_parser] def withDeclName := leading_parser "with_decl_name% " >> optional "?" >> ident >> termParser
@[builtin_term_parser] def typeOf := leading_parser "type_of% " >> termParser maxPrec
@[builtin_term_parser] def ensureTypeOf := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
@[builtin_term_parser] def ensureExpectedType := leading_parser "ensure_expected_type% " >> strLit >> termParser maxPrec
@[builtin_term_parser] def noImplicitLambda := leading_parser "no_implicit_lambda% " >> termParser maxPrec
@[builtin_term_parser] def withDeclName := leading_parser
"with_decl_name% " >> optional "?" >> ident >> termParser
@[builtin_term_parser] def typeOf := leading_parser
"type_of% " >> termParser maxPrec
@[builtin_term_parser] def ensureTypeOf := leading_parser
"ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
@[builtin_term_parser] def ensureExpectedType := leading_parser
"ensure_expected_type% " >> strLit >> termParser maxPrec
@[builtin_term_parser] def noImplicitLambda := leading_parser
"no_implicit_lambda% " >> termParser maxPrec
/--
`clear% x; e` elaborates `x` after clearing the free variable `x` from the local context.
If `x` cannot be cleared (due to dependencies), it will keep `x` without failing.
-/
@[builtin_term_parser] def clear := leading_parser "clear% " >> ident >> semicolonOrLinebreak >> termParser
@[builtin_term_parser] def clear := leading_parser
"clear% " >> ident >> semicolonOrLinebreak >> termParser
@[builtin_term_parser] def letMVar := leading_parser "let_mvar% " >> "?" >> ident >> " := " >> termParser >> "; " >> termParser
@[builtin_term_parser] def waitIfTypeMVar := leading_parser "wait_if_type_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def waitIfTypeContainsMVar := leading_parser "wait_if_type_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def waitIfContainsMVar := leading_parser "wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def letMVar := leading_parser
"let_mvar% " >> "?" >> ident >> " := " >> termParser >> "; " >> termParser
@[builtin_term_parser] def waitIfTypeMVar := leading_parser
"wait_if_type_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def waitIfTypeContainsMVar := leading_parser
"wait_if_type_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def waitIfContainsMVar := leading_parser
"wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtin_term_parser] def defaultOrOfNonempty := leading_parser "default_or_ofNonempty% " >> optional "unsafe"
@[builtin_term_parser] def defaultOrOfNonempty := leading_parser
"default_or_ofNonempty% " >> optional "unsafe"
/--
Helper parser for marking `match`-alternatives that should not trigger errors if unused.
We use them to implement `macro_rules` and `elab_rules`
-/
@[builtin_term_parser] def noErrorIfUnused := leading_parser "no_error_if_unused%" >> termParser
@[builtin_term_parser] def noErrorIfUnused := leading_parser
"no_error_if_unused%" >> termParser
def namedArgument := leading_parser (withAnonymousAntiquot := false) atomic ("(" >> ident >> " := ") >> termParser >> ")"
def namedArgument := leading_parser (withAnonymousAntiquot := false)
atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
def ellipsis := leading_parser (withAnonymousAntiquot := false) ".."
def argument :=
checkWsBefore "expected space" >>
@ -412,41 +553,61 @@ def argument :=
-- `app` precedence is `lead` (cannot be used as argument)
-- `lhs` precedence is `max` (i.e. does not accept `arg` precedence)
-- argument precedence is `arg` (i.e. does not accept `lead` precedence)
@[builtin_term_parser] def app := trailing_parser:leadPrec:maxPrec many1 argument
@[builtin_term_parser] def app := trailing_parser:leadPrec:maxPrec many1 argument
/--
The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
More precisely,
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)` where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`), `e.f` is translated to `T.f (p := e)` where
`p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type, the above is repeated for every base type of the structure.
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
`e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type,
the above is repeated for every base type of the structure.
The field index notation `e.i`, where `i` is a positive number, is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. -/
@[builtin_term_parser] def proj := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
@[builtin_term_parser] def completion := trailing_parser checkNoWsBefore >> "."
@[builtin_term_parser] def arrow := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
The field index notation `e.i`, where `i` is a positive number,
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. -/
@[builtin_term_parser] def proj := trailing_parser
checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
@[builtin_term_parser] def completion := trailing_parser
checkNoWsBefore >> "."
@[builtin_term_parser] 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
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
checkStackTop isIdent "expected preceding identifier" >>
checkNoWsBefore "no space before '.{'" >> ".{" >>
sepBy1 levelParser ", " >> "}"
/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
@[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
@[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
checkStackTop isIdent "expected preceding identifier" >>
checkNoWsBefore "no space before '@'" >> "@" >>
optional (atomic (ident >> ":")) >> termParser maxPrec
/-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/
@[builtin_term_parser] def pipeProj := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
@[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec " |>."
/--
`e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
-/
@[builtin_term_parser] def pipeProj := trailing_parser:minPrec
" |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
@[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec
" |>."
/--
`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`.
See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.
You can also view `h ▸ e` as a "type casting" operation
where you change the type of `e` by using `h`.
See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
-/
@[builtin_term_parser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@[builtin_term_parser] def subst := trailing_parser:75
" ▸ " >> sepBy1 (termParser 75) " ▸ "
def bracketedBinderF := bracketedBinder -- no default arg
instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩
@ -459,16 +620,21 @@ function `lean_set_panic_messages(false)` has been executed before. If the C
function `lean_set_exit_on_panic(true)` has been executed before, the process is
then aborted.
-/
@[builtin_term_parser] def panic := leading_parser:leadPrec "panic! " >> termParser
@[builtin_term_parser] def panic := leading_parser:leadPrec
"panic! " >> termParser
/-- A shorthand for `panic! "unreachable code has been reached"`. -/
@[builtin_term_parser] def unreachable := leading_parser:leadPrec "unreachable!"
@[builtin_term_parser] def unreachable := leading_parser:leadPrec
"unreachable!"
/--
`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
-/
@[builtin_term_parser] def dbgTrace := leading_parser:leadPrec withPosition ("dbg_trace" >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtin_term_parser] def dbgTrace := leading_parser:leadPrec
withPosition ("dbg_trace" >> (interpolatedStr termParser <|> termParser)) >>
optSemicolon termParser
/-- `assert! cond` panics if `cond` evaluates to `false`. -/
@[builtin_term_parser] def assert := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
@[builtin_term_parser] def assert := leading_parser:leadPrec
withPosition ("assert! " >> termParser) >> optSemicolon termParser
def macroArg := termParser maxPrec
@ -476,16 +642,21 @@ def macroDollarArg := leading_parser "$" >> termParser 10
def macroLastArg := macroDollarArg <|> macroArg
-- Macro for avoiding exponentially big terms when using `STWorld`
@[builtin_term_parser] def stateRefT := leading_parser "StateRefT" >> macroArg >> macroLastArg
@[builtin_term_parser] def stateRefT := leading_parser
"StateRefT" >> macroArg >> macroLastArg
@[builtin_term_parser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
@[builtin_term_parser] def dynamicQuot := leading_parser
"`(" >> ident >> "|" >> withoutPosition (incQuotDepth (parserOfStack 1)) >> ")"
@[builtin_term_parser] def dotIdent := leading_parser "." >> checkNoWsBefore >> rawIdent
@[builtin_term_parser] def dotIdent := leading_parser
"." >> checkNoWsBefore >> rawIdent
end Term
@[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"
@[builtin_term_parser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")"
@[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
"`(tactic|" >> withoutPosition (incQuotDepth tacticParser) >> ")"
@[builtin_term_parser] def Tactic.quotSeq : Parser := leading_parser
"`(tactic|" >> withoutPosition (incQuotDepth Tactic.seq1) >> ")"
open Term in
builtin_initialize

132
stage0/src/Lean/PrettyPrinter/Formatter.lean generated
View file

@ -173,7 +173,7 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter :=
else
x
@[combinator_formatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter :=
@[combinator_formatter orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter :=
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
@ -211,20 +211,20 @@ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do
@[implemented_by formatterForKindUnsafe]
opaque formatterForKind (k : SyntaxNodeKind) : Formatter
@[combinator_formatter Lean.Parser.withAntiquot]
@[combinator_formatter withAntiquot]
def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.formatter antiP p
@[combinator_formatter Lean.Parser.withAntiquotSuffixSplice]
@[combinator_formatter withAntiquotSuffixSplice]
def withAntiquotSuffixSplice.formatter (_ : SyntaxNodeKind) (p suffix : Formatter) : Formatter := do
if (← getCur).isAntiquotSuffixSplice then
visitArgs <| suffix *> p
else
p
@[combinator_formatter Lean.Parser.tokenWithAntiquot]
@[combinator_formatter tokenWithAntiquot]
def tokenWithAntiquot.formatter (p : Formatter) : Formatter := do
if (← getCur).isTokenAntiquot then
visitArgs p
@ -246,7 +246,7 @@ def categoryFormatterCore (cat : Name) : Formatter := do
withAntiquot.formatter (mkAntiquot.formatter' cat.toString cat (isPseudoKind := true)) (formatterForKind stx.getKind)
modify fun st => { st with mustBeGrouped := true, isUngrouped := !st.mustBeGrouped }
@[combinator_formatter Lean.Parser.categoryParser]
@[combinator_formatter categoryParser]
def categoryParser.formatter (cat : Name) : Formatter := do
concat <| categoryFormatterCore cat
unless (← get).isUngrouped do
@ -259,31 +259,31 @@ def categoryParser.formatter (cat : Name) : Formatter := do
def categoryFormatter (cat : Name) : Formatter :=
fill <| indent <| categoryFormatterCore cat
@[combinator_formatter Lean.Parser.categoryParserOfStack]
@[combinator_formatter categoryParserOfStack]
def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
categoryParser.formatter stx.getId
@[combinator_formatter Lean.Parser.parserOfStack]
@[combinator_formatter parserOfStack]
def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
formatterForKind stx.getKind
@[combinator_formatter Lean.Parser.error]
@[combinator_formatter error]
def error.formatter (_msg : String) : Formatter := pure ()
@[combinator_formatter Lean.Parser.errorAtSavedPos]
@[combinator_formatter errorAtSavedPos]
def errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Formatter := pure ()
@[combinator_formatter Lean.Parser.atomic]
@[combinator_formatter atomic]
def atomic.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.lookahead]
@[combinator_formatter lookahead]
def lookahead.formatter (_ : Formatter) : Formatter := pure ()
@[combinator_formatter Lean.Parser.notFollowedBy]
@[combinator_formatter notFollowedBy]
def notFollowedBy.formatter (_ : Formatter) : Formatter := pure ()
@[combinator_formatter Lean.Parser.andthen]
@[combinator_formatter andthen]
def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1
def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
@ -292,12 +292,12 @@ def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
trace[PrettyPrinter.format.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
throwBacktrack
@[combinator_formatter Lean.Parser.node]
@[combinator_formatter node]
def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do
checkKind k;
visitArgs p
@[combinator_formatter Lean.Parser.trailingNode]
@[combinator_formatter trailingNode]
def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Formatter := do
checkKind k
visitArgs do
@ -370,7 +370,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
modify fun st => { st with leadWord := "" }
| _ => pure ()
@[combinator_formatter Lean.Parser.symbolNoAntiquot]
@[combinator_formatter symbolNoAntiquot]
def symbolNoAntiquot.formatter (sym : String) : Formatter := do
let stx ← getCur
if stx.isToken sym then do
@ -381,11 +381,11 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'"
throwBacktrack
@[combinator_formatter Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter
@[combinator_formatter nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter
@[combinator_formatter Lean.Parser.rawCh] def rawCh.formatter (ch : Char) := symbolNoAntiquot.formatter ch.toString
@[combinator_formatter rawCh] def rawCh.formatter (ch : Char) := symbolNoAntiquot.formatter ch.toString
@[combinator_formatter Lean.Parser.unicodeSymbolNoAntiquot]
@[combinator_formatter unicodeSymbolNoAntiquot]
def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
let Syntax.atom info val ← getCur
| throwError m!"not an atom: {← getCur}"
@ -395,7 +395,7 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
pushToken info asciiSym;
goLeft
@[combinator_formatter Lean.Parser.identNoAntiquot]
@[combinator_formatter identNoAntiquot]
def identNoAntiquot.formatter : Formatter := do
checkKind identKind
let stx@(Syntax.ident info _ id _) ← getCur
@ -404,14 +404,14 @@ def identNoAntiquot.formatter : Formatter := do
withMaybeTag (getExprPos? stx) (pushToken info id.toString)
goLeft
@[combinator_formatter Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
@[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
checkKind identKind
let Syntax.ident info _ id _ ← getCur
| throwError m!"not an ident: {← getCur}"
pushToken info id.toString
goLeft
@[combinator_formatter Lean.Parser.identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
@[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
def visitAtom (k : SyntaxNodeKind) : Formatter := do
let stx ← getCur
@ -422,24 +422,24 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
pushToken info val
goLeft
@[combinator_formatter Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@[combinator_formatter Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
@[combinator_formatter Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
@[combinator_formatter Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
@[combinator_formatter Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind
@[combinator_formatter Lean.Parser.fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
@[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@[combinator_formatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
@[combinator_formatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
@[combinator_formatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
@[combinator_formatter scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind
@[combinator_formatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
@[combinator_formatter Lean.Parser.manyNoAntiquot]
@[combinator_formatter manyNoAntiquot]
def manyNoAntiquot.formatter (p : Formatter) : Formatter := do
let stx ← getCur
visitArgs $ stx.getArgs.size.forM fun _ => p
@[combinator_formatter Lean.Parser.many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p
@[combinator_formatter many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p
@[combinator_formatter Lean.Parser.optionalNoAntiquot]
@[combinator_formatter optionalNoAntiquot]
def optionalNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p
@[combinator_formatter Lean.Parser.many1Unbox]
@[combinator_formatter many1Unbox]
def many1Unbox.formatter (p : Formatter) : Formatter := do
let stx ← getCur
if stx.getKind == nullKind then do
@ -447,65 +447,65 @@ def many1Unbox.formatter (p : Formatter) : Formatter := do
else
p
@[combinator_formatter Lean.Parser.sepByNoAntiquot]
@[combinator_formatter sepByNoAntiquot]
def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
let stx ← getCur
visitArgs <| (List.range stx.getArgs.size).reverse.forM fun i => if i % 2 == 0 then p else pSep
@[combinator_formatter Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter
@[combinator_formatter sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter
@[combinator_formatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withoutInfo] def withoutInfo.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.setExpected]
@[combinator_formatter withPosition] def withPosition.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withPositionAfterLinebreak] def withPositionAfterLinebreak.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p
@[combinator_formatter withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withoutInfo] def withoutInfo.formatter (p : Formatter) : Formatter := p
@[combinator_formatter setExpected]
def setExpected.formatter (_expected : List String) (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (_declName : Name) (p : Formatter) : Formatter := p
@[combinator_formatter incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinator_formatter decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinator_formatter suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
@[combinator_formatter evalInsideQuot] def evalInsideQuot.formatter (_declName : Name) (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
@[combinator_formatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
let st ← get
if st.leadWord != "" then
pushLine
@[combinator_formatter Lean.Parser.checkPrec] def checkPrec.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkLhsPrec] def checkLhsPrec.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.setLhsPrec] def setLhsPrec.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkStackTop] def checkStackTop.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
@[combinator_formatter checkPrec] def checkPrec.formatter : Formatter := pure ()
@[combinator_formatter checkLhsPrec] def checkLhsPrec.formatter : Formatter := pure ()
@[combinator_formatter setLhsPrec] def setLhsPrec.formatter : Formatter := pure ()
@[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
@[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
-- prevent automatic whitespace insertion
modify fun st => { st with leadWord := "" }
@[combinator_formatter Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkTailWs] def checkTailWs.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkColEq] def checkColEq.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkColGe] def checkColGe.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkColGt] def checkColGt.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkLineEq] def checkLineEq.formatter : Formatter := pure ()
@[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
@[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
@[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure ()
@[combinator_formatter checkColGe] def checkColGe.formatter : Formatter := pure ()
@[combinator_formatter checkColGt] def checkColGt.formatter : Formatter := pure ()
@[combinator_formatter checkLineEq] def checkLineEq.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.eoi] def eoi.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.skip] def skip.formatter : Formatter := pure ()
@[combinator_formatter eoi] def eoi.formatter : Formatter := pure ()
@[combinator_formatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
@[combinator_formatter skip] def skip.formatter : Formatter := pure ()
@[combinator_formatter Lean.Parser.pushNone] def pushNone.formatter : Formatter := goLeft
@[combinator_formatter pushNone] def pushNone.formatter : Formatter := goLeft
@[combinator_formatter Lean.Parser.withOpenDecl] def withOpenDecl.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.withOpen] def withOpen.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withOpenDecl] def withOpenDecl.formatter (p : Formatter) : Formatter := p
@[combinator_formatter withOpen] def withOpen.formatter (p : Formatter) : Formatter := p
@[combinator_formatter Lean.Parser.interpolatedStr]
@[combinator_formatter interpolatedStr]
def interpolatedStr.formatter (p : Formatter) : Formatter := do
visitArgs $ (← getCur).getArgs.reverse.forM fun chunk =>
match chunk.isLit? interpolatedStrLitKind with
| some str => push str *> goLeft
| none => p
@[combinator_formatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (_label : String) (p : Formatter) : Formatter := p
@[combinator_formatter dbgTraceState] def dbgTraceState.formatter (_label : String) (p : Formatter) : Formatter := p
@[combinator_formatter ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Formatter) : Formatter :=
@[combinator_formatter _root_.ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Formatter) : Formatter :=
if c then t else e
abbrev FormatterAliasValue := AliasValue Formatter

132
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean generated
View file

@ -162,7 +162,7 @@ unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttr
namespace Parenthesizer
open Lean.Core
open Lean.Core Parser
open Std.Format
def throwBacktrack {α} : ParenthesizerM α :=
@ -247,7 +247,7 @@ def visitToken : Parenthesizer := do
modify fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true }
goLeft
@[combinator_parenthesizer Lean.Parser.orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
@[combinator_parenthesizer orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
@ -276,7 +276,7 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
@[implemented_by parenthesizerForKindUnsafe]
opaque parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
@[combinator_parenthesizer Lean.Parser.withAntiquot]
@[combinator_parenthesizer withAntiquot]
def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
-- early check as minor optimization that also cleans up the backtrack traces
@ -285,14 +285,14 @@ def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do
else
p
@[combinator_parenthesizer Lean.Parser.withAntiquotSuffixSplice]
@[combinator_parenthesizer withAntiquotSuffixSplice]
def withAntiquotSuffixSplice.parenthesizer (_ : SyntaxNodeKind) (p suffix : Parenthesizer) : Parenthesizer := do
if (← getCur).isAntiquotSuffixSplice then
visitArgs <| suffix *> p
else
p
@[combinator_parenthesizer Lean.Parser.tokenWithAntiquot]
@[combinator_parenthesizer tokenWithAntiquot]
def tokenWithAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
if (← getCur).isTokenAntiquot then
visitArgs p
@ -310,7 +310,7 @@ def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer :=
withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString cat (isPseudoKind := true)) (parenthesizerForKind stx.getKind)
modify fun st => { st with contCat := cat }
@[combinator_parenthesizer Lean.Parser.categoryParser]
@[combinator_parenthesizer categoryParser]
def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
let env ← getEnv
match categoryParenthesizerAttribute.getValues env cat with
@ -319,13 +319,13 @@ def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
-- In this case this node will never be parenthesized since we don't know which parentheses to use.
| _ => parenthesizeCategoryCore cat prec
@[combinator_parenthesizer Lean.Parser.categoryParserOfStack]
@[combinator_parenthesizer categoryParserOfStack]
def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesizer := do
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
categoryParser.parenthesizer stx.getId prec
@[combinator_parenthesizer Lean.Parser.parserOfStack]
@[combinator_parenthesizer parserOfStack]
def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesizer := do
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
@ -350,27 +350,27 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
def rawStx.parenthesizer : CategoryParenthesizer | _ => do
goLeft
@[combinator_parenthesizer Lean.Parser.error]
@[combinator_parenthesizer error]
def error.parenthesizer (_msg : String) : Parenthesizer :=
pure ()
@[combinator_parenthesizer Lean.Parser.errorAtSavedPos]
@[combinator_parenthesizer errorAtSavedPos]
def errorAtSavedPos.parenthesizer (_msg : String) (_delta : Bool) : Parenthesizer :=
pure ()
@[combinator_parenthesizer Lean.Parser.atomic]
@[combinator_parenthesizer atomic]
def atomic.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p
@[combinator_parenthesizer Lean.Parser.lookahead]
@[combinator_parenthesizer lookahead]
def lookahead.parenthesizer (_ : Parenthesizer) : Parenthesizer :=
pure ()
@[combinator_parenthesizer Lean.Parser.notFollowedBy]
@[combinator_parenthesizer notFollowedBy]
def notFollowedBy.parenthesizer (_ : Parenthesizer) : Parenthesizer :=
pure ()
@[combinator_parenthesizer Lean.Parser.andthen]
@[combinator_parenthesizer andthen]
def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer :=
p2 *> p1
@ -381,16 +381,16 @@ def checkKind (k : SyntaxNodeKind) : Parenthesizer := do
-- HACK; see `orelse.parenthesizer`
throwBacktrack
@[combinator_parenthesizer Lean.Parser.node]
@[combinator_parenthesizer node]
def node.parenthesizer (k : SyntaxNodeKind) (p : Parenthesizer) : Parenthesizer := do
checkKind k
visitArgs p
@[combinator_parenthesizer Lean.Parser.checkPrec]
@[combinator_parenthesizer checkPrec]
def checkPrec.parenthesizer (prec : Nat) : Parenthesizer :=
addPrecCheck prec
@[combinator_parenthesizer Lean.Parser.leadingNode]
@[combinator_parenthesizer leadingNode]
def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
node.parenthesizer k p
addPrecCheck prec
@ -399,7 +399,7 @@ def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesiz
-- into a trailing one.
modify fun st => { st with contPrec := Nat.min (Parser.maxPrec-1) prec }
@[combinator_parenthesizer Lean.Parser.trailingNode]
@[combinator_parenthesizer trailingNode]
def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Parenthesizer) : Parenthesizer := do
checkKind k
visitArgs do
@ -413,33 +413,33 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Pa
-- parser is calling us.
categoryParser.parenthesizer ctx.cat lhsPrec
@[combinator_parenthesizer Lean.Parser.rawCh] def rawCh.parenthesizer (_ch : Char) := visitToken
@[combinator_parenthesizer rawCh] def rawCh.parenthesizer (_ch : Char) := visitToken
@[combinator_parenthesizer Lean.Parser.symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (_sym : String) := visitToken
@[combinator_parenthesizer Lean.Parser.unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken
@[combinator_parenthesizer symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (_sym : String) := visitToken
@[combinator_parenthesizer unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken
@[combinator_parenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := do checkKind identKind; visitToken
@[combinator_parenthesizer Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.identEq] def identEq.parenthesizer (_id : Name) := visitToken
@[combinator_parenthesizer Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken
@[combinator_parenthesizer identNoAntiquot] def identNoAntiquot.parenthesizer := do checkKind identKind; visitToken
@[combinator_parenthesizer rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer identEq] def identEq.parenthesizer (_id : Name) := visitToken
@[combinator_parenthesizer nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken
@[combinator_parenthesizer Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.fieldIdx] def fieldIdx.parenthesizer := visitToken
@[combinator_parenthesizer charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer nameLitNoAntiquot] def nameLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer numLitNoAntiquot] def numLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken
@[combinator_parenthesizer fieldIdx] def fieldIdx.parenthesizer := visitToken
@[combinator_parenthesizer Lean.Parser.manyNoAntiquot]
@[combinator_parenthesizer manyNoAntiquot]
def manyNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
visitArgs $ stx.getArgs.size.forM fun _ => p
@[combinator_parenthesizer Lean.Parser.many1NoAntiquot]
@[combinator_parenthesizer many1NoAntiquot]
def many1NoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
manyNoAntiquot.parenthesizer p
@[combinator_parenthesizer Lean.Parser.many1Unbox]
@[combinator_parenthesizer many1Unbox]
def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
if stx.getKind == nullKind then
@ -447,55 +447,55 @@ def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do
else
p
@[combinator_parenthesizer Lean.Parser.optionalNoAntiquot]
@[combinator_parenthesizer optionalNoAntiquot]
def optionalNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
visitArgs p
@[combinator_parenthesizer Lean.Parser.sepByNoAntiquot]
@[combinator_parenthesizer sepByNoAntiquot]
def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
let stx ← getCur
visitArgs <| (List.range stx.getArgs.size).reverse.forM fun i => if i % 2 == 0 then p else pSep
@[combinator_parenthesizer Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.parenthesizer := sepByNoAntiquot.parenthesizer
@[combinator_parenthesizer sepBy1NoAntiquot] def sepBy1NoAntiquot.parenthesizer := sepByNoAntiquot.parenthesizer
@[combinator_parenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
@[combinator_parenthesizer withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
-- We assume the formatter will indent syntax sufficiently such that parenthesizing a `withPosition` node is never necessary
modify fun st => { st with contPrec := none }
p
@[combinator_parenthesizer Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.parenthesizer (p : Parenthesizer) : Parenthesizer :=
@[combinator_parenthesizer withPositionAfterLinebreak] def withPositionAfterLinebreak.parenthesizer (p : Parenthesizer) : Parenthesizer :=
-- TODO: improve?
withPosition.parenthesizer p
@[combinator_parenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.withoutInfo] def withoutInfo.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.setExpected]
@[combinator_parenthesizer withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer withoutInfo] def withoutInfo.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer setExpected]
def setExpected.parenthesizer (_expected : List String) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (_declName : Name) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer evalInsideQuot] def evalInsideQuot.parenthesizer (_declName : Name) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkColEq] def checkColEq.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkLineEq] def checkLineEq.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.eoi] def eoi.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.skip] def skip.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkLinebreakBefore] def checkLinebreakBefore.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkColEq] def checkColEq.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkLineEq] def checkLineEq.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer eoi] def eoi.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer skip] def skip.parenthesizer : Parenthesizer := pure ()
@[combinator_parenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
@[combinator_parenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
@[combinator_parenthesizer Lean.Parser.withOpenDecl] def withOpenDecl.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.withOpen] def withOpen.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer withOpenDecl] def withOpenDecl.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer withOpen] def withOpen.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer Lean.Parser.interpolatedStr]
@[combinator_parenthesizer interpolatedStr]
def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
visitArgs $ (← getCur).getArgs.reverse.forM fun chunk =>
if chunk.isOfKind interpolatedStrLitKind then
@ -503,9 +503,9 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
else
p
@[combinator_parenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (_label : String) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer dbgTraceState] def dbgTraceState.parenthesizer (_label : String) (p : Parenthesizer) : Parenthesizer := p
@[combinator_parenthesizer ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Parenthesizer) : Parenthesizer :=
@[combinator_parenthesizer _root_.ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Parenthesizer) : Parenthesizer :=
if c then t else e
open Parser

1622
stage0/stdlib/Lean/Parser.c generated
View file

File diff suppressed because it is too large Load diff

1839
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff

534
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

238
stage0/stdlib/Lean/Parser/Level.c generated
View file

@ -66,6 +66,7 @@ static lean_object* l_Lean_Parser_Level_imax_parenthesizer___closed__4;
static lean_object* l_Lean_Parser_Level_hole_formatter___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Level_ident_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Level_imax_parenthesizer___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withoutPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_levelParser_formatter(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Level_paren_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Level_max_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -111,6 +112,7 @@ extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Level___hyg_5____closed__3;
static lean_object* l___regBuiltin_Lean_Parser_Level_num_declRange___closed__6;
static lean_object* l_Lean_Parser_Level_addLit_formatter___closed__1;
static lean_object* l_Lean_Parser_Level_paren___closed__14;
static lean_object* l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__3;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Level_addLit_declRange(lean_object*);
static lean_object* l___regBuiltin_Lean_Parser_Level_num_declRange___closed__1;
@ -217,6 +219,7 @@ static lean_object* l_Lean_Parser_Level_max_parenthesizer___closed__3;
static lean_object* l___regBuiltin_Lean_Parser_Level_max_declRange___closed__2;
static lean_object* l___regBuiltin_Lean_Parser_Level_imax_declRange___closed__1;
lean_object* l_Lean_Parser_ident_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withoutPosition(lean_object*);
static lean_object* l_Lean_Parser_Level_hole_parenthesizer___closed__1;
static lean_object* l_Lean_Parser_Level_paren_formatter___closed__5;
LEAN_EXPORT lean_object* l_Lean_Parser_levelParser_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -261,6 +264,7 @@ lean_object* l_Lean_Parser_andthen(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Level_imax___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Level_imax___closed__6;
static lean_object* l_Lean_Parser_Level_paren_parenthesizer___closed__8;
static lean_object* l_Lean_Parser_Level_imax_formatter___closed__3;
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Level_addLit___closed__4;
@ -273,12 +277,14 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Level_hole_formatter(lean_object*, lean_o
static lean_object* l_Lean_Parser_Level_hole___closed__7;
static lean_object* l_Lean_Parser_Level_imax___closed__4;
static lean_object* l_Lean_Parser_Level_paren_parenthesizer___closed__1;
static lean_object* l_Lean_Parser_Level_paren_formatter___closed__8;
static lean_object* l_Lean_Parser_Level_paren_formatter___closed__2;
lean_object* l_Lean_Parser_ident_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_symbol_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Level_max_parenthesizer___closed__7;
static lean_object* l_Lean_Parser_Level_paren___closed__8;
static lean_object* l_Lean_Parser_Level_hole___closed__4;
lean_object* l_Lean_PrettyPrinter_Formatter_withoutPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Parser_Level_hole_formatter___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Level___hyg_5_(lean_object*);
static lean_object* l___regBuiltin_Lean_Parser_Level_imax_declRange___closed__4;
@ -459,35 +465,34 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Level_paren___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes(")", 1);
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__7;
x_2 = l_Lean_Parser_withoutPosition(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__8;
x_2 = l_Lean_Parser_symbol(x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string_from_bytes(")", 1);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___closed__7;
x_2 = l_Lean_Parser_Level_paren___closed__9;
x_3 = l_Lean_Parser_andthen(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__9;
x_2 = l_Lean_Parser_symbol(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___closed__6;
x_1 = l_Lean_Parser_Level_paren___closed__8;
x_2 = l_Lean_Parser_Level_paren___closed__10;
x_3 = l_Lean_Parser_andthen(x_1, x_2);
return x_3;
@ -496,20 +501,30 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Level_paren___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_paren___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Level_paren___closed__11;
x_4 = l_Lean_Parser_leadingNode(x_1, x_2, x_3);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___closed__6;
x_2 = l_Lean_Parser_Level_paren___closed__11;
x_3 = l_Lean_Parser_andthen(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_paren___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Level_paren___closed__12;
x_4 = l_Lean_Parser_leadingNode(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___closed__4;
x_2 = l_Lean_Parser_Level_paren___closed__12;
x_2 = l_Lean_Parser_Level_paren___closed__13;
x_3 = l_Lean_Parser_withAntiquot(x_1, x_2);
return x_3;
}
@ -518,7 +533,7 @@ static lean_object* _init_l_Lean_Parser_Level_paren() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Level_paren___closed__13;
x_1 = l_Lean_Parser_Level_paren___closed__14;
return x_1;
}
}
@ -551,8 +566,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_paren_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(19u);
x_2 = lean_unsigned_to_nat(78u);
x_1 = lean_unsigned_to_nat(20u);
x_2 = lean_unsigned_to_nat(43u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -566,7 +581,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_paren_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_paren_declRange___closed__2;
x_4 = lean_unsigned_to_nat(78u);
x_4 = lean_unsigned_to_nat(43u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -694,38 +709,36 @@ return x_2;
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__8;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_levelParser_formatter___rarg), 5, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren_formatter___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_withoutPosition_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_formatter___closed__4;
x_2 = l_Lean_Parser_Level_paren_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__9;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_formatter___closed__2;
x_1 = l_Lean_Parser_Level_paren_formatter___closed__4;
x_2 = l_Lean_Parser_Level_paren_formatter___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -736,10 +749,22 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_formatter___closed__2;
x_2 = l_Lean_Parser_Level_paren_formatter___closed__6;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_formatter___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_paren___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Level_paren_formatter___closed__6;
x_3 = l_Lean_Parser_Level_paren_formatter___closed__7;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -752,7 +777,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Level_paren_formatter___closed__1;
x_7 = l_Lean_Parser_Level_paren_formatter___closed__7;
x_7 = l_Lean_Parser_Level_paren_formatter___closed__8;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -857,8 +882,8 @@ static lean_object* _init_l_Lean_Parser_Level_paren_parenthesizer___closed__4()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__8;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_parenthesizer), 6, 1);
x_1 = l_Lean_Parser_Level_paren_parenthesizer___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_withoutPosition_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -866,20 +891,18 @@ return x_2;
static lean_object* _init_l_Lean_Parser_Level_paren_parenthesizer___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Level_paren_parenthesizer___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Level_paren___closed__9;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_parenthesizer___closed__2;
x_1 = l_Lean_Parser_Level_paren_parenthesizer___closed__4;
x_2 = l_Lean_Parser_Level_paren_parenthesizer___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -890,10 +913,22 @@ return x_3;
static lean_object* _init_l_Lean_Parser_Level_paren_parenthesizer___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren_parenthesizer___closed__2;
x_2 = l_Lean_Parser_Level_paren_parenthesizer___closed__6;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren_parenthesizer___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_paren___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Level_paren_parenthesizer___closed__6;
x_3 = l_Lean_Parser_Level_paren_parenthesizer___closed__7;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -906,7 +941,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Level_paren_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Level_paren_parenthesizer___closed__7;
x_7 = l_Lean_Parser_Level_paren_parenthesizer___closed__8;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -1087,7 +1122,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_max_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(20u);
x_1 = lean_unsigned_to_nat(21u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1099,8 +1134,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_max_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(20u);
x_2 = lean_unsigned_to_nat(124u);
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(73u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1114,7 +1149,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_max_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_max_declRange___closed__2;
x_4 = lean_unsigned_to_nat(124u);
x_4 = lean_unsigned_to_nat(73u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1127,7 +1162,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_max_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(20u);
x_1 = lean_unsigned_to_nat(21u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1139,7 +1174,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_max_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(20u);
x_1 = lean_unsigned_to_nat(21u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1229,7 +1264,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_max_formatter___closed__3;
x_2 = l_Lean_Parser_Level_paren_formatter___closed__4;
x_2 = l_Lean_Parser_Level_paren_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1553,7 +1588,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_imax_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(23u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1565,8 +1600,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_imax_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_2 = lean_unsigned_to_nat(124u);
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(73u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1580,7 +1615,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_imax_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_imax_declRange___closed__2;
x_4 = lean_unsigned_to_nat(124u);
x_4 = lean_unsigned_to_nat(73u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1593,7 +1628,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_imax_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(23u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1605,7 +1640,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_imax_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(23u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1946,7 +1981,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_hole_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(22u);
x_1 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1958,8 +1993,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_hole_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(56u);
x_1 = lean_unsigned_to_nat(26u);
x_2 = lean_unsigned_to_nat(5u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1973,7 +2008,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_hole_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_hole_declRange___closed__2;
x_4 = lean_unsigned_to_nat(56u);
x_4 = lean_unsigned_to_nat(5u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1986,7 +2021,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_hole_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(22u);
x_1 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1998,7 +2033,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_hole_declRange___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(22u);
x_1 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2278,7 +2313,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_num_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(27u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2290,8 +2325,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_num_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_2 = lean_unsigned_to_nat(65u);
x_1 = lean_unsigned_to_nat(28u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2305,7 +2340,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_num_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_num_declRange___closed__2;
x_4 = lean_unsigned_to_nat(65u);
x_4 = lean_unsigned_to_nat(29u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -2318,7 +2353,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_num_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(27u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2330,7 +2365,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_num_declRange___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(27u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2484,20 +2519,21 @@ return x_7;
static lean_object* _init_l___regBuiltin_Lean_Parser_Level_ident_declRange___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(29u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Level_ident_declRange___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(71u);
x_1 = lean_unsigned_to_nat(30u);
x_2 = lean_unsigned_to_nat(35u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2511,7 +2547,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_ident_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_ident_declRange___closed__2;
x_4 = lean_unsigned_to_nat(71u);
x_4 = lean_unsigned_to_nat(35u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -2524,7 +2560,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_ident_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(24u);
x_1 = lean_unsigned_to_nat(29u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2536,7 +2572,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_ident_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(24u);
x_1 = lean_unsigned_to_nat(29u);
x_2 = lean_unsigned_to_nat(33u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2702,7 +2738,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_addLit_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(25u);
x_1 = lean_unsigned_to_nat(31u);
x_2 = lean_unsigned_to_nat(24u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2714,8 +2750,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_addLit_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(25u);
x_2 = lean_unsigned_to_nat(72u);
x_1 = lean_unsigned_to_nat(32u);
x_2 = lean_unsigned_to_nat(17u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2729,7 +2765,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Level_addLit_declRange___closed__1;
x_2 = lean_unsigned_to_nat(24u);
x_3 = l___regBuiltin_Lean_Parser_Level_addLit_declRange___closed__2;
x_4 = lean_unsigned_to_nat(72u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -2742,7 +2778,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_addLit_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(25u);
x_1 = lean_unsigned_to_nat(31u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2754,7 +2790,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Level_addLit_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(25u);
x_1 = lean_unsigned_to_nat(31u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2992,6 +3028,8 @@ l_Lean_Parser_Level_paren___closed__12 = _init_l_Lean_Parser_Level_paren___close
lean_mark_persistent(l_Lean_Parser_Level_paren___closed__12);
l_Lean_Parser_Level_paren___closed__13 = _init_l_Lean_Parser_Level_paren___closed__13();
lean_mark_persistent(l_Lean_Parser_Level_paren___closed__13);
l_Lean_Parser_Level_paren___closed__14 = _init_l_Lean_Parser_Level_paren___closed__14();
lean_mark_persistent(l_Lean_Parser_Level_paren___closed__14);
l_Lean_Parser_Level_paren = _init_l_Lean_Parser_Level_paren();
lean_mark_persistent(l_Lean_Parser_Level_paren);
res = l___regBuiltin_Lean_Parser_Level_paren(lean_io_mk_world());
@ -3028,6 +3066,8 @@ l_Lean_Parser_Level_paren_formatter___closed__6 = _init_l_Lean_Parser_Level_pare
lean_mark_persistent(l_Lean_Parser_Level_paren_formatter___closed__6);
l_Lean_Parser_Level_paren_formatter___closed__7 = _init_l_Lean_Parser_Level_paren_formatter___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_paren_formatter___closed__7);
l_Lean_Parser_Level_paren_formatter___closed__8 = _init_l_Lean_Parser_Level_paren_formatter___closed__8();
lean_mark_persistent(l_Lean_Parser_Level_paren_formatter___closed__8);
l___regBuiltin_Lean_Parser_Level_paren_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Level_paren_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Level_paren_formatter___closed__1);
l___regBuiltin_Lean_Parser_Level_paren_formatter___closed__2 = _init_l___regBuiltin_Lean_Parser_Level_paren_formatter___closed__2();
@ -3053,6 +3093,8 @@ l_Lean_Parser_Level_paren_parenthesizer___closed__6 = _init_l_Lean_Parser_Level_
lean_mark_persistent(l_Lean_Parser_Level_paren_parenthesizer___closed__6);
l_Lean_Parser_Level_paren_parenthesizer___closed__7 = _init_l_Lean_Parser_Level_paren_parenthesizer___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_paren_parenthesizer___closed__7);
l_Lean_Parser_Level_paren_parenthesizer___closed__8 = _init_l_Lean_Parser_Level_paren_parenthesizer___closed__8();
lean_mark_persistent(l_Lean_Parser_Level_paren_parenthesizer___closed__8);
l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__1);
l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__2 = _init_l___regBuiltin_Lean_Parser_Level_paren_parenthesizer___closed__2();

770
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

62
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -729,8 +729,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_unknown_declRange___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_2 = lean_unsigned_to_nat(121u);
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -744,7 +744,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Tactic_unknown_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___regBuiltin_Lean_Parser_Tactic_unknown_declRange___closed__2;
x_4 = lean_unsigned_to_nat(121u);
x_4 = lean_unsigned_to_nat(63u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1128,7 +1128,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nestedTactic_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1140,7 +1140,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nestedTactic_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1168,7 +1168,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nestedTactic_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1180,7 +1180,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nestedTactic_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(23u);
x_1 = lean_unsigned_to_nat(24u);
x_2 = lean_unsigned_to_nat(41u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1514,7 +1514,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_match_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(41u);
x_1 = lean_unsigned_to_nat(42u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1526,8 +1526,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_match_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(41u);
x_2 = lean_unsigned_to_nat(196u);
x_1 = lean_unsigned_to_nat(45u);
x_2 = lean_unsigned_to_nat(32u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1541,7 +1541,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Tactic_match_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___regBuiltin_Lean_Parser_Tactic_match_declRange___closed__2;
x_4 = lean_unsigned_to_nat(196u);
x_4 = lean_unsigned_to_nat(32u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -1554,7 +1554,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_match_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(41u);
x_1 = lean_unsigned_to_nat(42u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1566,7 +1566,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_match_declRange___cl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(41u);
x_1 = lean_unsigned_to_nat(42u);
x_2 = lean_unsigned_to_nat(36u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2334,7 +2334,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(60u);
x_1 = lean_unsigned_to_nat(64u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2346,8 +2346,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(60u);
x_2 = lean_unsigned_to_nat(97u);
x_1 = lean_unsigned_to_nat(65u);
x_2 = lean_unsigned_to_nat(41u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2361,7 +2361,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange___closed__2;
x_4 = lean_unsigned_to_nat(97u);
x_4 = lean_unsigned_to_nat(41u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -2374,7 +2374,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(60u);
x_1 = lean_unsigned_to_nat(64u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2386,7 +2386,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_introMatch_declRange
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(60u);
x_1 = lean_unsigned_to_nat(64u);
x_2 = lean_unsigned_to_nat(39u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2738,7 +2738,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_decide_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(70u);
x_1 = lean_unsigned_to_nat(75u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2750,8 +2750,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_decide_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(70u);
x_2 = lean_unsigned_to_nat(80u);
x_1 = lean_unsigned_to_nat(76u);
x_2 = lean_unsigned_to_nat(28u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2765,7 +2765,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Tactic_decide_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___regBuiltin_Lean_Parser_Tactic_decide_declRange___closed__2;
x_4 = lean_unsigned_to_nat(80u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -2778,7 +2778,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_decide_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(70u);
x_1 = lean_unsigned_to_nat(75u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2790,7 +2790,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_decide_declRange___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(70u);
x_1 = lean_unsigned_to_nat(75u);
x_2 = lean_unsigned_to_nat(35u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -3126,7 +3126,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(85u);
x_1 = lean_unsigned_to_nat(91u);
x_2 = lean_unsigned_to_nat(25u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -3138,8 +3138,8 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(85u);
x_2 = lean_unsigned_to_nat(93u);
x_1 = lean_unsigned_to_nat(92u);
x_2 = lean_unsigned_to_nat(35u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -3153,7 +3153,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRange___closed__1;
x_2 = lean_unsigned_to_nat(25u);
x_3 = l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRange___closed__2;
x_4 = lean_unsigned_to_nat(93u);
x_4 = lean_unsigned_to_nat(35u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -3166,7 +3166,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(85u);
x_1 = lean_unsigned_to_nat(91u);
x_2 = lean_unsigned_to_nat(29u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -3178,7 +3178,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_nativeDecide_declRan
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(85u);
x_1 = lean_unsigned_to_nat(91u);
x_2 = lean_unsigned_to_nat(41u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);

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

File diff suppressed because it is too large Load diff