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-12-06 19:08:18 -08:00
parent 6af3eac142
commit a08dcef4f6
18 changed files with 10607 additions and 1730 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/Init/System/ST.lean generated
View file

@ -22,12 +22,14 @@ class STWorld (σ : outParam Type) (m : Type → Type)
instance {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
@[inline] def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α :=
@[noinline nospecialize]
def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α :=
match x Unit () with
| EStateM.Result.ok a _ => Except.ok a
| EStateM.Result.error ex _ => Except.error ex
@[inline] def runST {α : Type} (x : forall (σ : Type), ST σ α) : α :=
@[noinline nospecialize]
def runST {α : Type} (x : forall (σ : Type), ST σ α) : α :=
match x Unit () with
| EStateM.Result.ok a _ => a
| EStateM.Result.error ex _ => nomatch ex

12
stage0/src/Lean/Elab/Command.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ResolveName
import Lean.Meta.Reduce
import Lean.Elab.Log
import Lean.Elab.Term
import Lean.Elab.Binders
@ -543,6 +544,17 @@ open Meta
let type ← inferType e
logInfo m!"{e} : {type}"
@[builtinCommandElab Lean.Parser.Command.reduce] def elabReduce : CommandElab := fun stx => do
let term := stx[1]
withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
let e ← Term.elabTerm term none
Term.synthesizeSyntheticMVarsNoPostponing
let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
-- TODO: add options or notation for setting the following parameters
withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false)
logInfo e
def hasNoErrorMessages : CommandElabM Bool := do
return !(← get).messages.hasErrors

2
stage0/src/Lean/Meta/AbstractNestedProofs.lean generated
View file

@ -47,7 +47,7 @@ partial def visit (e : Expr) : M Expr := do
| none => pure localDecl
lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
withLCtx lctx localInstances k
checkCache e fun e => do
checkCache e fun _ => do
if (← isNonTrivialProof e) then
mkAuxLemma e
else match e with

4
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -301,7 +301,7 @@ where
The context `Nat` is the position of `xs[0]` in the local context. -/
collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT NameHashSet MetaM) Unit := do
let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT NameHashSet MetaM)) Unit :=
checkCache e fun e => do
checkCache e fun _ => do
match e with
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
@ -559,7 +559,7 @@ instance : MonadCache Expr Expr CheckAssignmentM := {
}
@[inline] private def visit (f : Expr → CheckAssignmentM Expr) (e : Expr) : CheckAssignmentM Expr :=
if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f
if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e (fun _ => f e)
private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do
let ctx ← read

2
stage0/src/Lean/Meta/ForEachExpr.lean generated
View file

@ -35,7 +35,7 @@ private partial def visitBinder (fn : Expr → MetaM Bool) : Array Expr → Nat
| fvars, j, e => visit fn $ e.instantiateRevRange j fvars.size fvars
partial def visit (fn : Expr → MetaM Bool) (e : Expr) : M Unit :=
checkCache e fun e => do
checkCache e fun _ => do
if (← liftM (fn e)) then
match e with
| Expr.forallE _ _ _ _ => visitBinder fn #[] 0 e

68
stage0/src/Lean/Meta/InferType.lean generated
View file

@ -6,7 +6,65 @@ Authors: Leonardo de Moura
import Lean.Data.LBool
import Lean.Meta.Basic
namespace Lean.Meta
namespace Lean
/-
Auxiliary function for instantiating the loose bound variables in `e` with `args[start:stop]`.
This function is similar to `instantiateRevRange`, but it applies beta-reduction when
we instantiate a bound variable with a lambda expression.
Example: Given the term `#0 a`, and `start := 0, stop := 1, args := #[fun x => x]` the result is
`a` instead of `(fun x => x) a`.
This reduction is useful when we are inferring the type of eliminator-like applications.
For example, given `(n m : Nat) (f : Nat → Nat) (h : m = n)`,
the type of `Eq.subst (motive := fun x => f m = f x) h rfl`
is `motive n` which is `(fun (x : Nat) => f m = f x) n`
This function reduces the new application to `f m = f n`
We use it to implement `inferAppType`
-/
partial def Expr.instantiateBetaRevRange (e : Expr) (start : Nat) (stop : Nat) (args : Array Expr) : Expr :=
if e.hasLooseBVars && stop > start then
assert! stop ≤ args.size
visit e 0 |>.run
else
e
where
visit (e : Expr) (offset : Nat) : MonadStateCacheT (Expr × Nat) Expr Id Expr :=
if offset >= e.looseBVarRange then
-- `e` doesn't have free variables
return e
else checkCache (e, offset) fun _ => do
match e with
| Expr.forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
| Expr.lam _ d b _ => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
| Expr.letE _ t v b _ => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
| Expr.mdata _ b _ => return e.updateMData! (← visit b offset)
| Expr.proj _ _ b _ => return e.updateProj! (← visit b offset)
| Expr.app f a _ =>
e.withAppRev fun f revArgs => do
let fNew ← visit f offset
let revArgs ← revArgs.mapM (visit · offset)
if f.isBVar then
-- try to beta reduce if `f` was a bound variable
return fNew.betaRev revArgs
else
return mkAppRev fNew revArgs
| Expr.bvar vidx _ =>
-- Recall that looseBVarRange for `Expr.bvar` is `vidx+1`.
-- So, we must have offset ≤ vidx, since we are in the "else" branch of `if offset >= e.looseBVarRange`
let n := stop - start
if vidx < offset + n then
return args[stop - (vidx - offset) - 1].liftLooseBVars 0 offset
else
return mkBVar (vidx - n)
-- The following cases are unreachable because they never contain loose bound variables
| Expr.const .. => unreachable!
| Expr.fvar .. => unreachable!
| Expr.mvar .. => unreachable!
| Expr.sort .. => unreachable!
| Expr.lit .. => unreachable!
namespace Meta
def throwFunctionExpected {α} (f : Expr) : MetaM α :=
throwError! "function expected{indentExpr f}"
@ -14,14 +72,16 @@ def throwFunctionExpected {α} (f : Expr) : MetaM α :=
private def inferAppType (f : Expr) (args : Array Expr) : MetaM Expr := do
let mut fType ← inferType f
let mut j := 0
/- TODO: check whether `instantiateBetaRevRange` is too expensive, and
use it only when `args` contains a lambda expression. -/
for i in [:args.size] do
match fType with
| Expr.forallE _ _ b _ => fType := b
| _ =>
match (← whnf $ fType.instantiateRevRange j i args) with
match (← whnf <| fType.instantiateBetaRevRange j i args) with
| Expr.forallE _ _ b _ => j := i; fType := b
| _ => throwFunctionExpected $ mkAppRange f 0 (i+1) args
pure $ fType.instantiateRevRange j args.size args
| _ => throwFunctionExpected <| mkAppRange f 0 (i+1) args
return fType.instantiateBetaRevRange j args.size args
def throwIncorrectNumberOfLevels {α} (constName : Name) (us : List Level) : MetaM α :=
throwError! "incorrect number of universe levels {mkConst constName us}"

2
stage0/src/Lean/Meta/PPGoal.lean generated
View file

@ -75,7 +75,7 @@ partial def visitVisibleExpr (e : Expr) : M Unit := do
where
visit (e : Expr) : MonadCacheT Expr Unit M Unit := do
if e.hasFVar then
checkCache e fun e => do
checkCache e fun _ => do
match e with
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b

4
stage0/src/Lean/Meta/Transform.lean generated
View file

@ -34,7 +34,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
let inst : STWorld IO.RealWorld m := ⟨⟩
let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
let rec visit (e : Expr) : MonadCacheT Expr Expr m Expr :=
checkCache e fun e => Core.withIncRecDepth do
checkCache e fun _ => Core.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT Expr Expr m Expr := do
match (← post e) with
| TransformStep.done e => pure e
@ -66,7 +66,7 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
let inst : STWorld IO.RealWorld m := ⟨⟩
let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
let rec visit (e : Expr) : MonadCacheT Expr Expr m Expr :=
checkCache e fun e => Meta.withIncRecDepth do
checkCache e fun _ => Meta.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT Expr Expr m Expr := do
match (← post e) with
| TransformStep.done e => pure e

6
stage0/src/Lean/MetavarContext.lean generated
View file

@ -520,7 +520,7 @@ partial def instantiateLevelMVars {m} [Monad m] [MonadMCtx m] : Level → m Leve
partial def instantiateExprMVars {m ω} [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLiftT (ST ω) m] (e : Expr) : MonadCacheT Expr Expr m Expr :=
if !e.hasMVar then
pure e
else checkCache e fun e => do match e with
else checkCache e fun _ => do match e with
| Expr.proj _ _ s _ => return e.updateProj! (← instantiateExprMVars s)
| Expr.forallE _ d b _ => return e.updateForallE! (← instantiateExprMVars d) (← instantiateExprMVars b)
| Expr.lam _ d b _ => return e.updateLambdaE! (← instantiateExprMVars d) (← instantiateExprMVars b)
@ -579,7 +579,7 @@ partial def instantiateExprMVars {m ω} [Monad m] [MonadMCtx m] [STWorld ω m] [
let result := mkAppRange result fvars.size args.size args
pure $ result
| _ => instApp
| e@(Expr.mvar mvarId _) => checkCache e fun e => do
| e@(Expr.mvar mvarId _) => checkCache e fun _ => do
let mctx ← getMCtx
match mctx.getExprAssignment? mvarId with
| some newE => do
@ -838,7 +838,7 @@ private def anyDependsOn (mctx : MetavarContext) (es : Array Expr) (fvarId : FVa
private partial def elimMVarDepsAux (xs : Array Expr) (e : Expr) : M Expr :=
let rec
visit (e : Expr) : M Expr :=
if !e.hasMVar then pure e else checkCache e elim,
if !e.hasMVar then pure e else checkCache e fun _ => elim e,
elim (e : Expr) : M Expr := do
match e with
| Expr.proj _ _ s _ => return e.updateProj! (← visit s)

2
stage0/src/Lean/Util/ForEachExpr.lean generated
View file

@ -16,7 +16,7 @@ addresses. Note that the following code is parametric in a monad `m`.
variables {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
namespace ForEachExpr
@[specialize] partial def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit :=
checkCache e fun e => do
checkCache e fun _ => do
if (← g e) then
match e with
| Expr.forallE _ d b _ => do visit g d; visit g b

29
stage0/src/Lean/Util/MonadCache.lean generated
View file

@ -13,11 +13,11 @@ class MonadCache (α β : Type) (m : Type → Type) where
/-- If entry `a := b` is already in the cache, then return `b`.
Otherwise, execute `b ← f a`, store `a := b` in the cache and return `b`. -/
@[inline] def checkCache {α β : Type} {m : Type → Type} [MonadCache α β m] [Monad m] (a : α) (f : α → m β) : m β := do
@[inline] def checkCache {α β : Type} {m : Type → Type} [MonadCache α β m] [Monad m] (a : α) (f : Unit → m β) : m β := do
match (← MonadCache.findCached? a) with
| some b => pure b
| none => do
let b ← f a
let b ← f ()
MonadCache.cache a b
pure b
@ -77,4 +77,29 @@ instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceA
instance [MonadRef m] : MonadRef (MonadCacheT α β m) := inferInstanceAs (MonadRef (StateRefT' _ _ _))
end MonadCacheT
/- Similar to `MonadCacheT`, but using `StateT` instead of `StateRefT` -/
def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := StateT (HashMap α β) m
namespace MonadStateCacheT
variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) := {
getCache := (get : StateT ..),
modifyCache := fun f => (modify f : StateT ..)
}
@[inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ :=
x.run' Std.mkHashMap
instance : Monad (MonadStateCacheT α β m) := inferInstanceAs (Monad (StateT _ _))
instance : MonadLift m (MonadStateCacheT α β m) := inferInstanceAs (MonadLift m (StateT _ _))
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadStateCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateT _ _))
instance : MonadControl m (MonadStateCacheT α β m) := inferInstanceAs (MonadControl m (StateT _ _))
instance [MonadFinally m] : MonadFinally (MonadStateCacheT α β m) := inferInstanceAs (MonadFinally (StateT _ _))
instance [MonadRef m] : MonadRef (MonadStateCacheT α β m) := inferInstanceAs (MonadRef (StateT _ _))
end MonadStateCacheT
end Lean

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Command
// Imports: Init Lean.ResolveName Lean.Elab.Log Lean.Elab.Term Lean.Elab.Binders Lean.Elab.SyntheticMVars Lean.Elab.DeclModifiers
// Imports: Init Lean.ResolveName Lean.Meta.Reduce Lean.Elab.Log Lean.Elab.Term Lean.Elab.Binders Lean.Elab.SyntheticMVars Lean.Elab.DeclModifiers
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -27,6 +27,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Command_0__Lean_E
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabCommand___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_getVarDecls___boxed(lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabCommand___spec__7(lean_object*);
lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Elab_Command_elabSection(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabInitQuot_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addNamespace(lean_object*, lean_object*, lean_object*, lean_object*);
@ -69,6 +70,7 @@ lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__10(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabCheck___lambda__2___closed__1;
lean_object* l_Lean_Elab_Command_elabReduce___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSetOption_match__3___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_MessageData_ofList___closed__3;
@ -168,6 +170,7 @@ lean_object* l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___at_Lean_Elab_Comman
lean_object* l_Lean_Elab_Command_elabInitQuot___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureNoUnassignedMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_Context_cmdPos___default;
lean_object* l_Lean_Elab_Command_elabReduce___lambda__2___closed__1;
lean_object* l_Lean_ofExcept___at_Lean_Elab_Command_elabEvalUnsafe___spec__3(lean_object*);
lean_object* l_Lean_Elab_Command_elabOpen___closed__2;
lean_object* l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__3;
@ -185,6 +188,8 @@ lean_object* l_Lean_Elab_Command_addLinter(lean_object*, lean_object*);
extern lean_object* l_Lean_Core_instMonadEnvCoreM___closed__1;
lean_object* l_Lean_Meta_mkLambdaFVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addScope___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabReduce___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabReduce___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__3;
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addScopes___closed__1;
lean_object* lean_array_push(lean_object*, lean_object*);
@ -256,6 +261,7 @@ lean_object* l_List_head_x21___at_Lean_Elab_Command_instMonadOptionsCommandElabM
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadEnvCommandElabM___closed__4;
lean_object* l_Lean_Elab_Command_elabReduce___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabCheckFailure(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedException___closed__1;
lean_object* l_Lean_Elab_Command_elabCheck___closed__3;
@ -458,6 +464,7 @@ lean_object* l_Lean_Elab_Command_elabOpenOnly(lean_object*, lean_object*, lean_o
lean_object* l_Lean_Name_getNumParts(lean_object*);
lean_object* l_Lean_Elab_Command_hasNoErrorMessages(lean_object*);
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_Command_elabCommand___spec__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Command_elabEnd___closed__1;
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_liftAttrM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabUniverses___closed__1;
@ -492,6 +499,7 @@ lean_object* l_Lean_Elab_Command_instMonadRecDepthCommandElabM___lambda__1(lean_
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd___closed__2;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runLinters___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_WHNF___hyg_15____closed__2;
lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___closed__2;
@ -528,6 +536,7 @@ lean_object* l_Lean_Elab_Command_failIfSucceeds___lambda__1(uint8_t, lean_object
lean_object* l_Lean_InternalExceptionId_getName(lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclIdCore(lean_object*);
lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Command_expandDeclId___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabCommand___spec__7___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabInitQuot___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabOpenHiding(lean_object*, lean_object*, lean_object*, lean_object*);
@ -565,6 +574,7 @@ extern lean_object* l_Lean_Syntax_mkApp___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabCheck___closed__1;
lean_object* l_Lean_Elab_Command_elabEvalUnsafe_match__4(lean_object*);
lean_object* l_Lean_Elab_Command_elabReduce_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_checkEndHeader_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabCheckFailure___closed__3;
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
@ -587,6 +597,7 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabComma
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabExport___closed__1;
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_instAddErrorMessageContextCommandElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce(lean_object*);
lean_object* l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__1;
lean_object* l_Lean_Elab_Command_getScope(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_getSepArgs___spec__1(lean_object*, size_t, size_t, lean_object*);
@ -603,6 +614,7 @@ lean_object* l_Lean_Elab_Command_expandInCmd(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__8;
lean_object* l_Lean_Elab_Command_elabVariable___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_pushScope___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addScope___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabReduce(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_addUnivLevel___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabCheck(lean_object*);
@ -661,6 +673,7 @@ lean_object* l_Lean_Syntax_getPos(lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__1;
lean_object* l_Lean_Meta_reduce_visit(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandDeclId___at_Lean_Elab_Command_expandDeclId___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__2;
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
@ -799,6 +812,7 @@ lean_object* l_Lean_Elab_Command_elabOpenOnly___boxed(lean_object*, lean_object*
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabInitQuot_match__1(lean_object*);
lean_object* l_Lean_Elab_Command_elabSynth___closed__3;
lean_object* l_Lean_Elab_Command_elabReduce_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd_match__2(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Command_mkMessageAux(lean_object*, lean_object*, lean_object*, uint8_t);
@ -822,6 +836,7 @@ extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__2___clo
lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Command_expandDeclId___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__7;
lean_object* l_Std_PersistentArray_foldlM___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Command_elabSynth___closed__2;
extern lean_object* l_instReprChar___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_893____closed__1;
@ -13032,7 +13047,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Command_modifyScope___closed__1;
x_2 = l_Lean_Elab_Command_modifyScope___closed__2;
x_3 = lean_unsigned_to_nat(389u);
x_3 = lean_unsigned_to_nat(390u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -18268,6 +18283,642 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Command_elabReduce_match__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
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_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Lean_Elab_Command_elabReduce_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabReduce_match__1___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_Command_elabReduce___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, lean_object* x_7, lean_object* x_8) {
_start:
{
uint8_t x_9; lean_object* x_10; lean_object* x_11;
x_9 = 0;
x_10 = lean_box(0);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_11 = l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(x_9, x_10, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_13 = l_Lean_Meta_instantiateMVarsImp(x_1, x_4, x_5, x_6, x_7, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_unsigned_to_nat(1u);
x_17 = l_Lean_Elab_Term_levelMVarToParam(x_14, x_16, x_2, x_3, x_4, x_5, x_6, x_7, x_15);
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 = lean_ctor_get(x_18, 0);
lean_inc(x_20);
lean_dec(x_18);
x_21 = !lean_is_exclusive(x_6);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_22 = lean_ctor_get(x_6, 0);
x_23 = l_Lean_Meta_initFn____x40_Lean_Meta_WHNF___hyg_15____closed__2;
x_24 = l_Lean_KVMap_setBool(x_22, x_23, x_9);
lean_ctor_set(x_6, 0, x_24);
x_25 = lean_ctor_get(x_4, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_4, 1);
lean_inc(x_26);
x_27 = lean_ctor_get(x_4, 2);
lean_inc(x_27);
x_28 = !lean_is_exclusive(x_25);
if (x_28 == 0)
{
uint8_t x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32;
x_29 = 0;
lean_ctor_set_uint8(x_25, 5, x_29);
x_30 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_30, 0, x_25);
lean_ctor_set(x_30, 1, x_26);
lean_ctor_set(x_30, 2, x_27);
x_31 = 1;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_32 = l_Lean_Meta_reduce_visit(x_31, x_9, x_9, x_20, x_30, x_5, x_6, x_7, x_19);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36; lean_object* x_37;
x_33 = lean_ctor_get(x_32, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_inc(x_34);
lean_dec(x_32);
x_35 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_35, 0, x_33);
x_36 = 0;
x_37 = l_Lean_Elab_log___at_Lean_Elab_Term_traceAtCmdPos___spec__2(x_35, x_36, x_2, x_3, x_4, x_5, x_6, x_7, x_34);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_37;
}
else
{
uint8_t x_38;
lean_dec(x_6);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_38 = !lean_is_exclusive(x_32);
if (x_38 == 0)
{
return x_32;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_32, 0);
x_40 = lean_ctor_get(x_32, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_32);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
else
{
uint8_t x_42; uint8_t x_43; uint8_t x_44; uint8_t x_45; uint8_t x_46; uint8_t x_47; uint8_t x_48; uint8_t x_49; uint8_t x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54;
x_42 = lean_ctor_get_uint8(x_25, 0);
x_43 = lean_ctor_get_uint8(x_25, 1);
x_44 = lean_ctor_get_uint8(x_25, 2);
x_45 = lean_ctor_get_uint8(x_25, 3);
x_46 = lean_ctor_get_uint8(x_25, 4);
x_47 = lean_ctor_get_uint8(x_25, 6);
x_48 = lean_ctor_get_uint8(x_25, 7);
x_49 = lean_ctor_get_uint8(x_25, 8);
lean_dec(x_25);
x_50 = 0;
x_51 = lean_alloc_ctor(0, 0, 9);
lean_ctor_set_uint8(x_51, 0, x_42);
lean_ctor_set_uint8(x_51, 1, x_43);
lean_ctor_set_uint8(x_51, 2, x_44);
lean_ctor_set_uint8(x_51, 3, x_45);
lean_ctor_set_uint8(x_51, 4, x_46);
lean_ctor_set_uint8(x_51, 5, x_50);
lean_ctor_set_uint8(x_51, 6, x_47);
lean_ctor_set_uint8(x_51, 7, x_48);
lean_ctor_set_uint8(x_51, 8, x_49);
x_52 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_26);
lean_ctor_set(x_52, 2, x_27);
x_53 = 1;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_54 = l_Lean_Meta_reduce_visit(x_53, x_9, x_9, x_20, x_52, x_5, x_6, x_7, x_19);
if (lean_obj_tag(x_54) == 0)
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; uint8_t x_58; lean_object* x_59;
x_55 = lean_ctor_get(x_54, 0);
lean_inc(x_55);
x_56 = lean_ctor_get(x_54, 1);
lean_inc(x_56);
lean_dec(x_54);
x_57 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_57, 0, x_55);
x_58 = 0;
x_59 = l_Lean_Elab_log___at_Lean_Elab_Term_traceAtCmdPos___spec__2(x_57, x_58, x_2, x_3, x_4, x_5, x_6, x_7, x_56);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_59;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
lean_dec(x_6);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_60 = lean_ctor_get(x_54, 0);
lean_inc(x_60);
x_61 = lean_ctor_get(x_54, 1);
lean_inc(x_61);
if (lean_is_exclusive(x_54)) {
lean_ctor_release(x_54, 0);
lean_ctor_release(x_54, 1);
x_62 = x_54;
} else {
lean_dec_ref(x_54);
x_62 = lean_box(0);
}
if (lean_is_scalar(x_62)) {
x_63 = lean_alloc_ctor(1, 2, 0);
} else {
x_63 = x_62;
}
lean_ctor_set(x_63, 0, x_60);
lean_ctor_set(x_63, 1, x_61);
return x_63;
}
}
}
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; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; uint8_t x_76; uint8_t x_77; uint8_t x_78; uint8_t x_79; uint8_t x_80; uint8_t x_81; uint8_t x_82; uint8_t x_83; lean_object* x_84; uint8_t x_85; lean_object* x_86; lean_object* x_87; uint8_t x_88; lean_object* x_89;
x_64 = lean_ctor_get(x_6, 0);
x_65 = lean_ctor_get(x_6, 1);
x_66 = lean_ctor_get(x_6, 2);
x_67 = lean_ctor_get(x_6, 3);
x_68 = lean_ctor_get(x_6, 4);
x_69 = lean_ctor_get(x_6, 5);
lean_inc(x_69);
lean_inc(x_68);
lean_inc(x_67);
lean_inc(x_66);
lean_inc(x_65);
lean_inc(x_64);
lean_dec(x_6);
x_70 = l_Lean_Meta_initFn____x40_Lean_Meta_WHNF___hyg_15____closed__2;
x_71 = l_Lean_KVMap_setBool(x_64, x_70, x_9);
x_72 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_72, 0, x_71);
lean_ctor_set(x_72, 1, x_65);
lean_ctor_set(x_72, 2, x_66);
lean_ctor_set(x_72, 3, x_67);
lean_ctor_set(x_72, 4, x_68);
lean_ctor_set(x_72, 5, x_69);
x_73 = lean_ctor_get(x_4, 0);
lean_inc(x_73);
x_74 = lean_ctor_get(x_4, 1);
lean_inc(x_74);
x_75 = lean_ctor_get(x_4, 2);
lean_inc(x_75);
x_76 = lean_ctor_get_uint8(x_73, 0);
x_77 = lean_ctor_get_uint8(x_73, 1);
x_78 = lean_ctor_get_uint8(x_73, 2);
x_79 = lean_ctor_get_uint8(x_73, 3);
x_80 = lean_ctor_get_uint8(x_73, 4);
x_81 = lean_ctor_get_uint8(x_73, 6);
x_82 = lean_ctor_get_uint8(x_73, 7);
x_83 = lean_ctor_get_uint8(x_73, 8);
if (lean_is_exclusive(x_73)) {
x_84 = x_73;
} else {
lean_dec_ref(x_73);
x_84 = lean_box(0);
}
x_85 = 0;
if (lean_is_scalar(x_84)) {
x_86 = lean_alloc_ctor(0, 0, 9);
} else {
x_86 = x_84;
}
lean_ctor_set_uint8(x_86, 0, x_76);
lean_ctor_set_uint8(x_86, 1, x_77);
lean_ctor_set_uint8(x_86, 2, x_78);
lean_ctor_set_uint8(x_86, 3, x_79);
lean_ctor_set_uint8(x_86, 4, x_80);
lean_ctor_set_uint8(x_86, 5, x_85);
lean_ctor_set_uint8(x_86, 6, x_81);
lean_ctor_set_uint8(x_86, 7, x_82);
lean_ctor_set_uint8(x_86, 8, x_83);
x_87 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_87, 0, x_86);
lean_ctor_set(x_87, 1, x_74);
lean_ctor_set(x_87, 2, x_75);
x_88 = 1;
lean_inc(x_7);
lean_inc(x_72);
lean_inc(x_5);
x_89 = l_Lean_Meta_reduce_visit(x_88, x_9, x_9, x_20, x_87, x_5, x_72, x_7, x_19);
if (lean_obj_tag(x_89) == 0)
{
lean_object* x_90; lean_object* x_91; lean_object* x_92; uint8_t x_93; lean_object* x_94;
x_90 = lean_ctor_get(x_89, 0);
lean_inc(x_90);
x_91 = lean_ctor_get(x_89, 1);
lean_inc(x_91);
lean_dec(x_89);
x_92 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_92, 0, x_90);
x_93 = 0;
x_94 = l_Lean_Elab_log___at_Lean_Elab_Term_traceAtCmdPos___spec__2(x_92, x_93, x_2, x_3, x_4, x_5, x_72, x_7, x_91);
lean_dec(x_7);
lean_dec(x_72);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_94;
}
else
{
lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98;
lean_dec(x_72);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_95 = lean_ctor_get(x_89, 0);
lean_inc(x_95);
x_96 = lean_ctor_get(x_89, 1);
lean_inc(x_96);
if (lean_is_exclusive(x_89)) {
lean_ctor_release(x_89, 0);
lean_ctor_release(x_89, 1);
x_97 = x_89;
} else {
lean_dec_ref(x_89);
x_97 = lean_box(0);
}
if (lean_is_scalar(x_97)) {
x_98 = lean_alloc_ctor(1, 2, 0);
} else {
x_98 = x_97;
}
lean_ctor_set(x_98, 0, x_95);
lean_ctor_set(x_98, 1, x_96);
return x_98;
}
}
}
else
{
uint8_t x_99;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_99 = !lean_is_exclusive(x_13);
if (x_99 == 0)
{
return x_13;
}
else
{
lean_object* x_100; lean_object* x_101; lean_object* x_102;
x_100 = lean_ctor_get(x_13, 0);
x_101 = lean_ctor_get(x_13, 1);
lean_inc(x_101);
lean_inc(x_100);
lean_dec(x_13);
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;
}
}
}
else
{
uint8_t x_103;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_103 = !lean_is_exclusive(x_11);
if (x_103 == 0)
{
return x_11;
}
else
{
lean_object* x_104; lean_object* x_105; lean_object* x_106;
x_104 = lean_ctor_get(x_11, 0);
x_105 = lean_ctor_get(x_11, 1);
lean_inc(x_105);
lean_inc(x_104);
lean_dec(x_11);
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;
}
}
}
}
static lean_object* _init_l_Lean_Elab_Command_elabReduce___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabReduce___lambda__1), 8, 0);
return x_1;
}
}
lean_object* l_Lean_Elab_Command_elabReduce___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = l_Lean_Elab_Term_resetMessageLog(x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
lean_inc(x_5);
lean_inc(x_3);
x_12 = l_Lean_Elab_Term_addAutoBoundImplicits(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21;
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_box(0);
x_15 = 1;
x_16 = lean_box(x_15);
x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabTerm___boxed), 10, 3);
lean_closure_set(x_17, 0, x_1);
lean_closure_set(x_17, 1, x_14);
lean_closure_set(x_17, 2, x_16);
x_18 = l_Lean_Elab_Command_elabReduce___lambda__2___closed__1;
x_19 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg), 9, 2);
lean_closure_set(x_19, 0, x_17);
lean_closure_set(x_19, 1, x_18);
x_20 = 0;
x_21 = l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(x_19, x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_13);
return x_21;
}
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
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;
}
}
}
}
lean_object* l_Lean_Elab_Command_elabReduce(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t 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;
x_5 = lean_unsigned_to_nat(1u);
x_6 = l_Lean_Syntax_getArg(x_1, x_5);
x_7 = lean_st_ref_get(x_3, x_4);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = lean_ctor_get(x_8, 0);
lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_st_ref_get(x_3, x_9);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l___private_Lean_Elab_Command_0__Lean_Elab_Command_getVarDecls(x_12);
lean_dec(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabReduce___lambda__2___boxed), 9, 1);
lean_closure_set(x_15, 0, x_6);
x_16 = 1;
x_17 = lean_box(x_16);
x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabBinders___rarg___boxed), 10, 3);
lean_closure_set(x_18, 0, x_14);
lean_closure_set(x_18, 1, x_15);
lean_closure_set(x_18, 2, x_17);
x_19 = lean_box(x_16);
x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg___boxed), 9, 2);
lean_closure_set(x_20, 0, x_18);
lean_closure_set(x_20, 1, x_19);
x_21 = l_Lean_Elab_Command_elabCheck___closed__3;
lean_inc(x_2);
x_22 = l_Lean_Elab_Command_liftTermElabM___rarg(x_21, x_20, x_2, x_3, x_13);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = l_Lean_setEnv___at_Lean_Elab_Command_elabInitQuot___spec__1(x_10, x_2, x_3, x_24);
lean_dec(x_2);
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_ctor_get(x_25, 0);
lean_dec(x_27);
lean_ctor_set(x_25, 0, x_23);
return x_25;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_ctor_get(x_25, 1);
lean_inc(x_28);
lean_dec(x_25);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_23);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_30 = lean_ctor_get(x_22, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_22, 1);
lean_inc(x_31);
lean_dec(x_22);
x_32 = l_Lean_setEnv___at_Lean_Elab_Command_elabInitQuot___spec__1(x_10, x_2, x_3, x_31);
lean_dec(x_2);
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
{
lean_object* x_34;
x_34 = lean_ctor_get(x_32, 0);
lean_dec(x_34);
lean_ctor_set_tag(x_32, 1);
lean_ctor_set(x_32, 0, x_30);
return x_32;
}
else
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_32, 1);
lean_inc(x_35);
lean_dec(x_32);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
}
}
lean_object* l_Lean_Elab_Command_elabReduce___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_Command_elabReduce___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_2);
return x_10;
}
}
lean_object* l_Lean_Elab_Command_elabReduce___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Command_elabReduce(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("reduce");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
x_2 = l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabReduce___boxed), 4, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Command_commandElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Command_hasNoErrorMessages___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -23962,6 +24613,7 @@ return x_6;
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_ResolveName(lean_object*);
lean_object* initialize_Lean_Meta_Reduce(lean_object*);
lean_object* initialize_Lean_Elab_Log(lean_object*);
lean_object* initialize_Lean_Elab_Term(lean_object*);
lean_object* initialize_Lean_Elab_Binders(lean_object*);
@ -23978,6 +24630,9 @@ lean_dec_ref(res);
res = initialize_Lean_ResolveName(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Reduce(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Log(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -24340,6 +24995,17 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabCheck___closed__2);
res = l___regBuiltin_Lean_Elab_Command_elabCheck(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_elabReduce___lambda__2___closed__1 = _init_l_Lean_Elab_Command_elabReduce___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_elabReduce___lambda__2___closed__1);
l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1);
l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2 = _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2);
l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3 = _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabReduce___closed__3);
res = l___regBuiltin_Lean_Elab_Command_elabReduce(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__1 = _init_l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__1);
l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__2 = _init_l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__2();

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

File diff suppressed because it is too large Load diff

74
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

@ -52,8 +52,8 @@ lean_object* l_Lean_Meta_isDelayedAssigned___at_Lean_Meta_CheckAssignment_check_
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isSynthetic_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldBothDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_collectLetDepsAux_match__1(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262_(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248_(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263_(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249_(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__4;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldBothDefEq_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -308,6 +308,7 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqProofIrrel_matc
lean_object* l_Lean_Meta_CheckAssignment_assignToConstFun___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* l_Lean_Meta_isExprDefEqAuxImpl___closed__1;
lean_object* l_Lean_Expr_headBeta(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1;
lean_object* l_Lean_Meta_isExprDefEqAuxImpl_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkMVar___closed__4;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignmentFOApprox_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -325,7 +326,6 @@ uint8_t l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_sameHeadSymbol(lean_object*
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_807____closed__1;
lean_object* l_Lean_Meta_CheckAssignment_assignToConstFun___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process___spec__2(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1;
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_assignConst___lambda__1___closed__1;
@ -343,7 +343,6 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqProofIrrel_matc
lean_object* l_Lean_Meta_throwIsDefEqStuck___rarg(lean_object*);
lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_unfoldDefinitionImp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadFunctorReaderT___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isListLevelDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Std_AssocList_contains___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_cache___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_run___closed__2;
@ -363,6 +362,7 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__
lean_object* l_Lean_Meta_mkFreshExprMVarAt___at___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarCore___spec__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_toCtorIfLit(lean_object*);
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visitMain___at_Lean_Meta_CheckAssignment_check___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1;
lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__32___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_foldlM___at_Lean_Meta_CheckAssignment_check___spec__49(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstance___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImp___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -405,7 +405,6 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDe
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visitMain___at_Lean_Meta_CheckAssignment_check___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Std_PersistentArray_anyM___at_Lean_Meta_CheckAssignment_check___spec__43(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___spec__60(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1;
lean_object* l_Std_PersistentArray_anyMAux___at_Lean_Meta_CheckAssignment_check___spec__30___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_addLetDeps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgs_processOtherArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -415,6 +414,7 @@ lean_object* l_Lean_Meta_CheckAssignment_instMonadCacheExprExprCheckAssignmentM_
lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__67___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignmentFOApproxAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignmentQuick_check_visit_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_TransparencyMode_beq(uint8_t, uint8_t);
@ -441,6 +441,7 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(le
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__11(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___spec__54___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1;
extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLeftRight(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_checkAssignment(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -460,7 +461,6 @@ lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Meta_isDefEqBindingDomain_loop_match__1(lean_object*);
lean_object* l_Std_HashSetImp_insert___at_Lean_NameHashSet_insert___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2;
lean_object* l_Lean_ConstantInfo_hints(lean_object*);
lean_object* l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_tryHeuristic___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_addLetDeps___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -490,6 +490,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___sp
size_t l_USize_land(size_t, size_t);
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visitMain___at_Lean_Meta_CheckAssignment_check___spec__21(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2;
lean_object* l_Lean_Meta_CheckAssignment_checkMVar___closed__1;
lean_object* l_Lean_registerInternalExceptionId(lean_object*, lean_object*);
lean_object* l_Lean_isProjectionFn___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -499,7 +500,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___sp
lean_object* l_Lean_Meta_isDefEqNat_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__10(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgs___spec__1___lambda__3(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_assignConst_match__1(lean_object*);
lean_object* l_Lean_Meta_mkLambdaFVars___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_findCached_x3f___spec__1___boxed(lean_object*, lean_object*);
@ -623,8 +623,8 @@ uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Std_PersistentArray_anyMAux___at_Lean_Meta_CheckAssignment_check___spec__44___boxed(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isAssigned_match__1(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8248_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8254_(lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_assignToConstFun_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_insert___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_cache___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instAddMessageContext___rarg(lean_object*, lean_object*, lean_object*);
@ -11814,7 +11814,7 @@ lean_dec(x_5);
return x_10;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1() {
_start:
{
lean_object* x_1;
@ -11822,26 +11822,26 @@ x_1 = lean_mk_string("checkAssignment");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248_(lean_object* x_1) {
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2;
x_3 = l_Lean_registerInternalExceptionId(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1() {
_start:
{
lean_object* x_1;
@ -11849,21 +11849,21 @@ x_1 = lean_mk_string("outOfScope");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262_(lean_object* x_1) {
lean_object* l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2;
x_2 = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2;
x_3 = l_Lean_registerInternalExceptionId(x_2, x_1);
return x_3;
}
@ -64956,7 +64956,7 @@ x_10 = l_Lean_Meta_isExprDefEqAuxImpl___lambda__1(x_1, x_2, x_9, x_4, x_5, x_6,
return x_10;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1() {
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1() {
_start:
{
lean_object* x_1;
@ -64964,12 +64964,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_isExprDefEqAuxImpl), 7, 0);
return x_1;
}
}
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239_(lean_object* x_1) {
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = l_Lean_Meta_isExprDefEqAuxRef;
x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1;
x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1;
x_4 = lean_st_ref_set(x_2, x_3, x_1);
x_5 = !lean_is_exclusive(x_4);
if (x_5 == 0)
@ -64991,7 +64991,7 @@ return x_8;
}
}
}
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8248_(lean_object* x_1) {
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8254_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -65232,20 +65232,20 @@ l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___closed__
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___closed__3);
l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___closed__4 = _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___closed__4();
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps___closed__4);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__1);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248____closed__2);
res = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2248_(lean_io_mk_world());
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__1);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249____closed__2);
res = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2249_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_CheckAssignment_checkAssignmentExceptionId = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkAssignmentExceptionId);
lean_dec_ref(res);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__1);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262____closed__2);
res = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2262_(lean_io_mk_world());
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__1);
l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2 = _init_l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263____closed__2);
res = l_Lean_Meta_CheckAssignment_initFn____x40_Lean_Meta_ExprDefEq___hyg_2263_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_CheckAssignment_outOfScopeExceptionId = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_CheckAssignment_outOfScopeExceptionId);
@ -65388,12 +65388,12 @@ l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1 = _init_l_Lean_Meta_isExp
lean_mark_persistent(l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1);
l_Lean_Meta_isExprDefEqAuxImpl___closed__1 = _init_l_Lean_Meta_isExprDefEqAuxImpl___closed__1();
lean_mark_persistent(l_Lean_Meta_isExprDefEqAuxImpl___closed__1);
l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239____closed__1);
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8239_(lean_io_mk_world());
l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1();
lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245____closed__1);
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8245_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8248_(lean_io_mk_world());
res = l_Lean_Meta_initFn____x40_Lean_Meta_ExprDefEq___hyg_8254_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

2277
stage0/stdlib/Lean/Meta/InferType.c generated
View file

File diff suppressed because it is too large Load diff

60
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

@ -87,6 +87,7 @@ lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isNatValueTransition_match__1(lean_object*);
lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__8___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_instantiateBetaRevRange_visit___closed__1;
lean_object* l_Lean_Meta_MatcherApp_addArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible___spec__1___closed__2;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
@ -428,7 +429,6 @@ extern lean_object* l_Lean_Expr_instInhabitedExpr;
lean_object* l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isVariableTransition___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_FindImpl_initCache;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12;
lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_HashSet_instInhabitedHashSet___closed__1;
lean_object* l_Std_HashSetImp_expand___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__2(lean_object*, lean_object*);
@ -564,7 +564,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop_
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___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*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue_match__2(lean_object*);
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
lean_object* l_instBEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor_match__1(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f_match__1(lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceStep___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -580,7 +579,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoA
lean_object* l_Lean_Meta_Match_Unify_unify(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_expandIfVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Position_lt___closed__1;
lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
@ -20367,16 +20365,6 @@ return x_12;
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Position_lt___closed__1;
x_2 = lean_alloc_closure((void*)(l_instBEq___rarg), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Std_HashSet_instInhabitedHashSet___closed__1;
@ -20386,7 +20374,7 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__3() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__2() {
_start:
{
lean_object* x_1;
@ -20394,16 +20382,16 @@ x_1 = lean_mk_string("matcher: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__4() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__3;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__2;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__5() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__4() {
_start:
{
lean_object* x_1;
@ -20411,16 +20399,16 @@ x_1 = lean_mk_string("matcher levels: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__6() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__5;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__4;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__6() {
_start:
{
lean_object* x_1;
@ -20428,16 +20416,16 @@ x_1 = lean_mk_string(", uElim: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__8() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__6;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__9() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__8() {
_start:
{
lean_object* x_1;
@ -20445,16 +20433,16 @@ x_1 = lean_mk_string("matcher value: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__9;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__8;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10() {
_start:
{
lean_object* x_1;
@ -20462,11 +20450,11 @@ x_1 = lean_mk_string("\ntype: ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12() {
static lean_object* _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11;
x_1 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
@ -20502,7 +20490,7 @@ x_28 = lean_st_ref_get(x_15, x_22);
x_29 = lean_ctor_get(x_28, 1);
lean_inc(x_29);
lean_dec(x_28);
x_30 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__2;
x_30 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__1;
x_31 = lean_st_mk_ref(x_30, x_29);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
@ -20675,7 +20663,7 @@ block_74:
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; lean_object* x_73;
x_66 = lean_unsigned_to_nat(0u);
x_67 = l_List_lengthAux___rarg(x_5, x_66);
x_68 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__1;
x_68 = l_Lean_Expr_instantiateBetaRevRange_visit___closed__1;
lean_inc(x_67);
x_69 = l_Nat_foldAux___at_Lean_Meta_Match_mkMatcher___spec__5(x_68, x_39, x_67, x_67, x_27);
lean_dec(x_67);
@ -20714,7 +20702,7 @@ lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean
lean_inc(x_62);
x_77 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_77, 0, x_62);
x_78 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__4;
x_78 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__3;
x_79 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_79, 0, x_78);
lean_ctor_set(x_79, 1, x_77);
@ -20938,11 +20926,11 @@ lean_dec(x_128);
x_130 = l_List_map___at_Lean_Meta_Match_mkMatcher___spec__9(x_129);
x_131 = l_Lean_MessageData_ofList(x_130);
lean_dec(x_130);
x_132 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__6;
x_132 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__5;
x_133 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_133, 0, x_132);
lean_ctor_set(x_133, 1, x_131);
x_134 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__8;
x_134 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7;
x_135 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_135, 0, x_133);
lean_ctor_set(x_135, 1, x_134);
@ -21013,11 +21001,11 @@ lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163;
lean_inc(x_55);
x_160 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_160, 0, x_55);
x_161 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10;
x_161 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__9;
x_162 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_162, 0, x_161);
lean_ctor_set(x_162, 1, x_160);
x_163 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12;
x_163 = l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11;
x_164 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_164, 0, x_162);
lean_ctor_set(x_164, 1, x_163);
@ -23872,8 +23860,6 @@ l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10 = _init_l_Lean_Meta_Match_m
lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10);
l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11 = _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11();
lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__1___closed__11);
l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12 = _init_l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12();
lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__1___closed__12);
l_Lean_Meta_Match_mkMatcher___lambda__2___closed__1 = _init_l_Lean_Meta_Match_mkMatcher___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Meta_Match_mkMatcher___lambda__2___closed__1);
l_Lean_Meta_Match_mkMatcher___lambda__2___closed__2 = _init_l_Lean_Meta_Match_mkMatcher___lambda__2___closed__2();

7153
stage0/stdlib/Lean/MetavarContext.c generated
View file

File diff suppressed because it is too large Load diff

353
stage0/stdlib/Lean/Util/MonadCache.c generated
View file

@ -13,45 +13,71 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_run___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadRefMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_checkCache___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadExceptOfMonadCacheT___rarg(lean_object*);
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_instMonadFunctorStateT___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadControlMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_run(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheReaderT(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheExceptT(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
lean_object* l_Lean_MonadCacheT_instMonadMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ST_Prim_mkRef___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT___rarg(lean_object*);
lean_object* l_Lean_checkCache(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheExceptT___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadMonadCacheT___rarg(lean_object*);
extern lean_object* l_ExceptT_lift___rarg___closed__1;
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadFinallyMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify___at_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheReaderT___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheReaderT___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateRefT_x27_instMonadExceptOfStateRefT_x27___rarg(lean_object*);
lean_object* l_StateT_monadControl___rarg(lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_cache___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modifyThe___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_checkCache_match__1(lean_object*, lean_object*);
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_findCached_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_checkCache___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___rarg(lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_get___rarg(lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadFunctorReaderT___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_checkCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_instMonadCache(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_run___rarg___closed__1;
lean_object* l_modify___at_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT___rarg(lean_object*, lean_object*);
lean_object* l_StateT_lift___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_instMonadExceptOfStateT___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instMonadControlReaderT___closed__2;
lean_object* l_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify___at_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_run___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___rarg(lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadRefMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateRefT_x27_run_x27___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_findCached_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_run___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheReaderT___rarg(lean_object*);
lean_object* l_StateRefT_x27_run___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_findCached_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -67,23 +93,32 @@ lean_object* l_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___rarg(l
lean_object* l_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_cache(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadHashMapCacheAdapter_instMonadCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___rarg(lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ST_Prim_Ref_modifyGetUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_checkCache_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_instMonadStateT___rarg(lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadLiftMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_tryFinally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_HashMap_instInhabitedHashMap___closed__1;
lean_object* l_Lean_MonadCacheT_instMonadLiftMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadFinallyMonadCacheT___rarg(lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_run(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify___at_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadRefMonadCacheT___rarg(lean_object*, lean_object*);
extern lean_object* l_tryFinally___rarg___closed__1;
lean_object* l_Lean_instMonadCacheExceptT___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadControlMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadCacheExceptT___rarg(lean_object*, lean_object*);
lean_object* l_Lean_MonadCacheT_instMonadFinallyMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instMonadRef___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_checkCache_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -136,36 +171,36 @@ _start:
{
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_inc(x_2);
x_7 = lean_apply_1(x_1, x_2);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_box(0);
x_8 = lean_apply_1(x_1, x_7);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_checkCache___rarg___lambda__1), 5, 4);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_5);
x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
x_9 = lean_alloc_closure((void*)(l_Lean_checkCache___rarg___lambda__1), 5, 4);
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_3);
lean_closure_set(x_9, 2, x_4);
lean_closure_set(x_9, 3, x_5);
x_10 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_10 = lean_ctor_get(x_6, 0);
lean_inc(x_10);
lean_dec(x_6);
x_11 = lean_ctor_get(x_4, 0);
x_11 = lean_ctor_get(x_6, 0);
lean_inc(x_11);
lean_dec(x_4);
x_12 = lean_ctor_get(x_11, 1);
lean_dec(x_6);
x_12 = lean_ctor_get(x_4, 0);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_apply_2(x_12, lean_box(0), x_10);
return x_13;
lean_dec(x_4);
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_apply_2(x_13, lean_box(0), x_11);
return x_14;
}
}
}
@ -182,8 +217,8 @@ x_7 = lean_apply_1(x_6, x_3);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_checkCache___rarg___lambda__2), 6, 5);
lean_closure_set(x_8, 0, x_4);
lean_closure_set(x_8, 1, x_3);
lean_closure_set(x_8, 2, x_1);
lean_closure_set(x_8, 1, x_1);
lean_closure_set(x_8, 2, x_3);
lean_closure_set(x_8, 3, x_2);
lean_closure_set(x_8, 4, x_5);
x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
@ -734,6 +769,280 @@ lean_dec(x_5);
return x_8;
}
}
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg(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;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_6 = lean_apply_1(x_2, x_3);
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_apply_2(x_5, lean_box(0), x_8);
return x_9;
}
}
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg), 3, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg(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_inc(x_3);
x_4 = lean_alloc_closure((void*)(l_StateT_get___rarg), 2, 1);
lean_closure_set(x_4, 0, x_3);
x_5 = lean_alloc_closure((void*)(l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg), 3, 1);
lean_closure_set(x_5, 0, x_3);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg___boxed), 3, 0);
return x_4;
}
}
lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___rarg(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_MonadStateCacheT_run___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
lean_dec(x_4);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
lean_dec(x_5);
x_7 = l_Std_HashMap_instInhabitedHashMap___closed__1;
x_8 = lean_apply_1(x_3, x_7);
x_9 = l_tryFinally___rarg___closed__1;
x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_9, x_8);
return x_10;
}
}
lean_object* l_Lean_MonadStateCacheT_run(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_run___rarg), 3, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_run___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_run(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_StateT_instMonadStateT___rarg(x_1);
return x_2;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___rarg), 1, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_StateT_lift___rarg), 4, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT___rarg), 1, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadLiftMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_StateT_instMonadExceptOfStateT___rarg(x_1, lean_box(0), x_3);
return x_4;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT___rarg), 3, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadExceptOfMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_StateT_monadControl___rarg(x_1);
return x_2;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___rarg), 1, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_StateT_tryFinally___rarg), 7, 2);
lean_closure_set(x_3, 0, x_2);
lean_closure_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___rarg), 2, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_inc(x_1);
x_3 = lean_alloc_closure((void*)(l_StateT_instMonadFunctorStateT___boxed), 4, 3);
lean_closure_set(x_3, 0, lean_box(0));
lean_closure_set(x_3, 1, lean_box(0));
lean_closure_set(x_3, 2, x_1);
x_4 = lean_alloc_closure((void*)(l_StateT_lift___rarg), 4, 1);
lean_closure_set(x_4, 0, x_1);
x_5 = l_Lean_instMonadRef___rarg(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT___rarg), 2, 0);
return x_6;
}
}
lean_object* l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_MonadStateCacheT_instMonadRefMonadStateCacheT(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Std_Data_HashMap(lean_object*);
static bool _G_initialized = false;