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-10-19 15:44:53 -07:00
parent 69dfb23805
commit 9f6821d685
7 changed files with 2945 additions and 2450 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
stage0/src/Lean/Compiler/InitAttr.lean generated
View file

@ -57,18 +57,26 @@ getInitFnNameForCore? env builtinInitAttr fn
def getRegularInitFnNameFor? (env : Environment) (fn : Name) : Option Name :=
getInitFnNameForCore? env regularInitAttr fn
-- Only used
def isIOUnitInitFn (env : Environment) (fn : Name) : Bool :=
let aux (attr : ParametricAttribute Name) : Bool :=
match attr.getParam env fn with
| some Name.anonymous => true
| _ => false
aux builtinInitAttr || aux regularInitAttr
@[export lean_get_init_fn_name_for]
def getInitFnNameFor? (env : Environment) (fn : Name) : Option Name :=
getBuiltinInitFnNameFor? env fn <|> getRegularInitFnNameFor? env fn
def isIOUnitInitFnCore (env : Environment) (attr : ParametricAttribute Name) (fn : Name) : Bool :=
match attr.getParam env fn with
| some Name.anonymous => true
| _ => false
@[export lean_is_io_unit_regular_init_fn]
def isIOUnitRegularInitFn (env : Environment) (fn : Name) : Bool :=
isIOUnitInitFnCore env regularInitAttr fn
@[export lean_is_io_unit_builtin_init_fn]
def isIOUnitBuiltinInitFn (env : Environment) (fn : Name) : Bool :=
isIOUnitInitFnCore env builtinInitAttr fn
def isIOUnitInitFn (env : Environment) (fn : Name) : Bool :=
isIOUnitBuiltinInitFn env fn || isIOUnitRegularInitFn env fn
def hasInitAttr (env : Environment) (fn : Name) : Bool :=
(getInitFnNameFor? env fn).isSome

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

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -5,13 +6,15 @@ Authors: Leonardo de Moura
-/
import Lean.Meta.Closure
namespace Lean
namespace Meta
namespace Lean.Meta
namespace AbstractNestedProofs
def isNonTrivialProof (e : Expr) : MetaM Bool :=
condM (not <$> isProof e) (pure false) $ e.withApp fun f args =>
pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic
def isNonTrivialProof (e : Expr) : MetaM Bool := do
if ! (← isProof e) then
pure false
else
e.withApp fun f args =>
pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic
structure Context :=
(baseName : Name)
@ -22,40 +25,40 @@ structure State :=
abbrev M := ReaderT Context $ MonadCacheT Expr Expr $ StateRefT State $ MetaM
private def mkAuxLemma (e : Expr) : M Expr := do
ctx ← read;
s ← get;
lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx;
modify fun s => { s with nextIdx := s.nextIdx + 1 };
let ctx ← read
let s ← get
let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx
modify fun s => { s with nextIdx := s.nextIdx + 1 }
mkAuxDefinitionFor lemmaName e
partial def visit : Expr → M Expr
| e =>
if e.isAtomic then pure e
else do
let visitBinders (xs : Array Expr) (k : M Expr) : M Expr := do {
localInstances ← getLocalInstances;
lctx ← getLCtx;
lctx ← xs.foldlM
(fun (lctx : LocalContext) x => do
let xFVarId := x.fvarId!;
localDecl ← getLocalDecl xFVarId;
type ← visit localDecl.type;
let localDecl := localDecl.setType type;
localDecl ← match localDecl.value? with
| some value => do value ← visit value; pure $ localDecl.setValue value
| none => pure localDecl;
pure $ lctx.modifyLocalDecl xFVarId fun _ => localDecl)
lctx;
withLCtx lctx localInstances k
};
checkCache e fun e => condM (liftM $ isNonTrivialProof e) (mkAuxLemma e) $ match e with
| Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do b ← visit b; mkLambdaFVars xs b
| Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do b ← visit b; mkLambdaFVars xs b
| Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do b ← visit b; mkForallFVars xs b
| Expr.mdata _ b _ => do b ← visit b; pure $ e.updateMData! b
| Expr.proj _ _ b _ => do b ← visit b; pure $ e.updateProj! b
| Expr.app _ _ _ => e.withApp fun f args => do args ← args.mapM visit; pure $ mkAppN f args
| _ => pure e
partial def visit (e : Expr) : M Expr := do
if e.isAtomic then
pure e
else
let visitBinders (xs : Array Expr) (k : M Expr) : M Expr := do
let localInstances ← getLocalInstances
let lctx ← getLCtx
for x in xs do
let xFVarId := x.fvarId!
let localDecl ← getLocalDecl xFVarId
let type ← visit localDecl.type
let localDecl := localDecl.setType type
let localDecl ← match localDecl.value? with
| some value => do let value ← visit value; pure $ localDecl.setValue value
| none => pure localDecl
lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
withLCtx lctx localInstances k
checkCache e fun e =>
if (← isNonTrivialProof e) then
mkAuxLemma e
else match e with
| Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b)
| Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b)
| Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b)
| Expr.mdata _ b _ => do pure $ e.updateMData! (← visit b)
| Expr.proj _ _ b _ => do pure $ e.updateProj! (← visit b)
| Expr.app _ _ _ => e.withApp fun f args => do pure $ mkAppN f (← args.mapM visit)
| _ => pure e
end AbstractNestedProofs
@ -63,5 +66,4 @@ end AbstractNestedProofs
def abstractNestedProofs (mainDeclName : Name) (e : Expr) : MetaM Expr :=
(((AbstractNestedProofs.visit e).run { baseName := mainDeclName }).run).run' { nextIdx := 1 }
end Meta
end Lean
end Lean.Meta

56
stage0/src/Lean/Meta/GeneralizeTelescope.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -5,8 +6,7 @@ Authors: Leonardo de Moura
-/
import Lean.Meta.KAbstract
namespace Lean
namespace Meta
namespace Lean.Meta
namespace GeneralizeTelescope
structure Entry :=
@ -14,40 +14,40 @@ structure Entry :=
(type : Expr)
(modified : Bool)
partial def updateTypes (e newE : Expr) : Array Entry → Nat → MetaM (Array Entry)
partial def updateTypes (e eNew : Expr) : Array Entry → Nat → MetaM (Array Entry)
| entries, i =>
if h : i < entries.size then
let entry := entries.get ⟨i, h⟩;
let entry := entries.get ⟨i, h⟩
match entry with
| ⟨_, type, _⟩ => do
typeAbst ← kabstract type e;
let typeAbst ← kabstract type e
if typeAbst.hasLooseBVars then do
let typeNew := typeAbst.instantiate1 newE;
let entries := entries.set ⟨i, h⟩ { entry with type := typeNew, modified := true };
updateTypes entries (i+1)
let typeNew := typeAbst.instantiate1 eNew
let entries := entries.set ⟨i, h⟩ { entry with type := typeNew, modified := true }
updateTypes e eNew entries (i+1)
else
updateTypes entries (i+1)
updateTypes e eNew entries (i+1)
else
pure entries
partial def generalizeTelescopeAux {α} (prefixForNewVars : Name) (k : Array Expr → MetaM α) : Array Entry → Nat → Nat → Array Expr → MetaM α
| entries, i, nextVarIdx, fvars =>
| entries, i, nextVarIdx, fvars => do
if h : i < entries.size then
let replace (e : Expr) (type : Expr) : MetaM α := do {
let userName := prefixForNewVars.appendIndexAfter nextVarIdx;
withLocalDeclD userName type $ fun x => do
entries ← updateTypes e x entries (i+1);
generalizeTelescopeAux entries (i+1) (nextVarIdx+1) (fvars.push x)
};
let replace (e : Expr) (type : Expr) : MetaM α := do
let userName := prefixForNewVars.appendIndexAfter nextVarIdx
withLocalDeclD userName type fun x => do
entries ← updateTypes e x entries (i+1)
generalizeTelescopeAux prefixForNewVars k entries (i+1) (nextVarIdx+1) (fvars.push x)
match entries.get ⟨i, h⟩ with
| ⟨e@(Expr.fvar fvarId _), type, false⟩ => do
localDecl ← getLocalDecl fvarId;
| ⟨e@(Expr.fvar fvarId _), type, false⟩ =>
let localDecl ← getLocalDecl fvarId
match localDecl with
| LocalDecl.cdecl _ _ _ _ _ => generalizeTelescopeAux entries (i+1) nextVarIdx (fvars.push e)
| LocalDecl.ldecl _ _ _ _ _ _ => replace e type
| ⟨e, type, modified⟩ => do
when modified $ unlessM (isTypeCorrect type) $
throwError $ "failed to create telescope generalizing " ++ (entries.map Entry.expr);
| LocalDecl.cdecl .. => generalizeTelescopeAux prefixForNewVars k entries (i+1) nextVarIdx (fvars.push e)
| LocalDecl.ldecl .. => replace e type
| ⟨e, type, modified⟩ =>
if modified then
unless (← isTypeCorrect type) do
throwError! "failed to create telescope generalizing {entries.map Entry.expr}"
replace e type
else
k fvars
@ -88,12 +88,10 @@ open GeneralizeTelescope
```
and the type for the new variable abstracting `h` is `xs = aux_2` which is not type correct. -/
def generalizeTelescope {α} (es : Array Expr) (prefixForNewVars : Name) (k : Array Expr → MetaM α) : MetaM α := do
es ← es.mapM $ fun e => do {
type ← inferType e;
type ← instantiateMVars type;
let es ← es.mapM fun e => do
let type ← inferType e
let type ← instantiateMVars type
pure { expr := e, type := type, modified := false : Entry }
};
generalizeTelescopeAux prefixForNewVars k es 0 1 #[]
end Meta
end Lean
end Lean.Meta

214
stage0/stdlib/Lean/Compiler/InitAttr.c generated
View file

@ -30,6 +30,7 @@ extern lean_object* l_Lean_registerInternalExceptionId___closed__2;
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__7;
lean_object* l_List_map___main___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
uint8_t lean_is_io_unit_regular_init_fn(lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -44,11 +45,11 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_registerInitAttr(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIOUnitInitFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__10;
extern lean_object* l_Lean_Name_inhabited;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttr___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIOUnitInitFnCore_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr_match__3(lean_object*);
lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttr___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_getIOTypeArg___boxed(lean_object*);
@ -66,6 +67,7 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_throwUnknownConstant___at_Lean_registerInitAttr___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l_Lean_isIOUnitInitFnCore(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qsortAux___main___at_Lean_registerInitAttr___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
@ -82,6 +84,7 @@ lean_object* l_Std_RBNode_fold___main___at_Lean_registerInitAttr___spec__8(lean_
lean_object* l_Lean_throwUnknownConstant___at_Lean_registerInitAttr___spec__6(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_378____closed__1;
lean_object* l_Lean_isIOUnitInitFnCore_match__1(lean_object*);
lean_object* l_Lean_registerParametricAttribute___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwUnknownConstant___at_Lean_registerInitAttr___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at_Lean_registerInitAttr___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -92,7 +95,7 @@ lean_object* l_Lean_registerInitAttr___lambda__2(lean_object*, lean_object*, lea
lean_object* l_Lean_getInitFnNameForCore_x3f___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalName___at_Lean_registerInitAttr___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_isIOUnitInitFn_match__1(lean_object*);
lean_object* l_Lean_isIOUnitBuiltinInitFn___boxed(lean_object*, lean_object*);
lean_object* l_Array_binSearchAux___main___at_Lean_getInitFnNameForCore_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_hasInitAttr___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__5;
@ -107,6 +110,7 @@ lean_object* l_Lean_throwError___at_Lean_registerInitAttr___spec__2(lean_object*
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_is_io_unit_builtin_init_fn(lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_getIOTypeArg_match__1(lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__13;
extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__4;
@ -129,8 +133,10 @@ uint8_t l___private_Lean_Compiler_InitAttr_0__Lean_isIOUnit(lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_registerInitAttr___spec__7___lambda__1___boxed(lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_Lean_AddMessageContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIOUnitInitFnCore___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__8;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_isIOUnitRegularInitFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__2;
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerInitAttr___lambda__1___closed__1;
@ -2954,7 +2960,30 @@ lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_isIOUnitInitFn_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* lean_get_init_fn_name_for(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_builtinInitAttr;
lean_inc(x_2);
x_4 = l_Lean_getInitFnNameForCore_x3f(x_1, x_3, x_2);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_regularInitAttr;
x_6 = l_Lean_getInitFnNameForCore_x3f(x_1, x_5, x_2);
lean_dec(x_1);
return x_6;
}
else
{
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
}
lean_object* l_Lean_isIOUnitInitFnCore_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -2989,82 +3018,116 @@ return x_8;
}
}
}
lean_object* l_Lean_isIOUnitInitFn_match__1(lean_object* x_1) {
lean_object* l_Lean_isIOUnitInitFnCore_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_isIOUnitInitFn_match__1___rarg), 3, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_isIOUnitInitFnCore_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_isIOUnitInitFnCore(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_2, x_1, x_3);
if (lean_obj_tag(x_4) == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
lean_dec(x_4);
if (lean_obj_tag(x_6) == 0)
{
uint8_t x_7;
x_7 = 1;
return x_7;
}
else
{
uint8_t x_8;
lean_dec(x_6);
x_8 = 0;
return x_8;
}
}
}
}
lean_object* l_Lean_isIOUnitInitFnCore___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = l_Lean_isIOUnitInitFnCore(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
x_5 = lean_box(x_4);
return x_5;
}
}
uint8_t lean_is_io_unit_regular_init_fn(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_Lean_regularInitAttr;
x_4 = l_Lean_isIOUnitInitFnCore(x_1, x_3, x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_isIOUnitRegularInitFn___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_is_io_unit_regular_init_fn(x_1, x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t lean_is_io_unit_builtin_init_fn(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_Lean_builtinInitAttr;
x_4 = l_Lean_isIOUnitInitFnCore(x_1, x_3, x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_isIOUnitBuiltinInitFn___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_is_io_unit_builtin_init_fn(x_1, x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Lean_isIOUnitInitFn(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_builtinInitAttr;
lean_object* x_3; uint8_t x_4;
x_3 = l_Lean_builtinInitAttr;
lean_inc(x_2);
x_12 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_11, x_1, x_2);
if (lean_obj_tag(x_12) == 0)
x_4 = l_Lean_isIOUnitInitFnCore(x_1, x_3, x_2);
if (x_4 == 0)
{
lean_object* x_13;
x_13 = lean_box(0);
x_3 = x_13;
goto block_10;
}
else
{
lean_object* x_14;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
lean_dec(x_12);
if (lean_obj_tag(x_14) == 0)
{
uint8_t x_15;
lean_dec(x_2);
x_15 = 1;
return x_15;
}
else
{
lean_object* x_16;
lean_dec(x_14);
x_16 = lean_box(0);
x_3 = x_16;
goto block_10;
}
}
block_10:
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = l_Lean_regularInitAttr;
x_5 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_4, x_1, x_2);
if (lean_obj_tag(x_5) == 0)
{
uint8_t x_6;
x_6 = 0;
lean_object* x_5; uint8_t x_6;
x_5 = l_Lean_regularInitAttr;
x_6 = l_Lean_isIOUnitInitFnCore(x_1, x_5, x_2);
return x_6;
}
else
{
lean_object* x_7;
x_7 = lean_ctor_get(x_5, 0);
lean_inc(x_7);
lean_dec(x_5);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
x_8 = 1;
return x_8;
}
else
{
uint8_t x_9;
lean_dec(x_7);
x_9 = 0;
return x_9;
}
}
uint8_t x_7;
lean_dec(x_2);
x_7 = 1;
return x_7;
}
}
}
@ -3078,29 +3141,6 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* lean_get_init_fn_name_for(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_builtinInitAttr;
lean_inc(x_2);
x_4 = l_Lean_getInitFnNameForCore_x3f(x_1, x_3, x_2);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_regularInitAttr;
x_6 = l_Lean_getInitFnNameForCore_x3f(x_1, x_5, x_2);
lean_dec(x_1);
return x_6;
}
else
{
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
}
uint8_t l_Lean_hasInitAttr(lean_object* x_1, lean_object* x_2) {
_start:
{

3909
stage0/stdlib/Lean/Meta/AbstractNestedProofs.c generated
View file

File diff suppressed because it is too large Load diff

927
stage0/stdlib/Lean/Meta/GeneralizeTelescope.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -82,7 +82,6 @@ lean_object* l___private_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_ob
lean_object* l_Lean_Meta_isExprDefEq___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__5___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Meta_isExprDefEqGuarded___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__1___boxed(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_throwInductiveTypeExpected(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3___closed__2;
extern lean_object* l_Lean_MessageData_ofList___closed__3;
@ -107,7 +106,6 @@ lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___closed__1;
lean_object* l_Lean_Meta_Match_Unify_unify___closed__3;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_HeadIndex_1__headNumArgsAux___main(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_3__checkTraceOptionM___at_Lean_Meta_Match_Unify_assign___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Meta_Match_Extension_mkExtension___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__3___boxed(lean_object*, lean_object*);
@ -131,6 +129,7 @@ extern lean_object* l_Lean_registerInternalExceptionId___closed__2;
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor_match__5(lean_object*);
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Meta_Match_mkMatcher___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__7;
@ -161,7 +160,6 @@ lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__3;
lean_object* l_Array_iterateMAux___main___at_Lean_Meta_Match_Extension_mkExtension___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNumPatterns(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4(lean_object*);
lean_object* l_Lean_Expr_constructorApp_x3f(lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_applyFVarSubst___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__3(lean_object*);
@ -263,7 +261,6 @@ uint8_t l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Ma
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux(lean_object*);
lean_object* l_Lean_Meta_Match_Unify_State_fvarSubst___default;
extern lean_object* l_Lean_levelZero;
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Example_toMessageData_match__1(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_Meta_Match_Extension_mkExtension___spec__4(lean_object*, lean_object*);
@ -290,7 +287,6 @@ uint8_t l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Ma
uint8_t l_List_elem___main___at_Lean_Occurrences_contains___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___closed__3;
lean_object* l_List_map___main___at_Lean_Meta_Match_Pattern_applyFVarSubst___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_7756_(lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__4(lean_object*, lean_object*, lean_object*);
@ -333,7 +329,6 @@ lean_object* l___private_Lean_Util_Trace_3__checkTraceOptionM___at_Lean_Meta_Mat
lean_object* l_List_map___main___at_Lean_Meta_Match_processInaccessibleAsCtor___spec__1(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_collectArraySizes_match__1(lean_object*);
extern lean_object* l_Lean_Meta_isExprDefEq___rarg___closed__2;
uint8_t l_Lean_Occurrences_beq(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isFirstPatternVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterMapMAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__8___closed__1;
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
@ -390,7 +385,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVa
extern lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__8;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit___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_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible___spec__1(lean_object*);
lean_object* l_Lean_Expr_toHeadIndex___main(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceStep___closed__3;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_3__checkTraceOptionM___at___private_Lean_Meta_WHNF_0__Lean_Meta_whnfCoreImp___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -453,7 +447,6 @@ lean_object* l_Lean_Meta_Match_Extension_State_map___default___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasRecursiveType_match__1(lean_object*);
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_replaceFVarId___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_replaceFVarId___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Pattern_toMessageData___closed__8;
uint8_t l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasCtorPattern___spec__1(uint8_t, lean_object*);
@ -471,7 +464,6 @@ lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta
extern lean_object* l_Lean_MessageData_nil___closed__1;
lean_object* l_Lean_Meta_Match_Extension_extension;
extern lean_object* l_List_map___main___at_Lean_Meta_DiscrTree_Trie_format___spec__2___rarg___closed__2;
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_assign(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Meta_Match_Extension_State_addEntry___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_occurs_match__1(lean_object*);
@ -500,6 +492,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPatte
lean_object* l_List_filterAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___lambda__2(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_expandVarIntoArrayLit_loop_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_29__withExistingLocalDeclsImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasCtorPattern_match__1(lean_object*);
@ -512,6 +505,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVari
extern lean_object* l_IO_Error_Inhabited___closed__1;
lean_object* l_Lean_Meta_Match_Example_toMessageData_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_toMessageData___closed__2;
lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Meta_generalizeTelescope___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_addMatcherInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_applyFVarSubst___spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Closure_1__mkAuxDefinitionImp___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -523,6 +517,7 @@ lean_object* l_Lean_Meta_Match_Example_toMessageData___closed__4;
extern lean_object* l_Lean_Literal_type___closed__2;
lean_object* l_Array_umapMAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__6___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isConstructorTransition___boxed(lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Pattern_toMessageData___spec__2(lean_object*);
@ -541,6 +536,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstru
lean_object* l_Lean_Meta_Match_Extension_extension___closed__4;
uint8_t l_Array_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Meta_Match_Alt_toMessageData___closed__1;
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3(lean_object*);
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
lean_object* l_Lean_Meta_Match_Unify_unify___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Meta_Match_Unify_unify___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -694,7 +690,6 @@ lean_object* l_Lean_Meta_Match_Extension_extension___elambda__1___boxed(lean_obj
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasCtorPattern___boxed(lean_object*);
lean_object* l_Lean_Meta_matchMatcherApp_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__1;
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEq___spec__3(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___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -750,15 +745,12 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceState(lea
lean_object* l_Lean_Meta_Match_Example_varsToUnderscore_match__1(lean_object*);
extern lean_object* l_Lean_ResolveName_resolveNamespaceUsingScope___closed__3;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Meta_Match_Alt_checkAndReplaceFVarId___spec__1(lean_object*);
lean_object* l_Lean_Meta_kabstract_visit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isNatValueTransition(lean_object*);
lean_object* l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern___spec__1___boxed(lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern___boxed(lean_object*);
lean_object* l_Lean_Meta_caseValues(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_List_foldl___main___at_Lean_Meta_Match_Pattern_toMessageData___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Example_replaceFVarId(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVariable___closed__1;
@ -790,7 +782,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3
lean_object* l_List_replace___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withMVarContext___at_Lean_Meta_revert___spec__5___rarg(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_isValueTransition___boxed(lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_substCore___spec__6___rarg(lean_object*, uint8_t, 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__3___closed__1;
lean_object* l_Lean_Meta_Match_withGoalOf___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___closed__1;
@ -818,7 +809,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_collectValues_
lean_object* l_Lean_Meta_Match_Unify_occurs___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceStep___closed__1;
lean_object* l_List_mapM___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_matchMatcherApp_x3f_match__1(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -873,6 +864,7 @@ lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor_match__1___rarg(lean_ob
lean_object* l_Lean_Meta_mkAuxDefinition___at_Lean_Meta_Match_mkMatcher___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_kabstract___at_Lean_Meta_GeneralizeTelescope_updateTypes___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__4(lean_object*, lean_object*);
extern lean_object* l_Nat_Inhabited;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -919,7 +911,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux___
lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__2___closed__2;
lean_object* l_Lean_throwError___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterMapMAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVariable___spec__1___closed__2;
lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Meta_abstractMVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Extension_extension___elambda__2___boxed(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern_match__1(lean_object*);
lean_object* l_Std_AssocList_foldlM___at_Lean_Meta_Match_Extension_State_addEntry___spec__10(lean_object*, lean_object*);
@ -953,6 +944,7 @@ lean_object* l_Lean_Meta_Match_Extension_extension___elambda__2(lean_object*);
lean_object* l_Lean_Meta_Match_Unify_isAltVar(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_hasArrayLitPattern_match__1(lean_object*);
lean_object* l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_inLocalDecls___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_find_x3f___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_expandIfVar___boxed(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_process___closed__2;
@ -983,6 +975,7 @@ lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__2___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwNonSupported___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Example_replaceFVarId_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
@ -6450,7 +6443,7 @@ lean_closure_set(x_48, 9, x_1);
lean_closure_set(x_48, 10, x_14);
lean_closure_set(x_48, 11, x_5);
x_49 = 0;
x_50 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_substCore___spec__6___rarg(x_44, x_49, x_38, x_48, x_6, x_7, x_8, x_9, x_46);
x_50 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(x_44, x_49, x_38, x_48, x_6, x_7, x_8, x_9, x_46);
return x_50;
}
else
@ -6493,7 +6486,7 @@ lean_closure_set(x_62, 9, x_1);
lean_closure_set(x_62, 10, x_14);
lean_closure_set(x_62, 11, x_5);
x_63 = 0;
x_64 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_substCore___spec__6___rarg(x_44, x_63, x_38, x_62, x_6, x_7, x_8, x_9, x_60);
x_64 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(x_44, x_63, x_38, x_62, x_6, x_7, x_8, x_9, x_60);
return x_64;
}
}
@ -14034,13 +14027,13 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f(lean
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_9 = l_Lean_Meta_instantiateMVars___at_Lean_Meta_abstractMVars___spec__1(x_2, x_4, x_5, x_6, x_7, x_8);
x_9 = l_Lean_Meta_instantiateMVars___at_Lean_Meta_generalizeTelescope___spec__1(x_2, x_4, x_5, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Meta_instantiateMVars___at_Lean_Meta_abstractMVars___spec__1(x_3, x_4, x_5, x_6, x_7, x_11);
x_12 = l_Lean_Meta_instantiateMVars___at_Lean_Meta_generalizeTelescope___spec__1(x_3, x_4, x_5, x_6, x_7, x_11);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
@ -21059,7 +21052,7 @@ lean_closure_set(x_18, 3, x_3);
lean_closure_set(x_18, 4, x_4);
lean_closure_set(x_18, 5, x_15);
x_19 = 0;
x_20 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_substCore___spec__6___rarg(x_17, x_19, x_3, x_18, x_7, x_8, x_9, x_10, x_11);
x_20 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(x_17, x_19, x_3, x_18, x_7, x_8, x_9, x_10, x_11);
return x_20;
}
else
@ -30172,7 +30165,7 @@ lean_closure_set(x_16, 5, x_5);
lean_closure_set(x_16, 6, x_14);
x_17 = l_Lean_Meta_Match_mkMatcher___lambda__3___closed__2;
x_18 = 0;
x_19 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_substCore___spec__6___rarg(x_17, x_18, x_14, x_16, x_7, x_8, x_9, x_10, x_15);
x_19 = l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(x_17, x_18, x_14, x_16, x_7, x_8, x_9, x_10, x_15);
return x_19;
}
else
@ -31517,120 +31510,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_MatcherApp_addArg_match__2___rarg),
return x_2;
}
}
lean_object* l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__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; uint8_t x_34;
x_34 = l_Lean_Expr_isFVar(x_2);
if (x_34 == 0)
{
uint8_t x_35;
x_35 = 0;
x_9 = x_35;
goto block_33;
}
else
{
lean_object* x_36; uint8_t x_37;
x_36 = lean_box(0);
x_37 = l_Lean_Occurrences_beq(x_3, x_36);
x_9 = x_37;
goto block_33;
}
block_33:
{
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = l_Lean_Expr_toHeadIndex___main(x_2);
x_11 = lean_unsigned_to_nat(0u);
x_12 = l___private_Lean_HeadIndex_1__headNumArgsAux___main(x_2, x_11);
x_13 = lean_unsigned_to_nat(1u);
x_14 = lean_st_mk_ref(x_13, x_8);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Lean_Meta_kabstract_visit(x_2, x_3, x_10, x_12, x_1, x_11, x_15, x_4, x_5, x_6, x_7, x_16);
lean_dec(x_12);
lean_dec(x_10);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_st_ref_get(x_15, x_19);
lean_dec(x_15);
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
{
lean_object* x_22;
x_22 = lean_ctor_get(x_20, 0);
lean_dec(x_22);
lean_ctor_set(x_20, 0, x_18);
return x_20;
}
else
{
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_20, 1);
lean_inc(x_23);
lean_dec(x_20);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_18);
lean_ctor_set(x_24, 1, x_23);
return x_24;
}
}
else
{
uint8_t x_25;
lean_dec(x_15);
x_25 = !lean_is_exclusive(x_17);
if (x_25 == 0)
{
return x_17;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_17, 0);
x_27 = lean_ctor_get(x_17, 1);
lean_inc(x_27);
lean_inc(x_26);
lean_dec(x_17);
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
return x_28;
}
}
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_29 = l_Lean_mkOptionalNode___closed__2;
x_30 = lean_array_push(x_29, x_2);
x_31 = lean_expr_abstract(x_1, x_30);
lean_dec(x_30);
lean_dec(x_1);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_8);
return x_32;
}
}
}
}
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__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) {
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__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, lean_object* x_9) {
_start:
{
lean_object* x_10; uint8_t x_11;
@ -31651,7 +31531,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_19 = l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__1(x_4, x_17, x_18, x_5, x_6, x_7, x_8, x_9);
x_19 = l_Lean_Meta_kabstract___at_Lean_Meta_GeneralizeTelescope_updateTypes___spec__1(x_4, x_17, x_18, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
@ -31712,7 +31592,7 @@ return x_28;
}
}
}
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3(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* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__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) {
_start:
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
@ -31745,7 +31625,7 @@ return x_18;
}
}
}
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4___rarg(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* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
uint8_t x_8; lean_object* x_9;
@ -31797,11 +31677,11 @@ return x_17;
}
}
}
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4(lean_object* x_1) {
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4___rarg), 7, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3___rarg), 7, 0);
return x_2;
}
}
@ -32243,7 +32123,7 @@ lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_16 = l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__2(x_2, x_3, x_15, x_12, x_6, x_7, x_8, x_9, x_13);
x_16 = l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__1(x_2, x_3, x_15, x_12, x_6, x_7, x_8, x_9, x_13);
if (lean_obj_tag(x_16) == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
@ -32252,7 +32132,7 @@ lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3(x_17, x_4, x_6, x_7, x_8, x_9, x_18);
x_19 = l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__2(x_17, x_4, x_6, x_7, x_8, x_9, x_18);
x_20 = lean_ctor_get(x_2, 2);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
@ -32487,34 +32367,25 @@ lean_inc(x_8);
x_9 = lean_alloc_closure((void*)(l_Lean_Meta_MatcherApp_addArg___lambda__4), 9, 2);
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_1);
x_10 = l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__4___rarg(x_8, x_9, x_3, x_4, x_5, x_6, x_7);
x_10 = l_Lean_Meta_lambdaTelescope___at_Lean_Meta_MatcherApp_addArg___spec__3___rarg(x_8, x_9, x_3, x_4, x_5, x_6, x_7);
return x_10;
}
}
lean_object* l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Meta_kabstract___at_Lean_Meta_MatcherApp_addArg___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_3);
return x_9;
}
}
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
lean_object* l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_10 = l_Nat_foldRevMAux___main___at_Lean_Meta_MatcherApp_addArg___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
}
}
lean_object* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3___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* l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_8 = l_Lean_Meta_mkArrow___at_Lean_Meta_MatcherApp_addArg___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);