checkpoint

src/library/blast/CMakeLists.txt

@@ -1 +1 @@
-add_library(blast OBJECT state.cpp expr.cpp)
+add_library(blast OBJECT state.cpp expr.cpp hypothesis.cpp)

src/library/blast/goal.h

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/rb_map.h"
+#include "library/blast/expr.h"
+#include "library/blast/hypothesis.h"
+
+namespace lean {
+namespace blast {
+class goal {
+    typedef rb_map<unsigned, hypothesis, unsigned_cmp> context;
+    friend class state;
+    unsigned m_next;
+    context  m_context;
+    expr const & mk_lref(expr const & type, optional<expr> const & value);
+public:
+    goal():m_next(0) {}
+    hypothesis const * get(unsigned idx) const { return m_context.find(idx); }
+    hypothesis const * get(expr const & e) const {
+        lean_assert(is_lref(e));
+        return get(get_lmindex(e));
+    }
+};
+}}

src/library/blast/hypothesis.cpp

@@ -0,0 +1,50 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/blast/hypothesis.h"
+
+namespace lean {
+namespace blast {
+struct justification_idx_gen {
+    unsigned       m_next_idx;
+    list<unsigned> m_free_list;
+public:
+    justification_idx_gen():m_next_idx(0) {}
+    void recycle(unsigned idx) {
+        m_free_list = cons(idx, m_free_list);
+    }
+    unsigned next() {
+        if (m_free_list) {
+            unsigned r = head(m_free_list);
+            m_free_list = tail(m_free_list);
+            return r;
+        } else {
+            unsigned r = m_next_idx;
+            m_next_idx++;
+            return r;
+        }
+    }
+};
+
+MK_THREAD_LOCAL_GET_DEF(justification_idx_gen, get_justification_idx_gen)
+
+justification_cell::justification_cell():m_rc(0) {
+    m_idx = get_justification_idx_gen().next();
+}
+
+void justification_cell::dealloc() {
+    get_justification_idx_gen().recycle(m_idx);
+    delete this;
+}
+
+justification::justification():m_ptr(nullptr) {}
+justification::justification(justification_cell & ptr):m_ptr(&ptr) { if (m_ptr) m_ptr->inc_ref(); }
+justification::justification(justification const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+justification::justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+justification::~justification() { if (m_ptr) m_ptr->dec_ref(); }
+justification & justification::operator=(justification const & s) { LEAN_COPY_REF(s); }
+justification & justification::operator=(justification && s) { LEAN_MOVE_REF(s); }
+}}

src/library/blast/hypothesis.h

@@ -0,0 +1,66 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/rc.h"
+#include "util/rb_tree.h"
+#include "kernel/expr.h"
+
+namespace lean {
+namespace blast {
+class hypothesis;
+class state;
+class goal;
+
+class justification_cell {
+    MK_LEAN_RC();
+    unsigned m_idx;
+    void dealloc();
+public:
+    justification_cell();
+    virtual ~justification_cell() {}
+    virtual expr to_expr(hypothesis const &) const = 0;
+    /** \brief Return thread local unique identifier associated with justification object */
+    unsigned get_idx() const { return m_idx; }
+};
+
+class justification {
+    justification_cell * m_ptr;
+public:
+    justification();
+    justification(justification_cell & c);
+    justification(justification const & s);
+    justification(justification && s);
+    ~justification();
+
+    justification & operator=(justification const & s);
+    justification & operator=(justification && s);
+    expr to_expr(hypothesis const & h) const { return m_ptr->to_expr(h); }
+};
+
+typedef rb_tree<unsigned, unsigned_cmp> hypothesis_set;
+
+class hypothesis {
+    friend class goal;
+    bool           m_active;
+    unsigned       m_depth;
+    hypothesis_set m_backward_deps;
+    hypothesis_set m_forward_deps;
+    expr           m_type;
+    optional<expr> m_value;
+    justification  m_jst;
+public:
+    hypothesis();
+    bool is_active() const { return m_active; }
+    unsigned get_depth() const { return m_depth; }
+    hypothesis_set const & get_backward_deps() const { return m_backward_deps; }
+    hypothesis_set const & get_forward_deps() const { return m_forward_deps; }
+    expr const & get_type() const { return m_type; }
+    optional<expr> const & get_value() const { return m_value; }
+    justification const & get_justification() const { return m_jst; }
+};
+}
+}

src/library/blast/state.h

@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
-
 namespace lean {
 namespace blast {
 class state {