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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 19:20:50 -08:00
parent ac2fb7e149
commit 781956e455
25 changed files with 23408 additions and 23122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -62,7 +62,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
else if kind == `Lean.Parser.Syntax.paren then
toParserDescrAux (stx.getArg 1)
else if kind == `Lean.Parser.Syntax.cat then do
let cat : Name := stx.getIdAt 0;
let cat := (stx.getIdAt 0).eraseMacroScopes;
let rbp? : Option Nat := expandOptPrecedence (stx.getArg 1);
env ← liftM getEnv;
unless (Parser.isParserCategory env cat) $ liftM $ throwError (stx.getArg 3) ("unknown category '" ++ cat ++ "'");
@ -161,7 +161,7 @@ else do
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab :=
fun stx => do
env ← getEnv;
let cat := stx.getIdAt 4;
let cat := (stx.getIdAt 4).eraseMacroScopes;
unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 4) ("unknown category '" ++ cat ++ "'");
kind ← elabKind (stx.getArg 1) cat;
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
@ -187,10 +187,14 @@ adaptExpander $ fun stx => match_syntax stx with
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
-- wrap all occurrences of the given `ident` nodes in antiquotations
/- Wrap all occurrences of the given `ident` nodes in antiquotations -/
private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
| stx => match_syntax stx with
| `($id:ident) => if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then Syntax.node `antiquot #[mkAtom "$", Unhygienic.run `($id:ident), mkNullNode, mkNullNode] else stx
| `($id:ident) =>
if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
Syntax.node `antiquot #[mkAtom "$", Unhygienic.run `($id:ident), mkNullNode, mkNullNode]
else
stx
| _ => match stx with
| Syntax.node k args => Syntax.node k (args.map antiquote)
| stx => stx
@ -293,7 +297,7 @@ adaptExpander $ fun stx => do
let args := (stx.getArg 2).getArgs;
let cat := stx.getArg 4;
let rhsBody := stx.getArg 7;
kind ← mkFreshKind cat.getId;
kind ← mkFreshKind (cat.getId).eraseMacroScopes;
-- build parser
stxPart ← expandMacroHeadIntoSyntaxItem head;
stxParts ← args.mapM expandMacroArgIntoSyntaxItem;

25
stage0/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
View file

@ -5,15 +5,36 @@ Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.Tactic
import Init.Lean.Elab.Tactic.Basic
namespace Lean
namespace Elab
namespace Term
open Tactic (TacticM evalTactic getUnsolvedGoals)
def liftTacticElabM {α} (ref : Syntax) (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
withMVarContext mvarId $ fun ctx s =>
match x { ref := ref, main := mvarId, .. ctx } { goals := [mvarId], .. s } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) newS.toTermState
| EStateM.Result.ok a newS => EStateM.Result.ok a newS.toTermState
def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
val ← instantiateMVars ref (mkMVar mvarId);
when val.hasMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val)
def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };
remainingGoals ← liftTacticElabM ref mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
let tailRef := ref.getTailWithInfo.getD ref;
unless remainingGoals.isEmpty (reportUnsolvedGoals tailRef remainingGoals);
ensureAssignmentHasNoMVars tailRef mvarId
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
elabTerm stx expectedType? false errToSorry
-- Remark: if `ctx.errToSorry` is already false, then we don't enable it. Recall tactics disable `errToSorry`
adaptReader (fun (ctx : Context) => { errToSorry := ctx.errToSorry && errToSorry, .. ctx }) $
elabTerm stx expectedType? false
/--
Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.

42
stage0/src/Init/Lean/Elab/Tactic.lean
View file

@ -6,44 +6,4 @@ Authors: Leonardo de Moura, Sebastian Ullrich
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.Tactic.Basic
namespace Lean
namespace Elab
namespace Term
def mkTacticMVar (ref : Syntax) (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
mvar ← mkFreshExprMVar ref type MetavarKind.syntheticOpaque `main;
let mvarId := mvar.mvarId!;
registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode;
pure mvar
@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
fun stx expectedType? =>
match expectedType? with
| some expectedType => mkTacticMVar stx expectedType (stx.getArg 1)
| none => throwError stx ("invalid tactic block, expected type has not been provided")
open Tactic (TacticM evalTactic getUnsolvedGoals)
def liftTacticElabM {α} (ref : Syntax) (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
withMVarContext mvarId $ fun ctx s =>
match x { ref := ref, main := mvarId, .. ctx } { goals := [mvarId], .. s } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) newS.toTermState
| EStateM.Result.ok a newS => EStateM.Result.ok a newS.toTermState
def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
val ← instantiateMVars ref (mkMVar mvarId);
when val.hasMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val)
def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };
remainingGoals ← liftTacticElabM ref mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
let tailRef := ref.getTailWithInfo.getD ref;
unless remainingGoals.isEmpty (reportUnsolvedGoals tailRef remainingGoals);
ensureAssignmentHasNoMVars tailRef mvarId
end Term
end Elab
end Lean
import Init.Lean.Elab.Tactic.ElabTerm

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

@ -5,10 +5,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Util.CollectMVars
import Init.Lean.Elab.Util
import Init.Lean.Elab.Term
import Init.Lean.Meta.Tactic.Assumption
import Init.Lean.Meta.Tactic.Intro
import Init.Lean.Elab.Util
import Init.Lean.Elab.Term
namespace Lean
namespace Elab
@ -68,7 +68,6 @@ def addContext (msg : MessageData) : TacticM MessageData := liftTermElabM $ Term
def isExprMVarAssigned (mvarId : MVarId) : TacticM Bool := liftTermElabM $ Term.isExprMVarAssigned mvarId
def assignExprMVar (mvarId : MVarId) (val : Expr) : TacticM Unit := liftTermElabM $ Term.assignExprMVar mvarId val
def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType ref expectedType? e
def elabTerm (stx : Syntax) (expectedType? : Option Expr) : TacticM Expr := liftTermElabM $ Term.elabTerm stx expectedType?
def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals ref goals
/-- Collect unassigned metavariables -/
@ -250,35 +249,8 @@ fun stx => match_syntax stx with
| `(tactic| intro $h) => liftMetaTactic stx $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId h.getId; pure [mvarId]
| _ => throwUnsupportedSyntax
@[builtinTactic «exact»] def evalExact : Tactic :=
fun stx => match_syntax stx with
| `(tactic| exact $e) => do
let ref := stx;
(g, gs) ← getMainGoal stx;
withMVarContext g $ do {
decl ← getMVarDecl g;
val ← elabTerm e decl.type;
val ← ensureHasType ref decl.type val;
ensureHasNoMVars ref val;
assignExprMVar g val
};
setGoals gs
| _ => throwUnsupportedSyntax
@[builtinTactic «refine»] def evalRefine : Tactic :=
fun stx => match_syntax stx with
| `(tactic| refine $e) => do
let ref := stx;
(g, gs) ← getMainGoal stx;
gs' ← withMVarContext g $ do {
decl ← getMVarDecl g;
val ← elabTerm e decl.type;
val ← ensureHasType ref decl.type val;
assignExprMVar g val;
collectMVars ref val
};
setGoals (gs' ++ gs)
| _ => throwUnsupportedSyntax
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalTactic (stx.getArg 1)
@[builtinTactic nestedTacticBlock] def evalNestedTacticBlock : Tactic :=
fun stx => focus stx (evalTactic (stx.getArg 1))
@ -299,6 +271,11 @@ fun stx => match_syntax stx with
setGoals gs
| _ => throwUnsupportedSyntax
@[builtinTactic «orelse»] def evalOrelse : Tactic :=
fun stx => match_syntax stx with
| `(tactic| $tac1 <|> $tac2) => evalTactic tac1 <|> evalTactic tac2
| _ => throwUnsupportedSyntax
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.tactic;
pure ()

54
stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean Normal file
View file

@ -0,0 +1,54 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Elab.Tactic.Basic
import Init.Lean.Elab.SynthesizeSyntheticMVars
namespace Lean
namespace Elab
namespace Tactic
/- `elabTerm` for Tactics and basic tactics that use it. -/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) : TacticM Expr :=
liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { errToSorry := false, .. ctx }) $ do
e ← Term.elabTerm stx expectedType?;
Term.synthesizeSyntheticMVars false;
Term.instantiateMVars stx e
@[builtinTactic «exact»] def evalExact : Tactic :=
fun stx => match_syntax stx with
| `(tactic| exact $e) => do
let ref := stx;
(g, gs) ← getMainGoal stx;
withMVarContext g $ do {
decl ← getMVarDecl g;
val ← elabTerm e decl.type;
val ← ensureHasType ref decl.type val;
ensureHasNoMVars ref val;
assignExprMVar g val
};
setGoals gs
| _ => throwUnsupportedSyntax
@[builtinTactic «refine»] def evalRefine : Tactic :=
fun stx => match_syntax stx with
| `(tactic| refine $e) => do
let ref := stx;
(g, gs) ← getMainGoal stx;
gs' ← withMVarContext g $ do {
decl ← getMVarDecl g;
val ← elabTerm e decl.type;
val ← ensureHasType ref decl.type val;
assignExprMVar g val;
collectMVars ref val
};
setGoals (gs' ++ gs)
| _ => throwUnsupportedSyntax
end Tactic
end Elab
end Lean

25
stage0/src/Init/Lean/Elab/Term.lean
View file

@ -32,6 +32,7 @@ structure Context extends Meta.Context :=
The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
the list of pending synthetic metavariables, and returns `?m`. -/
(mayPostpone : Bool := true)
(errToSorry : Bool := true)
/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
inductive SyntheticMVarKind
@ -432,14 +433,14 @@ pure mvar
/-
Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
an error is found. -/
private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Expr) (errToSorry : Bool) (catchExPostpone : Bool)
private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
: List TermElab → TermElabM Expr
| [] => do
let refFmt := stx.prettyPrint;
throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
| (elabFn::elabFns) => catch (elabFn stx expectedType?)
(fun ex => match ex with
| Exception.ex (Elab.Exception.error errMsg) => if errToSorry then exceptionToSorry stx errMsg expectedType? else throw ex
| Exception.ex (Elab.Exception.error errMsg) => do ctx ← read; if ctx.errToSorry then exceptionToSorry stx errMsg expectedType? else throw ex
| Exception.ex Elab.Exception.unsupportedSyntax => do set s; elabTermUsing elabFns
| Exception.postpone =>
if catchExPostpone then do
@ -470,14 +471,14 @@ match x stx scp with
| none => throwUnsupportedSyntax
/- Main loop for `elabTerm` -/
partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := true) (errToSorry := true) : Syntax → TermElabM Expr
partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := 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
| some elabFns => elabTermUsing s node expectedType? catchExPostpone elabFns
| none => do
scp ← getCurrMacroScope;
env ← getEnv;
@ -498,8 +499,8 @@ partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := true)
and returned.
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 :=
elabTermAux expectedType? catchExPostpone errToSorry stx
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
elabTermAux expectedType? catchExPostpone stx
/-- Adapt a syntax transformation to a regular, term-producing elaborator. -/
def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab :=
@ -643,6 +644,18 @@ fun stx expectedType? =>
let name := stx.getIdAt 1;
mkFreshExprMVar stx expectedType? MetavarKind.syntheticOpaque name
def mkTacticMVar (ref : Syntax) (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
mvar ← mkFreshExprMVar ref type MetavarKind.syntheticOpaque `main;
let mvarId := mvar.mvarId!;
registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode;
pure mvar
@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
fun stx expectedType? =>
match expectedType? with
| some expectedType => mkTacticMVar stx expectedType (stx.getArg 1)
| none => throwError stx ("invalid tactic block, expected type has not been provided")
/-- Main loop for `mkPairs`. -/
private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syntax
| i, acc =>

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

@ -46,6 +46,9 @@ private def extractMacroScopesAux : Name → List MacroScope → Name × List Ma
def extractMacroScopes (n : Name) : Name × List MacroScope :=
extractMacroScopesAux n []
def Name.eraseMacroScopes (n : Name) : Name :=
(extractMacroScopes n).1
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
{ getCurrMacroScope := liftM (getCurrMacroScope : m Nat),
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }

5
stage0/src/Init/Lean/Parser/Syntax.lean
View file

@ -62,8 +62,9 @@ def identPrec := parser! ident >> optPrecedence
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgSimple := parser! ident >> ":" >> ident >> optPrecedence
def macroArg := try strLitPrec <|> try macroArgSimple
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> (ident >> optPrecedence)
def macroArgSimple := parser! ident >> ":" >> macroArgType
def macroArg := try strLitPrec <|> try macroArgSimple
def macroHead := try strLitPrec <|> try identPrec
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"

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

@ -205,3 +205,5 @@ instance MacroM.monadQuotation : MonadQuotation MacroM :=
abbrev Macro := Syntax → MacroM Syntax
end Lean
abbrev Array.getSepElems := @Array.getEvenElems

2
stage0/stdlib/CMakeLists.txt
View file

File diff suppressed because one or more lines are too long

80
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -275,7 +275,7 @@ lean_object* l_Lean_Elab_Term_ElabFComp(lean_object*, lean_object*, lean_object*
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*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_elabMapRev___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__2;
@ -2601,12 +2601,12 @@ 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_elabTermAux___main(x_2, x_61, x_61, x_57, x_3, x_26);
x_62 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_61, x_57, x_3, x_26);
return x_62;
}
else
{
lean_object* x_63; 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; lean_object* x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; uint8_t x_76; lean_object* x_77;
lean_object* x_63; 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; lean_object* x_71; lean_object* x_72; uint8_t x_73; uint8_t x_74; lean_object* x_75; lean_object* x_76; uint8_t x_77; lean_object* x_78;
x_63 = lean_ctor_get(x_3, 0);
x_64 = lean_ctor_get(x_3, 1);
x_65 = lean_ctor_get(x_3, 2);
@ -2618,6 +2618,7 @@ x_70 = lean_ctor_get(x_3, 7);
x_71 = lean_ctor_get(x_3, 8);
x_72 = lean_ctor_get(x_3, 9);
x_73 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
x_74 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
lean_inc(x_72);
lean_inc(x_71);
lean_inc(x_70);
@ -2629,34 +2630,35 @@ lean_inc(x_65);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_3);
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_1);
lean_ctor_set(x_74, 1, x_71);
x_75 = lean_alloc_ctor(0, 10, 1);
lean_ctor_set(x_75, 0, x_63);
lean_ctor_set(x_75, 1, x_64);
lean_ctor_set(x_75, 2, x_65);
lean_ctor_set(x_75, 3, x_66);
lean_ctor_set(x_75, 4, x_67);
lean_ctor_set(x_75, 5, x_68);
lean_ctor_set(x_75, 6, x_69);
lean_ctor_set(x_75, 7, x_70);
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_elabTermAux___main(x_2, x_76, x_76, x_57, x_75, x_26);
return x_77;
x_75 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_75, 0, x_1);
lean_ctor_set(x_75, 1, x_71);
x_76 = lean_alloc_ctor(0, 10, 2);
lean_ctor_set(x_76, 0, x_63);
lean_ctor_set(x_76, 1, x_64);
lean_ctor_set(x_76, 2, x_65);
lean_ctor_set(x_76, 3, x_66);
lean_ctor_set(x_76, 4, x_67);
lean_ctor_set(x_76, 5, x_68);
lean_ctor_set(x_76, 6, x_69);
lean_ctor_set(x_76, 7, x_70);
lean_ctor_set(x_76, 8, x_75);
lean_ctor_set(x_76, 9, x_72);
lean_ctor_set_uint8(x_76, sizeof(void*)*10, x_73);
lean_ctor_set_uint8(x_76, sizeof(void*)*10 + 1, x_74);
x_77 = 1;
x_78 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_77, x_57, x_76, x_26);
return x_78;
}
}
}
else
{
lean_object* x_78;
lean_object* x_79;
lean_dec(x_37);
lean_dec(x_2);
x_78 = lean_box(0);
x_27 = x_78;
x_79 = lean_box(0);
x_27 = x_79;
goto block_34;
}
}
@ -2681,11 +2683,11 @@ return x_33;
}
else
{
lean_object* x_79;
lean_object* x_80;
lean_dec(x_22);
lean_dec(x_2);
x_79 = lean_box(0);
x_15 = x_79;
x_80 = lean_box(0);
x_15 = x_80;
goto block_21;
}
block_21:
@ -2707,27 +2709,27 @@ return x_20;
}
else
{
uint8_t x_80;
uint8_t x_81;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_80 = !lean_is_exclusive(x_5);
if (x_80 == 0)
x_81 = !lean_is_exclusive(x_5);
if (x_81 == 0)
{
return x_5;
}
else
{
lean_object* x_81; lean_object* x_82; lean_object* x_83;
x_81 = lean_ctor_get(x_5, 0);
x_82 = lean_ctor_get(x_5, 1);
lean_object* x_82; lean_object* x_83; lean_object* x_84;
x_82 = lean_ctor_get(x_5, 0);
x_83 = lean_ctor_get(x_5, 1);
lean_inc(x_83);
lean_inc(x_82);
lean_inc(x_81);
lean_dec(x_5);
x_83 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
return x_83;
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;
}
}
}
@ -5417,7 +5419,7 @@ x_11 = lean_array_push(x_10, x_7);
x_12 = lean_array_push(x_11, x_9);
x_13 = l_Lean_mkAppStx(x_1, x_12);
x_14 = 1;
x_15 = l_Lean_Elab_Term_elabTermAux___main(x_3, x_14, x_14, x_13, x_4, x_5);
x_15 = l_Lean_Elab_Term_elabTermAux___main(x_3, x_14, x_13, x_4, x_5);
return x_15;
}
}

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

@ -143,6 +143,7 @@ lean_object* l_Lean_SMap_empty___at_Lean_Elab_Command_mkBuiltinCommandElabTable_
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport(lean_object*);
lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__2;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_isLevelDefEqAux___main___closed__5;
lean_object* l_List_foldl___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_addOpenDecl___spec__1(lean_object*, lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
@ -159,6 +160,7 @@ lean_object* l_Lean_Elab_mkMessageAt___at_Lean_Elab_Command_throwError___spec__3
lean_object* l_Lean_Elab_Command_elabSetOption___closed__3;
extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
lean_object* l_Lean_Elab_Command_elabSynth___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabVariables___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabUniverses___boxed(lean_object*, lean_object*, lean_object*);
@ -271,7 +273,7 @@ lean_object* l_Lean_Elab_Command_addBuiltinCommandElab___boxed(lean_object*, lea
lean_object* l_Lean_Elab_Command_CommandElabCoreM_monadState;
lean_object* l___private_Init_Lean_Elab_Command_14__checkEndHeader___boxed(lean_object*, lean_object*);
size_t l_Lean_Name_hash(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_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1___closed__4;
lean_object* l___private_Init_Lean_Elab_Command_1__ioErrorToMessage___boxed(lean_object*, lean_object*, lean_object*);
@ -386,7 +388,6 @@ extern lean_object* l_Lean_Syntax_inhabited;
lean_object* l_Lean_Meta_synthInstance(lean_object*, lean_object*, lean_object*);
lean_object* l_List_drop___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_addUnivLevel___spec__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_evalTactic___main___closed__4;
lean_object* l_Lean_Elab_Command_elabExport___closed__2;
lean_object* l_Lean_Elab_Command_elabCommand___main___closed__1;
lean_object* l_AssocList_contains___main___at_Lean_Elab_Command_addBuiltinCommandElab___spec__3___boxed(lean_object*, lean_object*);
@ -425,6 +426,7 @@ lean_object* l_Lean_Elab_Command_elabEnd___closed__1;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_withDeclId___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__5;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverse___closed__2;
lean_object* l_Lean_Elab_Command_elabCommand___main___closed__4;
lean_object* l_Lean_Elab_Command_elabEnd___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_withIncRecDepth(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
@ -4852,6 +4854,16 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Command_elabCommand___main___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_Meta_isLevelDefEqAux___main___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Command_elabCommand___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -4979,7 +4991,7 @@ lean_inc(x_82);
x_83 = lean_ctor_get(x_81, 1);
lean_inc(x_83);
lean_dec(x_81);
x_84 = l_Lean_Elab_Tactic_evalTactic___main___closed__4;
x_84 = l_Lean_Elab_Command_elabCommand___main___closed__4;
x_85 = l_Lean_checkTraceOption(x_82, x_84);
lean_dec(x_82);
if (x_85 == 0)
@ -5387,7 +5399,7 @@ lean_inc(x_162);
x_163 = lean_ctor_get(x_161, 1);
lean_inc(x_163);
lean_dec(x_161);
x_164 = l_Lean_Elab_Tactic_evalTactic___main___closed__4;
x_164 = l_Lean_Elab_Command_elabCommand___main___closed__4;
x_165 = l_Lean_checkTraceOption(x_162, x_164);
lean_dec(x_162);
if (x_165 == 0)
@ -5879,7 +5891,7 @@ lean_inc(x_253);
x_254 = lean_ctor_get(x_252, 1);
lean_inc(x_254);
lean_dec(x_252);
x_255 = l_Lean_Elab_Tactic_evalTactic___main___closed__4;
x_255 = l_Lean_Elab_Command_elabCommand___main___closed__4;
x_256 = l_Lean_checkTraceOption(x_253, x_255);
lean_dec(x_253);
if (x_256 == 0)
@ -6571,7 +6583,7 @@ lean_inc(x_16);
lean_inc(x_15);
lean_inc(x_13);
lean_inc(x_12);
x_24 = lean_alloc_ctor(0, 10, 1);
x_24 = lean_alloc_ctor(0, 10, 2);
lean_ctor_set(x_24, 0, x_20);
lean_ctor_set(x_24, 1, x_12);
lean_ctor_set(x_24, 2, x_13);
@ -6583,6 +6595,7 @@ lean_ctor_set(x_24, 7, x_23);
lean_ctor_set(x_24, 8, x_16);
lean_ctor_set(x_24, 9, x_17);
lean_ctor_set_uint8(x_24, sizeof(void*)*10, x_8);
lean_ctor_set_uint8(x_24, sizeof(void*)*10 + 1, x_8);
return x_24;
}
}
@ -16092,7 +16105,7 @@ _start:
uint8_t x_7; lean_object* x_8;
x_7 = 1;
lean_inc(x_5);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_7, x_7, x_2, x_5, x_6);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_7, x_2, x_5, x_6);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
@ -16722,7 +16735,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_elabTermAux___main(x_6, x_7, x_7, x_1, x_4, x_5);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_6, x_7, x_1, x_4, x_5);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
@ -22382,6 +22395,8 @@ l_Lean_Elab_Command_elabCommand___main___closed__2 = _init_l_Lean_Elab_Command_e
lean_mark_persistent(l_Lean_Elab_Command_elabCommand___main___closed__2);
l_Lean_Elab_Command_elabCommand___main___closed__3 = _init_l_Lean_Elab_Command_elabCommand___main___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_elabCommand___main___closed__3);
l_Lean_Elab_Command_elabCommand___main___closed__4 = _init_l_Lean_Elab_Command_elabCommand___main___closed__4();
lean_mark_persistent(l_Lean_Elab_Command_elabCommand___main___closed__4);
l___private_Init_Lean_Elab_Command_9__toCommandResult___rarg___closed__1 = _init_l___private_Init_Lean_Elab_Command_9__toCommandResult___rarg___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Command_9__toCommandResult___rarg___closed__1);
l_Lean_Elab_Command_CommandElabM_inhabited___closed__1 = _init_l_Lean_Elab_Command_CommandElabM_inhabited___closed__1();

86
stage0/stdlib/Init/Lean/Elab/Definition.c
View file

@ -70,7 +70,7 @@ extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2
lean_object* l_Lean_Expr_fvarId_x21(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_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___closed__1;
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*);
@ -1194,7 +1194,7 @@ return x_29;
}
else
{
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; uint8_t x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
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; uint8_t x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_30 = lean_ctor_get(x_8, 1);
x_31 = lean_ctor_get(x_8, 2);
x_32 = lean_ctor_get(x_8, 3);
@ -1205,6 +1205,7 @@ x_36 = lean_ctor_get(x_8, 7);
x_37 = lean_ctor_get(x_8, 8);
x_38 = lean_ctor_get(x_8, 9);
x_39 = lean_ctor_get_uint8(x_8, sizeof(void*)*10);
x_40 = lean_ctor_get_uint8(x_8, sizeof(void*)*10 + 1);
lean_inc(x_38);
lean_inc(x_37);
lean_inc(x_36);
@ -1215,71 +1216,72 @@ lean_inc(x_32);
lean_inc(x_31);
lean_inc(x_30);
lean_dec(x_8);
x_40 = lean_ctor_get(x_14, 0);
lean_inc(x_40);
x_41 = lean_ctor_get(x_14, 3);
x_41 = lean_ctor_get(x_14, 0);
lean_inc(x_41);
x_42 = lean_ctor_get(x_14, 4);
x_42 = lean_ctor_get(x_14, 3);
lean_inc(x_42);
x_43 = lean_ctor_get(x_14, 4);
lean_inc(x_43);
if (lean_is_exclusive(x_14)) {
lean_ctor_release(x_14, 0);
lean_ctor_release(x_14, 1);
lean_ctor_release(x_14, 2);
lean_ctor_release(x_14, 3);
lean_ctor_release(x_14, 4);
x_43 = x_14;
x_44 = x_14;
} else {
lean_dec_ref(x_14);
x_43 = lean_box(0);
x_44 = lean_box(0);
}
if (lean_is_scalar(x_43)) {
x_44 = lean_alloc_ctor(0, 5, 0);
if (lean_is_scalar(x_44)) {
x_45 = lean_alloc_ctor(0, 5, 0);
} else {
x_44 = x_43;
x_45 = x_44;
}
lean_ctor_set(x_44, 0, x_40);
lean_ctor_set(x_44, 1, x_16);
lean_ctor_set(x_44, 2, x_17);
lean_ctor_set(x_44, 3, x_41);
lean_ctor_set(x_44, 4, x_42);
x_45 = lean_alloc_ctor(0, 10, 1);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_30);
lean_ctor_set(x_45, 2, x_31);
lean_ctor_set(x_45, 3, x_32);
lean_ctor_set(x_45, 4, x_33);
lean_ctor_set(x_45, 5, x_34);
lean_ctor_set(x_45, 6, x_35);
lean_ctor_set(x_45, 7, x_36);
lean_ctor_set(x_45, 8, x_37);
lean_ctor_set(x_45, 9, x_38);
lean_ctor_set_uint8(x_45, sizeof(void*)*10, x_39);
x_46 = lean_apply_3(x_7, x_18, x_45, x_15);
return x_46;
lean_ctor_set(x_45, 0, x_41);
lean_ctor_set(x_45, 1, x_16);
lean_ctor_set(x_45, 2, x_17);
lean_ctor_set(x_45, 3, x_42);
lean_ctor_set(x_45, 4, x_43);
x_46 = lean_alloc_ctor(0, 10, 2);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_30);
lean_ctor_set(x_46, 2, x_31);
lean_ctor_set(x_46, 3, x_32);
lean_ctor_set(x_46, 4, x_33);
lean_ctor_set(x_46, 5, x_34);
lean_ctor_set(x_46, 6, x_35);
lean_ctor_set(x_46, 7, x_36);
lean_ctor_set(x_46, 8, x_37);
lean_ctor_set(x_46, 9, x_38);
lean_ctor_set_uint8(x_46, sizeof(void*)*10, x_39);
lean_ctor_set_uint8(x_46, sizeof(void*)*10 + 1, x_40);
x_47 = lean_apply_3(x_7, x_18, x_46, x_15);
return x_47;
}
}
else
{
uint8_t x_47;
uint8_t x_48;
lean_dec(x_8);
lean_dec(x_7);
x_47 = !lean_is_exclusive(x_11);
if (x_47 == 0)
x_48 = !lean_is_exclusive(x_11);
if (x_48 == 0)
{
return x_11;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_11, 0);
x_49 = lean_ctor_get(x_11, 1);
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_11, 0);
x_50 = lean_ctor_get(x_11, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_11);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
@ -2018,7 +2020,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_elabTermAux___main(x_15, x_16, x_16, x_14, x_3, x_4);
x_17 = l_Lean_Elab_Term_elabTermAux___main(x_15, x_16, x_14, x_3, x_4);
return x_17;
}
}

22429
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

3879
stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
View file

File diff suppressed because it is too large Load diff

1200
stage0/stdlib/Init/Lean/Elab/Tactic.c
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

922
stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c Normal file
View file

@ -0,0 +1,922 @@
// Lean compiler output
// Module: Init.Lean.Elab.Tactic.ElabTerm
// Imports: Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.SynthesizeSyntheticMVars
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(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___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1;
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRefine(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3;
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTerm___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1;
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_setGoals(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_10__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTerm(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
lean_object* l_Lean_Elab_Tactic_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_collectMVars(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2;
extern lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3;
lean_object* l_Lean_Elab_Tactic_evalExact(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTerm___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_3);
if (x_5 == 0)
{
uint8_t x_6; uint8_t x_7; lean_object* x_8;
x_6 = 0;
lean_ctor_set_uint8(x_3, sizeof(void*)*10 + 1, x_6);
x_7 = 1;
lean_inc(x_3);
lean_inc(x_2);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_7, x_2, x_3, x_4);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_box(0);
lean_inc(x_3);
x_12 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_10__synthesizeSyntheticMVarsAux___main(x_6, x_11, x_3, x_10);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = l_Lean_Elab_Term_instantiateMVars(x_2, x_9, x_3, x_13);
lean_dec(x_2);
return x_14;
}
else
{
uint8_t x_15;
lean_dec(x_9);
lean_dec(x_3);
lean_dec(x_2);
x_15 = !lean_is_exclusive(x_12);
if (x_15 == 0)
{
return x_12;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_12, 0);
x_17 = lean_ctor_get(x_12, 1);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_12);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
return x_18;
}
}
}
else
{
uint8_t x_19;
lean_dec(x_3);
lean_dec(x_2);
x_19 = !lean_is_exclusive(x_8);
if (x_19 == 0)
{
return x_8;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_8, 0);
x_21 = lean_ctor_get(x_8, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_8);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
else
{
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; uint8_t x_33; uint8_t x_34; lean_object* x_35; uint8_t x_36; lean_object* x_37;
x_23 = lean_ctor_get(x_3, 0);
x_24 = lean_ctor_get(x_3, 1);
x_25 = lean_ctor_get(x_3, 2);
x_26 = lean_ctor_get(x_3, 3);
x_27 = lean_ctor_get(x_3, 4);
x_28 = lean_ctor_get(x_3, 5);
x_29 = lean_ctor_get(x_3, 6);
x_30 = lean_ctor_get(x_3, 7);
x_31 = lean_ctor_get(x_3, 8);
x_32 = lean_ctor_get(x_3, 9);
x_33 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
lean_inc(x_32);
lean_inc(x_31);
lean_inc(x_30);
lean_inc(x_29);
lean_inc(x_28);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_3);
x_34 = 0;
x_35 = lean_alloc_ctor(0, 10, 2);
lean_ctor_set(x_35, 0, x_23);
lean_ctor_set(x_35, 1, x_24);
lean_ctor_set(x_35, 2, x_25);
lean_ctor_set(x_35, 3, x_26);
lean_ctor_set(x_35, 4, x_27);
lean_ctor_set(x_35, 5, x_28);
lean_ctor_set(x_35, 6, x_29);
lean_ctor_set(x_35, 7, x_30);
lean_ctor_set(x_35, 8, x_31);
lean_ctor_set(x_35, 9, x_32);
lean_ctor_set_uint8(x_35, sizeof(void*)*10, x_33);
lean_ctor_set_uint8(x_35, sizeof(void*)*10 + 1, x_34);
x_36 = 1;
lean_inc(x_35);
lean_inc(x_2);
x_37 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_36, x_2, x_35, x_4);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_38 = lean_ctor_get(x_37, 0);
lean_inc(x_38);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
lean_dec(x_37);
x_40 = lean_box(0);
lean_inc(x_35);
x_41 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_10__synthesizeSyntheticMVarsAux___main(x_34, x_40, x_35, x_39);
if (lean_obj_tag(x_41) == 0)
{
lean_object* x_42; lean_object* x_43;
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
x_43 = l_Lean_Elab_Term_instantiateMVars(x_2, x_38, x_35, x_42);
lean_dec(x_2);
return x_43;
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
lean_dec(x_38);
lean_dec(x_35);
lean_dec(x_2);
x_44 = lean_ctor_get(x_41, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_41, 1);
lean_inc(x_45);
if (lean_is_exclusive(x_41)) {
lean_ctor_release(x_41, 0);
lean_ctor_release(x_41, 1);
x_46 = x_41;
} else {
lean_dec_ref(x_41);
x_46 = lean_box(0);
}
if (lean_is_scalar(x_46)) {
x_47 = lean_alloc_ctor(1, 2, 0);
} else {
x_47 = x_46;
}
lean_ctor_set(x_47, 0, x_44);
lean_ctor_set(x_47, 1, x_45);
return x_47;
}
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
lean_dec(x_35);
lean_dec(x_2);
x_48 = lean_ctor_get(x_37, 0);
lean_inc(x_48);
x_49 = lean_ctor_get(x_37, 1);
lean_inc(x_49);
if (lean_is_exclusive(x_37)) {
lean_ctor_release(x_37, 0);
lean_ctor_release(x_37, 1);
x_50 = x_37;
} else {
lean_dec_ref(x_37);
x_50 = lean_box(0);
}
if (lean_is_scalar(x_50)) {
x_51 = lean_alloc_ctor(1, 2, 0);
} else {
x_51 = x_50;
}
lean_ctor_set(x_51, 0, x_48);
lean_ctor_set(x_51, 1, x_49);
return x_51;
}
}
}
}
lean_object* l_Lean_Elab_Tactic_elabTerm(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabTerm___lambda__1), 4, 2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = l_Lean_Elab_Tactic_liftTermElabM___rarg(x_5, x_3, x_4);
return x_6;
}
}
lean_object* l_Lean_Elab_Tactic_evalExact___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) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_4, 2);
lean_inc(x_7);
x_8 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_8, 0, x_7);
lean_inc(x_5);
lean_inc(x_8);
x_9 = l_Lean_Elab_Tactic_elabTerm(x_1, x_8, x_5, x_6);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
lean_inc(x_5);
lean_inc(x_2);
x_12 = l_Lean_Elab_Tactic_ensureHasType(x_2, x_8, x_10, x_5, x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
lean_inc(x_5);
lean_inc(x_13);
x_15 = l_Lean_Elab_Tactic_ensureHasNoMVars(x_2, x_13, x_5, x_14);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l_Lean_Elab_Tactic_assignExprMVar(x_3, x_13, x_5, x_16);
return x_17;
}
else
{
uint8_t x_18;
lean_dec(x_13);
lean_dec(x_5);
lean_dec(x_3);
x_18 = !lean_is_exclusive(x_15);
if (x_18 == 0)
{
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 0);
x_20 = lean_ctor_get(x_15, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_15);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
else
{
uint8_t x_22;
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_12);
if (x_22 == 0)
{
return x_12;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_12, 0);
x_24 = lean_ctor_get(x_12, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_12);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_26 = !lean_is_exclusive(x_9);
if (x_26 == 0)
{
return x_9;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_9, 0);
x_28 = lean_ctor_get(x_9, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_9);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
}
lean_object* l_Lean_Elab_Tactic_evalExact(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_29; uint8_t x_30;
x_29 = l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
lean_inc(x_1);
x_30 = l_Lean_Syntax_isOfKind(x_1, x_29);
if (x_30 == 0)
{
uint8_t x_31;
x_31 = 0;
x_4 = x_31;
goto block_28;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
x_32 = l_Lean_Syntax_getArgs(x_1);
x_33 = lean_array_get_size(x_32);
lean_dec(x_32);
x_34 = lean_unsigned_to_nat(2u);
x_35 = lean_nat_dec_eq(x_33, x_34);
lean_dec(x_33);
x_4 = x_35;
goto block_28;
}
block_28:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_1);
x_6 = l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(x_2, x_3);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_unsigned_to_nat(1u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
lean_inc(x_2);
lean_inc(x_1);
x_9 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
lean_inc(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_14, 0, x_12);
lean_inc(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalExact___lambda__1___boxed), 6, 3);
lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_1);
lean_closure_set(x_15, 2, x_12);
x_16 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_16, 0, x_14);
lean_closure_set(x_16, 1, x_15);
lean_inc(x_2);
x_17 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_12, x_16, x_2, x_11);
lean_dec(x_12);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = l_Lean_Elab_Tactic_setGoals(x_13, x_2, x_18);
lean_dec(x_2);
return x_19;
}
else
{
uint8_t x_20;
lean_dec(x_13);
lean_dec(x_2);
x_20 = !lean_is_exclusive(x_17);
if (x_20 == 0)
{
return x_17;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 0);
x_22 = lean_ctor_get(x_17, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_17);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
}
else
{
uint8_t x_24;
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_24 = !lean_is_exclusive(x_9);
if (x_24 == 0)
{
return x_9;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_9, 0);
x_26 = lean_ctor_get(x_9, 1);
lean_inc(x_26);
lean_inc(x_25);
lean_dec(x_9);
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
return x_27;
}
}
}
}
}
}
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Elab_Tactic_evalExact___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
return x_7;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalExact");
return x_1;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalExact), 3, 0);
return x_1;
}
}
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2;
x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3;
x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Tactic_evalRefine___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) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_4, 2);
lean_inc(x_7);
x_8 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_8, 0, x_7);
lean_inc(x_5);
lean_inc(x_8);
x_9 = l_Lean_Elab_Tactic_elabTerm(x_1, x_8, x_5, x_6);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
lean_inc(x_5);
lean_inc(x_2);
x_12 = l_Lean_Elab_Tactic_ensureHasType(x_2, x_8, x_10, x_5, x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
lean_inc(x_5);
lean_inc(x_13);
x_15 = l_Lean_Elab_Tactic_assignExprMVar(x_3, x_13, x_5, x_14);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l_Lean_Elab_Tactic_collectMVars(x_2, x_13, x_5, x_16);
return x_17;
}
else
{
uint8_t x_18;
lean_dec(x_13);
lean_dec(x_5);
lean_dec(x_2);
x_18 = !lean_is_exclusive(x_15);
if (x_18 == 0)
{
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 0);
x_20 = lean_ctor_get(x_15, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_15);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
else
{
uint8_t x_22;
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_12);
if (x_22 == 0)
{
return x_12;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_12, 0);
x_24 = lean_ctor_get(x_12, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_12);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_26 = !lean_is_exclusive(x_9);
if (x_26 == 0)
{
return x_9;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_9, 0);
x_28 = lean_ctor_get(x_9, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_9);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
}
lean_object* l_Lean_Elab_Tactic_evalRefine(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_31; uint8_t x_32;
x_31 = l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
lean_inc(x_1);
x_32 = l_Lean_Syntax_isOfKind(x_1, x_31);
if (x_32 == 0)
{
uint8_t x_33;
x_33 = 0;
x_4 = x_33;
goto block_30;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37;
x_34 = l_Lean_Syntax_getArgs(x_1);
x_35 = lean_array_get_size(x_34);
lean_dec(x_34);
x_36 = lean_unsigned_to_nat(2u);
x_37 = lean_nat_dec_eq(x_35, x_36);
lean_dec(x_35);
x_4 = x_37;
goto block_30;
}
block_30:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_1);
x_6 = l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(x_2, x_3);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_unsigned_to_nat(1u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
lean_inc(x_2);
lean_inc(x_1);
x_9 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
lean_inc(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_14, 0, x_12);
lean_inc(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalRefine___lambda__1___boxed), 6, 3);
lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_1);
lean_closure_set(x_15, 2, x_12);
x_16 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_16, 0, x_14);
lean_closure_set(x_16, 1, x_15);
lean_inc(x_2);
x_17 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_12, x_16, x_2, x_11);
lean_dec(x_12);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_List_append___rarg(x_18, x_13);
x_21 = l_Lean_Elab_Tactic_setGoals(x_20, x_2, x_19);
lean_dec(x_2);
return x_21;
}
else
{
uint8_t x_22;
lean_dec(x_13);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_17);
if (x_22 == 0)
{
return x_17;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_17, 0);
x_24 = lean_ctor_get(x_17, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_17);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_26 = !lean_is_exclusive(x_9);
if (x_26 == 0)
{
return x_9;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_9, 0);
x_28 = lean_ctor_get(x_9, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_9);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
}
}
}
lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Elab_Tactic_evalRefine___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
return x_7;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalRefine");
return x_1;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalRefine), 3, 0);
return x_1;
}
}
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2;
x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3;
x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*);
lean_object* initialize_Init_Lean_Elab_SynthesizeSyntheticMVars(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Elab_Tactic_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Elab_SynthesizeSyntheticMVars(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1);
l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2);
l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__3);
res = l___regBuiltinTactic_Lean_Elab_Tactic_evalExact(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1);
l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__2);
l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3();
lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3);
res = l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(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
}
#endif

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

File diff suppressed because it is too large Load diff

12
stage0/stdlib/Init/Lean/Elab/TermApp.c
View file

@ -164,7 +164,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_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_TermApp_19__expandApp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
@ -940,7 +940,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_elabTermAux___main(x_8, x_9, x_9, x_7, x_5, x_6);
x_10 = l_Lean_Elab_Term_elabTermAux___main(x_8, 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;
@ -6472,7 +6472,7 @@ lean_dec(x_206);
x_213 = lean_box(0);
x_214 = 1;
lean_inc(x_9);
x_215 = l_Lean_Elab_Term_elabTermAux___main(x_213, x_214, x_214, x_2, x_9, x_10);
x_215 = l_Lean_Elab_Term_elabTermAux___main(x_213, x_214, x_2, x_9, x_10);
if (lean_obj_tag(x_215) == 0)
{
uint8_t x_216;
@ -6872,7 +6872,7 @@ lean_dec(x_302);
x_306 = lean_box(0);
x_307 = 1;
lean_inc(x_9);
x_308 = l_Lean_Elab_Term_elabTermAux___main(x_306, x_307, x_307, x_2, x_9, x_10);
x_308 = l_Lean_Elab_Term_elabTermAux___main(x_306, x_307, x_2, x_9, x_10);
if (lean_obj_tag(x_308) == 0)
{
uint8_t x_309;
@ -7200,7 +7200,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_elabTermAux___main(x_13, x_14, x_14, x_2, x_9, x_10);
x_15 = l_Lean_Elab_Term_elabTermAux___main(x_13, x_14, x_2, x_9, x_10);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_16;
@ -7512,7 +7512,7 @@ lean_dec(x_71);
x_75 = lean_box(0);
x_76 = 1;
lean_inc(x_9);
x_77 = l_Lean_Elab_Term_elabTermAux___main(x_75, x_76, x_76, x_2, x_9, x_10);
x_77 = l_Lean_Elab_Term_elabTermAux___main(x_75, x_76, x_2, x_9, x_10);
if (lean_obj_tag(x_77) == 0)
{
uint8_t x_78;

2458
stage0/stdlib/Init/Lean/Elab/TermBinders.c
View file

File diff suppressed because it is too large Load diff

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

@ -17,6 +17,7 @@ lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_extractMacroScopes(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__3;
lean_object* l_Lean_Name_eraseMacroScopes(lean_object*);
lean_object* l___private_Init_Lean_Hygiene_1__extractMacroScopesAux(lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_run(lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg(lean_object*, lean_object*, lean_object*);
@ -164,6 +165,17 @@ x_3 = l___private_Init_Lean_Hygiene_1__extractMacroScopesAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Name_eraseMacroScopes(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_extractMacroScopes(x_1);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

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

@ -45,6 +45,7 @@ lean_object* l_Lean_Parser_ParserState_mkError(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mixfix;
lean_object* l_Lean_Parser_Command_mixfixSymbol___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_lookahead___closed__4;
lean_object* l_Lean_Parser_Command_macroArgType___closed__4;
lean_object* l_Lean_Parser_Syntax_num___closed__5;
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__1;
lean_object* l_Lean_Parser_Syntax_try___closed__3;
@ -60,6 +61,7 @@ lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__3;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_stxQuot___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_macroArgType___closed__2;
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__8;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__7;
lean_object* l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__2;
@ -77,6 +79,7 @@ lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__5;
lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macro___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_macroArgType___closed__1;
lean_object* l_Lean_Parser_Syntax_sepBy___closed__3;
lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__8;
@ -155,6 +158,7 @@ lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, le
lean_object* l_Lean_Parser_Command_infixl___closed__4;
lean_object* l_Lean_Parser_Syntax_many___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_paren___closed__3;
lean_object* l_Lean_Parser_Command_macroArgType___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_infix;
lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__2;
@ -273,6 +277,7 @@ lean_object* l_Lean_Parser_Syntax_optional___closed__4;
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_syntax___closed__3;
lean_object* l_Lean_Parser_Syntax_orelse___closed__3;
lean_object* l_Lean_Parser_Command_macroArgType___closed__3;
lean_object* l_Lean_Parser_Syntax_sepBy1___closed__4;
lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__6;
lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
@ -303,11 +308,13 @@ lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__9;
lean_object* l_Lean_Parser_precedence___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_identPrec___closed__3;
lean_object* l_Lean_Parser_Command_macroArgType;
lean_object* l_Lean_Parser_Syntax_num___closed__2;
lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__5;
lean_object* l_Lean_Parser_Syntax_num___closed__1;
lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_postfix___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macroArgType___closed__5;
lean_object* l_Lean_Parser_Command_syntax___closed__10;
lean_object* l_Lean_Parser_Syntax_ident;
lean_object* l_Lean_Parser_Syntax_num___closed__4;
@ -10487,6 +10494,253 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Parser_Command_macroArgType___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
x_9 = l_Lean_Parser_Syntax_ident___elambda__1___closed__4;
x_10 = l_Lean_Parser_Syntax_ident___elambda__1___closed__6;
lean_inc(x_2);
x_11 = l_Lean_Parser_nonReservedSymbolFnAux(x_9, x_10, x_2, x_3);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_nat_dec_eq(x_14, x_8);
lean_dec(x_14);
if (x_15 == 0)
{
lean_dec(x_13);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_inc(x_8);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_7, x_8);
lean_dec(x_7);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = l_Lean_Parser_Syntax_num___elambda__1___closed__4;
x_20 = l_Lean_Parser_Syntax_num___elambda__1___closed__6;
lean_inc(x_2);
x_21 = l_Lean_Parser_nonReservedSymbolFnAux(x_19, x_20, x_2, x_16);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23;
lean_dec(x_18);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_23 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_8);
lean_dec(x_8);
return x_23;
}
else
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_26 = lean_nat_dec_eq(x_25, x_8);
lean_dec(x_25);
if (x_26 == 0)
{
lean_object* x_27;
lean_dec(x_24);
lean_dec(x_18);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_27 = l_Lean_Parser_mergeOrElseErrors(x_21, x_13, x_8);
lean_dec(x_8);
return x_27;
}
else
{
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_inc(x_8);
x_28 = l_Lean_Parser_ParserState_restore(x_21, x_18, x_8);
lean_dec(x_18);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
x_30 = lean_array_get_size(x_29);
lean_dec(x_29);
x_31 = l_Lean_Parser_Syntax_str___elambda__1___closed__4;
x_32 = l_Lean_Parser_Syntax_str___elambda__1___closed__6;
lean_inc(x_2);
x_33 = l_Lean_Parser_nonReservedSymbolFnAux(x_31, x_32, x_2, x_28);
x_34 = lean_ctor_get(x_33, 3);
lean_inc(x_34);
if (lean_obj_tag(x_34) == 0)
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_30);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_35 = l_Lean_Parser_mergeOrElseErrors(x_33, x_24, x_8);
x_36 = l_Lean_Parser_mergeOrElseErrors(x_35, x_13, x_8);
lean_dec(x_8);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_37 = lean_ctor_get(x_34, 0);
lean_inc(x_37);
lean_dec(x_34);
x_38 = lean_ctor_get(x_33, 1);
lean_inc(x_38);
x_39 = lean_nat_dec_eq(x_38, x_8);
lean_dec(x_38);
if (x_39 == 0)
{
lean_object* x_40; lean_object* x_41;
lean_dec(x_37);
lean_dec(x_30);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_40 = l_Lean_Parser_mergeOrElseErrors(x_33, x_24, x_8);
x_41 = l_Lean_Parser_mergeOrElseErrors(x_40, x_13, x_8);
lean_dec(x_8);
return x_41;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
lean_inc(x_8);
x_42 = l_Lean_Parser_ParserState_restore(x_33, x_30, x_8);
lean_dec(x_30);
lean_inc(x_2);
lean_inc(x_1);
x_43 = lean_apply_3(x_5, x_1, x_2, x_42);
x_44 = lean_ctor_get(x_43, 3);
lean_inc(x_44);
if (lean_obj_tag(x_44) == 0)
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_45 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_43);
x_46 = l_Lean_Parser_mergeOrElseErrors(x_45, x_37, x_8);
x_47 = l_Lean_Parser_mergeOrElseErrors(x_46, x_24, x_8);
x_48 = l_Lean_Parser_mergeOrElseErrors(x_47, x_13, x_8);
lean_dec(x_8);
return x_48;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
lean_dec(x_44);
lean_dec(x_2);
lean_dec(x_1);
x_49 = l_Lean_Parser_mergeOrElseErrors(x_43, x_37, x_8);
x_50 = l_Lean_Parser_mergeOrElseErrors(x_49, x_24, x_8);
x_51 = l_Lean_Parser_mergeOrElseErrors(x_50, x_13, x_8);
lean_dec(x_8);
return x_51;
}
}
}
}
}
}
}
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgType___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_str___closed__1;
x_2 = l_Lean_Parser_Syntax_cat___closed__1;
x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgType___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_num___closed__1;
x_2 = l_Lean_Parser_Command_macroArgType___closed__1;
x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgType___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_ident___closed__1;
x_2 = l_Lean_Parser_Command_macroArgType___closed__2;
x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgType___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_macroArgType___elambda__1), 3, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgType___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_macroArgType___closed__3;
x_2 = l_Lean_Parser_Command_macroArgType___closed__4;
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_Parser_Command_macroArgType() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_macroArgType___closed__5;
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1() {
_start:
{
@ -10579,7 +10833,7 @@ return x_11;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_34; lean_object* x_35;
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_inc(x_10);
x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
lean_dec(x_9);
@ -10587,134 +10841,102 @@ x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
lean_inc(x_5);
lean_inc(x_2);
lean_inc(x_1);
x_34 = lean_apply_3(x_5, x_1, x_2, x_16);
x_35 = lean_ctor_get(x_34, 3);
lean_inc(x_35);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_inc(x_2);
x_37 = l_Lean_Parser_tokenFn(x_2, x_34);
x_38 = lean_ctor_get(x_37, 3);
lean_inc(x_38);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40;
x_39 = lean_ctor_get(x_37, 0);
lean_inc(x_39);
x_40 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_39);
lean_dec(x_39);
if (lean_obj_tag(x_40) == 2)
{
lean_object* x_41; lean_object* x_42; uint8_t x_43;
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
x_42 = l_Lean_Parser_mkAntiquot___closed__4;
x_43 = lean_string_dec_eq(x_41, x_42);
lean_dec(x_41);
if (x_43 == 0)
{
lean_object* x_44; lean_object* x_45;
x_44 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_45 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_44, x_36);
x_19 = x_45;
goto block_33;
}
else
{
lean_dec(x_36);
x_19 = x_37;
goto block_33;
}
}
else
{
lean_object* x_46; lean_object* x_47;
lean_dec(x_40);
x_46 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_46, x_36);
x_19 = x_47;
goto block_33;
}
}
else
{
lean_object* x_48; lean_object* x_49;
lean_dec(x_38);
x_48 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_48, x_36);
x_19 = x_49;
goto block_33;
}
}
else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52;
lean_dec(x_35);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_50 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_51 = l_Lean_Parser_ParserState_mkNode(x_34, x_50, x_18);
x_52 = l_Lean_Parser_mergeOrElseErrors(x_51, x_13, x_10);
lean_dec(x_10);
return x_52;
}
block_33:
{
lean_object* x_20;
x_19 = lean_apply_3(x_5, x_1, x_2, x_16);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_21; lean_object* x_22;
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_inc(x_2);
lean_inc(x_1);
x_21 = lean_apply_3(x_5, x_1, x_2, x_19);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
x_22 = l_Lean_Parser_tokenFn(x_2, x_19);
x_23 = lean_ctor_get(x_22, 3);
lean_inc(x_23);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = l_Lean_Parser_optPrecedence___elambda__1(x_1, x_2, x_21);
x_24 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_18);
x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_13, x_10);
lean_dec(x_10);
return x_26;
}
else
lean_object* x_24; lean_object* x_25;
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
x_25 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_24);
lean_dec(x_24);
if (lean_obj_tag(x_25) == 2)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_dec(x_22);
lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = l_Lean_Parser_mkAntiquot___closed__4;
x_28 = lean_string_dec_eq(x_26, x_27);
lean_dec(x_26);
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_2);
lean_dec(x_1);
x_27 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_28 = l_Lean_Parser_ParserState_mkNode(x_21, x_27, x_18);
x_29 = l_Lean_Parser_mergeOrElseErrors(x_28, x_13, x_10);
x_29 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_29, x_21);
x_31 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_18);
x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_13, x_10);
lean_dec(x_10);
return x_29;
return x_33;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
lean_dec(x_21);
x_34 = l_Lean_Parser_Command_macroArgType___elambda__1(x_1, x_2, x_22);
x_35 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_18);
x_37 = l_Lean_Parser_mergeOrElseErrors(x_36, x_13, x_10);
lean_dec(x_10);
return x_37;
}
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
lean_dec(x_25);
lean_dec(x_2);
lean_dec(x_1);
x_38 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_39 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_38, x_21);
x_40 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_41 = l_Lean_Parser_ParserState_mkNode(x_39, x_40, x_18);
x_42 = l_Lean_Parser_mergeOrElseErrors(x_41, x_13, x_10);
lean_dec(x_10);
return x_42;
}
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
lean_dec(x_23);
lean_dec(x_2);
lean_dec(x_1);
x_43 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_43, x_21);
x_45 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_46 = l_Lean_Parser_ParserState_mkNode(x_44, x_45, x_18);
x_47 = l_Lean_Parser_mergeOrElseErrors(x_46, x_13, x_10);
lean_dec(x_10);
return x_47;
}
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
lean_dec(x_20);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_30 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_31 = l_Lean_Parser_ParserState_mkNode(x_19, x_30, x_18);
x_32 = l_Lean_Parser_mergeOrElseErrors(x_31, x_13, x_10);
x_48 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_49 = l_Lean_Parser_ParserState_mkNode(x_19, x_48, x_18);
x_50 = l_Lean_Parser_mergeOrElseErrors(x_49, x_13, x_10);
lean_dec(x_10);
return x_32;
}
return x_50;
}
}
}
@ -10723,11 +10945,13 @@ return x_32;
lean_object* _init_l_Lean_Parser_Command_macroArgSimple___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_mkAntiquot___closed__5;
x_2 = l_Lean_Parser_Syntax_cat___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_macroArgType;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_mkAntiquot___closed__5;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_macroArgSimple___closed__2() {
@ -14237,6 +14461,18 @@ lean_mark_persistent(l_Lean_Parser_Command_syntaxCat);
res = l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Command_macroArgType___closed__1 = _init_l_Lean_Parser_Command_macroArgType___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType___closed__1);
l_Lean_Parser_Command_macroArgType___closed__2 = _init_l_Lean_Parser_Command_macroArgType___closed__2();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType___closed__2);
l_Lean_Parser_Command_macroArgType___closed__3 = _init_l_Lean_Parser_Command_macroArgType___closed__3();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType___closed__3);
l_Lean_Parser_Command_macroArgType___closed__4 = _init_l_Lean_Parser_Command_macroArgType___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType___closed__4);
l_Lean_Parser_Command_macroArgType___closed__5 = _init_l_Lean_Parser_Command_macroArgType___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType___closed__5);
l_Lean_Parser_Command_macroArgType = _init_l_Lean_Parser_Command_macroArgType();
lean_mark_persistent(l_Lean_Parser_Command_macroArgType);
l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1 = _init_l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1);
l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2 = _init_l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2();

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

@ -13,6 +13,7 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Array_getSepElems___rarg___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_pushLeading;
lean_object* l_Lean_MacroM_monadQuotation;
lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
@ -27,10 +28,15 @@ 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*);
lean_object* l_Lean_ParserDescr_char(uint8_t);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
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* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1(lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind___closed__2;
lean_object* l_Lean_Syntax_getKind___closed__1;
lean_object* l_Lean_Name_hashable;
@ -38,14 +44,18 @@ 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*);
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_optional___rarg___closed__1;
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_num___boxed(lean_object*);
lean_object* l_Array_getSepElems(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*);
lean_object* l_Array_getSepElems___rarg(lean_object*);
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_ParserDescr_parser(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
@ -90,6 +100,7 @@ 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*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* _init_l_Lean_Name_inhabited() {
_start:
{
@ -829,6 +840,77 @@ x_1 = l_Lean_MacroM_monadQuotation___closed__2;
return x_1;
}
}
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_array_get_size(x_2);
x_6 = lean_nat_dec_lt(x_3, x_5);
lean_dec(x_5);
if (x_6 == 0)
{
lean_dec(x_3);
return x_4;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_array_fget(x_2, x_3);
x_8 = lean_array_push(x_4, x_7);
x_9 = lean_nat_add(x_3, x_1);
lean_dec(x_3);
x_3 = x_9;
x_4 = x_8;
goto _start;
}
}
}
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Array_getSepElems___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = lean_unsigned_to_nat(2u);
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Array_empty___closed__1;
x_5 = l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(x_2, x_1, x_3, x_4);
return x_5;
}
}
lean_object* l_Array_getSepElems(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_getSepElems___rarg___boxed), 1, 0);
return x_2;
}
}
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
lean_object* l_Array_getSepElems___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Array_getSepElems___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
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*);