From 27f6bfd3f0ac44a8044f2a98e5076f9fd764abce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Jan 2015 16:50:32 -0800 Subject: [PATCH] refactor(*): add file constants.txt with all constants used by the Lean binary --- script/gen_constants_cpp.py | 89 ++++ src/frontends/lean/builtin_exprs.cpp | 28 +- src/frontends/lean/elaborator.cpp | 3 +- src/frontends/lean/pp.cpp | 10 +- src/frontends/lean/structure_cmd.cpp | 9 +- src/frontends/lean/tactic_hint.cpp | 3 +- src/library/CMakeLists.txt | 2 +- src/library/constants.cpp | 434 ++++++++++++++++++++ src/library/constants.h | 114 +++++ src/library/constants.txt | 106 +++++ src/library/definitional/cases_on.cpp | 5 +- src/library/definitional/equations.cpp | 9 +- src/library/definitional/no_confusion.cpp | 28 +- src/library/init_module.cpp | 3 + src/library/num.cpp | 15 +- src/library/resolve_macro.cpp | 15 +- src/library/string.cpp | 17 +- src/library/tactic/apply_tactic.cpp | 9 +- src/library/tactic/assert_tactic.cpp | 3 +- src/library/tactic/class_instance_synth.cpp | 6 +- src/library/tactic/clear_tactic.cpp | 5 +- src/library/tactic/exact_tactic.cpp | 3 +- src/library/tactic/expr_to_tactic.cpp | 81 ++-- src/library/tactic/generalize_tactic.cpp | 5 +- src/library/tactic/intros_tactic.cpp | 5 +- src/library/tactic/inversion_tactic.cpp | 41 +- src/library/tactic/rename_tactic.cpp | 3 +- src/library/tactic/revert_tactic.cpp | 5 +- src/library/tactic/trace_tactic.cpp | 5 +- src/library/tactic/unfold_tactic.cpp | 3 +- src/library/tactic/util.cpp | 6 +- src/library/tactic/whnf_tactic.cpp | 3 +- src/library/util.cpp | 99 ++--- 33 files changed, 933 insertions(+), 239 deletions(-) create mode 100644 script/gen_constants_cpp.py create mode 100644 src/library/constants.cpp create mode 100644 src/library/constants.h create mode 100644 src/library/constants.txt diff --git a/script/gen_constants_cpp.py b/script/gen_constants_cpp.py new file mode 100644 index 000000000..5b6bdcbab --- /dev/null +++ b/script/gen_constants_cpp.py @@ -0,0 +1,89 @@ +#!/usr/bin/env python +# -*- coding: utf-8 -*- +# +# Copyright (c) 2015 Microsoft Corporation. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# +# Author: Leonardo de Moura +# +# Given a text file containing constants defined in the Lean libraries, +# this script generates .h and .cpp files for initialing/finalizing theses constants +# as C++ name objects. +# +# This script is used to generate src/library/constants.cpp and src/library/constants.h +import sys +import os + +def error(msg): + print("Error: %s" % msg) + exit(1) + +def to_c_const(s): + out = "" + for c in s: + if c == '.' or c == '_': + out += '_' + elif c.isalpha() or c.isdigit(): + out += c + else: + error("unsupported character in constant: %s" % s) + return out + +def main(argv=None): + if argv is None: + argv = sys.argv[1:] + infile = argv[0] + basename, ext = os.path.splitext(infile) + cppfile = basename + ".cpp" + hfile = basename + ".h" + constants = [] + with open(infile, 'r') as f: + for line in f: + constants.append([to_c_const(line.strip()), line.strip()]) + with open(hfile, 'w') as f: + f.write('// Copyright (c) 2015 Microsoft Corporation. All rights reserved.\n') + f.write('// Released under Apache 2.0 license as described in the file LICENSE.\n') + f.write('// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n') + f.write('#include "util/name.h"\n') + f.write('namespace lean {\n') + f.write('void initialize_constants();\n') + f.write('void finalize_constants();\n') + for c in constants: + f.write('name const & get_%s_name();\n' % c[0]) + f.write('}\n') + with open(cppfile, 'w') as f: + f.write('// Copyright (c) 2015 Microsoft Corporation. All rights reserved.\n') + f.write('// Released under Apache 2.0 license as described in the file LICENSE.\n') + f.write('// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n') + f.write('#include "util/name.h"\n') + f.write('namespace lean{\n') + # declare constants + for c in constants: + f.write('name const * g_%s = nullptr;\n' % c[0]) + # initialize constants + f.write('void initialize_constants() {\n') + for c in constants: + f.write(' g_%s = new name{' % c[0]) + first = True + for part in c[1].split('.'): + if not first: + f.write(", ") + f.write('"%s"' % part) + first = False + f.write('};\n') + f.write('}\n') + # finalize constants + f.write('void finalize_constants() {\n') + for c in constants: + f.write(' delete g_%s;\n' % c[0]) + f.write('}\n') + # get methods + for c in constants: + f.write('name const & get_%s_name() { return *g_%s; }\n' % (c[0], c[0])) + # end namespace + f.write('}\n') + print("done") + return 0 + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index c85748e4f..ce8bbe87e 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "library/typed_expr.h" #include "library/choice.h" #include "library/let.h" +#include "library/constants.h" #include "library/definitional/equations.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/decl_cmds.h" @@ -123,8 +124,8 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const static environment open_tactic_namespace(parser & p) { if (!is_tactic_namespace_open(p.env())) { - environment env = using_namespace(p.env(), p.ios(), "tactic"); - env = add_aliases(env, name("tactic"), name()); + environment env = using_namespace(p.env(), p.ios(), get_tactic_name()); + env = add_aliases(env, get_tactic_name(), name()); return env; } else { return p.env(); @@ -330,9 +331,8 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) return p.save_pos(mk_show_annotation(r), pos); } -static name * g_exists_elim = nullptr; static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) { - if (!p.env().find(*g_exists_elim)) + if (!p.env().find(get_exists_elim_name())) throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists.elim' theorem", pos); // exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) buffer ps; @@ -364,28 +364,26 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po expr a = ps[i]; expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false)); expr H2 = Fun({a, H}, b); - b = mk_app(mk_constant(*g_exists_elim), H_aux, H2); + b = mk_app(mk_constant(get_exists_elim_name()), H_aux, H2); H = H_aux; } expr a = ps[0]; expr H2 = Fun({a, H}, b); - expr r = mk_app(mk_constant(*g_exists_elim), H1, H2); + expr r = mk_app(mk_constant(get_exists_elim_name()), H1, H2); return p.rec_save_pos(r, pos); } -static name * g_ite = nullptr; -static name * g_dite = nullptr; static expr * g_not = nullptr; static unsigned g_then_else_prec = 45; static expr parse_ite(parser & p, expr const & c, pos_info const & pos) { - if (!p.env().find(*g_ite)) + if (!p.env().find(get_ite_name())) throw parser_error("invalid use of 'if-then-else' expression, environment does not contain 'ite' definition", pos); p.check_token_next(get_then_tk(), "invalid 'if-then-else' expression, 'then' expected"); expr t = p.parse_expr(g_then_else_prec); p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected"); expr e = p.parse_expr(g_then_else_prec); - return p.save_pos(mk_app(mk_constant(*g_ite), c, t, e), pos); + return p.save_pos(mk_app(mk_constant(get_ite_name()), c, t, e), pos); } static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info const & pos) { @@ -406,7 +404,7 @@ static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info auto pos = p.pos(); e = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos); } - return p.save_pos(mk_app(p.save_pos(mk_constant(*g_dite), pos), c, t, e), pos); + return p.save_pos(mk_app(p.save_pos(mk_constant(get_dite_name()), pos), c, t, e), pos); } static expr parse_if_then_else(parser & p, unsigned, expr const *, pos_info const & pos) { @@ -523,10 +521,7 @@ parse_table get_builtin_led_table() { void initialize_builtin_exprs() { notation::H_show = new name("H_show"); - notation::g_exists_elim = new name{"exists", "elim"}; - notation::g_ite = new name("ite"); - notation::g_dite = new name("dite"); - notation::g_not = new expr(mk_constant("not")); + notation::g_not = new expr(mk_constant(get_not_name())); g_nud_table = new parse_table(); *g_nud_table = notation::init_nud_table(); g_led_table = new parse_table(); @@ -537,9 +532,6 @@ void finalize_builtin_exprs() { delete g_led_table; delete g_nud_table; delete notation::H_show; - delete notation::g_exists_elim; - delete notation::g_ite; - delete notation::g_dite; delete notation::g_not; } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3c732c99b..7905298c6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -32,6 +32,7 @@ Author: Leonardo de Moura #include "library/deep_copy.h" #include "library/typed_expr.h" #include "library/local_context.h" +#include "library/constants.h" #include "library/util.h" #include "library/choice_iterator.h" #include "library/pp_options.h" @@ -1068,7 +1069,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { new_R = visit(equations_wf_rel(eqns), cs); new_Hwf = visit(equations_wf_proof(eqns), cs); expr Hwf_type = infer_type(*new_Hwf, cs); - expr wf = visit(mk_constant("well_founded"), cs); + expr wf = visit(mk_constant(get_well_founded_name()), cs); wf = ::lean::mk_app(wf, *new_R); justification j = mk_type_mismatch_jst(*new_Hwf, Hwf_type, wf, equations_wf_proof(eqns)); auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j, m_relax_main_opaque); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 97d252243..3db36ddc4 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/let.h" #include "library/print.h" #include "library/pp_options.h" +#include "library/constants.h" #include "frontends/lean/pp.h" #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" @@ -59,10 +60,11 @@ class nat_numeral_pp { expr m_succ; public: nat_numeral_pp(): - m_num_type(mk_constant("num")), m_nat("nat"), - m_nat_of_num(mk_constant(name{"nat", "of_num"})), - m_zero(mk_constant(name{"nat", "zero"})), - m_succ(mk_constant(name{"nat", "succ"})) { + m_num_type(mk_constant(get_num_name())), + m_nat(get_nat_name()), + m_nat_of_num(mk_constant(get_nat_of_num_name())), + m_zero(mk_constant(get_nat_zero_name())), + m_succ(mk_constant(get_nat_succ_name())) { } // Return ture if the environment has a coercion from num->nat diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 8ee292690..ba0a4c78c 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -28,6 +28,7 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/protected.h" #include "library/class.h" +#include "library/constants.h" #include "library/util.h" #include "library/kernel_serializer.h" #include "library/definitional/rec_on.h" @@ -821,13 +822,13 @@ struct structure_cmd_fn { expr proj = mk_app(mk_app(mk_constant(m_name + mlocal_name(field), st_ls), m_params), st); lhs = mk_app(lhs, proj); } - expr eq = mk_app(mk_constant("eq", to_list(sort_level(m_type))), st_type, lhs, st); + expr eq = mk_app(mk_constant(get_eq_name(), to_list(sort_level(m_type))), st_type, lhs, st); level eq_lvl = sort_level(m_tc->ensure_type(eq).first); levels rec_ls = levels(eq_lvl, st_ls); expr rec = mk_app(mk_constant(inductive::get_elim_name(m_name), rec_ls), m_params); expr type_former = Fun(st, eq); expr mk = mk_app(mk_app(mk_constant(m_mk, st_ls), m_params), m_fields); - expr refl = mk_app(mk_constant(name{"eq", "refl"}, to_list(sort_level(m_type))), st_type, mk); + expr refl = mk_app(mk_constant(get_eq_refl_name(), to_list(sort_level(m_type))), st_type, mk); refl = Fun(m_fields, refl); rec = mk_app(rec, type_former, refl, st); expr eta_type = infer_implicit(Pi(m_params, Pi(st, eq)), true); @@ -859,8 +860,8 @@ struct structure_cmd_fn { name proj_name = m_name + field_name; expr lhs = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), mk_fields); expr rhs = field; - expr eq = mk_app(mk_constant("eq", to_list(field_level)), field_type, lhs, rhs); - expr refl = mk_app(mk_constant(name{"eq", "refl"}, to_list(field_level)), field_type, lhs); + expr eq = mk_app(mk_constant(get_eq_name(), to_list(field_level)), field_type, lhs, rhs); + expr refl = mk_app(mk_constant(get_eq_refl_name(), to_list(field_level)), field_type, lhs); name proj_over_name = m_name + field_name + m_mk_short; expr proj_over_type = infer_implicit(Pi(m_params, Pi(m_fields, eq)), m_params.size(), true); expr proj_over_value = Fun(m_params, Fun(m_fields, refl)); diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index 63629dea4..695ad256d 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "kernel/type_checker.h" #include "library/scoped_ext.h" +#include "library/constants.h" #include "library/kernel_serializer.h" #include "library/tactic/tactic.h" #include "frontends/lean/tactic_hint.h" @@ -77,7 +78,7 @@ expr parse_tactic_name(parser & p) { name pre_tac = p.check_constant_next("invalid tactic name, constant expected"); auto decl = p.env().get(pre_tac); expr pre_tac_type = decl.get_type(); - if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name("tactic")) + if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != get_tactic_name()) throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos); buffer ls; for (auto const & n : decl.get_univ_params()) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index eef161710..f6ead79c7 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp - kernel_bindings.cpp io_state_stream.cpp bin_app.cpp + kernel_bindings.cpp io_state_stream.cpp bin_app.cpp constants.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp diff --git a/src/library/constants.cpp b/src/library/constants.cpp new file mode 100644 index 000000000..7b544c7e5 --- /dev/null +++ b/src/library/constants.cpp @@ -0,0 +1,434 @@ +// Copyright (c) 2015 Microsoft Corporation. All rights reserved. +// Released under Apache 2.0 license as described in the file LICENSE. +// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py +#include "util/name.h" +namespace lean{ +name const * g_absurd = nullptr; +name const * g_and = nullptr; +name const * g_and_elim_left = nullptr; +name const * g_and_elim_right = nullptr; +name const * g_and_intro = nullptr; +name const * g_bool = nullptr; +name const * g_bool_ff = nullptr; +name const * g_bool_tt = nullptr; +name const * g_char = nullptr; +name const * g_char_mk = nullptr; +name const * g_dite = nullptr; +name const * g_eq = nullptr; +name const * g_eq_rec = nullptr; +name const * g_eq_rec_eq = nullptr; +name const * g_eq_refl = nullptr; +name const * g_eq_symm = nullptr; +name const * g_eq_trans = nullptr; +name const * g_exists_elim = nullptr; +name const * g_false = nullptr; +name const * g_heq = nullptr; +name const * g_heq_refl = nullptr; +name const * g_heq_to_eq = nullptr; +name const * g_ite = nullptr; +name const * g_lift = nullptr; +name const * g_lift_down = nullptr; +name const * g_lift_up = nullptr; +name const * g_nat = nullptr; +name const * g_nat_of_num = nullptr; +name const * g_nat_succ = nullptr; +name const * g_nat_zero = nullptr; +name const * g_not = nullptr; +name const * g_num = nullptr; +name const * g_num_zero = nullptr; +name const * g_num_pos = nullptr; +name const * g_or = nullptr; +name const * g_or_elim = nullptr; +name const * g_or_intro_left = nullptr; +name const * g_or_intro_right = nullptr; +name const * g_pos_num = nullptr; +name const * g_pos_num_one = nullptr; +name const * g_pos_num_bit0 = nullptr; +name const * g_pos_num_bit1 = nullptr; +name const * g_prod = nullptr; +name const * g_prod_mk = nullptr; +name const * g_prod_pr1 = nullptr; +name const * g_prod_pr2 = nullptr; +name const * g_sigma = nullptr; +name const * g_sigma_mk = nullptr; +name const * g_string = nullptr; +name const * g_string_empty = nullptr; +name const * g_string_str = nullptr; +name const * g_tactic = nullptr; +name const * g_tactic_apply = nullptr; +name const * g_tactic_assert_hypothesis = nullptr; +name const * g_tactic_fapply = nullptr; +name const * g_tactic_rapply = nullptr; +name const * g_tactic_eassumption = nullptr; +name const * g_tactic_and_then = nullptr; +name const * g_tactic_append = nullptr; +name const * g_tactic_assumption = nullptr; +name const * g_tactic_at_most = nullptr; +name const * g_tactic_beta = nullptr; +name const * g_tactic_builtin = nullptr; +name const * g_tactic_clear = nullptr; +name const * g_tactic_clear_lst = nullptr; +name const * g_tactic_determ = nullptr; +name const * g_tactic_discard = nullptr; +name const * g_tactic_intro = nullptr; +name const * g_tactic_intro_lst = nullptr; +name const * g_tactic_inversion = nullptr; +name const * g_tactic_inversion_with = nullptr; +name const * g_tactic_exact = nullptr; +name const * g_tactic_expr = nullptr; +name const * g_tactic_expr_builtin = nullptr; +name const * g_tactic_expr_list = nullptr; +name const * g_tactic_expr_list_cons = nullptr; +name const * g_tactic_expr_list_nil = nullptr; +name const * g_tactic_fail = nullptr; +name const * g_tactic_fixpoint = nullptr; +name const * g_tactic_focus_at = nullptr; +name const * g_tactic_generalize = nullptr; +name const * g_tactic_generalize_lst = nullptr; +name const * g_tactic_id = nullptr; +name const * g_tactic_interleave = nullptr; +name const * g_tactic_now = nullptr; +name const * g_tactic_or_else = nullptr; +name const * g_tactic_par = nullptr; +name const * g_tactic_state = nullptr; +name const * g_tactic_rename = nullptr; +name const * g_tactic_repeat = nullptr; +name const * g_tactic_revert = nullptr; +name const * g_tactic_revert_lst = nullptr; +name const * g_tactic_rotate_left = nullptr; +name const * g_tactic_rotate_right = nullptr; +name const * g_tactic_trace = nullptr; +name const * g_tactic_try_for = nullptr; +name const * g_tactic_unfold = nullptr; +name const * g_tactic_whnf = nullptr; +name const * g_true = nullptr; +name const * g_true_intro = nullptr; +name const * g_truncation = nullptr; +name const * g_truncation_is_trunc = nullptr; +name const * g_truncation_nat_to_trunc_index = nullptr; +name const * g_unit = nullptr; +name const * g_unit_star = nullptr; +name const * g_well_founded = nullptr; +void initialize_constants() { + g_absurd = new name{"absurd"}; + g_and = new name{"and"}; + g_and_elim_left = new name{"and", "elim_left"}; + g_and_elim_right = new name{"and", "elim_right"}; + g_and_intro = new name{"and", "intro"}; + g_bool = new name{"bool"}; + g_bool_ff = new name{"bool", "ff"}; + g_bool_tt = new name{"bool", "tt"}; + g_char = new name{"char"}; + g_char_mk = new name{"char", "mk"}; + g_dite = new name{"dite"}; + g_eq = new name{"eq"}; + g_eq_rec = new name{"eq", "rec"}; + g_eq_rec_eq = new name{"eq_rec_eq"}; + g_eq_refl = new name{"eq", "refl"}; + g_eq_symm = new name{"eq", "symm"}; + g_eq_trans = new name{"eq", "trans"}; + g_exists_elim = new name{"exists", "elim"}; + g_false = new name{"false"}; + g_heq = new name{"heq"}; + g_heq_refl = new name{"heq", "refl"}; + g_heq_to_eq = new name{"heq", "to_eq"}; + g_ite = new name{"ite"}; + g_lift = new name{"lift"}; + g_lift_down = new name{"lift", "down"}; + g_lift_up = new name{"lift", "up"}; + g_nat = new name{"nat"}; + g_nat_of_num = new name{"nat", "of_num"}; + g_nat_succ = new name{"nat", "succ"}; + g_nat_zero = new name{"nat", "zero"}; + g_not = new name{"not"}; + g_num = new name{"num"}; + g_num_zero = new name{"num", "zero"}; + g_num_pos = new name{"num", "pos"}; + g_or = new name{"or"}; + g_or_elim = new name{"or", "elim"}; + g_or_intro_left = new name{"or", "intro_left"}; + g_or_intro_right = new name{"or", "intro_right"}; + g_pos_num = new name{"pos_num"}; + g_pos_num_one = new name{"pos_num", "one"}; + g_pos_num_bit0 = new name{"pos_num", "bit0"}; + g_pos_num_bit1 = new name{"pos_num", "bit1"}; + g_prod = new name{"prod"}; + g_prod_mk = new name{"prod", "mk"}; + g_prod_pr1 = new name{"prod", "pr1"}; + g_prod_pr2 = new name{"prod", "pr2"}; + g_sigma = new name{"sigma"}; + g_sigma_mk = new name{"sigma", "mk"}; + g_string = new name{"string"}; + g_string_empty = new name{"string", "empty"}; + g_string_str = new name{"string", "str"}; + g_tactic = new name{"tactic"}; + g_tactic_apply = new name{"tactic", "apply"}; + g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"}; + g_tactic_fapply = new name{"tactic", "fapply"}; + g_tactic_rapply = new name{"tactic", "rapply"}; + g_tactic_eassumption = new name{"tactic", "eassumption"}; + g_tactic_and_then = new name{"tactic", "and_then"}; + g_tactic_append = new name{"tactic", "append"}; + g_tactic_assumption = new name{"tactic", "assumption"}; + g_tactic_at_most = new name{"tactic", "at_most"}; + g_tactic_beta = new name{"tactic", "beta"}; + g_tactic_builtin = new name{"tactic", "builtin"}; + g_tactic_clear = new name{"tactic", "clear"}; + g_tactic_clear_lst = new name{"tactic", "clear_lst"}; + g_tactic_determ = new name{"tactic", "determ"}; + g_tactic_discard = new name{"tactic", "discard"}; + g_tactic_intro = new name{"tactic", "intro"}; + g_tactic_intro_lst = new name{"tactic", "intro_lst"}; + g_tactic_inversion = new name{"tactic", "inversion"}; + g_tactic_inversion_with = new name{"tactic", "inversion_with"}; + g_tactic_exact = new name{"tactic", "exact"}; + g_tactic_expr = new name{"tactic", "expr"}; + g_tactic_expr_builtin = new name{"tactic", "expr", "builtin"}; + g_tactic_expr_list = new name{"tactic", "expr_list"}; + g_tactic_expr_list_cons = new name{"tactic", "expr_list", "cons"}; + g_tactic_expr_list_nil = new name{"tactic", "expr_list", "nil"}; + g_tactic_fail = new name{"tactic", "fail"}; + g_tactic_fixpoint = new name{"tactic", "fixpoint"}; + g_tactic_focus_at = new name{"tactic", "focus_at"}; + g_tactic_generalize = new name{"tactic", "generalize"}; + g_tactic_generalize_lst = new name{"tactic", "generalize_lst"}; + g_tactic_id = new name{"tactic", "id"}; + g_tactic_interleave = new name{"tactic", "interleave"}; + g_tactic_now = new name{"tactic", "now"}; + g_tactic_or_else = new name{"tactic", "or_else"}; + g_tactic_par = new name{"tactic", "par"}; + g_tactic_state = new name{"tactic", "state"}; + g_tactic_rename = new name{"tactic", "rename"}; + g_tactic_repeat = new name{"tactic", "repeat"}; + g_tactic_revert = new name{"tactic", "revert"}; + g_tactic_revert_lst = new name{"tactic", "revert_lst"}; + g_tactic_rotate_left = new name{"tactic", "rotate_left"}; + g_tactic_rotate_right = new name{"tactic", "rotate_right"}; + g_tactic_trace = new name{"tactic", "trace"}; + g_tactic_try_for = new name{"tactic", "try_for"}; + g_tactic_unfold = new name{"tactic", "unfold"}; + g_tactic_whnf = new name{"tactic", "whnf"}; + g_true = new name{"true"}; + g_true_intro = new name{"true", "intro"}; + g_truncation = new name{"truncation"}; + g_truncation_is_trunc = new name{"truncation", "is_trunc"}; + g_truncation_nat_to_trunc_index = new name{"truncation", "nat_to_trunc_index"}; + g_unit = new name{"unit"}; + g_unit_star = new name{"unit", "star"}; + g_well_founded = new name{"well_founded"}; +} +void finalize_constants() { + delete g_absurd; + delete g_and; + delete g_and_elim_left; + delete g_and_elim_right; + delete g_and_intro; + delete g_bool; + delete g_bool_ff; + delete g_bool_tt; + delete g_char; + delete g_char_mk; + delete g_dite; + delete g_eq; + delete g_eq_rec; + delete g_eq_rec_eq; + delete g_eq_refl; + delete g_eq_symm; + delete g_eq_trans; + delete g_exists_elim; + delete g_false; + delete g_heq; + delete g_heq_refl; + delete g_heq_to_eq; + delete g_ite; + delete g_lift; + delete g_lift_down; + delete g_lift_up; + delete g_nat; + delete g_nat_of_num; + delete g_nat_succ; + delete g_nat_zero; + delete g_not; + delete g_num; + delete g_num_zero; + delete g_num_pos; + delete g_or; + delete g_or_elim; + delete g_or_intro_left; + delete g_or_intro_right; + delete g_pos_num; + delete g_pos_num_one; + delete g_pos_num_bit0; + delete g_pos_num_bit1; + delete g_prod; + delete g_prod_mk; + delete g_prod_pr1; + delete g_prod_pr2; + delete g_sigma; + delete g_sigma_mk; + delete g_string; + delete g_string_empty; + delete g_string_str; + delete g_tactic; + delete g_tactic_apply; + delete g_tactic_assert_hypothesis; + delete g_tactic_fapply; + delete g_tactic_rapply; + delete g_tactic_eassumption; + delete g_tactic_and_then; + delete g_tactic_append; + delete g_tactic_assumption; + delete g_tactic_at_most; + delete g_tactic_beta; + delete g_tactic_builtin; + delete g_tactic_clear; + delete g_tactic_clear_lst; + delete g_tactic_determ; + delete g_tactic_discard; + delete g_tactic_intro; + delete g_tactic_intro_lst; + delete g_tactic_inversion; + delete g_tactic_inversion_with; + delete g_tactic_exact; + delete g_tactic_expr; + delete g_tactic_expr_builtin; + delete g_tactic_expr_list; + delete g_tactic_expr_list_cons; + delete g_tactic_expr_list_nil; + delete g_tactic_fail; + delete g_tactic_fixpoint; + delete g_tactic_focus_at; + delete g_tactic_generalize; + delete g_tactic_generalize_lst; + delete g_tactic_id; + delete g_tactic_interleave; + delete g_tactic_now; + delete g_tactic_or_else; + delete g_tactic_par; + delete g_tactic_state; + delete g_tactic_rename; + delete g_tactic_repeat; + delete g_tactic_revert; + delete g_tactic_revert_lst; + delete g_tactic_rotate_left; + delete g_tactic_rotate_right; + delete g_tactic_trace; + delete g_tactic_try_for; + delete g_tactic_unfold; + delete g_tactic_whnf; + delete g_true; + delete g_true_intro; + delete g_truncation; + delete g_truncation_is_trunc; + delete g_truncation_nat_to_trunc_index; + delete g_unit; + delete g_unit_star; + delete g_well_founded; +} +name const & get_absurd_name() { return *g_absurd; } +name const & get_and_name() { return *g_and; } +name const & get_and_elim_left_name() { return *g_and_elim_left; } +name const & get_and_elim_right_name() { return *g_and_elim_right; } +name const & get_and_intro_name() { return *g_and_intro; } +name const & get_bool_name() { return *g_bool; } +name const & get_bool_ff_name() { return *g_bool_ff; } +name const & get_bool_tt_name() { return *g_bool_tt; } +name const & get_char_name() { return *g_char; } +name const & get_char_mk_name() { return *g_char_mk; } +name const & get_dite_name() { return *g_dite; } +name const & get_eq_name() { return *g_eq; } +name const & get_eq_rec_name() { return *g_eq_rec; } +name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; } +name const & get_eq_refl_name() { return *g_eq_refl; } +name const & get_eq_symm_name() { return *g_eq_symm; } +name const & get_eq_trans_name() { return *g_eq_trans; } +name const & get_exists_elim_name() { return *g_exists_elim; } +name const & get_false_name() { return *g_false; } +name const & get_heq_name() { return *g_heq; } +name const & get_heq_refl_name() { return *g_heq_refl; } +name const & get_heq_to_eq_name() { return *g_heq_to_eq; } +name const & get_ite_name() { return *g_ite; } +name const & get_lift_name() { return *g_lift; } +name const & get_lift_down_name() { return *g_lift_down; } +name const & get_lift_up_name() { return *g_lift_up; } +name const & get_nat_name() { return *g_nat; } +name const & get_nat_of_num_name() { return *g_nat_of_num; } +name const & get_nat_succ_name() { return *g_nat_succ; } +name const & get_nat_zero_name() { return *g_nat_zero; } +name const & get_not_name() { return *g_not; } +name const & get_num_name() { return *g_num; } +name const & get_num_zero_name() { return *g_num_zero; } +name const & get_num_pos_name() { return *g_num_pos; } +name const & get_or_name() { return *g_or; } +name const & get_or_elim_name() { return *g_or_elim; } +name const & get_or_intro_left_name() { return *g_or_intro_left; } +name const & get_or_intro_right_name() { return *g_or_intro_right; } +name const & get_pos_num_name() { return *g_pos_num; } +name const & get_pos_num_one_name() { return *g_pos_num_one; } +name const & get_pos_num_bit0_name() { return *g_pos_num_bit0; } +name const & get_pos_num_bit1_name() { return *g_pos_num_bit1; } +name const & get_prod_name() { return *g_prod; } +name const & get_prod_mk_name() { return *g_prod_mk; } +name const & get_prod_pr1_name() { return *g_prod_pr1; } +name const & get_prod_pr2_name() { return *g_prod_pr2; } +name const & get_sigma_name() { return *g_sigma; } +name const & get_sigma_mk_name() { return *g_sigma_mk; } +name const & get_string_name() { return *g_string; } +name const & get_string_empty_name() { return *g_string_empty; } +name const & get_string_str_name() { return *g_string_str; } +name const & get_tactic_name() { return *g_tactic; } +name const & get_tactic_apply_name() { return *g_tactic_apply; } +name const & get_tactic_assert_hypothesis_name() { return *g_tactic_assert_hypothesis; } +name const & get_tactic_fapply_name() { return *g_tactic_fapply; } +name const & get_tactic_rapply_name() { return *g_tactic_rapply; } +name const & get_tactic_eassumption_name() { return *g_tactic_eassumption; } +name const & get_tactic_and_then_name() { return *g_tactic_and_then; } +name const & get_tactic_append_name() { return *g_tactic_append; } +name const & get_tactic_assumption_name() { return *g_tactic_assumption; } +name const & get_tactic_at_most_name() { return *g_tactic_at_most; } +name const & get_tactic_beta_name() { return *g_tactic_beta; } +name const & get_tactic_builtin_name() { return *g_tactic_builtin; } +name const & get_tactic_clear_name() { return *g_tactic_clear; } +name const & get_tactic_clear_lst_name() { return *g_tactic_clear_lst; } +name const & get_tactic_determ_name() { return *g_tactic_determ; } +name const & get_tactic_discard_name() { return *g_tactic_discard; } +name const & get_tactic_intro_name() { return *g_tactic_intro; } +name const & get_tactic_intro_lst_name() { return *g_tactic_intro_lst; } +name const & get_tactic_inversion_name() { return *g_tactic_inversion; } +name const & get_tactic_inversion_with_name() { return *g_tactic_inversion_with; } +name const & get_tactic_exact_name() { return *g_tactic_exact; } +name const & get_tactic_expr_name() { return *g_tactic_expr; } +name const & get_tactic_expr_builtin_name() { return *g_tactic_expr_builtin; } +name const & get_tactic_expr_list_name() { return *g_tactic_expr_list; } +name const & get_tactic_expr_list_cons_name() { return *g_tactic_expr_list_cons; } +name const & get_tactic_expr_list_nil_name() { return *g_tactic_expr_list_nil; } +name const & get_tactic_fail_name() { return *g_tactic_fail; } +name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; } +name const & get_tactic_focus_at_name() { return *g_tactic_focus_at; } +name const & get_tactic_generalize_name() { return *g_tactic_generalize; } +name const & get_tactic_generalize_lst_name() { return *g_tactic_generalize_lst; } +name const & get_tactic_id_name() { return *g_tactic_id; } +name const & get_tactic_interleave_name() { return *g_tactic_interleave; } +name const & get_tactic_now_name() { return *g_tactic_now; } +name const & get_tactic_or_else_name() { return *g_tactic_or_else; } +name const & get_tactic_par_name() { return *g_tactic_par; } +name const & get_tactic_state_name() { return *g_tactic_state; } +name const & get_tactic_rename_name() { return *g_tactic_rename; } +name const & get_tactic_repeat_name() { return *g_tactic_repeat; } +name const & get_tactic_revert_name() { return *g_tactic_revert; } +name const & get_tactic_revert_lst_name() { return *g_tactic_revert_lst; } +name const & get_tactic_rotate_left_name() { return *g_tactic_rotate_left; } +name const & get_tactic_rotate_right_name() { return *g_tactic_rotate_right; } +name const & get_tactic_trace_name() { return *g_tactic_trace; } +name const & get_tactic_try_for_name() { return *g_tactic_try_for; } +name const & get_tactic_unfold_name() { return *g_tactic_unfold; } +name const & get_tactic_whnf_name() { return *g_tactic_whnf; } +name const & get_true_name() { return *g_true; } +name const & get_true_intro_name() { return *g_true_intro; } +name const & get_truncation_name() { return *g_truncation; } +name const & get_truncation_is_trunc_name() { return *g_truncation_is_trunc; } +name const & get_truncation_nat_to_trunc_index_name() { return *g_truncation_nat_to_trunc_index; } +name const & get_unit_name() { return *g_unit; } +name const & get_unit_star_name() { return *g_unit_star; } +name const & get_well_founded_name() { return *g_well_founded; } +} diff --git a/src/library/constants.h b/src/library/constants.h new file mode 100644 index 000000000..c086a469c --- /dev/null +++ b/src/library/constants.h @@ -0,0 +1,114 @@ +// Copyright (c) 2015 Microsoft Corporation. All rights reserved. +// Released under Apache 2.0 license as described in the file LICENSE. +// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py +#include "util/name.h" +namespace lean { +void initialize_constants(); +void finalize_constants(); +name const & get_absurd_name(); +name const & get_and_name(); +name const & get_and_elim_left_name(); +name const & get_and_elim_right_name(); +name const & get_and_intro_name(); +name const & get_bool_name(); +name const & get_bool_ff_name(); +name const & get_bool_tt_name(); +name const & get_char_name(); +name const & get_char_mk_name(); +name const & get_dite_name(); +name const & get_eq_name(); +name const & get_eq_rec_name(); +name const & get_eq_rec_eq_name(); +name const & get_eq_refl_name(); +name const & get_eq_symm_name(); +name const & get_eq_trans_name(); +name const & get_exists_elim_name(); +name const & get_false_name(); +name const & get_heq_name(); +name const & get_heq_refl_name(); +name const & get_heq_to_eq_name(); +name const & get_ite_name(); +name const & get_lift_name(); +name const & get_lift_down_name(); +name const & get_lift_up_name(); +name const & get_nat_name(); +name const & get_nat_of_num_name(); +name const & get_nat_succ_name(); +name const & get_nat_zero_name(); +name const & get_not_name(); +name const & get_num_name(); +name const & get_num_zero_name(); +name const & get_num_pos_name(); +name const & get_or_name(); +name const & get_or_elim_name(); +name const & get_or_intro_left_name(); +name const & get_or_intro_right_name(); +name const & get_pos_num_name(); +name const & get_pos_num_one_name(); +name const & get_pos_num_bit0_name(); +name const & get_pos_num_bit1_name(); +name const & get_prod_name(); +name const & get_prod_mk_name(); +name const & get_prod_pr1_name(); +name const & get_prod_pr2_name(); +name const & get_sigma_name(); +name const & get_sigma_mk_name(); +name const & get_string_name(); +name const & get_string_empty_name(); +name const & get_string_str_name(); +name const & get_tactic_name(); +name const & get_tactic_apply_name(); +name const & get_tactic_assert_hypothesis_name(); +name const & get_tactic_fapply_name(); +name const & get_tactic_rapply_name(); +name const & get_tactic_eassumption_name(); +name const & get_tactic_and_then_name(); +name const & get_tactic_append_name(); +name const & get_tactic_assumption_name(); +name const & get_tactic_at_most_name(); +name const & get_tactic_beta_name(); +name const & get_tactic_builtin_name(); +name const & get_tactic_clear_name(); +name const & get_tactic_clear_lst_name(); +name const & get_tactic_determ_name(); +name const & get_tactic_discard_name(); +name const & get_tactic_intro_name(); +name const & get_tactic_intro_lst_name(); +name const & get_tactic_inversion_name(); +name const & get_tactic_inversion_with_name(); +name const & get_tactic_exact_name(); +name const & get_tactic_expr_name(); +name const & get_tactic_expr_builtin_name(); +name const & get_tactic_expr_list_name(); +name const & get_tactic_expr_list_cons_name(); +name const & get_tactic_expr_list_nil_name(); +name const & get_tactic_fail_name(); +name const & get_tactic_fixpoint_name(); +name const & get_tactic_focus_at_name(); +name const & get_tactic_generalize_name(); +name const & get_tactic_generalize_lst_name(); +name const & get_tactic_id_name(); +name const & get_tactic_interleave_name(); +name const & get_tactic_now_name(); +name const & get_tactic_or_else_name(); +name const & get_tactic_par_name(); +name const & get_tactic_state_name(); +name const & get_tactic_rename_name(); +name const & get_tactic_repeat_name(); +name const & get_tactic_revert_name(); +name const & get_tactic_revert_lst_name(); +name const & get_tactic_rotate_left_name(); +name const & get_tactic_rotate_right_name(); +name const & get_tactic_trace_name(); +name const & get_tactic_try_for_name(); +name const & get_tactic_unfold_name(); +name const & get_tactic_whnf_name(); +name const & get_true_name(); +name const & get_true_intro_name(); +name const & get_truncation_name(); +name const & get_truncation_is_trunc_name(); +name const & get_truncation_nat_to_trunc_index_name(); +name const & get_unit_name(); +name const & get_unit_star_name(); +name const & get_well_founded_name(); +} diff --git a/src/library/constants.txt b/src/library/constants.txt new file mode 100644 index 000000000..e681e3418 --- /dev/null +++ b/src/library/constants.txt @@ -0,0 +1,106 @@ +absurd +and +and.elim_left +and.elim_right +and.intro +bool +bool.ff +bool.tt +char +char.mk +dite +eq +eq.rec +eq_rec_eq +eq.refl +eq.symm +eq.trans +exists.elim +false +heq +heq.refl +heq.to_eq +ite +lift +lift.down +lift.up +nat +nat.of_num +nat.succ +nat.zero +not +num +num.zero +num.pos +or +or.elim +or.intro_left +or.intro_right +pos_num +pos_num.one +pos_num.bit0 +pos_num.bit1 +prod +prod.mk +prod.pr1 +prod.pr2 +sigma +sigma.mk +string +string.empty +string.str +tactic +tactic.apply +tactic.assert_hypothesis +tactic.fapply +tactic.rapply +tactic.eassumption +tactic.and_then +tactic.append +tactic.assumption +tactic.at_most +tactic.beta +tactic.builtin +tactic.clear +tactic.clear_lst +tactic.determ +tactic.discard +tactic.intro +tactic.intro_lst +tactic.inversion +tactic.inversion_with +tactic.exact +tactic.expr +tactic.expr.builtin +tactic.expr_list +tactic.expr_list.cons +tactic.expr_list.nil +tactic.fail +tactic.fixpoint +tactic.focus_at +tactic.generalize +tactic.generalize_lst +tactic.id +tactic.interleave +tactic.now +tactic.or_else +tactic.par +tactic.state +tactic.rename +tactic.repeat +tactic.revert +tactic.revert_lst +tactic.rotate_left +tactic.rotate_right +tactic.trace +tactic.try_for +tactic.unfold +tactic.whnf +true +true.intro +truncation +truncation.is_trunc +truncation.nat_to_trunc_index +unit +unit.star +well_founded diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index a80400f6b..6ecf5b657 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/protected.h" #include "library/reducible.h" +#include "library/constants.h" namespace lean { static void throw_corrupted(name const & n) { @@ -81,8 +82,8 @@ environment mk_cases_on(environment const & env, name const & n) { optional star; // we use unit if num_types > 1 if (num_types > 1) { - unit = mk_constant(name("unit"), to_list(elim_univ)); - star = mk_constant(name({"unit", "star"}), to_list(elim_univ)); + unit = mk_constant(get_unit_name(), to_list(elim_univ)); + star = mk_constant(get_unit_star_name(), to_list(elim_univ)); } // rec_params order diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index 1616a97f0..1984ce2c0 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/annotation.h" #include "library/util.h" #include "library/locals.h" +#include "library/constants.h" #include "library/normalize.h" #include "library/pp_options.h" #include "library/tactic/inversion_tactic.h" @@ -1210,14 +1211,14 @@ class equation_compiler_fn { */ optional to_below(expr const & d, expr const & a, expr const & b) { expr const & fn = get_app_fn(d); - if (is_constant(fn) && const_name(fn) == "prod") { + if (is_constant(fn) && const_name(fn) == get_prod_name()) { if (auto r = to_below(app_arg(app_fn(d)), a, mk_pr1(m_main.m_tc, b))) return r; else if (auto r = to_below(app_arg(d), a, mk_pr2(m_main.m_tc, b))) return r; else return none_expr(); - } else if (is_constant(fn) && const_name(fn) == "and") { + } else if (is_constant(fn) && const_name(fn) == get_and_name()) { // For ibelow, we use "and" instead of products if (auto r = to_below(app_arg(app_fn(d)), a, mk_and_elim_left(m_main.m_tc, b))) return r; @@ -1523,7 +1524,7 @@ class equation_compiler_fn { C = Fun(C_args, type); } else { expr d = binding_domain(C_type); - expr unit = mk_constant("unit", rlvl); + expr unit = mk_constant(get_unit_name(), rlvl); to_telescope_ext(d, C_args); C = Fun(C_args, unit); } @@ -1566,7 +1567,7 @@ class equation_compiler_fn { new_ctx.append(rest); F = compile_pat_match(program(prg_i, to_list(new_ctx)), *p_idx); } else { - expr star = mk_constant(name{"unit", "star"}, rlvl); + expr star = mk_constant(get_unit_star_name(), rlvl); buffer F_args; F_args.append(C_args); below = mk_app(below, F_args); diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index 72c7bc51f..7412a2c2c 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/util.h" #include "library/reducible.h" +#include "library/constants.h" namespace lean { static void throw_corrupted(name const & n) { @@ -43,8 +44,6 @@ optional mk_no_confusion_type(environment const & env, name const & rlvl = mk_max(plvl, ind_lvl); if (length(ilvls) != length(ind_decl.get_univ_params())) return optional(); // type does not have only a restricted eliminator - name eq_name("eq"); - name heq_name("heq"); // All inductive datatype parameters and indices are arguments buffer args; ind_type = to_telescope(ngen, ind_type, args, some(mk_implicit_binder_info())); @@ -67,7 +66,7 @@ optional mk_no_confusion_type(environment const & env, name const & if (impredicative) Pres = P; else - Pres = mk_app(mk_constant("lift", {plvl, ind_lvl}), P); + Pres = mk_app(mk_constant(get_lift_name(), {plvl, ind_lvl}), P); name no_confusion_type_name{n, "no_confusion_type"}; expr no_confusion_type_type = Pi(args, R); // Create type former @@ -114,9 +113,9 @@ optional mk_no_confusion_type(environment const & env, name const & level l = sort_level(tc.ensure_type(lhs_type).first); expr h_type; if (tc.is_def_eq(lhs_type, rhs_type).first) { - h_type = mk_app(mk_constant(eq_name, to_list(l)), lhs_type, lhs, rhs); + h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs); } else { - h_type = mk_app(mk_constant(heq_name, to_list(l)), lhs_type, lhs, rhs_type, rhs); + h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs); } rtype_hyp.push_back(mk_local(ngen.next(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); } @@ -162,10 +161,6 @@ environment mk_no_confusion(environment const & env, name const & n) { expr ind_type = instantiate_type_univ_params(ind_decl, tail(ls)); level ind_lvl = get_datatype_level(ind_type); expr no_confusion_type_type = instantiate_type_univ_params(no_confusion_type_decl, ls); - name eq_name("eq"); - name heq_name("heq"); - name eq_refl_name{"eq", "refl"}; - name heq_refl_name{"heq", "refl"}; buffer args; expr type = no_confusion_type_type; type = to_telescope(ngen, type, args, some(mk_implicit_binder_info())); @@ -178,12 +173,12 @@ environment mk_no_confusion(environment const & env, name const & n) { expr v_type = mlocal_type(v1); expr lift_up; if (!impredicative) { - lift_up = mk_app(mk_constant(name{"lift", "up"}, {head(ls), ind_lvl}), P); + lift_up = mk_app(mk_constant(get_lift_up_name(), {head(ls), ind_lvl}), P); } level v_lvl = sort_level(tc.ensure_type(v_type).first); - expr eq_v = mk_app(mk_constant(eq_name, to_list(v_lvl)), v_type); + expr eq_v = mk_app(mk_constant(get_eq_name(), to_list(v_lvl)), v_type); expr H12 = mk_local(ngen.next(), "H12", mk_app(eq_v, v1, v2), binder_info()); - lean_assert(impredicative != inductive::has_dep_elim(env, eq_name)); + lean_assert(impredicative != inductive::has_dep_elim(env, get_eq_name())); args.push_back(H12); name no_confusion_name{n, "no_confusion"}; expr no_confusion_ty = Pi(args, range); @@ -229,10 +224,10 @@ environment mk_no_confusion(environment const & env, name const & n) { while (is_pi(Ht)) { buffer eq_args; expr eq_fn = get_app_args(binding_domain(Ht), eq_args); - if (const_name(eq_fn) == eq_name) { - refl_args.push_back(mk_app(mk_constant(eq_refl_name, const_levels(eq_fn)), eq_args[0], eq_args[2])); + if (const_name(eq_fn) == get_eq_name()) { + refl_args.push_back(mk_app(mk_constant(get_eq_refl_name(), const_levels(eq_fn)), eq_args[0], eq_args[2])); } else { - refl_args.push_back(mk_app(mk_constant(heq_refl_name, const_levels(eq_fn)), eq_args[0], eq_args[1])); + refl_args.push_back(mk_app(mk_constant(get_heq_refl_name(), const_levels(eq_fn)), eq_args[0], eq_args[1])); } Ht = binding_body(Ht); } @@ -249,13 +244,12 @@ environment mk_no_confusion(environment const & env, name const & n) { // // eq.rec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12 // - name eq_rec_name{"eq", "rec"}; level eq_rec_l1; if (impredicative) eq_rec_l1 = head(ls); else eq_rec_l1 = mk_max(head(ls), ind_lvl); - expr eq_rec = mk_app(mk_constant(eq_rec_name, {eq_rec_l1, v_lvl}), v_type, v1); + expr eq_rec = mk_app(mk_constant(get_eq_rec_name(), {eq_rec_l1, v_lvl}), v_type, v1); // create eq_rec type_former // (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) expr a = mk_local(ngen.next(), "a", v_type, binder_info()); diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 67393561b..699ceff61 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "library/unifier.h" #include "library/kernel_serializer.h" #include "library/let.h" @@ -35,6 +36,7 @@ Author: Leonardo de Moura namespace lean { void initialize_library_module() { + initialize_constants(); initialize_fingerprint(); initialize_print(); initialize_placeholder(); @@ -94,5 +96,6 @@ void finalize_library_module() { finalize_placeholder(); finalize_print(); finalize_fingerprint(); + finalize_constants(); } } diff --git a/src/library/num.cpp b/src/library/num.cpp index 8de6ab82a..caf9e08f5 100644 --- a/src/library/num.cpp +++ b/src/library/num.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/type_checker.h" #include "library/num.h" +#include "library/constants.h" namespace lean { static expr * g_num = nullptr; @@ -17,13 +18,13 @@ static expr * g_bit0 = nullptr; static expr * g_bit1 = nullptr; void initialize_num() { - g_num = new expr(Const("num")); - g_pos_num = new expr(Const("pos_num")); - g_zero = new expr(Const({"num", "zero"})); - g_pos = new expr(Const({"num", "pos"})); - g_one = new expr(Const({"pos_num", "one"})); - g_bit0 = new expr(Const({"pos_num", "bit0"})); - g_bit1 = new expr(Const({"pos_num", "bit1"})); + g_num = new expr(Const(get_num_name())); + g_pos_num = new expr(Const(get_pos_num_name())); + g_zero = new expr(Const(get_num_zero_name())); + g_pos = new expr(Const(get_num_pos_name())); + g_one = new expr(Const(get_pos_num_one_name())); + g_bit0 = new expr(Const(get_pos_num_bit0_name())); + g_bit1 = new expr(Const(get_pos_num_bit1_name())); } void finalize_num() { diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index 760f4f0e6..4dd3f7cff 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/kernel_serializer.h" #include "library/bin_app.h" +#include "library/constants.h" namespace lean { static name * g_resolve_macro_name = nullptr; @@ -315,13 +316,13 @@ expr mk_resolve_macro(expr const & l, expr const & H1, expr const & H2) { void initialize_resolve_macro() { g_resolve_macro_name = new name("resolve"); g_resolve_opcode = new std::string("Res"); - g_or = new expr(Const("or")); - g_not = new expr(Const("not")); - g_false = new expr(Const("false")); - g_or_elim = new expr(Const(name("or", "elim"))); - g_or_intro_left = new expr(Const(name("or", "intro_left"))); - g_or_intro_right = new expr(Const(name("or", "intro_right"))); - g_absurd_elim = new expr(Const("absurd_elim")); + g_or = new expr(Const(get_or_name())); + g_not = new expr(Const(get_not_name())); + g_false = new expr(Const(get_false_name())); + g_or_elim = new expr(Const(get_or_elim_name())); + g_or_intro_left = new expr(Const(get_or_intro_left_name())); + g_or_intro_right = new expr(Const(get_or_intro_right_name())); + g_absurd_elim = new expr(Const(get_absurd_name())); g_var_0 = new expr(mk_var(0)); g_resolve_macro_definition = new macro_definition(new resolve_macro_definition_cell()); register_macro_deserializer(*g_resolve_opcode, diff --git a/src/library/string.cpp b/src/library/string.cpp index 45ede9e9c..cbdbd6fcf 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/kernel_serializer.h" #include "library/string.h" +#include "library/constants.h" namespace lean { static name * g_string_macro = nullptr; @@ -90,14 +91,14 @@ string_macro const & to_string_macro(expr const & e) { void initialize_string() { g_string_macro = new name("string_macro"); g_string_opcode = new std::string("Str"); - g_bool = new expr(Const(name("bool"))); - g_ff = new expr(Const(name("bool", "ff"))); - g_tt = new expr(Const(name("bool", "tt"))); - g_char = new expr(Const(name("char"))); - g_ascii = new expr(Const(name("char", "mk"))); - g_string = new expr(Const(name("string"))); - g_empty = new expr(Const(name("string", "empty"))); - g_str = new expr(Const(name("string", "str"))); + g_bool = new expr(Const(get_bool_name())); + g_ff = new expr(Const(get_bool_ff_name())); + g_tt = new expr(Const(get_bool_tt_name())); + g_char = new expr(Const(get_char_name())); + g_ascii = new expr(Const(get_char_mk_name())); + g_string = new expr(Const(get_string_name())); + g_empty = new expr(Const(get_string_empty_name())); + g_str = new expr(Const(get_string_str_name())); register_macro_deserializer(*g_string_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index f3b8fca2c..bc111ecfd 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/unifier.h" #include "library/occurs.h" +#include "library/constants.h" #include "library/metavar_closure.h" #include "library/type_util.h" #include "library/tactic/expr_to_tactic.h" @@ -186,25 +187,25 @@ void open_apply_tactic(lua_State * L) { } void initialize_apply_tactic() { - register_tac(name({"tactic", "apply"}), + register_tac(get_tactic_apply_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument"); return apply_tactic(fn, get_tactic_expr_expr(app_arg(e))); }); - register_tac(name({"tactic", "rapply"}), + register_tac(get_tactic_rapply_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'rapply' tactic, invalid argument"); return rapply_tactic(fn, get_tactic_expr_expr(app_arg(e))); }); - register_tac(name({"tactic", "fapply"}), + register_tac(get_tactic_fapply_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument"); return fapply_tactic(fn, get_tactic_expr_expr(app_arg(e))); }); - register_simple_tac(name({"tactic", "eassumption"}), + register_simple_tac(get_tactic_eassumption_name(), []() { return eassumption_tactic(); }); } diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp index 9a44911a2..dffc19b68 100644 --- a/src/library/tactic/assert_tactic.cpp +++ b/src/library/tactic/assert_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/abstract.h" +#include "library/constants.h" #include "library/tactic/tactic.h" #include "library/tactic/elaborate.h" #include "library/tactic/expr_to_tactic.h" @@ -46,7 +47,7 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) } void initialize_assert_tactic() { - register_tac(name{"tactic", "assert_hypothesis"}, + register_tac(get_tactic_assert_hypothesis_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'assert' tactic, argument must be an identifier"); check_tactic_expr(app_arg(e), "invalid 'assert' tactic, argument must be an expression"); diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index 6ce3f7aa7..6c63808a0 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/generic_exception.h" #include "library/util.h" +#include "library/constants.h" #include "library/tactic/util.h" #include "library/tactic/class_instance_synth.h" @@ -472,10 +473,9 @@ optional mk_class_instance(environment const & env, io_state const & ios, } optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type) { - name is_trunc{"truncation", "is_trunc"}; - expr trunc_index = mk_app(mk_constant(name{"truncation", "nat_to_trunc_index"}), mk_constant(name{"nat", "zero"})); + expr trunc_index = mk_app(mk_constant(get_truncation_nat_to_trunc_index_name()), mk_constant(get_nat_zero_name())); level lvl = sort_level(tc.ensure_type(type).first); - expr is_hset = mk_app(mk_constant(name{"truncation", "is_trunc"}, {lvl}), trunc_index, type); + expr is_hset = mk_app(mk_constant(get_truncation_is_trunc_name(), {lvl}), trunc_index, type); return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), is_hset); } } diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index eea2dd417..ff37c0528 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "kernel/abstract.h" #include "library/locals.h" #include "library/tactic/tactic.h" @@ -42,12 +43,12 @@ tactic clear_tactic(name const & n) { } void initialize_clear_tactic() { - register_tac(name({"tactic", "clear"}), + register_tac(get_tactic_clear_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name n = tactic_expr_to_id(app_arg(e), "invalid 'clear' tactic, argument must be an identifier"); return clear_tactic(n); }); - register_tac(name({"tactic", "clear_lst"}), + register_tac(get_tactic_clear_lst_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected"); diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index e1972cb34..f7386c49e 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "kernel/type_checker.h" #include "library/tactic/tactic.h" #include "library/tactic/elaborate.h" @@ -34,7 +35,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) { static expr * g_exact_tac_fn = nullptr; expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } void initialize_exact_tactic() { - name exact_tac_name({"tactic", "exact"}); + name const & exact_tac_name = get_tactic_exact_name(); g_exact_tac_fn = new expr(Const(exact_tac_name)); register_tac(exact_tac_name, [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index eff033b1f..9fe08c177 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/annotation.h" #include "library/string.h" #include "library/num.h" +#include "library/constants.h" #include "library/kernel_serializer.h" #include "library/tactic/expr_to_tactic.h" @@ -65,16 +66,10 @@ expr const & get_tactic_expr_type() { return *g_tactic_expr_type; } expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; } expr const & get_tactic_expr_list_type() { return *g_tactic_expr_list_type; } -static name * g_tactic_expr_name = nullptr; static std::string * g_tactic_expr_opcode = nullptr; - -static name * g_tactic_name = nullptr; static std::string * g_tactic_opcode = nullptr; -name const & get_tactic_expr_name() { return *g_tactic_expr_name; } std::string const & get_tactic_expr_opcode() { return *g_tactic_expr_opcode; } - -name const & get_tactic_name() { return *g_tactic_name; } std::string const & get_tactic_opcode() { return *g_tactic_opcode; } class tactic_expr_macro_definition_cell : public macro_definition_cell { @@ -305,12 +300,9 @@ void initialize_expr_to_tactic() { g_map = new expr_to_tactic_map(); - g_tactic_name = new name("tactic"); - - g_tactic_expr_type = new expr(mk_constant(name(*g_tactic_name, "expr"))); - g_tactic_expr_builtin = new expr(mk_constant(name(const_name(*g_tactic_expr_type), "builtin"))); - g_tactic_expr_list_type = new expr(mk_constant(name(*g_tactic_name, "expr_list"))); - g_tactic_expr_name = new name("tactic-expr"); + g_tactic_expr_type = new expr(mk_constant(get_tactic_expr_name())); + g_tactic_expr_builtin = new expr(mk_constant(get_tactic_expr_builtin_name())); + g_tactic_expr_list_type = new expr(mk_constant(get_tactic_expr_list_name())); g_tactic_expr_opcode = new std::string("TACE"); g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); @@ -321,59 +313,52 @@ void initialize_expr_to_tactic() { return mk_tactic_expr(args[0]); }); - g_expr_list_cons = new expr(mk_constant(name({"tactic", "expr_list", "cons"}))); - g_expr_list_nil = new expr(mk_constant(name({"tactic", "expr_list", "nil"}))); + g_expr_list_cons = new expr(mk_constant(get_tactic_expr_list_cons_name())); + g_expr_list_nil = new expr(mk_constant(get_tactic_expr_list_nil_name())); - name builtin_tac_name(*g_tactic_name, "builtin"); - name and_then_tac_name(*g_tactic_name, "and_then"); - name or_else_tac_name(*g_tactic_name, "or_else"); - name repeat_tac_name(*g_tactic_name, "repeat"); - name fixpoint_name(*g_tactic_name, "fixpoint"); - name determ_tac_name(*g_tactic_name, "determ"); - name id_tac_name(*g_tactic_name, "id"); - g_and_then_tac_fn = new expr(Const(and_then_tac_name)); - g_or_else_tac_fn = new expr(Const(or_else_tac_name)); - g_id_tac_fn = new expr(Const(id_tac_name)); - g_repeat_tac_fn = new expr(Const(repeat_tac_name)); - g_determ_tac_fn = new expr(Const(determ_tac_name)); - g_tac_type = new expr(Const(*g_tactic_name)); - g_builtin_tac = new expr(Const(builtin_tac_name)); - g_fixpoint_tac = new expr(Const(fixpoint_name)); + g_and_then_tac_fn = new expr(Const(get_tactic_and_then_name())); + g_or_else_tac_fn = new expr(Const(get_tactic_or_else_name())); + g_id_tac_fn = new expr(Const(get_tactic_id_name())); + g_repeat_tac_fn = new expr(Const(get_tactic_repeat_name())); + g_determ_tac_fn = new expr(Const(get_tactic_determ_name())); + g_tac_type = new expr(Const(get_tactic_name())); + g_builtin_tac = new expr(Const(get_tactic_builtin_name())); + g_fixpoint_tac = new expr(Const(get_tactic_fixpoint_name())); - register_simple_tac(id_tac_name, + register_simple_tac(get_tactic_id_name(), []() { return id_tactic(); }); - register_simple_tac(name(*g_tactic_name, "now"), + register_simple_tac(get_tactic_now_name(), []() { return now_tactic(); }); - register_simple_tac(name(*g_tactic_name, "assumption"), + register_simple_tac(get_tactic_assumption_name(), []() { return assumption_tactic(); }); - register_simple_tac(name(*g_tactic_name, "fail"), + register_simple_tac(get_tactic_fail_name(), []() { return fail_tactic(); }); - register_simple_tac(name(*g_tactic_name, "beta"), + register_simple_tac(get_tactic_beta_name(), []() { return beta_tactic(); }); - register_bin_tac(and_then_tac_name, + register_bin_tac(get_tactic_and_then_name(), [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); - register_bin_tac(name(*g_tactic_name, "append"), + register_bin_tac(get_tactic_append_name(), [](tactic const & t1, tactic const & t2) { return append(t1, t2); }); - register_bin_tac(name(*g_tactic_name, "interleave"), + register_bin_tac(get_tactic_interleave_name(), [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); }); - register_bin_tac(name(*g_tactic_name, "par"), + register_bin_tac(get_tactic_par_name(), [](tactic const & t1, tactic const & t2) { return par(t1, t2); }); - register_bin_tac(or_else_tac_name, + register_bin_tac(get_tactic_or_else_name(), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); - register_unary_tac(repeat_tac_name, + register_unary_tac(get_tactic_repeat_name(), [](tactic const & t1) { return repeat(t1); }); - register_unary_num_tac(name(*g_tactic_name, "at_most"), + register_unary_num_tac(get_tactic_at_most_name(), [](tactic const & t, unsigned k) { return take(t, k); }); - register_unary_num_tac(name(*g_tactic_name, "discard"), + register_unary_num_tac(get_tactic_discard_name(), [](tactic const & t, unsigned k) { return discard(t, k); }); - register_unary_num_tac(name(*g_tactic_name, "focus_at"), + register_unary_num_tac(get_tactic_focus_at_name(), [](tactic const & t, unsigned k) { return focus(t, k); }); - register_unary_num_tac(name(*g_tactic_name, "try_for"), + register_unary_num_tac(get_tactic_try_for_name(), [](tactic const & t, unsigned k) { return try_for(t, k); }); - register_num_tac(name(*g_tactic_name, "rotate_left"), [](unsigned k) { return rotate_left(k); }); - register_num_tac(name(*g_tactic_name, "rotate_right"), [](unsigned k) { return rotate_right(k); }); + register_num_tac(get_tactic_rotate_left_name(), [](unsigned k) { return rotate_left(k); }); + register_num_tac(get_tactic_rotate_right_name(), [](unsigned k) { return rotate_right(k); }); - register_tac(fixpoint_name, + register_tac(get_tactic_fixpoint_name(), [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { if (!is_constant(app_fn(e))) throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument"); @@ -388,7 +373,6 @@ void finalize_expr_to_tactic() { delete g_tactic_expr_type; delete g_tactic_expr_builtin; delete g_tactic_expr_list_type; - delete g_tactic_expr_name; delete g_tactic_expr_opcode; delete g_tactic_expr_macro; delete g_fixpoint_tac; @@ -400,7 +384,6 @@ void finalize_expr_to_tactic() { delete g_and_then_tac_fn; delete g_id_tac_fn; delete g_map; - delete g_tactic_name; delete g_tactic_opcode; delete g_by_name; delete g_tmp_prefix; diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 3c1e3226b..ed4f685e0 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "kernel/abstract.h" #include "library/reducible.h" #include "library/tactic/elaborate.h" @@ -49,14 +50,14 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & } void initialize_generalize_tactic() { - register_tac(name({"tactic", "generalize"}), + register_tac(get_tactic_generalize_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'generalize' tactic, invalid argument"); // TODO(Leo): allow user to provide name to abstract variable return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x"); }); - register_tac(name({"tactic", "generalize_lst"}), + register_tac(get_tactic_generalize_lst_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { buffer args; get_tactic_expr_list_elements(app_arg(e), args, "invalid 'generalizes' tactic, list of expressions expected"); diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index 49b676d0c..c34dc449c 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/src/library/tactic/intros_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "kernel/instantiate.h" #include "library/reducible.h" #include "library/tactic/intros_tactic.h" @@ -57,12 +58,12 @@ tactic intros_tactic(list _ns, bool relax_main_opaque) { } void initialize_intros_tactic() { - register_tac(name({"tactic", "intro"}), + register_tac(get_tactic_intro_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name const & id = tactic_expr_to_id(app_arg(e), "invalid 'intro' tactic, argument must be an identifier"); return intros_tactic(to_list(id)); }); - register_tac(name({"tactic", "intro_lst"}), + register_tac(get_tactic_intro_lst_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers"); diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 449eb5f76..3c84eb6be 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/locals.h" #include "library/util.h" +#include "library/constants.h" #include "library/reducible.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -70,7 +71,7 @@ optional apply_eq_rec_eq(type_checker & tc, io_state const & ios, list args; expr const & heq_fn = get_app_args(eq, args); constraint_seq cs; if (m_tc.is_def_eq(args[0], args[2], justification(), cs) && !cs) { buffer hyps; g.get_hyps(hyps); - expr new_eq = mk_app(mk_constant("eq", const_levels(heq_fn)), args[0], args[1], args[3]); + expr new_eq = mk_app(mk_constant(get_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3]); expr new_hyp = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), new_eq, binder_info()); expr new_type = instantiate(binding_body(type), new_hyp); hyps.push_back(new_hyp); @@ -556,7 +557,7 @@ class inversion_tac { goal new_g(new_meta, new_type); hyps.pop_back(); expr H = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); - expr to_eq = mk_app(mk_constant({"heq", "to_eq"}, const_levels(heq_fn)), args[0], args[1], args[3], H); + expr to_eq = mk_app(mk_constant(get_heq_to_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H); expr val = g.abstract(Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq))); assign(g.get_name(), val); return new_g; @@ -573,7 +574,7 @@ class inversion_tac { */ goal intro_next_eq_simple(goal const & g, expr const & type) { expr eq = binding_domain(type); - lean_assert(const_name(get_app_fn(eq)) == "eq"); + lean_assert(const_name(get_app_fn(eq)) == get_eq_name()); buffer hyps; g.get_hyps(hyps); expr new_hyp = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); @@ -594,7 +595,7 @@ class inversion_tac { expr const & eq_fn = get_app_fn(eq); if (!is_constant(eq_fn)) throw_ill_formed_goal(); - if (const_name(eq_fn) == "eq") { + if (const_name(eq_fn) == get_eq_name()) { expr const & lhs = app_arg(app_fn(eq)); expr const & rhs = app_arg(eq); expr new_lhs = m_tc.whnf(lhs).first; @@ -608,7 +609,7 @@ class inversion_tac { } else { return intro_next_eq_simple(g, type); } - } else if (m_proof_irrel && const_name(eq_fn) == "heq") { + } else if (m_proof_irrel && const_name(eq_fn) == get_heq_name()) { return intro_next_heq(g); } else { throw_ill_formed_goal(); @@ -625,9 +626,9 @@ class inversion_tac { if (!is_app(v_type)) throw_unification_eq_rec_failure(); expr const & lift = app_fn(v_type); - if (!is_constant(lift) || const_name(lift) != "lift") + if (!is_constant(lift) || const_name(lift) != get_lift_name()) throw_unification_eq_rec_failure(); - return mk_app(mk_constant(name{"lift", "down"}, const_levels(lift)), app_arg(v_type), v); + return mk_app(mk_constant(get_lift_down_name(), const_levels(lift)), app_arg(v_type), v); } else { return v; } @@ -759,7 +760,7 @@ class inversion_tac { tformer = Fun(rhs, deps_g_type); else tformer = Fun(rhs, Fun(eq, deps_g_type)); - expr eq_rec = mk_constant(name{"eq", "rec"}, {eq_rec_lvl1, eq_rec_lvl2}); + expr eq_rec = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2}); eq_rec = mk_app(eq_rec, A, lhs, tformer); buffer new_hyps; new_hyps.append(non_deps); @@ -800,7 +801,7 @@ class inversion_tac { expr new_meta = mk_app(new_mvar, hyps); goal new_g(new_meta, new_type); level eq_symm_lvl = sort_level(m_tc.ensure_type(A).first); - expr symm_pr = mk_constant(name{"eq", "symm"}, {eq_symm_lvl}); + expr symm_pr = mk_constant(get_eq_symm_name(), {eq_symm_lvl}); symm_pr = mk_app(symm_pr, A, lhs, rhs, eq); expr val = g.abstract(mk_app(new_meta, symm_pr)); assign(g.get_name(), val); @@ -954,12 +955,12 @@ tactic inversion_tactic(name const & n, list const & ids) { } void initialize_inversion_tactic() { - register_tac(name({"tactic", "inversion"}), + register_tac(get_tactic_inversion_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name n = tactic_expr_to_id(app_arg(e), "invalid 'inversion/cases' tactic, argument must be an identifier"); return inversion_tactic(n, list()); }); - register_tac(name({"tactic", "inversion_with"}), + register_tac(get_tactic_inversion_with_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases-with' tactic, argument must be an identifier"); buffer ids; diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp index 65a55413b..1bd47b40b 100644 --- a/src/library/tactic/rename_tactic.cpp +++ b/src/library/tactic/rename_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "kernel/replace_fn.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -51,7 +52,7 @@ void initialize_rename_tactic() { return rename_tactic(get_rename_arg(app_arg(app_fn(e))), get_rename_arg(app_arg(e))); }; - register_tac(name({"tactic", "rename"}), fn); + register_tac(get_tactic_rename_name(), fn); } void finalize_rename_tactic() { diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 121d0a63b..086c6031d 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/abstract.h" +#include "library/constants.h" #include "library/locals.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -42,13 +43,13 @@ tactic revert_tactic(name const & n) { } void initialize_revert_tactic() { - register_tac(name({"tactic", "revert"}), + register_tac(get_tactic_revert_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name n = tactic_expr_to_id(app_arg(e), "invalid 'revert' tactic, argument must be an identifier"); return revert_tactic(n); }); - register_tac(name({"tactic", "revert_lst"}), + register_tac(get_tactic_revert_lst_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected"); diff --git a/src/library/tactic/trace_tactic.cpp b/src/library/tactic/trace_tactic.cpp index 2a379d156..e14c9b803 100644 --- a/src/library/tactic/trace_tactic.cpp +++ b/src/library/tactic/trace_tactic.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "kernel/type_checker.h" +#include "library/constants.h" #include "library/string.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -56,7 +57,7 @@ tactic suppress_trace(tactic const & t) { } void initialize_trace_tactic() { - register_tac(name({"tactic", "state"}), + register_tac(get_tactic_state_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) { if (p) if (auto it = p->get_pos_info(e)) @@ -64,7 +65,7 @@ void initialize_trace_tactic() { return trace_state_tactic(); }); - register_tac(name({"tactic", "trace"}), + register_tac(get_tactic_trace_name(), [](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer args; get_app_args(e, args); diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index 925d0714a..77688a8cb 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/instantiate.h" +#include "library/constants.h" #include "library/replace_visitor.h" #include "library/tactic/unfold_tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -115,7 +116,7 @@ tactic unfold_tactic() { } void initialize_unfold_tactic() { - register_tac(name({"tactic", "unfold"}), + register_tac(get_tactic_unfold_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { name const & id = tactic_expr_to_id(app_arg(e), "invalid 'unfold' tactic, argument must be an identifier"); diff --git a/src/library/tactic/util.cpp b/src/library/tactic/util.cpp index d435102e3..86b9dcc61 100644 --- a/src/library/tactic/util.cpp +++ b/src/library/tactic/util.cpp @@ -6,20 +6,20 @@ Author: Leonardo de Moura */ #include "kernel/type_checker.h" #include "library/aliases.h" +#include "library/constants.h" #include "library/tactic/util.h" #include "library/tactic/proof_state.h" namespace lean { bool is_tactic_namespace_open(environment const & env) { - name apply_tac({"tactic", "apply"}); for (name const & a : get_expr_aliases(env, "apply")) { - if (a == apply_tac) { + if (a == get_tactic_apply_name()) { // make sure the type is the expected one if (auto d = env.find(a)) { expr t = d->get_type(); if (is_pi(t)) { expr b = binding_body(t); - if (!is_constant(b) || const_name(b) != "tactic") + if (!is_constant(b) || const_name(b) != get_tactic_name()) throw exception("tactic namespace declarations have been modified, " "function 'tactic.apply' is expected to return a 'tactic'"); } diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp index 18c9e9c63..d50c30693 100644 --- a/src/library/tactic/whnf_tactic.cpp +++ b/src/library/tactic/whnf_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/constants.h" #include "library/reducible.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/elaborate.h" @@ -32,7 +33,7 @@ tactic whnf_tactic(bool relax_main_opaque) { } void initialize_whnf_tactic() { - register_tac(name({"tactic", "whnf"}), + register_tac(get_tactic_whnf_name(), [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { return whnf_tactic(); }); diff --git a/src/library/util.cpp b/src/library/util.cpp index ac132a070..e4982ba6d 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/locals.h" #include "library/util.h" +#include "library/constants.h" namespace lean { bool is_def_app(environment const & env, expr const & e) { @@ -82,23 +83,23 @@ bool has_constructor(environment const & env, name const & c, name const & I, un } bool has_unit_decls(environment const & env) { - return has_constructor(env, name{"unit", "star"}, "unit", 0); + return has_constructor(env, get_unit_star_name(), get_unit_name(), 0); } bool has_eq_decls(environment const & env) { - return has_constructor(env, name{"eq", "refl"}, "eq", 2); + return has_constructor(env, get_eq_refl_name(), get_eq_name(), 2); } bool has_heq_decls(environment const & env) { - return has_constructor(env, name{"heq", "refl"}, "heq", 2); + return has_constructor(env, get_heq_refl_name(), get_heq_name(), 2); } bool has_prod_decls(environment const & env) { - return has_constructor(env, name{"prod", "mk"}, "prod", 4); + return has_constructor(env, get_prod_mk_name(), get_prod_name(), 4); } bool has_lift_decls(environment const & env) { - return has_constructor(env, name{"lift", "up"}, "lift", 2); + return has_constructor(env, get_lift_up_name(), get_lift_name(), 2); } bool is_recursive_datatype(environment const & env, name const & n) { @@ -222,45 +223,13 @@ static expr * g_and_intro = nullptr; static expr * g_and_elim_left = nullptr; static expr * g_and_elim_right = nullptr; -static name * g_unit_name = nullptr; -static name * g_unit_mk_name = nullptr; -static name * g_prod_name = nullptr; -static name * g_prod_mk_name = nullptr; -static name * g_pr1_name = nullptr; -static name * g_pr2_name = nullptr; - -static name * g_eq_name = nullptr; -static name * g_eq_refl_name = nullptr; -static name * g_eq_rec_name = nullptr; - -static name * g_heq_name = nullptr; - -static name * g_sigma_name = nullptr; -static name * g_sigma_mk_name = nullptr; - void initialize_library_util() { - g_true = new expr(mk_constant("true")); - g_true_intro = new expr(mk_constant(name({"true", "intro"}))); - g_and = new expr(mk_constant("and")); - g_and_intro = new expr(mk_constant(name({"and", "intro"}))); - g_and_elim_left = new expr(mk_constant(name({"and", "elim_left"}))); - g_and_elim_right = new expr(mk_constant(name({"and", "elim_right"}))); - - g_unit_name = new name("unit"); - g_unit_mk_name = new name{"unit", "star"}; - g_prod_name = new name("prod"); - g_prod_mk_name = new name{"prod", "mk"}; - g_pr1_name = new name{"prod", "pr1"}; - g_pr2_name = new name{"prod", "pr2"}; - - g_eq_name = new name("eq"); - g_eq_refl_name = new name{"eq", "refl"}; - g_eq_rec_name = new name{"eq", "rec"}; - - g_heq_name = new name("heq"); - - g_sigma_name = new name("sigma"); - g_sigma_mk_name = new name{"sigma", "mk"}; + g_true = new expr(mk_constant(get_true_name())); + g_true_intro = new expr(mk_constant(get_true_intro_name())); + g_and = new expr(mk_constant(get_and_name())); + g_and_intro = new expr(mk_constant(get_and_intro_name())); + g_and_elim_left = new expr(mk_constant(get_and_elim_left_name())); + g_and_elim_right = new expr(mk_constant(get_and_elim_right_name())); } void finalize_library_util() { @@ -270,18 +239,6 @@ void finalize_library_util() { delete g_and_intro; delete g_and_elim_left; delete g_and_elim_right; - delete g_unit_name; - delete g_unit_mk_name; - delete g_prod_name; - delete g_prod_mk_name; - delete g_pr1_name; - delete g_pr2_name; - delete g_eq_name; - delete g_eq_refl_name; - delete g_eq_rec_name; - delete g_heq_name; - delete g_sigma_name; - delete g_sigma_mk_name; } expr mk_true() { @@ -311,17 +268,17 @@ expr mk_and_elim_right(type_checker & tc, expr const & H) { } expr mk_unit(level const & l) { - return mk_constant(*g_unit_name, {l}); + return mk_constant(get_unit_name(), {l}); } expr mk_unit_mk(level const & l) { - return mk_constant(*g_unit_mk_name, {l}); + return mk_constant(get_unit_star_name(), {l}); } expr mk_prod(type_checker & tc, expr const & A, expr const & B) { level l1 = sort_level(tc.ensure_type(A).first); level l2 = sort_level(tc.ensure_type(B).first); - return mk_app(mk_constant(*g_prod_name, {l1, l2}), A, B); + return mk_app(mk_constant(get_prod_name(), {l1, l2}), A, B); } expr mk_pair(type_checker & tc, expr const & a, expr const & b) { @@ -329,21 +286,21 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b) { expr B = tc.infer(b).first; level l1 = sort_level(tc.ensure_type(A).first); level l2 = sort_level(tc.ensure_type(B).first); - return mk_app(mk_constant(*g_prod_mk_name, {l1, l2}), A, B, a, b); + return mk_app(mk_constant(get_prod_mk_name(), {l1, l2}), A, B, a, b); } expr mk_pr1(type_checker & tc, expr const & p) { expr AxB = tc.whnf(tc.infer(p).first).first; expr const & A = app_arg(app_fn(AxB)); expr const & B = app_arg(AxB); - return mk_app(mk_constant(*g_pr1_name, const_levels(get_app_fn(AxB))), A, B, p); + return mk_app(mk_constant(get_prod_pr1_name(), const_levels(get_app_fn(AxB))), A, B, p); } expr mk_pr2(type_checker & tc, expr const & p) { expr AxB = tc.whnf(tc.infer(p).first).first; expr const & A = app_arg(app_fn(AxB)); expr const & B = app_arg(AxB); - return mk_app(mk_constant(*g_pr2_name, const_levels(get_app_fn(AxB))), A, B, p); + return mk_app(mk_constant(get_prod_pr2_name(), const_levels(get_app_fn(AxB))), A, B, p); } expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); } @@ -358,30 +315,30 @@ expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) { expr A = tc.whnf(tc.infer(lhs).first).first; level lvl = sort_level(tc.ensure_type(A).first); - return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs); + return mk_app(mk_constant(get_eq_name(), {lvl}), A, lhs, rhs); } expr mk_refl(type_checker & tc, expr const & a) { expr A = tc.whnf(tc.infer(a).first).first; level lvl = sort_level(tc.ensure_type(A).first); - return mk_app(mk_constant(*g_eq_refl_name, {lvl}), A, a); + return mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a); } expr mk_heq(type_checker & tc, expr const & lhs, expr const & rhs) { expr A = tc.whnf(tc.infer(lhs).first).first; expr B = tc.whnf(tc.infer(rhs).first).first; level lvl = sort_level(tc.ensure_type(A).first); - return mk_app(mk_constant(*g_heq_name, {lvl}), A, lhs, B, rhs); + return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs); } bool is_eq_rec(expr const & e) { expr const & fn = get_app_fn(e); - return is_constant(fn) && const_name(fn) == *g_eq_rec_name; + return is_constant(fn) && const_name(fn) == get_eq_rec_name(); } bool is_eq(expr const & e) { expr const & fn = get_app_fn(e); - return is_constant(fn) && const_name(fn) == *g_eq_name; + return is_constant(fn) && const_name(fn) == get_eq_name(); } bool is_eq_a_a(expr const & e) { @@ -406,7 +363,7 @@ bool is_eq_a_a(type_checker & tc, expr const & e) { void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer const & s, buffer & eqs) { lean_assert(t.size() == s.size()); lean_assert(std::all_of(s.begin(), s.end(), is_local)); - lean_assert(inductive::has_dep_elim(tc.env(), *g_eq_name)); + lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name())); buffer> t_aux; name e_name("e"); for (unsigned i = 0; i < t.size(); i++) { @@ -435,7 +392,7 @@ void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer co rec_args.push_back(eqs[j]); level rec_l1 = sort_level(tc.ensure_type(s_i_ty).first); level rec_l2 = sort_level(tc.ensure_type(mlocal_type(s[j])).first); - t_i = mk_app(mk_constant(*g_eq_rec_name, {rec_l1, rec_l2}), rec_args.size(), rec_args.data()); + t_i = mk_app(mk_constant(get_eq_rec_name(), {rec_l1, rec_l2}), rec_args.size(), rec_args.data()); } t_aux.back().push_back(t_i); } @@ -446,7 +403,7 @@ void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer co void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer & eqs) { lean_assert(std::all_of(t.begin(), t.end(), is_local)); - lean_assert(inductive::has_dep_elim(tc.env(), *g_eq_name)); + lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name())); buffer s; for (unsigned i = 0; i < t.size(); i++) { expr ty = mlocal_type(t[i]); @@ -478,7 +435,7 @@ expr telescope_to_sigma(type_checker & tc, unsigned sz, expr const * ts, constra expr const & Ba = r; level l1 = sort_level(tc.ensure_type(A, cs)); level l2 = sort_level(tc.ensure_type(Ba, cs)); - r = mk_app(mk_constant(*g_sigma_name, {l1, l2}), A, Fun(a, Ba)); + r = mk_app(mk_constant(get_sigma_name(), {l1, l2}), A, Fun(a, Ba)); } return r; } @@ -497,7 +454,7 @@ expr mk_sigma_mk(type_checker & tc, unsigned sz, expr const * ts, expr const * a expr arg4 = mk_sigma_mk(tc, sz-1, new_ts.data(), as+1, cs); level l1 = sort_level(tc.ensure_type(arg1, cs)); level l2 = sort_level(tc.ensure_type(arg2_core, cs)); - return mk_app(mk_constant(*g_sigma_mk_name, {l1, l2}), arg1, arg2, arg3, arg4); + return mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), arg1, arg2, arg3, arg4); } expr mk_sigma_mk(type_checker & tc, buffer const & ts, buffer const & as, constraint_seq & cs) {