chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
9a349a913a
commit
2fbf3cff15
12 changed files with 2743 additions and 2142 deletions
|
|
@ -50,7 +50,7 @@ private partial def insertAux (s : String) (val : α) : Trie α → String.Pos
|
|||
def insert (t : Trie α) (s : String) (val : α) : Trie α :=
|
||||
insertAux s val t 0
|
||||
|
||||
private partial def findAux (s : String) : Trie α → String.Pos → Option α
|
||||
private partial def findAux? (s : String) : Trie α → String.Pos → Option α
|
||||
| Trie.Node val m, i =>
|
||||
match s.atEnd i with
|
||||
| true => val
|
||||
|
|
@ -59,10 +59,10 @@ private partial def findAux (s : String) : Trie α → String.Pos → Option α
|
|||
let i := s.next i;
|
||||
match RBNode.find Char.lt m c with
|
||||
| none => none
|
||||
| some t => findAux t i
|
||||
| some t => findAux? t i
|
||||
|
||||
def find (t : Trie α) (s : String) : Option α :=
|
||||
findAux s t 0
|
||||
def find? (t : Trie α) (s : String) : Option α :=
|
||||
findAux? s t 0
|
||||
|
||||
private def updtAcc (v : Option α) (i : String.Pos) (acc : String.Pos × Option α) : String.Pos × Option α :=
|
||||
match v, acc with
|
||||
|
|
|
|||
|
|
@ -604,14 +604,6 @@ fun stx expectedType? => match_syntax stx with
|
|||
but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/
|
||||
@[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom
|
||||
|
||||
@[builtinTermElab sortApp] def elabSortApp : TermElab :=
|
||||
fun stx _ => do
|
||||
u ← elabLevel (stx.getArg 1);
|
||||
if (stx.getArg 0).getKind == `Lean.Parser.Term.sort then do
|
||||
pure $ mkSort u
|
||||
else
|
||||
pure $ mkSort (mkLevelSucc u)
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab.app;
|
||||
pure ()
|
||||
|
|
|
|||
|
|
@ -102,8 +102,13 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
|
|||
if ctx.leadingIdentAsSymbol && rbp?.isNone then
|
||||
`(ParserDescr.nonReservedSymbol $(quote atom) false)
|
||||
else
|
||||
-- TODO: fix (quote rbp?)
|
||||
`(ParserDescr.symbol $(quote atom) $(quote rbp?))
|
||||
match rbp? with
|
||||
| some rbp => `(ParserDescr.symbol $(quote atom) $(quote rbp))
|
||||
| none => do
|
||||
env ← liftM getEnv;
|
||||
match Parser.getTokenLbp? env atom with
|
||||
| some lbp => `(ParserDescr.symbol $(quote atom) $(quote lbp))
|
||||
| none => `(ParserDescr.symbol $(quote atom) 0)
|
||||
| none => liftM throwUnsupportedSyntax
|
||||
else if kind == `Lean.Parser.Syntax.num then
|
||||
`(ParserDescr.numLit)
|
||||
|
|
|
|||
|
|
@ -3,6 +3,59 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
|
||||
/-!
|
||||
# Basic Lean parser infrastructure
|
||||
|
||||
The Lean parser was developed with the following primary goals in mind:
|
||||
|
||||
* flexibility: Lean's grammar is complex and includes indentation and other whitespace sensitivity. It should be
|
||||
possible to introduce such custom "tweaks" locally without having to adjust the fundamental parsing approach.
|
||||
* extensibility: Lean's grammar can be extended on the fly within a Lean file, and with Lean 4 we want to extend this
|
||||
to cover embedding domain-specific languages that may look nothing like Lean, down to using a separate set of tokens.
|
||||
* losslessness: The parser should produce a concrete syntax tree that preserves all whitespace and other "sub-token"
|
||||
information for the use in tooling.
|
||||
* performance: The overhead of the parser building blocks, and the overall parser performance on average-complexity
|
||||
input, should be comparable with that of the previous parser hand-written in C++. No fancy optimizations should be
|
||||
necessary for this.
|
||||
|
||||
Given these constraints, we decided to implement a combinatoric, non-monadic, lexer-less, memoizing recursive-descent
|
||||
parser. Using combinators instead of some more formal and introspectible grammar representation ensures ultimate
|
||||
flexibility as well as efficient extensibility: there is (almost) no pre-processing necessary when extending the grammar
|
||||
with a new parser. However, because the all results the combinators produce are of the homogeneous `Syntax` type, the
|
||||
basic parser type is not actually a monad but a monomorphic linear function `ParserState → ParserState`, avoiding
|
||||
constructing and deconstructing countless monadic return values. Instead of explicitly returning syntax objects, parsers
|
||||
push (zero or more of) them onto a syntax stack inside the linear state. Chaining parsers via `>>` accumulates their
|
||||
output on the stack. Combinators such as `node` then pop off all syntax objects produced during their invocation and
|
||||
wrap them in a single `Syntax.node` object that is again pushed on this stack. Instead of calling `node` directly, we
|
||||
usually use the macro `parser! p`, which unfolds to `node k p` where the new syntax node kind `k` is the name of the
|
||||
declaration being defined.
|
||||
We remark the design is inspired by the "Arrow"-approach described at the paper "Generalizing Monads to Arrows", and
|
||||
used at the Swierstra and Duponcheel's parsing library (SDPL). As in SDPL, a parser is a combination of static information
|
||||
(`ParserInfo`) which is computed before parsing begins, and the parsing function `ParserState → ParserState`.
|
||||
|
||||
The lack of a dedicated lexer ensures we can modify and replace the lexical grammar at any point, and simplifies
|
||||
detecting and propagating whitespace. The parser still has a concept of "tokens", however, and caches the most recent
|
||||
one for performance: when `tokenFn` is called twice at the same position in the input, it will reuse the result of the
|
||||
first call. `tokenFn` recognizes some built-in variable-length tokens such as identifiers as well as any fixed token in
|
||||
the `ParserContext`'s `TokenTable` (a trie); however, the same cache field and strategy could be reused by custom token
|
||||
parsers. Tokens also play a central role in the `prattParser` combinator, which selects a *leading* parser followed by
|
||||
zero or more *trailing* parsers based on the current token (via `peekToken`) and its associated precedence; see the
|
||||
documentation of `prattParser` for more details. Token precedences are specified via the `symbol` parser, or with
|
||||
`symbolNoWs` for tokens that should not be preceded by whitespace. The `Parser` type is extended with additional
|
||||
metadata over the mere parsing function to propagate token information: `collectTokens` collects all tokens within a
|
||||
parser for registering. `firstTokens` holds information about the "FIRST" token set used to speed up parser selection in
|
||||
`prattParser`. If multiple parsers accept the same current token, `prattParser` tries all of them using the backtracking
|
||||
`longestMatchFn` combinator. This is the only case where standard parsers might execute arbitrary backtracking. At the
|
||||
moment there is no memoization shared by these parallel parsers apart from the first token, though we might change this
|
||||
in the future if the need arises.
|
||||
|
||||
Finally, error reporting follows the standard combinatoric approach of collecting a single unexpected token/... and zero
|
||||
or more expected tokens (see `Error` below). Expected tokens are e.g. set by `symbol` and merged by `<|>`. Combinators
|
||||
running multiple parsers should check if an error message is set in the parser state (`hasError`) and act accordingly.
|
||||
Error recovery is left to the designer of the specific language; for example, Lean's top-level `parseCommand` loop skips
|
||||
tokens until the next command keyword on error.
|
||||
-/
|
||||
prelude
|
||||
import Lean.Data.Trie
|
||||
import Lean.Data.Position
|
||||
|
|
@ -1053,15 +1106,19 @@ let asciiSym := asciiSym.trim;
|
|||
{ info := unicodeSymbolInfo sym asciiSym lbp,
|
||||
fn := unicodeSymbolFn sym asciiSym }
|
||||
|
||||
/- Succeeds if RBP > lower -/
|
||||
def checkRBPGreaterFn (lower : Nat) (errorMsg : String) : ParserFn :=
|
||||
/- Succeeds if RBP < upper -/
|
||||
def checkRbpLtFn (upper : Nat) (errorMsg : String) : ParserFn :=
|
||||
fun c s =>
|
||||
if c.rbp > lower then s.mkUnexpectedError errorMsg
|
||||
else s
|
||||
if c.rbp < upper then s
|
||||
else s.mkUnexpectedError errorMsg
|
||||
|
||||
def checkRBPGreater (lower : Nat) (errorMsg : String) : Parser :=
|
||||
def checkRbpLt (lower : Nat) (errorMsg : String := "unexpected RBP") : Parser :=
|
||||
{ info := epsilonInfo,
|
||||
fn := checkRBPGreaterFn lower errorMsg }
|
||||
fn := checkRbpLtFn lower errorMsg }
|
||||
|
||||
/- Succeeds if RBP <= upper -/
|
||||
def checkRbpLe (upper : Nat) (errorMsg : String := "unexpected RBP") : Parser :=
|
||||
checkRbpLt (upper + 1) errorMsg
|
||||
|
||||
def mkAtomicInfo (k : String) : ParserInfo :=
|
||||
{ firstTokens := FirstTokens.tokens [ { val := k } ] }
|
||||
|
|
@ -1548,7 +1605,22 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par
|
|||
trailingLoop s
|
||||
|
||||
/--
|
||||
Implements a recursive precedence parser according to Pratt's algorithm.
|
||||
|
||||
Implements a recursive precedence parser according to Pratt's algorithm: select a parser (or more, via
|
||||
`longestMatchFn`) from `leadingTable` based on the current token (falling back to unindexed `leadingParsers` such as
|
||||
application), then chain with parsers from `trailingTable`/`trailingParsers` as long as the precedence of the current
|
||||
token is higher than `rbp` of the parser state.
|
||||
|
||||
As an extension of the original algorithm, we also check the current token's precedence before calling the leading
|
||||
parser(s). We do this so we can define an n-ary application parser:
|
||||
```
|
||||
@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec)
|
||||
```
|
||||
If the nested `termParser appPrec` did not check the precedence of the first token, we would accept bogus input such as
|
||||
`f x fun y => y` because we would never check the precedence of `fun`. Note that, in contrast to trailing tokens, a
|
||||
leading token is accepted if its precedence is *at least* `rbp`. This is necessary so that `f x y` is not parsed as
|
||||
`f (x y)`: the nested `termParser` call must accept the leading token `x` but not the trailing token `y`. But both have
|
||||
the same precedence as identifiers, so we must use different comparisons.
|
||||
|
||||
`antiquotParser` should be a `mkAntiquot` parser (or always fail) and is tried before all other parsers.
|
||||
It should not be added to the regular leading parsers because it would heavily
|
||||
|
|
@ -1627,7 +1699,7 @@ private def mergePrecendences (msgPreamble : String) (sym : String) : Option Nat
|
|||
|
||||
private def addTokenConfig (tokens : TokenTable) (tk : TokenConfig) : Except String TokenTable := do
|
||||
if tk.val == "" then throw "invalid empty symbol"
|
||||
else match tokens.find tk.val with
|
||||
else match tokens.find? tk.val with
|
||||
| none => pure $ tokens.insert tk.val tk
|
||||
| some oldTk => do
|
||||
lbp ← mergePrecendences "" tk.val oldTk.lbp tk.lbp;
|
||||
|
|
@ -1855,6 +1927,11 @@ kinds.foldl (fun ks k _ => k::ks) []
|
|||
def getTokenTable (env : Environment) : TokenTable :=
|
||||
(parserExtension.getState env).tokens
|
||||
|
||||
def getTokenLbp? (env : Environment) (sym : String) : Option Nat := do
|
||||
let tokens := getTokenTable env;
|
||||
tk ← tokens.find? sym;
|
||||
tk.lbp
|
||||
|
||||
def mkInputContext (input : String) (fileName : String) : InputContext :=
|
||||
{ input := input,
|
||||
fileName := fileName,
|
||||
|
|
|
|||
|
|
@ -52,8 +52,8 @@ def namedPattern := checkNoWsBefore "no space before '@'" >> parser! symbol "@"
|
|||
@[builtinTermParser] def num : Parser := parser! numLit
|
||||
@[builtinTermParser] def str : Parser := parser! strLit
|
||||
@[builtinTermParser] def char : Parser := parser! charLit
|
||||
@[builtinTermParser] def type := parser! symbol "Type" appPrec
|
||||
@[builtinTermParser] def sort := parser! symbol "Sort" appPrec
|
||||
@[builtinTermParser] def type := parser! symbol "Type" appPrec >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def sort := parser! symbol "Sort" appPrec >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def prop := parser! symbol "Prop" appPrec
|
||||
@[builtinTermParser] def hole := parser! symbol "_" appPrec
|
||||
@[builtinTermParser] def namedHole := parser! symbol "?" appPrec >> ident
|
||||
|
|
@ -91,7 +91,7 @@ def explicitBinder (requireType := false) := parser! symbol "(" appPrec >> many1
|
|||
def implicitBinder (requireType := false) := parser! symbol "{" appPrec >> many1 binderIdent >> binderType requireType >> "}"
|
||||
def instBinder := parser! symbol "[" appPrec >> optIdent >> termParser >> "]"
|
||||
def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
|
||||
@[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkRBPGreater 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
|
||||
@[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkRbpLe 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
|
||||
def simpleBinder := parser! many1 binderIdent
|
||||
@[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" leadPrec >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
|
||||
|
||||
|
|
@ -149,7 +149,6 @@ def namedArgument := parser! try (symbol "(" appPrec >> ident >> " := ") >> ter
|
|||
@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec)
|
||||
|
||||
def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort)
|
||||
@[builtinTermParser] def sortApp := tparser! checkIsSort >> levelParser appPrec
|
||||
@[builtinTermParser] def proj := tparser! symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
|
||||
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
|
||||
@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" (appPrec+1) >> termParser >>"]"
|
||||
|
|
|
|||
|
|
@ -14,10 +14,12 @@
|
|||
extern "C" {
|
||||
#endif
|
||||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__5(lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1(lean_object*);
|
||||
uint8_t l_RBNode_isRed___rarg(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_4__updtAcc(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_6__toStringAux___main___rarg(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__4(lean_object*);
|
||||
lean_object* l_RBNode_fold___main___at___private_Lean_Data_Trie_6__toStringAux___main___spec__2___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
|
||||
|
|
@ -25,40 +27,38 @@ lean_object* l_Lean_Parser_Trie_HasEmptyc(lean_object*);
|
|||
lean_object* l_Lean_Parser_Trie_HasToString___rarg(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__7___rarg(lean_object*, uint32_t, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_matchPrefix___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f(lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_empty(lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg(lean_object*, uint32_t);
|
||||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__5___rarg(lean_object*, uint32_t, lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__7(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_string_append(lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__3___rarg(lean_object*, uint32_t, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_6__toStringAux___rarg(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_find___rarg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux___main(lean_object*);
|
||||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_5__matchPrefixAux___main___spec__1___rarg(lean_object*, uint32_t);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_matchPrefix___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_HasEmptyc___closed__1;
|
||||
lean_object* l___private_Lean_Data_Trie_4__updtAcc___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_2__insertAux___main(lean_object*);
|
||||
lean_object* l_Lean_Format_joinSep___main___at___private_Lean_Data_Trie_6__toStringAux___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_UInt32_decLt(uint32_t, uint32_t);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__3(lean_object*);
|
||||
extern lean_object* l_Char_HasRepr___closed__1;
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_insert___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux___main(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_matchPrefix(lean_object*);
|
||||
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Options_empty;
|
||||
lean_object* l_Lean_Parser_Trie_find___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_find(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_2__insertAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__2___rarg(lean_object*, uint32_t, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_HasToString(lean_object*);
|
||||
|
|
@ -66,8 +66,8 @@ lean_object* l_Lean_Parser_Trie_Inhabited(lean_object*);
|
|||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__2(lean_object*);
|
||||
lean_object* l_RBNode_fold___main___at___private_Lean_Data_Trie_6__toStringAux___main___spec__2(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_2__insertAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_insert___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__6(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__6___rarg(lean_object*, uint32_t, lean_object*);
|
||||
|
|
@ -76,7 +76,6 @@ lean_object* l___private_Lean_Data_Trie_2__insertAux___rarg(lean_object*, lean_o
|
|||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_5__matchPrefixAux___main___spec__1___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_4__updtAcc___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_format_group(lean_object*);
|
||||
|
|
@ -84,11 +83,12 @@ lean_object* l_RBNode_setBlack___rarg(lean_object*);
|
|||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__1___rarg(lean_object*, uint32_t);
|
||||
lean_object* l_Lean_Parser_Trie_empty___closed__1;
|
||||
lean_object* l___private_Lean_Data_Trie_2__insertAux(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_2__insertAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_1__insertEmptyAux(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__1(lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg(lean_object*, uint32_t);
|
||||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Format_joinSep___main___at___private_Lean_Data_Trie_6__toStringAux___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_6__toStringAux(lean_object*);
|
||||
|
|
@ -98,10 +98,10 @@ uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
|
|||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux(lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_5__matchPrefixAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_insert___at___private_Lean_Data_Trie_2__insertAux___main___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_6__toStringAux___main(lean_object*);
|
||||
lean_object* l_Lean_Parser_Trie_insert(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at___private_Lean_Data_Trie_2__insertAux___main___spec__4___rarg(lean_object*, uint32_t, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_singleton___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_5__matchPrefixAux___main___spec__1(lean_object*);
|
||||
lean_object* _init_l_Lean_Parser_Trie_empty___closed__1() {
|
||||
|
|
@ -10223,7 +10223,7 @@ lean_dec(x_2);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg(lean_object* x_1, uint32_t x_2) {
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg(lean_object* x_1, uint32_t x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 0)
|
||||
|
|
@ -10279,15 +10279,15 @@ goto _start;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1(lean_object* x_1) {
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; uint8_t x_6;
|
||||
|
|
@ -10304,7 +10304,7 @@ lean_dec(x_4);
|
|||
x_7 = lean_string_utf8_get(x_1, x_3);
|
||||
x_8 = lean_string_utf8_next(x_1, x_3);
|
||||
lean_dec(x_3);
|
||||
x_9 = l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg(x_5, x_7);
|
||||
x_9 = l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg(x_5, x_7);
|
||||
if (lean_obj_tag(x_9) == 0)
|
||||
{
|
||||
lean_object* x_10;
|
||||
|
|
@ -10331,80 +10331,80 @@ return x_4;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main(lean_object* x_1) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Trie_3__findAux___main___rarg___boxed), 3, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint32_t x_3; lean_object* x_4;
|
||||
x_3 = lean_unbox_uint32(x_2);
|
||||
lean_dec(x_2);
|
||||
x_4 = l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux___main___spec__1___rarg(x_1, x_3);
|
||||
x_4 = l_RBNode_find___main___at___private_Lean_Data_Trie_3__findAux_x3f___main___spec__1___rarg(x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux___main___rarg(x_1, x_2, x_3);
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux___main___rarg(x_1, x_2, x_3);
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux(lean_object* x_1) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Trie_3__findAux___rarg___boxed), 3, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Trie_3__findAux_x3f___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux___rarg(x_1, x_2, x_3);
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux_x3f___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Trie_find___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4;
|
||||
x_3 = lean_unsigned_to_nat(0u);
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux___main___rarg(x_2, x_1, x_3);
|
||||
x_4 = l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(x_2, x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Trie_find(lean_object* x_1) {
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_Trie_find___rarg___boxed), 2, 0);
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_Trie_find_x3f___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Trie_find___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_Lean_Parser_Trie_find_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_Trie_find___rarg(x_1, x_2);
|
||||
x_3 = l_Lean_Parser_Trie_find_x3f___rarg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -226,6 +226,7 @@ uint8_t l_Lean_Elab_Term_blockImplicitLambda(lean_object*);
|
|||
lean_object* l_Lean_Delaborator_delabOfNat___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_Delaborator_delabLit(lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabAttribute___closed__2;
|
||||
lean_object* l_Lean_Delaborator_delabSort___closed__14;
|
||||
lean_object* l_Lean_Delaborator_mkDelabAttribute___lambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabForall___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabAppImplicit___closed__5;
|
||||
|
|
@ -241,6 +242,7 @@ lean_object* l_Lean_Delaborator_delabFor___main(lean_object*, lean_object*, lean
|
|||
extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Syntax_getId(lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabProjectionApp___closed__3;
|
||||
lean_object* l_Lean_Delaborator_delabSort___closed__15;
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_Delaborator_delabForall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_withAppFnArgs(lean_object*);
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
|
|
@ -260,6 +262,7 @@ lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lea
|
|||
extern lean_object* l_Lean_numLitKind___closed__2;
|
||||
lean_object* l_Lean_Level_getOffsetAux___main(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_evalNat___main___closed__6;
|
||||
extern lean_object* l_Lean_mkAppStx___closed__6;
|
||||
lean_object* l_Lean_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_ReaderT_failure___at_Lean_Delaborator_DelabM_inhabited___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
|
||||
|
|
@ -484,7 +487,6 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabForall(lean_object*);
|
|||
lean_object* l_Array_anyRangeMAux___main___at_Lean_Delaborator_hasIdent___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_getExprKind___closed__29;
|
||||
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
|
||||
extern lean_object* l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Delaborator_getExprKind___closed__25;
|
||||
lean_object* l_Array_anyRangeMAux___main___at_Lean_Delaborator_delabForall___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_quote___main___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -8197,22 +8199,18 @@ return x_5;
|
|||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__5;
|
||||
x_3 = lean_alloc_ctor(2, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("sortApp");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_1 = l_Lean_mkAppStx___closed__6;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__1;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -8220,9 +8218,9 @@ lean_object* _init_l_Lean_Delaborator_delabSort___closed__3() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__5;
|
||||
x_3 = lean_alloc_ctor(2, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -8242,9 +8240,9 @@ lean_object* _init_l_Lean_Delaborator_delabSort___closed__5() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_prop___elambda__1___closed__5;
|
||||
x_3 = lean_alloc_ctor(2, 2, 0);
|
||||
x_1 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__4;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -8264,9 +8262,9 @@ lean_object* _init_l_Lean_Delaborator_delabSort___closed__7() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_prop___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__6;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_prop___elambda__1___closed__5;
|
||||
x_3 = lean_alloc_ctor(2, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -8275,14 +8273,36 @@ return x_3;
|
|||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__7;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_prop___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__8;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__10() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Delaborator_delabSort___closed__7;
|
||||
x_1 = l_Lean_Delaborator_delabSort___closed__9;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__9() {
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__11() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -8294,44 +8314,44 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__10() {
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__12() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__9;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__11;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__11() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_type___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__10;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__12() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Delaborator_delabSort___closed__11;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__13() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_type___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__12;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__14() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabSort___closed__15() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__11;
|
||||
x_2 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -8377,7 +8397,7 @@ lean_object* x_20; lean_object* x_21;
|
|||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_7);
|
||||
x_20 = l_Lean_Delaborator_delabSort___closed__8;
|
||||
x_20 = l_Lean_Delaborator_delabSort___closed__10;
|
||||
x_21 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_20);
|
||||
lean_ctor_set(x_21, 1, x_8);
|
||||
|
|
@ -8395,7 +8415,7 @@ lean_dec(x_22);
|
|||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_7);
|
||||
x_23 = l_Lean_Delaborator_delabSort___closed__12;
|
||||
x_23 = l_Lean_Delaborator_delabSort___closed__14;
|
||||
x_24 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_24, 0, x_23);
|
||||
lean_ctor_set(x_24, 1, x_8);
|
||||
|
|
@ -8425,9 +8445,9 @@ if (x_27 == 0)
|
|||
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
|
||||
x_28 = lean_ctor_get(x_25, 0);
|
||||
x_29 = l_Lean_Level_quote___main(x_28);
|
||||
x_30 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_30 = l_Lean_Delaborator_delabSort___closed__15;
|
||||
x_31 = lean_array_push(x_30, x_29);
|
||||
x_32 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_32 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_33 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_33, 0, x_32);
|
||||
lean_ctor_set(x_33, 1, x_31);
|
||||
|
|
@ -8444,9 +8464,9 @@ x_35 = lean_ctor_get(x_25, 0);
|
|||
lean_inc(x_35);
|
||||
lean_dec(x_25);
|
||||
x_36 = l_Lean_Level_quote___main(x_35);
|
||||
x_37 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_37 = l_Lean_Delaborator_delabSort___closed__15;
|
||||
x_38 = lean_array_push(x_37, x_36);
|
||||
x_39 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_39 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_40 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_40, 0, x_39);
|
||||
lean_ctor_set(x_40, 1, x_38);
|
||||
|
|
@ -8483,9 +8503,9 @@ if (x_45 == 0)
|
|||
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
|
||||
x_46 = lean_ctor_get(x_43, 0);
|
||||
x_47 = l_Lean_Level_quote___main(x_46);
|
||||
x_48 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_48 = l_Lean_Delaborator_delabSort___closed__15;
|
||||
x_49 = lean_array_push(x_48, x_47);
|
||||
x_50 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_50 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_51 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_51, 0, x_50);
|
||||
lean_ctor_set(x_51, 1, x_49);
|
||||
|
|
@ -8502,9 +8522,9 @@ x_53 = lean_ctor_get(x_43, 0);
|
|||
lean_inc(x_53);
|
||||
lean_dec(x_43);
|
||||
x_54 = l_Lean_Level_quote___main(x_53);
|
||||
x_55 = l_Lean_Delaborator_delabSort___closed__13;
|
||||
x_55 = l_Lean_Delaborator_delabSort___closed__15;
|
||||
x_56 = lean_array_push(x_55, x_54);
|
||||
x_57 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_57 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_58 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_58, 0, x_57);
|
||||
lean_ctor_set(x_58, 1, x_56);
|
||||
|
|
@ -8523,9 +8543,9 @@ block_19:
|
|||
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
|
||||
lean_dec(x_11);
|
||||
x_12 = l_Lean_Level_quote___main(x_10);
|
||||
x_13 = l_Lean_Delaborator_delabSort___closed__4;
|
||||
x_13 = l_Lean_Delaborator_delabSort___closed__6;
|
||||
x_14 = lean_array_push(x_13, x_12);
|
||||
x_15 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_15 = l_Lean_Delaborator_delabSort___closed__2;
|
||||
x_16 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_16, 0, x_15);
|
||||
lean_ctor_set(x_16, 1, x_14);
|
||||
|
|
@ -18861,6 +18881,10 @@ l_Lean_Delaborator_delabSort___closed__12 = _init_l_Lean_Delaborator_delabSort__
|
|||
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__12);
|
||||
l_Lean_Delaborator_delabSort___closed__13 = _init_l_Lean_Delaborator_delabSort___closed__13();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__13);
|
||||
l_Lean_Delaborator_delabSort___closed__14 = _init_l_Lean_Delaborator_delabSort___closed__14();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__14);
|
||||
l_Lean_Delaborator_delabSort___closed__15 = _init_l_Lean_Delaborator_delabSort___closed__15();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__15);
|
||||
l___regBuiltin_Lean_Delaborator_delabSort___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabSort___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSort___closed__1);
|
||||
res = l___regBuiltin_Lean_Delaborator_delabSort(lean_io_mk_world());
|
||||
|
|
|
|||
|
|
@ -17,7 +17,6 @@ lean_object* l_Lean_Elab_Term_addNamedArg___closed__5;
|
|||
lean_object* l_Lean_Elab_Term_getEnv___rarg(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_7__hasOnlyTypeMVar___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_18__elabAppLValsAux___main___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabSortApp(lean_object*);
|
||||
extern lean_object* l_Lean_fieldIdxKind;
|
||||
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
|
||||
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
|
||||
|
|
@ -109,9 +108,7 @@ lean_object* l___private_Lean_Elab_App_18__elabAppLValsAux___main___closed__1;
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_elabId(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_addNamedArg___closed__6;
|
||||
lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__2;
|
||||
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1;
|
||||
lean_object* l___private_Lean_Elab_App_21__elabAppFn___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabArrayRef(lean_object*);
|
||||
|
|
@ -277,13 +274,10 @@ uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_addNamedArg___spec__1(le
|
|||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
extern lean_object* l_Lean_mkAppStx___closed__5;
|
||||
uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
|
||||
lean_object* l_Lean_Elab_Term_elabSortApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_10__elabAppArgsAux___main___closed__1;
|
||||
lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__16;
|
||||
lean_object* l___private_Lean_Elab_App_10__elabAppArgsAux___main___closed__2;
|
||||
lean_object* l_Lean_mkLevelSucc(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabSortApp(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_getRevArg_x21___main(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_20__elabAppFnId___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
|
||||
|
|
@ -390,7 +384,6 @@ lean_object* l___private_Lean_Elab_App_11__elabAppArgs___boxed(lean_object*, lea
|
|||
lean_object* l_Array_insertAt___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_findField_x3f___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__12;
|
||||
extern lean_object* l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Name_components(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_App_25__elabAppAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_mkAppStx___closed__1;
|
||||
|
|
@ -17729,132 +17722,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabSortApp(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_5 = lean_unsigned_to_nat(1u);
|
||||
x_6 = l_Lean_Syntax_getArg(x_1, x_5);
|
||||
x_7 = l_Lean_Elab_Term_elabLevel(x_6, x_3, x_4);
|
||||
if (lean_obj_tag(x_7) == 0)
|
||||
{
|
||||
uint8_t x_8;
|
||||
x_8 = !lean_is_exclusive(x_7);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
|
||||
x_9 = lean_ctor_get(x_7, 0);
|
||||
x_10 = lean_unsigned_to_nat(0u);
|
||||
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
|
||||
x_12 = l_Lean_Syntax_getKind(x_11);
|
||||
x_13 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
|
||||
x_14 = lean_name_eq(x_12, x_13);
|
||||
lean_dec(x_12);
|
||||
if (x_14 == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16;
|
||||
x_15 = l_Lean_mkLevelSucc(x_9);
|
||||
x_16 = l_Lean_mkSort(x_15);
|
||||
lean_ctor_set(x_7, 0, x_16);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_17;
|
||||
x_17 = l_Lean_mkSort(x_9);
|
||||
lean_ctor_set(x_7, 0, x_17);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
|
||||
x_18 = lean_ctor_get(x_7, 0);
|
||||
x_19 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_19);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_7);
|
||||
x_20 = lean_unsigned_to_nat(0u);
|
||||
x_21 = l_Lean_Syntax_getArg(x_1, x_20);
|
||||
x_22 = l_Lean_Syntax_getKind(x_21);
|
||||
x_23 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
|
||||
x_24 = lean_name_eq(x_22, x_23);
|
||||
lean_dec(x_22);
|
||||
if (x_24 == 0)
|
||||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
x_25 = l_Lean_mkLevelSucc(x_18);
|
||||
x_26 = l_Lean_mkSort(x_25);
|
||||
x_27 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_27, 0, x_26);
|
||||
lean_ctor_set(x_27, 1, x_19);
|
||||
return x_27;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_28; lean_object* x_29;
|
||||
x_28 = l_Lean_mkSort(x_18);
|
||||
x_29 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_29, 0, x_28);
|
||||
lean_ctor_set(x_29, 1, x_19);
|
||||
return x_29;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_30;
|
||||
x_30 = !lean_is_exclusive(x_7);
|
||||
if (x_30 == 0)
|
||||
{
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_31; lean_object* x_32; lean_object* x_33;
|
||||
x_31 = lean_ctor_get(x_7, 0);
|
||||
x_32 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_32);
|
||||
lean_inc(x_31);
|
||||
lean_dec(x_7);
|
||||
x_33 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_33, 0, x_31);
|
||||
lean_ctor_set(x_33, 1, x_32);
|
||||
return x_33;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabSortApp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Elab_Term_elabSortApp(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabSortApp___boxed), 4, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabSortApp(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_2 = l_Lean_Elab_Term_termElabAttribute;
|
||||
x_3 = l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1;
|
||||
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Elab_App_27__regTraceClasses(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -18167,11 +18034,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabRawIdent___closed__1);
|
|||
res = l___regBuiltin_Lean_Elab_Term_elabRawIdent(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabSortApp___closed__1);
|
||||
res = l___regBuiltin_Lean_Elab_Term_elabSortApp(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = l___private_Lean_Elab_App_27__regTraceClasses(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -34,7 +34,6 @@ lean_object* l_IO_ofExcept___at___private_Lean_Parser_Parser_15__addBuiltinParse
|
|||
lean_object* l_Lean_Parser_symbolAux___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_hashOrelse;
|
||||
lean_object* l_RBNode_ins___main___at_Lean_Parser_TokenMap_insert___spec__7___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
size_t l_USize_add(size_t, size_t);
|
||||
lean_object* l_Lean_Parser_manyAux___main___closed__1;
|
||||
lean_object* l_Lean_Parser_numLit___elambda__1___closed__2;
|
||||
|
|
@ -135,6 +134,7 @@ lean_object* l_Lean_Parser_hexNumberFn(lean_object*, lean_object*, lean_object*)
|
|||
lean_object* l_Array_foldSepBy___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLitFnAux(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_List_elem___main___at_Lean_NameHashSet_insert___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_getTokenLbp_x3f___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_10__noImmediateColon___elambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_ParserState_next(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -162,7 +162,6 @@ lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_mkAntiquot___closed__17;
|
||||
lean_object* l_Lean_Syntax_foldSepArgsM(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_builtinParserCategoriesRef;
|
||||
lean_object* l_Lean_Parser_checkRBPGreater(lean_object*, lean_object*);
|
||||
lean_object* lean_environment_find(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_parserExtension;
|
||||
lean_object* l_Lean_Parser_unquotedSymbolFn___closed__1;
|
||||
|
|
@ -175,6 +174,7 @@ lean_object* l_Lean_Parser_parserExtension___closed__2;
|
|||
uint8_t l_Lean_Parser_isLitKind(lean_object*);
|
||||
lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_whitespace___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_22__ParserExtension_addImported___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRbpLtFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_binNumberFn___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_fieldIdxKind___closed__1;
|
||||
lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__1;
|
||||
|
|
@ -185,6 +185,7 @@ lean_object* l_Lean_Parser_TokenConfig_HasBeq___closed__1;
|
|||
lean_object* l_Lean_Parser_categoryParserOfStackFn___closed__2;
|
||||
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkColGe(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRbpLtFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l___private_Lean_Parser_Parser_4__isToken(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_25__ParserAttribute_add___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolFn(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -305,7 +306,6 @@ lean_object* l_Lean_Parser_ident___closed__1;
|
|||
lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgsM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_finishCommentBlock___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_indexed___rarg(lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
uint8_t l_Lean_Parser_takeWhileFn___lambda__1(lean_object*, uint32_t);
|
||||
uint32_t l_Lean_Parser_getNext(lean_object*, lean_object*);
|
||||
|
|
@ -352,6 +352,7 @@ lean_object* l_Lean_Syntax_forArgsM(lean_object*);
|
|||
lean_object* l_Lean_Parser_throwUnknownParserCategory(lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_6__nameLitAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_mkAntiquot___closed__15;
|
||||
lean_object* l_Lean_Parser_checkRbpLt___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_decimalNumberFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_PrattParsingTables_inhabited___closed__1;
|
||||
lean_object* l_Lean_Parser_compileParserDescr___main___closed__3;
|
||||
|
|
@ -495,7 +496,6 @@ lean_object* l_Lean_Parser_identFnAux___main(lean_object*, lean_object*, lean_ob
|
|||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_numLitKind___closed__1;
|
||||
lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_optionaInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_FirstTokens_seq(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_13__throwParserCategoryAlreadyDefined___rarg___closed__1;
|
||||
|
|
@ -598,6 +598,7 @@ lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
|
|||
lean_object* l_Lean_Parser_FirstTokens_merge(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLit___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_pushNone___elambda__1___rarg(lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRbpLe(lean_object*, lean_object*);
|
||||
lean_object* lean_eval_const(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_mkParserAttributeImpl(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_fieldIdx___closed__5;
|
||||
|
|
@ -724,6 +725,7 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkParserExtensio
|
|||
lean_object* l_Lean_Parser_mkAntiquot___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__2;
|
||||
lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRbpLe___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Array_foldSepByM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Lean_Environment_5__envExtensionsRef;
|
||||
|
|
@ -786,6 +788,7 @@ lean_object* l_Lean_Parser_mkAntiquot___closed__16;
|
|||
lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_20__updateBuiltinTokens___closed__1;
|
||||
lean_object* l_Lean_Parser_compileParserDescr___main___closed__2;
|
||||
lean_object* l_Lean_Parser_getTokenLbp_x3f(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_FirstTokens_HasToString___closed__1;
|
||||
lean_object* l_Lean_Parser_FirstTokens_HasToString;
|
||||
lean_object* l_Array_iterateMAux___main___at___private_Lean_Parser_Parser_25__ParserAttribute_add___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -844,7 +847,6 @@ lean_object* l_Lean_Parser_quotedSymbolFn___boxed(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Name_toExprAux___main(lean_object*);
|
||||
uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Parser_10__noImmediateColon___closed__2;
|
||||
lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_mkParserExtension___closed__5;
|
||||
lean_object* l_Lean_Parser_dollarSymbol___closed__3;
|
||||
lean_object* l_Lean_Parser_satisfySymbolFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -865,7 +867,7 @@ lean_object* l_Lean_Parser_epsilonInfo___closed__3;
|
|||
lean_object* l_Lean_Parser_unquotedSymbol;
|
||||
lean_object* l___private_Lean_Parser_Parser_1__expectedToString___main(lean_object*);
|
||||
lean_object* l_Lean_Parser_hashOrelse___closed__1;
|
||||
lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkRbpLt___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2___boxed(lean_object*);
|
||||
lean_object* l_Lean_Parser_many1Indent(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_whitespace___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -932,6 +934,7 @@ lean_object* l_Lean_Syntax_forSepArgsM___rarg___boxed(lean_object*, lean_object*
|
|||
lean_object* l_Lean_Parser_rawFn(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_charLitFn___closed__1;
|
||||
lean_object* l_Lean_Parser_dollarSymbol___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_checkRbpLt(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_compileParserDescr___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_regBuiltinTermParserAttr(lean_object*);
|
||||
lean_object* l_Lean_Parser_nodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1100,6 +1103,7 @@ lean_object* l_Lean_Parser_compileParserDescr___main___closed__4;
|
|||
lean_object* l_Lean_Parser_Parser_inhabited___closed__1;
|
||||
lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
|
||||
lean_object* l_Lean_Parser_categoryParserOfStack___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__1;
|
||||
lean_object* l_List_foldlM___main___at___private_Lean_Parser_Parser_25__ParserAttribute_add___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -11026,48 +11030,48 @@ lean_dec(x_1);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Lean_Parser_checkRbpLtFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; uint8_t x_6;
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
x_6 = lean_nat_dec_lt(x_1, x_5);
|
||||
x_6 = lean_nat_dec_lt(x_5, x_1);
|
||||
if (x_6 == 0)
|
||||
{
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Lean_Parser_ParserState_mkUnexpectedError(x_4, x_2);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRbpLtFn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Lean_Parser_checkRbpLtFn(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Lean_Parser_checkRbpLt___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Lean_Parser_checkRbpLtFn(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRBPGreater(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_Lean_Parser_checkRbpLt(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_checkRBPGreater___elambda__1___boxed), 4, 2);
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_checkRbpLt___elambda__1___boxed), 4, 2);
|
||||
lean_closure_set(x_3, 0, x_1);
|
||||
lean_closure_set(x_3, 1, x_2);
|
||||
x_4 = l_Lean_Parser_epsilonInfo;
|
||||
|
|
@ -11077,16 +11081,35 @@ lean_ctor_set(x_5, 1, x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Lean_Parser_checkRbpLt___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Parser_checkRBPGreater___elambda__1(x_1, x_2, x_3, x_4);
|
||||
x_5 = l_Lean_Parser_checkRbpLt___elambda__1(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRbpLe(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_add(x_1, x_3);
|
||||
x_5 = l_Lean_Parser_checkRbpLt(x_4, x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkRbpLe___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_checkRbpLe(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -29315,7 +29338,7 @@ if (x_7 == 0)
|
|||
lean_object* x_8; lean_object* x_9;
|
||||
x_8 = lean_unsigned_to_nat(0u);
|
||||
lean_inc(x_1);
|
||||
x_9 = l___private_Lean_Data_Trie_3__findAux___main___rarg(x_3, x_1, x_8);
|
||||
x_9 = l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(x_3, x_1, x_8);
|
||||
if (lean_obj_tag(x_9) == 0)
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11;
|
||||
|
|
@ -35466,6 +35489,42 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_getTokenLbp_x3f(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = l_Lean_Parser_getTokenTable(x_1);
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(x_2, x_3, x_4);
|
||||
if (lean_obj_tag(x_5) == 0)
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_box(0);
|
||||
return x_6;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_5);
|
||||
x_8 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_7);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_getTokenLbp_x3f___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_getTokenLbp_x3f(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_mkInputContext(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -70,7 +70,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___
|
|||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_strLitNoAntiquot_parenthesizer___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withPosition_parenthesizer___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_evalNat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_Traverser_up(lean_object*);
|
||||
|
|
@ -607,6 +606,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1(lean_o
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWsAux_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6;
|
||||
lean_object* l_Nat_forMAux___main___at_Lean_PrettyPrinter_Parenthesizer_visit___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
extern lean_object* l___private_Lean_Meta_Tactic_Util_1__regTraceClasses___closed__1;
|
||||
extern lean_object* l_Lean_mkAppStx___closed__2;
|
||||
lean_object* l___private_Lean_PrettyPrinter_Parenthesizer_1__regTraceClasses(lean_object*);
|
||||
|
|
@ -12502,7 +12502,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__3;
|
||||
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -12548,7 +12548,7 @@ if (lean_obj_tag(x_8) == 0)
|
|||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_9 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__1;
|
||||
x_10 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_10 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_11 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__6;
|
||||
lean_inc(x_1);
|
||||
x_12 = l_Lean_Parser_unicodeSymbolFnAux(x_9, x_10, x_11, x_1, x_7);
|
||||
|
|
@ -12591,7 +12591,7 @@ _start:
|
|||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__1;
|
||||
x_3 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_3 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_4 = l_Lean_Parser_unicodeSymbolInfo(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue