max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(kernel): proper constant_info and declaration objects for quot type

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-28 13:43:44 -07:00
parent a178f181a8
commit 101886ffae
10 changed files with 61 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/declaration.lean
View file

@ -60,7 +60,7 @@ inductive declaration
| axiom_decl (val : axiom_val)
| defn_decl (val : definition_val)
| thm_decl (val : theorem_val)
| quot_decl (id : name)
| quot_decl
| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `meta`
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool)

2
src/frontends/lean/builtin_cmds.cpp
View file

@ -383,7 +383,7 @@ static environment help_cmd(parser & p) {
}
static environment init_quot_cmd(parser & p) {
return module::add_quot(p.env());
return module::add(p.env(), mk_quot_decl());
}
/*

18
src/kernel/declaration.cpp
View file

@ -59,6 +59,13 @@ theorem_val::theorem_val(name const & n, level_param_names const & lparams, expr
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
}
quot_val::quot_val(name const & n, level_param_names const & lparams, expr const & type, quot_kind k):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(k));
}
quot_kind quot_val::get_quot_kind() const { return static_cast<quot_kind>(cnstr_scalar<unsigned char>(raw(), sizeof(object*))); }
recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs):
object_ref(mk_cnstr(0, cnstr, nat(nfields), rhs)) {
}
@ -166,9 +173,8 @@ declaration mk_mutual_definitions(definition_vals const & ds) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::MutualDefinition), ds));
}
declaration mk_quot_decl(name const & n) {
inc(n.raw());
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Quot), n.raw()));
declaration mk_quot_decl() {
return declaration(box(static_cast<unsigned>(declaration_kind::Quot)));
}
inductive_type::inductive_type(name const & id, expr const & type, constructors const & cnstrs):
@ -198,6 +204,10 @@ constant_info::constant_info(definition_val const & v):
object_ref(mk_cnstr(static_cast<unsigned>(constant_info_kind::Definition), v)) {
}
constant_info::constant_info(quot_val const & v):
object_ref(mk_cnstr(static_cast<unsigned>(constant_info_kind::Quot), v)) {
}
static reducibility_hints * g_opaque = nullptr;
reducibility_hints const & constant_info::get_hints() const {
@ -212,8 +222,8 @@ bool constant_info::is_meta() const {
case constant_info_kind::Axiom: return to_axiom_val().is_meta();
case constant_info_kind::Definition: return to_definition_val().is_meta();
case constant_info_kind::Theorem: return false;
case constant_info_kind::Inductive: return false; // TODO(Leo): to_inductive_val().is_meta();
case constant_info_kind::Quot: return false;
case constant_info_kind::Inductive: return false; // TODO(Leo): to_inductive_val().is_meta();
case constant_info_kind::Constructor: return false; // TODO(Leo): to_constructor_val().is_meta();
case constant_info_kind::Recursor: return false; // TODO(Leo): to_recursor_val().is_meta();
}

21
src/kernel/declaration.h
View file

@ -181,7 +181,7 @@ public:
/* low-level constructors */
explicit declaration(object * o):object_ref(o) {}
explicit declaration(object_ref const & o):object_ref(o) {}
declaration_kind kind() const { return static_cast<declaration_kind>(cnstr_tag(raw())); }
declaration_kind kind() const { return static_cast<declaration_kind>(obj_tag(raw())); }
declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; }
declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; }
@ -223,7 +223,7 @@ declaration mk_theorem(name const & n, level_param_names const & params, expr co
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta = false);
declaration mk_mutual_definitions(definition_vals const & ds);
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta);
declaration mk_quot_decl(name const & n);
declaration mk_quot_decl();
/** \brief Return true iff \c e depends on meta-declarations */
bool use_meta(environment const & env, expr const & e);
@ -348,6 +348,8 @@ public:
bool is_meta() const;
};
enum class quot_kind { Type, Mk, Lift, Ind };
/*
inductive quot_kind
| type -- `quot`
@ -358,6 +360,19 @@ inductive quot_kind
structure quot_val extends constant_val :=
(kind : quot_kind)
*/
class quot_val : public object_ref {
public:
quot_val(name const & n, level_param_names const & lparams, expr const & type, quot_kind k);
quot_val(quot_val const & other):object_ref(other) {}
quot_val(quot_val && other):object_ref(other) {}
quot_val & operator=(quot_val const & other) { object_ref::operator=(other); return *this; }
quot_val & operator=(quot_val && other) { object_ref::operator=(other); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
expr const & get_type() const { return to_constant_val().get_type(); }
quot_kind get_quot_kind() const;
};
/*
/-- Information associated with constant declarations. -/
@ -379,8 +394,10 @@ public:
constant_info();
constant_info(declaration const & d);
constant_info(definition_val const & v);
constant_info(quot_val const & v);
constant_info(constant_info const & other):object_ref(other) {}
constant_info(constant_info && other):object_ref(other) {}
constant_info_kind kind() const { return static_cast<constant_info_kind>(cnstr_tag(raw())); }
constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; }

19
src/kernel/environment.cpp
View file

@ -51,14 +51,6 @@ bool environment::is_builtin(name const & n) const {
return m_header->is_builtin(*this, n) || (m_quot_initialized && quot_is_decl(n));
}
environment environment::add_quot() const {
if (m_quot_initialized)
return *this;
environment new_env = quot_declare(*this);
new_env.m_quot_initialized = true;
return new_env;
}
static void check_no_metavar(environment const & env, name const & n, expr const & e) {
if (has_metavar(e))
throw declaration_has_metavars_exception(env, n, e);
@ -109,7 +101,7 @@ environment environment::add_axiom(declaration const & d, bool check) const {
axiom_val const & v = d.to_axiom_val();
if (check)
check_constant_val(*this, v.to_constant_val(), !d.is_meta());
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
return add(constant_info(d));
}
environment environment::add_definition(declaration const & d, bool check) const {
@ -122,7 +114,7 @@ environment environment::add_definition(declaration const & d, bool check) const
type_checker checker(*this, memoize, non_meta_only);
check_constant_val(*this, v.to_constant_val(), checker);
}
environment new_env(*this, insert(m_constants, v.get_name(), constant_info(d)));
environment new_env = add(constant_info(d));
if (check) {
bool memoize = true; bool non_meta_only = false;
type_checker checker(new_env, memoize, non_meta_only);
@ -140,7 +132,7 @@ environment environment::add_definition(declaration const & d, bool check) const
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
return add(constant_info(d));
}
}
@ -155,7 +147,7 @@ environment environment::add_theorem(declaration const & d, bool check) const {
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
return add(constant_info(d));
}
environment environment::add_mutual(declaration const & d, bool check) const {
@ -173,7 +165,7 @@ environment environment::add_mutual(declaration const & d, bool check) const {
/* Add declarations */
environment new_env = *this;
for (definition_val const & v : vs) {
new_env.m_constants.insert(v.get_name(), constant_info(v));
new_env.add_core(constant_info(v));
}
/* Check actual definitions */
if (check) {
@ -194,6 +186,7 @@ environment environment::add(declaration const & d, bool check) const {
case declaration_kind::Definition: return add_definition(d, check);
case declaration_kind::Theorem: return add_theorem(d, check);
case declaration_kind::MutualDefinition: return add_mutual(d, check);
case declaration_kind::Quot: return add_quot();
default:
// NOT IMPLEMENTED YET.
lean_unreachable();

13
src/kernel/environment.h
View file

@ -73,16 +73,20 @@ class environment {
constants m_constants;
extensions m_extensions;
environment(environment const & env, constants const & cs):
m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(cs), m_extensions(env.m_extensions) {}
environment(environment const & env, extensions const & exts):
m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(env.m_constants), m_extensions(exts) {}
void add_core(constant_info const & info) { m_constants.insert(info.get_name(), info); }
environment add(constant_info const & info) const {
environment new_env(*this);
new_env.add_core(info);
return new_env;
}
environment add_axiom(declaration const & d, bool check) const;
environment add_definition(declaration const & d, bool check) const;
environment add_theorem(declaration const & d, bool check) const;
environment add_mutual(declaration const & d, bool check) const;
environment add_quot(declaration const & d) const;
environment add_quot() const;
public:
environment(unsigned trust_lvl = 0);
@ -110,9 +114,6 @@ public:
/** \brief Extends the current environment with the given declaration */
environment add(declaration const & d, bool check = true) const;
/* \brief Add `quot` type. */
environment add_quot() const;
/* \brief Add (mutually recursive) inductive declarations */
environment add(inductive_decl const & decl) const;

26
src/kernel/quot.cpp
View file

@ -18,10 +18,6 @@ name * quot_consts::g_quot_lift = nullptr;
name * quot_consts::g_quot_ind = nullptr;
name * quot_consts::g_quot_mk = nullptr;
static environment add_constant(environment const & env, name const & n, std::initializer_list<name> lvls, expr const & type) {
return env.add(mk_axiom(n, level_param_names(lvls), type));
}
static void check_eq_type(environment const & env) {
optional<inductive::inductive_decl> decl = inductive::is_inductive_decl(env, "eq");
if (!decl) throw exception("failed to initialize quot module, environment does not have 'eq' type");
@ -43,9 +39,11 @@ static void check_eq_type(environment const & env) {
}
}
environment quot_declare(environment const & env) {
check_eq_type(env);
environment new_env = env;
environment environment::add_quot() const {
if (m_quot_initialized)
return *this;
check_eq_type(*this);
environment new_env = *this;
name u_name("u");
local_ctx lctx;
name_generator g;
@ -54,12 +52,11 @@ environment quot_declare(environment const & env) {
expr alpha = lctx.mk_local_decl(g, "α", Sort_u, mk_implicit_binder_info());
expr r = lctx.mk_local_decl(g, "r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
/* constant {u} quot {α : Sort u} (r : α → α → Prop) : Sort u */
new_env = add_constant(new_env, *quot_consts::g_quot, {u_name}, lctx.mk_pi({alpha, r}, Sort_u));
new_env.add_core(constant_info(quot_val(*quot_consts::g_quot, {u_name}, lctx.mk_pi({alpha, r}, Sort_u), quot_kind::Type)));
expr quot_r = mk_app(mk_constant(*quot_consts::g_quot, {u}), alpha, r);
expr a = lctx.mk_local_decl(g, "a", alpha);
/* constant {u} quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : @quot.{u} α r */
new_env = add_constant(new_env, *quot_consts::g_quot_mk, {u_name},
lctx.mk_pi({alpha, r, a}, quot_r));
new_env.add_core(constant_info(quot_val(*quot_consts::g_quot_mk, {u_name}, lctx.mk_pi({alpha, r, a}, quot_r), quot_kind::Mk)));
/* make r implicit */
lctx = local_ctx();
alpha = lctx.mk_local_decl(g, "α", Sort_u, mk_implicit_binder_info());
@ -79,8 +76,8 @@ environment quot_declare(environment const & env) {
expr sanity = lctx.mk_pi({a, b}, mk_arrow(r_a_b, f_a_eq_f_b));
/* constant {u v} quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)
: (∀ a b : α, r a b → f a = f b) → @quot.{u} α r → β */
new_env = add_constant(new_env, *quot_consts::g_quot_lift, {u_name, v_name},
lctx.mk_pi({alpha, r, beta, f}, mk_arrow(sanity, mk_arrow(quot_r, beta))));
new_env.add_core(constant_info(quot_val(*quot_consts::g_quot_lift, {u_name, v_name},
lctx.mk_pi({alpha, r, beta, f}, mk_arrow(sanity, mk_arrow(quot_r, beta))), quot_kind::Lift)));
/* {β : @quot.{u} α r → Prop} */
beta = lctx.mk_local_decl(g, "β", mk_arrow(quot_r, mk_Prop()), mk_implicit_binder_info());
expr quot_mk_a = mk_app(mk_constant(*quot_consts::g_quot_mk, {u}), alpha, r, a);
@ -89,8 +86,9 @@ environment quot_declare(environment const & env) {
expr beta_q = mk_app(beta, q);
/* constant {u} quot.ind {α : Sort u} {r : α → α → Prop} {β : @quot.{u} α r → Prop}
: (∀ a : α, β (@quot.mk.{u} α r a)) → ∀ q : @quot.{u} α r, β q */
new_env = add_constant(new_env, *quot_consts::g_quot_ind, {u_name},
lctx.mk_pi({alpha, r, beta}, mk_arrow(all_quot, lctx.mk_pi(q, beta_q))));
new_env.add_core(constant_info(quot_val(*quot_consts::g_quot_ind, {u_name},
lctx.mk_pi({alpha, r, beta}, mk_arrow(all_quot, lctx.mk_pi(q, beta_q))), quot_kind::Ind)));
new_env.m_quot_initialized = true;
return new_env;
}

5
src/kernel/quot.h
View file

@ -20,7 +20,7 @@ class quot_consts {
friend bool quot_is_rec(name const & n);
template<typename WHNF> friend optional<expr> quot_reduce_rec(expr const & e, WHNF const & whnf);
template<typename WHNF, typename IS_STUCK> friend optional<expr> quot_is_stuck(expr const & e, WHNF const & whnf, IS_STUCK const & is_stuck);
friend environment quot_declare(environment const & env);
friend class environment;
friend void initialize_quot();
friend void finalize_quot();
};
@ -94,9 +94,6 @@ template<typename WHNF, typename IS_STUCK> optional<expr> quot_is_stuck(expr con
return is_stuck(whnf(args[mk_pos]));
}
/** Declare `quot` type. */
environment quot_declare(environment const & env);
void initialize_quot();
void finalize_quot();
}

20
src/library/module.cpp
View file

@ -224,20 +224,6 @@ struct inductive_modification : public modification {
}
};
struct quot_modification : public modification {
LEAN_MODIFICATION("quot")
void perform(environment & env) const override {
env = env.add_quot();
}
void serialize(serializer &) const override {}
static std::shared_ptr<modification const> deserialize(deserializer &) {
return std::make_shared<quot_modification>();
}
};
namespace module {
environment add(environment const & env, std::shared_ptr<modification const> const & modf) {
module_ext ext = get_extension(env);
@ -263,10 +249,6 @@ environment add(environment const & env, declaration const & d) {
return add(new_env, std::make_shared<decl_modification>(d));
}
environment add_quot(environment const & env) {
return add_and_perform(env, std::make_shared<quot_modification>());
}
using inductive::certified_inductive_decl;
environment add_inductive(environment env,
@ -460,11 +442,9 @@ void initialize_module() {
g_object_readers = new object_readers();
decl_modification::init();
inductive_modification::init();
quot_modification::init();
}
void finalize_module() {
quot_modification::finalize();
inductive_modification::finalize();
decl_modification::finalize();
delete g_object_readers;

3
src/library/module.h
View file

@ -123,9 +123,6 @@ environment add(environment const & env, declaration const & d);
environment add_inductive(environment env,
inductive::inductive_decl const & decl,
bool is_meta);
/** \brief The following function must be invoked to register the `quot` type computation rules in the kernel. */
environment add_quot(environment const & env);
}
void initialize_module();
void finalize_module();