From e0b0ca48309910fd18c4805c756a0779635663bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Mar 2019 13:00:58 -0700 Subject: [PATCH] chore(*): adapt C++ code to camelCase --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/lean_elaborator.cpp | 2 +- src/frontends/lean/token_table.cpp | 2 +- src/kernel/quot.cpp | 24 ++++++++++++------------ src/library/compiler/util.cpp | 12 ++++++------ 6 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index e423ed365d..2772de9504 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -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)); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b8205c3c9c..557a94ae85 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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", diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 45cc7aa37a..f503f7013d 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -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") { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 6e37bea18d..13f5b2fd3a 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -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}; diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp index 5c25cd6b96..988882c714 100644 --- a/src/kernel/quot.cpp +++ b/src/kernel/quot.cpp @@ -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() { diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index a26264d916..5641251a34 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -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]"); })); }