From 101886ffae4cadc0a9131be2e841debfbc4d791f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Aug 2018 13:43:44 -0700 Subject: [PATCH] feat(kernel): proper constant_info and declaration objects for `quot` type --- library/init/lean/declaration.lean | 2 +- src/frontends/lean/builtin_cmds.cpp | 2 +- src/kernel/declaration.cpp | 18 ++++++++++++++---- src/kernel/declaration.h | 21 +++++++++++++++++++-- src/kernel/environment.cpp | 19 ++++++------------- src/kernel/environment.h | 13 +++++++------ src/kernel/quot.cpp | 26 ++++++++++++-------------- src/kernel/quot.h | 5 +---- src/library/module.cpp | 20 -------------------- src/library/module.h | 3 --- 10 files changed, 61 insertions(+), 68 deletions(-) diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean index 1824c0aefe..314d00fd1b 100644 --- a/library/init/lean/declaration.lean +++ b/library/init/lean/declaration.lean @@ -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) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 07a63638a5..7d40e4b2dc 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -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()); } /* diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 5fe4be0bac..6c36a374c5 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -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(raw(), sizeof(object*), static_cast(k)); +} + +quot_kind quot_val::get_quot_kind() const { return static_cast(cnstr_scalar(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(declaration_kind::MutualDefinition), ds)); } -declaration mk_quot_decl(name const & n) { - inc(n.raw()); - return declaration(mk_cnstr(static_cast(declaration_kind::Quot), n.raw())); +declaration mk_quot_decl() { + return declaration(box(static_cast(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(constant_info_kind::Definition), v)) { } +constant_info::constant_info(quot_val const & v): + object_ref(mk_cnstr(static_cast(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(); } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index cba9226ad4..50da11038f 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -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(cnstr_tag(raw())); } + declaration_kind kind() const { return static_cast(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(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(cnstr_tag(raw())); } constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index ab8e7652c8..9043235a69 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -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(); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 1be3cd5a19..9436702ce8 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -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; diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp index ce3c3fe444..ef080472a4 100644 --- a/src/kernel/quot.cpp +++ b/src/kernel/quot.cpp @@ -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 lvls, expr const & type) { - return env.add(mk_axiom(n, level_param_names(lvls), type)); -} - static void check_eq_type(environment const & env) { optional 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; } diff --git a/src/kernel/quot.h b/src/kernel/quot.h index 50c4dd5336..0c47143850 100644 --- a/src/kernel/quot.h +++ b/src/kernel/quot.h @@ -20,7 +20,7 @@ class quot_consts { friend bool quot_is_rec(name const & n); template friend optional quot_reduce_rec(expr const & e, WHNF const & whnf); template friend optional 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 optional 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(); } diff --git a/src/library/module.cpp b/src/library/module.cpp index c17480a759..6e4f8048dc 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -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 deserialize(deserializer &) { - return std::make_shared(); - } -}; - namespace module { environment add(environment const & env, std::shared_ptr 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(d)); } -environment add_quot(environment const & env) { - return add_and_perform(env, std::make_shared()); -} - 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; diff --git a/src/library/module.h b/src/library/module.h index 147bb4e5a9..65c5ec2617 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -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();