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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-22 12:59:33 -08:00
parent 5193ce45e4
commit ff43704411
19 changed files with 11111 additions and 10098 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
stage0/src/Init/Lean/Elab/Syntax.lean
View file

@ -31,31 +31,29 @@ else if ds.size == 1 then
else
ds.foldlFromM (fun r d => `(ParserDescr.andthen $r $d)) (ds.get! 0) 1
/- The translator from `syntax` to `ParserDescr` syntax uses the following modes -/
inductive ToParserDescrMode
| anyCat -- Node kind `Lean.Parser.Syntax.cat` is allowed for any category
| exceptCat (catName : Name) -- Node kind `Lean.Parser.Syntax.cat` is allowed if the category is not `catName`
| toPushLeading (catName : Name) -- Node kind `Lean.Parser.Syntax.cat` is allowed if the category is `catName`, and it is translated into `ParserDescr.pushLeading`
structure ToParserDescrContext :=
(catName : Name)
(first : Bool)
(pushLeadingAllowed : Bool)
/- When `leadingIdentAsSymbol == true` we convert
`Lean.Parser.Syntax.atom` into `Lean.ParserDescr.nonReservedSymbol`
See comment at `Parser.ParserCategory`. -/
(leadingIdentAsSymbol : Bool)
abbrev ToParserDescrM := ReaderT ToParserDescrMode (StateT Bool TermElabM)
private def getMode : ToParserDescrM ToParserDescrMode := read
abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateT Bool TermElabM)
private def markAsTrailingParser : ToParserDescrM Unit := set true
@[inline] private def withAnyIfNotFirst {α} (first : Bool) (x : ToParserDescrM α) : ToParserDescrM α :=
fun mode => match mode, first with
| mode, true => x mode
| _, false => x ToParserDescrMode.anyCat
@[inline] private def withFirst {α} (first : Bool) (x : ToParserDescrM α) : ToParserDescrM α :=
adaptReader (fun (ctx : ToParserDescrContext) => { first := ctx.first && first, .. ctx }) x
@[inline] private def withNoPushLeading {α} (x : ToParserDescrM α) : ToParserDescrM α :=
fun mode => match mode with
| ToParserDescrMode.toPushLeading cat => x (ToParserDescrMode.exceptCat cat)
| mode => x mode
adaptReader (fun (ctx : ToParserDescrContext) => { pushLeadingAllowed := false, .. ctx }) x
partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
| stx =>
let kind := stx.getKind;
if kind == nullKind then do
args ← stx.getArgs.mapIdxM $ fun i arg => withAnyIfNotFirst (i == 0) (toParserDescrAux arg);
args ← stx.getArgs.mapIdxM $ fun i arg => withFirst (i == 0) (toParserDescrAux arg);
liftM $ mkParserSeq args
else if kind == choiceKind then do
toParserDescrAux (stx.getArg 0)
@ -66,30 +64,26 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
let rbp? : Option Nat := expandOptPrecedence (stx.getArg 1);
env ← liftM getEnv;
unless (Parser.isParserCategory env cat) $ liftM $ throwError (stx.getArg 3) ("unknown category '" ++ cat ++ "'");
mode ← getMode;
match mode with
| ToParserDescrMode.toPushLeading cat' =>
if cat == cat' then do
unless rbp?.isNone $ liftM $ throwError (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
markAsTrailingParser; -- mark as trailing par
`(ParserDescr.pushLeading)
else
let rbp := rbp?.getD 0;
`(ParserDescr.parser $(quote cat) $(quote rbp))
| ToParserDescrMode.anyCat =>
ctx ← read;
if ctx.first && cat == ctx.catName then do
unless rbp?.isNone $ liftM $ throwError (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
ctx ← read;
unless ctx.pushLeadingAllowed $ liftM $
throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion");
markAsTrailingParser; -- mark as trailing par
`(ParserDescr.pushLeading)
else
let rbp := rbp?.getD 0;
`(ParserDescr.parser $(quote cat) $(quote rbp))
| ToParserDescrMode.exceptCat cat' =>
if cat == cat' then
liftM $ throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion")
else
let rbp := rbp?.getD 0;
`(ParserDescr.parser $(quote cat) $(quote rbp))
else if kind == `Lean.Parser.Syntax.atom then do
match (stx.getArg 0).isStrLit? with
| some atom =>
let rbp : Option Nat := expandOptPrecedence (stx.getArg 1);
`(ParserDescr.symbol $(quote atom) $(quote rbp))
| some atom => do
let rbp? : Option Nat := expandOptPrecedence (stx.getArg 1);
ctx ← read;
if ctx.leadingIdentAsSymbol && rbp?.isNone then
`(ParserDescr.nonReservedSymbol $(quote atom) false)
else
`(ParserDescr.symbol $(quote atom) $(quote rbp?))
| none => liftM throwUnsupportedSyntax
else if kind == `Lean.Parser.Syntax.num then
`(ParserDescr.num)
@ -133,9 +127,10 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
where `newStx` is of category `term`. After elaboration, `newStx` should have type
`TrailingParserDescr` if `trailingParser == true`, and `ParserDescr` otherwise. -/
def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) :=
let mode := ToParserDescrMode.toPushLeading catName;
(toParserDescrAux stx mode).run false
def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) := do
env ← getEnv;
let leadingIdentAsSymbol := Parser.leadingIdentAsSymbol env catName;
(toParserDescrAux stx { catName := catName, first := true, pushLeadingAllowed := true, leadingIdentAsSymbol := leadingIdentAsSymbol }).run false
end Term

40
stage0/src/Init/Lean/Elab/Tactic/Basic.lean
View file

@ -160,15 +160,38 @@ private def evalTacticUsing (s : State) (stx : Syntax) : List Tactic → TacticM
| [] => do
let refFmt := stx.prettyPrint;
throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
| (elabFn::elabFns) => catch (elabFn stx)
| (evalFn::evalFns) => catch (evalFn stx)
(fun ex => match ex with
| Exception.error _ => throw ex
| Exception.unsupportedSyntax => do set s; evalTacticUsing elabFns)
| Exception.error _ =>
match evalFns with
| [] => throw ex
| _ => do set s; evalTacticUsing evalFns
| Exception.unsupportedSyntax => do set s; evalTacticUsing evalFns)
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (stx : Syntax) (x : TacticM α) : TacticM α :=
adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x
@[specialize] private def expandTacticMacroFns (evalTactic : Syntax → TacticM Unit) (stx : Syntax) : List Macro → TacticM Unit
| [] => throwError stx ("tactic '" ++ toString stx.getKind ++ "' has not been implemented")
| m::ms => do
scp ← getCurrMacroScope;
match m stx scp with
| none => expandTacticMacroFns ms
| some stx' =>
catch
(evalTactic stx')
(fun ex => match ms with
| [] => throw ex
| _ => expandTacticMacroFns ms)
@[inline] def expandTacticMacro (evalTactic : Syntax → TacticM Unit) (stx : Syntax) : TacticM Unit := do
env ← getEnv;
let k := stx.getKind;
let table := (macroAttribute.ext.getState env).table;
let macroFns := (table.find? k).getD [];
expandTacticMacroFns evalTactic stx macroFns
partial def evalTactic : Syntax → TacticM Unit
| stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
| Syntax.node k args =>
@ -177,18 +200,13 @@ partial def evalTactic : Syntax → TacticM Unit
-- Syntax quotations can return multiple ones
stx.forSepArgsM evalTactic
else do
trace `Elab.step stx $ fun _ => stx;
trace `Elab.step stx $ fun _ => stx;
s ← get;
let table := (tacticElabAttribute.ext.getState s.env).table;
let k := stx.getKind;
match table.find? k with
| some elabFns => evalTacticUsing s stx elabFns
| none => do
scp ← getCurrMacroScope;
env ← getEnv;
match expandMacro env stx scp with
| some stx' => withMacroExpansion stx $ evalTactic stx'
| none => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
| some evalFns => evalTacticUsing s stx evalFns
| none => expandTacticMacro evalTactic stx
| _ => throwError stx "unexpected command"
/-- Adapt a syntax transformation to a regular tactic evaluator. -/

14
stage0/src/Init/Lean/Hygiene.lean
View file

@ -35,20 +35,6 @@ instance MonadQuotation : MonadQuotation Unhygienic := {
protected def run {α : Type} (x : Unhygienic α) : α := run x 0 1
end Unhygienic
private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
| n , acc => (n, acc.reverse)
/--
Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
This operation is useful for analyzing/transforming the original identifiers, then adding back
the scopes (via `addMacroScopes`). -/
def extractMacroScopes (n : Name) : Name × List MacroScope :=
extractMacroScopesAux n []
def Name.eraseMacroScopes (n : Name) : Name :=
(extractMacroScopes n).1
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
{ getCurrMacroScope := liftM (getCurrMacroScope : m Nat),
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }

35
stage0/src/Init/Lean/Parser/Parser.lean
View file

@ -1070,7 +1070,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind numLitKind) then s.mkErrorAt "numeral" iniPos else s
@[inline] def numLit {k : ParserKind} : Parser k :=
@[inline] def numLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := numLitFn,
info := mkAtomicInfo "numLit" }
@ -1080,7 +1080,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind strLitKind) then s.mkErrorAt "string literal" iniPos else s
@[inline] def strLit {k : ParserKind} : Parser k :=
@[inline] def strLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := strLitFn,
info := mkAtomicInfo "strLit" }
@ -1090,7 +1090,7 @@ fun _ c s =>
let s := tokenFn c s;
if s.hasError || !(s.stxStack.back.isOfKind charLitKind) then s.mkErrorAt "character literal" iniPos else s
@[inline] def charLit {k : ParserKind} : Parser k :=
@[inline] def charLitNoAntiquot {k : ParserKind} : Parser k :=
{ fn := charLitFn,
info := mkAtomicInfo "charLit" }
@ -1476,6 +1476,15 @@ mkAntiquot "ident" `ident <|> identNoAntiquot
def rawIdent {k : ParserKind} : Parser k :=
mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
def numLit {k : ParserKind} : Parser k :=
mkAntiquot "numLit" numLitKind <|> numLitNoAntiquot
def strLit {k : ParserKind} : Parser k :=
mkAntiquot "strLit" strLitKind <|> strLitNoAntiquot
def charLit {k : ParserKind} : Parser k :=
mkAntiquot "charLit" charLitKind <|> charLitNoAntiquot
def categoryParserOfStackFn (offset : Nat) : ParserFn leading :=
fun rbp ctx s =>
let stack := s.stxStack;
@ -1747,13 +1756,31 @@ if isParserCategory env catName then
else
pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName leadingIdentAsSymbol
def categoryParserFnImpl (catName : Name) : ParserFn leading :=
/-
Return true if in the given category leading identifiers in parsers may be treated as atoms/symbols.
See comment at `ParserCategory`. -/
def leadingIdentAsSymbol (env : Environment) (catName : Name) : Bool :=
match (parserExtension.getState env).categories.find? catName with
| none => false
| some cat => cat.leadingIdentAsSymbol
def categoryParserFnImplAux (catName : Name) : ParserFn leading :=
fun rbp ctx s =>
let categories := (parserExtension.getState ctx.env).categories;
match categories.find? catName with
| some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol rbp ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
private def catNameToString : Name → String
| Name.str Name.anonymous s _ => s
| n => n.toString
def categoryParserFnImpl (catName : Name) : ParserFn leading :=
if catName != `term then
orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName)
else
categoryParserFnImplAux catName
@[init] def setCategoryParserFnRef : IO Unit :=
categoryParserFnRef.set categoryParserFnImpl

161
stage0/src/Init/Lean/Syntax.lean
View file

@ -316,165 +316,4 @@ mkStxStrLit val
def mkStxNumLitAux (val : Nat) : Syntax :=
mkStxNumLit (toString val)
namespace Syntax
/- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
different ways of representing them. So, our atoms contain just the parsed string.
The main Lean parser uses the kind `numLitKind` for storing natural numbers that can be encoded
in binary, octal, decimal and hexadecimal format. `isNatLit` implements a "decoder"
for Syntax objects representing these numerals. -/
private partial def decodeBinLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if c == '0' then decodeBinLitAux (s.next i) (2*val)
else if c == '1' then decodeBinLitAux (s.next i) (2*val + 1)
else none
private partial def decodeOctalLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if '0' ≤ c && c ≤ '7' then decodeOctalLitAux (s.next i) (8*val + c.toNat - '0'.toNat)
else none
private def decodeHexDigit (s : String) (i : String.Pos) : Option (Nat × String.Pos) :=
let c := s.get i;
let i := s.next i;
if '0' ≤ c && c ≤ '9' then some (c.toNat - '0'.toNat, i)
else if 'a' ≤ c && c ≤ 'f' then some (10 + c.toNat - 'a'.toNat, i)
else if 'A' ≤ c && c ≤ 'F' then some (10 + c.toNat - 'A'.toNat, i)
else none
private partial def decodeHexLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else match decodeHexDigit s i with
| some (d, i) => decodeHexLitAux i (16*val + d)
| none => none
private partial def decodeDecimalLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux (s.next i) (10*val + c.toNat - '0'.toNat)
else none
private def decodeNatLitVal (s : String) : Option Nat :=
let len := s.length;
if len == 0 then none
else
let c := s.get 0;
if c == '0' then
if len == 1 then some 0
else
let c := s.get 1;
if c == 'x' || c == 'X' then decodeHexLitAux s 2 0
else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0
else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0
else if c.isDigit then decodeDecimalLitAux s 0 0
else none
else if c.isDigit then decodeDecimalLitAux s 0 0
else none
def isNatLitAux (nodeKind : SyntaxNodeKind) : Syntax → Option Nat
| Syntax.node k args =>
if k == nodeKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeNatLitVal val
| _ => none
else
none
| _ => none
def isNatLit? (s : Syntax) : Option Nat :=
isNatLitAux numLitKind s
def isFieldIdx? (s : Syntax) : Option Nat :=
isNatLitAux fieldIdxKind s
def isIdOrAtom? : Syntax → Option String
| Syntax.atom _ val => some val
| Syntax.ident _ rawVal _ _ => some rawVal.toString
| _ => none
def toNat (stx : Syntax) : Nat :=
match stx.isNatLit? with
| some val => val
| none => 0
private def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
let c := s.get i;
let i := s.next i;
if c == '\\' then pure ('\\', i)
else if c = '\"' then pure ('\"', i)
else if c = '\'' then pure ('\'', i)
else if c = 'n' then pure ('\n', i)
else if c = 't' then pure ('\t', i)
else if c = 'x' then do
(d₁, i) ← decodeHexDigit s i;
(d₂, i) ← decodeHexDigit s i;
pure (Char.ofNat (16*d₁ + d₂), i)
else if c = 'u' then do
(d₁, i) ← decodeHexDigit s i;
(d₂, i) ← decodeHexDigit s i;
(d₃, i) ← decodeHexDigit s i;
(d₄, i) ← decodeHexDigit s i;
pure $ (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i)
else
none
partial def decodeStrLitAux (s : String) : String.Pos → String → Option String
| i, acc => do
let c := s.get i;
let i := s.next i;
if c == '\"' then
pure acc
else if c == '\\' then do
(c, i) ← decodeQuotedChar s i;
decodeStrLitAux i (acc.push c)
else
decodeStrLitAux i (acc.push c)
def decodeStrLit (s : String) : Option String :=
decodeStrLitAux s 1 ""
def isStrLit? : Syntax → Option String
| Syntax.node k args =>
if k == strLitKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeStrLit val
| _ => none
else
none
| _ => none
def decodeCharLit (s : String) : Option Char :=
let c := s.get 1;
if c == '\\' then do
(c, _) ← decodeQuotedChar s 2;
pure c
else
pure c
def isCharLit? : Syntax → Option Char
| Syntax.node k args =>
if k == charLitKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeCharLit val
| _ => none
else
none
| _ => none
def hasArgs : Syntax → Bool
| Syntax.node _ args => args.size > 0
| _ => false
end Syntax
end Lean

190
stage0/src/Init/LeanInit.lean
View file

@ -226,6 +226,20 @@ mkNameNum n scp
def addMacroScopes (n : Name) (scps : List MacroScope) : Name :=
scps.foldl addMacroScope n
private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
| n , acc => (n, acc.reverse)
/--
Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
This operation is useful for analyzing/transforming the original identifiers, then adding back
the scopes (via `addMacroScopes`). -/
def extractMacroScopes (n : Name) : Name × List MacroScope :=
extractMacroScopesAux n []
def Name.eraseMacroScopes (n : Name) : Name :=
(extractMacroScopes n).1
abbrev MacroM := ReaderT MacroScope (OptionT Id)
instance MacroM.monadQuotation : MonadQuotation MacroM :=
@ -264,6 +278,11 @@ def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
let info := src.getHeadInfo;
Syntax.atom info val
def Syntax.identToAtom (stx : Syntax) : Syntax :=
match stx with
| Syntax.ident info _ val _ => Syntax.atom info val.eraseMacroScopes.toString
| _ => stx
@[export lean_mk_syntax_ident]
def mkIdent (val : Name) : Syntax :=
Syntax.ident none (toString val).toSubstring val []
@ -321,6 +340,177 @@ mkStxLit strLitKind (repr val) info
def mkStxNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
mkStxLit numLitKind val info
namespace Syntax
/- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
different ways of representing them. So, our atoms contain just the parsed string.
The main Lean parser uses the kind `numLitKind` for storing natural numbers that can be encoded
in binary, octal, decimal and hexadecimal format. `isNatLit` implements a "decoder"
for Syntax objects representing these numerals. -/
private partial def decodeBinLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if c == '0' then decodeBinLitAux (s.next i) (2*val)
else if c == '1' then decodeBinLitAux (s.next i) (2*val + 1)
else none
private partial def decodeOctalLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if '0' ≤ c && c ≤ '7' then decodeOctalLitAux (s.next i) (8*val + c.toNat - '0'.toNat)
else none
private def decodeHexDigit (s : String) (i : String.Pos) : Option (Nat × String.Pos) :=
let c := s.get i;
let i := s.next i;
if '0' ≤ c && c ≤ '9' then some (c.toNat - '0'.toNat, i)
else if 'a' ≤ c && c ≤ 'f' then some (10 + c.toNat - 'a'.toNat, i)
else if 'A' ≤ c && c ≤ 'F' then some (10 + c.toNat - 'A'.toNat, i)
else none
private partial def decodeHexLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else match decodeHexDigit s i with
| some (d, i) => decodeHexLitAux i (16*val + d)
| none => none
private partial def decodeDecimalLitAux (s : String) : String.Pos → Nat → Option Nat
| i, val =>
if s.atEnd i then some val
else
let c := s.get i;
if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux (s.next i) (10*val + c.toNat - '0'.toNat)
else none
private def decodeNatLitVal (s : String) : Option Nat :=
let len := s.length;
if len == 0 then none
else
let c := s.get 0;
if c == '0' then
if len == 1 then some 0
else
let c := s.get 1;
if c == 'x' || c == 'X' then decodeHexLitAux s 2 0
else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0
else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0
else if c.isDigit then decodeDecimalLitAux s 0 0
else none
else if c.isDigit then decodeDecimalLitAux s 0 0
else none
def isNatLitAux (nodeKind : SyntaxNodeKind) : Syntax → Option Nat
| Syntax.node k args =>
if k == nodeKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeNatLitVal val
| _ => none
else
none
| _ => none
def isNatLit? (s : Syntax) : Option Nat :=
isNatLitAux numLitKind s
def isFieldIdx? (s : Syntax) : Option Nat :=
isNatLitAux fieldIdxKind s
def isIdOrAtom? : Syntax → Option String
| Syntax.atom _ val => some val
| Syntax.ident _ rawVal _ _ => some rawVal.toString
| _ => none
def toNat (stx : Syntax) : Nat :=
match stx.isNatLit? with
| some val => val
| none => 0
private def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
let c := s.get i;
let i := s.next i;
if c == '\\' then pure ('\\', i)
else if c = '\"' then pure ('\"', i)
else if c = '\'' then pure ('\'', i)
else if c = 'n' then pure ('\n', i)
else if c = 't' then pure ('\t', i)
else if c = 'x' then do
(d₁, i) ← decodeHexDigit s i;
(d₂, i) ← decodeHexDigit s i;
pure (Char.ofNat (16*d₁ + d₂), i)
else if c = 'u' then do
(d₁, i) ← decodeHexDigit s i;
(d₂, i) ← decodeHexDigit s i;
(d₃, i) ← decodeHexDigit s i;
(d₄, i) ← decodeHexDigit s i;
pure $ (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i)
else
none
partial def decodeStrLitAux (s : String) : String.Pos → String → Option String
| i, acc => do
let c := s.get i;
let i := s.next i;
if c == '\"' then
pure acc
else if c == '\\' then do
(c, i) ← decodeQuotedChar s i;
decodeStrLitAux i (acc.push c)
else
decodeStrLitAux i (acc.push c)
def decodeStrLit (s : String) : Option String :=
decodeStrLitAux s 1 ""
def isStrLit? : Syntax → Option String
| Syntax.node k args =>
if k == strLitKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeStrLit val
| _ => none
else
none
| _ => none
def decodeCharLit (s : String) : Option Char :=
let c := s.get 1;
if c == '\\' then do
(c, _) ← decodeQuotedChar s 2;
pure c
else
pure c
def isCharLit? : Syntax → Option Char
| Syntax.node k args =>
if k == charLitKind && args.size == 1 then
match args.get! 0 with
| (Syntax.atom _ val) => decodeCharLit val
| _ => none
else
none
| _ => none
def hasArgs : Syntax → Bool
| Syntax.node _ args => args.size > 0
| _ => false
def identToStrLit (stx : Syntax) : Syntax :=
match stx with
| Syntax.ident info _ val _ => mkStxStrLit val.toString info
| _ => stx
def strLitToAtom (stx : Syntax) : Syntax :=
match stx.isStrLit? with
| none => stx
| some val => Syntax.atom stx.getHeadInfo val
end Syntax
end Lean
abbrev Array.getSepElems := @Array.getEvenElems

4
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -475,6 +475,7 @@ lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg(lean_o
extern lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__2;
lean_object* l_Array_toList___rarg(lean_object*);
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__3(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_25__BuiltinParserAttribute_add___closed__2;
lean_object* l_Lean_Elab_Command_setOption___closed__3;
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1___closed__5;
lean_object* l___private_Init_Lean_Elab_Command_4__modifyGetState___rarg(lean_object*, lean_object*, lean_object*);
@ -537,7 +538,6 @@ lean_object* l_Lean_Elab_Command_elabOpenOnly___boxed(lean_object*, lean_object*
extern lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1___closed__1;
lean_object* l_Lean_Elab_Command_elabSynth___closed__3;
extern lean_object* l___private_Init_Lean_Parser_Parser_24__BuiltinParserAttribute_add___closed__2;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkMessageAux(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -3755,7 +3755,7 @@ lean_dec(x_13);
lean_dec(x_11);
lean_dec(x_2);
lean_dec(x_1);
x_25 = l___private_Init_Lean_Parser_Parser_24__BuiltinParserAttribute_add___closed__2;
x_25 = l___private_Init_Lean_Parser_Parser_25__BuiltinParserAttribute_add___closed__2;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_12);

9020
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

File diff suppressed because it is too large Load diff

3385
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Init/Lean/Elab/Term.c
View file

@ -657,6 +657,7 @@ lean_object* l_Lean_Elab_Term_monadLog___closed__11;
lean_object* l_Lean_Elab_Term_mkTacticMVar___closed__2;
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_25__BuiltinParserAttribute_add___closed__2;
lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStr(lean_object*);
@ -757,7 +758,6 @@ lean_object* l_Lean_Elab_Term_elabRawNumLit___closed__5;
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__6;
lean_object* l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__1;
lean_object* l_Lean_Elab_Term_resolveName___closed__1;
extern lean_object* l___private_Init_Lean_Parser_Parser_24__BuiltinParserAttribute_add___closed__2;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__2;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resettingSynthInstanceCache(lean_object*);
@ -3122,7 +3122,7 @@ lean_dec(x_13);
lean_dec(x_11);
lean_dec(x_2);
lean_dec(x_1);
x_25 = l___private_Init_Lean_Parser_Parser_24__BuiltinParserAttribute_add___closed__2;
x_25 = l___private_Init_Lean_Parser_Parser_25__BuiltinParserAttribute_add___closed__2;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_12);

62
stage0/stdlib/Init/Lean/Hygiene.c
View file

@ -13,12 +13,8 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_extractMacroScopes(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__3;
lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux(lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_run(lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -32,7 +28,6 @@ lean_object* l_Lean_Unhygienic_MonadQuotation;
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__1;
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__2;
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(lean_object*, lean_object*);
lean_object* l_ReaderT_read___at_Lean_Unhygienic_MonadQuotation___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -119,63 +114,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Unhygienic_run___rarg), 1, 0);
return x_2;
}
}
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 2)
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_5, 0, x_4);
lean_ctor_set(x_5, 1, x_2);
x_1 = x_3;
x_2 = x_5;
goto _start;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = l_List_reverse___rarg(x_2);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set(x_8, 1, x_7);
return x_8;
}
}
}
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_extractMacroScopes(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Name_eraseMacroScopes(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_extractMacroScopes(x_1);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

4
stage0/stdlib/Init/Lean/Meta/Offset.c
View file

@ -13,7 +13,6 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l___private_Init_Lean_Syntax_10__decodeNatLitVal___closed__1;
lean_object* l___private_Init_Lean_Meta_Offset_1__getOffsetAux___main___boxed(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*);
@ -30,6 +29,7 @@ lean_object* l_Lean_Meta_evalNat___main___closed__11;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Meta_evalNat___main(lean_object*);
lean_object* l_Lean_Meta_isDefEqOffset(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_LeanInit_7__decodeNatLitVal___closed__1;
lean_object* l_Lean_Meta_evalNat___main___closed__12;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_Literal_type___closed__1;
@ -233,7 +233,7 @@ return x_12;
else
{
lean_object* x_13;
x_13 = l___private_Init_Lean_Syntax_10__decodeNatLitVal___closed__1;
x_13 = l___private_Init_LeanInit_7__decodeNatLitVal___closed__1;
return x_13;
}
}

813
stage0/stdlib/Init/Lean/Parser/Command.c
View file

@ -305,7 +305,6 @@ lean_object* l_Lean_Parser_Command_namespace___closed__3;
lean_object* l_Lean_Parser_Command_openHiding___closed__3;
lean_object* l_Lean_Parser_Command_init__quot___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__1;
extern lean_object* l_Lean_Parser_strLit___closed__1;
lean_object* l_Lean_Parser_Command_openHiding___closed__5;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_introRule___elambda__1___closed__3;
@ -342,7 +341,6 @@ lean_object* l_Lean_Parser_Command_attrInstance___closed__2;
lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_numLit___closed__1;
lean_object* l_Lean_Parser_Command_structure;
lean_object* l_Lean_Parser_Command_declModifiers___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Command_declaration(lean_object*);
@ -351,6 +349,7 @@ lean_object* l_Lean_Parser_Command_openRenamingItem___closed__7;
extern lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___closed__1;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__10;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_check___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__8;
@ -546,6 +545,7 @@ lean_object* l_Lean_Parser_Command_example___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_partial___closed__3;
extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__2;
lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_stxQuot___closed__2;
@ -887,7 +887,6 @@ lean_object* l_Lean_Parser_Command_section___closed__7;
lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__8;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_declValEqns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structure___closed__9;
lean_object* l_Lean_Parser_strLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_declaration___closed__2;
lean_object* l_Lean_Parser_Command_end___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__8;
@ -1093,7 +1092,6 @@ lean_object* l_Lean_Parser_regCommandParserAttribute(lean_object*);
lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_declaration___closed__13;
lean_object* l_Lean_Parser_Command_namespace___closed__6;
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_init__quot___closed__4;
lean_object* l_Lean_Parser_Command_structure___closed__5;
lean_object* l_Lean_Parser_Command_abbrev___closed__6;
@ -2330,100 +2328,118 @@ return x_1;
lean_object* l_Lean_Parser_Command_attrArg___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
lean_inc(x_2);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
x_6 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
x_10 = lean_ctor_get(x_3, 0);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_11 = lean_array_get_size(x_10);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
x_12 = lean_ctor_get(x_3, 1);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
lean_inc(x_2);
lean_inc(x_1);
x_13 = lean_apply_3(x_9, x_1, x_2, x_3);
x_14 = lean_ctor_get(x_13, 3);
lean_inc(x_14);
if (lean_obj_tag(x_14) == 0)
{
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
return x_9;
lean_dec(x_1);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
lean_inc(x_2);
x_17 = l_Lean_Parser_strLitFn___rarg(x_2, x_14);
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19;
lean_dec(x_14);
x_16 = lean_ctor_get(x_13, 1);
lean_inc(x_16);
x_17 = lean_nat_dec_eq(x_16, x_12);
lean_dec(x_16);
if (x_17 == 0)
{
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
x_19 = l_Lean_Parser_mergeOrElseErrors(x_17, x_11, x_8);
lean_dec(x_8);
return x_19;
lean_dec(x_1);
return x_13;
}
else
{
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = lean_ctor_get(x_18, 0);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
x_22 = lean_nat_dec_eq(x_21, x_8);
lean_dec(x_21);
if (x_22 == 0)
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_inc(x_12);
x_18 = l_Lean_Parser_ParserState_restore(x_13, x_11, x_12);
lean_dec(x_11);
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_array_get_size(x_19);
lean_dec(x_19);
lean_inc(x_2);
lean_inc(x_1);
x_21 = lean_apply_3(x_5, x_1, x_2, x_18);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23;
lean_dec(x_20);
lean_dec(x_16);
lean_dec(x_7);
lean_dec(x_2);
x_23 = l_Lean_Parser_mergeOrElseErrors(x_17, x_11, x_8);
lean_dec(x_8);
lean_dec(x_1);
x_23 = l_Lean_Parser_mergeOrElseErrors(x_21, x_15, x_12);
lean_dec(x_12);
return x_23;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_inc(x_8);
x_24 = l_Lean_Parser_ParserState_restore(x_17, x_16, x_8);
lean_dec(x_16);
x_25 = l_Lean_Parser_numLitFn___rarg(x_2, x_24);
x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_20, x_8);
x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_11, x_8);
lean_dec(x_8);
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_26 = lean_nat_dec_eq(x_25, x_12);
lean_dec(x_25);
if (x_26 == 0)
{
lean_object* x_27;
lean_dec(x_24);
lean_dec(x_20);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
x_27 = l_Lean_Parser_mergeOrElseErrors(x_21, x_15, x_12);
lean_dec(x_12);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
lean_inc(x_12);
x_28 = l_Lean_Parser_ParserState_restore(x_21, x_20, x_12);
lean_dec(x_20);
x_29 = lean_apply_3(x_7, x_1, x_2, x_28);
x_30 = l_Lean_Parser_mergeOrElseErrors(x_29, x_24, x_12);
x_31 = l_Lean_Parser_mergeOrElseErrors(x_30, x_15, x_12);
lean_dec(x_12);
return x_31;
}
}
}
}
@ -2432,11 +2448,15 @@ return x_27;
lean_object* _init_l_Lean_Parser_Command_attrArg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_strLit___closed__1;
x_2 = l_Lean_Parser_numLit___closed__1;
x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = l_Lean_Parser_orelseInfo(x_2, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Command_attrArg___closed__2() {
@ -21235,334 +21255,367 @@ return x_3;
lean_object* l_Lean_Parser_Command_set__option___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = l_Lean_Parser_Command_set__option___elambda__1___closed__4;
x_6 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
x_8 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
x_10 = l_Lean_Parser_Command_set__option___elambda__1___closed__4;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
x_12 = lean_ctor_get(x_3, 0);
lean_inc(x_12);
x_13 = lean_array_get_size(x_12);
lean_dec(x_12);
x_14 = lean_ctor_get(x_3, 1);
lean_inc(x_14);
lean_inc(x_2);
lean_inc(x_1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
x_15 = lean_apply_3(x_11, x_1, x_2, x_3);
x_16 = lean_ctor_get(x_15, 3);
lean_inc(x_16);
if (lean_obj_tag(x_16) == 0)
{
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_90; lean_object* x_91;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
lean_object* x_17; lean_object* x_18; uint8_t x_19;
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_16);
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
x_19 = lean_nat_dec_eq(x_18, x_14);
lean_dec(x_18);
if (x_19 == 0)
{
lean_dec(x_17);
lean_inc(x_2);
x_90 = l_Lean_Parser_tokenFn(x_2, x_16);
x_91 = lean_ctor_get(x_90, 3);
lean_inc(x_91);
if (lean_obj_tag(x_91) == 0)
{
lean_object* x_92; lean_object* x_93;
x_92 = lean_ctor_get(x_90, 0);
lean_inc(x_92);
x_93 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_92);
lean_dec(x_92);
if (lean_obj_tag(x_93) == 2)
{
lean_object* x_94; lean_object* x_95; uint8_t x_96;
x_94 = lean_ctor_get(x_93, 1);
lean_inc(x_94);
lean_dec(x_93);
x_95 = l_Lean_Parser_Command_set__option___elambda__1___closed__6;
x_96 = lean_string_dec_eq(x_94, x_95);
lean_dec(x_94);
if (x_96 == 0)
{
lean_object* x_97; lean_object* x_98;
x_97 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_10);
x_98 = l_Lean_Parser_ParserState_mkErrorsAt(x_90, x_97, x_10);
x_19 = x_98;
goto block_89;
}
else
{
x_19 = x_90;
goto block_89;
}
}
else
{
lean_object* x_99; lean_object* x_100;
lean_dec(x_93);
x_99 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_10);
x_100 = l_Lean_Parser_ParserState_mkErrorsAt(x_90, x_99, x_10);
x_19 = x_100;
goto block_89;
}
}
else
{
lean_object* x_101; lean_object* x_102;
lean_dec(x_91);
x_101 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_10);
x_102 = l_Lean_Parser_ParserState_mkErrorsAt(x_90, x_101, x_10);
x_19 = x_102;
goto block_89;
}
block_89:
{
lean_object* x_20;
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_21; lean_object* x_22;
lean_inc(x_2);
x_21 = lean_apply_3(x_5, x_1, x_2, x_19);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_23 = lean_ctor_get(x_21, 0);
lean_inc(x_23);
x_24 = lean_array_get_size(x_23);
lean_dec(x_23);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_26 = l_Lean_Parser_Command_set__option___elambda__1___closed__7;
x_27 = l_Lean_Parser_Command_set__option___elambda__1___closed__10;
lean_inc(x_2);
x_28 = l_Lean_Parser_nonReservedSymbolFnAux(x_26, x_27, x_2, x_21);
x_29 = lean_ctor_get(x_28, 3);
lean_inc(x_29);
if (lean_obj_tag(x_29) == 0)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_2);
x_30 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_31 = l_Lean_Parser_ParserState_mkNode(x_28, x_30, x_18);
x_32 = l_Lean_Parser_mergeOrElseErrors(x_31, x_13, x_10);
lean_dec(x_10);
return x_32;
}
else
{
lean_object* x_33; lean_object* x_34; uint8_t x_35;
x_33 = lean_ctor_get(x_29, 0);
lean_inc(x_33);
lean_dec(x_29);
x_34 = lean_ctor_get(x_28, 1);
lean_inc(x_34);
x_35 = lean_nat_dec_eq(x_34, x_25);
lean_dec(x_34);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_33);
lean_dec(x_25);
lean_dec(x_24);
lean_dec(x_2);
x_36 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_37 = l_Lean_Parser_ParserState_mkNode(x_28, x_36, x_18);
x_38 = l_Lean_Parser_mergeOrElseErrors(x_37, x_13, x_10);
lean_dec(x_10);
return x_38;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
lean_inc(x_25);
x_39 = l_Lean_Parser_ParserState_restore(x_28, x_24, x_25);
lean_dec(x_24);
x_40 = lean_ctor_get(x_39, 0);
lean_inc(x_40);
x_41 = lean_array_get_size(x_40);
lean_dec(x_40);
x_42 = l_Lean_Parser_Command_set__option___elambda__1___closed__8;
x_43 = l_Lean_Parser_Command_set__option___elambda__1___closed__12;
lean_inc(x_2);
x_44 = l_Lean_Parser_nonReservedSymbolFnAux(x_42, x_43, x_2, x_39);
x_45 = lean_ctor_get(x_44, 3);
lean_inc(x_45);
if (lean_obj_tag(x_45) == 0)
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
lean_dec(x_41);
lean_dec(x_2);
x_46 = l_Lean_Parser_mergeOrElseErrors(x_44, x_33, x_25);
lean_dec(x_25);
x_47 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_48 = l_Lean_Parser_ParserState_mkNode(x_46, x_47, x_18);
x_49 = l_Lean_Parser_mergeOrElseErrors(x_48, x_13, x_10);
lean_dec(x_10);
return x_49;
}
else
{
lean_object* x_50; lean_object* x_51; uint8_t x_52;
x_50 = lean_ctor_get(x_45, 0);
lean_inc(x_50);
lean_dec(x_45);
x_51 = lean_ctor_get(x_44, 1);
lean_inc(x_51);
x_52 = lean_nat_dec_eq(x_51, x_25);
lean_dec(x_51);
if (x_52 == 0)
{
lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56;
lean_dec(x_50);
lean_dec(x_41);
lean_dec(x_2);
x_53 = l_Lean_Parser_mergeOrElseErrors(x_44, x_33, x_25);
lean_dec(x_25);
x_54 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_55 = l_Lean_Parser_ParserState_mkNode(x_53, x_54, x_18);
x_56 = l_Lean_Parser_mergeOrElseErrors(x_55, x_13, x_10);
lean_dec(x_10);
return x_56;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
lean_inc(x_25);
x_57 = l_Lean_Parser_ParserState_restore(x_44, x_41, x_25);
lean_dec(x_41);
x_58 = lean_ctor_get(x_57, 0);
lean_inc(x_58);
x_59 = lean_array_get_size(x_58);
lean_dec(x_58);
lean_inc(x_2);
x_60 = l_Lean_Parser_strLitFn___rarg(x_2, x_57);
x_61 = lean_ctor_get(x_60, 3);
lean_inc(x_61);
if (lean_obj_tag(x_61) == 0)
{
lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
lean_dec(x_59);
lean_dec(x_2);
x_62 = l_Lean_Parser_mergeOrElseErrors(x_60, x_50, x_25);
x_63 = l_Lean_Parser_mergeOrElseErrors(x_62, x_33, x_25);
lean_dec(x_25);
x_64 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_65 = l_Lean_Parser_ParserState_mkNode(x_63, x_64, x_18);
x_66 = l_Lean_Parser_mergeOrElseErrors(x_65, x_13, x_10);
lean_dec(x_10);
return x_66;
}
else
{
lean_object* x_67; lean_object* x_68; uint8_t x_69;
x_67 = lean_ctor_get(x_61, 0);
lean_inc(x_67);
lean_dec(x_61);
x_68 = lean_ctor_get(x_60, 1);
lean_inc(x_68);
x_69 = lean_nat_dec_eq(x_68, x_25);
lean_dec(x_68);
if (x_69 == 0)
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
lean_dec(x_67);
lean_dec(x_59);
lean_dec(x_2);
x_70 = l_Lean_Parser_mergeOrElseErrors(x_60, x_50, x_25);
x_71 = l_Lean_Parser_mergeOrElseErrors(x_70, x_33, x_25);
lean_dec(x_25);
x_72 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_73 = l_Lean_Parser_ParserState_mkNode(x_71, x_72, x_18);
x_74 = l_Lean_Parser_mergeOrElseErrors(x_73, x_13, x_10);
lean_dec(x_10);
return x_74;
}
else
{
lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82;
lean_inc(x_25);
x_75 = l_Lean_Parser_ParserState_restore(x_60, x_59, x_25);
lean_dec(x_59);
x_76 = l_Lean_Parser_numLitFn___rarg(x_2, x_75);
x_77 = l_Lean_Parser_mergeOrElseErrors(x_76, x_67, x_25);
x_78 = l_Lean_Parser_mergeOrElseErrors(x_77, x_50, x_25);
x_79 = l_Lean_Parser_mergeOrElseErrors(x_78, x_33, x_25);
lean_dec(x_25);
x_80 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_81 = l_Lean_Parser_ParserState_mkNode(x_79, x_80, x_18);
x_82 = l_Lean_Parser_mergeOrElseErrors(x_81, x_13, x_10);
lean_dec(x_10);
return x_82;
}
}
}
}
}
}
}
else
{
lean_object* x_83; lean_object* x_84; lean_object* x_85;
lean_dec(x_22);
lean_dec(x_2);
x_83 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_84 = l_Lean_Parser_ParserState_mkNode(x_21, x_83, x_18);
x_85 = l_Lean_Parser_mergeOrElseErrors(x_84, x_13, x_10);
lean_dec(x_10);
return x_85;
}
}
else
{
lean_object* x_86; lean_object* x_87; lean_object* x_88;
lean_dec(x_20);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_86 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_87 = l_Lean_Parser_ParserState_mkNode(x_19, x_86, x_18);
x_88 = l_Lean_Parser_mergeOrElseErrors(x_87, x_13, x_10);
lean_dec(x_10);
return x_88;
return x_15;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_94; lean_object* x_95;
lean_inc(x_14);
x_20 = l_Lean_Parser_ParserState_restore(x_15, x_13, x_14);
lean_dec(x_13);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_array_get_size(x_21);
lean_dec(x_21);
lean_inc(x_2);
x_94 = l_Lean_Parser_tokenFn(x_2, x_20);
x_95 = lean_ctor_get(x_94, 3);
lean_inc(x_95);
if (lean_obj_tag(x_95) == 0)
{
lean_object* x_96; lean_object* x_97;
x_96 = lean_ctor_get(x_94, 0);
lean_inc(x_96);
x_97 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_96);
lean_dec(x_96);
if (lean_obj_tag(x_97) == 2)
{
lean_object* x_98; lean_object* x_99; uint8_t x_100;
x_98 = lean_ctor_get(x_97, 1);
lean_inc(x_98);
lean_dec(x_97);
x_99 = l_Lean_Parser_Command_set__option___elambda__1___closed__6;
x_100 = lean_string_dec_eq(x_98, x_99);
lean_dec(x_98);
if (x_100 == 0)
{
lean_object* x_101; lean_object* x_102;
x_101 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_14);
x_102 = l_Lean_Parser_ParserState_mkErrorsAt(x_94, x_101, x_14);
x_23 = x_102;
goto block_93;
}
else
{
x_23 = x_94;
goto block_93;
}
}
else
{
lean_object* x_103; lean_object* x_104;
lean_dec(x_97);
x_103 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_14);
x_104 = l_Lean_Parser_ParserState_mkErrorsAt(x_94, x_103, x_14);
x_23 = x_104;
goto block_93;
}
}
else
{
lean_object* x_105; lean_object* x_106;
lean_dec(x_95);
x_105 = l_Lean_Parser_Command_set__option___elambda__1___closed__15;
lean_inc(x_14);
x_106 = l_Lean_Parser_ParserState_mkErrorsAt(x_94, x_105, x_14);
x_23 = x_106;
goto block_93;
}
block_93:
{
lean_object* x_24;
x_24 = lean_ctor_get(x_23, 3);
lean_inc(x_24);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25; lean_object* x_26;
lean_inc(x_2);
lean_inc(x_1);
x_25 = lean_apply_3(x_9, x_1, x_2, x_23);
x_26 = lean_ctor_get(x_25, 3);
lean_inc(x_26);
if (lean_obj_tag(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; lean_object* x_33;
x_27 = lean_ctor_get(x_25, 0);
lean_inc(x_27);
x_28 = lean_array_get_size(x_27);
lean_dec(x_27);
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
x_30 = l_Lean_Parser_Command_set__option___elambda__1___closed__7;
x_31 = l_Lean_Parser_Command_set__option___elambda__1___closed__10;
lean_inc(x_2);
x_32 = l_Lean_Parser_nonReservedSymbolFnAux(x_30, x_31, x_2, x_25);
x_33 = lean_ctor_get(x_32, 3);
lean_inc(x_33);
if (lean_obj_tag(x_33) == 0)
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_dec(x_29);
lean_dec(x_28);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_34 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_35 = l_Lean_Parser_ParserState_mkNode(x_32, x_34, x_22);
x_36 = l_Lean_Parser_mergeOrElseErrors(x_35, x_17, x_14);
lean_dec(x_14);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_37 = lean_ctor_get(x_33, 0);
lean_inc(x_37);
lean_dec(x_33);
x_38 = lean_ctor_get(x_32, 1);
lean_inc(x_38);
x_39 = lean_nat_dec_eq(x_38, x_29);
lean_dec(x_38);
if (x_39 == 0)
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
lean_dec(x_37);
lean_dec(x_29);
lean_dec(x_28);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_40 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_41 = l_Lean_Parser_ParserState_mkNode(x_32, x_40, x_22);
x_42 = l_Lean_Parser_mergeOrElseErrors(x_41, x_17, x_14);
lean_dec(x_14);
return x_42;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
lean_inc(x_29);
x_43 = l_Lean_Parser_ParserState_restore(x_32, x_28, x_29);
lean_dec(x_28);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_array_get_size(x_44);
lean_dec(x_44);
x_46 = l_Lean_Parser_Command_set__option___elambda__1___closed__8;
x_47 = l_Lean_Parser_Command_set__option___elambda__1___closed__12;
lean_inc(x_2);
x_48 = l_Lean_Parser_nonReservedSymbolFnAux(x_46, x_47, x_2, x_43);
x_49 = lean_ctor_get(x_48, 3);
lean_inc(x_49);
if (lean_obj_tag(x_49) == 0)
{
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
lean_dec(x_45);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_50 = l_Lean_Parser_mergeOrElseErrors(x_48, x_37, x_29);
lean_dec(x_29);
x_51 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_52 = l_Lean_Parser_ParserState_mkNode(x_50, x_51, x_22);
x_53 = l_Lean_Parser_mergeOrElseErrors(x_52, x_17, x_14);
lean_dec(x_14);
return x_53;
}
else
{
lean_object* x_54; lean_object* x_55; uint8_t x_56;
x_54 = lean_ctor_get(x_49, 0);
lean_inc(x_54);
lean_dec(x_49);
x_55 = lean_ctor_get(x_48, 1);
lean_inc(x_55);
x_56 = lean_nat_dec_eq(x_55, x_29);
lean_dec(x_55);
if (x_56 == 0)
{
lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
lean_dec(x_54);
lean_dec(x_45);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_57 = l_Lean_Parser_mergeOrElseErrors(x_48, x_37, x_29);
lean_dec(x_29);
x_58 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_59 = l_Lean_Parser_ParserState_mkNode(x_57, x_58, x_22);
x_60 = l_Lean_Parser_mergeOrElseErrors(x_59, x_17, x_14);
lean_dec(x_14);
return x_60;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65;
lean_inc(x_29);
x_61 = l_Lean_Parser_ParserState_restore(x_48, x_45, x_29);
lean_dec(x_45);
x_62 = lean_ctor_get(x_61, 0);
lean_inc(x_62);
x_63 = lean_array_get_size(x_62);
lean_dec(x_62);
lean_inc(x_2);
lean_inc(x_1);
x_64 = lean_apply_3(x_5, x_1, x_2, x_61);
x_65 = lean_ctor_get(x_64, 3);
lean_inc(x_65);
if (lean_obj_tag(x_65) == 0)
{
lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70;
lean_dec(x_63);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
x_66 = l_Lean_Parser_mergeOrElseErrors(x_64, x_54, x_29);
x_67 = l_Lean_Parser_mergeOrElseErrors(x_66, x_37, x_29);
lean_dec(x_29);
x_68 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_69 = l_Lean_Parser_ParserState_mkNode(x_67, x_68, x_22);
x_70 = l_Lean_Parser_mergeOrElseErrors(x_69, x_17, x_14);
lean_dec(x_14);
return x_70;
}
else
{
lean_object* x_71; lean_object* x_72; uint8_t x_73;
x_71 = lean_ctor_get(x_65, 0);
lean_inc(x_71);
lean_dec(x_65);
x_72 = lean_ctor_get(x_64, 1);
lean_inc(x_72);
x_73 = lean_nat_dec_eq(x_72, x_29);
lean_dec(x_72);
if (x_73 == 0)
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
lean_dec(x_71);
lean_dec(x_63);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
x_74 = l_Lean_Parser_mergeOrElseErrors(x_64, x_54, x_29);
x_75 = l_Lean_Parser_mergeOrElseErrors(x_74, x_37, x_29);
lean_dec(x_29);
x_76 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_77 = l_Lean_Parser_ParserState_mkNode(x_75, x_76, x_22);
x_78 = l_Lean_Parser_mergeOrElseErrors(x_77, x_17, x_14);
lean_dec(x_14);
return x_78;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86;
lean_inc(x_29);
x_79 = l_Lean_Parser_ParserState_restore(x_64, x_63, x_29);
lean_dec(x_63);
x_80 = lean_apply_3(x_7, x_1, x_2, x_79);
x_81 = l_Lean_Parser_mergeOrElseErrors(x_80, x_71, x_29);
x_82 = l_Lean_Parser_mergeOrElseErrors(x_81, x_54, x_29);
x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_37, x_29);
lean_dec(x_29);
x_84 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_85 = l_Lean_Parser_ParserState_mkNode(x_83, x_84, x_22);
x_86 = l_Lean_Parser_mergeOrElseErrors(x_85, x_17, x_14);
lean_dec(x_14);
return x_86;
}
}
}
}
}
}
}
else
{
lean_object* x_87; lean_object* x_88; lean_object* x_89;
lean_dec(x_26);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_87 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_88 = l_Lean_Parser_ParserState_mkNode(x_25, x_87, x_22);
x_89 = l_Lean_Parser_mergeOrElseErrors(x_88, x_17, x_14);
lean_dec(x_14);
return x_89;
}
}
else
{
lean_object* x_90; lean_object* x_91; lean_object* x_92;
lean_dec(x_24);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_90 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_91 = l_Lean_Parser_ParserState_mkNode(x_23, x_90, x_22);
x_92 = l_Lean_Parser_mergeOrElseErrors(x_91, x_17, x_14);
lean_dec(x_14);
return x_92;
}
}
}

315
stage0/stdlib/Init/Lean/Parser/Level.c
View file

@ -62,7 +62,6 @@ lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, le
lean_object* l_Lean_Parser_Level_imax___closed__3;
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__6;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_numLit___closed__1;
lean_object* l_Lean_Parser_Level_max___closed__3;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__4;
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__4;
@ -95,6 +94,7 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___closed__1;
lean_object* l_Lean_Parser_Level_num___elambda__1___closed__3;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_num___elambda__1___closed__5;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__11;
lean_object* l_Lean_Parser_Level_imax___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_ident___closed__1;
@ -120,6 +120,7 @@ extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr__
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__3;
lean_object* l_Lean_Parser_Level_max___closed__4;
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__5;
lean_object* l_Lean_Parser_numLit(uint8_t);
lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__2;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__3;
lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*);
@ -163,7 +164,6 @@ lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_obje
lean_object* l_Lean_Parser_Level_paren___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object*);
lean_object* l_Lean_Parser_Level_imax___closed__4;
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__7;
lean_object* l_Lean_Parser_Level_paren___closed__8;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4;
@ -175,6 +175,7 @@ lean_object* l_Lean_Parser_Level_paren___closed__1;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_max___closed__2;
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__6;
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__7;
lean_object* _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__1() {
_start:
{
@ -1691,64 +1692,81 @@ x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Level_num___elambda__1___closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = l_Lean_Parser_numLit(x_1);
return x_2;
}
}
lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Level_num___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Level_num___elambda__1___closed__4;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
lean_inc(x_2);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_2);
lean_inc(x_1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
return x_9;
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_numLitFn___rarg(x_2, x_14);
x_18 = l_Lean_Parser_Level_num___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_16);
x_20 = l_Lean_Parser_mergeOrElseErrors(x_19, x_11, x_8);
lean_dec(x_8);
return x_20;
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
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;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = l_Lean_Parser_Level_num___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_18);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_10);
lean_dec(x_10);
return x_22;
}
}
}
@ -1756,11 +1774,13 @@ return x_20;
lean_object* _init_l_Lean_Parser_Level_num___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_num___elambda__1___closed__2;
x_2 = l_Lean_Parser_numLit___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Level_num___elambda__1___closed__2;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Level_num___closed__2() {
@ -2020,19 +2040,18 @@ return x_2;
lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_3 = lean_string_append(x_1, x_2);
return x_3;
uint8_t x_1; lean_object* x_2;
x_1 = 1;
x_2 = l_Lean_Parser_numLit(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__4;
x_2 = l_Char_HasRepr___closed__1;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
@ -2041,8 +2060,18 @@ lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__5;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Level_addLit___elambda__1___closed__5;
x_2 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2052,94 +2081,106 @@ return x_3;
lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
lean_dec(x_4);
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_4 = l_Lean_Parser_Level_addLit___elambda__1___closed__4;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
lean_inc(x_1);
lean_inc(x_3);
x_6 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1);
x_7 = lean_ctor_get(x_3, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
x_8 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1);
x_9 = lean_ctor_get(x_3, 3);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
lean_dec(x_3);
lean_inc(x_2);
x_9 = l_Lean_Parser_tokenFn(x_2, x_6);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
x_11 = l_Lean_Parser_tokenFn(x_2, x_8);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
x_12 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_11);
lean_dec(x_11);
if (lean_obj_tag(x_12) == 2)
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 1);
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_15 = lean_string_dec_eq(x_13, x_14);
x_14 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_13);
lean_dec(x_13);
if (x_15 == 0)
if (lean_obj_tag(x_14) == 2)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_17 = lean_string_dec_eq(x_15, x_16);
lean_dec(x_15);
if (x_17 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_dec(x_5);
lean_dec(x_2);
x_16 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_17 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_16, x_8);
x_18 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_5);
return x_19;
lean_dec(x_1);
x_18 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_19 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_18, x_10);
x_20 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_7);
return x_21;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_8);
x_20 = l_Lean_Parser_numLitFn___rarg(x_2, x_9);
x_21 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_22 = l_Lean_Parser_ParserState_mkNode(x_20, x_21, x_5);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_12);
lean_dec(x_2);
x_23 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_23, x_8);
x_25 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_5);
return x_26;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_10);
lean_dec(x_2);
x_27 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_27, x_8);
x_29 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_5);
return x_30;
x_22 = lean_apply_3(x_5, x_1, x_2, x_11);
x_23 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_24 = l_Lean_Parser_ParserState_mkNode(x_22, x_23, x_7);
return x_24;
}
}
else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_7);
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
lean_dec(x_14);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_25 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_25, x_10);
x_27 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_7);
return x_28;
}
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_12);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_29 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_29, x_10);
x_31 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_7);
return x_32;
}
}
else
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_31 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_6, x_31, x_5);
return x_32;
lean_dec(x_1);
x_33 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_34 = l_Lean_Parser_ParserState_mkNode(x_8, x_33, x_7);
return x_34;
}
}
}
@ -2166,11 +2207,13 @@ return x_3;
lean_object* _init_l_Lean_Parser_Level_addLit___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_addLit___closed__2;
x_2 = l_Lean_Parser_numLit___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Level_addLit___closed__2;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___closed__4() {
@ -2399,6 +2442,8 @@ l_Lean_Parser_Level_num___elambda__1___closed__3 = _init_l_Lean_Parser_Level_num
lean_mark_persistent(l_Lean_Parser_Level_num___elambda__1___closed__3);
l_Lean_Parser_Level_num___elambda__1___closed__4 = _init_l_Lean_Parser_Level_num___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Level_num___elambda__1___closed__4);
l_Lean_Parser_Level_num___elambda__1___closed__5 = _init_l_Lean_Parser_Level_num___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Level_num___elambda__1___closed__5);
l_Lean_Parser_Level_num___closed__1 = _init_l_Lean_Parser_Level_num___closed__1();
lean_mark_persistent(l_Lean_Parser_Level_num___closed__1);
l_Lean_Parser_Level_num___closed__2 = _init_l_Lean_Parser_Level_num___closed__2();
@ -2445,6 +2490,8 @@ l_Lean_Parser_Level_addLit___elambda__1___closed__5 = _init_l_Lean_Parser_Level_
lean_mark_persistent(l_Lean_Parser_Level_addLit___elambda__1___closed__5);
l_Lean_Parser_Level_addLit___elambda__1___closed__6 = _init_l_Lean_Parser_Level_addLit___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Level_addLit___elambda__1___closed__6);
l_Lean_Parser_Level_addLit___elambda__1___closed__7 = _init_l_Lean_Parser_Level_addLit___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_addLit___elambda__1___closed__7);
l_Lean_Parser_Level_addLit___closed__1 = _init_l_Lean_Parser_Level_addLit___closed__1();
lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__1);
l_Lean_Parser_Level_addLit___closed__2 = _init_l_Lean_Parser_Level_addLit___closed__2();

2642
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

File diff suppressed because it is too large Load diff

360
stage0/stdlib/Init/Lean/Parser/Syntax.c
View file

@ -163,13 +163,11 @@ lean_object* l_Lean_Parser_Command_macroArgType___elambda__1(lean_object*, lean_
lean_object* l_Lean_Parser_Command_infix;
lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Command_reserve(lean_object*);
lean_object* l_Lean_Parser_Command_syntax___closed__12;
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_identPrec;
lean_object* l_Lean_Parser_Command_infixl___closed__2;
extern lean_object* l_Lean_Parser_strLit___closed__1;
lean_object* l_Lean_Parser_Syntax_many1___closed__4;
lean_object* l_Lean_Parser_precedence___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__1;
@ -195,7 +193,6 @@ lean_object* l_Lean_Parser_Command_mixfix___closed__8;
lean_object* l_Lean_Parser_Syntax_ident___closed__3;
lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_macro__rules___closed__6;
extern lean_object* l_Lean_Parser_numLit___closed__1;
lean_object* l_Lean_Parser_Syntax_ident___closed__5;
lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__5;
@ -209,6 +206,7 @@ lean_object* l_Lean_Parser_Command_macroArg;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__1;
extern lean_object* l_Lean_Parser_mkAntiquot___closed__5;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_infix___closed__4;
lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_prefix___closed__4;
@ -341,6 +339,7 @@ lean_object* l_Lean_Parser_Command_macroTailTactic;
lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_termParser___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_Term_stxQuot___closed__2;
lean_object* l_Lean_Parser_Command_infix___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_maxPrec;
@ -528,7 +527,6 @@ lean_object* l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__3;
lean_object* l_Lean_Parser_Command_identPrec___closed__2;
lean_object* l_Lean_Parser_Syntax_sepBy1___closed__6;
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__7;
lean_object* l_Lean_Parser_strLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__1;
lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_mixfixSymbol;
@ -651,7 +649,6 @@ lean_object* l_Lean_Parser_Syntax_optional___closed__1;
lean_object* l_Lean_Parser_Syntax_cat___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__3;
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_object*);
lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__8;
lean_object* l_Lean_Parser_Syntax_many1___elambda__1(lean_object*, lean_object*, lean_object*);
@ -706,6 +703,7 @@ lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macro___closed__9;
lean_object* l_Lean_Parser_Command_syntax___closed__4;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_macro__rules___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1___closed__4;
lean_object* l_Lean_Parser_syntaxParser(uint8_t, lean_object*);
lean_object* l_Lean_Parser_Command_macro__rules___closed__5;
@ -971,54 +969,58 @@ return x_1;
lean_object* l_Lean_Parser_precedenceLit___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
lean_dec(x_4);
x_6 = lean_ctor_get(x_3, 1);
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
lean_inc(x_2);
x_7 = l_Lean_Parser_numLitFn___rarg(x_2, x_3);
x_8 = lean_ctor_get(x_7, 3);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_7;
}
else
{
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_ctor_get(x_7, 1);
lean_inc(x_2);
lean_inc(x_1);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
x_11 = lean_nat_dec_eq(x_10, x_6);
lean_dec(x_10);
if (x_11 == 0)
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_9);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_7;
return x_9;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_inc(x_6);
x_12 = l_Lean_Parser_ParserState_restore(x_7, x_5, x_6);
lean_dec(x_5);
x_13 = l_Lean_Parser_maxPrec___elambda__1(x_1, x_2, x_12);
x_14 = l_Lean_Parser_mergeOrElseErrors(x_13, x_9, x_6);
lean_dec(x_6);
return x_14;
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = l_Lean_Parser_maxPrec___elambda__1(x_1, x_2, x_14);
x_16 = l_Lean_Parser_mergeOrElseErrors(x_15, x_11, x_8);
lean_dec(x_8);
return x_16;
}
}
}
@ -1026,13 +1028,15 @@ return x_14;
lean_object* _init_l_Lean_Parser_precedenceLit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_maxPrec;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_numLit___closed__1;
x_4 = l_Lean_Parser_orelseInfo(x_3, x_2);
return x_4;
x_3 = l_Lean_Parser_maxPrec;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = l_Lean_Parser_orelseInfo(x_2, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_precedenceLit___closed__2() {
@ -2198,83 +2202,89 @@ return x_5;
lean_object* l_Lean_Parser_Syntax_atom___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Syntax_atom___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Syntax_atom___elambda__1___closed__4;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
lean_inc(x_2);
lean_inc(x_1);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
if (x_13 == 0)
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
lean_inc(x_2);
x_17 = l_Lean_Parser_strLitFn___rarg(x_2, x_14);
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
lean_inc(x_1);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_17);
x_20 = l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_16);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_11, x_8);
lean_dec(x_8);
return x_22;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_21 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_19);
x_22 = l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_18);
x_24 = l_Lean_Parser_mergeOrElseErrors(x_23, x_13, x_10);
lean_dec(x_10);
return x_24;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_dec(x_18);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_20);
lean_dec(x_2);
lean_dec(x_1);
x_23 = l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
x_24 = l_Lean_Parser_ParserState_mkNode(x_17, x_23, x_16);
x_25 = l_Lean_Parser_mergeOrElseErrors(x_24, x_11, x_8);
lean_dec(x_8);
return x_25;
x_25 = l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
x_26 = l_Lean_Parser_ParserState_mkNode(x_19, x_25, x_18);
x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_13, x_10);
lean_dec(x_10);
return x_27;
}
}
}
@ -2283,13 +2293,15 @@ return x_25;
lean_object* _init_l_Lean_Parser_Syntax_atom___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_optPrecedence;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_strLit___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
x_3 = l_Lean_Parser_optPrecedence;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = l_Lean_Parser_andthenInfo(x_2, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Syntax_atom___closed__2() {
@ -4665,7 +4677,7 @@ lean_dec(x_13);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_16 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_17 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_16, x_8);
x_18 = l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_5);
@ -4684,7 +4696,7 @@ else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_dec(x_12);
x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_23 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_22, x_8);
x_24 = l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_5);
@ -4695,7 +4707,7 @@ else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_dec(x_10);
x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__6;
x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_26, x_8);
x_28 = l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_5);
@ -7669,83 +7681,89 @@ return x_5;
lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__4;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
lean_inc(x_2);
lean_inc(x_1);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
if (x_13 == 0)
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
lean_inc(x_2);
x_17 = l_Lean_Parser_strLitFn___rarg(x_2, x_14);
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
lean_inc(x_1);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_17);
x_20 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_16);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_11, x_8);
lean_dec(x_8);
return x_22;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_21 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_19);
x_22 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2;
x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_18);
x_24 = l_Lean_Parser_mergeOrElseErrors(x_23, x_13, x_10);
lean_dec(x_10);
return x_24;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_dec(x_18);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_20);
lean_dec(x_2);
lean_dec(x_1);
x_23 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2;
x_24 = l_Lean_Parser_ParserState_mkNode(x_17, x_23, x_16);
x_25 = l_Lean_Parser_mergeOrElseErrors(x_24, x_11, x_8);
lean_dec(x_8);
return x_25;
x_25 = l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2;
x_26 = l_Lean_Parser_ParserState_mkNode(x_19, x_25, x_18);
x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_13, x_10);
lean_dec(x_10);
return x_27;
}
}
}

363
stage0/stdlib/Init/Lean/Parser/Term.c
View file

@ -33,7 +33,6 @@ lean_object* l_Lean_Parser_Term_not;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_Parser_Term_letIdDecl;
lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_charLit___closed__1;
lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_iff(lean_object*);
@ -189,6 +188,7 @@ lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_lt(lean_object*);
lean_object* l_Lean_Parser_Term_explicitUniv;
extern lean_object* l_Int_repr___closed__1;
lean_object* l_Lean_Parser_charLit(uint8_t);
lean_object* l_Lean_Parser_Term_bnot___closed__1;
lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_inaccessible___closed__4;
@ -470,7 +470,6 @@ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__9;
lean_object* l_Lean_Parser_Term_prod___closed__3;
lean_object* l_Lean_Parser_Term_doId___closed__4;
lean_object* l_Lean_Parser_Term_lt___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_strLit___closed__1;
lean_object* l_Lean_Parser_darrow___elambda__1___rarg___closed__8;
lean_object* l_Lean_Parser_Term_pow___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_uminus___closed__7;
@ -530,7 +529,6 @@ lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_sorry(lean_object*);
lean_object* l_Lean_Parser_Term_nomatch___closed__4;
extern lean_object* l_Lean_Parser_numLit___closed__1;
lean_object* l_Lean_Parser_Term_or___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_listLit___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_ge___closed__1;
@ -551,6 +549,7 @@ lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__3;
lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object*);
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___closed__1;
lean_object* l_Lean_Parser_Term_str___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_listLit___closed__6;
lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_paren___closed__1;
@ -905,6 +904,7 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1(lean_object*, lean_object*, lea
lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_letEqns___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_char___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_cdot___closed__5;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_tupleTail___elambda__1___spec__1(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_num___closed__1;
@ -943,6 +943,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__2;
lean_object* l_Lean_Parser_Term_match___closed__2;
lean_object* l_Lean_Parser_Term_binderIdent___closed__2;
extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_append___closed__1;
@ -1519,7 +1520,6 @@ lean_object* l_Lean_Parser_Term_binderType___closed__4;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_bne___closed__2;
lean_object* l_Lean_Parser_strLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_where___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_subtype___closed__10;
lean_object* l_Lean_Parser_Term_append___elambda__1(lean_object*, lean_object*, lean_object*);
@ -1832,7 +1832,6 @@ lean_object* l_Lean_Parser_Term_antiquot___closed__1;
lean_object* l_Lean_Parser_Term_doPat___closed__5;
lean_object* l_Lean_Parser_categoryParser___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__4;
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_binderDefault___closed__3;
lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__5;
@ -1841,7 +1840,6 @@ lean_object* l_Lean_Parser_Term_structInst___closed__11;
lean_object* l_Lean_Parser_Term_mapConstRev___closed__1;
lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__8;
lean_object* l_Lean_Parser_charLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_do___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_letDecl___closed__3;
@ -1891,6 +1889,7 @@ extern lean_object* l_addParenHeuristic___closed__1;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_instBinder___closed__6;
lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__7;
lean_object* l_Lean_Parser_strLit(uint8_t);
lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_char___elambda__1___closed__1;
@ -3866,61 +3865,69 @@ return x_5;
lean_object* l_Lean_Parser_Term_num___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Term_num___elambda__1___closed__3;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Term_num___elambda__1___closed__3;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
lean_inc(x_2);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_2);
lean_inc(x_1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
return x_9;
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_numLitFn___rarg(x_2, x_14);
x_18 = l_Lean_Parser_Term_num___elambda__1___closed__1;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_16);
x_20 = l_Lean_Parser_mergeOrElseErrors(x_19, x_11, x_8);
lean_dec(x_8);
return x_20;
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
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;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = l_Lean_Parser_Term_num___elambda__1___closed__1;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_18);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_10);
lean_dec(x_10);
return x_22;
}
}
}
@ -3928,11 +3935,13 @@ return x_20;
lean_object* _init_l_Lean_Parser_Term_num___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_num___elambda__1___closed__1;
x_2 = l_Lean_Parser_numLit___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Level_num___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_num___elambda__1___closed__1;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_num___closed__2() {
@ -4027,64 +4036,81 @@ x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_str___elambda__1___closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = l_Lean_Parser_strLit(x_1);
return x_2;
}
}
lean_object* l_Lean_Parser_Term_str___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Term_str___elambda__1___closed__4;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
lean_inc(x_2);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_2);
lean_inc(x_1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
return x_9;
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_strLitFn___rarg(x_2, x_14);
x_18 = l_Lean_Parser_Term_str___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_16);
x_20 = l_Lean_Parser_mergeOrElseErrors(x_19, x_11, x_8);
lean_dec(x_8);
return x_20;
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
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;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = l_Lean_Parser_Term_str___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_18);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_10);
lean_dec(x_10);
return x_22;
}
}
}
@ -4092,11 +4118,13 @@ return x_20;
lean_object* _init_l_Lean_Parser_Term_str___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_str___elambda__1___closed__2;
x_2 = l_Lean_Parser_strLit___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_str___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_str___elambda__1___closed__2;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_str___closed__2() {
@ -4191,64 +4219,81 @@ x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_char___elambda__1___closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = l_Lean_Parser_charLit(x_1);
return x_2;
}
}
lean_object* l_Lean_Parser_Term_char___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Term_char___elambda__1___closed__4;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Term_char___elambda__1___closed__5;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
x_6 = l_Lean_Parser_Term_char___elambda__1___closed__4;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
lean_inc(x_2);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_2);
lean_inc(x_1);
x_11 = lean_apply_3(x_7, x_1, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
return x_9;
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_charLitFn___rarg(x_2, x_14);
x_18 = l_Lean_Parser_Term_char___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_16);
x_20 = l_Lean_Parser_mergeOrElseErrors(x_19, x_11, x_8);
lean_dec(x_8);
return x_20;
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_10);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
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;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = l_Lean_Parser_Term_char___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_18);
x_22 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_10);
lean_dec(x_10);
return x_22;
}
}
}
@ -4256,11 +4301,13 @@ return x_20;
lean_object* _init_l_Lean_Parser_Term_char___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_char___elambda__1___closed__2;
x_2 = l_Lean_Parser_charLit___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_char___elambda__1___closed__5;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_char___elambda__1___closed__2;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_char___closed__2() {
@ -37355,6 +37402,8 @@ l_Lean_Parser_Term_str___elambda__1___closed__3 = _init_l_Lean_Parser_Term_str__
lean_mark_persistent(l_Lean_Parser_Term_str___elambda__1___closed__3);
l_Lean_Parser_Term_str___elambda__1___closed__4 = _init_l_Lean_Parser_Term_str___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_str___elambda__1___closed__4);
l_Lean_Parser_Term_str___elambda__1___closed__5 = _init_l_Lean_Parser_Term_str___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_str___elambda__1___closed__5);
l_Lean_Parser_Term_str___closed__1 = _init_l_Lean_Parser_Term_str___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_str___closed__1);
l_Lean_Parser_Term_str___closed__2 = _init_l_Lean_Parser_Term_str___closed__2();
@ -37376,6 +37425,8 @@ l_Lean_Parser_Term_char___elambda__1___closed__3 = _init_l_Lean_Parser_Term_char
lean_mark_persistent(l_Lean_Parser_Term_char___elambda__1___closed__3);
l_Lean_Parser_Term_char___elambda__1___closed__4 = _init_l_Lean_Parser_Term_char___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_char___elambda__1___closed__4);
l_Lean_Parser_Term_char___elambda__1___closed__5 = _init_l_Lean_Parser_Term_char___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_char___elambda__1___closed__5);
l_Lean_Parser_Term_char___closed__1 = _init_l_Lean_Parser_Term_char___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_char___closed__1);
l_Lean_Parser_Term_char___closed__2 = _init_l_Lean_Parser_Term_char___closed__2();

1790
stage0/stdlib/Init/Lean/Syntax.c
View file

File diff suppressed because it is too large Load diff

1936
stage0/stdlib/Init/LeanInit.c
View file

File diff suppressed because it is too large Load diff