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

feat: simplistic linter framework

Browse source
This commit is contained in:
Sebastian Ullrich 2019-11-09 17:53:10 +01:00 • committed by Leonardo de Moura
parent da69beac0a
commit dac6f273b5
10 changed files with 4678 additions and 2534 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/Init/Lean/Default.lean
View file

@ -21,3 +21,4 @@ import Init.Lean.MetavarContext
import Init.Lean.TypeClass
import Init.Lean.Trace
import Init.Lean.AuxRecursor
import Init.Lean.Linter

28
library/Init/Lean/Linter.lean Normal file
View file

@ -0,0 +1,28 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
prelude
import Init.System.IO
import Init.Lean.Attributes
import Init.Lean.Message
import Init.Lean.Syntax
namespace Lean
def Linter := Environment → Name → /-Syntax → -/IO MessageLog
def mkLintersRef : IO (IO.Ref (Array Linter)) :=
IO.mkRef #[]
/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
environment (which only contains `import`ed objects). -/
@[init mkLintersRef, export lean_linters_ref]
constant lintersRef : IO.Ref (Array Linter) := arbitrary _
def addLinter (l : Linter) : IO Unit := do
ls ← lintersRef.get;
lintersRef.set (ls.push l)
end Lean

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/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/HashSet.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/Control.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.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/PersistentHashSet.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/AuxRecursor.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/LBool.c ./Init/Lean/LOption.c ./Init/Lean/Level.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/Meta.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/MonadCache.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/Lean/WHNF.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/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/HashSet.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/Control.c ./Init/Data/List/Default.c ./Init/Data/List/Instances.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.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/PersistentHashSet.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/AuxRecursor.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/LBool.c ./Init/Lean/LOption.c ./Init/Lean/Level.c ./Init/Lean/Linter.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/Meta.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/MonadCache.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/Lean/WHNF.c ./Init/System/Default.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c)

6
src/stage0/Init/Lean/Default.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Default
// Imports: Init.Lean.Path Init.Lean.Compiler.Default Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser.Default Init.Lean.ReducibilityAttrs Init.Lean.Elaborator.Default Init.Lean.EqnCompiler.Default Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.TypeClass.Default Init.Lean.Trace Init.Lean.AuxRecursor
// Imports: Init.Lean.Path Init.Lean.Compiler.Default Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser.Default Init.Lean.ReducibilityAttrs Init.Lean.Elaborator.Default Init.Lean.EqnCompiler.Default Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.TypeClass.Default Init.Lean.Trace Init.Lean.AuxRecursor Init.Lean.Linter
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -30,6 +30,7 @@ lean_object* initialize_Init_Lean_MetavarContext(lean_object*);
lean_object* initialize_Init_Lean_TypeClass_Default(lean_object*);
lean_object* initialize_Init_Lean_Trace(lean_object*);
lean_object* initialize_Init_Lean_AuxRecursor(lean_object*);
lean_object* initialize_Init_Lean_Linter(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Default(lean_object* w) {
lean_object * res;
@ -86,6 +87,9 @@ lean_dec_ref(res);
res = initialize_Init_Lean_AuxRecursor(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Linter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

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

@ -65,6 +65,7 @@ size_t lean_expr_hash(lean_object*);
lean_object* l_Lean_Expr_appFn_x21___boxed(lean_object*);
extern lean_object* l_List_get_x21___main___rarg___closed__2;
lean_object* l_Lean_Expr_updateLambda_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVar___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_5__mkAppRevRangeAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_panicWithPos___at_Lean_Expr_constLevels_x21___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ExprStructEq_Hashable;
@ -117,6 +118,7 @@ lean_object* l___private_Init_Lean_Expr_4__withAppRevAux___main(lean_object*);
lean_object* l_Lean_ExprStructEq_HasToString(lean_object*);
lean_object* l_Lean_mkAppRev(lean_object*, lean_object*);
lean_object* l_Lean_Expr_constLevels_x21(lean_object*);
uint8_t lean_expr_has_loose_bvar(lean_object*, lean_object*);
lean_object* l_Lean_mkAppRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateMData_x21(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
@ -2609,6 +2611,17 @@ x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_hasLooseBVar___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_expr_has_loose_bvar(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_Expr_instantiate___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -3168,7 +3181,7 @@ lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_5 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_6 = lean_unsigned_to_nat(464u);
x_6 = lean_unsigned_to_nat(467u);
x_7 = lean_unsigned_to_nat(16u);
x_8 = l_Lean_Expr_appFn_x21___closed__1;
x_9 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_5, x_6, x_7, x_8);
@ -3199,7 +3212,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
lean_dec(x_2);
lean_dec(x_1);
x_4 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_5 = lean_unsigned_to_nat(473u);
x_5 = lean_unsigned_to_nat(476u);
x_6 = lean_unsigned_to_nat(16u);
x_7 = l_Lean_Expr_constName_x21___closed__1;
x_8 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_4, x_5, x_6, x_7);
@ -3238,7 +3251,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
lean_dec(x_2);
lean_dec(x_1);
x_4 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_5 = lean_unsigned_to_nat(482u);
x_5 = lean_unsigned_to_nat(485u);
x_6 = lean_unsigned_to_nat(12u);
x_7 = l_Lean_Expr_updateSort_x21___closed__1;
x_8 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_4, x_5, x_6, x_7);
@ -3285,7 +3298,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
lean_dec(x_2);
lean_dec(x_1);
x_4 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_5 = lean_unsigned_to_nat(499u);
x_5 = lean_unsigned_to_nat(502u);
x_6 = lean_unsigned_to_nat(15u);
x_7 = l_Lean_Expr_updateMData_x21___closed__1;
x_8 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_4, x_5, x_6, x_7);
@ -3316,7 +3329,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
lean_dec(x_2);
lean_dec(x_1);
x_4 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_5 = lean_unsigned_to_nat(504u);
x_5 = lean_unsigned_to_nat(507u);
x_6 = lean_unsigned_to_nat(16u);
x_7 = l_Lean_Expr_updateProj_x21___closed__1;
x_8 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_4, x_5, x_6, x_7);
@ -3358,7 +3371,7 @@ lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_6 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_7 = lean_unsigned_to_nat(513u);
x_7 = lean_unsigned_to_nat(516u);
x_8 = lean_unsigned_to_nat(22u);
x_9 = l_Lean_Expr_updateForall_x21___closed__1;
x_10 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_6, x_7, x_8, x_9);
@ -3393,7 +3406,7 @@ lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_7 = lean_unsigned_to_nat(518u);
x_7 = lean_unsigned_to_nat(521u);
x_8 = lean_unsigned_to_nat(22u);
x_9 = l_Lean_Expr_updateForall_x21___closed__1;
x_10 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_6, x_7, x_8, x_9);
@ -3435,7 +3448,7 @@ lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_6 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_7 = lean_unsigned_to_nat(527u);
x_7 = lean_unsigned_to_nat(530u);
x_8 = lean_unsigned_to_nat(18u);
x_9 = l_Lean_Expr_updateLambda_x21___closed__1;
x_10 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_6, x_7, x_8, x_9);
@ -3470,7 +3483,7 @@ lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_7 = lean_unsigned_to_nat(532u);
x_7 = lean_unsigned_to_nat(535u);
x_8 = lean_unsigned_to_nat(18u);
x_9 = l_Lean_Expr_updateLambda_x21___closed__1;
x_10 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_6, x_7, x_8, x_9);
@ -3503,7 +3516,7 @@ lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_7 = lean_unsigned_to_nat(541u);
x_7 = lean_unsigned_to_nat(544u);
x_8 = lean_unsigned_to_nat(18u);
x_9 = l_Lean_Expr_letName_x21___closed__1;
x_10 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_6, x_7, x_8, x_9);

106
src/stage0/Init/Lean/Linter.c Normal file
View file

@ -0,0 +1,106 @@
// Lean compiler output
// Module: Init.Lean.Linter
// Imports: Init.System.IO Init.Lean.Attributes Init.Lean.Message Init.Lean.Syntax
#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
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_linters_ref;
lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addLinter(lean_object*, lean_object*);
lean_object* l_Lean_mkLintersRef(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_mkLintersRef(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Array_empty___closed__1;
x_3 = lean_io_mk_ref(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_addLinter(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_linters_ref;
x_4 = lean_io_ref_get(x_3, x_2);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_4);
x_7 = lean_array_push(x_5, x_1);
x_8 = lean_io_ref_set(x_3, x_7, x_6);
return x_8;
}
else
{
uint8_t x_9;
lean_dec(x_1);
x_9 = !lean_is_exclusive(x_4);
if (x_9 == 0)
{
return x_4;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_4, 0);
x_11 = lean_ctor_get(x_4, 1);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_4);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
}
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Init_Lean_Attributes(lean_object*);
lean_object* initialize_Init_Lean_Message(lean_object*);
lean_object* initialize_Init_Lean_Syntax(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Linter(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Attributes(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Message(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Syntax(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_mkLintersRef(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_linters_ref = lean_io_result_get_value(res);
lean_mark_persistent(lean_linters_ref);
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

82
src/stage0/Init/Lean/LocalContext.c
View file

@ -148,6 +148,7 @@ lean_object* l_Array_anyMAux___main___at_Lean_LocalContext_anyM___spec__4___rarg
lean_object* l___private_Init_Lean_LocalContext_1__popTailNoneAux(lean_object*);
lean_object* l_PersistentHashMap_erase___at_Lean_LocalContext_erase___spec__1(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insert___at_Lean_LocalContext_mkLocalDecl___spec__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_loose_bvar(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_PersistentArray_set___rarg(lean_object*, lean_object*, lean_object*);
@ -6931,7 +6932,7 @@ if (lean_obj_tag(x_12) == 0)
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_5);
x_13 = l_Lean_LocalDecl_value___closed__1;
x_14 = lean_unsigned_to_nat(256u);
x_14 = lean_unsigned_to_nat(259u);
x_15 = lean_unsigned_to_nat(12u);
x_16 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
x_17 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_13, x_14, x_15, x_16);
@ -6975,7 +6976,7 @@ goto _start;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_28 = lean_ctor_get(x_19, 2);
lean_inc(x_28);
x_29 = lean_ctor_get(x_19, 3);
@ -6983,15 +6984,28 @@ lean_inc(x_29);
x_30 = lean_ctor_get(x_19, 4);
lean_inc(x_30);
lean_dec(x_19);
x_31 = lean_expr_abstract_range(x_29, x_9, x_3);
lean_dec(x_29);
x_32 = lean_expr_abstract_range(x_30, x_9, x_3);
x_31 = lean_expr_has_loose_bvar(x_5, x_6);
if (x_31 == 0)
{
lean_dec(x_30);
x_33 = lean_expr_mk_let(x_28, x_31, x_32, x_5);
lean_dec(x_29);
lean_dec(x_28);
x_4 = x_9;
x_5 = x_33;
goto _start;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_expr_abstract_range(x_29, x_9, x_3);
lean_dec(x_29);
x_34 = lean_expr_abstract_range(x_30, x_9, x_3);
lean_dec(x_30);
x_35 = lean_expr_mk_let(x_28, x_33, x_34, x_5);
x_4 = x_9;
x_5 = x_35;
goto _start;
}
}
}
}
else
@ -7057,7 +7071,7 @@ if (lean_obj_tag(x_11) == 0)
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_4);
x_12 = l_Lean_LocalDecl_value___closed__1;
x_13 = lean_unsigned_to_nat(256u);
x_13 = lean_unsigned_to_nat(259u);
x_14 = lean_unsigned_to_nat(12u);
x_15 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
x_16 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_12, x_13, x_14, x_15);
@ -7089,7 +7103,7 @@ goto _start;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_25 = lean_ctor_get(x_18, 2);
lean_inc(x_25);
x_26 = lean_ctor_get(x_18, 3);
@ -7097,15 +7111,28 @@ lean_inc(x_26);
x_27 = lean_ctor_get(x_18, 4);
lean_inc(x_27);
lean_dec(x_18);
x_28 = lean_expr_abstract_range(x_26, x_8, x_2);
lean_dec(x_26);
x_29 = lean_expr_abstract_range(x_27, x_8, x_2);
x_28 = lean_expr_has_loose_bvar(x_4, x_5);
if (x_28 == 0)
{
lean_dec(x_27);
x_30 = lean_expr_mk_let(x_25, x_28, x_29, x_4);
lean_dec(x_26);
lean_dec(x_25);
x_3 = x_8;
x_4 = x_30;
goto _start;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_expr_abstract_range(x_26, x_8, x_2);
lean_dec(x_26);
x_31 = lean_expr_abstract_range(x_27, x_8, x_2);
lean_dec(x_27);
x_32 = lean_expr_mk_let(x_25, x_30, x_31, x_4);
x_3 = x_8;
x_4 = x_32;
goto _start;
}
}
}
}
else
@ -7167,7 +7194,7 @@ if (lean_obj_tag(x_11) == 0)
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_4);
x_12 = l_Lean_LocalDecl_value___closed__1;
x_13 = lean_unsigned_to_nat(256u);
x_13 = lean_unsigned_to_nat(259u);
x_14 = lean_unsigned_to_nat(12u);
x_15 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___closed__1;
x_16 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_12, x_13, x_14, x_15);
@ -7199,7 +7226,7 @@ goto _start;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_25 = lean_ctor_get(x_18, 2);
lean_inc(x_25);
x_26 = lean_ctor_get(x_18, 3);
@ -7207,15 +7234,28 @@ lean_inc(x_26);
x_27 = lean_ctor_get(x_18, 4);
lean_inc(x_27);
lean_dec(x_18);
x_28 = lean_expr_abstract_range(x_26, x_8, x_2);
lean_dec(x_26);
x_29 = lean_expr_abstract_range(x_27, x_8, x_2);
x_28 = lean_expr_has_loose_bvar(x_4, x_5);
if (x_28 == 0)
{
lean_dec(x_27);
x_30 = lean_expr_mk_let(x_25, x_28, x_29, x_4);
lean_dec(x_26);
lean_dec(x_25);
x_3 = x_8;
x_4 = x_30;
goto _start;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_expr_abstract_range(x_26, x_8, x_2);
lean_dec(x_26);
x_31 = lean_expr_abstract_range(x_27, x_8, x_2);
lean_dec(x_27);
x_32 = lean_expr_mk_let(x_25, x_30, x_31, x_4);
x_3 = x_8;
x_4 = x_32;
goto _start;
}
}
}
}
else

5609
src/stage0/Init/Lean/Meta.c
View file

File diff suppressed because it is too large Load diff

1341
src/stage0/Init/Lean/MetavarContext.c
View file

File diff suppressed because it is too large Load diff

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

@ -6741,7 +6741,7 @@ lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean
x_80 = lean_ctor_get(x_71, 0);
lean_dec(x_80);
x_81 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_82 = lean_unsigned_to_nat(473u);
x_82 = lean_unsigned_to_nat(476u);
x_83 = lean_unsigned_to_nat(16u);
x_84 = l_Lean_Expr_constName_x21___closed__1;
x_85 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_81, x_82, x_83, x_84);
@ -6755,7 +6755,7 @@ x_86 = lean_ctor_get(x_71, 1);
lean_inc(x_86);
lean_dec(x_71);
x_87 = l_Lean_Expr_getRevArg_x21___main___closed__1;
x_88 = lean_unsigned_to_nat(473u);
x_88 = lean_unsigned_to_nat(476u);
x_89 = lean_unsigned_to_nat(16u);
x_90 = l_Lean_Expr_constName_x21___closed__1;
x_91 = l_panicWithPos___at_Lean_Expr_getRevArg_x21___main___spec__1(x_87, x_88, x_89, x_90);