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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-24 19:36:58 -07:00
parent c76820a251
commit cf734814fd
36 changed files with 14540 additions and 14282 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
stage0/src/Init/Prelude.lean generated
View file

@ -2026,11 +2026,9 @@ def maxRecDepthErrorMessage : String :=
namespace Macro
/- References -/
constant MethodsRefPointed : PointedType.{0}
private constant MethodsRefPointed : PointedType.{0}
def MethodsRef : Type := MethodsRefPointed.type
instance : Inhabited MethodsRef where
default := MethodsRefPointed.val
private def MethodsRef : Type := MethodsRefPointed.type
structure Context where
methods : MethodsRef
@ -2102,7 +2100,10 @@ unsafe def mkMethodsImp (methods : Methods) : MethodsRef :=
unsafeCast methods
@[implementedBy mkMethodsImp]
constant mkMethods (methods : Methods) : MethodsRef
constant mkMethods (methods : Methods) : MethodsRef := MethodsRefPointed.val
instance : Inhabited MethodsRef where
default := mkMethods arbitrary
unsafe def getMethodsImp : MacroM Methods :=
bind read fun ctx => pure (unsafeCast (ctx.methods))

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

@ -30,12 +30,12 @@ instance : Inhabited Attribute where
attrKind := leading_parser optional («scoped» <|> «local»)
```
-/
def toAttributeKind [Monad m] [MonadResolveName m] [MonadError m] (attrKindStx : Syntax) : m AttributeKind := do
def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
if attrKindStx[0].isNone then
return AttributeKind.global
else if attrKindStx[0][0].getKind == ``Lean.Parser.Term.scoped then
if (← getCurrNamespace).isAnonymous then
throwError "scoped attributes must be used inside namespaces"
if (← Macro.getCurrNamespace).isAnonymous then
throw <| Macro.Exception.error (← getRef) "scoped attributes must be used inside namespaces"
return AttributeKind.scoped
else
return AttributeKind.local
@ -45,7 +45,7 @@ def mkAttrKindGlobal : Syntax :=
def elabAttr {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (attrInstance : Syntax) : m Attribute := do
/- attrInstance := ppGroup $ leading_parser attrKind >> attrParser -/
let attrKind ← toAttributeKind attrInstance[0]
let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
let attr := attrInstance[1]
let attr ← liftMacroM <| expandMacros attr
let attrName ←

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

@ -120,7 +120,7 @@ partial def main (type : Syntax) : CommandElabM Name := do
if str.isEmpty then
mkFreshInstanceName
else
mkUnusedBaseName <| Name.mkSimple ("inst" ++ str)
liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ str)
end MkInstanceName
@ -139,7 +139,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
let attrKind ← toAttributeKind stx[0]
let attrKind ← liftMacroM <| toAttributeKind stx[0]
let prio ← liftMacroM <| expandOptNamedPrio stx[2]
let attrStx ← `(attr| instance $(quote prio):numLit)
let (binders, type) := expandDeclSig stx[4]

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

@ -37,10 +37,40 @@ private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
k == ``Lean.Parser.Term.termTry ||
k == ``Lean.Parser.Term.termFor
/-- Given `stx` which is a `letPatDecl`, `letEqnsDecl`, or `letIdDecl`, return true if it has binders. -/
private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
let k := letDeclArg.getKind
if k == ``Lean.Parser.Term.letPatDecl then
false
else if k == ``Lean.Parser.Term.letEqnsDecl then
true
else if k == ``Lean.Parser.Term.letIdDecl then
-- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
let binders := letDeclArg[1]
binders.getNumArgs > 0
else
false
/-- Return `true` if the given `letDecl` contains binders. -/
private def letDeclHasBinders (letDecl : Syntax) : Bool :=
letDeclArgHasBinders letDecl[0]
/-- Return true if we should generate an error message when lifting a method over this kind of syntax. -/
private def liftMethodForbiddenBinder (k : SyntaxNodeKind) : Bool :=
k == ``Lean.Parser.Term.fun ||
k == ``Lean.Parser.Term.matchAlts
private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
let k := stx.getKind
if k == ``Lean.Parser.Term.fun || k == ``Lean.Parser.Term.matchAlts ||
k == ``Lean.Parser.Term.doLetRec || k == ``Lean.Parser.Term.letrec then
-- It is never ok to lift over this kind of binder
true
-- The following kinds of `let`-expressions require extra checks to decide whether they contain binders or not
else if k == ``Lean.Parser.Term.let then
letDeclHasBinders stx[1]
else if k == ``Lean.Parser.Term.doLet then
letDeclHasBinders stx[2]
else if k == ``Lean.Parser.Term.doLetArrow then
letDeclArgHasBinders stx[2]
else
false
private partial def hasLiftMethod : Syntax → Bool
| Syntax.node k args =>
@ -1138,7 +1168,7 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
return stx
else if k == `Lean.Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
if inBinder then
Macro.throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun` or `match`-alternative, and it can often be fixed by adding a missing `do`"
Macro.throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"
let term := args[1]
let term ← expandLiftMethodAux inQuot inBinder term
let auxDoElem ← `(doElem| let a ← $term:term)
@ -1146,7 +1176,7 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
`(a)
else do
let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
let inBinder := inBinder || (!inQuot && liftMethodForbiddenBinder k)
let inBinder := inBinder || (!inQuot && liftMethodForbiddenBinder stx)
let args ← args.mapM (expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder)
return Syntax.node k args
| stx => pure stx

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

@ -240,7 +240,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
```
It generates the names `term_+_` and `term[_,]`
-/
partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : CommandElabM Name :=
partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : MacroM Name := do
mkUnusedBaseName <| Name.mkSimple <| appendCatName <| visit stx ""
where
visit (stx : Syntax) (acc : String) : String :=
@ -295,7 +295,7 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
| none => precDefault
let name ← match name? with
| some name => pure name.getId
| none => mkNameFromParserSyntax cat syntaxParser
| none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
let prio ← liftMacroM <| evalOptPrio prio?
let stxNodeKind := (← getCurrNamespace) ++ name
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
@ -422,14 +422,14 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
| stx => stx
/- Convert `notation` command lhs item into a `syntax` command item -/
def expandNotationItemIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term, stx[1]]
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
throwUnsupportedSyntax
Macro.throwUnsupported
def strLitToPattern (stx: Syntax) : MacroM Syntax :=
match stx.isStrLit? with
@ -437,22 +437,22 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
| none => Macro.throwUnsupported
/- Convert `notation` command lhs item into a pattern element -/
def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax :=
def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
mkAntiquotNode stx[0]
else if k == strLitKind then
liftMacroM <| strLitToPattern stx
strLitToPattern stx
else
throwUnsupportedSyntax
Macro.throwUnsupported
/-- Try to derive a `SimpleDelab` from a notation.
The notation must be of the form `notation ... => c var_1 ... var_n`
where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/
def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax := do
def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do
match qrhs with
| `($c:ident $args*) =>
let [(c, [])] ← resolveGlobalName c.getId | failure
let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
guard <| args.allDiff
-- replace head constant with (unused) antiquotation so we're not dependent on the exact pretty printing of the head
@ -461,13 +461,13 @@ def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax)
| `($qrhs) => `($pat)
| _ => throw ())
| `($c:ident) =>
let [(c, [])] ← resolveGlobalName c.getId | failure
let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
`(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun _ => `($pat))
| _ => failure
private def expandNotationAux (ref : Syntax)
(currNamespace : Name) (attrKind : Syntax) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
let prio ← liftMacroM <| evalOptPrio prio?
(currNamespace : Name) (attrKind : Syntax) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do
let prio ← evalOptPrio prio?
-- build parser
let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
let cat := mkIdentFrom ref `term
@ -490,15 +490,12 @@ private def expandNotationAux (ref : Syntax)
| some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
| none => mkNullNode #[stxDecl, macroDecl]
@[builtinCommandElab «notation»] def expandNotation : CommandElab :=
adaptExpander fun stx => do
let currNamespace ← getCurrNamespace
match stx with
| `($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) =>
-- trigger scoped checks early and only once
let _ ← toAttributeKind attrKind
expandNotationAux stx currNamespace attrKind prec? name? prio? items rhs
| _ => throwUnsupportedSyntax
@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro
| stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
-- trigger scoped checks early and only once
let _ ← toAttributeKind attrKind
expandNotationAux stx (← Macro.getCurrNamespace) attrKind prec? name? prio? items rhs
| _ => Macro.throwUnsupported
/- Convert `macro` argument into a `syntax` command item -/
def expandMacroArgIntoSyntaxItem : Macro
@ -531,28 +528,28 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do
/- «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/
def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro := fun stx => do
let attrKind := stx[0]
let prec := stx[2].getOptional?
let name? ← liftMacroM <| expandOptNamedName stx[3]
let prio ← liftMacroM <| expandOptNamedPrio stx[4]
let name? ← expandOptNamedName stx[3]
let prio ← expandOptNamedPrio stx[4]
let head := stx[5]
let args := stx[6].getArgs
let cat := stx[8]
-- build parser
let stxPart ← liftMacroM <| expandMacroArgIntoSyntaxItem head
let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
let stxPart ← expandMacroArgIntoSyntaxItem head
let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
let stxParts := #[stxPart] ++ stxParts
-- name
let name ← match name? with
| some name => pure name
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build macro rules
let patHead ← liftMacroM <| expandMacroArgIntoPattern head
let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
let patHead ← expandMacroArgIntoPattern head
let patArgs ← args.mapM expandMacroArgIntoPattern
/- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs)
let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) (#[patHead] ++ patArgs)
if stx.getArgs.size == 11 then
-- `stx` is of the form `macro $head $args* : $cat => term`
let rhs := stx[10]
@ -566,10 +563,6 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d
let macroRulesCmd ← `(macro_rules | `($pat) => `($rhsBody))
return mkNullNode #[stxCmd, macroRulesCmd]
@[builtinCommandElab «macro»] def elabMacro : CommandElab :=
adaptExpander fun stx => do
expandMacro (← getCurrNamespace) stx
builtin_initialize
registerTraceClass `Elab.syntax
@ -602,8 +595,8 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
-- name
let name ← match name? with
| some name => pure name
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build pattern for `martch_syntax
| none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build pattern for syntax `match`
let patHead ← liftMacroM <| expandMacroArgIntoPattern head
let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs)

13
stage0/src/Lean/Elab/Util.lean generated
View file

@ -182,17 +182,16 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
liftMacroM (x stx)
partial def mkUnusedBaseName [Monad m] [MonadEnv m] [MonadResolveName m] (baseName : Name) : m Name := do
let currNamespace ← getCurrNamespace
let env ← getEnv
if env.contains (currNamespace ++ baseName) then
let rec loop (idx : Nat) :=
partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
let currNamespace ← Macro.getCurrNamespace
if ← Macro.hasDecl (currNamespace ++ baseName) then
let rec loop (idx : Nat) := do
let name := baseName.appendIndexAfter idx
if env.contains (currNamespace ++ name) then
if ← Macro.hasDecl (currNamespace ++ name) then
loop (idx+1)
else
name
return loop 1
loop 1
else
return baseName

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

@ -244,6 +244,10 @@ def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : P
let stack := stack.push newNode
⟨stack, lhsPrec, pos, cache, err⟩
def setError (s : ParserState) (msg : String) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
def mkError (s : ParserState) (msg : String) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩

15
stage0/src/Lean/Parser/StrInterpolation.lean generated
View file

@ -15,7 +15,9 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
let rec parse (startPos : Nat) (c : ParserContext) (s : ParserState) : ParserState :=
let i := s.pos
if input.atEnd i then
s.mkUnexpectedErrorAt "unterminated string literal" startPos
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "unterminated string literal"
else
let curr := input.get i
let s := s.setPos (input.next i)
@ -29,8 +31,15 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
let s := p c s
if s.hasError then s
else
let pos := s.pos
andthenFn (satisfyFn (· == '}') "expected '}'") (parse pos) c s
let i := s.pos
let curr := input.get i
if curr == '}' then
let s := s.setPos (input.next i)
parse i c s
else
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "'}'"
else
parse startPos c s
let startPos := s.pos

40
stage0/stdlib/Init/Prelude.c generated
View file

@ -179,7 +179,6 @@ lean_object* l_Lean_instInhabitedParserDescr;
lean_object* l_instLTFin(lean_object*);
lean_object* l_EStateM_dummySave(lean_object*, lean_object*);
lean_object* l_instInhabitedOption(lean_object*);
lean_object* l_Lean_Macro_MethodsRefPointed;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Substring_bsize_match__1(lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -790,6 +789,7 @@ lean_object* l___private_Init_Prelude_0__Lean_assembleParts___closed__1;
lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Macro_instInhabitedMethods;
lean_object* l_instHOrElse___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_Macro_MethodsRefPointed;
lean_object* l_dite___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_String_utf8ByteSize___boxed(lean_object*);
lean_object* l_id___rarg(lean_object*);
@ -797,6 +797,7 @@ lean_object* l_Lean_interpolatedStrKind___closed__1;
lean_object* l_Monad_seqLeft___default___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_arbitrary(lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_simpMacroScopesAux_match__1(lean_object*);
lean_object* l_Lean_Macro_instInhabitedMethodsRef___closed__1;
lean_object* l_Eq_ndrec___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_getPos_x3f(lean_object*, uint8_t);
lean_object* lean_simp_macro_scopes(lean_object*);
@ -11140,15 +11141,7 @@ x_1 = l_Lean_maxRecDepthErrorMessage___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Macro_MethodsRefPointed() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Macro_instInhabitedMethodsRef() {
static lean_object* _init_l___private_Init_Prelude_0__Lean_Macro_MethodsRefPointed() {
_start:
{
lean_object* x_1;
@ -12090,6 +12083,23 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Macro_instInhabitedMethodsRef___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Macro_instInhabitedMethods___closed__5;
x_2 = x_1;
return x_2;
}
}
static lean_object* _init_l_Lean_Macro_instInhabitedMethodsRef() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Macro_instInhabitedMethodsRef___closed__1;
return x_1;
}
}
lean_object* l_Lean_Macro_getMethodsImp(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -12655,10 +12665,8 @@ l_Lean_maxRecDepthErrorMessage___closed__1 = _init_l_Lean_maxRecDepthErrorMessag
lean_mark_persistent(l_Lean_maxRecDepthErrorMessage___closed__1);
l_Lean_maxRecDepthErrorMessage = _init_l_Lean_maxRecDepthErrorMessage();
lean_mark_persistent(l_Lean_maxRecDepthErrorMessage);
l_Lean_Macro_MethodsRefPointed = _init_l_Lean_Macro_MethodsRefPointed();
lean_mark_persistent(l_Lean_Macro_MethodsRefPointed);
l_Lean_Macro_instInhabitedMethodsRef = _init_l_Lean_Macro_instInhabitedMethodsRef();
lean_mark_persistent(l_Lean_Macro_instInhabitedMethodsRef);
l___private_Init_Prelude_0__Lean_Macro_MethodsRefPointed = _init_l___private_Init_Prelude_0__Lean_Macro_MethodsRefPointed();
lean_mark_persistent(l___private_Init_Prelude_0__Lean_Macro_MethodsRefPointed);
l_Lean_Macro_Context_currRecDepth___default = _init_l_Lean_Macro_Context_currRecDepth___default();
lean_mark_persistent(l_Lean_Macro_Context_currRecDepth___default);
l_Lean_Macro_Context_maxRecDepth___default = _init_l_Lean_Macro_Context_maxRecDepth___default();
@ -12703,6 +12711,10 @@ l_Lean_Macro_instInhabitedMethods___closed__5 = _init_l_Lean_Macro_instInhabited
lean_mark_persistent(l_Lean_Macro_instInhabitedMethods___closed__5);
l_Lean_Macro_instInhabitedMethods = _init_l_Lean_Macro_instInhabitedMethods();
lean_mark_persistent(l_Lean_Macro_instInhabitedMethods);
l_Lean_Macro_instInhabitedMethodsRef___closed__1 = _init_l_Lean_Macro_instInhabitedMethodsRef___closed__1();
lean_mark_persistent(l_Lean_Macro_instInhabitedMethodsRef___closed__1);
l_Lean_Macro_instInhabitedMethodsRef = _init_l_Lean_Macro_instInhabitedMethodsRef();
lean_mark_persistent(l_Lean_Macro_instInhabitedMethodsRef);
l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__1 = _init_l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__1);
l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__2 = _init_l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__2();

4
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -434,6 +434,7 @@ extern lean_object* l_Lean_Elab_Term_termElabAttribute;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_App_0__Lean_Elab_Term_getSuccess___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFnId(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_LocalDecl_type(lean_object*);
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_hasOptAutoParams___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -467,7 +468,6 @@ extern lean_object* l_Lean_Elab_postponeExceptionId;
lean_object* l_Lean_throwError___at___private_Lean_Elab_App_0__Lean_Elab_Term_throwLValError___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures_match__1(lean_object*);
extern lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda__1___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_Term_expandArgs_match__2(lean_object*);
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandApp_match__1___rarg(lean_object*, lean_object*);
@ -5206,7 +5206,7 @@ static lean_object* _init_l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArg
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_myMacro____x40_Init_Notation___hyg_2278____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

987
stage0/stdlib/Lean/Elab/Attributes.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -333,6 +333,7 @@ extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_948___
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_getFunBinderIds_x3f___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__3;
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM;
@ -363,7 +364,6 @@ lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Binders_0__Lean_Elab_Term
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__10;
extern lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__1;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getBinderIds___boxed__const__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_quoteAutoTactic_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__6;
@ -2554,7 +2554,7 @@ static lean_object* _init_l_Lean_Elab_Term_declareTacticSyntax___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -22118,7 +22118,7 @@ static lean_object* _init_l_Lean_Elab_Term_elabLetDeclAux___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_myMacro____x40_Init_Notation___hyg_15449____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

6
stage0/stdlib/Lean/Elab/Command.c generated
View file

@ -667,6 +667,7 @@ lean_object* l_Lean_Elab_Command_addUnivLevel(lean_object*, lean_object*, lean_o
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedNameGenerator___closed__1;
extern lean_object* l_Lean_instInhabitedTraceState___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_List_drop___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadRecDepthCommandElabM___closed__4;
lean_object* l_Lean_Elab_Command_instMonadTraceCommandElabM___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -715,7 +716,6 @@ lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__6(lean_object*, lean_o
extern lean_object* l_Lean_Parser_Command_end___elambda__1___closed__1;
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1501____closed__1;
lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Command_elabEnd___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_Command_elabExport___closed__1;
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_instAddErrorMessageContextCommandElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce(lean_object*);
@ -9624,7 +9624,7 @@ static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_4162____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -13321,7 +13321,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabCommand___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Elab_Command_elabCommand___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

20
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -315,7 +315,6 @@ lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___at_Lean_Elab_Comm
lean_object* l_Lean_addDeclarationRanges___at_Lean_Elab_Command_elabAxiom___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__11___closed__2;
lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_elabMutualInductive___boxed__const__1;
lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualNamespace___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__4;
@ -378,6 +377,7 @@ lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__2___rarg(lean_obje
lean_object* l___regBuiltin_Lean_Elab_Command_elabAttr(lean_object*);
uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_Lean_Elab_Command_elabMutual___closed__1;
extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__20___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualElement___closed__1;
lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
@ -4030,7 +4030,6 @@ x_9 = x_4 < x_3;
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11;
lean_dec(x_7);
x_10 = x_5;
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
@ -4074,7 +4073,6 @@ lean_ctor_set(x_36, 3, x_33);
lean_ctor_set(x_36, 4, x_34);
lean_ctor_set(x_36, 5, x_35);
lean_ctor_set(x_36, 6, x_29);
lean_inc(x_7);
lean_inc(x_36);
x_37 = l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1(x_25, x_36, x_7, x_28);
lean_dec(x_25);
@ -4108,7 +4106,6 @@ else
{
uint8_t x_45;
lean_dec(x_14);
lean_dec(x_7);
x_45 = !lean_is_exclusive(x_42);
if (x_45 == 0)
{
@ -4154,7 +4151,6 @@ else
{
uint8_t x_54;
lean_dec(x_14);
lean_dec(x_7);
x_54 = !lean_is_exclusive(x_51);
if (x_54 == 0)
{
@ -4183,7 +4179,6 @@ lean_dec(x_23);
lean_dec(x_14);
x_58 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__8___closed__2;
x_59 = l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__6(x_58, x_36, x_7, x_39);
lean_dec(x_7);
x_60 = !lean_is_exclusive(x_59);
if (x_60 == 0)
{
@ -4211,7 +4206,6 @@ uint8_t x_64;
lean_dec(x_36);
lean_dec(x_23);
lean_dec(x_14);
lean_dec(x_7);
x_64 = !lean_is_exclusive(x_37);
if (x_64 == 0)
{
@ -4659,6 +4653,7 @@ lean_dec(x_3);
x_10 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_11 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__8(x_1, x_2, x_9, x_10, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_2);
lean_dec(x_1);
@ -4805,7 +4800,6 @@ if (lean_obj_tag(x_5) == 0)
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Syntax_getArg(x_1, x_6);
lean_inc(x_3);
lean_inc(x_2);
x_8 = l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1(x_7, x_2, x_3, x_4);
lean_dec(x_7);
@ -5202,7 +5196,6 @@ x_11 = lean_unsigned_to_nat(0u);
x_12 = lean_array_uset(x_3, x_2, x_11);
x_13 = x_10;
x_14 = l_Lean_Syntax_getArg(x_13, x_11);
lean_inc(x_5);
lean_inc(x_4);
x_15 = l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1(x_14, x_4, x_5, x_6);
lean_dec(x_14);
@ -7164,7 +7157,7 @@ lean_dec(x_13);
lean_dec(x_12);
x_30 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_30, 0, x_24);
x_31 = l_Lean_Elab_elabAttr___rarg___lambda__11___closed__2;
x_31 = l_Lean_Elab_elabAttr___rarg___lambda__20___closed__2;
x_32 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_30);
@ -7267,7 +7260,7 @@ lean_dec(x_49);
lean_dec(x_48);
x_67 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_67, 0, x_61);
x_68 = l_Lean_Elab_elabAttr___rarg___lambda__11___closed__2;
x_68 = l_Lean_Elab_elabAttr___rarg___lambda__20___closed__2;
x_69 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_67);
@ -7621,7 +7614,6 @@ lean_inc(x_15);
x_16 = lean_ctor_get(x_13, 1);
lean_inc(x_16);
lean_dec(x_13);
lean_inc(x_3);
lean_inc(x_2);
x_17 = l_Lean_Elab_elabAttrs___at_Lean_Elab_Command_elabMutualDef___spec__3(x_16, x_2, x_3, x_14);
lean_dec(x_16);
@ -7642,7 +7634,6 @@ x_24 = lean_usize_of_nat(x_23);
lean_dec(x_23);
x_25 = lean_box(0);
x_26 = l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__3(x_10, x_15, x_18, x_22, x_24, x_10, x_25, x_2, x_3, x_19);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_22);
if (lean_obj_tag(x_26) == 0)
@ -7696,7 +7687,6 @@ else
{
uint8_t x_35;
lean_dec(x_15);
lean_dec(x_3);
lean_dec(x_2);
x_35 = !lean_is_exclusive(x_17);
if (x_35 == 0)
@ -7721,7 +7711,6 @@ return x_38;
else
{
uint8_t x_39;
lean_dec(x_3);
lean_dec(x_2);
x_39 = !lean_is_exclusive(x_12);
if (x_39 == 0)
@ -7823,6 +7812,7 @@ _start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Command_elabAttr(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_5;
}

2653
stage0/stdlib/Lean/Elab/DefView.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/Deriving/Basic.c generated
View file

@ -94,6 +94,7 @@ size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_elabDeriving___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_DerivingClassView_applyHandlers(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Elab_applyDerivingHandlers___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_registerBuiltinDerivingHandler___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabNamespace___spec__1___rarg(lean_object*);
extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__1;
@ -102,7 +103,6 @@ lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
lean_object* l_Lean_throwError___at_Lean_Elab_elabDeriving___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logException___at_Lean_Elab_Command_runLinters___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_instAddErrorMessageContextCommandElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
@ -2215,7 +2215,7 @@ static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___h
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_595____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

4
stage0/stdlib/Lean/Elab/Deriving/Util.c generated
View file

@ -136,6 +136,7 @@ lean_object* l_Lean_Elab_Deriving_mkImplicitBinders___boxed__const__1;
extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5;
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_Elab_Deriving_mkInstanceCmds___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_Deriving_mkHeader(lean_object*);
lean_object* l_Lean_Elab_Deriving_mkContext_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -146,7 +147,6 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___privat
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_mkDiscrs___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_mkInductiveApp___spec__1(size_t, size_t, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__1;
lean_object* l_Lean_Elab_Deriving_explicitBinderF;
@ -1540,7 +1540,7 @@ static lean_object* _init_l_Lean_Elab_Deriving_mkContext___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Elab_Deriving_mkContext___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

381
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -192,6 +192,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__1;
size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Lean_Parser_Term_doIfLetBind___elambda__1___closed__1;
extern lean_object* l_Array_empty___closed__1;
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_19973____closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkDoIfView___boxed(lean_object*, lean_object*, lean_object*);
@ -272,6 +273,7 @@ extern lean_object* l_termDepIfThenElse___closed__7;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match__3(lean_object*);
lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__13;
lean_object* l_Array_sequenceMap_loop___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Do_mkJmp___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f___lambda__1(lean_object*);
@ -425,11 +427,11 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureInsideFor___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureInsideFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___spec__1___closed__4;
lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__4;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__29;
lean_object* l_Lean_Elab_Term_Do_getDoLetVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__14;
@ -765,6 +767,7 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_withNewMutableVars(lean_object*);
extern lean_object* l_Lean_nullKind___closed__2;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_19003____closed__3;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_checkLetArrowRHS___closed__2;
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___lambda__1___closed__2;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let__delayed___elambda__1___closed__1;
@ -797,6 +800,7 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__
uint8_t l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasExitPoint___spec__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_getPatternVarsEx___spec__1(size_t, size_t, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13376____closed__3;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_mkJmp___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkIdBindFor___closed__1;
lean_object* l_Lean_Elab_Term_Do_eraseOptVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -807,7 +811,7 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_toDoElem(lean_object*, l
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__5(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__15;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28839_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28926_(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__24;
lean_object* l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasTerminalAction___spec__1___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___lambda__1___closed__1;
@ -846,6 +850,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_CodeBlocl_toMessageDa
lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__10;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkIdBindFor___closed__2;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
lean_object* l_Lean_Elab_Term_Do_getDoLetRecVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Term_Do_ToTerm_Kind_isRegular(uint8_t);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_extendUpdatedVarsAux_update___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -866,7 +871,6 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__10;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_mkForInBody___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkPureUnitAction(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__31;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_Term_Do_ToTerm_reassignToTerm(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -983,6 +987,7 @@ lean_object* l_Lean_Elab_Term_Do_mkFreshJP___lambda__1___closed__1;
lean_object* l_Lean_Elab_Term_Do_mkIte_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_attachJP___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkMonadAlias___closed__3;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_Kind_isRegular_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode_match__1(lean_object*);
extern lean_object* l_Lean_Parser_Term_doContinue___elambda__1___closed__5;
@ -1510,24 +1515,208 @@ x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_liftMethodForbiddenBinder(lean_object* x_1) {
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_myMacro____x40_Init_Notation___hyg_13376____closed__10;
x_3 = lean_name_eq(x_1, x_2);
if (x_3 == 0)
lean_object* x_2; lean_object* x_3; uint8_t x_4;
lean_inc(x_1);
x_2 = l_Lean_Syntax_getKind(x_1);
x_3 = l_Lean_Parser_Term_letPatDecl___closed__2;
x_4 = lean_name_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_4; uint8_t x_5;
x_4 = l_myMacro____x40_Init_Notation___hyg_13978____closed__8;
x_5 = lean_name_eq(x_1, x_4);
return x_5;
lean_object* x_5; uint8_t x_6;
x_5 = l_Lean_Parser_Term_letEqnsDecl___closed__2;
x_6 = lean_name_eq(x_2, x_5);
if (x_6 == 0)
{
lean_object* x_7; uint8_t x_8;
x_7 = l_myMacro____x40_Init_Notation___hyg_15449____closed__6;
x_8 = lean_name_eq(x_2, x_7);
lean_dec(x_2);
if (x_8 == 0)
{
uint8_t x_9;
lean_dec(x_1);
x_9 = 0;
return x_9;
}
else
{
uint8_t x_6;
x_6 = 1;
return x_6;
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_10 = lean_unsigned_to_nat(1u);
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
lean_dec(x_1);
x_12 = l_Lean_Syntax_getNumArgs(x_11);
lean_dec(x_11);
x_13 = lean_unsigned_to_nat(0u);
x_14 = lean_nat_dec_lt(x_13, x_12);
lean_dec(x_12);
return x_14;
}
}
else
{
uint8_t x_15;
lean_dec(x_2);
lean_dec(x_1);
x_15 = 1;
return x_15;
}
}
else
{
uint8_t x_16;
lean_dec(x_2);
lean_dec(x_1);
x_16 = 0;
return x_16;
}
}
}
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
x_4 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders(x_3);
return x_4;
}
}
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_liftMethodForbiddenBinder(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
lean_inc(x_1);
x_2 = l_Lean_Syntax_getKind(x_1);
x_3 = l_myMacro____x40_Init_Notation___hyg_13376____closed__10;
x_4 = lean_name_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; uint8_t x_6;
x_5 = l_myMacro____x40_Init_Notation___hyg_13978____closed__8;
x_6 = lean_name_eq(x_2, x_5);
if (x_6 == 0)
{
lean_object* x_7; uint8_t x_8;
x_7 = l_Lean_Parser_Term_doLetRec___elambda__1___closed__2;
x_8 = lean_name_eq(x_2, x_7);
if (x_8 == 0)
{
lean_object* x_9; uint8_t x_10;
x_9 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_19973____closed__2;
x_10 = lean_name_eq(x_2, x_9);
if (x_10 == 0)
{
lean_object* x_11; uint8_t x_12;
x_11 = l_myMacro____x40_Init_Notation___hyg_15449____closed__2;
x_12 = lean_name_eq(x_2, x_11);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14;
x_13 = l_Lean_Parser_Term_doLet___elambda__1___closed__2;
x_14 = lean_name_eq(x_2, x_13);
if (x_14 == 0)
{
lean_object* x_15; uint8_t x_16;
x_15 = l_Lean_Parser_Term_doLetArrow___elambda__1___closed__2;
x_16 = lean_name_eq(x_2, x_15);
lean_dec(x_2);
if (x_16 == 0)
{
uint8_t x_17;
lean_dec(x_1);
x_17 = 0;
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_18 = lean_unsigned_to_nat(2u);
x_19 = l_Lean_Syntax_getArg(x_1, x_18);
lean_dec(x_1);
x_20 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclArgHasBinders(x_19);
return x_20;
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
lean_dec(x_2);
x_21 = lean_unsigned_to_nat(2u);
x_22 = l_Lean_Syntax_getArg(x_1, x_21);
lean_dec(x_1);
x_23 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders(x_22);
lean_dec(x_22);
return x_23;
}
}
else
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
lean_dec(x_2);
x_24 = lean_unsigned_to_nat(1u);
x_25 = l_Lean_Syntax_getArg(x_1, x_24);
lean_dec(x_1);
x_26 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_letDeclHasBinders(x_25);
lean_dec(x_25);
return x_26;
}
}
else
{
uint8_t x_27;
lean_dec(x_2);
lean_dec(x_1);
x_27 = 1;
return x_27;
}
}
else
{
uint8_t x_28;
lean_dec(x_2);
lean_dec(x_1);
x_28 = 1;
return x_28;
}
}
else
{
uint8_t x_29;
lean_dec(x_2);
lean_dec(x_1);
x_29 = 1;
return x_29;
}
}
else
{
uint8_t x_30;
lean_dec(x_2);
lean_dec(x_1);
x_30 = 1;
return x_30;
}
}
}
@ -1536,7 +1725,6 @@ _start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_liftMethodForbiddenBinder(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
@ -22584,7 +22772,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_3 = lean_unsigned_to_nat(724u);
x_3 = lean_unsigned_to_nat(754u);
x_4 = lean_unsigned_to_nat(13u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25134,7 +25322,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__17;
x_3 = lean_unsigned_to_nat(843u);
x_3 = lean_unsigned_to_nat(873u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -26746,7 +26934,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(852u);
x_3 = lean_unsigned_to_nat(882u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -26972,7 +27160,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(856u);
x_3 = lean_unsigned_to_nat(886u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28139,7 +28327,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(864u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28217,7 +28405,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(868u);
x_3 = lean_unsigned_to_nat(898u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -29432,7 +29620,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5;
x_3 = lean_unsigned_to_nat(879u);
x_3 = lean_unsigned_to_nat(909u);
x_4 = lean_unsigned_to_nat(28u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -40603,7 +40791,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_mkNestedKind___closed__1;
x_3 = lean_unsigned_to_nat(1026u);
x_3 = lean_unsigned_to_nat(1056u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -40796,7 +40984,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__3;
x_3 = lean_unsigned_to_nat(1082u);
x_3 = lean_unsigned_to_nat(1112u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -47329,80 +47517,83 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_T
return x_2;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
uint8_t x_9; uint8_t x_10; uint8_t x_11;
x_9 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_liftMethodForbiddenBinder(x_2);
x_10 = l_Lean_Syntax_isQuot(x_1);
x_11 = x_4 < x_3;
if (x_11 == 0)
uint8_t x_8; uint8_t x_9; uint8_t x_10;
lean_inc(x_1);
x_8 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_liftMethodForbiddenBinder(x_1);
x_9 = l_Lean_Syntax_isQuot(x_1);
x_10 = x_3 < x_2;
if (x_10 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_7);
x_12 = x_5;
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_6);
lean_dec(x_1);
x_11 = x_4;
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_5);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_6);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_8);
return x_14;
lean_ctor_set(x_13, 1, x_7);
return x_13;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_15 = lean_array_uget(x_5, x_4);
x_16 = lean_unsigned_to_nat(0u);
x_17 = lean_array_uset(x_5, x_4, x_16);
x_18 = x_15;
lean_inc(x_7);
x_19 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux(x_10, x_9, x_18, x_6, x_7, x_8);
if (lean_obj_tag(x_19) == 0)
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_array_uget(x_4, x_3);
x_15 = lean_unsigned_to_nat(0u);
x_16 = lean_array_uset(x_4, x_3, x_15);
x_17 = x_14;
lean_inc(x_6);
x_18 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux(x_9, x_8, x_17, x_5, x_6, x_7);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27;
x_20 = lean_ctor_get(x_19, 0);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; size_t x_24; lean_object* x_25; lean_object* x_26;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_dec(x_18);
x_21 = lean_ctor_get(x_19, 0);
lean_inc(x_21);
lean_dec(x_19);
x_22 = lean_ctor_get(x_20, 0);
x_22 = lean_ctor_get(x_19, 1);
lean_inc(x_22);
x_23 = lean_ctor_get(x_20, 1);
lean_inc(x_23);
lean_dec(x_20);
x_24 = 1;
x_25 = x_4 + x_24;
x_26 = x_22;
x_27 = lean_array_uset(x_17, x_4, x_26);
x_4 = x_25;
x_5 = x_27;
x_6 = x_23;
x_8 = x_21;
lean_dec(x_19);
x_23 = 1;
x_24 = x_3 + x_23;
x_25 = x_21;
x_26 = lean_array_uset(x_16, x_3, x_25);
x_3 = x_24;
x_4 = x_26;
x_5 = x_22;
x_7 = x_20;
goto _start;
}
else
{
uint8_t x_29;
lean_dec(x_17);
lean_dec(x_7);
x_29 = !lean_is_exclusive(x_19);
if (x_29 == 0)
uint8_t x_28;
lean_dec(x_16);
lean_dec(x_6);
lean_dec(x_1);
x_28 = !lean_is_exclusive(x_18);
if (x_28 == 0)
{
return x_19;
return x_18;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_19, 0);
x_31 = lean_ctor_get(x_19, 1);
lean_inc(x_31);
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_18, 0);
x_30 = lean_ctor_get(x_18, 1);
lean_inc(x_30);
lean_dec(x_19);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
return x_32;
lean_inc(x_29);
lean_dec(x_18);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
}
}
@ -48013,7 +48204,7 @@ static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBl
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun` or `match`-alternative, and it can often be fixed by adding a missing `do`");
x_1 = lean_mk_string("cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`");
return x_1;
}
}
@ -48415,14 +48606,12 @@ if (x_1 == 0)
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_15 = lean_box_usize(x_12);
x_16 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___boxed__const__1;
lean_inc(x_7);
lean_inc(x_3);
x_17 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed), 8, 5);
x_17 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed), 7, 4);
lean_closure_set(x_17, 0, x_3);
lean_closure_set(x_17, 1, x_7);
lean_closure_set(x_17, 2, x_15);
lean_closure_set(x_17, 3, x_16);
lean_closure_set(x_17, 4, x_13);
lean_closure_set(x_17, 1, x_15);
lean_closure_set(x_17, 2, x_16);
lean_closure_set(x_17, 3, x_13);
x_18 = !lean_is_exclusive(x_3);
if (x_18 == 0)
{
@ -49598,18 +49787,16 @@ return x_361;
}
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
size_t x_9; size_t x_10; lean_object* x_11;
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_9 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_10 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_11 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(x_1, x_2, x_9, x_10, x_5, x_6, x_7, x_8);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__1(x_1, x_8, x_9, x_4, x_5, x_6, x_7);
return x_10;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethodAux___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
@ -69964,7 +70151,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_elabDo___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -70483,7 +70670,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28839_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28926_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -71474,7 +71661,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Do_elabDo___closed__1);
res = l___regBuiltin_Lean_Elab_Term_Do_elabDo(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28839_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28926_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1();

4
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

@ -371,6 +371,7 @@ lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_elab
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkHeaders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_mod(size_t, size_t);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_getResultingUniverse___closed__3;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_Command_shouldInferResultUniverse_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectLevelParamsInInductive(lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabHeaderAux___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -408,7 +409,6 @@ lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkIndFVar2Cons
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkParamsAndResultType___lambda__1___closed__3;
lean_object* l_Lean_Meta_transform_visit_visitForall___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_checkParamOccs___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_expandCoe___closed__2;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___spec__6___lambda__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_elabCtorType___lambda__3___closed__2;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -592,7 +592,7 @@ static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_Command_inductive___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

1207
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/Log.c generated
View file

@ -78,13 +78,13 @@ lean_object* l_Lean_Elab_log___rarg(lean_object*, lean_object*, lean_object*, le
lean_object* l_Lean_Elab_logWarning___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logAt___rarg___lambda__8(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logDbgTrace(lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_logAt___rarg___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
lean_object* l_Lean_Elab_trace___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logAt___rarg___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logAt___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda__1___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_logAt___rarg___lambda__7(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logException_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getRefPos(lean_object*);
@ -1269,7 +1269,7 @@ static lean_object* _init_l_Lean_Elab_logDbgTrace___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_742____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

4
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -616,6 +616,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_waitExpectedType(lean
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandMacrosInPatterns___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_type(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___lambda__1___closed__2;
@ -681,7 +682,6 @@ extern lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda_
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__10;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_quotedNameToPattern___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_withElaboratedLHS___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkLocalDeclFor_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_ToDepElimPattern_main___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1234,7 +1234,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_Matc
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_myMacro____x40_Init_Notation___hyg_13978____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

797
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

File diff suppressed because it is too large Load diff

12
stage0/stdlib/Lean/Elab/PreDefinition/Main.c generated
View file

@ -94,8 +94,8 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_mkHashMapImp___rarg(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
size_t l_Lean_Name_hash(lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
lean_object* l_Std_AssocList_replace___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__16(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_collectMVarsAtPreDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
@ -473,7 +473,7 @@ lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean
x_43 = lean_ctor_get(x_37, 1);
lean_inc(x_43);
lean_dec(x_37);
x_44 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_44 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
x_45 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_44, x_2, x_3, x_4, x_5, x_6, x_7, x_43);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
@ -491,7 +491,7 @@ block_24:
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_1, 4);
lean_inc(x_10);
x_11 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_11 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
lean_inc(x_10);
x_12 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__1___boxed), 12, 3);
lean_closure_set(x_12, 0, x_1);
@ -569,7 +569,7 @@ x_31 = l_Lean_KernelException_toMessageData___closed__15;
x_32 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
x_33 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_33 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
x_34 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_33, x_32, x_2, x_3, x_4, x_5, x_6, x_7, x_26);
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
@ -2845,7 +2845,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -3527,7 +3527,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8___lambda__3___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

4
stage0/stdlib/Lean/Elab/PreDefinition/Structural.c generated
View file

@ -225,6 +225,7 @@ uint8_t l_Lean_Expr_isHeadBetaTarget(lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_toBelowAux___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_ensureNoRecFn___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_findRecArg_loop___rarg___closed__10;
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_replaceRecApps_loop___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_throwStructuralFailed___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_findRecArg_loop___spec__4(lean_object*);
@ -233,7 +234,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structu
extern lean_object* l_Lean_Core_betaReduce___closed__2;
lean_object* l_Lean_Meta_decLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__6___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
lean_object* l_Lean_throwError___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_findRecArg_loop___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Structural_State_matcherBelowDep___default;
@ -5884,7 +5884,7 @@ static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_0__Lean
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1200____closed__2;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1204____closed__2;
x_2 = l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_toBelowAux___closed__10;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

4
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -615,6 +615,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lea
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___lambda__1___closed__11;
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__3(lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__29;
lean_object* l_Lean_Elab_Term_Quotation_myMacro____x40_Lean_Elab_Quotation___hyg_3801____closed__10;
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_4261____closed__1;
@ -688,7 +689,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compile
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__10;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__18;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___lambda__1___closed__21;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__20;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__30;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__15___closed__10;
@ -31563,7 +31563,7 @@ static lean_object* _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quot
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

4
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -438,6 +438,7 @@ lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName_throwUnknownExpectedType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_fmt___at_Lean_Level_PP_Result_format___spec__1(lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_List_foldlM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_groupKind;
uint8_t l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___lambda__1(lean_object*);
@ -477,7 +478,6 @@ lean_object* l_List_map___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_St
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__4;
lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields___spec__3___closed__4;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
uint8_t l_Lean_Expr_isMVar(lean_object*);
extern lean_object* l_Id_instMonadId;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_groupFields_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -2865,7 +2865,7 @@ static lean_object* _init_l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_Str
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

1742
stage0/stdlib/Lean/Elab/Structure.c generated
View file

File diff suppressed because it is too large Load diff

20132
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Elab/SyntheticMVars.c generated
View file

@ -188,6 +188,7 @@ lean_object* l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_E
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_getSomeSynthethicMVarsRef_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_runTactic___closed__1;
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizePendingInstMVar___lambda__1___closed__2;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance_match__1___rarg(lean_object*, lean_object*);
extern uint8_t l_Lean_instInhabitedBinderInfo;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVarsUsingDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -206,7 +207,6 @@ lean_object* l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_E
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_reportStuckSyntheticMVars_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizePendingInstMVar___closed__1;
extern lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_SavedState_restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3203,7 +3203,7 @@ static lean_object* _init_l_Lean_commitWhenSome_x3f___at___private_Lean_Elab_Syn
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Meta_SynthInstance_resume___closed__4;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -8515,7 +8515,7 @@ static lean_object* _init_l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -8671,7 +8671,7 @@ x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
x_29 = l_List_reverse___rarg(x_16);
x_30 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_30 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_inc(x_8);
lean_inc(x_4);
x_31 = l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___spec__1(x_1, x_2, x_30, x_29, x_26, x_3, x_4, x_5, x_6, x_7, x_8, x_28);
@ -8890,7 +8890,7 @@ x_91 = lean_ctor_get(x_90, 1);
lean_inc(x_91);
lean_dec(x_90);
x_92 = l_List_reverse___rarg(x_16);
x_93 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_93 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_inc(x_8);
lean_inc(x_4);
x_94 = l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___spec__1(x_1, x_2, x_93, x_92, x_88, x_3, x_4, x_5, x_6, x_7, x_8, x_91);

16
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -267,7 +267,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalOpen___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_getOptRotation___boxed(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalOpen___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l_Array_qsort_sort___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___spec__1___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -314,6 +313,7 @@ lean_object* l_Lean_Elab_Tactic_orElse___rarg(lean_object*, lean_object*, lean_o
lean_object* l_Lean_Elab_Tactic_evalIntro_introStep_match__1___rarg(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__11;
lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Tactic_evalOpen___spec__9(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_intros___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSkip(lean_object*);
@ -471,6 +471,7 @@ lean_object* l_Lean_resolveNamespace___at_Lean_Elab_Tactic_evalOpen___spec__5(le
lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalClear___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Elab_Tactic_getNameOfIdent_x27___boxed(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalIntros___closed__2;
lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -527,7 +528,6 @@ lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_getResetInfoTrees___at_
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13978____closed__10;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalTacticAux___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars___closed__2;
lean_object* l_List_rotateRight___rarg(lean_object*, lean_object*);
@ -4180,7 +4180,7 @@ lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; uint
x_55 = lean_ctor_get(x_50, 1);
lean_inc(x_55);
lean_dec(x_50);
x_56 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_56 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_57 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_56, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_55);
x_58 = lean_ctor_get(x_57, 0);
lean_inc(x_58);
@ -4417,7 +4417,7 @@ lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122;
x_119 = lean_ctor_get(x_114, 1);
lean_inc(x_119);
lean_dec(x_114);
x_120 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_120 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_121 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_120, x_4, x_5, x_92, x_7, x_8, x_9, x_10, x_11, x_119);
x_122 = lean_ctor_get(x_121, 0);
lean_inc(x_122);
@ -4674,7 +4674,7 @@ lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188;
x_185 = lean_ctor_get(x_180, 1);
lean_inc(x_185);
lean_dec(x_180);
x_186 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_186 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_187 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_186, x_4, x_5, x_158, x_7, x_8, x_9, x_10, x_11, x_185);
x_188 = lean_ctor_get(x_187, 0);
lean_inc(x_188);
@ -4957,7 +4957,7 @@ lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264;
x_261 = lean_ctor_get(x_256, 1);
lean_inc(x_261);
lean_dec(x_256);
x_262 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_262 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_263 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_262, x_4, x_5, x_234, x_7, x_8, x_9, x_10, x_11, x_261);
x_264 = lean_ctor_get(x_263, 0);
lean_inc(x_264);
@ -5293,7 +5293,7 @@ lean_object* x_349; lean_object* x_350; lean_object* x_351; lean_object* x_352;
x_349 = lean_ctor_get(x_344, 1);
lean_inc(x_349);
lean_dec(x_344);
x_350 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_350 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_351 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_350, x_4, x_5, x_322, x_7, x_8, x_9, x_296, x_11, x_349);
x_352 = lean_ctor_get(x_351, 0);
lean_inc(x_352);
@ -24057,7 +24057,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basi
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e_____closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

6
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

@ -322,6 +322,7 @@ lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType(lean_object*, lean_object*,
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getFType___boxed(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalCases___lambda__2___boxed(lean_object**);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -345,7 +346,6 @@ lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0_
extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
lean_object* l_Lean_Expr_bindingName_x21(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalCases___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_ElimApp_evalAlts___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_hasArgs(lean_object*);
lean_object* l_Lean_resolveGlobalConst___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7364,7 +7364,7 @@ static lean_object* _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Ta
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_Tactic_induction___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -12537,7 +12537,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Indu
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_Tactic_cases___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

20
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -532,7 +532,6 @@ lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_elabCompletion___spec__1(le
lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Level_normLtAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr_mkMessage___lambda__2___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_LVal_isFieldName_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -628,6 +627,7 @@ lean_object* l_List_forIn_loop___at_Lean_Elab_Term_logUnassignedUsingErrorInfos_
uint8_t l_Lean_Level_any(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___closed__4;
lean_object* l_Lean_mkAnnotation(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
extern lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg___closed__2;
lean_object* l_Lean_Elab_log___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicit(lean_object*);
@ -968,6 +968,7 @@ lean_object* l_List_foldr___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwS
lean_object* l_Lean_Elab_Term_mkNoImplicitLambdaAnnotation___closed__1;
lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveId_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_resolveNamespace___at_Lean_Elab_Term_elabOpen___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM;
lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_traceAtCmdPos___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1060,7 +1061,6 @@ lean_object* l_Lean_Elab_elabSetOption___at_Lean_Elab_Term_elabSetOption___spec_
lean_object* l_List_mapM___at_Lean_Elab_Term_resolveName_x27___spec__6___closed__1;
lean_object* l_Lean_Elab_Term_elabScientificLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l_Lean_Elab_Term_mkFreshIdent___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -9825,7 +9825,7 @@ static lean_object* _init_l_Lean_Elab_Term_MVarErrorInfo_logError___closed__13()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__12;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -22673,7 +22673,7 @@ static lean_object* _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeE
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Exception___hyg_3____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -25040,7 +25040,7 @@ static lean_object* _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImpli
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -29025,7 +29025,7 @@ lean_dec(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_27 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_28 = lean_box(0);
x_29 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3(x_24, x_4, x_1, x_2, x_3, x_27, x_28, x_5, x_6, x_7, x_8, x_9, x_10, x_21);
lean_dec(x_24);
@ -29108,7 +29108,7 @@ lean_dec(x_49);
if (x_50 == 0)
{
lean_object* x_51; lean_object* x_52; lean_object* x_53;
x_51 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_51 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_52 = lean_box(0);
x_53 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3(x_48, x_4, x_1, x_2, x_3, x_51, x_52, x_47, x_6, x_7, x_8, x_9, x_10, x_21);
lean_dec(x_48);
@ -29231,7 +29231,7 @@ lean_dec(x_83);
if (x_84 == 0)
{
lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_85 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_85 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_86 = lean_box(0);
x_87 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3(x_82, x_4, x_1, x_2, x_3, x_85, x_86, x_81, x_6, x_7, x_8, x_9, x_10, x_68);
lean_dec(x_82);
@ -33683,7 +33683,7 @@ static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_85
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Lean_Parser_Tactic_letrec___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -55422,7 +55422,7 @@ static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12817__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_myMacro____x40_Init_Coe___hyg_166____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

337
stage0/stdlib/Lean/Elab/Util.c generated
View file

@ -29,6 +29,7 @@ extern lean_object* l_Std_Format_format_unicode___closed__1;
lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMacroAttribute(lean_object*);
lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__7;
lean_object* l_Lean_Macro_getCurrNamespace(lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MacroScopesView_format___boxed(lean_object*, lean_object*);
lean_object* l_String_toFormat(lean_object*);
@ -55,7 +56,6 @@ lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__2(lean_object*, lean_object
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_List_forM___at_Lean_Elab_liftMacroM___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg(lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Elab_getMacros___spec__4(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute___rarg___closed__1;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_280____closed__1;
@ -82,7 +82,6 @@ lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__6;
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__2;
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ScopedEnvExtension_getState___at_Lean_Elab_getMacros___spec__1___boxed(lean_object*, lean_object*);
@ -97,6 +96,7 @@ lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacroFns(lean_object*
lean_object* l_Lean_Elab_liftMacroM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_53____spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___at_Lean_Elab_liftMacroM___spec__2___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -107,7 +107,6 @@ lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2___boxed(lean_object**);
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__5;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_36____closed__8;
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Elab_getMacros___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespacesAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instMonadMacroAdapter(lean_object*, lean_object*);
@ -116,12 +115,12 @@ lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespacesAux_match__1___rarg(lean
uint8_t l_Lean_Option_get___at_Lean_ppExpr___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_280_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_640_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253_(lean_object*);
lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_IO_instInhabitedError___closed__1;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Syntax_prettyPrint(lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName_loop(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -135,9 +134,9 @@ lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__1;
lean_object* l_List_forM___at_Lean_Elab_liftMacroM___spec__2(lean_object*);
lean_object* l_Lean_Elab_instMonadMacroAdapter___rarg(lean_object*, lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack(lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_hasDecl(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacroFns_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_liftMacroM(lean_object*, lean_object*);
@ -157,6 +156,7 @@ extern lean_object* l_Lean_Parser_Command_namedName___elambda__1___closed__2;
lean_object* l_Lean_Elab_addMacroStack___rarg___lambda__1___closed__3;
lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Elab_getMacros___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_fmt___at_Lean_Level_PP_Result_format___spec__1(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
lean_object* l_Lean_Syntax_unsetTrailing(lean_object*);
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1(lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__1;
@ -173,21 +173,19 @@ lean_object* l_Lean_Elab_macroAttribute;
lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1___closed__2;
lean_object* lean_environment_main_module(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_280____closed__3;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__1;
lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute(lean_object*);
lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacroFns_match__2(lean_object*);
lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__5;
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro(lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_getBetterRef_match__2(lean_object*);
uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object*, lean_object*);
extern lean_object* l_Lean_getSanitizeNames___closed__2;
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l_Lean_getSanitizeNames___closed__1;
lean_object* l_Lean_throwError___at_Lean_Attribute_Builtin_getId___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -243,7 +241,7 @@ lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__9(lean_object*, lean_object
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint(lean_object*);
lean_object* l_Lean_Elab_addMacroStack_match__1(lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName(lean_object*);
lean_object* l_Lean_Elab_mkUnusedBaseName(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Attribute_Builtin_getId(lean_object*, lean_object*, lean_object*, lean_object*);
@ -3320,136 +3318,219 @@ x_18 = l_Lean_Elab_adaptMacro___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x
return x_18;
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; uint8_t x_7;
lean_inc(x_4);
lean_inc(x_1);
x_5 = l_Lean_Name_appendIndexAfter(x_1, x_4);
lean_inc(x_5);
x_6 = l_Lean_Name_append(x_2, x_5);
lean_inc(x_3);
x_7 = l_Lean_Environment_contains(x_3, x_6);
lean_dec(x_6);
if (x_7 == 0)
{
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_5;
}
else
{
lean_object* x_8; lean_object* x_9;
lean_dec(x_5);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_add(x_4, x_8);
lean_dec(x_4);
x_4 = x_9;
goto _start;
}
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName_loop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_mkUnusedBaseName_loop(x_1, x_2, x_3, x_4);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; uint8_t x_6;
lean_inc(x_2);
x_5 = l_Lean_Name_append(x_1, x_2);
lean_inc(x_4);
x_6 = l_Lean_Environment_contains(x_4, x_5);
lean_dec(x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_4);
x_7 = lean_ctor_get(x_3, 0);
lean_inc(x_7);
lean_dec(x_3);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_apply_2(x_8, lean_box(0), x_2);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_10 = lean_ctor_get(x_3, 0);
lean_inc(x_10);
lean_dec(x_3);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Elab_mkUnusedBaseName_loop(x_2, x_1, x_4, x_12);
x_14 = lean_apply_2(x_11, lean_box(0), x_13);
return x_14;
}
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Lean_Elab_mkUnusedBaseName_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_inc(x_1);
x_6 = l_Lean_Name_appendIndexAfter(x_1, x_3);
lean_inc(x_6);
x_7 = l_Lean_Name_append(x_2, x_6);
lean_inc(x_4);
x_8 = l_Lean_Macro_hasDecl(x_7, x_4, x_5);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; uint8_t x_10;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_unbox(x_9);
lean_dec(x_9);
if (x_10 == 0)
{
uint8_t x_11;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1___boxed), 4, 3);
lean_closure_set(x_7, 0, x_5);
lean_closure_set(x_7, 1, x_2);
lean_closure_set(x_7, 2, x_3);
x_8 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_6, x_7);
x_11 = !lean_is_exclusive(x_8);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_8, 0);
lean_dec(x_12);
lean_ctor_set(x_8, 0, x_6);
return x_8;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_8, 1);
lean_inc(x_13);
lean_dec(x_8);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_6);
lean_ctor_set(x_14, 1, x_13);
return x_14;
}
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_6);
x_15 = lean_ctor_get(x_8, 1);
lean_inc(x_15);
lean_dec(x_8);
x_16 = lean_unsigned_to_nat(1u);
x_17 = lean_nat_add(x_3, x_16);
lean_dec(x_3);
x_3 = x_17;
x_5 = x_15;
goto _start;
}
}
else
{
uint8_t x_19;
lean_dec(x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_19 = !lean_is_exclusive(x_8);
if (x_19 == 0)
{
return x_8;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_8, 0);
x_21 = lean_ctor_get(x_8, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_8);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName_loop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_Elab_mkUnusedBaseName_loop(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_2);
return x_6;
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
lean_inc(x_2);
x_4 = l_Lean_Macro_getCurrNamespace(x_2, x_3);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_1, 1);
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_3);
lean_inc(x_5);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_mkUnusedBaseName___rarg___lambda__2), 5, 4);
lean_closure_set(x_7, 0, x_2);
lean_closure_set(x_7, 1, x_4);
lean_closure_set(x_7, 2, x_1);
lean_closure_set(x_7, 3, x_5);
x_8 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_7);
lean_dec(x_4);
lean_inc(x_1);
x_7 = l_Lean_Name_append(x_5, x_1);
lean_inc(x_2);
x_8 = l_Lean_Macro_hasDecl(x_7, x_2, x_6);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; uint8_t x_10;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_unbox(x_9);
lean_dec(x_9);
if (x_10 == 0)
{
uint8_t x_11;
lean_dec(x_5);
lean_dec(x_2);
x_11 = !lean_is_exclusive(x_8);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_8, 0);
lean_dec(x_12);
lean_ctor_set(x_8, 0, x_1);
return x_8;
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName(lean_object* x_1) {
_start:
else
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_mkUnusedBaseName___rarg), 4, 0);
return x_2;
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_8, 1);
lean_inc(x_13);
lean_dec(x_8);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_1);
lean_ctor_set(x_14, 1, x_13);
return x_14;
}
}
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
else
{
lean_object* x_5;
x_5 = l_Lean_Elab_mkUnusedBaseName___rarg___lambda__1(x_1, x_2, x_3, x_4);
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_8, 1);
lean_inc(x_15);
lean_dec(x_8);
x_16 = lean_unsigned_to_nat(1u);
x_17 = l_Lean_Elab_mkUnusedBaseName_loop(x_1, x_5, x_16, x_2, x_15);
lean_dec(x_5);
return x_17;
}
}
else
{
uint8_t x_18;
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
x_18 = !lean_is_exclusive(x_8);
if (x_18 == 0)
{
return x_8;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_8, 0);
x_20 = lean_ctor_get(x_8, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_8);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1() {
}
else
{
uint8_t x_22;
lean_dec(x_2);
lean_dec(x_1);
x_22 = !lean_is_exclusive(x_4);
if (x_22 == 0)
{
return x_4;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_4, 0);
x_24 = lean_ctor_get(x_4, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_4);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -3459,21 +3540,21 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_919____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
if (lean_obj_tag(x_3) == 0)
{
@ -3481,7 +3562,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
return x_6;
}
@ -3596,11 +3677,11 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_macroAttribute = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_macroAttribute);
lean_dec_ref(res);
l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248____closed__2);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1248_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253____closed__2);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1253_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

140
stage0/stdlib/Lean/Parser/Basic.c generated
View file

@ -94,7 +94,6 @@ lean_object* l_Lean_Parser_FirstTokens_toOptional_match__1(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_fieldIdxKind___closed__2;
lean_object* l_Lean_Parser_strAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Parser_eoi;
@ -129,7 +128,6 @@ lean_object* l_Lean_Parser_hexNumberFn___boxed(lean_object*, lean_object*, lean_
lean_object* l_Lean_Parser_parserOfStackFnUnsafe_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_peekTokenAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__2(lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125____boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_longestMatchFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_fieldIdx___closed__6;
lean_object* l_Lean_Parser_errorAtSavedPos___closed__1;
@ -173,6 +171,7 @@ extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__17;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_tokenWithAntiquotFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbolInfo___closed__2;
lean_object* l_Lean_Parser_anyOfFn_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -203,11 +202,11 @@ lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__2(lean_object*,
lean_object* l_Lean_Parser_instInhabitedParserInfo___closed__1;
lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__1;
lean_object* l_Lean_Parser_leadingParserAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____lambda__1(lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
uint8_t l_Lean_Parser_hexNumberFn___lambda__1(uint32_t);
lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_satisfyFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1;
lean_object* l_Lean_Parser_mkTokenAndFixPos___closed__2;
lean_object* l_Lean_Parser_mkAntiquot___closed__9;
uint8_t l_Lean_Parser_octalNumberFn___lambda__1(uint32_t);
@ -220,6 +219,7 @@ lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__4(lean_object*);
lean_object* l_Lean_Parser_ParserInfo_collectTokens___default___boxed(lean_object*);
lean_object* l_Lean_Parser_ParserState_mkTrailingNode(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_ins___at_Lean_Parser_TokenMap_insert___spec__4(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____lambda__1(lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__4;
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_Error_expectedToString_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
@ -232,6 +232,7 @@ lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withoutForbidden___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
lean_object* l_Lean_Parser_notFollowedBy(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163____boxed(lean_object*, lean_object*);
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Parser_info___default___closed__1;
uint8_t l_Char_isWhitespace(uint32_t);
@ -276,7 +277,6 @@ lean_object* l_Lean_Parser_instInhabitedParserInfo___closed__3;
lean_object* l_Lean_Parser_nameLitFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_setExpected___elambda__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_instInhabitedParserInfo___lambda__2___boxed(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1;
extern lean_object* l_term___x24_______closed__5;
lean_object* l_Lean_Parser_strLitFnAux___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nameLitKind;
@ -297,7 +297,6 @@ lean_object* l_Lean_Parser_tokenWithAntiquotFn___lambda__2___closed__3;
lean_object* l_Lean_Parser_checkPrecFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_indexed___rarg(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__6(lean_object*);
uint32_t l_Lean_Parser_getNext(lean_object*, lean_object*);
@ -342,6 +341,7 @@ lean_object* l_Lean_Parser_manyAux___lambda__2___boxed(lean_object*, lean_object
lean_object* l_Lean_Parser_symbolNoAntiquot(lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2(lean_object*);
lean_object* l_Lean_Parser_checkOutsideQuot___closed__1;
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
lean_object* l_Lean_Parser_evalParserConst___rarg___boxed(lean_object*);
@ -351,10 +351,12 @@ lean_object* l_Lean_Parser_mkIdResult___boxed(lean_object*, lean_object*, lean_o
lean_object* l_Lean_Parser_fieldIdx___closed__1;
lean_object* l_Lean_Parser_TokenMap_insert(lean_object*);
lean_object* l_Lean_Parser_setExpected___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1;
lean_object* l_Lean_Parser_unicodeSymbol(lean_object*, lean_object*);
lean_object* l_Lean_Parser_longestMatchFn___closed__1;
lean_object* l_Lean_Parser_checkStackTopFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeWhileFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withAntiquotSuffixSplice(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_unicodeSymbolInfo___elambda__1(lean_object*);
@ -526,6 +528,7 @@ lean_object* l_Lean_Parser_checkWsBefore(lean_object*);
lean_object* l_Lean_Parser_checkNoWsBeforeFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_setCache(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_foldArgsM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__10;
lean_object* l_Std_RBNode_ins___at_Lean_Parser_TokenMap_insert___spec__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_antiquotNestedExpr___closed__5;
@ -613,7 +616,6 @@ lean_object* l_Lean_Parser_identFnAux_parse___boxed(lean_object*, lean_object*,
lean_object* l_Lean_Parser_identFnAux_parse___lambda__2___closed__1;
lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3;
lean_object* l_Lean_Parser_leadingParserAux_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1(lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__7___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__7___rarg___boxed(lean_object*, lean_object*);
@ -730,6 +732,7 @@ lean_object* l_String_intercalate(lean_object*, lean_object*);
lean_object* l_Lean_Parser_leadingParser___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_FirstTokens_toStr_match__1(lean_object*);
lean_object* l_Lean_Parser_charLitFn___closed__3;
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1(lean_object*);
lean_object* l_Lean_Parser_hexDigitFn(lean_object*, lean_object*);
lean_object* l_List_redLength___rarg(lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__16;
@ -746,6 +749,7 @@ lean_object* l_Lean_Parser_categoryParserOfStackFn___boxed(lean_object*, lean_ob
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_checkNoImmediateColon___elambda__1___closed__1;
lean_object* l_Lean_Parser_runLongestMatchParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkTrailingNode___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquotSplice___closed__6;
lean_object* l_Lean_Parser_FirstTokens_merge_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -759,6 +763,7 @@ lean_object* l_Lean_Parser_sepByNoAntiquot___boxed(lean_object*, lean_object*, l
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_tokenFnAux_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_PrattParsingTables_trailingTable___default;
lean_object* l_Lean_Parser_ParserModuleContext_currNamespace___default;
lean_object* l_Lean_Parser_ParserState_setError(lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__5___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkUnexpectedErrorAt(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_TokenMap_insert___spec__1(lean_object*);
@ -791,7 +796,7 @@ lean_object* l_Lean_Parser_Error_instToStringError___closed__1;
lean_object* l_Lean_Parser_checkTailNoWs_match__1(lean_object*);
lean_object* l_Lean_Parser_TokenMap_instEmptyCollectionTokenMap(lean_object*);
lean_object* l_Lean_Parser_orelseInfo___elambda__1(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125_(uint8_t, uint8_t);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163_(uint8_t, uint8_t);
extern lean_object* l_Array_instToStringArray___rarg___closed__1;
lean_object* l_Lean_Parser_errorAtSavedPos(lean_object*, uint8_t);
lean_object* l_Lean_Parser_mkAntiquot___closed__14;
@ -918,8 +923,8 @@ extern lean_object* l_Lean_Syntax_antiquotSpliceKind_x3f_match__1___rarg___close
lean_object* l_Lean_Parser_mkAntiquot___closed__6;
lean_object* l_Lean_Parser_parserOfStackFnUnsafe___closed__1;
extern lean_object* l_Lean_Syntax_mkAntiquotNode___closed__6;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476_(lean_object*);
uint8_t l_Lean_Parser_instInhabitedLeadingIdentBehavior;
lean_object* l_Lean_Parser_fieldIdx___closed__7;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
@ -1007,10 +1012,8 @@ lean_object* l_Lean_Parser_unicodeSymbolFnAux___boxed(lean_object*, lean_object*
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
lean_object* l_Lean_Parser_indexed___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1;
lean_object* l_Lean_Parser_rawFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_categoryParserOfStackFn(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_keepPrevError(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_checkWsBefore___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1___elambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1031,7 +1034,6 @@ lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__2___rarg(lean_ob
lean_object* l_Lean_Parser_mkAntiquot___closed__2;
lean_object* l_Lean_Parser_withResultOfInfo(lean_object*);
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14904____closed__9;
lean_object* l_Lean_Parser_categoryParserOfStack___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qpartition_loop___at_Lean_Parser_Error_toString___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1071,7 +1073,6 @@ lean_object* l_Lean_Parser_numberFnAux___boxed(lean_object*, lean_object*);
uint8_t lean_string_dec_lt(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_forArgsM___spec__1(lean_object*);
lean_object* l_Lean_Parser_fieldIdxFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_hexNumberFn___closed__2;
lean_object* l_Lean_Parser_mkIdent(lean_object*, lean_object*, lean_object*);
@ -3479,6 +3480,61 @@ lean_dec(x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_ParserState_setError(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_1);
if (x_3 == 0)
{
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 = lean_ctor_get(x_1, 4);
lean_dec(x_4);
x_5 = lean_box(0);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_2);
lean_ctor_set(x_6, 1, x_5);
x_7 = l_Lean_instInhabitedParserDescr___closed__1;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_1, 4, x_9);
return x_1;
}
else
{
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; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_10 = lean_ctor_get(x_1, 0);
x_11 = lean_ctor_get(x_1, 1);
x_12 = lean_ctor_get(x_1, 2);
x_13 = lean_ctor_get(x_1, 3);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_1);
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_2);
lean_ctor_set(x_15, 1, x_14);
x_16 = l_Lean_instInhabitedParserDescr___closed__1;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
x_19 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_19, 0, x_10);
lean_ctor_set(x_19, 1, x_11);
lean_ctor_set(x_19, 2, x_12);
lean_ctor_set(x_19, 3, x_13);
lean_ctor_set(x_19, 4, x_18);
return x_19;
}
}
}
lean_object* l_Lean_Parser_ParserState_mkError(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -26914,7 +26970,7 @@ x_1 = 0;
return x_1;
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
switch (x_1) {
@ -26996,15 +27052,15 @@ return x_24;
}
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1(lean_object* x_1) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg___boxed), 6, 0);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; uint8_t x_8; lean_object* x_9;
@ -27012,11 +27068,11 @@ x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = lean_unbox(x_2);
lean_dec(x_2);
x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
return x_9;
}
}
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125_(uint8_t x_1, uint8_t x_2) {
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163_(uint8_t x_1, uint8_t x_2) {
_start:
{
switch (x_1) {
@ -27077,7 +27133,7 @@ return x_11;
}
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125____boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
@ -27085,7 +27141,7 @@ x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125_(x_3, x_4);
x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163_(x_3, x_4);
x_6 = lean_box(x_5);
return x_6;
}
@ -27094,7 +27150,7 @@ static lean_object* _init_l_Lean_Parser_instBEqLeadingIdentBehavior___closed__1(
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7125____boxed), 2, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7163____boxed), 2, 0);
return x_1;
}
}
@ -28356,7 +28412,7 @@ lean_dec(x_1);
return x_6;
}
}
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
@ -28381,7 +28437,7 @@ return x_7;
}
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
@ -28389,34 +28445,34 @@ x_4 = l_Lean_Parser_whitespace(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1___boxed), 3, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1___boxed), 3, 0);
return x_1;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420_(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1;
x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____spec__1(x_2, x_1);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1;
x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____spec__1(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____lambda__1(x_1, x_2, x_3);
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____lambda__1(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____lambda__1(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____lambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
@ -28442,19 +28498,19 @@ return x_7;
}
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____lambda__1), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____lambda__1), 1, 0);
return x_1;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438_(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1;
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
return x_3;
}
@ -33462,16 +33518,16 @@ l_Lean_Parser_instInhabitedParserCategory___closed__1 = _init_l_Lean_Parser_inst
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory___closed__1);
l_Lean_Parser_instInhabitedParserCategory = _init_l_Lean_Parser_instInhabitedParserCategory();
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory);
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7420_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7458_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Parser_categoryParserFnRef = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Parser_categoryParserFnRef);
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7438_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7476_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Parser_categoryParserFnExtension = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension);

116
stage0/stdlib/Lean/Parser/StrInterpolation.c generated
View file

@ -18,14 +18,13 @@ lean_object* l_Lean_Parser_quotedCharCoreFn(lean_object*, lean_object*, lean_obj
uint8_t l_Lean_Parser_isQuotableCharDefault(uint32_t);
lean_object* l_Lean_Parser_ParserState_next(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStrNoAntiquot___closed__1;
lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
extern lean_object* l_Lean_interpolatedStrKind;
lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
lean_object* l_Lean_Parser_interpolatedStrFn_parse___lambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_mkNodeToken(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_strLitFnAux___closed__1;
lean_object* l_Lean_Parser_satisfyFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStr___elambda__1___closed__1;
lean_object* l_Lean_Parser_interpolatedStr___elambda__1___closed__2;
@ -35,7 +34,6 @@ lean_object* l_Lean_Parser_interpolatedStrFn___closed__1;
lean_object* l_Lean_Parser_interpolatedStrFn_parse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStrFn_parse___closed__1;
lean_object* l_Lean_Parser_interpolatedStrNoAntiquot(lean_object*);
lean_object* l_Lean_Parser_interpolatedStrFn_parse___closed__3;
uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*);
uint8_t l_Lean_Parser_isQuotableCharForStrInterpolant(uint32_t);
@ -45,8 +43,7 @@ uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStr(lean_object*);
lean_object* l_Lean_Parser_interpolatedStr___closed__1;
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
uint8_t l_Lean_Parser_interpolatedStrFn_parse___lambda__1(uint32_t);
lean_object* l_Lean_Parser_ParserState_mkUnexpectedErrorAt(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_setError(lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStr___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStrFn_parse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -88,20 +85,11 @@ x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Lean_Parser_interpolatedStrFn_parse___lambda__1(uint32_t x_1) {
_start:
{
uint32_t x_2; uint8_t x_3;
x_2 = 125;
x_3 = x_1 == x_2;
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_interpolatedStrFn_parse___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_interpolatedStrFn_parse___lambda__1___boxed), 1, 0);
x_1 = lean_mk_string("'}'");
return x_1;
}
}
@ -109,14 +97,6 @@ static lean_object* _init_l_Lean_Parser_interpolatedStrFn_parse___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("expected '}'");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_interpolatedStrFn_parse___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_isQuotableCharForStrInterpolant___boxed), 1, 0);
return x_1;
}
@ -174,28 +154,33 @@ return x_21;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30;
lean_object* x_25; uint32_t x_26; uint32_t x_27; uint8_t x_28;
x_25 = lean_ctor_get(x_21, 2);
lean_inc(x_25);
x_26 = l_Lean_Parser_interpolatedStrFn_parse___closed__1;
x_27 = l_Lean_Parser_interpolatedStrFn_parse___closed__2;
x_28 = l_Lean_Parser_satisfyFn(x_26, x_27, x_5, x_21);
x_29 = lean_ctor_get(x_28, 4);
lean_inc(x_29);
x_30 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_713____at_Lean_Parser_ParserState_hasError___spec__1(x_29, x_23);
lean_dec(x_29);
if (x_30 == 0)
x_26 = lean_string_utf8_get(x_2, x_25);
x_27 = 125;
x_28 = x_26 == x_27;
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
lean_dec(x_25);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
return x_28;
x_29 = lean_box(0);
x_30 = l_Lean_Parser_ParserState_pushSyntax(x_21, x_29);
x_31 = l_Lean_interpolatedStrKind;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_3);
x_33 = l_Lean_Parser_interpolatedStrFn_parse___closed__1;
x_34 = l_Lean_Parser_ParserState_setError(x_32, x_33);
return x_34;
}
else
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_string_utf8_next(x_2, x_25);
x_36 = l_Lean_Parser_ParserState_setPos(x_21, x_35);
x_4 = x_25;
x_6 = x_28;
x_6 = x_36;
goto _start;
}
}
@ -203,65 +188,58 @@ goto _start;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_32 = l_Lean_Parser_interpolatedStrFn_parse___closed__3;
x_33 = l_Lean_Parser_quotedCharCoreFn(x_32, x_5, x_11);
x_34 = lean_ctor_get(x_33, 4);
lean_inc(x_34);
x_35 = lean_box(0);
x_36 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_713____at_Lean_Parser_ParserState_hasError___spec__1(x_34, x_35);
lean_dec(x_34);
if (x_36 == 0)
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42;
x_38 = l_Lean_Parser_interpolatedStrFn_parse___closed__2;
x_39 = l_Lean_Parser_quotedCharCoreFn(x_38, x_5, x_11);
x_40 = lean_ctor_get(x_39, 4);
lean_inc(x_40);
x_41 = lean_box(0);
x_42 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_713____at_Lean_Parser_ParserState_hasError___spec__1(x_40, x_41);
lean_dec(x_40);
if (x_42 == 0)
{
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_33;
return x_39;
}
else
{
x_6 = x_33;
x_6 = x_39;
goto _start;
}
}
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
lean_dec(x_1);
x_38 = l_Lean_interpolatedStrLitKind;
x_39 = l_Lean_Parser_mkNodeToken(x_38, x_4, x_5, x_11);
x_44 = l_Lean_interpolatedStrLitKind;
x_45 = l_Lean_Parser_mkNodeToken(x_44, x_4, x_5, x_11);
lean_dec(x_5);
x_40 = l_Lean_interpolatedStrKind;
x_41 = l_Lean_Parser_ParserState_mkNode(x_39, x_40, x_3);
return x_41;
x_46 = l_Lean_interpolatedStrKind;
x_47 = l_Lean_Parser_ParserState_mkNode(x_45, x_46, x_3);
return x_47;
}
}
else
{
lean_object* x_42; lean_object* x_43;
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_4);
lean_dec(x_1);
x_42 = l_Lean_Parser_strLitFnAux___closed__1;
x_43 = l_Lean_Parser_ParserState_mkUnexpectedErrorAt(x_6, x_42, x_4);
return x_43;
x_48 = lean_box(0);
x_49 = l_Lean_Parser_ParserState_pushSyntax(x_6, x_48);
x_50 = l_Lean_interpolatedStrKind;
x_51 = l_Lean_Parser_ParserState_mkNode(x_49, x_50, x_3);
x_52 = l_Lean_Parser_strLitFnAux___closed__1;
x_53 = l_Lean_Parser_ParserState_setError(x_51, x_52);
return x_53;
}
}
}
lean_object* l_Lean_Parser_interpolatedStrFn_parse___lambda__1___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint32(x_1);
lean_dec(x_1);
x_3 = l_Lean_Parser_interpolatedStrFn_parse___lambda__1(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_interpolatedStrFn_parse___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -456,8 +434,6 @@ l_Lean_Parser_interpolatedStrFn_parse___closed__1 = _init_l_Lean_Parser_interpol
lean_mark_persistent(l_Lean_Parser_interpolatedStrFn_parse___closed__1);
l_Lean_Parser_interpolatedStrFn_parse___closed__2 = _init_l_Lean_Parser_interpolatedStrFn_parse___closed__2();
lean_mark_persistent(l_Lean_Parser_interpolatedStrFn_parse___closed__2);
l_Lean_Parser_interpolatedStrFn_parse___closed__3 = _init_l_Lean_Parser_interpolatedStrFn_parse___closed__3();
lean_mark_persistent(l_Lean_Parser_interpolatedStrFn_parse___closed__3);
l_Lean_Parser_interpolatedStrFn___closed__1 = _init_l_Lean_Parser_interpolatedStrFn___closed__1();
lean_mark_persistent(l_Lean_Parser_interpolatedStrFn___closed__1);
l_Lean_Parser_interpolatedStrNoAntiquot___closed__1 = _init_l_Lean_Parser_interpolatedStrNoAntiquot___closed__1();