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-22 13:13:37 -07:00
parent 311265d833
commit fafad59577
3 changed files with 27 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
stage0/src/Init/LeanInit.lean generated
View file

@ -83,6 +83,13 @@ mkNameStr Name.anonymous s
namespace Name
@[extern "lean_name_eq"]
protected def beq : (@& Name) → (@& Name) → Bool
| anonymous, anonymous => true
| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && beq p₁ p₂
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && beq p₁ p₂
| _, _ => false
@[extern "lean_name_eq"]
protected def Name.beq : (@& Name) → (@& Name) → Bool
| anonymous, anonymous => true

11
stage0/src/library/compiler/compiler.cpp generated
View file

@ -173,13 +173,16 @@ environment compile(environment const & env, options const & opts, names cs) {
}
}
if (length(cs) == 1 && is_extern_constant(env, head(cs))) {
/* Generate boxed version for extern/native constant if needed. */
return ir::add_extern(env, head(cs));
if (length(cs) == 1) {
name c = get_real_name(head(cs));
if (is_extern_constant(env, c)) {
/* Generate boxed version for extern/native constant if needed. */
return ir::add_extern(env, c);
}
}
for (name const & c : cs) {
lean_assert(!is_extern_constant(env, c));
lean_assert(!is_extern_constant(env, get_real_name(c)));
constant_info cinfo = env.get(c);
if (!cinfo.is_definition() && !cinfo.is_opaque()) return env;
if (has_synthetic_sorry(cinfo)) return env;

13
stage0/stdlib/Init/LeanInit.c generated
View file

@ -91,6 +91,7 @@ uint8_t l_Char_isDigit(uint32_t);
lean_object* l_Lean_charLitKind___closed__2;
lean_object* l_Lean_Substring_HasQuote(lean_object*);
lean_object* l___private_Init_LeanInit_8__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_8__decodeOctalLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isGreek___boxed(lean_object*);
lean_object* l_Lean_Substring_HasQuote___closed__2;
@ -341,6 +342,7 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
uint8_t l_Lean_isGreek(uint32_t);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_MacroScopesView_review(lean_object*);
lean_object* l_Lean_Name_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg___boxed(lean_object*, lean_object*);
lean_object* l_Array_filterSepElems(lean_object*, lean_object*);
lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(lean_object*, lean_object*);
@ -1215,6 +1217,17 @@ x_3 = lean_name_mk_string(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_name_eq(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_Name_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{