From cbac21ec7f9e5e64b53a50bd0fa73f6a7795b583 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Jul 2014 19:05:22 -0700 Subject: [PATCH] feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions Signed-off-by: Leonardo de Moura --- library/standard/tactic.lean | 29 ++++++++ src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/expr_to_tactic.cpp | 97 +++++++++++++++++++++++++++ src/library/tactic/expr_to_tactic.h | 27 ++++++++ 4 files changed, 155 insertions(+), 1 deletion(-) create mode 100644 library/standard/tactic.lean create mode 100644 src/library/tactic/expr_to_tactic.cpp create mode 100644 src/library/tactic/expr_to_tactic.h diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean new file mode 100644 index 000000000..25dc2ee13 --- /dev/null +++ b/library/standard/tactic.lean @@ -0,0 +1,29 @@ +import logic + +namespace tactic +-- This is just a trick to embed the 'tactic language' as a +-- Lean expression. We should view (tactic A) as automation +-- that when execute produces a term of type A. +-- tactic_value is just a "dummy" for creating the "fake" +inductive tactic (A : Type) : Type := +| tactic_value {} : tactic A +-- Remark the following names are not arbitrary, the tactic module +-- uses them when converting Lean expressions into actual tactic objects. +-- The bultin 'by' construct triggers the process of converting a +-- a term of type (tactic A) into a tactic that sythesizes a term +-- of type A +definition then_tac {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value +definition orelse_tac {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value +definition repeat_tac {A : Type} (t : tactic A) : tactic A := tactic_value +definition now {A : Type} : tactic A := tactic_value +definition state {A : Type} : tactic A := tactic_value +definition fail {A : Type} : tactic A := tactic_value +definition id {A : Type} : tactic A := tactic_value +definition beta {A : Type} : tactic A := tactic_value +definition apply {A : Type} {B : Type} (b : B) : tactic A := tactic_value + +infixl `;`:200 := then_tac +infixl `|`:100 := orelse_tac +notation `!`:max t:max := repeat_tac t +end + diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index c0c757da9..814dc03d2 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,5 @@ -add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp) +add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp +expr_to_tactic.cpp) # simplify_tactic.cpp) diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp new file mode 100644 index 000000000..596d3ac41 --- /dev/null +++ b/src/library/tactic/expr_to_tactic.cpp @@ -0,0 +1,97 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "kernel/instantiate.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +typedef std::unordered_map expr_to_tactic_map; +expr_to_tactic_map & get_expr_to_tactic_map() { + static expr_to_tactic_map g_map; + return g_map; +} + +void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) { + get_expr_to_tactic_map().insert(mk_pair(n, fn)); +} + +tactic expr_to_tactic(environment const & env, expr const & e) { + expr const & f = get_app_fn(e); + if (is_constant(f)) { + auto const & map = get_expr_to_tactic_map(); + auto it = map.find(const_name(f)); + if (it != map.end()) { + return it->second(env, e); + } else if (auto it = env.find(const_name(f))) { + if (it->is_definition()) { + buffer locals; + get_app_rev_args(e, locals); + expr v = it->get_value(); + v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f)); + v = apply_beta(v, locals.size(), locals.data()); + return expr_to_tactic(env, v); + } + } + throw exception("failed to convert expression into tactic"); + } else if (is_lambda(f)) { + buffer locals; + get_app_rev_args(e, locals); + return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data())); + } else { + throw exception("failed to convert expression into tactic"); + } +} + +register_bin_tac::register_bin_tac(name const & n, std::function f) { + register_expr_to_tactic(n, [=](environment const & env, expr const & e) { + return f(expr_to_tactic(env, app_arg(app_fn(e))), + expr_to_tactic(env, app_arg(e))); + }); +} + +register_unary_tac::register_unary_tac(name const & n, std::function f) { + register_expr_to_tactic(n, [=](environment const & env, expr const & e) { + return f(expr_to_tactic(env, app_arg(e))); + }); +} + +static register_tac reg_id(name({"tactic", "id"}), [](environment const &, expr const &) { return id_tactic(); }); +static register_tac reg_now(name({"tactic", "now"}), [](environment const &, expr const &) { return now_tactic(); }); +static register_tac reg_fail(name({"tactic", "fail"}), [](environment const &, expr const &) { return fail_tactic(); }); +static register_tac reg_beta(name({"tactic", "beta"}), [](environment const &, expr const &) { return beta_tactic(); }); +static register_bin_tac reg_then(name({"tactic", "then_tac"}), [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); +static register_bin_tac reg_orelse(name({"tactic", "orelse_tac"}), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); +static register_unary_tac reg_repeat(name({"tactic", "repeat_tac"}), [](tactic const & t1) { return repeat(t1); }); + +// We encode the 'by' expression that is used to trigger tactic execution. +// This is a trick to avoid creating a new kind of expression. +// 'by' macros are temporary objects used by the elaborator, +// and have no semantic significance. +[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'by' expression"); } +static name g_by_name("by"); +class by_macro_cell : public macro_definition_cell { +public: + virtual name get_name() const { return g_by_name; } + virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); } + virtual optional expand(expr const &, extension_context &) const { throw_ex(); } + virtual void write(serializer &) const { throw_ex(); } +}; + +static macro_definition g_by(new by_macro_cell()); +expr mk_by(expr const & e) { + return mk_macro(g_by, 1, &e); +} + +bool is_by(expr const & e) { + return is_macro(e) && macro_def(e) == g_by; +} + +expr const & get_by_arg(expr const & e) { + lean_assert(is_by(e)); + return macro_arg(e, 0); +} +} diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h new file mode 100644 index 000000000..83767a871 --- /dev/null +++ b/src/library/tactic/expr_to_tactic.h @@ -0,0 +1,27 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" + +namespace lean { +typedef std::function expr_to_tactic_fn; +void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn); +struct register_tac { + register_tac(name const & n, expr_to_tactic_fn fn) { register_expr_to_tactic(n, fn); } +}; +struct register_bin_tac { + register_bin_tac(name const & n, std::function f); +}; +struct register_unary_tac { + register_unary_tac(name const & n, std::function f); +}; + +tactic expr_to_tactic(environment const & env, expr const & e); +expr mk_by(expr const & e); +bool is_by(expr const & e); +expr const & get_by_arg(expr const & e); +}