chore: update stage0
This commit is contained in:
Mario Carneiro
Sebastian Ullrich
parent
711532f5c6
commit
76eddb06a5
5 changed files with 1327 additions and 1191 deletions
4
stage0/src/Lean/Parser/Basic.lean
generated
4
stage0/src/Lean/Parser/Basic.lean
generated
|
|
@ -1610,7 +1610,9 @@ inductive LeadingIdentBehavior where
|
|||
The method `termParser prec` is equivalent to the method above.
|
||||
-/
|
||||
structure ParserCategory where
|
||||
tables : PrattParsingTables
|
||||
ref : Name
|
||||
kinds : SyntaxNodeKindSet := {}
|
||||
tables : PrattParsingTables := {}
|
||||
behavior : LeadingIdentBehavior
|
||||
deriving Inhabited
|
||||
|
||||
|
|
|
|||
61
stage0/src/Lean/Parser/Extension.lean
generated
61
stage0/src/Lean/Parser/Extension.lean
generated
|
|
@ -46,9 +46,9 @@ private def addParserCategoryCore (categories : ParserCategories) (catName : Nam
|
|||
|
||||
/-- All builtin parser categories are Pratt's parsers -/
|
||||
|
||||
private def addBuiltinParserCategory (catName : Name) (behavior : LeadingIdentBehavior) : IO Unit := do
|
||||
private def addBuiltinParserCategory (catName ref : Name) (behavior : LeadingIdentBehavior) : IO Unit := do
|
||||
let categories ← builtinParserCategoriesRef.get
|
||||
let categories ← IO.ofExcept $ addParserCategoryCore categories catName { tables := {}, behavior := behavior}
|
||||
let categories ← IO.ofExcept $ addParserCategoryCore categories catName { ref, behavior }
|
||||
builtinParserCategoriesRef.set categories
|
||||
|
||||
namespace ParserExtension
|
||||
|
|
@ -56,21 +56,21 @@ namespace ParserExtension
|
|||
inductive OLeanEntry where
|
||||
| token (val : Token) : OLeanEntry
|
||||
| kind (val : SyntaxNodeKind) : OLeanEntry
|
||||
| category (catName : Name) (behavior : LeadingIdentBehavior)
|
||||
| category (catName : Name) (declName : Name) (behavior : LeadingIdentBehavior)
|
||||
| parser (catName : Name) (declName : Name) (prio : Nat) : OLeanEntry
|
||||
deriving Inhabited
|
||||
|
||||
inductive Entry where
|
||||
| token (val : Token) : Entry
|
||||
| kind (val : SyntaxNodeKind) : Entry
|
||||
| category (catName : Name) (behavior : LeadingIdentBehavior)
|
||||
| category (catName : Name) (declName : Name) (behavior : LeadingIdentBehavior)
|
||||
| parser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Entry
|
||||
deriving Inhabited
|
||||
|
||||
def Entry.toOLeanEntry : Entry → OLeanEntry
|
||||
| token v => OLeanEntry.token v
|
||||
| kind v => OLeanEntry.kind v
|
||||
| category c b => OLeanEntry.category c b
|
||||
| category c d b => OLeanEntry.category c d b
|
||||
| parser c d _ _ prio => OLeanEntry.parser c d prio
|
||||
|
||||
structure State where
|
||||
|
|
@ -102,40 +102,47 @@ def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
|
|||
abbrev getCategory (categories : ParserCategories) (catName : Name) : Option ParserCategory :=
|
||||
categories.find? catName
|
||||
|
||||
def addLeadingParser (categories : ParserCategories) (catName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories :=
|
||||
def addLeadingParser (categories : ParserCategories) (catName declName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories :=
|
||||
match getCategory categories catName with
|
||||
| none =>
|
||||
throwUnknownParserCategory catName
|
||||
| some cat =>
|
||||
let kinds := cat.kinds.insert declName
|
||||
let addTokens (tks : List Token) : Except String ParserCategories :=
|
||||
let tks := tks.map fun tk => Name.mkSimple tk
|
||||
let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with leadingTable := tables.leadingTable.insert tk (p, prio) }) cat.tables
|
||||
pure $ categories.insert catName { cat with tables := tables }
|
||||
let tks := tks.map Name.mkSimple
|
||||
let tables := tks.eraseDups.foldl (init := cat.tables) fun tables tk =>
|
||||
{ tables with leadingTable := tables.leadingTable.insert tk (p, prio) }
|
||||
pure $ categories.insert catName { cat with kinds, tables }
|
||||
match p.info.firstTokens with
|
||||
| FirstTokens.tokens tks => addTokens tks
|
||||
| FirstTokens.optTokens tks => addTokens tks
|
||||
| _ =>
|
||||
let tables := { cat.tables with leadingParsers := (p, prio) :: cat.tables.leadingParsers }
|
||||
pure $ categories.insert catName { cat with tables := tables }
|
||||
pure $ categories.insert catName { cat with kinds, tables }
|
||||
|
||||
private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) (prio : Nat) : PrattParsingTables :=
|
||||
let addTokens (tks : List Token) : PrattParsingTables :=
|
||||
let tks := tks.map fun tk => Name.mkSimple tk
|
||||
tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with trailingTable := tables.trailingTable.insert tk (p, prio) }) tables
|
||||
tks.eraseDups.foldl (init := tables) fun tables tk =>
|
||||
{ tables with trailingTable := tables.trailingTable.insert tk (p, prio) }
|
||||
match p.info.firstTokens with
|
||||
| FirstTokens.tokens tks => addTokens tks
|
||||
| FirstTokens.optTokens tks => addTokens tks
|
||||
| _ => { tables with trailingParsers := (p, prio) :: tables.trailingParsers }
|
||||
|
||||
def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) (prio : Nat) : Except String ParserCategories :=
|
||||
def addTrailingParser (categories : ParserCategories) (catName declName : Name) (p : TrailingParser) (prio : Nat) : Except String ParserCategories :=
|
||||
match getCategory categories catName with
|
||||
| none => throwUnknownParserCategory catName
|
||||
| some cat => pure $ categories.insert catName { cat with tables := addTrailingParserAux cat.tables p prio }
|
||||
| some cat =>
|
||||
let kinds := cat.kinds.insert declName
|
||||
let tables := addTrailingParserAux cat.tables p prio
|
||||
pure $ categories.insert catName { cat with kinds, tables }
|
||||
|
||||
def addParser (categories : ParserCategories) (catName : Name) (_declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories :=
|
||||
def addParser (categories : ParserCategories) (catName declName : Name)
|
||||
(leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories := do
|
||||
match leading, p with
|
||||
| true, p => addLeadingParser categories catName p prio
|
||||
| false, p => addTrailingParser categories catName p prio
|
||||
| true, p => addLeadingParser categories catName declName p prio
|
||||
| false, p => addTrailingParser categories catName declName p prio
|
||||
|
||||
def addParserTokens (tokenTable : TokenTable) (info : ParserInfo) : Except String TokenTable :=
|
||||
let newTokens := info.collectTokens []
|
||||
|
|
@ -151,17 +158,17 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
|
|||
match e with
|
||||
| Entry.token tk =>
|
||||
match addTokenConfig s.tokens tk with
|
||||
| Except.ok tokens => { s with tokens := tokens }
|
||||
| Except.ok tokens => { s with tokens }
|
||||
| _ => unreachable!
|
||||
| Entry.kind k =>
|
||||
{ s with kinds := s.kinds.insert k }
|
||||
| Entry.category catName behavior =>
|
||||
| Entry.category catName ref behavior =>
|
||||
if s.categories.contains catName then s
|
||||
else { s with
|
||||
categories := s.categories.insert catName { tables := {}, behavior := behavior } }
|
||||
categories := s.categories.insert catName { ref, behavior } }
|
||||
| Entry.parser catName declName leading parser prio =>
|
||||
match addParser s.categories catName declName leading parser prio with
|
||||
| Except.ok categories => { s with categories := categories }
|
||||
| Except.ok categories => { s with categories }
|
||||
| _ => unreachable!
|
||||
|
||||
/-- Parser aliases for making `ParserDescr` extensible -/
|
||||
|
|
@ -325,9 +332,9 @@ builtin_initialize
|
|||
}
|
||||
|
||||
private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → ImportM Entry
|
||||
| token tk => return Entry.token tk
|
||||
| kind k => return Entry.kind k
|
||||
| category c l => return Entry.category c l
|
||||
| token tk => return Entry.token tk
|
||||
| kind k => return Entry.kind k
|
||||
| category c d l => return Entry.category c d l
|
||||
| parser catName declName prio => do
|
||||
let (leading, p) ← mkParserOfConstant s.categories declName
|
||||
return Entry.parser catName declName leading p prio
|
||||
|
|
@ -344,11 +351,11 @@ builtin_initialize parserExtension : ParserExtension ←
|
|||
def isParserCategory (env : Environment) (catName : Name) : Bool :=
|
||||
(parserExtension.getState env).categories.contains catName
|
||||
|
||||
def addParserCategory (env : Environment) (catName : Name) (behavior : LeadingIdentBehavior) : Except String Environment := do
|
||||
def addParserCategory (env : Environment) (catName declName : Name) (behavior : LeadingIdentBehavior) : Except String Environment := do
|
||||
if isParserCategory env catName then
|
||||
throwParserCategoryAlreadyDefined catName
|
||||
else
|
||||
return parserExtension.addEntry env <| ParserExtension.Entry.category catName behavior
|
||||
return parserExtension.addEntry env <| ParserExtension.Entry.category catName declName behavior
|
||||
|
||||
def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBehavior :=
|
||||
match getCategory (parserExtension.getState env).categories catName with
|
||||
|
|
@ -504,7 +511,7 @@ The parsing tables for builtin parsers are "stored" in the extracted source code
|
|||
-/
|
||||
def registerBuiltinParserAttribute (attrName : Name) (catName : Name)
|
||||
(behavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Unit := do
|
||||
addBuiltinParserCategory catName behavior
|
||||
addBuiltinParserCategory catName ref behavior
|
||||
registerBuiltinAttribute {
|
||||
ref := ref
|
||||
name := attrName
|
||||
|
|
@ -554,7 +561,7 @@ builtin_initialize
|
|||
|
||||
def registerParserCategory (env : Environment) (attrName catName : Name)
|
||||
(behavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Environment := do
|
||||
let env ← IO.ofExcept $ addParserCategory env catName behavior
|
||||
let env ← IO.ofExcept $ addParserCategory env catName ref behavior
|
||||
registerAttributeOfBuilder env `parserAttr ref [DataValue.ofName attrName, DataValue.ofName catName]
|
||||
|
||||
-- declare `termParser` here since it is used everywhere via antiquotations
|
||||
|
|
|
|||
100
stage0/stdlib/Lean/Parser/Basic.c
generated
100
stage0/stdlib/Lean/Parser/Basic.c
generated
|
|
@ -101,7 +101,6 @@ static lean_object* l_Lean_Parser_hexNumberFn___closed__1;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_binNumberFn___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_numberFnAux(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_manyAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_withoutInfo(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_mkAntiquotSplice(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_identEqFn___closed__1;
|
||||
|
|
@ -492,7 +491,6 @@ static lean_object* l_Lean_Parser_antiquotExpr___closed__1;
|
|||
static lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_categoryParserOfStack(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1;
|
||||
static lean_object* l_Lean_Parser_mkAntiquot___closed__20;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkLhsPrec(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkWsBefore(lean_object*);
|
||||
|
|
@ -589,6 +587,7 @@ static lean_object* l_Lean_Parser_Error_toString___closed__2;
|
|||
extern lean_object* l_Lean_instInhabitedSyntax;
|
||||
static lean_object* l_Lean_Parser_identFnAux_parse___lambda__2___closed__1;
|
||||
static lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__7___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__7___rarg___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -598,6 +597,7 @@ static lean_object* l_Lean_Parser_antiquotExpr___elambda__1___closed__2;
|
|||
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_forArgsM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_instReprLeadingIdentBehavior___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_whitespace(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_sepBy1___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_rawCh(uint32_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_trailingLoop___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -627,6 +627,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_manyAux(lean_object*, lean_object*, lean_
|
|||
size_t lean_usize_of_nat(lean_object*);
|
||||
uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
|
||||
static lean_object* l_Lean_Parser_mkAntiquot___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_pushNone___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_chFn(uint32_t, uint8_t, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_antiquotNestedExpr;
|
||||
|
|
@ -638,6 +639,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_foldArgsM___
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_reprLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_9081____boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_trailingNodeAux(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_trailingNodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_FirstTokens_instToStringFirstTokens;
|
||||
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_foldArgs___spec__1___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_Error_expectedToString___closed__1;
|
||||
|
|
@ -701,6 +703,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_hexDigitFn(lean_object*, lean_object*);
|
|||
lean_object* l_List_redLength___rarg(lean_object*);
|
||||
static lean_object* l_Lean_Parser_mkAntiquot___closed__16;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkNoImmediateColon___elambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserCategory_tables___default;
|
||||
static lean_object* l_Lean_Parser_instInhabitedParserInfo___lambda__2___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkLineEq(lean_object*);
|
||||
|
|
@ -719,7 +722,6 @@ static lean_object* l_Lean_Parser_fieldIdxFn___closed__3;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserState_keepNewError___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_trailingLoop___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_sepByNoAntiquot___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_PrattParsingTables_trailingTable___default;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserModuleContext_currNamespace___default;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserState_setError(lean_object*, lean_object*);
|
||||
|
|
@ -769,6 +771,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_withoutInfo___elambda__1(lean_object*, le
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserModuleContext_openDecls___default;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_withResultOf(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__6___rarg___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_satisfySymbolFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_symbolInfo(lean_object*);
|
||||
|
|
@ -786,7 +789,6 @@ static lean_object* l_Lean_Parser_epsilonInfo___closed__3;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_instInhabitedParser;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_pushNone___elambda__1(lean_object*);
|
||||
static lean_object* l_Lean_Parser_FirstTokens_toStr___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkLinebreakBefore___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -807,7 +809,6 @@ LEAN_EXPORT lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_checkNoWsBefore___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_withAntiquotSpliceAndSuffix(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_PrattParsingTables_trailingParsers___default;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_noFirstTokenInfo___elambda__2(lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_withoutPosition(lean_object*);
|
||||
|
|
@ -875,9 +876,8 @@ LEAN_EXPORT lean_object* l_Lean_Parser_sepByInfo___elambda__2(lean_object*, lean
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_checkColGt(lean_object*);
|
||||
static lean_object* l_Lean_Parser_symbolInfo___closed__1;
|
||||
static lean_object* l_Lean_Parser_mkAntiquot___closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566_(lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Lean_Parser_instInhabitedLeadingIdentBehavior;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t, uint8_t);
|
||||
static lean_object* l_Lean_Parser_instBEqLeadingIdentBehavior___closed__1;
|
||||
|
|
@ -967,6 +967,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_ParserState_keepPrevError(lean_object*, l
|
|||
static lean_object* l_Lean_Parser_mkAntiquot___closed__25;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkWsBefore___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_sepBy1___elambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_ParserCategory_kinds___default;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_reprLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_9081____closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_TokenCacheEntry_stopPos___default;
|
||||
|
|
@ -995,6 +996,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_leadingParserAux___lambda__1___boxed(lean
|
|||
static lean_object* l_Lean_Parser_antiquotExpr___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_OrElseOnAntiquotBehavior_noConfusion___rarg___lambda__1___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_charLitNoAntiquot;
|
||||
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1;
|
||||
lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_fieldIdxFn___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_orelseFnCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -25839,16 +25841,36 @@ x_1 = l_Lean_Parser_instReprLeadingIdentBehavior___closed__1;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_ParserCategory_kinds___default() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_instInhabitedParserInfo___lambda__2___closed__3;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_ParserCategory_tables___default() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_instInhabitedPrattParsingTables___closed__1;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_instInhabitedParserCategory___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_instInhabitedPrattParsingTables___closed__1;
|
||||
x_2 = 0;
|
||||
x_3 = lean_alloc_ctor(0, 1, 1);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
|
||||
return x_3;
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Parser_instInhabitedParserInfo___lambda__2___closed__3;
|
||||
x_3 = l_Lean_Parser_instInhabitedPrattParsingTables___closed__1;
|
||||
x_4 = 0;
|
||||
x_5 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_5, 0, x_1);
|
||||
lean_ctor_set(x_5, 1, x_2);
|
||||
lean_ctor_set(x_5, 2, x_3);
|
||||
lean_ctor_set_uint8(x_5, sizeof(void*)*3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_instInhabitedParserCategory() {
|
||||
|
|
@ -26875,7 +26897,7 @@ lean_dec(x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
|
|
@ -26883,19 +26905,19 @@ x_4 = l_Lean_Parser_whitespace(x_2, x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1() {
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1___boxed), 3, 0);
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1___boxed), 3, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; uint8_t x_4;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1;
|
||||
x_3 = lean_st_mk_ref(x_2, x_1);
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
|
|
@ -26917,17 +26939,17 @@ return x_7;
|
|||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____lambda__1(x_1, x_2, x_3);
|
||||
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____lambda__1(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1() {
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -26935,11 +26957,11 @@ x_1 = l_Lean_Parser_categoryParserFnRef;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; uint8_t x_4;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1;
|
||||
x_3 = lean_st_ref_get(x_2, x_1);
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
|
|
@ -26961,19 +26983,19 @@ return x_7;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1() {
|
||||
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1), 1, 0);
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1), 1, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1;
|
||||
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1;
|
||||
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -31314,24 +31336,28 @@ l_Lean_Parser_instReprLeadingIdentBehavior___closed__1 = _init_l_Lean_Parser_ins
|
|||
lean_mark_persistent(l_Lean_Parser_instReprLeadingIdentBehavior___closed__1);
|
||||
l_Lean_Parser_instReprLeadingIdentBehavior = _init_l_Lean_Parser_instReprLeadingIdentBehavior();
|
||||
lean_mark_persistent(l_Lean_Parser_instReprLeadingIdentBehavior);
|
||||
l_Lean_Parser_ParserCategory_kinds___default = _init_l_Lean_Parser_ParserCategory_kinds___default();
|
||||
lean_mark_persistent(l_Lean_Parser_ParserCategory_kinds___default);
|
||||
l_Lean_Parser_ParserCategory_tables___default = _init_l_Lean_Parser_ParserCategory_tables___default();
|
||||
lean_mark_persistent(l_Lean_Parser_ParserCategory_tables___default);
|
||||
l_Lean_Parser_instInhabitedParserCategory___closed__1 = _init_l_Lean_Parser_instInhabitedParserCategory___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory___closed__1);
|
||||
l_Lean_Parser_instInhabitedParserCategory = _init_l_Lean_Parser_instInhabitedParserCategory();
|
||||
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory);
|
||||
l_Lean_Parser_indexed___rarg___closed__1 = _init_l_Lean_Parser_indexed___rarg___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_indexed___rarg___closed__1);
|
||||
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509____closed__1);
|
||||
if (builtin) {res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9509_(lean_io_mk_world());
|
||||
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541____closed__1);
|
||||
if (builtin) {res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9541_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Parser_categoryParserFnRef = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Parser_categoryParserFnRef);
|
||||
lean_dec_ref(res);
|
||||
}l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____lambda__1___closed__1);
|
||||
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534____closed__1);
|
||||
if (builtin) {res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9534_(lean_io_mk_world());
|
||||
}l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____lambda__1___closed__1);
|
||||
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566____closed__1);
|
||||
if (builtin) {res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_9566_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Parser_categoryParserFnExtension = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension);
|
||||
|
|
|
|||
2343
stage0/stdlib/Lean/Parser/Extension.c
generated
2343
stage0/stdlib/Lean/Parser/Extension.c
generated
File diff suppressed because it is too large
Load diff
10
stage0/stdlib/Lean/Server/Completion.c
generated
10
stage0/stdlib/Lean/Server/Completion.c
generated
|
|
@ -21717,7 +21717,7 @@ if (lean_obj_tag(x_15) == 0)
|
|||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_16 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_tacticCompletion___lambda__1___closed__7;
|
||||
x_17 = l_panic___at___private_Lean_Server_Completion_0__Lean_Server_Completion_tacticCompletion___spec__1(x_16);
|
||||
x_18 = lean_ctor_get(x_17, 0);
|
||||
x_18 = lean_ctor_get(x_17, 2);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_17);
|
||||
x_19 = lean_ctor_get(x_18, 0);
|
||||
|
|
@ -21743,7 +21743,7 @@ if (x_26 == 0)
|
|||
{
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; lean_object* x_34;
|
||||
x_27 = lean_ctor_get(x_15, 0);
|
||||
x_28 = lean_ctor_get(x_27, 0);
|
||||
x_28 = lean_ctor_get(x_27, 2);
|
||||
lean_inc(x_28);
|
||||
lean_dec(x_27);
|
||||
x_29 = lean_ctor_get(x_28, 0);
|
||||
|
|
@ -21766,7 +21766,7 @@ lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean
|
|||
x_35 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_35);
|
||||
lean_dec(x_15);
|
||||
x_36 = lean_ctor_get(x_35, 0);
|
||||
x_36 = lean_ctor_get(x_35, 2);
|
||||
lean_inc(x_36);
|
||||
lean_dec(x_35);
|
||||
x_37 = lean_ctor_get(x_36, 0);
|
||||
|
|
@ -21811,7 +21811,7 @@ if (lean_obj_tag(x_52) == 0)
|
|||
lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; uint8_t x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
x_53 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_tacticCompletion___lambda__1___closed__7;
|
||||
x_54 = l_panic___at___private_Lean_Server_Completion_0__Lean_Server_Completion_tacticCompletion___spec__1(x_53);
|
||||
x_55 = lean_ctor_get(x_54, 0);
|
||||
x_55 = lean_ctor_get(x_54, 2);
|
||||
lean_inc(x_55);
|
||||
lean_dec(x_54);
|
||||
x_56 = lean_ctor_get(x_55, 0);
|
||||
|
|
@ -21843,7 +21843,7 @@ if (lean_is_exclusive(x_52)) {
|
|||
lean_dec_ref(x_52);
|
||||
x_65 = lean_box(0);
|
||||
}
|
||||
x_66 = lean_ctor_get(x_64, 0);
|
||||
x_66 = lean_ctor_get(x_64, 2);
|
||||
lean_inc(x_66);
|
||||
lean_dec(x_64);
|
||||
x_67 = lean_ctor_get(x_66, 0);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue