From cf073f5ed093bb1d69c8ed167b0035ced509d7a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jun 2016 15:12:22 -0700 Subject: [PATCH] feat(library/tactic): add tactic_state --- library/init/meta/tactic.lean | 21 +++++++++ src/CMakeLists.txt | 4 +- src/init/init.cpp | 6 +-- src/library/tactic/CMakeLists.txt | 1 + src/library/tactic/init_module.cpp | 16 +++++++ src/library/tactic/init_module.h | 12 +++++ src/library/tactic/tactic_state.cpp | 68 +++++++++++++++++++++++++++++ src/library/tactic/tactic_state.h | 61 ++++++++++++++++++++++++++ 8 files changed, 184 insertions(+), 5 deletions(-) create mode 100644 library/init/meta/tactic.lean create mode 100644 src/library/tactic/CMakeLists.txt create mode 100644 src/library/tactic/init_module.cpp create mode 100644 src/library/tactic/init_module.h create mode 100644 src/library/tactic/tactic_state.cpp create mode 100644 src/library/tactic/tactic_state.h diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean new file mode 100644 index 0000000000..b13945451a --- /dev/null +++ b/library/init/meta/tactic.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2016 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.base_tactic init.meta.environment + +meta_constant tactic_state : Type₁ + +namespace tactic_state +meta_constant env : tactic_state → environment +end tactic_state + +open tactic + +meta_definition tactic [reducible] (A : Type) := base_tactic tactic_state A + +meta_definition get_env : tactic environment := +do s ← read, + return (tactic_state.env s) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 726c843e3d..fca9204609 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -328,8 +328,8 @@ add_subdirectory(kernel/hits) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library) set(LEAN_OBJS ${LEAN_OBJS} $) -# add_subdirectory(library/tactic) -# set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/tactic) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/definitional) set(LEAN_OBJS ${LEAN_OBJS} $) # add_subdirectory(library/blast) diff --git a/src/init/init.cpp b/src/init/init.cpp index f2aa1b17e9..6e60b1ecf6 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "kernel/hits/hits.h" #include "library/init_module.h" // #include "library/blast/init_module.h" -// #include "library/tactic/init_module.h" +#include "library/tactic/init_module.h" #include "library/definitional/init_module.h" #include "library/print.h" #include "library/vm/init_module.h" @@ -38,7 +38,7 @@ void initialize() { initialize_vm_core_module(); initialize_library_module(); initialize_compiler_module(); - // initialize_tactic_module(); + initialize_tactic_module(); // initialize_blast_module(); initialize_definitional_module(); initialize_frontend_lean_module(); @@ -50,7 +50,7 @@ void finalize() { finalize_frontend_lean_module(); finalize_definitional_module(); // finalize_blast_module(); - // finalize_tactic_module(); + finalize_tactic_module(); finalize_compiler_module(); finalize_library_module(); finalize_vm_core_module(); diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt new file mode 100644 index 0000000000..02a7fa203c --- /dev/null +++ b/src/library/tactic/CMakeLists.txt @@ -0,0 +1 @@ +add_library(tactic OBJECT tactic_state.cpp init_module.cpp) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp new file mode 100644 index 0000000000..a69e10052f --- /dev/null +++ b/src/library/tactic/init_module.cpp @@ -0,0 +1,16 @@ +/* +Copyright (c) 2016 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_state.h" + +namespace lean { +void initialize_tactic_module() { + initialize_tactic_state(); +} +void finalize_tactic_module() { + finalize_tactic_state(); +} +} diff --git a/src/library/tactic/init_module.h b/src/library/tactic/init_module.h new file mode 100644 index 0000000000..005deb1775 --- /dev/null +++ b/src/library/tactic/init_module.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2016 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_tactic_module(); +void finalize_tactic_module(); +} diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp new file mode 100644 index 0000000000..9e6f1a666c --- /dev/null +++ b/src/library/tactic/tactic_state.cpp @@ -0,0 +1,68 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/vm/vm_environment.h" +#include "library/tactic/tactic_state.h" + +namespace lean { +void tactic_state_cell::dealloc() { + this->~tactic_state_cell(); + get_vm_allocator().deallocate(sizeof(tactic_state_cell), this); +} + +tactic_state::tactic_state(environment const & env, options const & o, metavar_context const & ctx, list const & gs) { + m_ptr = new (get_vm_allocator().allocate(sizeof(tactic_state_cell))) tactic_state_cell(env, o, ctx, gs); +} + +tactic_state set_options(tactic_state const & s, options const & o) { + return tactic_state(s.env(), o, s.mctx(), s.goals()); +} + +tactic_state set_env(tactic_state const & s, environment const & env) { + return tactic_state(env, s.get_options(), s.mctx(), s.goals()); +} + +tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx) { + return tactic_state(s.env(), s.get_options(), mctx, s.goals()); +} + +tactic_state set_goals(tactic_state const & s, list const & gs) { + return tactic_state(s.env(), s.get_options(), s.mctx(), gs); +} + +tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list const & gs) { + return tactic_state(s.env(), s.get_options(), mctx, gs); +} + +struct vm_tactic_state : public vm_external { + tactic_state m_val; + vm_tactic_state(tactic_state const & v):m_val(v) {} + virtual void dealloc() override { + this->~vm_tactic_state(); get_vm_allocator().deallocate(sizeof(vm_tactic_state), this); + } +}; + +tactic_state const & to_tactic_state(vm_obj const & o) { + lean_assert(is_external(o)); + lean_assert(dynamic_cast(to_external(o))); + return static_cast(to_external(o))->m_val; +} + +vm_obj to_obj(tactic_state const & s) { + return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_tactic_state))) vm_tactic_state(s)); +} + +vm_obj tactic_state_env(vm_obj const & s) { + return to_obj(to_tactic_state(s).env()); +} + +void initialize_tactic_state() { + DECLARE_VM_BUILTIN(name({"tactic_state", "env"}), tactic_state_env); +} + +void finalize_tactic_state() { +} +} diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h new file mode 100644 index 0000000000..31de944b76 --- /dev/null +++ b/src/library/tactic/tactic_state.h @@ -0,0 +1,61 @@ +/* +Copyright (c) 2016 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/vm/vm.h" +#include "kernel/environment.h" +#include "library/metavar_context.h" + +namespace lean { +class tactic_state_cell { + MK_LEAN_RC(); + environment m_env; + options m_options; + metavar_context m_mctx; + list m_goals; + friend class tactic_state; + void dealloc(); +public: + tactic_state_cell(environment const & env, options const & o, metavar_context const & ctx, list const & gs): + m_rc(1), m_env(env), m_options(o), m_mctx(ctx), m_goals(gs) {} +}; + +class tactic_state { +private: + tactic_state_cell * m_ptr; + tactic_state_cell * steal_ptr() { tactic_state_cell * r = m_ptr; m_ptr = nullptr; return r; } + friend class optional; +public: + tactic_state(environment const & env, options const & o, metavar_context const & ctx, list const & gs); + tactic_state(tactic_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + tactic_state(tactic_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~tactic_state() { if (m_ptr) m_ptr->dec_ref(); } + + tactic_state_cell * raw() const { return m_ptr; } + options const & get_options() const { lean_assert(m_ptr); return m_ptr->m_options; } + environment const & env() const { lean_assert(m_ptr); return m_ptr->m_env; } + metavar_context const & mctx() const { lean_assert(m_ptr); return m_ptr->m_mctx; } + list const & goals() const { lean_assert(m_ptr); return m_ptr->m_goals; } + + tactic_state & operator=(tactic_state const & s) { LEAN_COPY_REF(s); } + tactic_state & operator=(tactic_state && s) { LEAN_MOVE_REF(s); } + + friend void swap(tactic_state & a, tactic_state & b) { std::swap(a.m_ptr, b.m_ptr); } + friend bool is_eqp(tactic_state const & a, tactic_state const & b) { return a.m_ptr == b.m_ptr; } +}; + +tactic_state set_options(tactic_state const & s, options const & o); +tactic_state set_env(tactic_state const & s, environment const & env); +tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx); +tactic_state set_goals(tactic_state const & s, list const & gs); +tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list const & gs); + +tactic_state const & to_tactic_state(vm_obj const & o); +vm_obj to_obj(tactic_state const & s); + +void initialize_tactic_state(); +void finalize_tactic_state(); +}