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-01-01 09:20:02 -08:00
parent 73e114c6a2
commit 53042658ec
5 changed files with 457 additions and 520 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Control/Except.lean
View file

@ -18,7 +18,7 @@ inductive Except (ε : Type u) (α : Type v)
attribute [unbox] Except
instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) :=
instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) :=
⟨Except.error (arbitrary ε)⟩
section

2
stage0/src/Init/Lean/Environment.lean
View file

@ -593,7 +593,7 @@ pExtDescrs.forM $ fun extDescr => do {
pure ()
@[extern "lean_eval_const"]
unsafe constant evalConst (α) [s : @& Inhabited α] (env : @& Environment) (constName : @& Name) : Except String α := arbitrary _
unsafe constant evalConst (α) (env : @& Environment) (constName : @& Name) : Except String α := arbitrary _
end Environment

2
stage0/src/library/compiler/ir_interpreter.cpp
View file

@ -893,7 +893,7 @@ uint32 run_main(environment const & env, int argv, char * argc[]) {
return interpreter(env).run_main(argv, argc);
}
extern "C" object * lean_eval_const(object * /* inh */, object * env, object * c) {
extern "C" object * lean_eval_const(object * env, object * c) {
try {
return mk_cnstr(1, run_boxed(TO_REF(environment, env), TO_REF(name, c), 0, 0)).steal();
} catch (exception & ex) {

13
stage0/stdlib/Init/Lean/Environment.c
View file

@ -108,7 +108,7 @@ lean_object* l_Lean_namespacesExt___elambda__4___rarg(lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1;
lean_object* l_Lean_PersistentEnvExtension_modifyState___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_evalConst___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_evalConst___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtension___rarg(lean_object*);
extern lean_object* l_List_repr___rarg___closed__3;
lean_object* l_Lean_PersistentEnvExtension_setState___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -231,7 +231,7 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_registerSimplePersisten
extern lean_object* l_List_reprAux___main___rarg___closed__1;
lean_object* l_Lean_SimplePersistentEnvExtension_modifyState___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_matchConst(lean_object*);
lean_object* lean_eval_const(lean_object*, lean_object*, lean_object*);
lean_object* lean_eval_const(lean_object*, lean_object*);
lean_object* l_Lean_SMap_contains___at_Lean_Environment_contains___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_SimplePersistentEnvExtension_getEntries___rarg(lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_registerSimplePersistentEnvExtension___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -12155,15 +12155,14 @@ lean_dec(x_1);
return x_5;
}
}
lean_object* l_Lean_Environment_evalConst___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Environment_evalConst___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_5;
x_5 = lean_eval_const(x_2, x_3, x_4);
lean_dec(x_4);
lean_object* x_4;
x_4 = lean_eval_const(x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
return x_4;
}
}
lean_object* l_Lean_matchConst___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {

958
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

File diff suppressed because it is too large Load diff