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

chore(*): adapt C++ code to camelCase

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-20 13:00:58 -07:00
parent bc75a24127
commit e0b0ca4830
6 changed files with 22 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_cmds.cpp
View file

@ -613,7 +613,7 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("#eval", "evaluate given expression using VM", eval_cmd));
add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd));
add_cmd(r, cmd_info("#help", "brief description of available commands and options", help_cmd));
add_cmd(r, cmd_info("init_quot", "initialize `quot` type computational rules", init_quot_cmd));
add_cmd(r, cmd_info("initQuot", "initialize `quot` type computational rules", init_quot_cmd));
add_cmd(r, cmd_info("import", "import module(s)", import_cmd));
add_cmd(r, cmd_info("hide", "hide aliases in the current scope", hide_cmd));
add_cmd(r, cmd_info("#unify", "(for debugging purposes)", unify_cmd));

2
src/frontends/lean/elaborator.cpp
View file

@ -4071,7 +4071,7 @@ void initialize_elaborator() {
register_system_attribute(
elaborator_strategy_proxy_attribute(
"elab_simple",
elab_simple,
"instructs elaborator that the arguments of the function application (f ...) "
"should be elaborated from left to right, and without propagating information from the expected type "
"to its arguments",

2
src/frontends/lean/lean_elaborator.cpp
View file

@ -397,7 +397,7 @@ static void elaborate_command(parser & p, expr const & cmd) {
} else if (*cmd_name == "structure") {
elab_structure_cmd(p, cmd);
return;
} else if (*cmd_name == "init_quot") {
} else if (*cmd_name == "initQuot") {
p.set_env(module::add(p.env(), mk_quot_decl()));
return;
} else if (*cmd_name == "variables") {

2
src/frontends/lean/token_table.cpp
View file

@ -108,7 +108,7 @@ void init_token_table(token_table & t) {
"import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
"set_option", "open", "export", "@[",
"attribute", "instance", "include", "omit", "init_quot",
"attribute", "instance", "include", "omit", "initQuot",
"run_cmd", "#check", "#reduce", "#eval", "#print", "#help", "#exit",
"#compile", "#unify", "#compact_tst", nullptr};

24
src/kernel/quot.cpp
View file

@ -17,13 +17,13 @@ name * quot_consts::g_quot_ind = nullptr;
name * quot_consts::g_quot_mk = nullptr;
static void check_eq_type(environment const & env) {
constant_info eq_info = env.get("eq");
if (!eq_info.is_inductive()) throw exception("failed to initialize quot module, environment does not have 'eq' type");
constant_info eq_info = env.get("Eq");
if (!eq_info.is_inductive()) throw exception("failed to initialize quot module, environment does not have 'Eq' type");
inductive_val eq_val = eq_info.to_inductive_val();
if (length(eq_info.get_lparams()) != 1)
throw exception("failed to initialize quot module, unexpected number of universe params at 'eq' type");
throw exception("failed to initialize quot module, unexpected number of universe params at 'Eq' type");
if (length(eq_val.get_cnstrs()) != 1)
throw exception("failed to initialize quot module, unexpected number of constructors for 'eq' type");
throw exception("failed to initialize quot module, unexpected number of constructors for 'Eq' type");
local_ctx lctx;
name_generator g;
{
@ -31,16 +31,16 @@ static void check_eq_type(environment const & env) {
expr alpha = lctx.mk_local_decl(g, "α", mk_sort(u), mk_implicit_binder_info());
expr expected_eq_type = lctx.mk_pi(alpha, mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
if (expected_eq_type != eq_info.get_type())
throw exception("failed to initialize quot module, 'eq' has an expected type");
throw exception("failed to initialize quot module, 'Eq' has an expected type");
}
{
constant_info eq_refl_info = env.get(head(eq_val.get_cnstrs()));
level u = mk_univ_param(head(eq_refl_info.get_lparams()));
expr alpha = lctx.mk_local_decl(g, "α", mk_sort(u), mk_implicit_binder_info());
expr a = lctx.mk_local_decl(g, "a", alpha);
expr expected_eq_refl_type = lctx.mk_pi({alpha, a}, mk_app(mk_constant("eq", {u}), alpha, a, a));
expr expected_eq_refl_type = lctx.mk_pi({alpha, a}, mk_app(mk_constant("Eq", {u}), alpha, a, a));
if (eq_refl_info.get_type() != expected_eq_refl_type)
throw exception("failed to initialize quot module, unexpected type for 'eq' type constructor");
throw exception("failed to initialize quot module, unexpected type for 'Eq' type constructor");
}
}
@ -76,7 +76,7 @@ environment environment::add_quot() const {
expr b = lctx.mk_local_decl(g, "b", alpha);
expr r_a_b = mk_app(r, a, b);
/* f a = f b */
expr f_a_eq_f_b = mk_app(mk_constant("eq", {v}), beta, mk_app(f, a), mk_app(f, b));
expr f_a_eq_f_b = mk_app(mk_constant("Eq", {v}), beta, mk_app(f, a), mk_app(f, b));
/* (∀ a b : α, r a b → f a = f b) */
expr sanity = lctx.mk_pi({a, b}, mk_arrow(r_a_b, f_a_eq_f_b));
/* constant {u v} quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)
@ -98,10 +98,10 @@ environment environment::add_quot() const {
}
void initialize_quot() {
quot_consts::g_quot = new name{"quot"};
quot_consts::g_quot_lift = new name{"quot", "lift"};
quot_consts::g_quot_ind = new name{"quot", "ind"};
quot_consts::g_quot_mk = new name{"quot", "mk"};
quot_consts::g_quot = new name{"Quot"};
quot_consts::g_quot_lift = new name{"Quot", "lift"};
quot_consts::g_quot_ind = new name{"Quot", "ind"};
quot_consts::g_quot_mk = new name{"Quot", "mk"};
}
void finalize_quot() {

12
src/library/compiler/util.cpp
View file

@ -97,10 +97,10 @@ bool has_inline_attribute(environment const & env, name const & n) {
}
bool has_inline_if_reduce_attribute(environment const & env, name const & n) {
if (has_attribute(env, "inline_if_reduce", n))
if (has_attribute(env, "inlineIfReduce", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inline_if_reduce]`
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inlineIfReduce]`
if `f` is marked. */
return has_inline_if_reduce_attribute(env, n.get_prefix());
}
@ -108,10 +108,10 @@ bool has_inline_if_reduce_attribute(environment const & env, name const & n) {
}
bool has_macro_inline_attribute(environment const & env, name const & n) {
if (has_attribute(env, "macro_inline", n))
if (has_attribute(env, "macroInline", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[macro_inline]`
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[macroInline]`
if `f` is marked. */
return has_macro_inline_attribute(env, n.get_prefix());
}
@ -551,7 +551,7 @@ void initialize_compiler_util() {
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'inline_if_reduce' use, only definitions can be marked as [inline_if_reduce]");
throw exception("invalid 'inline_if_reduce' use, only definitions can be marked as [inlineIfReduce]");
}));
register_system_attribute(basic_attribute::with_check(
@ -567,7 +567,7 @@ void initialize_compiler_util() {
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'macro_inline' use, only definitions can be marked as [macro_inline]");
throw exception("invalid 'macroInline' use, only definitions can be marked as [macroInline]");
}));
}