From 736060d87d1d19c3a3fb59a5e3dfe870be6ab77a Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 31 Mar 2020 20:44:17 -0400 Subject: [PATCH] feat(tactic/lint): add some hooks to allow linting of proof scripts --- library/init/meta/converter/conv.lean | 5 +- library/init/meta/executor.lean | 225 +++++++++++++++++++++++++ library/init/meta/interactive.lean | 5 +- library/init/meta/tactic.lean | 48 +----- src/frontends/lean/interactive.cpp | 2 +- src/frontends/lean/tactic_notation.cpp | 115 ++++++++++++- src/frontends/lean/tactic_notation.h | 4 +- 7 files changed, 350 insertions(+), 54 deletions(-) create mode 100644 library/init/meta/executor.lean diff --git a/library/init/meta/converter/conv.lean b/library/init/meta/converter/conv.lean index cd45a258d1..c8113b12d9 100644 --- a/library/init/meta/converter/conv.lean +++ b/library/init/meta/converter/conv.lean @@ -14,7 +14,7 @@ universe u /-- `conv α` is a tactic for discharging goals of the form `lhs ~ rhs` for some relation `~` (usually equality) and fixed lhs, rhs. Known in the literature as a __conversion__ tactic. -So for example, if one had the lemma `p : x = y`, then the conversion for `p` would be one that solves `p`. +So for example, if one had the lemma `p : x = y`, then the conversion for `p` would be one that solves `p`. -/ meta def conv (α : Type u) := tactic α @@ -28,6 +28,9 @@ by dunfold conv; apply_instance meta instance : alternative conv := by dunfold conv; apply_instance +meta instance : interactive.executor conv := +by dunfold conv; apply_instance + namespace conv /-- Applies the conversion `c`. Returns `(rhs,p)` where `p : r lhs rhs`. Throws away the return value of `c`.-/ meta def convert (c : conv unit) (lhs : expr) (rel : name := `eq) : tactic (expr × expr) := diff --git a/library/init/meta/executor.lean b/library/init/meta/executor.lean new file mode 100644 index 0000000000..aa3395bad3 --- /dev/null +++ b/library/init/meta/executor.lean @@ -0,0 +1,225 @@ +prelude +import init.meta.tactic init.meta.attribute init.meta.rb_map init.meta.derive + +universes u v + +namespace interactive + +-- meta def tactic_handler.get_state_dflt : tactic unit := +-- tactic.exact `(pure () : tactic unit) + +-- meta def tactic_handler.set_state_dflt : tactic unit := +-- tactic.exact `(pure : unit → tactic unit) + +-- meta structure tactic_handler (state : Type := unit) := +-- (name : name) +-- [state_has_reflect : has_reflect state] +-- (on_begin : tactic state) +-- (on_end : (state → tactic unit)) +-- (get_state : tactic state . tactic_handler.get_state_dflt) +-- (set_state : (state → tactic unit) . tactic_handler.set_state_dflt) + +-- attribute [instance] tactic_handler.state_has_reflect +-- attribute [derive has_reflect] tactic_handler + +-- meta instance : has_reflect tactic_handler +-- | a := `(_) +-- `({ tactic_handler . name := _, on_begin := _, on_end := _, state := _, get_state := _, set_state := _ }) + +-- meta instance state.has_reflect (hdl : tactic_handler) [reflected hdl] : has_reflect (option hdl.state) := +-- @option.has_reflect _ (tactic_handler.has_reflect _) $ reflected.subst `(tactic_handler.state) `(hdl) + +-- #check option.has_reflect +-- #check tactic_handler.has_reflect +open native +open tactic +-- #exit +namespace tactic_handler + +-- meta def to_user_attribute +-- {s : Type} (hdl : tactic_handler s) +-- [has_reflect s] [reflected s] : +-- user_attribute unit expr := +-- { name := hdl.name <.> "store", +-- -- reflect_param := state.has_reflect hdl, +-- -- (tactic_handler.has_reflect hdl hdl), +-- descr := to_string hdl.name ++ " store", +-- parser := fail "do not use" } + +-- meta def read_dyn (hdl : _root_.name) : tactic expr := +-- do c ← mk_const $ hdl <.> "store", +-- e ← eval_expr (user_attribute unit expr) c, +-- e.get_param hdl + +-- meta def write_dyn (hdl : _root_.name) (v : expr) : tactic unit := +-- do c ← mk_const $ hdl <.> "store", +-- infer_type c >>= trace, +-- trace hdl, +-- e ← eval_expr (user_attribute unit expr) c, +-- trace "b", +-- e.set hdl v tt, +-- trace "c" + +end tactic_handler + + +-- @[user_attribute] +-- meta def tactic_handler_attr : user_attribute := -- (rb_map name expr) := +-- { name := `tactic_handler, +-- descr := "descr", +-- after_set := some $ λ n p _, do +-- { `(tactic_handler %%state) ← tactic.mk_const n >>= infer_type +-- | fail "expecting definition of type `user_attribute`", +-- e ← resolve_name n, +-- df ← to_expr ``(tactic_handler.to_user_attribute %%e), +-- t ← infer_type df, +-- add_meta_definition (n <.> "store") [] t df, +-- infer_type df >>= trace, +-- set_basic_attribute ``user_attribute (n <.> "store") tt, +-- -- e ← mk_const n, +-- trace "\nAAA", +-- e_store ← mk_const (n <.> "store"), +-- infer_type e_store >>= trace, +-- trace "\nAAA", +-- val ← mk_mapp ``option.none [state], +-- trace "\nAAA", +-- let none_e : expr := reflect $ @none ℕ, +-- let v_e : expr := reflect val, +-- let n_e : expr := reflect n, +-- let b_e : expr := reflect tt, +-- x ← mk_mapp ``user_attribute.set [none,none,none,e_store,n_e,v_e,b_e,none_e], +-- tac ← eval_expr (tactic unit) x, +-- tac, +-- trace "\nAAA", +-- -- x ← mk_app ``user_attribute.set [e_store,n_e,v_e,b_e], +-- infer_type x >>= trace, +-- attr ← eval_expr (user_attribute unit expr) e_store, +-- -- infer_type attr >>= trace, +-- trace "state", +-- -- n_hdl ← mk_app ``tactic_handler.name [e] >>= eval_expr name, +-- -- tactic_handler.write_dyn n val, +-- trace "state" }, +-- } +-- #check @user_attribute.set +-- #exit +-- set_option trace.app_builder true +-- @[tactic_handler] +-- meta def my_tactic_handler : tactic_handler := +-- { name := `my_tactic_handler, +-- on_begin := tactic.trace "begin", +-- on_end := λ _, tactic.trace "end", } + +meta def foo : tactic unit := do +let n := `foo, +let n := reflect n, +trace_state, +add_decl $ mk_definition `foo [] `(name) n, +mk_const `foo >>= exact + +meta class is_advice_type (α : Type) := +-- [type_reflect : has_reflect α] +(to_format : α → format) +(to_format_name : name . foo) +-- (combine : α → α → α) + +meta instance : is_advice_type nat := +{ to_format := to_fmt, } +#check foo +@[derive has_reflect] +meta structure advice := +(to_format : name) +(val : expr) + +attribute [instance] is_advice_type.type_reflect + +@[user_attribute] +private meta def lint_advice_attr : user_attribute unit (list (pos × advice)) := -- (rb_map name expr) := +{ name := `_lint_advice, + descr := "descr", + parser := fail "do not use" } + +def lint_advice_carrier := () + +run_cmd lint_advice_attr.set ``lint_advice_carrier [] tt + +-- end interactive + + +-- namespace interactive + +open tactic + +declare_trace lint.all +declare_trace lint.tactic + +meta def executor.combine_advice_dflt : tactic unit := +tactic.refine ``(λ _ _, ()) + +meta def executor.default_resolve (pre n : name) : tactic name := +if is_trace_enabled_for `lint.all = tt ∨ is_trace_enabled_for (`lint ++ pre) = tt + then resolve_constant (pre <.> "linter" ++ n) <|> + pure (pre <.> "interactive" ++ n) + else pure $ pre <.> "interactive" ++ n + +-- meta def executor.resolve_tactic_name_dfl : tactic unit := +-- applyc ``executor.default_resolve +-- do `(name → (%%m : Type → Type*) name) ← tactic.target, +-- let n := m.get_app_fn.const_name, +-- let n : reflected n := reflect n, +-- e ← mk_mapp ``interactive.executor.default_resolve [m,none,n], +-- exact e + +/-- Typeclass for custom interaction monads, which provides + the information required to convert an interactive-mode + construction to a `tactic` which can actually be executed. + + Given a `[monad m]`, `execute_with` explains how to turn a `begin ... end` + block, or a `by ...` statement into a `tactic α` which can actually be + executed. The `inhabited` first argument facilitates the passing of an + optional configuration parameter `config`, using the syntax: + ``` + begin [custom_monad] with config, + ... + end + ``` +-/ +meta class executor (m : Type → Type u) [monad m] := +(config_type : Type) +(advice_type : Type := unit) +[inhabited : inhabited config_type] +-- [advice : monoid] +(combine_advice : advice_type → advice_type → advice_type . executor.combine_advice_dflt) +(format_advice : advice_type → format) +(execute_with : config_type → m punit → tactic.{u} punit) +(resolve_tactic_name : name → name → tactic name := executor.default_resolve) + +attribute [inline] executor.execute_with + +@[inline] +meta def executor.execute_explicit (m : Type → Type v) + [monad m] [e : executor m] : m punit → tactic punit := +executor.execute_with e.inhabited.default + +@[inline] +meta def executor.execute_with_explicit (m : Type → Type v) + [monad m] [executor m] : executor.config_type m → m punit → tactic punit := +executor.execute_with + +/-- Default `executor` instance for `tactic`s themselves -/ +meta instance : executor tactic := +{ config_type := punit, + inhabited := ⟨()⟩, + execute_with := λ _ tac, tac, + -- resolve_tactic_name := λ n, do + -- trace ("resolve " ++ to_string n) $ + -- pure $ `tactic.interactive ++ n + } + +end interactive + +namespace tactic + +notation `‹` p `›` := (by assumption : p) +notation `dec_trivial` := of_as_true (by tactic.triv) + +end tactic diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 477563d433..217fc99764 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -7,7 +7,7 @@ prelude import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic import init.meta.smt.congruence_closure init.category.combinators import init.meta.interactive_base init.meta.derive init.meta.match_tactic -import init.meta.congr_tactic +import init.meta.congr_tactic init.meta.executor open lean open lean.parser @@ -1724,3 +1724,6 @@ by tactic.mk_inj_eq lemma nat.succ.inj_eq (n₁ n₂ : nat) : (nat.succ n₁ = nat.succ n₂) = (n₁ = n₂) := by tactic.mk_inj_eq + +#print instances has_reflect +#check has_reflect diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 1d24029195..14c6a8d06f 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -8,6 +8,7 @@ import init.function init.data.option.basic init.util import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment import init.meta.pexpr init.data.repr init.data.string.basic init.meta.interaction_monad + init.meta.has_reflect meta constant tactic_state : Type @@ -30,6 +31,7 @@ meta constant get_options : tactic_state → options meta constant set_options : tactic_state → options → tactic_state end tactic_state + meta instance : has_to_format tactic_state := ⟨tactic_state.to_format⟩ @@ -81,47 +83,6 @@ meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) | exception t ref s := exception t ref s end -namespace interactive - -/-- Typeclass for custom interaction monads, which provides - the information required to convert an interactive-mode - construction to a `tactic` which can actually be executed. - - Given a `[monad m]`, `execute_with` explains how to turn a `begin ... end` - block, or a `by ...` statement into a `tactic α` which can actually be - executed. The `inhabited` first argument facilitates the passing of an - optional configuration parameter `config`, using the syntax: - ``` - begin [custom_monad] with config, - ... - end - ``` --/ -meta class executor (m : Type → Type u) [monad m] := -(config_type : Type) -[inhabited : inhabited config_type] -(execute_with : config_type → m unit → tactic unit) - -attribute [inline] executor.execute_with - -@[inline] -meta def executor.execute_explicit (m : Type → Type u) - [monad m] [e : executor m] : m unit → tactic unit := -executor.execute_with e.inhabited.default - -@[inline] -meta def executor.execute_with_explicit (m : Type → Type u) - [monad m] [executor m] : executor.config_type m → m unit → tactic unit := -executor.execute_with - -/-- Default `executor` instance for `tactic`s themselves -/ -meta instance : executor tactic := -{ config_type := unit, - inhabited := ⟨()⟩, - execute_with := λ _, id } - -end interactive - namespace tactic variables {α : Type u} @@ -264,6 +225,7 @@ meta instance {α} (a : α) : has_to_tactic_format (reflected a) := @[priority 10] meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α := ⟨(λ x, return x) ∘ to_fmt⟩ + namespace tactic open tactic_state @@ -877,8 +839,6 @@ meta def save_info (p : pos) : tactic unit := do s ← read, tactic.save_info_thunk p (λ _, tactic_state.to_format s) -notation `‹` p `›` := (by assumption : p) - /-- Swap first two goals, do nothing if tactic state does not have at least two goals. -/ meta def swap : tactic unit := do gs ← get_goals, @@ -1205,8 +1165,6 @@ infer_type fn >>= get_pi_arity meta def triv : tactic unit := mk_const `trivial >>= exact -notation `dec_trivial` := of_as_true (by tactic.triv) - meta def by_contradiction (H : option name := none) : tactic expr := do tgt : expr ← target, (match_not tgt >> return ()) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 3273ed7b67..558a1496b2 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -143,7 +143,7 @@ void report_info(environment const & env, options const & opts, io_state const & record["doc"] = it->get_description(); break; case break_at_pos_exception::token_context::interactive_tactic: { - auto n = get_interactive_tactic_full_name(e.m_token_info.m_param, e.m_token_info.m_token); + auto n = get_interactive_tactic_full_name(env, e.m_token_info.m_param, e.m_token_info.m_token); if (env.find(n)) { record = serialize_decl(e.m_token_info.m_token, n, env, opts); if (auto idx = e.m_token_info.m_tac_param_idx) diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 59f049a40a..74e3b32527 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/explicit.h" #include "kernel/scope_pos_info_provider.h" +#include "library/vm/vm_name.h" #include "library/vm/vm_nat.h" #include "library/vm/vm_format.h" #include "library/vm/vm_expr.h" @@ -110,9 +111,30 @@ static expr concat(parser & p, expr const & tac1, expr const & tac2, pos_info co return p.save_pos(mk_app(mk_constant(get_has_bind_seq_name()), tac1, tac2), pos); } -name get_interactive_tactic_full_name(name const & tac_class, name const & tac) { - return name(tac_class, "interactive") + tac; -} +// static name mk_tactic_resolve_tactic_name(environment const & env, name tac_class, name tactic_n); + +// name get_interactive_tactic_full_name(environment const & env, name const & tac_class, name const & tac) { + // std::cout << "full name\n"; + // p.next(); + // parser::local_scope scope1(p); + // meta_definition_scope scope2; + // p.clear_expr_locals(); + // auto tac_pos = p.pos(); + // try { + // // bool use_istep = true; + // // expr tac = parse_tactic(p, get_tactic_name(), use_istep); + // tac = mk_tactic_resolve_name(tac, get_tactic_name()); + // expr type = mk_tactic_unit(get_tactic_name()); + // expr r = p.save_pos(mk_typed_expr(type, tac), tac_pos); + // return p.save_pos(mk_by(r), pos); + // } catch (break_at_pos_exception & ex) { + // ex.report_goal_pos(tac_pos); + // throw ex; + // } + // return mk_tactic_resolve_tactic_name(env, tac_class, tac); + + // return name(tac_class, "interactive") + tac; +// } static bool is_curr_exact_shortcut(parser & p) { return p.curr_is_token(get_calc_tk()); @@ -130,7 +152,7 @@ static optional is_interactive_tactic(parser & p, name const & tac_class) default: return {}; } - id = get_interactive_tactic_full_name(tac_class, id); + id = get_interactive_tactic_full_name(p.env(), tac_class, id); if (p.env().find(id)) return optional(id); else @@ -270,7 +292,8 @@ struct parse_tactic_fn { } } else if (is_curr_exact_shortcut(m_p)) { expr arg = parse_qexpr(); - r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos); + name full_name = get_interactive_tactic_full_name(m_p.env(), m_tac_class, "exact"); + r = m_p.mk_app(m_p.save_pos(mk_constant(full_name), pos), arg, pos); if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, pos, m_tac_class); } else { r = m_p.parse_expr(); @@ -416,6 +439,77 @@ static name parse_tactic_class(parser & p, name tac_class) { } } + /* Constructs an app of: + interactive.executor.resolve_tactic_name : Π (m : Type → Type u) + [monad m] [interactive.executor m], + name → tactic name +*/ +// static name mk_tactic_resolve_tactic_name(environment const & env, name tac_class, name tactic_n) { +name get_interactive_tactic_full_name(environment const & env, + name const & tac_class, + name const & tactic_n) { + + // std::cout << "tactic_n: " << tactic_n << std::endl; + // std::cout << "tac_class: " << tac_class << std::endl; + // unsigned nlvl = env.get(tac_class).get_num_univ_params(); + + name resolve_tactic_fn = + name(get_interactive_executor_name(), + "resolve_tactic_name"); + metavar_context mctx = metavar_context(); + local_context lctx = local_context(); + environment l_env = env; + expr resolve_name_e; level_param_names ls; + std::tie(resolve_name_e, ls) = + lean::elaborate(l_env, options(), "_resolve_tactic", mctx, lctx, + mk_app({ mk_constant(resolve_tactic_fn), + mk_constant(tac_class) }), + true, false); + resolve_name_e = mctx.instantiate_mvars(resolve_name_e); + buffer args; + args.push_back(to_obj(tac_class)); + args.push_back(to_obj(tactic_n)); + tactic_state s = mk_tactic_state_for(env, options(), "_resolve_tactic", mctx, + lctx, mk_true()); + + expr dummy; + type_context_old ctx = mk_type_context_for(s); + try { + vm_obj r = tactic::evaluator(ctx, options(), dummy)(resolve_name_e, args, s); + if (tactic::is_result_success(r)) { + return to_name(tactic::get_success_value(r)); + } else { + vm_state S(env, options()); + tactic::report_exception(S, r); + } + } catch (exception & ex) { + throw nested_exception(sstream() << "failed to resolve tactic name '" << tactic_n << "'", ex); + } + throw exception(sstream() << "failed to resolve tactic name '" << tactic_n << "'"); + + // expr prove_injective_eq(environment const & env, expr const & inj_eq_type, name const & inj_eq_name) { + // try { + // type_context_old ctx(env, transparency_mode::Semireducible); + // expr dummy_ref; + // expr resolve_name_e = mk_app({ + // mk_constant(name(get_interactive_executor_name(), + // "resolve_tactic_name")), + // mk_constant(tac_class), + // tac + // }); + // tactic_state s = mk_tactic_state_for(env, options(), inj_eq_name, metavar_context(), local_context(), resolve_tactic_name); + // vm_obj r = tactic_evaluator(ctx, options(), dummy_ref)(mk_constant(get_tactic_mk_inj_eq_name()), s); + // if (auto new_s = tactic::is_success(r)) { + // metavar_context mctx = new_s->mctx(); + // return mctx.instantiate_mvars(new_s->main()); + // } + // } catch (exception & ex) { + // throw nested_exception(sstream() << "failed to generate auxiliary lemma '" << inj_eq_name << "'", ex); + // } + // throw exception(sstream() << "failed to generate auxiliary lemma '" << inj_eq_name << "'"); + +} + /* Constructs an app of: interactive.executor.execute_explicit : Π (m : Type → Type u) [monad m] [interactive.executor m], @@ -534,6 +628,7 @@ struct parse_begin_end_block_fn { ex.report_goal_pos(end_pos); throw; } + // std::cout << "here\n"; if (!is_ext_tactic_class && m_tac_class != get_tactic_name()) { return r; } else if (cfg) { @@ -576,14 +671,24 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { p.clear_expr_locals(); auto tac_pos = p.pos(); try { + tactic_state s = mk_tactic_state_for(p.env(), options(), "_resolve_tactic", + metavar_context(), + local_context(), mk_true()); + + // std::cout << "\n> there\n"; bool use_istep = true; expr tac = parse_tactic(p, get_tactic_name(), use_istep); + // std::cout << "> there B\n"; tac = mk_tactic_execute(tac, get_tactic_name()); + // std::cout << tac << std::endl; + // std::cout << "> there C\n"; expr type = mk_tactic_unit(get_tactic_name()); expr r = p.save_pos(mk_typed_expr(type, tac), tac_pos); return p.save_pos(mk_by(r), pos); } catch (break_at_pos_exception & ex) { + // std::cout << ">> there (exception 1)\n"; ex.report_goal_pos(tac_pos); + // std::cout << ">> there (exception 2)\n"; throw ex; } } diff --git a/src/frontends/lean/tactic_notation.h b/src/frontends/lean/tactic_notation.h index 445e064346..82a740d20f 100644 --- a/src/frontends/lean/tactic_notation.h +++ b/src/frontends/lean/tactic_notation.h @@ -7,7 +7,9 @@ Author: Leonardo de Moura #pragma once #include "frontends/lean/parser.h" namespace lean { -name get_interactive_tactic_full_name(name const & tac_class, name const & tac); +name get_interactive_tactic_full_name + (environment const & env, + name const & tac_class, name const & tac); expr parse_begin_end_expr(parser & p, pos_info const & pos); expr parse_curly_begin_end_expr(parser & p, pos_info const & pos); expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos);