From 6b8b5f3dd8a866227356cffbeec4cbeec9928861 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Jul 2014 08:06:28 -0700 Subject: [PATCH] feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure Signed-off-by: Leonardo de Moura --- library/standard/tactic.lean | 48 +++++++----- src/library/tactic/expr_to_tactic.cpp | 101 ++++++++++++++++++-------- src/library/tactic/expr_to_tactic.h | 7 +- src/library/tactic/tactic.cpp | 8 -- src/library/tactic/tactic.h | 6 -- 5 files changed, 108 insertions(+), 62 deletions(-) diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean index a0d264e13..60583a5b1 100644 --- a/library/standard/tactic.lean +++ b/library/standard/tactic.lean @@ -1,36 +1,48 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura -import logic string +import logic string num using string +using num namespace tactic -- This is just a trick to embed the 'tactic language' as a -- Lean expression. We should view 'tactic' as automation -- that when execute produces a term. --- tactic_value is just a "dummy" for creating the "fake" --- definitions +-- builtin_tactic is just a "dummy" for creating the +-- definitions that are actually implemented in C++ inductive tactic : Type := -| tactic_value : tactic +| builtin_tactic : tactic -- 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' into a tactic that sythesizes a term -definition and_then (t1 t2 : tactic) : tactic := tactic_value -definition or_else (t1 t2 : tactic) : tactic := tactic_value -definition repeat (t : tactic) : tactic := tactic_value -definition now : tactic := tactic_value -definition assumption : tactic := tactic_value -definition state : tactic := tactic_value -definition fail : tactic := tactic_value -definition id : tactic := tactic_value -definition beta : tactic := tactic_value -definition apply {B : Type} (b : B) : tactic := tactic_value -definition unfold {B : Type} (b : B) : tactic := tactic_value -definition exact {B : Type} (b : B) : tactic := tactic_value -definition trace (s : string) : tactic := tactic_value +definition and_then (t1 t2 : tactic) : tactic := builtin_tactic +definition or_else (t1 t2 : tactic) : tactic := builtin_tactic +definition append (t1 t2 : tactic) : tactic := builtin_tactic +definition interleave (t1 t2 : tactic) : tactic := builtin_tactic +definition par (t1 t2 : tactic) : tactic := builtin_tactic +definition repeat (t : tactic) : tactic := builtin_tactic +definition at_most (t : tactic) (k : num) : tactic := builtin_tactic +definition focus_at (t : tactic) (i : num) : tactic := builtin_tactic +definition try_for (t : tactic) (ms : num) : tactic := builtin_tactic +definition now : tactic := builtin_tactic +definition assumption : tactic := builtin_tactic +definition state : tactic := builtin_tactic +definition fail : tactic := builtin_tactic +definition id : tactic := builtin_tactic +definition beta : tactic := builtin_tactic +definition apply {B : Type} (b : B) : tactic := builtin_tactic +definition unfold {B : Type} (b : B) : tactic := builtin_tactic +definition exact {B : Type} (b : B) : tactic := builtin_tactic +definition trace (s : string) : tactic := builtin_tactic infixl `;`:200 := and_then infixl `|`:100 := or_else -notation `!`:max t:max := repeat t +notation `!` t:max := repeat t notation `⟦` t `⟧` := apply t +definition try (t : tactic) : tactic := t | id +notation `?` t:max := try t +definition repeat1 (t : tactic) : tactic := t ; !t +definition focus (t : tactic) : tactic := focus_at t 0 +definition determ (t : tactic) : tactic := at_most t 1 end diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 41d5a5584..b7caa93b0 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -6,9 +6,11 @@ Author: Leonardo de Moura */ #include #include +#include "util/sstream.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" #include "library/string.h" +#include "library/num.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/apply_tactic.h" @@ -23,26 +25,55 @@ 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(type_checker & tc, expr const & e, pos_info_provider const * p) { - expr f = get_app_fn(tc.whnf(e)); - if (is_constant(f)) { +static name g_tac("tactic"), g_builtin_tac(g_tac, "builtin_tactic"); +static name g_tac_name(g_tac, "tactic"), g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then"); +static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat"); +static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name)); +static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name)); +static expr g_tac_type(Const(g_tac_name)); +expr const & get_exact_tac_fn() { return g_exact_tac_fn; } +expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; } +expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; } +expr const & get_repeat_tac_fn() { return g_repeat_tac_fn; } +expr const & get_tactic_type() { return g_tac_type; } + +static void throw_failed(expr const & e) { + throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); +} + +/** \brief Return true if v is the constant tactic.builtin_tactic or the constant function that returns tactic.builtin_tactic */ +static bool is_builtin_tactic(expr const & v) { + if (is_lambda(v)) + return is_builtin_tactic(binding_body(v)); + else if (is_constant(v) && const_name(v) == g_builtin_tac) + return true; + else + return false; +} + +tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) { + e = tc.whnf(e); + expr f = get_app_fn(e); + if (!is_constant(f)) + throw_failed(e); + optional it = tc.env().find(const_name(f)); + if (!it || !it->is_definition()) + throw_failed(e); + expr v = it->get_value(); + if (is_builtin_tactic(v)) { auto const & map = get_expr_to_tactic_map(); - auto it = map.find(const_name(f)); - if (it != map.end()) { - return it->second(tc, e, p); - } else if (auto it = tc.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(tc, v, p); - } - } - throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); + auto it2 = map.find(const_name(f)); + if (it2 != map.end()) + return it2->second(tc, e, p); + else + throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << const_name(f) << "' was not found"); } else { - throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); + // unfold definition + buffer locals; + get_app_rev_args(e, locals); + v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f)); + v = apply_beta(v, locals.size(), locals.data()); + return expr_to_tactic(tc, v, p); } } @@ -80,16 +111,23 @@ register_unary_tac::register_unary_tac(name const & n, std::function f) { + register_expr_to_tactic(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { + buffer args; + get_app_args(e, args); + if (args.size() != 2) + throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments"); + tactic t = expr_to_tactic(tc, args[0], p); + optional k = to_num(args[1]); + if (!k) + k = to_num(tc.whnf(args[1])); + if (!k) + throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral"); + if (!k->is_unsigned_int()) + throw expr_to_tactic_exception(e, "invalid tactic, second argument does not fit in a machine unsigned integer"); + return f(t, k->get_unsigned_int()); + }); +} static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); }); static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); }); @@ -97,6 +135,9 @@ static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { retu static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); }); static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); }); static register_bin_tac reg_then(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); +static register_bin_tac reg_append(name(g_tac, "append"), [](tactic const & t1, tactic const & t2) { return append(t1, t2); }); +static register_bin_tac reg_interleave(name(g_tac, "interleave"), [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); }); +static register_bin_tac reg_par(name(g_tac, "par"), [](tactic const & t1, tactic const & t2) { return par(t1, t2); }); static register_bin_tac reg_orelse(g_or_else_tac_name, [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); static register_unary_tac reg_repeat(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); }); static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) { @@ -130,7 +171,9 @@ static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr co else return unfold_tactic(const_name(id)); }); - +static register_unary_num_tac reg_at_most(name(g_tac, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); }); +static register_unary_num_tac reg_focus_at(name(g_tac, "focus_at"), [](tactic const & t, unsigned k) { return focus(t, k); }); +static register_unary_num_tac reg_try_for(name(g_tac, "try_for"), [](tactic const & t, unsigned k) { return try_for(t, k); }); // We encode the 'by' expression that is used to trigger tactic execution. // This is a trick to avoid creating a new kind of expression. diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index ef62ead9e..0584357a4 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -10,7 +10,9 @@ Author: Leonardo de Moura namespace lean { class expr_to_tactic_exception : public tactic_exception { -public: expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {} +public: + expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {} + expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {} }; typedef std::function expr_to_tactic_fn; @@ -27,6 +29,9 @@ struct register_bin_tac { struct register_unary_tac { register_unary_tac(name const & n, std::function f); }; +struct register_unary_num_tac { + register_unary_num_tac(name const & n, std::function f); +}; expr const & get_tactic_type(); expr const & get_exact_tac_fn(); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 51c4290bd..5ad74634b 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -447,14 +447,11 @@ static int tactic_append(lua_State * L) { return push_tactic(L, append( static int tactic_interleave(lua_State * L) { return push_tactic(L, interleave(to_tactic(L, 1), to_tactic(L, 2))); } static int tactic_par(lua_State * L) { return push_tactic(L, par(to_tactic(L, 1), to_tactic(L, 2))); } static int tactic_repeat(lua_State * L) { return push_tactic(L, repeat(to_tactic(L, 1))); } -static int tactic_repeat1(lua_State * L) { return push_tactic(L, repeat1(to_tactic(L, 1))); } static int tactic_repeat_at_most(lua_State * L) { return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); } static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); } -static int tactic_determ(lua_State * L) { return push_tactic(L, determ(to_tactic(L, 1))); } static int tactic_suppress_trace(lua_State * L) { return push_tactic(L, suppress_trace(to_tactic(L, 1))); } static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); } static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); } -static int tactic_try(lua_State * L) { return push_tactic(L, orelse(to_tactic(L, 1), id_tactic())); } static int tactic_focus(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 1) @@ -528,9 +525,7 @@ static const struct luaL_Reg tactic_m[] = { {"append", safe_function}, {"interleave", safe_function}, {"par", safe_function}, - {"determ", safe_function}, {"repeat", safe_function}, - {"repeat1", safe_function}, {"repeat_at_most", safe_function}, {"take", safe_function}, {"suppress_trace", safe_function}, @@ -571,15 +566,12 @@ void open_tactic(lua_State * L) { SET_GLOBAL_FUN(nary_tactic, "Par"); SET_GLOBAL_FUN(tactic_repeat, "Repeat"); SET_GLOBAL_FUN(tactic_repeat_at_most, "RepeatAtMost"); - SET_GLOBAL_FUN(tactic_repeat1, "Repeat1"); SET_GLOBAL_FUN(mk_lua_cond_tactic, "Cond"); SET_GLOBAL_FUN(mk_lua_when_tactic, "When"); - SET_GLOBAL_FUN(tactic_try, "Try"); SET_GLOBAL_FUN(tactic_try_for, "TryFor"); SET_GLOBAL_FUN(tactic_take, "Take"); SET_GLOBAL_FUN(tactic_using_params, "Using"); SET_GLOBAL_FUN(tactic_using_params, "UsingParams"); - SET_GLOBAL_FUN(tactic_determ, "Determ"); SET_GLOBAL_FUN(tactic_focus, "Focus"); } } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 2fb52a192..909efcf8e 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -102,10 +102,6 @@ inline tactic par(tactic const & t1, tactic const & t2) { return par(t1, t2, 1); \brief Return a tactic that keeps applying \c t until it fails. */ tactic repeat(tactic const & t); -/** - \brief Similar to \c repeat, but applies \c t at least once. -*/ -inline tactic repeat1(tactic const & t) { return then(t, repeat(t)); } /** \brief Similar to \c repeat, but execute \c t at most \c k times. @@ -119,8 +115,6 @@ tactic repeat_at_most(tactic const & t, unsigned k); k elements from the sequence produced by \c t. */ tactic take(tactic const & t, unsigned k); -/** \brief Syntax sugar for take(t, 1) */ -inline tactic determ(tactic const & t) { return take(t, 1); } typedef std::function proof_state_pred; // NOLINT /** \brief Return a tactic that applies the predicate \c p to the input state.