From a03841c18bbd7a39d1830d195ded7f874f5310d9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2013 10:44:53 -0800 Subject: [PATCH] feat(tactic): refine tactic API Signed-off-by: Leonardo de Moura --- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/justification_builder.h | 4 ++-- src/library/tactic/proof_builder.h | 4 ++-- src/library/tactic/proof_state.h | 8 +++++++ src/library/tactic/tactic.cpp | 26 ++++++++++++++++++++++ src/library/tactic/tactic.h | 24 +++++++++++++++----- 6 files changed, 57 insertions(+), 11 deletions(-) create mode 100644 src/library/tactic/tactic.cpp diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index ad9dbb96f..fe30ad2a0 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(tactic goal.cpp) +add_library(tactic goal.cpp tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/justification_builder.h b/src/library/tactic/justification_builder.h index b94a2c7ce..33e14e300 100644 --- a/src/library/tactic/justification_builder.h +++ b/src/library/tactic/justification_builder.h @@ -18,7 +18,7 @@ class justification_builder_cell { MK_LEAN_RC(); public: virtual ~justification_builder_cell() {} - virtual justification operator()(name const & n, justification const & j, assignment const & a) const = 0; + virtual justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const = 0; }; class justification_builder { @@ -33,6 +33,6 @@ public: justification_builder & operator=(justification_builder const & s) { LEAN_COPY_REF(justification_builder, s); } justification_builder & operator=(justification_builder && s) { LEAN_MOVE_REF(justification_builder, s); } - justification operator()(name const & n, justification const & j, assignment const & a) const { return m_ptr->operator()(n, j, a); } + justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const { return m_ptr->operator()(n, j, env, a); } }; } diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index c7b2ed863..74b5551c2 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -21,7 +21,7 @@ class proof_builder_cell { MK_LEAN_RC(); public: virtual ~proof_builder_cell() {} - virtual expr operator()(proof_map const & p, assignment const & a) const = 0; + virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const = 0; }; class proof_builder { @@ -36,6 +36,6 @@ public: proof_builder & operator=(proof_builder const & s) { LEAN_COPY_REF(proof_builder, s); } proof_builder & operator=(proof_builder && s) { LEAN_MOVE_REF(proof_builder, s); } - expr operator()(proof_map const & p, assignment const & a) const { return m_ptr->operator()(p, a); } + expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_ptr->operator()(p, env, a); } }; } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 701299c68..b6e280bf4 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -12,10 +12,18 @@ Author: Leonardo de Moura namespace lean { class proof_state { + environment const m_env; list> m_goals; metavar_env m_menv; proof_builder m_proof_builder; justification_builder m_justification_builder; public: + proof_state(environment const & env, list> const & gs, metavar_env const & menv, proof_builder const & p, justification_builder const & j): + m_env(env), m_goals(gs), m_menv(menv), m_proof_builder(p), m_justification_builder(j) {} + environment const & get_environment() const { return m_env; } + list> const & get_goals() const { return m_goals; } + metavar_env const & get_menv() const { return m_menv; } + proof_builder const & get_proof_builder() const { return m_proof_builder; } + justification_builder const & get_justification_builder() const { return m_justification_builder; } }; } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp new file mode 100644 index 000000000..86fcbb72d --- /dev/null +++ b/src/library/tactic/tactic.cpp @@ -0,0 +1,26 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/tactic/tactic.h" + +namespace lean { +tactic_result::~tactic_result() { +} +void tactic_result::interrupt() { + m_result = true; +} + +tactic_cell::~tactic_cell() { +} + +tactic & tactic::operator=(tactic const & s) { + LEAN_COPY_REF(tactic, s); +} + +tactic & tactic::operator=(tactic && s) { + LEAN_MOVE_REF(tactic, s); +} +} diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 099cfc85d..9bd25490e 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -6,16 +6,28 @@ Author: Leonardo de Moura */ #pragma once #include -#include "util/lazy_list.h" +#include #include "library/tactic/proof_state.h" namespace lean { +class tactic_result { + volatile bool m_result; +public: + tactic_result():m_result(false) {} + bool interrupted() const { return m_result; } + virtual ~tactic_result(); + virtual void interrupt(); + virtual proof_state next() = 0; +}; + +typedef std::unique_ptr tactic_result_ref; + class tactic_cell { void dealloc() { delete this; } MK_LEAN_RC(); public: - virtual ~tactic_cell() {} - virtual lazy_list operator()(proof_state const & p) const = 0; + virtual ~tactic_cell(); + virtual tactic_result_ref operator()(proof_state const & p) const = 0; }; class tactic { @@ -27,10 +39,10 @@ public: tactic(tactic && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~tactic() { if (m_ptr) m_ptr->dec_ref(); } friend void swap(tactic & a, tactic & b) { std::swap(a.m_ptr, b.m_ptr); } - tactic & operator=(tactic const & s) { LEAN_COPY_REF(tactic, s); } - tactic & operator=(tactic && s) { LEAN_MOVE_REF(tactic, s); } + tactic & operator=(tactic const & s); + tactic & operator=(tactic && s); - lazy_list operator()(proof_state const & p) const { return m_ptr->operator()(p); } + tactic_result_ref operator()(proof_state const & p) const { return m_ptr->operator()(p); } }; }