diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean index 96cc74cb0d..32f71e3e6b 100644 --- a/library/init/lean/declaration.lean +++ b/library/init/lean/declaration.lean @@ -42,12 +42,8 @@ structure declaration_val := structure axiom_val extends declaration_val := (is_meta : bool) -/- TODO(Leo): the `value` field for `definition_val` and `theorem_val` should be a thunk. We will make this change - as soon as we add support for serializing thunks. - We need this feature to be able to load their values on demand in the kernel. -/ - structure definition_val extends declaration_val := -(value : task expr) (hints : reducibility_hints) (is_meta : bool) +(value : expr) (hints : reducibility_hints) (is_meta : bool) structure theorem_val extends declaration_val := (value : task expr) @@ -63,7 +59,7 @@ inductive declaration | axiom_decl (val : axiom_val) | defn_decl (val : definition_val) | thm_decl (val : theorem_val) -| quot_decl +| quot_decl (id : name) | 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) @@ -149,7 +145,7 @@ def type (d : constant_info) : expr := d.to_declaration_val.type def value : constant_info → option expr -| (defn_info {value := r, ..}) := some r.get +| (defn_info {value := r, ..}) := some r | (thm_info {value := r, ..}) := some r.get | _ := none diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 64917e03b8..2bab75ea8a 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -728,7 +728,7 @@ public: } ind_types.push_back(inductive_type(local_name(r.m_inds[i]), Pi(r.m_params, local_type(r.m_inds[i])), constructors(cnstrs))); } - m_env = m_env.add(inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta)); + m_env = m_env.add(mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta)); } environment inductive_cmd() { diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 25d0803645..abb11b8662 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -128,11 +128,11 @@ static object * mk_recursor_val(name const & n, level_param_names const & params bool declaration::is_meta() const { switch (kind()) { case declaration_kind::Definition: return cnstr_scalar(get_val_obj(), definition_scalar_offset()) != 0; - case declaration_kind::Inductive: return to_inductive_val().is_meta(); - case declaration_kind::Constructor: return to_constructor_val().is_meta(); - case declaration_kind::Recursor: return to_recursor_val().is_meta(); case declaration_kind::Axiom: return cnstr_scalar(get_val_obj(), axiom_scalar_offset()) != 0; case declaration_kind::Theorem: return false; + case declaration_kind::Inductive: lean_unreachable(); // TODO(Leo): + case declaration_kind::Quot: return false; + case declaration_kind::MutualDefinition: return true; } lean_unreachable(); } @@ -216,20 +216,9 @@ declaration mk_axiom_inferring_meta(environment const & env, name const & n, return mk_axiom(n, params, t, use_meta(env, t)); } -declaration mk_inductive(name const & n, level_param_names const & params, expr const & t, unsigned nparams, unsigned nindices, - names const & all, names const & cnstrs, names const & recs, bool is_rec, bool is_meta) { - return declaration(mk_cnstr(static_cast(declaration_kind::Inductive), - mk_inductive_val(n, params, t, nparams, nindices, all, cnstrs, recs, is_rec, is_meta))); -} - -declaration mk_constructor(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, bool is_meta) { - return declaration(mk_cnstr(static_cast(declaration_kind::Constructor), mk_constructor_val(n, params, t, induct, nparams, is_meta))); -} - -declaration mk_recursor(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, - unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta) { - return declaration(mk_cnstr(static_cast(declaration_kind::Constructor), - mk_recursor_val(n, params, t, induct, nparams, nindices, nmotives, nminor, k, rules, is_meta))); +declaration mk_quot_decl(name const & n) { + inc(n.raw()); + return declaration(mk_cnstr(static_cast(declaration_kind::Quot), n.raw())); } inductive_type::inductive_type(name const & id, expr const & type, constructors const & cnstrs): @@ -239,10 +228,12 @@ inductive_type::inductive_type(name const & id, expr const & type, constructors static unsigned inductive_decl_scalar_offset() { return sizeof(object*)*3; } -inductive_decl::inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta): - object_ref(mk_cnstr(0, lparams.raw(), nparams.raw(), types.raw(), sizeof(unsigned char))) { - inc(lparams.raw()), inc(nparams.raw()); inc(types.raw()); - cnstr_set_scalar(raw(), inductive_decl_scalar_offset(), static_cast(is_meta)); +declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta) { + declaration r(mk_cnstr(static_cast(declaration_kind::Inductive), + lparams.raw(), nparams.raw(), types.raw(), 1)); + inc(lparams.raw()); inc(nparams.raw()); inc(types.raw()); + cnstr_set_scalar(r.raw(), inductive_decl_scalar_offset(), static_cast(is_meta)); + return r; } bool inductive_decl::is_meta() const { return cnstr_scalar(raw(), inductive_decl_scalar_offset()) != 0; } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 834968ab8d..087aad90bd 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -77,6 +77,126 @@ public: expr const & get_type() const { return static_cast(cnstr_obj_ref(*this, 2)); } }; +/* +structure constructor := +(id : name) (type : expr) +*/ +typedef pair_ref constructor; +inline name const & constructor_name(constructor const & c) { return c.fst(); } +inline expr const & constructor_type(constructor const & c) { return c.snd(); } +typedef list_ref constructors; + +/** +structure inductive_type := +(id : name) (type : expr) (cnstrs : list constructor) +*/ +class inductive_type : public object_ref { +public: + inductive_type(name const & id, expr const & type, constructors const & cnstrs); + inductive_type(inductive_type const & other):object_ref(other) {} + inductive_type(inductive_type && other):object_ref(other) {} + inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; } + inductive_type & operator=(inductive_type && other) { object_ref::operator=(other); return *this; } + name const & get_name() const { return static_cast(cnstr_obj_ref(*this, 0)); } + expr const & get_type() const { return static_cast(cnstr_obj_ref(*this, 1)); } + constructors const & get_cnstrs() const { return static_cast(cnstr_obj_ref(*this, 2)); } +}; +typedef list_ref inductive_types; + +/* +inductive declaration +| axiom_decl (val : axiom_val) +| defn_decl (val : definition_val) +| thm_decl (val : theorem_val) +| quot_decl (id : name) +| 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) +*/ +enum class declaration_kind { Axiom, Definition, Theorem, Quot, MutualDefinition, Inductive }; +class declaration : public object_ref { + object * get_val_obj() const { return cnstr_obj(raw(), 0); } + object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); } + + declaration_val const & to_declaration_val() const { + lean_assert(is_axiom() || is_definition() || is_theorem()); + return static_cast(cnstr_obj_ref(to_val(), 0)); + } + +public: + declaration(); + declaration(declaration const & other):object_ref(other) {} + declaration(declaration && other):object_ref(other) {} + /* 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 & operator=(declaration const & other) { object_ref::operator=(other); return *this; } + declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; } + + friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); } + + bool is_definition() const { return kind() == declaration_kind::Definition; } + bool is_axiom() const { return kind() == declaration_kind::Axiom; } + bool is_theorem() const { return kind() == declaration_kind::Theorem; } + bool is_inductive() const { return kind() == declaration_kind::Inductive; } + bool is_meta() const; + bool has_value() const { return is_theorem() || is_definition(); } + + name const & get_name() const { return to_declaration_val().get_name(); } + level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); } + unsigned get_num_univ_params() const { return length(get_univ_params()); } + expr const & get_type() const { return to_declaration_val().get_type(); } + expr const & get_value() const { lean_assert(has_value()); return static_cast(cnstr_obj_ref(to_val(), 1)); } + reducibility_hints const & get_hints() const; + + void serialize(serializer & s) const { s.write_object(raw()); } + static declaration deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return declaration(o); } +}; + +inline serializer & operator<<(serializer & s, declaration const & l) { l.serialize(s); return s; } +inline declaration read_declaration(deserializer & d) { return declaration::deserialize(d); } +inline deserializer & operator>>(deserializer & d, declaration & l) { l = read_declaration(d); return d; } + +inline optional none_declaration() { return optional(); } +inline optional some_declaration(declaration const & o) { return optional(o); } +inline optional some_declaration(declaration && o) { return optional(std::forward(o)); } + +declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, + reducibility_hints const & hints, bool meta = false); +declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, + bool meta = false); +declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); +declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); +declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta = false); +declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta); +declaration mk_quot_decl(name const & n); + +/** \brief Return true iff \c e depends on meta-declarations */ +bool use_meta(environment const & env, expr const & e); + +/** \brief Similar to mk_definition but infer the value of meta flag. + That is, set it to true if \c t or \c v contains a meta declaration. */ +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, + expr const & t, expr const & v, reducibility_hints const & hints); +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, + expr const & t, expr const & v); +/** \brief Similar to mk_axiom but infer the value of meta flag. + That is, set it to true if \c t or \c v contains a meta declaration. */ +declaration mk_axiom_inferring_meta(environment const & env, name const & n, + level_param_names const & params, expr const & t); + +/** \brief View for manipulating declaration.induct_decl constructor. + | induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool) */ +class inductive_decl : public object_ref { +public: + inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); } + names const & get_lparams() const { return static_cast(cnstr_obj_ref(raw(), 0)); } + nat const & get_nparams() const { return static_cast(cnstr_obj_ref(raw(), 1)); } + inductive_types const & get_types() const { return static_cast(cnstr_obj_ref(raw(), 2)); } + bool is_meta() const; +}; + /* structure inductive_val extends declaration_val := (nparams : nat) -- Number of parameters @@ -182,147 +302,6 @@ structure quot_val extends declaration_val := (kind : quot_kind) */ - -/* -inductive declaration -| axiom_decl (val : axiom_val) -| defn_decl (val : definition_val) -| thm_decl (val : theorem_val) -| induct_decl (val : inductive_val) -| cnstr_decl (val : constructor_val) -| rec_decl (val : recursor_val) -*/ -enum class declaration_kind { Axiom, Definition, Theorem, Inductive, Constructor, Recursor }; -class declaration : public object_ref { - explicit declaration(object * o):object_ref(o) {} - explicit declaration(object_ref const & o):object_ref(o) {} - object * get_val_obj() const { return cnstr_obj(raw(), 0); } - object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); } - declaration_val const & to_declaration_val() const { return static_cast(cnstr_obj_ref(to_val(), 0)); } -public: - declaration(); - declaration(declaration const & other):object_ref(other) {} - declaration(declaration && other):object_ref(other) {} - declaration_kind kind() const { return static_cast(cnstr_tag(raw())); } - - declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; } - declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; } - - friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); } - - bool is_definition() const { return kind() == declaration_kind::Definition; } - bool is_axiom() const { return kind() == declaration_kind::Axiom; } - bool is_theorem() const { return kind() == declaration_kind::Theorem; } - bool is_inductive() const { return kind() == declaration_kind::Inductive; } - bool is_constructor() const { return kind() == declaration_kind::Constructor; } - bool is_recursor() const { return kind() == declaration_kind::Recursor; } - bool is_meta() const; - bool has_value() const { return is_theorem() || is_definition(); } - - name const & get_name() const { return to_declaration_val().get_name(); } - level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); } - unsigned get_num_univ_params() const { return length(get_univ_params()); } - expr const & get_type() const { return to_declaration_val().get_type(); } - expr const & get_value() const { lean_assert(has_value()); return static_cast(cnstr_obj_ref(to_val(), 1)); } - reducibility_hints const & get_hints() const; - - inductive_val const & to_inductive_val() const { lean_assert(is_inductive()); return static_cast(to_val()); } - constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast(to_val()); } - recursor_val const & to_recursor_val() const { lean_assert(is_recursor()); return static_cast(to_val()); } - - friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & hints, bool meta); - friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, - expr const & v, bool meta); - friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &); - friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta); - friend declaration mk_inductive(name const & n, level_param_names const & params, expr const & t, unsigned nparams, unsigned nindices, - names const & all, names const & cnstrs, names const & recs, bool is_rec, bool is_meta); - friend declaration mk_constructor(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, - bool is_meta); - friend declaration mk_recursor(name const & id, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, - unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta); - - void serialize(serializer & s) const { s.write_object(raw()); } - static declaration deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return declaration(o); } -}; - -inline serializer & operator<<(serializer & s, declaration const & l) { l.serialize(s); return s; } -inline declaration read_declaration(deserializer & d) { return declaration::deserialize(d); } -inline deserializer & operator>>(deserializer & d, declaration & l) { l = read_declaration(d); return d; } - -inline optional none_declaration() { return optional(); } -inline optional some_declaration(declaration const & o) { return optional(o); } -inline optional some_declaration(declaration && o) { return optional(std::forward(o)); } - -declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & hints, bool meta = false); -declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, - bool meta = false); -declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); -declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); -declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta = false); - -/** \brief Return true iff \c e depends on meta-declarations */ -bool use_meta(environment const & env, expr const & e); - -/** \brief Similar to mk_definition but infer the value of meta flag. - That is, set it to true if \c t or \c v contains a meta declaration. */ -declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, - expr const & t, expr const & v, reducibility_hints const & hints); -declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, - expr const & t, expr const & v); -/** \brief Similar to mk_axiom but infer the value of meta flag. - That is, set it to true if \c t or \c v contains a meta declaration. */ -declaration mk_axiom_inferring_meta(environment const & env, name const & n, - level_param_names const & params, expr const & t); - -declaration mk_inductive(name const & n, level_param_names const & params, expr const & t, unsigned nparams, unsigned nindices, - names const & all, names const & cnstrs, names const & recs, bool is_rec, bool is_meta); -declaration mk_constructor(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, - bool is_meta); -declaration mk_recursor(name const & id, level_param_names const & params, expr const & t, name const & induct, unsigned nparams, - unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta); - -typedef pair_ref constructor; -inline name const & constructor_name(constructor const & c) { return c.fst(); } -inline expr const & constructor_type(constructor const & c) { return c.snd(); } -typedef list_ref constructors; - -/** -structure inductive_type := -(id : name) (type : expr) (cnstrs : list constructor) -*/ -class inductive_type : public object_ref { -public: - inductive_type(name const & id, expr const & type, constructors const & cnstrs); - inductive_type(inductive_type const & other):object_ref(other) {} - inductive_type(inductive_type && other):object_ref(other) {} - inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; } - inductive_type & operator=(inductive_type && other) { object_ref::operator=(other); return *this; } - name const & get_name() const { return static_cast(cnstr_obj_ref(*this, 0)); } - expr const & get_type() const { return static_cast(cnstr_obj_ref(*this, 1)); } - constructors const & get_cnstrs() const { return static_cast(cnstr_obj_ref(*this, 2)); } -}; -typedef list_ref inductive_types; - -/** -structure inductive_decl := -(lparams : list name) (nparams : nat) (types : list inductive_type) -*/ -class inductive_decl : public object_ref { -public: - inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta); - inductive_decl(inductive_decl const & other):object_ref(other) {} - inductive_decl(inductive_decl && other):object_ref(other) {} - inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; } - inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; } - names const & get_lparams() const { return static_cast(cnstr_obj_ref(*this, 0)); } - nat const & get_nparams() const { return static_cast(cnstr_obj_ref(*this, 1)); } - inductive_types const & get_types() const { return static_cast(cnstr_obj_ref(*this, 2)); } - bool is_meta() const; -}; - /* /-- Information associated with constant declarations. -/ inductive constant_info diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index d65bb3743b..9e8c3c2696 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -136,7 +136,9 @@ environment environment::add_defn_thm_axiom(declaration const & d, bool check) c environment environment::add(declaration const & d, bool check) const { switch (d.kind()) { - case declaration_kind::Axiom: case declaration_kind::Definition: case declaration_kind::Theorem: + case declaration_kind::Axiom: + case declaration_kind::Definition: + case declaration_kind::Theorem: return add_defn_thm_axiom(d, check); default: // NOT IMPLEMENTED YET. diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 0b37b7474f..c0d526bfcd 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -79,6 +79,8 @@ class environment { m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(env.m_constants), m_extensions(exts) {} environment add_defn_thm_axiom(declaration const & d, bool check) const; + environment add_quot(declaration const & d) const; + public: environment(unsigned trust_lvl = 0); environment(unsigned trust_lvl, std::unique_ptr ext);