/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#include <string>
#include "util/rc.h"
#include "kernel/expr.h"
/*
  Kernel objects.

  We use abstract classes and virtual methods because a kernel
  frontend may need to create new objects for bookkeeping.
*/
namespace lean {
class io_state;
class object;
enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };

class object_cell {
protected:
    friend class object;
    void dealloc() { delete this; }
    MK_LEAN_RC();
    object_kind m_kind;
    /** \brief Set the opaque flag */
    virtual void set_opaque(bool ) { lean_unreachable(); } // LCOV_EXCL_LINE
public:
    object_cell(object_kind k):m_rc(1), m_kind(k) {}
    virtual ~object_cell() {}

    object_kind kind() const { return m_kind; }

    /**
        \brief Return the keyword used to define this object in a Lean
        file. The keyword is also used to identify the class of an object.
    */
    virtual char const * keyword() const = 0;

    /** \brief Return true iff object has a name. */
    virtual bool has_name() const { return false; }
    /** \brief Return object name. \pre has_name() */
    virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE

    /** \brief Has constraint level associated with it (for universal variables). */
    virtual bool has_cnstr_level() const { return false; }
    /** \brief Return the constraint level associated with the object. */
    virtual level get_cnstr_level() const { lean_unreachable(); } // LCOV_EXCL_LINE

    /** \brief Return true iff object has a type. */
    virtual bool has_type() const { return false; }
    /** \brief Return object type. \pre has_type() */
    virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE

    /** \brief Return true iff object is a definition */
    virtual bool is_definition() const { return false; }
    /** \brief Return true iff the definition is opaque. \pre is_definition() */
    virtual bool is_opaque() const { lean_unreachable(); } // LCOV_EXCL_LINE
    /** \brief Return object value. \pre is_definition() */
    virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE

    virtual bool is_axiom() const { return false; }
    virtual bool is_builtin() const { return false; }
    virtual bool is_builtin_set() const { return false; }
    virtual bool is_theorem() const { return false; }
    virtual bool is_var_decl() const { return false; }

    virtual bool in_builtin_set(expr const &) const { return false; }

    virtual unsigned get_weight() const { return 0; }

    virtual void write(serializer & ) const = 0;
    typedef void (*reader)(environment const & env, io_state const & ios, deserializer & d);
    static void register_deserializer(std::string const & k, reader rd);
    struct register_deserializer_fn {
        register_deserializer_fn(std::string const & k, reader rd) { register_deserializer(k, rd); }
    };
};

/**
   \brief Neutral objects are mainly used for bookkeeping in
   frontends built on top of the kernel.
   The kernel does *not* create neutral objects.
*/
class neutral_object_cell : public object_cell {
public:
    neutral_object_cell();
};

/**
   \brief Environment objects: definitions, theorems, axioms, universe
   variable declarations, etc.
*/
class object {
    object_cell * m_ptr;
    explicit object(object_cell * ptr):m_ptr(ptr) {}
    friend class environment_cell;
    void set_opaque(bool f) { m_ptr->set_opaque(f); }
public:
    object(object const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
    object(object && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
    ~object() { if (m_ptr) m_ptr->dec_ref(); }

    friend void swap(object & a, object & b) { std::swap(a.m_ptr, b.m_ptr); }

    object & operator=(object const & s) { LEAN_COPY_REF(s); }
    object & operator=(object && s) { LEAN_MOVE_REF(s); }

    object_kind kind() const { return m_ptr->kind(); }

    friend object mk_uvar_decl(name const & n, level const & l);
    friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
    friend object mk_theorem(name const & n, expr const & t, expr const & v);
    friend object mk_axiom(name const & n, expr const & t);
    friend object mk_var_decl(name const & n, expr const & t);
    friend object mk_neutral(neutral_object_cell * c);
    friend object mk_builtin(expr const & v);
    friend object mk_builtin_set(expr const & r);

    char const * keyword() const { return m_ptr->keyword(); }
    bool has_name() const { return m_ptr->has_name(); }
    name get_name() const { return m_ptr->get_name(); }
    bool has_type() const { return m_ptr->has_type(); }
    bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
    level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
    expr get_type() const { return m_ptr->get_type(); }
    bool is_definition() const { return m_ptr->is_definition(); }
    bool is_opaque() const { return m_ptr->is_opaque(); }
    expr get_value() const { return m_ptr->get_value(); }
    unsigned get_weight() const { return m_ptr->get_weight(); }

    bool is_axiom() const { return m_ptr->is_axiom(); }
    bool is_theorem() const { return m_ptr->is_theorem(); }
    bool is_var_decl() const { return m_ptr->is_var_decl(); }
    bool is_builtin() const { return m_ptr->is_builtin(); }
    bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
    bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }

    void write(serializer & s) const { m_ptr->write(s); }

    object_cell const * cell() const { return m_ptr; }
};

inline optional<object> none_object() { return optional<object>(); }
inline optional<object> some_object(object const & o) { return optional<object>(o); }
inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); }

object mk_uvar_decl(name const & n, level const & l);
object mk_builtin(expr const & v);
object mk_builtin_set(expr const & r);
object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
object mk_theorem(name const & n, expr const & t, expr const & v);
object mk_axiom(name const & n, expr const & t);
object mk_var_decl(name const & n, expr const & t);
inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); }

void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d);

/**
   \brief Helper function whether we should unfold an definition or not.

   1- We unfold definitions.
   2- We never unfold theorems.
   3- We unfold opaque definitions if \c unfold_opaque == true
*/
inline bool should_unfold(object const & obj, bool unfold_opaque) {
    return obj.is_definition() && !obj.is_theorem() && (unfold_opaque || !obj.is_opaque());
}
inline bool should_unfold(optional<object> const & obj, bool unfold_opaque) {
    return obj && should_unfold(*obj, unfold_opaque);
}
inline bool should_unfold(optional<object> const & obj) {
    return should_unfold(obj, false);
}
}