chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
b9c161b30c
commit
31cddbcb6f
29 changed files with 6770 additions and 3511 deletions
|
|
@ -42,15 +42,6 @@ def components' : Name → List Name
|
|||
def components (n : Name) : List Name :=
|
||||
n.components'.reverse
|
||||
|
||||
@[extern "lean_name_eq"]
|
||||
protected def beq : (@& Name) → (@& Name) → Bool
|
||||
| anonymous, anonymous => true
|
||||
| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && beq p₁ p₂
|
||||
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && beq p₁ p₂
|
||||
| _, _ => false
|
||||
|
||||
instance : HasBeq Name := ⟨Name.beq⟩
|
||||
|
||||
def eqStr : Name → String → Bool
|
||||
| str anonymous s _, s' => s == s'
|
||||
| _, _ => false
|
||||
|
|
|
|||
|
|
@ -207,30 +207,33 @@ private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM
|
|||
| Exception.error _ => throw ex
|
||||
| Exception.unsupportedSyntax => elabCommandUsing elabFns)
|
||||
|
||||
def elabCommandAux (stx : Syntax) : CommandElabM Unit :=
|
||||
withIncRecDepth stx $ withFreshMacroScope $ match stx with
|
||||
| Syntax.node _ _ => do
|
||||
trace `Elab.step stx $ fun _ => stx;
|
||||
s ← get;
|
||||
let table := (commandElabAttribute.ext.getState s.env).table;
|
||||
let k := stx.getKind;
|
||||
match table.find? k with
|
||||
| some elabFns => elabCommandUsing stx elabFns
|
||||
| none => throwError stx ("command '" ++ toString k ++ "' has not been implemented")
|
||||
| _ => throwError stx "unexpected command"
|
||||
|
||||
def elabCommand (stx : Syntax) : CommandElabM Unit :=
|
||||
if stx.getKind == nullKind then
|
||||
-- list of commands => elaborate in order
|
||||
-- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
|
||||
stx.getArgs.forM elabCommandAux
|
||||
else
|
||||
elabCommandAux stx
|
||||
|
||||
/- Elaborate `x` with `stx` on the macro stack -/
|
||||
@[inline] def withMacroExpansion {α} (stx : Syntax) (x : CommandElabM α) : CommandElabM α :=
|
||||
adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x
|
||||
|
||||
partial def elabCommand : Syntax → CommandElabM Unit
|
||||
| stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
|
||||
| Syntax.node _ _ => do
|
||||
trace `Elab.step stx $ fun _ => stx;
|
||||
s ← get;
|
||||
let table := (commandElabAttribute.ext.getState s.env).table;
|
||||
let k := stx.getKind;
|
||||
match table.find? k with
|
||||
| some elabFns => elabCommandUsing stx elabFns
|
||||
| none => do
|
||||
scp ← getCurrMacroScope;
|
||||
env ← getEnv;
|
||||
match expandMacro env stx scp with
|
||||
| some stx' => withMacroExpansion stx $
|
||||
if stx'.getKind == nullKind then
|
||||
-- list of commands => elaborate in order
|
||||
-- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
|
||||
stx'.getArgs.forM elabCommand
|
||||
else
|
||||
elabCommand stx'
|
||||
| none => throwError stx ("command '" ++ toString k ++ "' has not been implemented")
|
||||
| _ => throwError stx "unexpected command"
|
||||
|
||||
/-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
|
||||
def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab :=
|
||||
fun stx => withMacroExpansion stx $ do
|
||||
|
|
|
|||
|
|
@ -98,6 +98,7 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
|
|||
val ← Term.levelMVarToParam val;
|
||||
type ← Term.instantiateMVars ref type;
|
||||
val ← Term.instantiateMVars view.val val;
|
||||
Term.trace `Elab.definition.body ref $ fun _ => val;
|
||||
let usedParams : CollectLevelParams.State := {};
|
||||
let usedParams := collectLevelParams usedParams type;
|
||||
let usedParams := collectLevelParams usedParams val;
|
||||
|
|
@ -153,6 +154,10 @@ withDeclId view.declId $ fun name => do
|
|||
compileDecl ref decl;
|
||||
applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab.definition;
|
||||
pure ()
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -118,10 +118,22 @@ fun stx => do
|
|||
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
|
||||
type ← `(Lean.ParserDescr);
|
||||
val ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 2);
|
||||
d ← `(@[$catParserId:ident] private def $catParserId:ident : $type := ParserDescr.node $(quote kind) $val);
|
||||
-- TODO: meaningful, unhygienic def name for selective parser `open`ing?
|
||||
d ← `(@[$catParserId:ident] def myParser : $type := ParserDescr.node $(quote kind) $val);
|
||||
trace `Elab stx $ fun _ => d;
|
||||
withMacroExpansion stx $ elabCommand d
|
||||
|
||||
@[builtinCommandElab macro] def elabMacro : CommandElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(macro $alts*) => do
|
||||
-- TODO: clean up with matchAlt quotation
|
||||
k ← match_syntax ((alts.get! 0).getArg 1).getArg 0 with
|
||||
| `(`($quot)) => pure quot.getKind
|
||||
| stx => throwUnsupportedSyntax;
|
||||
-- TODO: meaningful, unhygienic def name for selective macro `open`ing?
|
||||
`(@[macro $(Lean.mkSimpleIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw ())
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -515,6 +515,29 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
|
|||
else
|
||||
throw ex)
|
||||
|
||||
@[inline] def adaptMacro (x : Macro) (stx : Syntax) : TermElabM Syntax := do
|
||||
scp ← getCurrMacroScope;
|
||||
env ← getEnv;
|
||||
match x stx scp with
|
||||
| some stx => pure stx
|
||||
| none => throwUnsupportedSyntax
|
||||
|
||||
/- Main loop for `elabTerm` -/
|
||||
partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := true) (errToSorry := true) : Syntax → TermElabM Expr
|
||||
| stx => withFreshMacroScope $ withIncRecDepth stx $ withNode stx $ fun node => do
|
||||
trace `Elab.step stx $ fun _ => stx;
|
||||
s ← get;
|
||||
let table := (termElabAttribute.ext.getState s.env).table;
|
||||
let k := node.getKind;
|
||||
match table.find? k with
|
||||
| some elabFns => elabTermUsing s node expectedType? errToSorry catchExPostpone elabFns
|
||||
| none => do
|
||||
scp ← getCurrMacroScope;
|
||||
env ← getEnv;
|
||||
match expandMacro env stx scp with
|
||||
| some stx' => withMacroExpansion stx $ elabTermAux stx'
|
||||
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
|
||||
/--
|
||||
Main function for elaborating terms.
|
||||
It extracts the elaboration methods from the environment using the node kind.
|
||||
|
|
@ -529,14 +552,7 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
|
|||
The option `catchExPostpone == false` is used to implement `resumeElabTerm`
|
||||
to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
|
||||
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errToSorry := true) : TermElabM Expr :=
|
||||
withFreshMacroScope $ withIncRecDepth stx $ withNode stx $ fun node => do
|
||||
trace `Elab.step stx $ fun _ => stx;
|
||||
s ← get;
|
||||
let table := (termElabAttribute.ext.getState s.env).table;
|
||||
let k := node.getKind;
|
||||
match table.find? k with
|
||||
| some elabFns => elabTermUsing s node expectedType? errToSorry catchExPostpone elabFns
|
||||
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
elabTermAux expectedType? catchExPostpone errToSorry stx
|
||||
|
||||
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
|
||||
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
|
||||
|
|
|
|||
|
|
@ -106,7 +106,8 @@ match mkElabFnOfConstant γ env typeName constName with
|
|||
pure $ ext.addEntry env { kind := kind, elabFn := f, constName := constName }
|
||||
|
||||
/- TODO: add support for scoped attributes -/
|
||||
def mkElabAttribute (γ) (attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String) (builtinTableRef : IO.Ref (ElabFnTable γ)) : IO (ElabAttribute γ) := do
|
||||
def mkElabAttributeAux (γ) (attrName : Name) (parserNamespace : Name) (typeName : Name) (descr : String) (kind : String) (builtinTableRef : IO.Ref (ElabFnTable γ))
|
||||
: IO (ElabAttribute γ) := do
|
||||
ext : ElabAttributeExtension γ ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
mkInitial := ElabAttribute.mkInitial builtinTableRef,
|
||||
|
|
@ -124,9 +125,38 @@ let attrImpl : AttributeImpl := {
|
|||
registerBuiltinAttribute attrImpl;
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
|
||||
def mkElabAttribute (γ) (attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String) (builtinTableRef : IO.Ref (ElabFnTable γ))
|
||||
: IO (ElabAttribute γ) :=
|
||||
mkElabAttributeAux γ attrName parserNamespace typeName (kind ++ " elaborator") kind builtinTableRef
|
||||
|
||||
abbrev MacroAttribute := ElabAttribute Macro
|
||||
abbrev MacroFnTable := ElabFnTable Macro
|
||||
|
||||
def mkBuiltinMacroFnTable : IO (IO.Ref MacroFnTable) := IO.mkRef {}
|
||||
@[init mkBuiltinMacroFnTable] constant builtinMacroFnTable : IO.Ref MacroFnTable := arbitrary _
|
||||
|
||||
def mkMacroAttribute : IO MacroAttribute :=
|
||||
mkElabAttributeAux Macro `macro Name.anonymous `Lean.Macro "macros" "macro" builtinMacroFnTable
|
||||
|
||||
@[init mkMacroAttribute] constant macroAttribute : MacroAttribute := arbitrary _
|
||||
|
||||
private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
|
||||
| [] => throw ()
|
||||
| m::ms => m stx <|> expandMacroFns ms
|
||||
|
||||
def expandMacro (env : Environment) : Macro :=
|
||||
fun stx =>
|
||||
let k := stx.getKind;
|
||||
let table := (macroAttribute.ext.getState env).table;
|
||||
match table.find? k with
|
||||
| some macroFns => expandMacroFns stx macroFns
|
||||
| none => throw ()
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab;
|
||||
registerTraceClass `Elab.step
|
||||
|
||||
|
||||
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -2,59 +2,14 @@
|
|||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich
|
||||
|
||||
Runtime support for making quotation terms auto-hygienic, by mangling identifiers
|
||||
introduced by them with a "macro scope" supplied by the context. Details to appear in a
|
||||
paper soon.
|
||||
-/
|
||||
prelude
|
||||
import Init.Control
|
||||
import Init.LeanInit
|
||||
import Init.Lean.Syntax
|
||||
|
||||
namespace Lean
|
||||
|
||||
abbrev MacroScope := Nat
|
||||
|
||||
/-- A monad that supports syntax quotations. Syntax quotations (in term
|
||||
position) are monadic values that when executed retrieve the current "macro
|
||||
scope" from the monad and apply it to every identifier they introduce
|
||||
(independent of whether this identifier turns out to be a reference to an
|
||||
existing declaration, or an actually fresh binding during further
|
||||
elaboration). -/
|
||||
class MonadQuotation (m : Type → Type) :=
|
||||
-- Get the fresh scope of the current macro invocation
|
||||
(getCurrMacroScope {} : m MacroScope)
|
||||
/- Execute action in a new macro invocation context. This transformer should be
|
||||
used at all places that morally qualify as the beginning of a "macro call",
|
||||
e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
|
||||
can also be used internally inside a "macro" if identifiers introduced by
|
||||
e.g. different recursive calls should be independent and not collide. While
|
||||
returning an intermediate syntax tree that will recursively be expanded by
|
||||
the elaborator can be used for the same effect, doing direct recursion inside
|
||||
the macro guarded by this transformer is often easier because one is not
|
||||
restricted to passing a single syntax tree. Modelling this helper as a
|
||||
transformer and not just a monadic action ensures that the current macro
|
||||
scope before the recursive call is restored after it, as expected. -/
|
||||
(withFreshMacroScope {α : Type} : m α → m α)
|
||||
export MonadQuotation
|
||||
|
||||
-- TODO: try harder to avoid clashes with other autogenerated names
|
||||
def addMacroScope (n : Name) (scp : MacroScope) : Name :=
|
||||
mkNameNum n scp
|
||||
|
||||
def addMacroScopes (n : Name) (scps : List MacroScope) : Name :=
|
||||
scps.foldl addMacroScope n
|
||||
|
||||
private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
|
||||
| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
|
||||
| n , acc => (n, acc.reverse)
|
||||
|
||||
/--
|
||||
Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
|
||||
This operation is useful for analyzing/transforming the original identifiers, then adding back
|
||||
the scopes (via `addMacroScopes`). -/
|
||||
def extractMacroScopes (n : Name) : Name × List MacroScope :=
|
||||
extractMacroScopesAux n []
|
||||
/- Remark: `MonadQuotation` class is part of the `Init` package and loaded by default since it is used in the builtin command `macro`. -/
|
||||
|
||||
/-- Simplistic MonadQuotation that does not guarantee globally fresh names, that
|
||||
is, between different runs of this or other MonadQuotation implementations.
|
||||
|
|
@ -80,6 +35,17 @@ instance MonadQuotation : MonadQuotation Unhygienic := {
|
|||
protected def run {α : Type} (x : Unhygienic α) : α := run x 0 1
|
||||
end Unhygienic
|
||||
|
||||
private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
|
||||
| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
|
||||
| n , acc => (n, acc.reverse)
|
||||
|
||||
/--
|
||||
Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
|
||||
This operation is useful for analyzing/transforming the original identifiers, then adding back
|
||||
the scopes (via `addMacroScopes`). -/
|
||||
def extractMacroScopes (n : Name) : Name × List MacroScope :=
|
||||
extractMacroScopesAux n []
|
||||
|
||||
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
|
||||
{ getCurrMacroScope := liftM (getCurrMacroScope : m Nat),
|
||||
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }
|
||||
|
|
|
|||
|
|
@ -9,13 +9,6 @@ import Init.Lean.Data.Name
|
|||
import Init.Lean.Data.Format
|
||||
|
||||
namespace Lean
|
||||
structure SourceInfo :=
|
||||
/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing,
|
||||
it is not at all clear what the preceding token was, especially with backtracking. -/
|
||||
(leading : Substring)
|
||||
(pos : String.Pos)
|
||||
(trailing : Substring)
|
||||
|
||||
namespace SourceInfo
|
||||
|
||||
def updateTrailing (info : SourceInfo) (trailing : Substring) : SourceInfo :=
|
||||
|
|
@ -36,8 +29,6 @@ end SourceInfo
|
|||
|
||||
/- Node kind generation -/
|
||||
|
||||
abbrev SyntaxNodeKind := Name
|
||||
|
||||
@[matchPattern] def choiceKind : SyntaxNodeKind := `choice
|
||||
@[matchPattern] def nullKind : SyntaxNodeKind := `null
|
||||
def strLitKind : SyntaxNodeKind := `strLit
|
||||
|
|
@ -47,15 +38,6 @@ def fieldIdxKind : SyntaxNodeKind := `fieldIdx
|
|||
|
||||
/- Syntax AST -/
|
||||
|
||||
inductive Syntax
|
||||
| missing {} : Syntax
|
||||
| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
|
||||
| atom {} (info : Option SourceInfo) (val : String) : Syntax
|
||||
| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
|
||||
|
||||
instance stxInh : Inhabited Syntax :=
|
||||
⟨Syntax.missing⟩
|
||||
|
||||
def Syntax.isMissing : Syntax → Bool
|
||||
| Syntax.missing => true
|
||||
| _ => false
|
||||
|
|
@ -138,12 +120,6 @@ def asNode : Syntax → SyntaxNode
|
|||
def getNumArgs (stx : Syntax) : Nat :=
|
||||
stx.asNode.getNumArgs
|
||||
|
||||
def getArgs (stx : Syntax) : Array Syntax :=
|
||||
stx.asNode.getArgs
|
||||
|
||||
def getArg (stx : Syntax) (i : Nat) : Syntax :=
|
||||
stx.asNode.getArg i
|
||||
|
||||
def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
|
||||
match stx with
|
||||
| node k _ => node k args
|
||||
|
|
@ -167,16 +143,6 @@ match stx with
|
|||
def getIdAt (stx : Syntax) (i : Nat) : Name :=
|
||||
(stx.getArg i).getId
|
||||
|
||||
def getKind (stx : Syntax) : SyntaxNodeKind :=
|
||||
match stx with
|
||||
| Syntax.node k args => k
|
||||
-- We use these "pseudo kinds" for antiquotation kinds.
|
||||
-- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident)
|
||||
-- is compiled to ``if stx.isOfKind `ident ...``
|
||||
| Syntax.missing => `missing
|
||||
| Syntax.atom _ v => v
|
||||
| Syntax.ident _ _ _ _ => `ident
|
||||
|
||||
@[specialize] partial def mreplace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m (Syntax)
|
||||
| stx@(node kind args) => do
|
||||
o ← fn stx;
|
||||
|
|
@ -185,9 +151,6 @@ match stx with
|
|||
| none => do args ← args.mapM mreplace; pure (node kind args)
|
||||
| stx => do o ← fn stx; pure $ o.getD stx
|
||||
|
||||
def isOfKind : Syntax → SyntaxNodeKind → Bool
|
||||
| stx, k => stx.getKind == k
|
||||
|
||||
@[specialize] partial def mrewriteBottomUp {m : Type → Type} [Monad m] (fn : Syntax → m (Syntax)) : Syntax → m (Syntax)
|
||||
| node kind args => do
|
||||
args ← args.mapM mrewriteBottomUp;
|
||||
|
|
|
|||
|
|
@ -1,12 +1,15 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
Authors: Leonardo de Moura and Sebastian Ullrich
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.String.Basic
|
||||
import Init.Data.Array.Basic
|
||||
import Init.Data.UInt
|
||||
import Init.Data.Hashable
|
||||
import Init.Control.Reader
|
||||
import Init.Control.Option
|
||||
|
||||
namespace Lean
|
||||
/-
|
||||
|
|
@ -47,6 +50,15 @@ Name.num p v $ mixHash (hash p) (hash v)
|
|||
def mkNameSimple (s : String) : Name :=
|
||||
mkNameStr Name.anonymous s
|
||||
|
||||
@[extern "lean_name_eq"]
|
||||
protected def Name.beq : (@& Name) → (@& Name) → Bool
|
||||
| Name.anonymous, Name.anonymous => true
|
||||
| Name.str p₁ s₁ _, Name.str p₂ s₂ _ => s₁ == s₂ && Name.beq p₁ p₂
|
||||
| Name.num p₁ n₁ _, Name.num p₂ n₂ _ => n₁ == n₂ && Name.beq p₁ p₂
|
||||
| _, _ => false
|
||||
|
||||
instance : HasBeq Name := ⟨Name.beq⟩
|
||||
|
||||
inductive ParserKind
|
||||
| leading | trailing
|
||||
|
||||
|
|
@ -97,4 +109,99 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
|
|||
@[matchPattern] abbrev ParserDescr.pushLeading := @ParserDescrCore.pushLeading
|
||||
@[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser
|
||||
|
||||
/- Syntax -/
|
||||
|
||||
structure SourceInfo :=
|
||||
/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing,
|
||||
it is not at all clear what the preceding token was, especially with backtracking. -/
|
||||
(leading : Substring)
|
||||
(pos : String.Pos)
|
||||
(trailing : Substring)
|
||||
|
||||
abbrev SyntaxNodeKind := Name
|
||||
|
||||
/- Syntax AST -/
|
||||
|
||||
inductive Syntax
|
||||
| missing {} : Syntax
|
||||
| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
|
||||
| atom {} (info : Option SourceInfo) (val : String) : Syntax
|
||||
| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
|
||||
|
||||
instance Syntax.inhabited : Inhabited Syntax :=
|
||||
⟨Syntax.missing⟩
|
||||
|
||||
namespace Syntax
|
||||
|
||||
def getKind (stx : Syntax) : SyntaxNodeKind :=
|
||||
match stx with
|
||||
| Syntax.node k args => k
|
||||
-- We use these "pseudo kinds" for antiquotation kinds.
|
||||
-- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident)
|
||||
-- is compiled to ``if stx.isOfKind `ident ...``
|
||||
| Syntax.missing => `missing
|
||||
| Syntax.atom _ v => mkNameSimple v
|
||||
| Syntax.ident _ _ _ _ => `ident
|
||||
|
||||
def isOfKind : Syntax → SyntaxNodeKind → Bool
|
||||
| stx, k => stx.getKind == k
|
||||
|
||||
def getArg (stx : Syntax) (i : Nat) : Syntax :=
|
||||
match stx with
|
||||
| Syntax.node _ args => args.get! i
|
||||
| _ => arbitrary _
|
||||
|
||||
def getArgs (stx : Syntax) : Array Syntax :=
|
||||
match stx with
|
||||
| Syntax.node _ args => args
|
||||
| _ => #[]
|
||||
|
||||
end Syntax
|
||||
|
||||
/-
|
||||
Runtime support for making quotation terms auto-hygienic, by mangling identifiers
|
||||
introduced by them with a "macro scope" supplied by the context. Details to appear in a
|
||||
paper soon.
|
||||
-/
|
||||
|
||||
abbrev MacroScope := Nat
|
||||
|
||||
/-- A monad that supports syntax quotations. Syntax quotations (in term
|
||||
position) are monadic values that when executed retrieve the current "macro
|
||||
scope" from the monad and apply it to every identifier they introduce
|
||||
(independent of whether this identifier turns out to be a reference to an
|
||||
existing declaration, or an actually fresh binding during further
|
||||
elaboration). -/
|
||||
class MonadQuotation (m : Type → Type) :=
|
||||
-- Get the fresh scope of the current macro invocation
|
||||
(getCurrMacroScope {} : m MacroScope)
|
||||
/- Execute action in a new macro invocation context. This transformer should be
|
||||
used at all places that morally qualify as the beginning of a "macro call",
|
||||
e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
|
||||
can also be used internally inside a "macro" if identifiers introduced by
|
||||
e.g. different recursive calls should be independent and not collide. While
|
||||
returning an intermediate syntax tree that will recursively be expanded by
|
||||
the elaborator can be used for the same effect, doing direct recursion inside
|
||||
the macro guarded by this transformer is often easier because one is not
|
||||
restricted to passing a single syntax tree. Modelling this helper as a
|
||||
transformer and not just a monadic action ensures that the current macro
|
||||
scope before the recursive call is restored after it, as expected. -/
|
||||
(withFreshMacroScope {α : Type} : m α → m α)
|
||||
export MonadQuotation
|
||||
|
||||
-- TODO: try harder to avoid clashes with other autogenerated names
|
||||
def addMacroScope (n : Name) (scp : MacroScope) : Name :=
|
||||
mkNameNum n scp
|
||||
|
||||
def addMacroScopes (n : Name) (scps : List MacroScope) : Name :=
|
||||
scps.foldl addMacroScope n
|
||||
|
||||
abbrev MacroM := ReaderT MacroScope (OptionT Id)
|
||||
|
||||
instance MacroM.monadQuotation : MonadQuotation MacroM :=
|
||||
{ getCurrMacroScope := fun scp => some scp,
|
||||
withFreshMacroScope := fun _ x => x }
|
||||
|
||||
abbrev Macro := Syntax → MacroM Syntax
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -52,7 +52,6 @@ extern lean_object* l_Lean_mkTagDeclarationExtension___closed__1;
|
|||
lean_object* l_Lean_registerEnumAttributes___rarg___lambda__2___closed__3;
|
||||
lean_object* l_Lean_ParametricAttribute_setParam___rarg___closed__2;
|
||||
lean_object* l_Lean_attributeExtension___elambda__4___rarg(lean_object*);
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Lean_ParametricAttribute_Inhabited(lean_object*);
|
||||
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkAttributeExtension___closed__2;
|
||||
|
|
@ -246,6 +245,7 @@ extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed_
|
|||
lean_object* l_Lean_mkAttributeImplBuilderTable___closed__1;
|
||||
lean_object* l_Array_qsortAux___main___at_Lean_registerEnumAttributes___spec__2(lean_object*);
|
||||
lean_object* l_Array_qsortAux___main___at_Lean_registerEnumAttributes___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
|
||||
lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
|
||||
uint8_t l_PersistentHashMap_containsAux___main___at_Lean_registerBuiltinAttribute___spec__2(lean_object*, size_t, lean_object*);
|
||||
|
|
@ -10924,7 +10924,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
if (lean_obj_tag(x_13) == 3)
|
||||
|
|
|
|||
|
|
@ -28,7 +28,6 @@ extern lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerTagAttri
|
|||
uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_mkProjectionFnInfoExtension___closed__3;
|
||||
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Lean_ExternAttrData_inhabited___closed__1;
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
extern lean_object* l_Lean_registerTagAttribute___closed__1;
|
||||
|
|
@ -109,6 +108,7 @@ extern lean_object* l_Option_HasRepr___rarg___closed__3;
|
|||
lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData(lean_object*);
|
||||
lean_object* lean_get_extern_attr_data(lean_object*, lean_object*);
|
||||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
|
||||
lean_object* l_RBNode_find___main___at_Lean_getExternAttrData___spec__2(lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
|
|
@ -266,7 +266,7 @@ x_5 = lean_nat_dec_eq(x_2, x_4);
|
|||
if (x_5 == 0)
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7;
|
||||
x_6 = l_Lean_stxInh;
|
||||
x_6 = l_Lean_Syntax_inhabited;
|
||||
x_7 = lean_array_get(x_6, x_1, x_2);
|
||||
if (lean_obj_tag(x_7) == 3)
|
||||
{
|
||||
|
|
@ -596,7 +596,7 @@ x_6 = lean_nat_dec_eq(x_4, x_5);
|
|||
if (x_6 == 0)
|
||||
{
|
||||
lean_object* x_7; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
|
||||
x_36 = l_Lean_stxInh;
|
||||
x_36 = l_Lean_Syntax_inhabited;
|
||||
x_37 = lean_array_get(x_36, x_3, x_5);
|
||||
x_38 = l_Lean_numLitKind;
|
||||
x_39 = l_Lean_Syntax_isNatLitAux(x_38, x_37);
|
||||
|
|
@ -628,7 +628,7 @@ lean_inc(x_8);
|
|||
x_9 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_9);
|
||||
lean_dec(x_7);
|
||||
x_10 = l_Lean_stxInh;
|
||||
x_10 = l_Lean_Syntax_inhabited;
|
||||
x_11 = lean_array_get(x_10, x_3, x_9);
|
||||
x_12 = l_Lean_Syntax_isStrLit_x3f(x_11);
|
||||
lean_dec(x_11);
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Name_isInternal___boxed(lean_object*);
|
||||
lean_object* l_Lean_NameSet_HasEmptyc;
|
||||
lean_object* l_Lean_Name_isPrefixOf___main___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_HasBeq;
|
||||
uint8_t l_Lean_Name_DecidableRel(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_quickLt___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_getNumParts___main___boxed(lean_object*);
|
||||
|
|
@ -103,7 +102,6 @@ lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1(lean_object*)
|
|||
lean_object* l_Lean_Name_getPrefix___boxed(lean_object*);
|
||||
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_components_x27___main(lean_object*);
|
||||
lean_object* l_Lean_Name_beq___boxed(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Name_isAnonymous(lean_object*);
|
||||
lean_object* l_RBNode_ins___main___at_Lean_NameSet_insert___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_NameSet_Inhabited;
|
||||
|
|
@ -112,7 +110,6 @@ lean_object* l_Lean_Name_replacePrefix___boxed(lean_object*, lean_object*, lean_
|
|||
lean_object* l_List_foldl___main___at_String_toName___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_getPrefix(lean_object*);
|
||||
lean_object* l_RBNode_setBlack___rarg(lean_object*);
|
||||
lean_object* l_Lean_Name_HasBeq___closed__1;
|
||||
lean_object* l_Lean_Name_append___main___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_String_trim(lean_object*);
|
||||
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
|
||||
|
|
@ -314,33 +311,6 @@ x_3 = l_List_reverse___rarg(x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = lean_name_eq(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_4 = lean_box(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Name_HasBeq___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Name_beq___boxed), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Name_HasBeq() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Name_HasBeq___closed__1;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
uint8_t l_Lean_Name_eqStr(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -8997,10 +8967,6 @@ l_Lean_stringToName___closed__1 = _init_l_Lean_stringToName___closed__1();
|
|||
lean_mark_persistent(l_Lean_stringToName___closed__1);
|
||||
l_Lean_stringToName = _init_l_Lean_stringToName();
|
||||
lean_mark_persistent(l_Lean_stringToName);
|
||||
l_Lean_Name_HasBeq___closed__1 = _init_l_Lean_Name_HasBeq___closed__1();
|
||||
lean_mark_persistent(l_Lean_Name_HasBeq___closed__1);
|
||||
l_Lean_Name_HasBeq = _init_l_Lean_Name_HasBeq();
|
||||
lean_mark_persistent(l_Lean_Name_HasBeq);
|
||||
l_Lean_Name_HasAppend___closed__1 = _init_l_Lean_Name_HasAppend___closed__1();
|
||||
lean_mark_persistent(l_Lean_Name_HasAppend___closed__1);
|
||||
l_Lean_Name_HasAppend = _init_l_Lean_Name_HasAppend();
|
||||
|
|
|
|||
|
|
@ -246,7 +246,6 @@ lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__11;
|
|||
lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__2;
|
||||
extern lean_object* l_Lean_Expr_heq_x3f___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabDiv___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabWhere___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabDollarProj(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -277,6 +276,7 @@ extern lean_object* l___private_Init_Lean_Elab_Quotation_4__quoteOption___rarg__
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv___closed__3;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_13__letBindRhss___main___closed__15;
|
||||
lean_object* l_Lean_Elab_Term_elabMapRev___closed__1;
|
||||
|
|
@ -2537,7 +2537,7 @@ lean_ctor_set(x_60, 0, x_1);
|
|||
lean_ctor_set(x_60, 1, x_59);
|
||||
lean_ctor_set(x_3, 8, x_60);
|
||||
x_61 = 1;
|
||||
x_62 = l_Lean_Elab_Term_elabTerm(x_57, x_2, x_61, x_61, x_3, x_26);
|
||||
x_62 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_61, x_61, x_57, x_3, x_26);
|
||||
return x_62;
|
||||
}
|
||||
else
|
||||
|
|
@ -2581,7 +2581,7 @@ lean_ctor_set(x_75, 8, x_74);
|
|||
lean_ctor_set(x_75, 9, x_72);
|
||||
lean_ctor_set_uint8(x_75, sizeof(void*)*10, x_73);
|
||||
x_76 = 1;
|
||||
x_77 = l_Lean_Elab_Term_elabTerm(x_57, x_2, x_76, x_76, x_75, x_26);
|
||||
x_77 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_76, x_76, x_57, x_75, x_26);
|
||||
return x_77;
|
||||
}
|
||||
}
|
||||
|
|
@ -5294,7 +5294,7 @@ x_12 = lean_array_push(x_11, x_9);
|
|||
x_13 = l_Array_iterateMAux___main___at_Lean_mkAppStx___spec__1(x_12, x_12, x_6, x_1);
|
||||
lean_dec(x_12);
|
||||
x_14 = 1;
|
||||
x_15 = l_Lean_Elab_Term_elabTerm(x_13, x_3, x_14, x_14, x_4, x_5);
|
||||
x_15 = l_Lean_Elab_Term_elabTermAux___main(x_3, x_14, x_14, x_13, x_4, x_5);
|
||||
return x_15;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -15,6 +15,7 @@ extern "C" {
|
|||
#endif
|
||||
lean_object* l_Lean_Elab_Term_mkForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_extractMacroScopes(lean_object*);
|
||||
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unreachable_x21___rarg(lean_object*);
|
||||
|
|
@ -24,11 +25,13 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_collectUsedFVarsA
|
|||
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabDefLike___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabDefLike___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabDefLike___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__4;
|
||||
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Command_removeUnused___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
|
||||
lean_object* lean_local_ctx_erase(lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabDefVal___closed__2;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_compileDecl(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -43,9 +46,11 @@ lean_object* l___private_Init_Lean_Elab_Term_20__synthesizeSyntheticMVarsAux___m
|
|||
lean_object* l_Lean_Elab_Command_collectUsedFVarsAtFVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Elab_Command_DefKind_isExample(uint8_t);
|
||||
lean_object* l_Lean_Name_getNumParts___main(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkFreshTypeMVar(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Command_removeUnused___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDeclName(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_collectUsedFVarsAtFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -60,12 +65,13 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_DefKind_isTheorem___boxed(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Term_14__resumePostponed___lambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_Command_11__getVarDecls(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getId(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabDefLike___spec__4(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef___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*);
|
||||
|
|
@ -74,6 +80,7 @@ lean_object* l_Lean_Elab_Command_withUsedWhen(lean_object*);
|
|||
lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Term_elabTypeStx___rarg___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_collectUsedFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_Definition_1__regTraceClasses(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_withUsedWhen___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -99,7 +106,10 @@ lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Elab_Command_removeUnused___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__3;
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__6;
|
||||
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__5;
|
||||
uint8_t l_Lean_Syntax_isNone(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_mkDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_applyAttributes___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1347,6 +1357,42 @@ lean_ctor_set_uint32(x_2, 0, x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("definition");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
x_2 = l_Lean_Elab_Command_mkDef___lambda__1___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("body");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Elab_Command_mkDef___lambda__1___closed__4;
|
||||
x_2 = l_Lean_Elab_Command_mkDef___lambda__1___closed__5;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_mkDef___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, uint8_t x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -1387,7 +1433,7 @@ lean_inc(x_11);
|
|||
x_22 = l_Lean_Elab_Term_mkLambda(x_1, x_10, x_20, x_11, x_21);
|
||||
if (lean_obj_tag(x_22) == 0)
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73;
|
||||
x_23 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get(x_22, 1);
|
||||
|
|
@ -1416,312 +1462,265 @@ lean_inc(x_33);
|
|||
lean_dec(x_31);
|
||||
lean_inc(x_11);
|
||||
x_34 = l_Lean_Elab_Term_instantiateMVars(x_5, x_29, x_11, x_33);
|
||||
x_35 = !lean_is_exclusive(x_34);
|
||||
if (x_35 == 0)
|
||||
{
|
||||
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
|
||||
x_36 = lean_ctor_get(x_34, 0);
|
||||
x_37 = lean_ctor_get(x_34, 1);
|
||||
x_38 = l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
|
||||
lean_inc(x_32);
|
||||
x_39 = l_Lean_CollectLevelParams_main___main(x_32, x_38);
|
||||
x_35 = lean_ctor_get(x_34, 0);
|
||||
lean_inc(x_35);
|
||||
x_36 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_36);
|
||||
x_40 = l_Lean_CollectLevelParams_main___main(x_36, x_39);
|
||||
x_41 = lean_ctor_get(x_40, 2);
|
||||
lean_inc(x_41);
|
||||
lean_dec(x_40);
|
||||
x_42 = l_Lean_Elab_Command_sortDeclLevelParams(x_6, x_41);
|
||||
if (lean_is_exclusive(x_34)) {
|
||||
lean_ctor_release(x_34, 0);
|
||||
lean_ctor_release(x_34, 1);
|
||||
x_37 = x_34;
|
||||
} else {
|
||||
lean_dec_ref(x_34);
|
||||
x_37 = lean_box(0);
|
||||
}
|
||||
x_69 = l_Lean_Elab_Term_getOptions(x_11, x_36);
|
||||
x_70 = lean_ctor_get(x_69, 0);
|
||||
lean_inc(x_70);
|
||||
x_71 = lean_ctor_get(x_69, 1);
|
||||
lean_inc(x_71);
|
||||
lean_dec(x_69);
|
||||
x_72 = l_Lean_Elab_Command_mkDef___lambda__1___closed__6;
|
||||
x_73 = l_Lean_checkTraceOption(x_70, x_72);
|
||||
lean_dec(x_70);
|
||||
if (x_73 == 0)
|
||||
{
|
||||
x_38 = x_71;
|
||||
goto block_68;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_74; lean_object* x_75; lean_object* x_76;
|
||||
lean_inc(x_35);
|
||||
x_74 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_74, 0, x_35);
|
||||
x_75 = l_Lean_Elab_Term_logTrace(x_72, x_1, x_74, x_11, x_71);
|
||||
x_76 = lean_ctor_get(x_75, 1);
|
||||
lean_inc(x_76);
|
||||
lean_dec(x_75);
|
||||
x_38 = x_76;
|
||||
goto block_68;
|
||||
}
|
||||
block_68:
|
||||
{
|
||||
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
|
||||
x_39 = l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
|
||||
lean_inc(x_32);
|
||||
x_40 = l_Lean_CollectLevelParams_main___main(x_32, x_39);
|
||||
lean_inc(x_35);
|
||||
x_41 = l_Lean_CollectLevelParams_main___main(x_35, x_40);
|
||||
x_42 = lean_ctor_get(x_41, 2);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_41);
|
||||
x_43 = l_Lean_Elab_Command_sortDeclLevelParams(x_6, x_42);
|
||||
switch (x_7) {
|
||||
case 0:
|
||||
{
|
||||
lean_object* x_43; lean_object* x_44; uint8_t x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
|
||||
lean_object* x_44; lean_object* x_45; uint8_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
|
||||
lean_dec(x_11);
|
||||
x_43 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_43, 0, x_8);
|
||||
lean_ctor_set(x_43, 1, x_42);
|
||||
lean_ctor_set(x_43, 2, x_32);
|
||||
x_44 = lean_ctor_get(x_9, 1);
|
||||
x_45 = lean_ctor_get_uint8(x_44, sizeof(void*)*2 + 3);
|
||||
x_46 = l_Lean_Elab_Command_mkDef___lambda__1___closed__2;
|
||||
x_47 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_47, 0, x_43);
|
||||
lean_ctor_set(x_47, 1, x_36);
|
||||
lean_ctor_set(x_47, 2, x_46);
|
||||
lean_ctor_set_uint8(x_47, sizeof(void*)*3, x_45);
|
||||
x_48 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_48, 0, x_47);
|
||||
x_44 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_44, 0, x_8);
|
||||
lean_ctor_set(x_44, 1, x_43);
|
||||
lean_ctor_set(x_44, 2, x_32);
|
||||
x_45 = lean_ctor_get(x_9, 1);
|
||||
x_46 = lean_ctor_get_uint8(x_45, sizeof(void*)*2 + 3);
|
||||
x_47 = l_Lean_Elab_Command_mkDef___lambda__1___closed__2;
|
||||
x_48 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_48, 0, x_44);
|
||||
lean_ctor_set(x_48, 1, x_35);
|
||||
lean_ctor_set(x_48, 2, x_47);
|
||||
lean_ctor_set_uint8(x_48, sizeof(void*)*3, x_46);
|
||||
x_49 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_49, 0, x_48);
|
||||
lean_ctor_set(x_34, 0, x_49);
|
||||
return x_34;
|
||||
x_50 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_50, 0, x_49);
|
||||
if (lean_is_scalar(x_37)) {
|
||||
x_51 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_51 = x_37;
|
||||
}
|
||||
lean_ctor_set(x_51, 0, x_50);
|
||||
lean_ctor_set(x_51, 1, x_38);
|
||||
return x_51;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
|
||||
lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57;
|
||||
lean_dec(x_11);
|
||||
x_50 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_50, 0, x_8);
|
||||
lean_ctor_set(x_50, 1, x_42);
|
||||
lean_ctor_set(x_50, 2, x_32);
|
||||
x_51 = lean_task_pure(x_36);
|
||||
x_52 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_52, 0, x_50);
|
||||
lean_ctor_set(x_52, 1, x_51);
|
||||
x_53 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_53, 0, x_52);
|
||||
x_54 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_54, 0, x_53);
|
||||
lean_ctor_set(x_34, 0, x_54);
|
||||
return x_34;
|
||||
x_52 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_52, 0, x_8);
|
||||
lean_ctor_set(x_52, 1, x_43);
|
||||
lean_ctor_set(x_52, 2, x_32);
|
||||
x_53 = lean_task_pure(x_35);
|
||||
x_54 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_54, 0, x_52);
|
||||
lean_ctor_set(x_54, 1, x_53);
|
||||
x_55 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_55, 0, x_54);
|
||||
x_56 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_56, 0, x_55);
|
||||
if (lean_is_scalar(x_37)) {
|
||||
x_57 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_57 = x_37;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* x_55; lean_object* x_56; lean_object* x_57;
|
||||
lean_dec(x_42);
|
||||
lean_free_object(x_34);
|
||||
lean_dec(x_36);
|
||||
lean_dec(x_32);
|
||||
lean_dec(x_8);
|
||||
x_55 = l___private_Init_Lean_Elab_Term_14__resumePostponed___lambda__1___closed__1;
|
||||
x_56 = l_unreachable_x21___rarg(x_55);
|
||||
x_57 = lean_apply_2(x_56, x_11, x_37);
|
||||
lean_ctor_set(x_57, 0, x_56);
|
||||
lean_ctor_set(x_57, 1, x_38);
|
||||
return x_57;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_58; lean_object* x_59; uint8_t x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
lean_dec(x_11);
|
||||
x_58 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_58, 0, x_8);
|
||||
lean_ctor_set(x_58, 1, x_42);
|
||||
lean_ctor_set(x_58, 2, x_32);
|
||||
x_59 = lean_ctor_get(x_9, 1);
|
||||
x_60 = lean_ctor_get_uint8(x_59, sizeof(void*)*2 + 3);
|
||||
x_61 = lean_alloc_ctor(0, 2, 1);
|
||||
lean_ctor_set(x_61, 0, x_58);
|
||||
lean_ctor_set(x_61, 1, x_36);
|
||||
lean_ctor_set_uint8(x_61, sizeof(void*)*2, x_60);
|
||||
x_62 = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(x_62, 0, x_61);
|
||||
x_63 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_63, 0, x_62);
|
||||
lean_ctor_set(x_34, 0, x_63);
|
||||
return x_34;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70;
|
||||
x_64 = lean_ctor_get(x_34, 0);
|
||||
x_65 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_65);
|
||||
lean_inc(x_64);
|
||||
lean_dec(x_34);
|
||||
x_66 = l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
|
||||
lean_inc(x_32);
|
||||
x_67 = l_Lean_CollectLevelParams_main___main(x_32, x_66);
|
||||
lean_inc(x_64);
|
||||
x_68 = l_Lean_CollectLevelParams_main___main(x_64, x_67);
|
||||
x_69 = lean_ctor_get(x_68, 2);
|
||||
lean_inc(x_69);
|
||||
lean_dec(x_68);
|
||||
x_70 = l_Lean_Elab_Command_sortDeclLevelParams(x_6, x_69);
|
||||
switch (x_7) {
|
||||
case 0:
|
||||
{
|
||||
lean_object* x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
|
||||
lean_dec(x_11);
|
||||
x_71 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_71, 0, x_8);
|
||||
lean_ctor_set(x_71, 1, x_70);
|
||||
lean_ctor_set(x_71, 2, x_32);
|
||||
x_72 = lean_ctor_get(x_9, 1);
|
||||
x_73 = lean_ctor_get_uint8(x_72, sizeof(void*)*2 + 3);
|
||||
x_74 = l_Lean_Elab_Command_mkDef___lambda__1___closed__2;
|
||||
x_75 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_75, 0, x_71);
|
||||
lean_ctor_set(x_75, 1, x_64);
|
||||
lean_ctor_set(x_75, 2, x_74);
|
||||
lean_ctor_set_uint8(x_75, sizeof(void*)*3, x_73);
|
||||
x_76 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_76, 0, x_75);
|
||||
x_77 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_77, 0, x_76);
|
||||
x_78 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_78, 0, x_77);
|
||||
lean_ctor_set(x_78, 1, x_65);
|
||||
return x_78;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84;
|
||||
lean_dec(x_11);
|
||||
x_79 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_79, 0, x_8);
|
||||
lean_ctor_set(x_79, 1, x_70);
|
||||
lean_ctor_set(x_79, 2, x_32);
|
||||
x_80 = lean_task_pure(x_64);
|
||||
x_81 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_81, 0, x_79);
|
||||
lean_ctor_set(x_81, 1, x_80);
|
||||
x_82 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_82, 0, x_81);
|
||||
x_83 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_83, 0, x_82);
|
||||
x_84 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_84, 0, x_83);
|
||||
lean_ctor_set(x_84, 1, x_65);
|
||||
return x_84;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* x_85; lean_object* x_86; lean_object* x_87;
|
||||
lean_dec(x_70);
|
||||
lean_dec(x_64);
|
||||
lean_object* x_58; lean_object* x_59; lean_object* x_60;
|
||||
lean_dec(x_43);
|
||||
lean_dec(x_37);
|
||||
lean_dec(x_35);
|
||||
lean_dec(x_32);
|
||||
lean_dec(x_8);
|
||||
x_85 = l___private_Init_Lean_Elab_Term_14__resumePostponed___lambda__1___closed__1;
|
||||
x_86 = l_unreachable_x21___rarg(x_85);
|
||||
x_87 = lean_apply_2(x_86, x_11, x_65);
|
||||
return x_87;
|
||||
x_58 = l___private_Init_Lean_Elab_Term_14__resumePostponed___lambda__1___closed__1;
|
||||
x_59 = l_unreachable_x21___rarg(x_58);
|
||||
x_60 = lean_apply_2(x_59, x_11, x_38);
|
||||
return x_60;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_88; lean_object* x_89; uint8_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
|
||||
lean_object* x_61; lean_object* x_62; uint8_t x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
|
||||
lean_dec(x_11);
|
||||
x_88 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_88, 0, x_8);
|
||||
lean_ctor_set(x_88, 1, x_70);
|
||||
lean_ctor_set(x_88, 2, x_32);
|
||||
x_89 = lean_ctor_get(x_9, 1);
|
||||
x_90 = lean_ctor_get_uint8(x_89, sizeof(void*)*2 + 3);
|
||||
x_91 = lean_alloc_ctor(0, 2, 1);
|
||||
lean_ctor_set(x_91, 0, x_88);
|
||||
lean_ctor_set(x_91, 1, x_64);
|
||||
lean_ctor_set_uint8(x_91, sizeof(void*)*2, x_90);
|
||||
x_92 = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(x_92, 0, x_91);
|
||||
x_93 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_93, 0, x_92);
|
||||
x_94 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_94, 0, x_93);
|
||||
lean_ctor_set(x_94, 1, x_65);
|
||||
return x_94;
|
||||
x_61 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_61, 0, x_8);
|
||||
lean_ctor_set(x_61, 1, x_43);
|
||||
lean_ctor_set(x_61, 2, x_32);
|
||||
x_62 = lean_ctor_get(x_9, 1);
|
||||
x_63 = lean_ctor_get_uint8(x_62, sizeof(void*)*2 + 3);
|
||||
x_64 = lean_alloc_ctor(0, 2, 1);
|
||||
lean_ctor_set(x_64, 0, x_61);
|
||||
lean_ctor_set(x_64, 1, x_35);
|
||||
lean_ctor_set_uint8(x_64, sizeof(void*)*2, x_63);
|
||||
x_65 = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(x_65, 0, x_64);
|
||||
x_66 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_66, 0, x_65);
|
||||
if (lean_is_scalar(x_37)) {
|
||||
x_67 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_67 = x_37;
|
||||
}
|
||||
lean_ctor_set(x_67, 0, x_66);
|
||||
lean_ctor_set(x_67, 1, x_38);
|
||||
return x_67;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_95;
|
||||
uint8_t x_77;
|
||||
lean_dec(x_17);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
x_95 = !lean_is_exclusive(x_22);
|
||||
if (x_95 == 0)
|
||||
x_77 = !lean_is_exclusive(x_22);
|
||||
if (x_77 == 0)
|
||||
{
|
||||
return x_22;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_96; lean_object* x_97; lean_object* x_98;
|
||||
x_96 = lean_ctor_get(x_22, 0);
|
||||
x_97 = lean_ctor_get(x_22, 1);
|
||||
lean_inc(x_97);
|
||||
lean_inc(x_96);
|
||||
lean_object* x_78; lean_object* x_79; lean_object* x_80;
|
||||
x_78 = lean_ctor_get(x_22, 0);
|
||||
x_79 = lean_ctor_get(x_22, 1);
|
||||
lean_inc(x_79);
|
||||
lean_inc(x_78);
|
||||
lean_dec(x_22);
|
||||
x_98 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_98, 0, x_96);
|
||||
lean_ctor_set(x_98, 1, x_97);
|
||||
return x_98;
|
||||
x_80 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_80, 0, x_78);
|
||||
lean_ctor_set(x_80, 1, x_79);
|
||||
return x_80;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_99;
|
||||
uint8_t x_81;
|
||||
lean_dec(x_17);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
x_99 = !lean_is_exclusive(x_19);
|
||||
if (x_99 == 0)
|
||||
x_81 = !lean_is_exclusive(x_19);
|
||||
if (x_81 == 0)
|
||||
{
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_100; lean_object* x_101; lean_object* x_102;
|
||||
x_100 = lean_ctor_get(x_19, 0);
|
||||
x_101 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_101);
|
||||
lean_inc(x_100);
|
||||
lean_object* x_82; lean_object* x_83; lean_object* x_84;
|
||||
x_82 = lean_ctor_get(x_19, 0);
|
||||
x_83 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_83);
|
||||
lean_inc(x_82);
|
||||
lean_dec(x_19);
|
||||
x_102 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_102, 0, x_100);
|
||||
lean_ctor_set(x_102, 1, x_101);
|
||||
return x_102;
|
||||
x_84 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_84, 0, x_82);
|
||||
lean_ctor_set(x_84, 1, x_83);
|
||||
return x_84;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_103;
|
||||
uint8_t x_85;
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_103 = !lean_is_exclusive(x_16);
|
||||
if (x_103 == 0)
|
||||
x_85 = !lean_is_exclusive(x_16);
|
||||
if (x_85 == 0)
|
||||
{
|
||||
return x_16;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_104; lean_object* x_105; lean_object* x_106;
|
||||
x_104 = lean_ctor_get(x_16, 0);
|
||||
x_105 = lean_ctor_get(x_16, 1);
|
||||
lean_inc(x_105);
|
||||
lean_inc(x_104);
|
||||
lean_object* x_86; lean_object* x_87; lean_object* x_88;
|
||||
x_86 = lean_ctor_get(x_16, 0);
|
||||
x_87 = lean_ctor_get(x_16, 1);
|
||||
lean_inc(x_87);
|
||||
lean_inc(x_86);
|
||||
lean_dec(x_16);
|
||||
x_106 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_106, 0, x_104);
|
||||
lean_ctor_set(x_106, 1, x_105);
|
||||
return x_106;
|
||||
x_88 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_88, 0, x_86);
|
||||
lean_ctor_set(x_88, 1, x_87);
|
||||
return x_88;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_107;
|
||||
uint8_t x_89;
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_107 = !lean_is_exclusive(x_13);
|
||||
if (x_107 == 0)
|
||||
x_89 = !lean_is_exclusive(x_13);
|
||||
if (x_89 == 0)
|
||||
{
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_108; lean_object* x_109; lean_object* x_110;
|
||||
x_108 = lean_ctor_get(x_13, 0);
|
||||
x_109 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_109);
|
||||
lean_inc(x_108);
|
||||
lean_object* x_90; lean_object* x_91; lean_object* x_92;
|
||||
x_90 = lean_ctor_get(x_13, 0);
|
||||
x_91 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_91);
|
||||
lean_inc(x_90);
|
||||
lean_dec(x_13);
|
||||
x_110 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_110, 0, x_108);
|
||||
lean_ctor_set(x_110, 1, x_109);
|
||||
return x_110;
|
||||
x_92 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_92, 0, x_90);
|
||||
lean_ctor_set(x_92, 1, x_91);
|
||||
return x_92;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2065,7 +2064,7 @@ lean_dec(x_1);
|
|||
x_15 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_15, 0, x_2);
|
||||
x_16 = 1;
|
||||
x_17 = l_Lean_Elab_Term_elabTerm(x_14, x_15, x_16, x_16, x_3, x_4);
|
||||
x_17 = l_Lean_Elab_Term_elabTermAux___main(x_15, x_16, x_16, x_14, x_3, x_4);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
|
|
@ -5683,6 +5682,62 @@ lean_dec(x_2);
|
|||
return x_10;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Elab_Definition_1__regTraceClasses(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_Elab_Command_mkDef___lambda__1___closed__4;
|
||||
x_3 = l_Lean_registerTraceClass(x_2, x_1);
|
||||
if (lean_obj_tag(x_3) == 0)
|
||||
{
|
||||
uint8_t x_4;
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_3, 0);
|
||||
lean_dec(x_5);
|
||||
x_6 = lean_box(0);
|
||||
lean_ctor_set(x_3, 0, x_6);
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9;
|
||||
x_7 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_3);
|
||||
x_8 = lean_box(0);
|
||||
x_9 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_9, 0, x_8);
|
||||
lean_ctor_set(x_9, 1, x_7);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_10;
|
||||
x_10 = !lean_is_exclusive(x_3);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = lean_ctor_get(x_3, 0);
|
||||
x_12 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_12);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_3);
|
||||
x_13 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_13, 0, x_11);
|
||||
lean_ctor_set(x_13, 1, x_12);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init_Lean_Util_CollectLevelParams(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Util_CollectFVars(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Elab_DeclModifiers(lean_object*);
|
||||
|
|
@ -5710,12 +5765,23 @@ l_Lean_Elab_Command_mkDef___lambda__1___closed__1 = _init_l_Lean_Elab_Command_mk
|
|||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__1);
|
||||
l_Lean_Elab_Command_mkDef___lambda__1___closed__2 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__2);
|
||||
l_Lean_Elab_Command_mkDef___lambda__1___closed__3 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__3);
|
||||
l_Lean_Elab_Command_mkDef___lambda__1___closed__4 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__4);
|
||||
l_Lean_Elab_Command_mkDef___lambda__1___closed__5 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__5);
|
||||
l_Lean_Elab_Command_mkDef___lambda__1___closed__6 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__6);
|
||||
l_Lean_Elab_Command_elabDefVal___closed__1 = _init_l_Lean_Elab_Command_elabDefVal___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_elabDefVal___closed__1);
|
||||
l_Lean_Elab_Command_elabDefVal___closed__2 = _init_l_Lean_Elab_Command_elabDefVal___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_elabDefVal___closed__2);
|
||||
l_Lean_Elab_Command_elabDefVal___closed__3 = _init_l_Lean_Elab_Command_elabDefVal___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_elabDefVal___closed__3);
|
||||
res = l___private_Init_Lean_Elab_Definition_1__regTraceClasses(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_mk_io_result(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
|
|
@ -43,8 +43,8 @@ lean_object* l_Lean_Parser_parseCommand___main(lean_object*, lean_object*, lean_
|
|||
lean_object* l_Lean_Elab_Frontend_processCommandsAux___boxed(lean_object*);
|
||||
extern lean_object* l_PersistentArray_empty___closed__3;
|
||||
lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabCommand___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Frontend_updateCmdPos(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Frontend_processCommand(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Frontend_processCommandsAux___main(lean_object*);
|
||||
lean_object* l_Lean_Elab_Frontend_liftIOCore_x21___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -376,7 +376,7 @@ lean_ctor_set(x_14, 4, x_6);
|
|||
lean_ctor_set(x_14, 5, x_12);
|
||||
lean_ctor_set(x_14, 6, x_13);
|
||||
lean_inc(x_14);
|
||||
x_15 = l_Lean_Elab_Command_elabCommand(x_1, x_14, x_7);
|
||||
x_15 = l_Lean_Elab_Command_elabCommand___main(x_1, x_14, x_7);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
uint8_t x_16;
|
||||
|
|
@ -683,7 +683,7 @@ lean_ctor_set(x_90, 4, x_82);
|
|||
lean_ctor_set(x_90, 5, x_88);
|
||||
lean_ctor_set(x_90, 6, x_89);
|
||||
lean_inc(x_90);
|
||||
x_91 = l_Lean_Elab_Command_elabCommand(x_1, x_90, x_83);
|
||||
x_91 = l_Lean_Elab_Command_elabCommand___main(x_1, x_90, x_83);
|
||||
if (lean_obj_tag(x_91) == 0)
|
||||
{
|
||||
uint8_t x_92;
|
||||
|
|
|
|||
|
|
@ -18,7 +18,6 @@ lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
|
|||
lean_object* lean_io_error_to_string(lean_object*);
|
||||
lean_object* l_List_map___main___at_Lean_Elab_headerToImports___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_List_append___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_headerToImports___closed__2;
|
||||
lean_object* l_Lean_Elab_headerToImports(lean_object*);
|
||||
|
|
@ -41,6 +40,7 @@ lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_FileMap_ofString(lean_object*);
|
||||
lean_object* lean_mk_empty_environment(uint32_t, lean_object*);
|
||||
lean_object* lean_import_modules(lean_object*, uint32_t, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
extern lean_object* l_Lean_normalizeModuleName___closed__1;
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* lean_parse_imports(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -200,7 +200,7 @@ x_2 = l_Lean_Syntax_asNode(x_1);
|
|||
x_3 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_3);
|
||||
lean_dec(x_2);
|
||||
x_4 = l_Lean_stxInh;
|
||||
x_4 = l_Lean_Syntax_inhabited;
|
||||
x_5 = lean_unsigned_to_nat(0u);
|
||||
x_6 = lean_array_get(x_4, x_3, x_5);
|
||||
x_7 = l_Lean_Syntax_isNone(x_6);
|
||||
|
|
|
|||
|
|
@ -112,7 +112,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_8__getHeadInfo___lambda__4___b
|
|||
lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__3;
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_8__getHeadInfo___spec__2___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabStxQuot___closed__1;
|
||||
extern lean_object* l_PersistentHashMap_mkCollisionNode___rarg___closed__1;
|
||||
|
|
@ -463,6 +462,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_10__compileStxMatch___main___c
|
|||
lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__14;
|
||||
lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__28;
|
||||
extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l___private_Init_Lean_Elab_Quotation_9__explodeHeadPat___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_Quotation_6__quoteSyntax___main___closed__15;
|
||||
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_10__compileStxMatch___main___spec__8___closed__8;
|
||||
|
|
@ -2273,7 +2273,7 @@ return x_8;
|
|||
else
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
|
||||
x_9 = l_Lean_stxInh;
|
||||
x_9 = l_Lean_Syntax_inhabited;
|
||||
x_10 = lean_unsigned_to_nat(2u);
|
||||
x_11 = lean_array_get(x_9, x_3, x_10);
|
||||
x_12 = l_Lean_Syntax_isNone(x_11);
|
||||
|
|
@ -6059,7 +6059,7 @@ _start:
|
|||
if (lean_obj_tag(x_1) == 0)
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l_Lean_stxInh;
|
||||
x_2 = l_Lean_Syntax_inhabited;
|
||||
x_3 = l_List_head_x21___rarg___closed__2;
|
||||
x_4 = lean_panic_fn(x_2, x_3);
|
||||
return x_4;
|
||||
|
|
@ -7546,7 +7546,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_List_Monad;
|
||||
x_2 = l_Lean_stxInh;
|
||||
x_2 = l_Lean_Syntax_inhabited;
|
||||
x_3 = l_monadInhabited___rarg(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -7556,7 +7556,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_List_head_x21___at___private_Init_Lean_Elab_Quotation_10__compileStxMatch___main___spec__2___closed__1;
|
||||
x_2 = l_Lean_stxInh;
|
||||
x_2 = l_Lean_Syntax_inhabited;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
|
|
@ -12047,7 +12047,7 @@ return x_18;
|
|||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; uint8_t x_41;
|
||||
x_19 = l_Lean_stxInh;
|
||||
x_19 = l_Lean_Syntax_inhabited;
|
||||
x_20 = lean_unsigned_to_nat(1u);
|
||||
x_21 = lean_array_get(x_19, x_4, x_20);
|
||||
x_22 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
|
|
@ -15645,7 +15645,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Name_inhabited;
|
||||
x_2 = l_Lean_stxInh;
|
||||
x_2 = l_Lean_Syntax_inhabited;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
|
|
@ -15967,7 +15967,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_197 = l_Lean_stxInh;
|
||||
x_197 = l_Lean_Syntax_inhabited;
|
||||
x_198 = lean_unsigned_to_nat(0u);
|
||||
x_199 = lean_array_get(x_197, x_4, x_198);
|
||||
x_200 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -15995,7 +15995,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_207 = l_Lean_stxInh;
|
||||
x_207 = l_Lean_Syntax_inhabited;
|
||||
x_208 = lean_unsigned_to_nat(0u);
|
||||
x_209 = lean_array_get(x_207, x_4, x_208);
|
||||
x_210 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -16023,7 +16023,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_217 = l_Lean_stxInh;
|
||||
x_217 = l_Lean_Syntax_inhabited;
|
||||
x_218 = lean_unsigned_to_nat(1u);
|
||||
x_219 = lean_array_get(x_217, x_4, x_218);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -16068,7 +16068,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_233 = l_Lean_stxInh;
|
||||
x_233 = l_Lean_Syntax_inhabited;
|
||||
x_234 = lean_unsigned_to_nat(2u);
|
||||
x_235 = lean_array_get(x_233, x_4, x_234);
|
||||
x_236 = lean_unsigned_to_nat(4u);
|
||||
|
|
@ -16099,7 +16099,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_245 = l_Lean_stxInh;
|
||||
x_245 = l_Lean_Syntax_inhabited;
|
||||
x_246 = lean_unsigned_to_nat(0u);
|
||||
x_247 = lean_array_get(x_245, x_4, x_246);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -16202,7 +16202,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_269 = l_Lean_stxInh;
|
||||
x_269 = l_Lean_Syntax_inhabited;
|
||||
x_270 = lean_unsigned_to_nat(1u);
|
||||
x_271 = lean_array_get(x_269, x_4, x_270);
|
||||
lean_inc(x_271);
|
||||
|
|
@ -16418,7 +16418,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_317 = l_Lean_stxInh;
|
||||
x_317 = l_Lean_Syntax_inhabited;
|
||||
x_318 = lean_unsigned_to_nat(1u);
|
||||
x_319 = lean_array_get(x_317, x_4, x_318);
|
||||
x_320 = l_Lean_Syntax_getArgs(x_319);
|
||||
|
|
@ -17470,7 +17470,7 @@ lean_free_object(x_116);
|
|||
lean_free_object(x_115);
|
||||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
x_627 = l_Lean_stxInh;
|
||||
x_627 = l_Lean_Syntax_inhabited;
|
||||
x_628 = lean_unsigned_to_nat(0u);
|
||||
x_629 = lean_array_get(x_627, x_4, x_628);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -18189,7 +18189,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_821 = l_Lean_stxInh;
|
||||
x_821 = l_Lean_Syntax_inhabited;
|
||||
x_822 = lean_unsigned_to_nat(0u);
|
||||
x_823 = lean_array_get(x_821, x_4, x_822);
|
||||
x_824 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -18216,7 +18216,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_831 = l_Lean_stxInh;
|
||||
x_831 = l_Lean_Syntax_inhabited;
|
||||
x_832 = lean_unsigned_to_nat(0u);
|
||||
x_833 = lean_array_get(x_831, x_4, x_832);
|
||||
x_834 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -18243,7 +18243,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_841 = l_Lean_stxInh;
|
||||
x_841 = l_Lean_Syntax_inhabited;
|
||||
x_842 = lean_unsigned_to_nat(1u);
|
||||
x_843 = lean_array_get(x_841, x_4, x_842);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -18287,7 +18287,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_857 = l_Lean_stxInh;
|
||||
x_857 = l_Lean_Syntax_inhabited;
|
||||
x_858 = lean_unsigned_to_nat(2u);
|
||||
x_859 = lean_array_get(x_857, x_4, x_858);
|
||||
x_860 = lean_unsigned_to_nat(4u);
|
||||
|
|
@ -18317,7 +18317,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_869 = l_Lean_stxInh;
|
||||
x_869 = l_Lean_Syntax_inhabited;
|
||||
x_870 = lean_unsigned_to_nat(0u);
|
||||
x_871 = lean_array_get(x_869, x_4, x_870);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -18421,7 +18421,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_891 = l_Lean_stxInh;
|
||||
x_891 = l_Lean_Syntax_inhabited;
|
||||
x_892 = lean_unsigned_to_nat(1u);
|
||||
x_893 = lean_array_get(x_891, x_4, x_892);
|
||||
lean_inc(x_893);
|
||||
|
|
@ -18636,7 +18636,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_939 = l_Lean_stxInh;
|
||||
x_939 = l_Lean_Syntax_inhabited;
|
||||
x_940 = lean_unsigned_to_nat(1u);
|
||||
x_941 = lean_array_get(x_939, x_4, x_940);
|
||||
x_942 = l_Lean_Syntax_getArgs(x_941);
|
||||
|
|
@ -19269,7 +19269,7 @@ lean_free_object(x_116);
|
|||
lean_free_object(x_115);
|
||||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
x_1132 = l_Lean_stxInh;
|
||||
x_1132 = l_Lean_Syntax_inhabited;
|
||||
x_1133 = lean_unsigned_to_nat(0u);
|
||||
x_1134 = lean_array_get(x_1132, x_4, x_1133);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -19964,7 +19964,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1294 = l_Lean_stxInh;
|
||||
x_1294 = l_Lean_Syntax_inhabited;
|
||||
x_1295 = lean_unsigned_to_nat(0u);
|
||||
x_1296 = lean_array_get(x_1294, x_4, x_1295);
|
||||
x_1297 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -19991,7 +19991,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1304 = l_Lean_stxInh;
|
||||
x_1304 = l_Lean_Syntax_inhabited;
|
||||
x_1305 = lean_unsigned_to_nat(0u);
|
||||
x_1306 = lean_array_get(x_1304, x_4, x_1305);
|
||||
x_1307 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -20018,7 +20018,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1314 = l_Lean_stxInh;
|
||||
x_1314 = l_Lean_Syntax_inhabited;
|
||||
x_1315 = lean_unsigned_to_nat(1u);
|
||||
x_1316 = lean_array_get(x_1314, x_4, x_1315);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -20062,7 +20062,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1330 = l_Lean_stxInh;
|
||||
x_1330 = l_Lean_Syntax_inhabited;
|
||||
x_1331 = lean_unsigned_to_nat(2u);
|
||||
x_1332 = lean_array_get(x_1330, x_4, x_1331);
|
||||
x_1333 = lean_unsigned_to_nat(4u);
|
||||
|
|
@ -20092,7 +20092,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1342 = l_Lean_stxInh;
|
||||
x_1342 = l_Lean_Syntax_inhabited;
|
||||
x_1343 = lean_unsigned_to_nat(0u);
|
||||
x_1344 = lean_array_get(x_1342, x_4, x_1343);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -20196,7 +20196,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1364 = l_Lean_stxInh;
|
||||
x_1364 = l_Lean_Syntax_inhabited;
|
||||
x_1365 = lean_unsigned_to_nat(1u);
|
||||
x_1366 = lean_array_get(x_1364, x_4, x_1365);
|
||||
lean_inc(x_1366);
|
||||
|
|
@ -20411,7 +20411,7 @@ lean_free_object(x_115);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1412 = l_Lean_stxInh;
|
||||
x_1412 = l_Lean_Syntax_inhabited;
|
||||
x_1413 = lean_unsigned_to_nat(1u);
|
||||
x_1414 = lean_array_get(x_1412, x_4, x_1413);
|
||||
x_1415 = l_Lean_Syntax_getArgs(x_1414);
|
||||
|
|
@ -21044,7 +21044,7 @@ lean_dec(x_1225);
|
|||
lean_free_object(x_115);
|
||||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
x_1605 = l_Lean_stxInh;
|
||||
x_1605 = l_Lean_Syntax_inhabited;
|
||||
x_1606 = lean_unsigned_to_nat(0u);
|
||||
x_1607 = lean_array_get(x_1605, x_4, x_1606);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -21772,7 +21772,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1773 = l_Lean_stxInh;
|
||||
x_1773 = l_Lean_Syntax_inhabited;
|
||||
x_1774 = lean_unsigned_to_nat(0u);
|
||||
x_1775 = lean_array_get(x_1773, x_4, x_1774);
|
||||
x_1776 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -21799,7 +21799,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1783 = l_Lean_stxInh;
|
||||
x_1783 = l_Lean_Syntax_inhabited;
|
||||
x_1784 = lean_unsigned_to_nat(0u);
|
||||
x_1785 = lean_array_get(x_1783, x_4, x_1784);
|
||||
x_1786 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -21826,7 +21826,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1793 = l_Lean_stxInh;
|
||||
x_1793 = l_Lean_Syntax_inhabited;
|
||||
x_1794 = lean_unsigned_to_nat(1u);
|
||||
x_1795 = lean_array_get(x_1793, x_4, x_1794);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -21870,7 +21870,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1809 = l_Lean_stxInh;
|
||||
x_1809 = l_Lean_Syntax_inhabited;
|
||||
x_1810 = lean_unsigned_to_nat(2u);
|
||||
x_1811 = lean_array_get(x_1809, x_4, x_1810);
|
||||
x_1812 = lean_unsigned_to_nat(4u);
|
||||
|
|
@ -21900,7 +21900,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1821 = l_Lean_stxInh;
|
||||
x_1821 = l_Lean_Syntax_inhabited;
|
||||
x_1822 = lean_unsigned_to_nat(0u);
|
||||
x_1823 = lean_array_get(x_1821, x_4, x_1822);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -22004,7 +22004,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1843 = l_Lean_stxInh;
|
||||
x_1843 = l_Lean_Syntax_inhabited;
|
||||
x_1844 = lean_unsigned_to_nat(1u);
|
||||
x_1845 = lean_array_get(x_1843, x_4, x_1844);
|
||||
lean_inc(x_1845);
|
||||
|
|
@ -22219,7 +22219,7 @@ lean_dec(x_1697);
|
|||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_1891 = l_Lean_stxInh;
|
||||
x_1891 = l_Lean_Syntax_inhabited;
|
||||
x_1892 = lean_unsigned_to_nat(1u);
|
||||
x_1893 = lean_array_get(x_1891, x_4, x_1892);
|
||||
x_1894 = l_Lean_Syntax_getArgs(x_1893);
|
||||
|
|
@ -22852,7 +22852,7 @@ lean_dec(x_1701);
|
|||
lean_dec(x_1697);
|
||||
lean_free_object(x_105);
|
||||
lean_dec(x_118);
|
||||
x_2084 = l_Lean_stxInh;
|
||||
x_2084 = l_Lean_Syntax_inhabited;
|
||||
x_2085 = lean_unsigned_to_nat(0u);
|
||||
x_2086 = lean_array_get(x_2084, x_4, x_2085);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -23612,7 +23612,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2259 = l_Lean_stxInh;
|
||||
x_2259 = l_Lean_Syntax_inhabited;
|
||||
x_2260 = lean_unsigned_to_nat(0u);
|
||||
x_2261 = lean_array_get(x_2259, x_4, x_2260);
|
||||
x_2262 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -23639,7 +23639,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2269 = l_Lean_stxInh;
|
||||
x_2269 = l_Lean_Syntax_inhabited;
|
||||
x_2270 = lean_unsigned_to_nat(0u);
|
||||
x_2271 = lean_array_get(x_2269, x_4, x_2270);
|
||||
x_2272 = lean_unsigned_to_nat(2u);
|
||||
|
|
@ -23666,7 +23666,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2279 = l_Lean_stxInh;
|
||||
x_2279 = l_Lean_Syntax_inhabited;
|
||||
x_2280 = lean_unsigned_to_nat(1u);
|
||||
x_2281 = lean_array_get(x_2279, x_4, x_2280);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -23710,7 +23710,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2295 = l_Lean_stxInh;
|
||||
x_2295 = l_Lean_Syntax_inhabited;
|
||||
x_2296 = lean_unsigned_to_nat(2u);
|
||||
x_2297 = lean_array_get(x_2295, x_4, x_2296);
|
||||
x_2298 = lean_unsigned_to_nat(4u);
|
||||
|
|
@ -23740,7 +23740,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2307 = l_Lean_stxInh;
|
||||
x_2307 = l_Lean_Syntax_inhabited;
|
||||
x_2308 = lean_unsigned_to_nat(0u);
|
||||
x_2309 = lean_array_get(x_2307, x_4, x_2308);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -23844,7 +23844,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2329 = l_Lean_stxInh;
|
||||
x_2329 = l_Lean_Syntax_inhabited;
|
||||
x_2330 = lean_unsigned_to_nat(1u);
|
||||
x_2331 = lean_array_get(x_2329, x_4, x_2330);
|
||||
lean_inc(x_2331);
|
||||
|
|
@ -24059,7 +24059,7 @@ lean_dec(x_2180);
|
|||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
lean_dec(x_1);
|
||||
x_2377 = l_Lean_stxInh;
|
||||
x_2377 = l_Lean_Syntax_inhabited;
|
||||
x_2378 = lean_unsigned_to_nat(1u);
|
||||
x_2379 = lean_array_get(x_2377, x_4, x_2378);
|
||||
x_2380 = l_Lean_Syntax_getArgs(x_2379);
|
||||
|
|
@ -24692,7 +24692,7 @@ lean_dec(x_2184);
|
|||
lean_dec(x_2180);
|
||||
lean_dec(x_2177);
|
||||
lean_dec(x_118);
|
||||
x_2570 = l_Lean_stxInh;
|
||||
x_2570 = l_Lean_Syntax_inhabited;
|
||||
x_2571 = lean_unsigned_to_nat(0u);
|
||||
x_2572 = lean_array_get(x_2570, x_4, x_2571);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -25202,7 +25202,7 @@ lean_dec(x_11);
|
|||
x_14 = l___private_Init_Lean_Elab_Quotation_14__exprPlaceholder;
|
||||
lean_inc_n(x_6, 2);
|
||||
x_15 = lean_local_ctx_mk_let_decl(x_12, x_6, x_6, x_14, x_9);
|
||||
x_16 = l_Lean_stxInh;
|
||||
x_16 = l_Lean_Syntax_inhabited;
|
||||
x_17 = lean_unsigned_to_nat(3u);
|
||||
x_18 = lean_array_get(x_16, x_4, x_17);
|
||||
lean_dec(x_4);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -36,7 +36,6 @@ lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_
|
|||
lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_TermApp_14__elabAppFn___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unreachable_x21___rarg(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Util_7__regTraceClasses___closed__2;
|
||||
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Term_elabExplicitUniv___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_fieldIdxKind___closed__2;
|
||||
extern lean_object* l_Lean_MessageData_ofList___closed__3;
|
||||
|
|
@ -53,7 +52,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__2;
|
|||
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__7;
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProj___closed__3;
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
lean_object* lean_environment_find(lean_object*, lean_object*);
|
||||
|
|
@ -95,6 +93,7 @@ lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__14;
|
|||
extern lean_object* l_Array_iterateMAux___main___at_Lean_mkAppStx___spec__1___closed__1;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_16__toMessageData___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_NamedArg_inhabited;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__3;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_17__mergeFailures(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_8__resolveLValLoop___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -143,7 +142,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main___closed__
|
|||
extern lean_object* l___private_Init_Lean_Elab_Term_14__resumePostponed___lambda__1___closed__1;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__26;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_17__mergeFailures___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabChoice___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_addNamedArg___closed__3;
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -162,6 +160,7 @@ lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main___closed__
|
|||
lean_object* l_Lean_Elab_Term_Arg_hasToString(lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at___private_Init_Lean_Elab_TermApp_8__resolveLValLoop___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_14__elabAppFn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getId(lean_object*);
|
||||
|
|
@ -222,6 +221,7 @@ extern lean_object* l_Lean_Meta_Exception_mkAppTypeMismatchMessage___closed__8;
|
|||
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__8;
|
||||
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_addNamedArg___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabId(lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_4__elabAppArgsAux___main___closed__5;
|
||||
lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main___closed__5;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp___closed__2;
|
||||
|
|
@ -911,7 +911,7 @@ x_8 = lean_alloc_ctor(1, 1, 0);
|
|||
lean_ctor_set(x_8, 0, x_4);
|
||||
x_9 = 1;
|
||||
lean_inc(x_5);
|
||||
x_10 = l_Lean_Elab_Term_elabTerm(x_7, x_8, x_9, x_9, x_5, x_6);
|
||||
x_10 = l_Lean_Elab_Term_elabTermAux___main(x_8, x_9, x_9, x_7, x_5, x_6);
|
||||
if (lean_obj_tag(x_10) == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
|
|
@ -6430,7 +6430,7 @@ lean_dec(x_206);
|
|||
x_213 = lean_box(0);
|
||||
x_214 = 1;
|
||||
lean_inc(x_9);
|
||||
x_215 = l_Lean_Elab_Term_elabTerm(x_2, x_213, x_214, x_214, x_9, x_10);
|
||||
x_215 = l_Lean_Elab_Term_elabTermAux___main(x_213, x_214, x_214, x_2, x_9, x_10);
|
||||
if (lean_obj_tag(x_215) == 0)
|
||||
{
|
||||
uint8_t x_216;
|
||||
|
|
@ -6830,7 +6830,7 @@ lean_dec(x_302);
|
|||
x_306 = lean_box(0);
|
||||
x_307 = 1;
|
||||
lean_inc(x_9);
|
||||
x_308 = l_Lean_Elab_Term_elabTerm(x_2, x_306, x_307, x_307, x_9, x_10);
|
||||
x_308 = l_Lean_Elab_Term_elabTermAux___main(x_306, x_307, x_307, x_2, x_9, x_10);
|
||||
if (lean_obj_tag(x_308) == 0)
|
||||
{
|
||||
uint8_t x_309;
|
||||
|
|
@ -7158,7 +7158,7 @@ lean_object* x_13; uint8_t x_14; lean_object* x_15;
|
|||
x_13 = lean_box(0);
|
||||
x_14 = 1;
|
||||
lean_inc(x_9);
|
||||
x_15 = l_Lean_Elab_Term_elabTerm(x_2, x_13, x_14, x_14, x_9, x_10);
|
||||
x_15 = l_Lean_Elab_Term_elabTermAux___main(x_13, x_14, x_14, x_2, x_9, x_10);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
uint8_t x_16;
|
||||
|
|
@ -7470,7 +7470,7 @@ lean_dec(x_71);
|
|||
x_75 = lean_box(0);
|
||||
x_76 = 1;
|
||||
lean_inc(x_9);
|
||||
x_77 = l_Lean_Elab_Term_elabTerm(x_2, x_75, x_76, x_76, x_9, x_10);
|
||||
x_77 = l_Lean_Elab_Term_elabTermAux___main(x_75, x_76, x_76, x_2, x_9, x_10);
|
||||
if (lean_obj_tag(x_77) == 0)
|
||||
{
|
||||
uint8_t x_78;
|
||||
|
|
@ -7784,7 +7784,7 @@ x_137 = l_Array_isEmpty___rarg(x_136);
|
|||
if (x_137 == 0)
|
||||
{
|
||||
lean_object* x_138; lean_object* x_139; lean_object* x_140;
|
||||
x_138 = l_Lean_stxInh;
|
||||
x_138 = l_Lean_Syntax_inhabited;
|
||||
x_139 = lean_array_get(x_138, x_136, x_70);
|
||||
lean_dec(x_136);
|
||||
x_140 = l_Lean_Elab_Term_elabExplicitUniv(x_139, x_9, x_10);
|
||||
|
|
@ -9716,7 +9716,7 @@ lean_object* _init_l___private_Init_Lean_Elab_TermApp_20__regTraceClasses___clos
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Elab_Util_7__regTraceClasses___closed__2;
|
||||
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
x_2 = l_Lean_Parser_Term_app___elambda__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@ lean_object* l___private_Init_Lean_Elab_TermBinders_10__expandFunBindersAux___bo
|
|||
lean_object* l_Lean_Elab_Term_elabDepArrow___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_nameToExprAux___main___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Util_7__regTraceClasses___closed__2;
|
||||
lean_object* l___private_Init_Lean_Elab_TermBinders_5__matchBinder___closed__2;
|
||||
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermBinders_5__matchBinder___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabDepArrow(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -81,6 +80,7 @@ lean_object* l___private_Init_Lean_Elab_TermBinders_11__expandFunBinders___boxed
|
|||
lean_object* l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_TermBinders_4__expandBinderModifier___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_withLetDecl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Term_8__expandCDot___closed__4;
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_TermBinders_11__expandFunBinders(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -109,7 +109,6 @@ lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
|
|||
lean_object* l___private_Init_Lean_Elab_TermBinders_8__getFunBinderIdsAux_x3f___main(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
|
||||
lean_object* l___private_Init_Lean_Elab_TermBinders_6__elabBinderViews(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermBinders_5__matchBinder___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -118,6 +117,7 @@ lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDepArrow___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabFun___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabFun___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Elab_TermBinders_6__elabBinderViews___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -15998,7 +15998,7 @@ lean_object* x_6; uint8_t x_7; lean_object* x_8;
|
|||
x_6 = lean_box(0);
|
||||
x_7 = 1;
|
||||
lean_inc(x_4);
|
||||
x_8 = l_Lean_Elab_Term_elabTerm(x_1, x_6, x_7, x_7, x_4, x_5);
|
||||
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_6, x_7, x_7, x_1, x_4, x_5);
|
||||
if (lean_obj_tag(x_8) == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
|
|
@ -16627,7 +16627,7 @@ x_10 = lean_alloc_ctor(1, 1, 0);
|
|||
lean_ctor_set(x_10, 0, x_8);
|
||||
x_11 = 1;
|
||||
lean_inc(x_5);
|
||||
x_12 = l_Lean_Elab_Term_elabTerm(x_2, x_10, x_11, x_11, x_5, x_9);
|
||||
x_12 = l_Lean_Elab_Term_elabTermAux___main(x_10, x_11, x_11, x_2, x_5, x_9);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
|
|
@ -16788,7 +16788,7 @@ _start:
|
|||
uint8_t x_7; lean_object* x_8;
|
||||
x_7 = 1;
|
||||
lean_inc(x_5);
|
||||
x_8 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_7, x_7, x_5, x_6);
|
||||
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_7, x_7, x_2, x_5, x_6);
|
||||
if (lean_obj_tag(x_8) == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
|
|
@ -16837,7 +16837,7 @@ lean_object* _init_l_Lean_Elab_Term_elabLetIdDecl___closed__1() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Elab_Util_7__regTraceClasses___closed__2;
|
||||
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
|
||||
x_2 = l_Lean_Parser_Term_let___elambda__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -16912,8 +16912,8 @@ if (x_27 == 0)
|
|||
lean_object* x_28; lean_object* x_29;
|
||||
lean_inc(x_1);
|
||||
x_28 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabLetIdDecl___lambda__2___boxed), 6, 3);
|
||||
lean_closure_set(x_28, 0, x_3);
|
||||
lean_closure_set(x_28, 1, x_4);
|
||||
lean_closure_set(x_28, 0, x_4);
|
||||
lean_closure_set(x_28, 1, x_3);
|
||||
lean_closure_set(x_28, 2, x_1);
|
||||
x_29 = l_Lean_Elab_Term_withLetDecl___rarg(x_1, x_8, x_21, x_22, x_28, x_5, x_25);
|
||||
lean_dec(x_1);
|
||||
|
|
@ -16951,8 +16951,8 @@ lean_inc(x_40);
|
|||
lean_dec(x_39);
|
||||
lean_inc(x_1);
|
||||
x_41 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabLetIdDecl___lambda__2___boxed), 6, 3);
|
||||
lean_closure_set(x_41, 0, x_3);
|
||||
lean_closure_set(x_41, 1, x_4);
|
||||
lean_closure_set(x_41, 0, x_4);
|
||||
lean_closure_set(x_41, 1, x_3);
|
||||
lean_closure_set(x_41, 2, x_1);
|
||||
x_42 = l_Lean_Elab_Term_withLetDecl___rarg(x_1, x_8, x_21, x_22, x_41, x_5, x_40);
|
||||
lean_dec(x_1);
|
||||
|
|
@ -17570,7 +17570,7 @@ x_99 = lean_alloc_ctor(1, 2, 0);
|
|||
lean_ctor_set(x_99, 0, x_98);
|
||||
lean_ctor_set(x_99, 1, x_97);
|
||||
x_100 = 1;
|
||||
x_101 = l_Lean_Elab_Term_elabTerm(x_99, x_2, x_100, x_100, x_3, x_82);
|
||||
x_101 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_100, x_100, x_99, x_3, x_82);
|
||||
return x_101;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Lean.Hygiene
|
||||
// Imports: Init.Control Init.Lean.Syntax
|
||||
// Imports: Init.Control Init.LeanInit Init.Lean.Syntax
|
||||
#include "runtime/lean.h"
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -27,99 +27,11 @@ lean_object* l_Lean_monadQuotationTrans(lean_object*, lean_object*);
|
|||
lean_object* l_ReaderT_read___at_Lean_Unhygienic_MonadQuotation___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Unhygienic_MonadQuotation___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_monadQuotationTrans___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Unhygienic_MonadQuotation;
|
||||
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__1;
|
||||
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addMacroScopes(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__2;
|
||||
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_List_foldl___main___at_Lean_addMacroScopes___spec__1(lean_object*, lean_object*);
|
||||
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addMacroScope(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_name_mk_numeral(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_List_foldl___main___at_Lean_addMacroScopes___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
{
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_2);
|
||||
x_5 = lean_name_mk_numeral(x_1, x_3);
|
||||
x_1 = x_5;
|
||||
x_2 = x_4;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_addMacroScopes(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_List_foldl___main___at_Lean_addMacroScopes___spec__1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 2)
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
lean_ctor_set(x_5, 1, x_2);
|
||||
x_1 = x_3;
|
||||
x_2 = x_5;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = l_List_reverse___rarg(x_2);
|
||||
x_8 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_8, 0, x_1);
|
||||
lean_ctor_set(x_8, 1, x_7);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_extractMacroScopes(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = lean_box(0);
|
||||
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_ReaderT_read___at_Lean_Unhygienic_MonadQuotation___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -206,6 +118,52 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Unhygienic_run___rarg), 1, 0);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 2)
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
lean_ctor_set(x_5, 1, x_2);
|
||||
x_1 = x_3;
|
||||
x_2 = x_5;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = l_List_reverse___rarg(x_2);
|
||||
x_8 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_8, 0, x_1);
|
||||
lean_ctor_set(x_8, 1, x_7);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_extractMacroScopes(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = lean_box(0);
|
||||
x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -262,6 +220,7 @@ return x_3;
|
|||
}
|
||||
}
|
||||
lean_object* initialize_Init_Control(lean_object*);
|
||||
lean_object* initialize_Init_LeanInit(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Syntax(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
lean_object* initialize_Init_Lean_Hygiene(lean_object* w) {
|
||||
|
|
@ -271,6 +230,9 @@ _G_initialized = true;
|
|||
res = initialize_Init_Control(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_LeanInit(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Lean_Syntax(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
|
|
|
|||
|
|
@ -142,7 +142,6 @@ lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_addParser(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_categoryParserFnRef;
|
||||
lean_object* l_Lean_Parser_optionalFn___boxed(lean_object*);
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Lean_Parser_InputContext_inhabited;
|
||||
lean_object* l_Lean_Parser_parserExtension___elambda__3___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Error_HasToString___closed__1;
|
||||
|
|
@ -752,6 +751,7 @@ lean_object* l_Lean_Parser_checkNoWsBefore___boxed(lean_object*, lean_object*);
|
|||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
lean_object* l_PersistentHashMap_containsAux___main___at___private_Init_Lean_Parser_Parser_9__addParserCategoryCore___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Parser_Parser_17__ParserExtension_addImported___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_Parser_unquotedSymbolFn(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Syntax_foldSepRevArgsM___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_String_intercalate(lean_object*, lean_object*);
|
||||
|
|
@ -8966,7 +8966,7 @@ x_2 = lean_array_get_size(x_1);
|
|||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_sub(x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_Lean_stxInh;
|
||||
x_5 = l_Lean_Syntax_inhabited;
|
||||
x_6 = lean_array_get(x_5, x_1, x_4);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
|
|
@ -36255,7 +36255,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
x_14 = lean_alloc_ctor(1, 1, 0);
|
||||
|
|
|
|||
|
|
@ -238,7 +238,6 @@ lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda
|
|||
lean_object* l_Lean_Parser_Term_match___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Term_show___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Lean_Parser_Term_cdot___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_andM___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__3;
|
||||
|
|
@ -1291,6 +1290,7 @@ lean_object* l_Lean_Parser_Term_uminus___closed__2;
|
|||
lean_object* l_Lean_Parser_Term_str___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_fromTerm___closed__4;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_Parser_Term_matchAlt___closed__9;
|
||||
lean_object* l_Lean_Parser_Term_arrayLit;
|
||||
lean_object* l_Lean_Parser_Term_mul___closed__2;
|
||||
|
|
@ -36477,7 +36477,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
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;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
x_14 = lean_unsigned_to_nat(1u);
|
||||
|
|
@ -36540,7 +36540,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(1u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
x_14 = l_Lean_Syntax_isNone(x_13);
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ extern "C" {
|
|||
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_stxInh;
|
||||
lean_object* l_Lean_Syntax_removeParen___closed__4;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
|
|
@ -39,6 +38,7 @@ lean_object* l_Lean_Syntax_manyToSepBy(lean_object*, lean_object*);
|
|||
lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*);
|
||||
extern lean_object* l_Array_forMAux___main___at_Lean_Environment_displayStats___spec__9___closed__2;
|
||||
extern lean_object* l_Option_HasRepr___rarg___closed__3;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_removeParen(lean_object*);
|
||||
uint8_t l_Lean_Syntax_isNone(lean_object*);
|
||||
|
|
@ -157,7 +157,7 @@ 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; lean_object* x_10; lean_object* x_11;
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
x_5 = l_Lean_stxInh;
|
||||
x_5 = l_Lean_Syntax_inhabited;
|
||||
x_6 = lean_unsigned_to_nat(0u);
|
||||
x_7 = lean_array_get(x_5, x_4, x_6);
|
||||
x_8 = l_Lean_mkOptionalNode___closed__1;
|
||||
|
|
@ -176,7 +176,7 @@ x_13 = lean_ctor_get(x_1, 1);
|
|||
lean_inc(x_13);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_1);
|
||||
x_14 = l_Lean_stxInh;
|
||||
x_14 = l_Lean_Syntax_inhabited;
|
||||
x_15 = lean_unsigned_to_nat(0u);
|
||||
x_16 = lean_array_get(x_14, x_13, x_15);
|
||||
x_17 = l_Lean_mkOptionalNode___closed__1;
|
||||
|
|
@ -261,7 +261,7 @@ return x_1;
|
|||
else
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
|
||||
x_6 = l_Lean_stxInh;
|
||||
x_6 = l_Lean_Syntax_inhabited;
|
||||
x_7 = lean_unsigned_to_nat(1u);
|
||||
x_8 = lean_array_get(x_6, x_3, x_7);
|
||||
x_9 = l_Lean_Syntax_getNumArgs(x_8);
|
||||
|
|
|
|||
|
|
@ -47,9 +47,7 @@ lean_object* l_Lean_Syntax_toNat___boxed(lean_object*);
|
|||
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_HasToString;
|
||||
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_stxInh;
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_fieldIdxKind___closed__1;
|
||||
|
|
@ -97,9 +95,7 @@ extern lean_object* l_Lean_Format_sbracket___closed__2;
|
|||
lean_object* l_Lean_SyntaxNode_getKind(lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_rewriteBottomUp(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__2;
|
||||
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__1;
|
||||
lean_object* l___private_Init_Lean_Syntax_11__decodeQuotedChar___boxed__const__3;
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main___closed__8;
|
||||
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
|
||||
|
|
@ -113,7 +109,6 @@ lean_object* l_Lean_Syntax_formatStxAux___main___closed__4;
|
|||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getIdAt(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__4;
|
||||
lean_object* l___private_Init_Lean_Syntax_7__decodeHexDigit___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
|
|
@ -145,7 +140,6 @@ lean_object* l_Lean_strLitKind___closed__1;
|
|||
lean_object* l_Lean_Syntax_isNatLitAux___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_3__updateLast(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArgs___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_updateLeading(lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main___closed__3;
|
||||
lean_object* l_Lean_mkNullNode(lean_object*);
|
||||
|
|
@ -217,6 +211,7 @@ lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__3___
|
|||
lean_object* l_Lean_SyntaxNode_getNumArgs(lean_object*);
|
||||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
extern lean_object* l_Lean_Format_paren___closed__1;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___boxed(lean_object*);
|
||||
|
|
@ -229,10 +224,7 @@ uint8_t l_Lean_Syntax_hasArgs(lean_object*);
|
|||
lean_object* l_String_quote(lean_object*);
|
||||
lean_object* l_Lean_Syntax_asNode___closed__1;
|
||||
lean_object* l_Lean_Syntax_HasToString___closed__2;
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_withArgs___rarg(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Format_sbracket___closed__1;
|
||||
lean_object* l_Lean_Syntax_getHeadInfo___boxed(lean_object*);
|
||||
|
|
@ -261,7 +253,6 @@ lean_object* l_Array_toList___rarg(lean_object*);
|
|||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__5(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_decodeStrLit(lean_object*);
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
lean_object* lean_mk_syntax_list(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getTailInfo___boxed(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_10__decodeNatLitVal(lean_object*);
|
||||
|
|
@ -269,7 +260,6 @@ lean_object* l___private_Init_Lean_Syntax_11__decodeQuotedChar___boxed__const__5
|
|||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_string_length(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__3;
|
||||
lean_object* lean_mk_syntax_str_lit(lean_object*);
|
||||
lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_9__decodeDecimalLitAux(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -745,14 +735,6 @@ x_1 = l_Lean_fieldIdxKind___closed__2;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_stxInh() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_box(0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
uint8_t l_Lean_Syntax_isMissing(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -880,7 +862,7 @@ _start:
|
|||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = l_Lean_stxInh;
|
||||
x_4 = l_Lean_Syntax_inhabited;
|
||||
x_5 = lean_array_get(x_4, x_3, x_2);
|
||||
return x_5;
|
||||
}
|
||||
|
|
@ -1200,50 +1182,6 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_Syntax_asNode(x_1);
|
||||
x_3 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_3);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArgs___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Syntax_getArgs(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_3 = l_Lean_Syntax_asNode(x_1);
|
||||
x_4 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_3);
|
||||
x_5 = l_Lean_stxInh;
|
||||
x_6 = lean_array_get(x_5, x_4, x_2);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_setArgs(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -1463,80 +1401,6 @@ lean_dec(x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("missing");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Syntax_getKind___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("ident");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Syntax_getKind___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
switch (lean_obj_tag(x_1)) {
|
||||
case 0:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Syntax_getKind___closed__2;
|
||||
return x_2;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_3);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_box(0);
|
||||
x_6 = lean_name_mk_string(x_5, x_4);
|
||||
return x_6;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_7;
|
||||
lean_dec(x_1);
|
||||
x_7 = l_Lean_Syntax_getKind___closed__4;
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -1734,26 +1598,6 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = l_Lean_Syntax_getKind(x_1);
|
||||
x_4 = lean_name_eq(x_3, x_2);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = l_Lean_Syntax_isOfKind(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
x_4 = lean_box(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -2645,7 +2489,7 @@ lean_dec(x_10);
|
|||
x_11 = lean_unsigned_to_nat(1u);
|
||||
x_12 = lean_nat_sub(x_5, x_11);
|
||||
lean_dec(x_5);
|
||||
x_13 = l_Lean_stxInh;
|
||||
x_13 = l_Lean_Syntax_inhabited;
|
||||
x_14 = lean_array_get(x_13, x_4, x_12);
|
||||
x_15 = l_Lean_Syntax_updateTrailing___main(x_1, x_14);
|
||||
x_16 = lean_array_set(x_4, x_12, x_15);
|
||||
|
|
@ -2660,7 +2504,7 @@ lean_dec(x_2);
|
|||
x_17 = lean_unsigned_to_nat(1u);
|
||||
x_18 = lean_nat_sub(x_5, x_17);
|
||||
lean_dec(x_5);
|
||||
x_19 = l_Lean_stxInh;
|
||||
x_19 = l_Lean_Syntax_inhabited;
|
||||
x_20 = lean_array_get(x_19, x_4, x_18);
|
||||
x_21 = l_Lean_Syntax_updateTrailing___main(x_1, x_20);
|
||||
x_22 = lean_array_set(x_4, x_18, x_21);
|
||||
|
|
@ -3184,7 +3028,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_obj
|
|||
x_6 = lean_unsigned_to_nat(1u);
|
||||
x_7 = lean_nat_sub(x_3, x_6);
|
||||
lean_dec(x_3);
|
||||
x_8 = l_Lean_stxInh;
|
||||
x_8 = l_Lean_Syntax_inhabited;
|
||||
x_9 = lean_array_get(x_8, x_2, x_7);
|
||||
lean_inc(x_1);
|
||||
x_10 = l_Lean_Syntax_setTailInfoAux___main(x_1, x_9);
|
||||
|
|
@ -3615,7 +3459,7 @@ lean_dec(x_10);
|
|||
if (x_12 == 0)
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = l_Lean_stxInh;
|
||||
x_13 = l_Lean_Syntax_inhabited;
|
||||
x_14 = lean_array_get(x_13, x_4, x_11);
|
||||
x_15 = l_Lean_Syntax_reprint___main(x_14);
|
||||
lean_dec(x_14);
|
||||
|
|
@ -4534,7 +4378,7 @@ _start:
|
|||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = l_Lean_stxInh;
|
||||
x_4 = l_Lean_Syntax_inhabited;
|
||||
x_5 = lean_array_get(x_4, x_3, x_2);
|
||||
x_6 = l_Lean_Syntax_getId(x_5);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -5445,7 +5289,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_4, x_12);
|
||||
if (lean_obj_tag(x_13) == 2)
|
||||
|
|
@ -6217,7 +6061,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
if (lean_obj_tag(x_13) == 2)
|
||||
|
|
@ -6357,7 +6201,7 @@ return x_10;
|
|||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = l_Lean_stxInh;
|
||||
x_11 = l_Lean_Syntax_inhabited;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get(x_11, x_3, x_12);
|
||||
if (lean_obj_tag(x_13) == 2)
|
||||
|
|
@ -6533,18 +6377,8 @@ l_Lean_fieldIdxKind___closed__2 = _init_l_Lean_fieldIdxKind___closed__2();
|
|||
lean_mark_persistent(l_Lean_fieldIdxKind___closed__2);
|
||||
l_Lean_fieldIdxKind = _init_l_Lean_fieldIdxKind();
|
||||
lean_mark_persistent(l_Lean_fieldIdxKind);
|
||||
l_Lean_stxInh = _init_l_Lean_stxInh();
|
||||
lean_mark_persistent(l_Lean_stxInh);
|
||||
l_Lean_Syntax_asNode___closed__1 = _init_l_Lean_Syntax_asNode___closed__1();
|
||||
lean_mark_persistent(l_Lean_Syntax_asNode___closed__1);
|
||||
l_Lean_Syntax_getKind___closed__1 = _init_l_Lean_Syntax_getKind___closed__1();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__1);
|
||||
l_Lean_Syntax_getKind___closed__2 = _init_l_Lean_Syntax_getKind___closed__2();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__2);
|
||||
l_Lean_Syntax_getKind___closed__3 = _init_l_Lean_Syntax_getKind___closed__3();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__3);
|
||||
l_Lean_Syntax_getKind___closed__4 = _init_l_Lean_Syntax_getKind___closed__4();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__4);
|
||||
l_Lean_Syntax_reprint___main___closed__1 = _init_l_Lean_Syntax_reprint___main___closed__1();
|
||||
lean_mark_persistent(l_Lean_Syntax_reprint___main___closed__1);
|
||||
l_Lean_Syntax_formatStxAux___main___closed__1 = _init_l_Lean_Syntax_formatStxAux___main___closed__1();
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.LeanInit
|
||||
// Imports: Init.Data.String.Basic Init.Data.UInt Init.Data.Hashable
|
||||
// Imports: Init.Data.String.Basic Init.Data.Array.Basic Init.Data.UInt Init.Data.Hashable Init.Control.Reader Init.Control.Option
|
||||
#include "runtime/lean.h"
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -14,10 +14,15 @@
|
|||
extern "C" {
|
||||
#endif
|
||||
lean_object* l_Lean_ParserDescr_pushLeading;
|
||||
lean_object* l_Lean_MacroM_monadQuotation;
|
||||
lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_optional(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_lookahead(uint8_t, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_many(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_HasBeq___closed__1;
|
||||
lean_object* l_Lean_ParserDescr_ident(uint8_t);
|
||||
lean_object* l_Lean_mkNameSimple(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_andthen___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -26,15 +31,21 @@ lean_object* l_Lean_Name_inhabited;
|
|||
extern lean_object* l_String_splitAux___main___closed__1;
|
||||
lean_object* l_Lean_Name_hashable___closed__1;
|
||||
lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__2;
|
||||
lean_object* l_Lean_Syntax_getKind___closed__1;
|
||||
lean_object* l_Lean_Name_hashable;
|
||||
lean_object* l_Lean_ParserDescr_str(uint8_t);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
|
||||
lean_object* l_Lean_Syntax_getKind___closed__4;
|
||||
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
|
||||
extern lean_object* l_optional___rarg___closed__1;
|
||||
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_num___boxed(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_hashEx___boxed(lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
size_t lean_name_hash(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArgs___boxed(lean_object*);
|
||||
size_t l_Lean_Name_hash(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_parser(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -48,18 +59,33 @@ lean_object* l_Lean_ParserDescr_ident___boxed(lean_object*);
|
|||
lean_object* l_Lean_ParserDescr_str___boxed(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_node___boxed(lean_object*, lean_object*, lean_object*);
|
||||
size_t lean_usize_of_nat(lean_object*);
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_ParserDescr_char___boxed(lean_object*);
|
||||
lean_object* l_Lean_HasBeq;
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object*);
|
||||
lean_object* l_Lean_Name_beq___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addMacroScopes(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
size_t lean_usize_mix_hash(size_t, size_t);
|
||||
lean_object* l_Lean_MacroM_monadQuotation___closed__1;
|
||||
lean_object* l_Lean_Syntax_getKind___closed__3;
|
||||
lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_foldl___main___at_Lean_addMacroScopes___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_num(uint8_t);
|
||||
lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object*, uint8_t);
|
||||
lean_object* l_Lean_Name_hash___boxed(lean_object*);
|
||||
lean_object* l_Lean_MacroM_monadQuotation___closed__2;
|
||||
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
|
||||
size_t lean_string_hash(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_sepBy1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -169,6 +195,33 @@ x_3 = lean_name_mk_string(x_2, x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = lean_name_eq(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_4 = lean_box(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_HasBeq___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Name_beq___boxed), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_HasBeq() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_HasBeq___closed__1;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -532,9 +585,244 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_inhabited() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_box(0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("missing");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Syntax_getKind___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("ident");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Syntax_getKind___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Syntax_getKind___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
switch (lean_obj_tag(x_1)) {
|
||||
case 0:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Syntax_getKind___closed__2;
|
||||
return x_2;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_3);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_box(0);
|
||||
x_6 = lean_name_mk_string(x_5, x_4);
|
||||
return x_6;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_7;
|
||||
lean_dec(x_1);
|
||||
x_7 = l_Lean_Syntax_getKind___closed__4;
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = l_Lean_Syntax_getKind(x_1);
|
||||
x_4 = lean_name_eq(x_3, x_2);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = l_Lean_Syntax_isOfKind(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
x_4 = lean_box(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 1)
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = l_Lean_Syntax_inhabited;
|
||||
x_5 = lean_array_get(x_4, x_3, x_2);
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_box(0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArg___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 1)
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_2);
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_empty___closed__1;
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_getArgs___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Syntax_getArgs(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_addMacroScope(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_name_mk_numeral(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_List_foldl___main___at_Lean_addMacroScopes___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
{
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_2);
|
||||
x_5 = lean_name_mk_numeral(x_1, x_3);
|
||||
x_1 = x_5;
|
||||
x_2 = x_4;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_addMacroScopes(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_List_foldl___main___at_Lean_addMacroScopes___spec__1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_apply_1(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_MacroM_monadQuotation___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__1), 3, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_MacroM_monadQuotation___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_optional___rarg___closed__1;
|
||||
x_2 = l_Lean_MacroM_monadQuotation___closed__1;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_MacroM_monadQuotation() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_MacroM_monadQuotation___closed__2;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init_Data_String_Basic(lean_object*);
|
||||
lean_object* initialize_Init_Data_Array_Basic(lean_object*);
|
||||
lean_object* initialize_Init_Data_UInt(lean_object*);
|
||||
lean_object* initialize_Init_Data_Hashable(lean_object*);
|
||||
lean_object* initialize_Init_Control_Reader(lean_object*);
|
||||
lean_object* initialize_Init_Control_Option(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
lean_object* initialize_Init_LeanInit(lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -543,20 +831,49 @@ _G_initialized = true;
|
|||
res = initialize_Init_Data_String_Basic(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Data_Array_Basic(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Data_UInt(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Data_Hashable(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Control_Reader(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Control_Option(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Name_inhabited = _init_l_Lean_Name_inhabited();
|
||||
lean_mark_persistent(l_Lean_Name_inhabited);
|
||||
l_Lean_Name_hashable___closed__1 = _init_l_Lean_Name_hashable___closed__1();
|
||||
lean_mark_persistent(l_Lean_Name_hashable___closed__1);
|
||||
l_Lean_Name_hashable = _init_l_Lean_Name_hashable();
|
||||
lean_mark_persistent(l_Lean_Name_hashable);
|
||||
l_Lean_HasBeq___closed__1 = _init_l_Lean_HasBeq___closed__1();
|
||||
lean_mark_persistent(l_Lean_HasBeq___closed__1);
|
||||
l_Lean_HasBeq = _init_l_Lean_HasBeq();
|
||||
lean_mark_persistent(l_Lean_HasBeq);
|
||||
l_Lean_ParserDescr_pushLeading = _init_l_Lean_ParserDescr_pushLeading();
|
||||
lean_mark_persistent(l_Lean_ParserDescr_pushLeading);
|
||||
l_Lean_Syntax_inhabited = _init_l_Lean_Syntax_inhabited();
|
||||
lean_mark_persistent(l_Lean_Syntax_inhabited);
|
||||
l_Lean_Syntax_getKind___closed__1 = _init_l_Lean_Syntax_getKind___closed__1();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__1);
|
||||
l_Lean_Syntax_getKind___closed__2 = _init_l_Lean_Syntax_getKind___closed__2();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__2);
|
||||
l_Lean_Syntax_getKind___closed__3 = _init_l_Lean_Syntax_getKind___closed__3();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__3);
|
||||
l_Lean_Syntax_getKind___closed__4 = _init_l_Lean_Syntax_getKind___closed__4();
|
||||
lean_mark_persistent(l_Lean_Syntax_getKind___closed__4);
|
||||
l_Lean_MacroM_monadQuotation___closed__1 = _init_l_Lean_MacroM_monadQuotation___closed__1();
|
||||
lean_mark_persistent(l_Lean_MacroM_monadQuotation___closed__1);
|
||||
l_Lean_MacroM_monadQuotation___closed__2 = _init_l_Lean_MacroM_monadQuotation___closed__2();
|
||||
lean_mark_persistent(l_Lean_MacroM_monadQuotation___closed__2);
|
||||
l_Lean_MacroM_monadQuotation = _init_l_Lean_MacroM_monadQuotation();
|
||||
lean_mark_persistent(l_Lean_MacroM_monadQuotation);
|
||||
return lean_mk_io_result(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue