feat(library/tactic): add tactic_state

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)

src/CMakeLists.txt

@@ -328,8 +328,8 @@ add_subdirectory(kernel/hits)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:hits>)
 add_subdirectory(library)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
-# add_subdirectory(library/tactic)
-# set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
+add_subdirectory(library/tactic)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
 add_subdirectory(library/definitional)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
 # add_subdirectory(library/blast)

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();

src/library/tactic/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(tactic OBJECT tactic_state.cpp init_module.cpp)

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();
+}
+}

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();
+}

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<expr> 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<expr> 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<expr> 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<vm_tactic_state*>(to_external(o)));
+    return static_cast<vm_tactic_state*>(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() {
+}
+}

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<expr>      m_goals;
+    friend class tactic_state;
+    void dealloc();
+public:
+    tactic_state_cell(environment const & env, options const & o, metavar_context const & ctx, list<expr> 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<tactic_state>;
+public:
+    tactic_state(environment const & env, options const & o, metavar_context const & ctx, list<expr> 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<expr> 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<expr> const & gs);
+tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list<expr> 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();
+}