From 9baf91e6417d1f918118637d3aaad5d5937635fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Oct 2019 10:56:59 -0700 Subject: [PATCH] feat: add `Level.isEquiv` --- library/Init/Lean/Level.lean | 12 +++-- src/kernel/level.cpp | 8 ++-- src/stage0/CMakeLists.txt | 2 +- src/stage0/Init/Lean/Expr.c | 56 ++++++++++++++++++++++-- src/stage0/Init/Lean/Level.c | 23 +++++++--- src/stage0/Init/Lean/TypeClass/Context.c | 10 ++--- src/stage0/Init/Lean/TypeContext.c | 28 ++++++++++++ tests/lean/run/expr1.lean | 10 +++++ 8 files changed, 128 insertions(+), 21 deletions(-) create mode 100644 src/stage0/Init/Lean/TypeContext.c diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean index 7bc36aa106..9f51e39dfd 100644 --- a/library/Init/Lean/Level.lean +++ b/library/Init/Lean/Level.lean @@ -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 diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 992616a703..c23700a366 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -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(l1); - level const & l2_ref = reinterpret_cast(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) { diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt index e38d10cde5..eaa2132ba4 100644 --- a/src/stage0/CMakeLists.txt +++ b/src/stage0/CMakeLists.txt @@ -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) diff --git a/src/stage0/Init/Lean/Expr.c b/src/stage0/Init/Lean/Expr.c index 88f25e21eb..966a6f3c87 100644 --- a/src/stage0/Init/Lean/Expr.c +++ b/src/stage0/Init/Lean/Expr.c @@ -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); diff --git a/src/stage0/Init/Lean/Level.c b/src/stage0/Init/Lean/Level.c index 7c8382ee19..e0b7352469 100644 --- a/src/stage0/Init/Lean/Level.c +++ b/src/stage0/Init/Lean/Level.c @@ -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: { diff --git a/src/stage0/Init/Lean/TypeClass/Context.c b/src/stage0/Init/Lean/TypeClass/Context.c index 2a0af891a6..dcb19cfe1c 100644 --- a/src/stage0/Init/Lean/TypeClass/Context.c +++ b/src/stage0/Init/Lean/TypeClass/Context.c @@ -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) diff --git a/src/stage0/Init/Lean/TypeContext.c b/src/stage0/Init/Lean/TypeContext.c new file mode 100644 index 0000000000..7850a83ea3 --- /dev/null +++ b/src/stage0/Init/Lean/TypeContext.c @@ -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 diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean index 0fa7b1173f..2e2542bbd8 100644 --- a/tests/lean/run/expr1.lean +++ b/tests/lean/run/expr1.lean @@ -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