sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: gen_constants_cpp.py: mark constants as persistent

Browse Source
This commit is contained in:
Sebastian Ullrich
2020-11-29 18:16:31 +01:00
parent ad5f8f021d
commit 65c1bc8952
2 changed files with 104 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
script/gen_constants_cpp.py
View File

@@ -74,6 +74,7 @@ def main(argv=None):
f.write('"%s"' % part)
first = False
f.write('};\n')
f.write(' mark_persistent(g_%s->raw());\n' % c[0])
f.write('}\n')
# finalize constants
f.write('void finalize_constants() {\n')

103
src/library/constants.cpp
View File

@@ -108,108 +108,211 @@ name const * g_uint64 = nullptr;
name const * g_usize = nullptr;
void initialize_constants() {
g_absurd = new name{"absurd"};
mark_persistent(g_absurd->raw());
g_and = new name{"And"};
mark_persistent(g_and->raw());
g_and_left = new name{"And", "left"};
mark_persistent(g_and_left->raw());
g_and_right = new name{"And", "right"};
mark_persistent(g_and_right->raw());
g_and_intro = new name{"And", "intro"};
mark_persistent(g_and_intro->raw());
g_and_rec = new name{"And", "rec"};
mark_persistent(g_and_rec->raw());
g_and_cases_on = new name{"And", "casesOn"};
mark_persistent(g_and_cases_on->raw());
g_array = new name{"Array"};
mark_persistent(g_array->raw());
g_array_sz = new name{"Array", "sz"};
mark_persistent(g_array_sz->raw());
g_array_data = new name{"Array", "data"};
mark_persistent(g_array_data->raw());
g_auto_param = new name{"autoParam"};
mark_persistent(g_auto_param->raw());
g_bit0 = new name{"bit0"};
mark_persistent(g_bit0->raw());
g_bit1 = new name{"bit1"};
mark_persistent(g_bit1->raw());
g_has_of_nat_of_nat = new name{"HasOfNat", "ofNat"};
mark_persistent(g_has_of_nat_of_nat->raw());
g_byte_array = new name{"ByteArray"};
mark_persistent(g_byte_array->raw());
g_bool = new name{"Bool"};
mark_persistent(g_bool->raw());
g_bool_false = new name{"Bool", "false"};
mark_persistent(g_bool_false->raw());
g_bool_true = new name{"Bool", "true"};
mark_persistent(g_bool_true->raw());
g_bool_cases_on = new name{"Bool", "casesOn"};
mark_persistent(g_bool_cases_on->raw());
g_cast = new name{"cast"};
mark_persistent(g_cast->raw());
g_char = new name{"Char"};
mark_persistent(g_char->raw());
g_congr_arg = new name{"congrArg"};
mark_persistent(g_congr_arg->raw());
g_decidable = new name{"Decidable"};
mark_persistent(g_decidable->raw());
g_decidable_is_true = new name{"Decidable", "isTrue"};
mark_persistent(g_decidable_is_true->raw());
g_decidable_is_false = new name{"Decidable", "isFalse"};
mark_persistent(g_decidable_is_false->raw());
g_decidable_decide = new name{"Decidable", "decide"};
mark_persistent(g_decidable_decide->raw());
g_empty = new name{"Empty"};
mark_persistent(g_empty->raw());
g_empty_rec = new name{"Empty", "rec"};
mark_persistent(g_empty_rec->raw());
g_empty_cases_on = new name{"Empty", "casesOn"};
mark_persistent(g_empty_cases_on->raw());
g_exists = new name{"Exists"};
mark_persistent(g_exists->raw());
g_eq = new name{"Eq"};
mark_persistent(g_eq->raw());
g_eq_cases_on = new name{"Eq", "casesOn"};
mark_persistent(g_eq_cases_on->raw());
g_eq_rec_on = new name{"Eq", "recOn"};
mark_persistent(g_eq_rec_on->raw());
g_eq_rec = new name{"Eq", "rec"};
mark_persistent(g_eq_rec->raw());
g_eq_ndrec = new name{"Eq", "ndrec"};
mark_persistent(g_eq_ndrec->raw());
g_eq_refl = new name{"Eq", "refl"};
mark_persistent(g_eq_refl->raw());
g_eq_subst = new name{"Eq", "subst"};
mark_persistent(g_eq_subst->raw());
g_eq_symm = new name{"Eq", "symm"};
mark_persistent(g_eq_symm->raw());
g_eq_trans = new name{"Eq", "trans"};
mark_persistent(g_eq_trans->raw());
g_float = new name{"Float"};
mark_persistent(g_float->raw());
g_float_array = new name{"FloatArray"};
mark_persistent(g_float_array->raw());
g_false = new name{"False"};
mark_persistent(g_false->raw());
g_false_rec = new name{"False", "rec"};
mark_persistent(g_false_rec->raw());
g_false_cases_on = new name{"False", "casesOn"};
mark_persistent(g_false_cases_on->raw());
g_has_add_add = new name{"HasAdd", "add"};
mark_persistent(g_has_add_add->raw());
g_has_neg_neg = new name{"HasNeg", "neg"};
mark_persistent(g_has_neg_neg->raw());
g_has_one_one = new name{"HasOne", "one"};
mark_persistent(g_has_one_one->raw());
g_has_zero_zero = new name{"HasZero", "zero"};
mark_persistent(g_has_zero_zero->raw());
g_heq = new name{"HEq"};
mark_persistent(g_heq->raw());
g_heq_refl = new name{"HEq", "refl"};
mark_persistent(g_heq_refl->raw());
g_iff = new name{"Iff"};
mark_persistent(g_iff->raw());
g_iff_refl = new name{"Iff", "refl"};
mark_persistent(g_iff_refl->raw());
g_int = new name{"Int"};
mark_persistent(g_int->raw());
g_int_nat_abs = new name{"Int", "natAbs"};
mark_persistent(g_int_nat_abs->raw());
g_int_dec_lt = new name{"Int", "decLt"};
mark_persistent(g_int_dec_lt->raw());
g_int_of_nat = new name{"Int", "ofNat"};
mark_persistent(g_int_of_nat->raw());
g_inline = new name{"inline"};
mark_persistent(g_inline->raw());
g_io = new name{"IO"};
mark_persistent(g_io->raw());
g_ite = new name{"ite"};
mark_persistent(g_ite->raw());
g_lc_proof = new name{"lcProof"};
mark_persistent(g_lc_proof->raw());
g_lc_unreachable = new name{"lcUnreachable"};
mark_persistent(g_lc_unreachable->raw());
g_list = new name{"List"};
mark_persistent(g_list->raw());
g_mut_quot = new name{"MutQuot"};
mark_persistent(g_mut_quot->raw());
g_nat = new name{"Nat"};
mark_persistent(g_nat->raw());
g_nat_succ = new name{"Nat", "succ"};
mark_persistent(g_nat_succ->raw());
g_nat_zero = new name{"Nat", "zero"};
mark_persistent(g_nat_zero->raw());
g_nat_has_zero = new name{"Nat", "HasZero"};
mark_persistent(g_nat_has_zero->raw());
g_nat_has_one = new name{"Nat", "HasOne"};
mark_persistent(g_nat_has_one->raw());
g_nat_has_add = new name{"Nat", "HasAdd"};
mark_persistent(g_nat_has_add->raw());
g_nat_add = new name{"Nat", "add"};
mark_persistent(g_nat_add->raw());
g_nat_dec_eq = new name{"Nat", "decEq"};
mark_persistent(g_nat_dec_eq->raw());
g_nat_sub = new name{"Nat", "sub"};
mark_persistent(g_nat_sub->raw());
g_ne = new name{"ne"};
mark_persistent(g_ne->raw());
g_not = new name{"Not"};
mark_persistent(g_not->raw());
g_opt_param = new name{"optParam"};
mark_persistent(g_opt_param->raw());
g_or = new name{"Or"};
mark_persistent(g_or->raw());
g_panic = new name{"panic"};
mark_persistent(g_panic->raw());
g_punit = new name{"PUnit"};
mark_persistent(g_punit->raw());
g_punit_unit = new name{"PUnit", "unit"};
mark_persistent(g_punit_unit->raw());
g_pprod = new name{"PProd"};
mark_persistent(g_pprod->raw());
g_pprod_mk = new name{"PProd", "mk"};
mark_persistent(g_pprod_mk->raw());
g_pprod_fst = new name{"PProd", "fst"};
mark_persistent(g_pprod_fst->raw());
g_pprod_snd = new name{"PProd", "snd"};
mark_persistent(g_pprod_snd->raw());
g_propext = new name{"propext"};
mark_persistent(g_propext->raw());
g_quot_mk = new name{"Quot", "mk"};
mark_persistent(g_quot_mk->raw());
g_quot_lift = new name{"Quot", "lift"};
mark_persistent(g_quot_lift->raw());
g_sorry_ax = new name{"sorryAx"};
mark_persistent(g_sorry_ax->raw());
g_string = new name{"String"};
mark_persistent(g_string->raw());
g_string_data = new name{"String", "data"};
mark_persistent(g_string_data->raw());
g_subsingleton_elim = new name{"Subsingleton", "elim"};
mark_persistent(g_subsingleton_elim->raw());
g_task = new name{"Task"};
mark_persistent(g_task->raw());
g_thunk = new name{"Thunk"};
mark_persistent(g_thunk->raw());
g_thunk_mk = new name{"Thunk", "mk"};
mark_persistent(g_thunk_mk->raw());
g_thunk_get = new name{"Thunk", "get"};
mark_persistent(g_thunk_get->raw());
g_true = new name{"True"};
mark_persistent(g_true->raw());
g_true_intro = new name{"True", "intro"};
mark_persistent(g_true_intro->raw());
g_unit = new name{"Unit"};
mark_persistent(g_unit->raw());
g_unit_unit = new name{"Unit", "unit"};
mark_persistent(g_unit_unit->raw());
g_uint8 = new name{"UInt8"};
mark_persistent(g_uint8->raw());
g_uint16 = new name{"UInt16"};
mark_persistent(g_uint16->raw());
g_uint32 = new name{"UInt32"};
mark_persistent(g_uint32->raw());
g_uint64 = new name{"UInt64"};
mark_persistent(g_uint64->raw());
g_usize = new name{"USize"};
mark_persistent(g_usize->raw());
}
void finalize_constants() {
delete g_absurd;