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

feat: add Level.isEquiv

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-21 10:56:59 -07:00
parent c30e9ca551
commit 9baf91e641
8 changed files with 128 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/Init/Lean/Level.lean
View file

@ -83,10 +83,16 @@ def Level.instantiate (s : Name → Option Level) : Level → Level
@[extern "lean_level_hash"]
constant Level.hash (n : @& Level) : USize := default USize
@[extern "lean_level_eqv"]
constant Level.eqv (a : @& Level) (b : @& Level) : Bool := default _
@[extern "lean_level_eq"]
constant Level.beq (a : @& Level) (b : @& Level) : Bool := default _
instance : HasBeq Level := ⟨Level.eqv⟩
instance : HasBeq Level := ⟨Level.beq⟩
/- Return true if `a` and `b` denote the same level.
Check is currently incomplete.
TODO: implement in Lean. -/
@[extern "lean_level_eqv"]
constant Level.isEquiv (a : @& Level) (b : @& Level) : Bool := default _
/- Level to Format -/
namespace LevelToFormat

8
src/kernel/level.cpp
View file

@ -258,9 +258,11 @@ bool operator==(level const & l1, level const & l2) {
}
extern "C" uint8 lean_level_eqv(object * l1, object * l2) {
level const & l1_ref = reinterpret_cast<level const &>(l1);
level const & l2_ref = reinterpret_cast<level const &>(l2);
return l1_ref == l2_ref;
return is_equivalent(TO_REF(level, l1), TO_REF(level, l2));
}
extern "C" uint8 lean_level_eq(object * l1, object * l2) {
return TO_REF(level, l1) == TO_REF(level, l2);
}
bool is_not_zero(level const & l) {

2
src/stage0/CMakeLists.txt
View file

@ -1 +1 @@
add_library (stage0 OBJECT ./Init/Coe.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Combinators.c ./Init/Control/Conditional.c ./Init/Control/Default.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/MonadFail.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/Default.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/BinomialHeap/Basic.c ./Init/Data/BinomialHeap/Default.c ./Init/Data/ByteArray/Basic.c ./Init/Data/ByteArray/Default.c ./Init/Data/Char/Basic.c ./Init/Data/Char/Default.c ./Init/Data/DList.c ./Init/Data/Default.c ./Init/Data/Fin/Basic.c ./Init/Data/Fin/Default.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashMap/Default.c ./Init/Data/Hashable.c ./Init/Data/Int/Basic.c ./Init/Data/Int/Default.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Default.c ./Init/Data/Nat/Div.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Default.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentArray/Default.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashMap/Default.c ./Init/Data/Queue/Basic.c ./Init/Data/Queue/Default.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBMap/Default.c ./Init/Data/RBTree/Basic.c ./Init/Data/RBTree/Default.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack/Basic.c ./Init/Data/Stack/Default.c ./Init/Data/String/Basic.c ./Init/Data/String/Default.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Default.c ./Init/Fix.c ./Init/Lean/Attributes.c ./Init/Lean/Class.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/Default.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/Default.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Declaration.c ./Init/Lean/Default.c ./Init/Lean/Elaborator/Alias.c ./Init/Lean/Elaborator/Basic.c ./Init/Lean/Elaborator/Command.c ./Init/Lean/Elaborator/Default.c ./Init/Lean/Elaborator/ElabStrategyAttrs.c ./Init/Lean/Elaborator/PreTerm.c ./Init/Lean/Elaborator/ResolveName.c ./Init/Lean/Elaborator/Term.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler/Default.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Expr.c ./Init/Lean/Format.c ./Init/Lean/KVMap.c ./Init/Lean/Level.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/Name.c ./Init/Lean/NameGenerator.c ./Init/Lean/Options.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Default.c ./Init/Lean/Parser/Identifier.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/Parser/Trie.c ./Init/Lean/Path.c ./Init/Lean/Position.c ./Init/Lean/ProjFns.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/SMap.c ./Init/Lean/Scopes.c ./Init/Lean/Syntax.c ./Init/Lean/ToExpr.c ./Init/Lean/Trace.c ./Init/Lean/TypeClass/Basic.c ./Init/Lean/TypeClass/Context.c ./Init/Lean/TypeClass/Default.c ./Init/Lean/TypeClass/Synth.c ./Init/Lean/Util.c ./Init/System/Default.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c)
add_library (stage0 OBJECT ./Init/Coe.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Combinators.c ./Init/Control/Conditional.c ./Init/Control/Default.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/MonadFail.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/Default.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/BinomialHeap/Basic.c ./Init/Data/BinomialHeap/Default.c ./Init/Data/ByteArray/Basic.c ./Init/Data/ByteArray/Default.c ./Init/Data/Char/Basic.c ./Init/Data/Char/Default.c ./Init/Data/DList.c ./Init/Data/Default.c ./Init/Data/Fin/Basic.c ./Init/Data/Fin/Default.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashMap/Default.c ./Init/Data/Hashable.c ./Init/Data/Int/Basic.c ./Init/Data/Int/Default.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Default.c ./Init/Data/Nat/Div.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Default.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentArray/Default.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashMap/Default.c ./Init/Data/Queue/Basic.c ./Init/Data/Queue/Default.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBMap/Default.c ./Init/Data/RBTree/Basic.c ./Init/Data/RBTree/Default.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack/Basic.c ./Init/Data/Stack/Default.c ./Init/Data/String/Basic.c ./Init/Data/String/Default.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Default.c ./Init/Fix.c ./Init/Lean/Attributes.c ./Init/Lean/Class.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/Default.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/Default.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Declaration.c ./Init/Lean/Default.c ./Init/Lean/Elaborator/Alias.c ./Init/Lean/Elaborator/Basic.c ./Init/Lean/Elaborator/Command.c ./Init/Lean/Elaborator/Default.c ./Init/Lean/Elaborator/ElabStrategyAttrs.c ./Init/Lean/Elaborator/PreTerm.c ./Init/Lean/Elaborator/ResolveName.c ./Init/Lean/Elaborator/Term.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler/Default.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Expr.c ./Init/Lean/Format.c ./Init/Lean/KVMap.c ./Init/Lean/Level.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/Name.c ./Init/Lean/NameGenerator.c ./Init/Lean/Options.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Default.c ./Init/Lean/Parser/Identifier.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/Parser/Trie.c ./Init/Lean/Path.c ./Init/Lean/Position.c ./Init/Lean/ProjFns.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/SMap.c ./Init/Lean/Scopes.c ./Init/Lean/Syntax.c ./Init/Lean/ToExpr.c ./Init/Lean/Trace.c ./Init/Lean/TypeClass/Basic.c ./Init/Lean/TypeClass/Context.c ./Init/Lean/TypeClass/Default.c ./Init/Lean/TypeClass/Synth.c ./Init/Lean/TypeContext.c ./Init/Lean/Util.c ./Init/System/Default.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c)

56
src/stage0/Init/Lean/Expr.c
View file

@ -26,6 +26,7 @@ lean_object* l_Lean_MData_empty;
lean_object* l_Lean_Expr_constName(lean_object*);
lean_object* lean_expr_mk_sort(lean_object*);
lean_object* l_Lean_Expr_pi___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppRevArgs(lean_object*);
lean_object* l_Lean_Expr_isLambda___boxed(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isSort(lean_object*);
@ -69,11 +70,13 @@ lean_object* l_Lean_Expr_hasMVar___boxed(lean_object*);
lean_object* l_Lean_Expr_sort___boxed(lean_object*);
lean_object* l_Lean_Expr_HasToString___closed__1;
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* l_Array_mkEmpty(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_mkApp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_beq___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isLet(lean_object*);
lean_object* l_Lean_Expr_bvarIdx___boxed(lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Init_Lean_Expr_2__getAppRevArgsAux___main(lean_object*, lean_object*);
lean_object* lean_expr_mk_proj(lean_object*, lean_object*, lean_object*);
extern lean_object* l_panicWithPos___rarg___closed__3;
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
@ -107,6 +110,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Expr_app___boxed(lean_object*, lean_object*);
lean_object* l_Array_push(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__2;
extern lean_object* l_panicWithPos___rarg___closed__1;
lean_object* l_Lean_Expr_getAppArgs(lean_object*);
@ -116,6 +120,7 @@ uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Array_set_x21(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarName___boxed(lean_object*);
uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
lean_object* l___private_Init_Lean_Expr_2__getAppRevArgsAux(lean_object*, lean_object*);
lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
lean_object* l_Lean_mkCApp(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__5;
@ -1093,6 +1098,49 @@ x_8 = l___private_Init_Lean_Expr_1__getAppArgsAux___main(x_1, x_5, x_7);
return x_8;
}
}
lean_object* l___private_Init_Lean_Expr_2__getAppRevArgsAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 5)
{
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_array_push(x_2, x_4);
x_1 = x_3;
x_2 = x_5;
goto _start;
}
else
{
lean_dec(x_1);
return x_2;
}
}
}
lean_object* l___private_Init_Lean_Expr_2__getAppRevArgsAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Lean_Expr_2__getAppRevArgsAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_getAppRevArgs(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Expr_getAppNumArgsAux___main(x_1, x_2);
x_4 = lean_mk_empty_array_with_capacity(x_3);
lean_dec(x_3);
x_5 = l___private_Init_Lean_Expr_2__getAppRevArgsAux___main(x_1, x_4);
return x_5;
}
}
uint8_t l_Lean_Expr_isAppOf(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1270,7 +1318,7 @@ else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Expr_constName___closed__1;
x_4 = lean_unsigned_to_nat(183u);
x_4 = lean_unsigned_to_nat(190u);
x_5 = lean_unsigned_to_nat(15u);
x_6 = l_Lean_Expr_constName___closed__2;
x_7 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_3, x_4, x_5, x_6);
@ -1343,7 +1391,7 @@ else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Expr_constName___closed__1;
x_4 = lean_unsigned_to_nat(187u);
x_4 = lean_unsigned_to_nat(194u);
x_5 = lean_unsigned_to_nat(16u);
x_6 = l_Lean_Expr_constLevels___closed__1;
x_7 = l_panicWithPos___at_Lean_Expr_constLevels___spec__1(x_3, x_4, x_5, x_6);
@ -1392,7 +1440,7 @@ else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Expr_constName___closed__1;
x_4 = lean_unsigned_to_nat(191u);
x_4 = lean_unsigned_to_nat(198u);
x_5 = lean_unsigned_to_nat(7u);
x_6 = l_Lean_Expr_bvarIdx___closed__1;
x_7 = l_panicWithPos___at_Array_findIdx_x21___spec__1(x_3, x_4, x_5, x_6);
@ -1431,7 +1479,7 @@ else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_Lean_Expr_constName___closed__1;
x_4 = lean_unsigned_to_nat(195u);
x_4 = lean_unsigned_to_nat(202u);
x_5 = lean_unsigned_to_nat(7u);
x_6 = l_Lean_Expr_fvarName___closed__1;
x_7 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_3, x_4, x_5, x_6);

23
src/stage0/Init/Lean/Level.c
View file

@ -22,7 +22,6 @@ lean_object* l_Lean_Level_instantiate(lean_object*, lean_object*);
lean_object* l_Lean_LevelToFormat_Result_format___main___closed__4;
lean_object* l_Lean_LevelToFormat_parenIfFalse(lean_object*, uint8_t);
uint8_t l_Lean_Level_hasMVar(lean_object*);
lean_object* l_Lean_Level_eqv___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Level_hasMVar___boxed(lean_object*);
lean_object* l_Lean_LevelToFormat_Result_format___main___closed__3;
lean_object* l_Lean_LevelToFormat_Result_max(lean_object*, lean_object*);
@ -34,6 +33,7 @@ lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_HasBeq___closed__1;
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_LevelToFormat_Result_format___main(lean_object*, uint8_t);
lean_object* l_Lean_Level_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_LevelToFormat_Result_format___main___closed__5;
lean_object* l_Lean_Level_mvar___boxed(lean_object*);
lean_object* l_Lean_LevelToFormat_levelHasToString___closed__1;
@ -44,7 +44,6 @@ lean_object* l_Lean_Level_toNat___main(lean_object*);
lean_object* l___private_Init_Lean_Level_1__formatLst___main___at_Lean_LevelToFormat_Result_format___main___spec__2(lean_object*);
lean_object* l_Lean_Level_instantiate___main(lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
uint8_t lean_level_eqv(lean_object*, lean_object*);
lean_object* l_Lean_Level_one;
lean_object* l_Lean_Level_hasParam___boxed(lean_object*);
lean_object* l_Lean_LevelToFormat_Level_format(lean_object*);
@ -53,6 +52,7 @@ lean_object* l_Lean_HasBeq;
lean_object* l_Lean_LevelToFormat_levelHasFormat___closed__1;
lean_object* l_Lean_LevelToFormat_Result_succ(lean_object*);
extern lean_object* l_Lean_Format_paren___closed__1;
uint8_t lean_level_eqv(lean_object*, lean_object*);
lean_object* l_Lean_Level_toOffset(lean_object*);
lean_object* l_Lean_Level_ofNat___boxed(lean_object*);
lean_object* l_Lean_fmt___at_Lean_LevelToFormat_Level_toResult___main___spec__1(lean_object*);
@ -79,6 +79,7 @@ lean_object* l_Lean_Nat_imax___boxed(lean_object*, lean_object*);
lean_object* level_mk_param(lean_object*);
lean_object* l_Lean_Level_param___boxed(lean_object*);
lean_object* l_Lean_LevelToFormat_Level_toResult___main(lean_object*);
lean_object* l_Lean_Level_isEquiv___boxed(lean_object*, lean_object*);
lean_object* level_mk_succ(lean_object*);
extern lean_object* l_System_FilePath_dirName___closed__1;
extern lean_object* l_Lean_HasRepr___closed__1;
@ -90,6 +91,7 @@ lean_object* l_Lean_Level_addOffsetAux___main(lean_object*, lean_object*);
lean_object* l_Lean_Level_addOffset(lean_object*, lean_object*);
lean_object* l_Lean_Level_hasMVar___main___boxed(lean_object*);
lean_object* l_Lean_Level_succ___boxed(lean_object*);
uint8_t lean_level_eq(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Level_1__formatLst___main(lean_object*, lean_object*);
lean_object* l_Lean_LevelToFormat_levelHasFormat;
lean_object* l_Lean_LevelToFormat_Result_format(lean_object*, uint8_t);
@ -816,11 +818,11 @@ x_3 = lean_box_usize(x_2);
return x_3;
}
}
lean_object* l_Lean_Level_eqv___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Level_beq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_level_eqv(x_1, x_2);
x_3 = lean_level_eq(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
@ -831,7 +833,7 @@ lean_object* _init_l_Lean_HasBeq___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Level_eqv___boxed), 2, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Level_beq___boxed), 2, 0);
return x_1;
}
}
@ -843,6 +845,17 @@ x_1 = l_Lean_HasBeq___closed__1;
return x_1;
}
}
lean_object* l_Lean_Level_isEquiv___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_level_eqv(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_LevelToFormat_Result_succ(lean_object* x_1) {
_start:
{

10
src/stage0/Init/Lean/TypeClass/Context.c
View file

@ -95,7 +95,6 @@ extern lean_object* l_panicWithPos___rarg___closed__3;
uint8_t l_Lean_TypeClass_Context_eFind___main(lean_object*, lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eIsMeta___boxed(lean_object*);
uint8_t lean_level_eqv(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uIsMeta___boxed(lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uInstantiate___main___boxed(lean_object*, lean_object*);
@ -188,6 +187,7 @@ uint8_t lean_expr_has_mvar(lean_object*);
uint8_t l_Lean_TypeClass_Context_eOccursIn___lambda__1(lean_object*, lean_object*);
lean_object* l_panicWithPos___at_Lean_TypeClass_Context_eAssign___spec__1___closed__1;
size_t lean_usize_of_nat(lean_object*);
uint8_t lean_level_eq(lean_object*, lean_object*);
lean_object* lean_expr_mk_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eNewMeta(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uHasTmpMVar___boxed(lean_object*);
@ -1803,7 +1803,7 @@ uint8_t l_Lean_TypeClass_Context_uOccursIn___lambda__1(lean_object* x_1, lean_ob
_start:
{
uint8_t x_3;
x_3 = lean_level_eqv(x_2, x_1);
x_3 = lean_level_eq(x_2, x_1);
return x_3;
}
}
@ -2277,7 +2277,7 @@ if (lean_obj_tag(x_110) == 0)
{
uint8_t x_111;
lean_dec(x_10);
x_111 = lean_level_eqv(x_7, x_12);
x_111 = lean_level_eq(x_7, x_12);
lean_dec(x_12);
lean_dec(x_7);
if (x_111 == 0)
@ -2688,7 +2688,7 @@ if (lean_obj_tag(x_220) == 0)
{
uint8_t x_221;
lean_dec(x_127);
x_221 = lean_level_eqv(x_7, x_125);
x_221 = lean_level_eq(x_7, x_125);
lean_dec(x_125);
lean_dec(x_7);
if (x_221 == 0)
@ -3123,7 +3123,7 @@ if (lean_obj_tag(x_337) == 0)
{
uint8_t x_338;
lean_dec(x_244);
x_338 = lean_level_eqv(x_235, x_241);
x_338 = lean_level_eq(x_235, x_241);
lean_dec(x_241);
lean_dec(x_235);
if (x_338 == 0)

28
src/stage0/Init/Lean/TypeContext.c Normal file
View file

@ -0,0 +1,28 @@
// Lean compiler output
// Module: Init.Lean.TypeContext
// Imports: Init.Lean.Expr
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init_Lean_Expr(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_TypeContext(lean_object* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (lean_io_result_is_error(w)) return w;
w = initialize_Init_Lean_Expr(w);
if (lean_io_result_is_error(w)) return w;
return w;
}
#ifdef __cplusplus
}
#endif

10
tests/lean/run/expr1.lean
View file

@ -14,3 +14,13 @@ do let f := Expr.const `f [];
pure ()
#eval tst1
def tst2 : IO Unit :=
do let l1 := Level.max (Level.param `a) (Level.param `b);
let l2 := Level.max (Level.param `b) (Level.param `a);
IO.println l1;
IO.println l2;
unless (Level.isEquiv l1 l2) $ throw "not equiv";
pure ()
#eval tst2