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

feat(kernel/declaration): add wrappers for accessing inductive/constructor/recursor declarations

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-25 15:01:02 -07:00
parent 7684860aec
commit bb0b43798c
3 changed files with 113 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,7 @@ structure recursor_rule :=
(rhs : expr) -- Right hand side of the reduction rule
structure recursor_val extends declaration_val :=
(induct : list name) -- List of all inductive datatypes in the mutual declaration that generated this recursor
(all : list name) -- List of all inductive datatypes in the mutual declaration that generated this recursor
(nparams : nat) -- Number of parameters
(nindices : nat) -- Number of indices
(nmotives : nat) -- Number of motives

14
src/kernel/declaration.cpp
View file

@ -49,6 +49,12 @@ static unsigned inductive_scalar_offset() { return sizeof(object*)*6; }
static unsigned constructor_scalar_offset() { return sizeof(object*)*3; }
static unsigned recursor_scalar_offset() { return sizeof(object*)*7; }
bool inductive_val::is_rec() const { return (cnstr_scalar<unsigned char>(raw(), inductive_scalar_offset()) & 1) != 0; }
bool inductive_val::is_meta() const { return (cnstr_scalar<unsigned char>(raw(), inductive_scalar_offset()) & 2) != 0; }
bool constructor_val::is_meta() const { return cnstr_scalar<unsigned char>(raw(), constructor_scalar_offset()); }
bool recursor_val::is_k() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 1) != 0; }
bool recursor_val::is_meta() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 2) != 0; }
object * declaration::mk_declaration_val(name const & n, level_param_names const & params, expr const & t) {
object * r = alloc_cnstr(0, 3, 0);
inc(n.raw()); cnstr_set_obj(r, 0, n.raw());
@ -127,9 +133,9 @@ bool declaration::is_meta() const {
switch (kind()) {
case declaration_kind::Definition: return cnstr_scalar<unsigned char>(get_val_obj(), definition_scalar_offset()) != 0;
case declaration_kind::Constant: return cnstr_scalar<unsigned char>(get_val_obj(), constant_scalar_offset()) != 0;
case declaration_kind::Inductive: return (cnstr_scalar<unsigned char>(get_val_obj(), inductive_scalar_offset()) & 2) != 0;
case declaration_kind::Constructor: return cnstr_scalar<unsigned char>(get_val_obj(), constructor_scalar_offset()) != 0;
case declaration_kind::Recursor: return (cnstr_scalar<unsigned char>(get_val_obj(), recursor_scalar_offset()) & 2) != 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 false;
case declaration_kind::Theorem: return false;
}
@ -140,7 +146,7 @@ static reducibility_hints * g_opaque = nullptr;
reducibility_hints const & declaration::get_hints() const {
if (is_definition())
return static_cast<reducibility_hints const &>(cnstr_obj_ref(get_val(), 2));
return static_cast<reducibility_hints const &>(cnstr_obj_ref(to_val(), 2));
else
return *g_opaque;
}

110
src/kernel/declaration.h
View file

@ -62,6 +62,67 @@ inline deserializer & operator>>(deserializer & d, reducibility_hints & l) { l =
> 0 If f2 should be unfolded */
int compare(reducibility_hints const & h1, reducibility_hints const & h2);
/*
structure declaration_val :=
(id : name) (lparams : list name) (type : expr)
*/
class declaration_val : public object_ref {
public:
declaration_val(declaration_val const & other):object_ref(other) {}
declaration_val(declaration_val && other):object_ref(other) {}
declaration_val & operator=(declaration_val const & other) { object_ref::operator=(other); return *this; }
declaration_val & operator=(declaration_val && other) { object_ref::operator=(other); return *this; }
name const & get_name() const { return static_cast<name const &>(cnstr_obj_ref(*this, 0)); }
level_param_names const & get_lparams() const { return static_cast<level_param_names const &>(cnstr_obj_ref(*this, 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 2)); }
};
/*
structure inductive_val extends declaration_val :=
(nparams : nat) -- Number of parameters
(nindices : nat) -- Number of indices
(all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
(cnstrs : list name) -- List of all constructors for this inductive datatype
(recs : list name) -- List of all recursors generated when the mutual inductive declaration containing this declaration was accepted by the kernel
-- Remark: `recs.length` may be greater than `all.length` if declaration contains nested inductives
-- The first element in the list is the recursor of this inductive declaration
(is_rec : bool) -- `tt` iff it is recursive
(is_meta : bool)
*/
class inductive_val : public object_ref {
public:
inductive_val(inductive_val const & other):object_ref(other) {}
inductive_val(inductive_val && other):object_ref(other) {}
inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 3)); }
names const & get_cnstrs() const { return static_cast<names const &>(cnstr_obj_ref(*this, 4)); }
names const & get_recs() const { return static_cast<names const &>(cnstr_obj_ref(*this, 5)); }
bool is_rec() const;
bool is_meta() const;
};
/*
structure constructor_val extends declaration_val :=
(induct : name) -- Inductive type this constructor is a member of
(nparams : nat) -- Number of parameters in inductive datatype `induct`
(is_meta : bool)
*/
class constructor_val : public object_ref {
public:
constructor_val(constructor_val const & other):object_ref(other) {}
constructor_val(constructor_val && other):object_ref(other) {}
constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
name const & get_induct() const { return static_cast<name const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
bool is_meta() const;
};
/*
structure recursor_rule :=
(cnstr : name) -- Reduction rule for this constructor
@ -82,8 +143,35 @@ public:
typedef list_ref<recursor_rule> recursor_rules;
/**
/*
structure recursor_val extends declaration_val :=
(all : list name) -- List of all inductive datatypes in the mutual declaration that generated this recursor
(nparams : nat) -- Number of parameters
(nindices : nat) -- Number of indices
(nmotives : nat) -- Number of motives
(nminors : nat) -- Number of minor premises
(k : bool) -- It supports K-like reduction
(rules : list recursor_rule) -- A reduction for each constructor
(is_meta : bool)
*/
class recursor_val : public object_ref {
public:
recursor_val(recursor_val const & other):object_ref(other) {}
recursor_val(recursor_val && other):object_ref(other) {}
recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 1)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 3)); }
nat const & get_nmotives() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 4)); }
nat const & get_nminors() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 5)); }
recursor_rules const & get_rules() const { return static_cast<recursor_rules const &>(cnstr_obj_ref(*this, 6)); }
bool is_k() const;
bool is_meta() const;
};
/*
inductive declaration
| const_decl (val : constant_val)
| defn_decl (val : definition_val)
@ -92,7 +180,6 @@ inductive declaration
| induct_decl (val : inductive_val)
| cnstr_decl (val : constructor_val)
| rec_decl (val : recursor_val)
*/
enum class declaration_kind { Constant, Definition, Axiom, Theorem, Inductive, Constructor, Recursor };
class declaration : public object_ref {
@ -110,8 +197,8 @@ class declaration : public object_ref {
unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta);
object * get_val_obj() const { return cnstr_obj(raw(), 0); }
object_ref const & get_val() const { return cnstr_obj_ref(*this, 0); }
object_ref const & get_declaration_val() const { return (kind() == declaration_kind::Axiom) ? get_val() : cnstr_obj_ref(get_val(), 0); }
object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); }
declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(kind() == declaration_kind::Axiom ? to_val() : cnstr_obj_ref(to_val(), 0)); }
public:
declaration();
declaration(declaration const & other):object_ref(other) {}
@ -127,16 +214,23 @@ public:
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 static_cast<name const &>(cnstr_obj_ref(get_declaration_val(), 0)); }
level_param_names const & get_univ_params() const { return static_cast<level_param_names const &>(cnstr_obj_ref(get_declaration_val(), 1)); }
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 static_cast<expr const &>(cnstr_obj_ref(get_declaration_val(), 2)); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_obj_ref(get_val(), 1)); }
expr const & get_type() const { return to_declaration_val().get_type(); }
expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(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<inductive_val const &>(to_val()); }
constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast<constructor_val const &>(to_val()); }
recursor_val const & to_recursor_val() const { lean_assert(is_recursor()); return static_cast<recursor_val const &>(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,