From dac6eec55661d3a2dab56859ffc05aef1aabb185 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jun 2017 21:12:29 -0700 Subject: [PATCH] feat(library/tactic): add hole_command bookkeeping --- library/init/meta/hole_command.lean | 48 ++++++++++++++++ src/library/constants.cpp | 4 ++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/hole_command.cpp | 87 +++++++++++++++++++++++++++++ src/library/tactic/hole_command.h | 11 ++++ src/library/tactic/init_module.cpp | 3 + tests/lean/run/check_constants.lean | 1 + 9 files changed, 157 insertions(+), 1 deletion(-) create mode 100644 library/init/meta/hole_command.lean create mode 100644 src/library/tactic/hole_command.cpp create mode 100644 src/library/tactic/hole_command.h diff --git a/library/init/meta/hole_command.lean b/library/init/meta/hole_command.lean new file mode 100644 index 0000000000..17712cb487 --- /dev/null +++ b/library/init/meta/hole_command.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.meta.tactic + +/-- +The front-end (e.g., Emacs, VS Code) can invoke commands for holes {! ... !} in +a declaration. A command is a tactic that takes the optional pre-term in the +hole, and returns a list of expressions. The Lean server converts the list +into a list of strings using the pretty printer, and return it to the front-end. +Each string represents a different way to fill the hole. +The front-end is responsible for replacing the hole with the user selected alternative. + +This infra-structure can be use to implement auto-fill and/or refine commands. + +An action may return an empty list. This is useful for actions that just return +information such as the type of an expression, its normal form, etc. +-/ +meta structure hole_command := +(name : string) +(descr : string) +(action : option pexpr → tactic (list expr)) + +open tactic + +@[hole_command] +meta def infer_type_cmd : hole_command := +{ name := "Infer", + descr := "Infer type of the expression in the hole", + action := λ o, do + some p ← return o | fail "Infer command, hole does not contain a term", + e ← to_expr p, + t ← infer_type e, + trace t, + return [] +} + +@[hole_command] +meta def show_goal_cmd : hole_command := +{ name := "Show", + descr := "Show the current goal", + action := λ _, do + trace_state, + return [] +} diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 612f3bded4..6909ae933a 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -119,6 +119,7 @@ name const * g_heq_refl = nullptr; name const * g_heq_symm = nullptr; name const * g_heq_trans = nullptr; name const * g_heq_of_eq = nullptr; +name const * g_hole_command = nullptr; name const * g_id_locked = nullptr; name const * g_if_neg = nullptr; name const * g_if_pos = nullptr; @@ -491,6 +492,7 @@ void initialize_constants() { g_heq_symm = new name{"heq", "symm"}; g_heq_trans = new name{"heq", "trans"}; g_heq_of_eq = new name{"heq_of_eq"}; + g_hole_command = new name{"hole_command"}; g_id_locked = new name{"id_locked"}; g_if_neg = new name{"if_neg"}; g_if_pos = new name{"if_pos"}; @@ -864,6 +866,7 @@ void finalize_constants() { delete g_heq_symm; delete g_heq_trans; delete g_heq_of_eq; + delete g_hole_command; delete g_id_locked; delete g_if_neg; delete g_if_pos; @@ -1236,6 +1239,7 @@ name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_symm_name() { return *g_heq_symm; } name const & get_heq_trans_name() { return *g_heq_trans; } name const & get_heq_of_eq_name() { return *g_heq_of_eq; } +name const & get_hole_command_name() { return *g_hole_command; } name const & get_id_locked_name() { return *g_id_locked; } name const & get_if_neg_name() { return *g_if_neg; } name const & get_if_pos_name() { return *g_if_pos; } diff --git a/src/library/constants.h b/src/library/constants.h index c807304d02..6ec2372aca 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -121,6 +121,7 @@ name const & get_heq_refl_name(); name const & get_heq_symm_name(); name const & get_heq_trans_name(); name const & get_heq_of_eq_name(); +name const & get_hole_command_name(); name const & get_id_locked_name(); name const & get_if_neg_name(); name const & get_if_pos_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 859d8957b5..4b3e7f997a 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -114,6 +114,7 @@ heq.refl heq.symm heq.trans heq_of_eq +hole_command id_locked if_neg if_pos diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index da3942a236..4f5f14c562 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -8,5 +8,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp simp_result.cpp user_attribute.cpp eval.cpp simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp - vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp + vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp hole_command.cpp elaborator_exception.cpp algebraic_normalizer.cpp tactic_evaluator.cpp) diff --git a/src/library/tactic/hole_command.cpp b/src/library/tactic/hole_command.cpp new file mode 100644 index 0000000000..0448c01d99 --- /dev/null +++ b/src/library/tactic/hole_command.cpp @@ -0,0 +1,87 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "util/name_hash_map.h" +#include "library/constants.h" +#include "library/util.h" +#include "library/attribute_manager.h" +#include "library/scoped_ext.h" +#include "library/vm/vm_string.h" +#include "library/tactic/tactic_state.h" + +namespace lean { +/* Persisting */ +struct hole_command_ext : public environment_extension { + name_map> m_cmds; +}; + +struct hole_command_ext_reg { + unsigned m_ext_id; + hole_command_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static hole_command_ext_reg * g_ext = nullptr; +static hole_command_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} +static environment update(environment const & env, hole_command_ext const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + +static environment add_hole_command(environment const & env, name const & d) { + auto const & ty = env.get(d).get_type(); + if (!is_constant(ty, get_hole_command_name())) + throw exception("invalid [hole_command], must be applied to definition of type hole_command"); + + vm_state vm(env, options()); + vm_obj o = vm.invoke(d, {}); + name n(to_string(cfield(o, 0))); + hole_command_ext ext = get_extension(env); + if (ext.m_cmds.contains(n)) + throw exception(sstream() << "hole commad named [" << n << "] has already been registered"); + std::string descr = to_string(cfield(o, 1)); + ext.m_cmds.insert(n, {n, descr}); + return update(env, ext); +} + +struct hole_command_modification : public modification { + LEAN_MODIFICATION("HOLE_CMD") + name m_name; + + hole_command_modification() {} + hole_command_modification(name const & name) : m_name(name) {} + + void perform(environment & env) const override { + env = add_hole_command(env, m_name); + } + + void serialize(serializer & s) const override { + s << m_name; + } + + static std::shared_ptr deserialize(deserializer & d) { + return std::make_shared(read_name(d)); + } +}; + +void initialize_hole_command() { + register_system_attribute(basic_attribute( + "hole_command", "register a definition of type `hole_command` in the system", + [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) { + if (!persistent) + throw exception("illegal [hole_command] application, cannot be used locally"); + return module::add_and_perform(env, std::make_shared(n)); + })); + g_ext = new hole_command_ext_reg(); + hole_command_modification::init(); +} +void finalize_hole_command() { + hole_command_modification::finalize(); + delete g_ext; +} +} diff --git a/src/library/tactic/hole_command.h b/src/library/tactic/hole_command.h new file mode 100644 index 0000000000..8aea3144e4 --- /dev/null +++ b/src/library/tactic/hole_command.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +void initialize_hole_command(); +void finalize_hole_command(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index a106eff9db..23d0abb28f 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -35,6 +35,7 @@ Author: Leonardo de Moura #include "library/tactic/norm_num_tactic.h" #include "library/tactic/destruct_tactic.h" #include "library/tactic/algebraic_normalizer.h" +#include "library/tactic/hole_command.h" #include "library/tactic/backward/init_module.h" #include "library/tactic/smt/init_module.h" @@ -72,10 +73,12 @@ void initialize_tactic_module() { initialize_vm_monitor(); initialize_destruct_tactic(); initialize_algebraic_normalizer(); + initialize_hole_command(); initialize_smt_module(); } void finalize_tactic_module() { finalize_smt_module(); + finalize_hole_command(); finalize_algebraic_normalizer(); finalize_destruct_tactic(); finalize_vm_monitor(); diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 3bc4b8824e..2fa2316f27 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -119,6 +119,7 @@ run_cmd script_check_id `heq.refl run_cmd script_check_id `heq.symm run_cmd script_check_id `heq.trans run_cmd script_check_id `heq_of_eq +run_cmd script_check_id `hole_command run_cmd script_check_id `id_locked run_cmd script_check_id `if_neg run_cmd script_check_id `if_pos