04fbbbb0d6
This is the first step in the declaration vs constant_info refactor.
Here is the design notes:
In Lean3, we use the `declaration` objects to represent new declarations
that are sent to the kernel, and to store information for all constants
declared in an environment.
This design decision was done when we did not have support for
mutual (meta) declarations, and information about inductive datatypes,
constructors and recursors were stored in an environment extension.
This design now seems weird since we have four different methods for
adding declarations into the environment:
```
environment add(certified_declaration const & d) const;
environment add_meta(buffer<declaration> const & ds, bool check = true) const;
environment add(inductive_decl const & decl) const;
environment add_quot() const;
```
Moreover, we use `mk_constant_assumption` to represent inductive
datatype, constructors, recursors, and `quot` primitives.
Since inductive datatypes, constructors, recursors and `quot` primitives
are not considered axioms, we have the method:
```
bool environment::is_builtin(name const & n) const;
```
We can avoid these hacks by having a type for representing
declarations (i.e., objects that are sent to the kernel) and
objects for storing information of the constant declarations stored
in an environment object.
A `declaration` object is now of the form
```
inductive declaration
| defn_decl (val : definition_val)
| axiom_decl (val : axiom_val)
| thm_decl (val : theorem_val)
| 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)
/-
If we want, we can let users specify their own names for `quot`,
`quot.mk`, `quot.lift` and `quot.ind`. We just need to add them
as fields of `declaration.quot_decl`.
-/
```
When we check a declaration, one or more `constant_info` objects are
created for each new constant in the declaration.
```
inductive constant_info
| assump_info (val : assumption_val)
| defn_info (val : definition_val)
| axiom_info (val : axiom_val)
| thm_info (val : theorem_val)
| quot_info (val : quot_val)
| induct_info (val : inductive_val)
| cnstr_info (val : constructor_val)
| rec_info (val : recursor_val)
```
For simple declarations `constant` (aka `assumption`), `definition`,
`theorem` and `axiom`, the information stored in the `constant_info` is
identical to the information in the `declaration` object. This is
expected since these are the original Lean3 declarations.
The `environment` object stores a mapping from `name` to
`constant_info`. The function `check` validates a declaration
and produces a `certified_declaration`. A `certified_declaration` is
a pair `(declaration, list constant_info)`. The `list` here makes it
explicit that a declaration may add one or more new constants into the
environment. Finally, the `environment` object has a single `add`
method and a single `get` and `find`:
```
environment add(certified_declaration const & d) const;
/** \brief Return info for the constant with name \c n (if it is defined in this environment). */
optional<constant_info> find(name const & n) const;
/** \brief Return info for the constant with name \c n. Throws an
exception if has not been declared in this environment. */
constant_info get(name const & n) const;
```
Moreover, the method `environment::builtin` is not necessary anymore.
If `environment::get(n)` returns an `axiom_info` or an `assump_info`, then
we know for sure the constant named `n` has been postulated.
This commit only defined the new types in Lean. I still need to make
the changes to the C++ code base.
158 lines
6.4 KiB
Text
158 lines
6.4 KiB
Text
/-
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import init.lean.expr
|
|
|
|
namespace lean
|
|
/--
|
|
Reducibility hints are used in the convertibility checker.
|
|
When trying to solve a constraint such a
|
|
|
|
(f ...) =?= (g ...)
|
|
|
|
where f and g are definitions, the checker has to decide which one will be unfolded.
|
|
If f (g) is opaque, then g (f) is unfolded if it is also not marked as opaque,
|
|
Else if f (g) is abbrev, then f (g) is unfolded if g (f) is also not marked as abbrev,
|
|
Else if f and g are regular, then we unfold the one with the biggest definitional height.
|
|
Otherwise both are unfolded.
|
|
|
|
The arguments of the `regular` constructor are: the definitional height and the flag `self_opt`.
|
|
|
|
The definitional height is by default computed by the kernel. It only takes into account
|
|
other regular definitions used in a definition. When creating declarations using meta-programming,
|
|
we can specify the definitional depth manually.
|
|
|
|
Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a
|
|
declaration during type checking.
|
|
|
|
Remark: the reducibility_hints are not related to the attributes: reducible/irrelevance/semireducible.
|
|
These attributes are used by the elaborator. The reducibility_hints are used by the kernel (and elaborator).
|
|
Moreover, the reducibility_hints cannot be changed after a declaration is added to the kernel. -/
|
|
inductive reducibility_hints
|
|
| opaque : reducibility_hints
|
|
| abbrev : reducibility_hints
|
|
| regular : uint32 → reducibility_hints
|
|
|
|
structure declaration_val :=
|
|
(id : name) (lparams : list name) (type : expr)
|
|
|
|
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 : expr) (hints : reducibility_hints) (is_meta : bool)
|
|
|
|
structure theorem_val extends declaration_val :=
|
|
(value : expr)
|
|
|
|
/-- The kernel compiles (mutual) inductive declarations (see `inductive_decls`) into a set of
|
|
- `declaration.induct_decl` (for each inductive datatype in the mutual declaration),
|
|
- `declaration.cnstr_decl` (for each constructor in the mutual declaration),
|
|
- `declaration.rec_decl` (automatically generated recursors).
|
|
|
|
This data is used to implement iota-reduction efficiently and compile nested inductive
|
|
declarations.
|
|
|
|
A series of checks are performed by the kernel to check whether a `inductive_decls`
|
|
is valid or not. -/
|
|
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)
|
|
|
|
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)
|
|
|
|
/-- Information for reducing a recursor -/
|
|
structure recursor_rule :=
|
|
(cnstr : name) -- Reduction rule for this constructor
|
|
(nfields : nat) -- Number of fields (i.e., without counting inductive datatype parameters)
|
|
(rhs : expr) -- Right hand side of the reduction rule
|
|
|
|
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
|
|
(nminor : nat) -- Number of minor premises
|
|
(k : bool) -- It supports K-like reduction
|
|
(rules : list recursor_rule) -- A reduction for each constructor
|
|
(is_meta : bool)
|
|
|
|
inductive quot_kind
|
|
| type -- `quot`
|
|
| cnstr -- `quot.mk`
|
|
| lift -- `quot.lift`
|
|
| ind -- `quot.ind`
|
|
|
|
structure quot_val extends declaration_val :=
|
|
(kind : quot_kind)
|
|
|
|
/-- Information associated with constant declarations. -/
|
|
inductive constant_info
|
|
| axiom_info (val : axiom_val)
|
|
| defn_info (val : definition_val)
|
|
| thm_info (val : theorem_val)
|
|
| quot_info (val : quot_val)
|
|
| induct_info (val : inductive_val)
|
|
| cnstr_info (val : constructor_val)
|
|
| rec_info (val : recursor_val)
|
|
|
|
namespace constant_info
|
|
|
|
def to_declaration_val : constant_info → declaration_val
|
|
| (defn_info {to_declaration_val := d, ..}) := d
|
|
| (axiom_info {to_declaration_val := d, ..}) := d
|
|
| (thm_info {to_declaration_val := d, ..}) := d
|
|
| (quot_info {to_declaration_val := d, ..}) := d
|
|
| (induct_info {to_declaration_val := d, ..}) := d
|
|
| (cnstr_info {to_declaration_val := d, ..}) := d
|
|
| (rec_info {to_declaration_val := d, ..}) := d
|
|
|
|
def id (d : constant_info) : name :=
|
|
d.to_declaration_val.id
|
|
|
|
def lparams (d : constant_info) : list name :=
|
|
d.to_declaration_val.lparams
|
|
|
|
def type (d : constant_info) : expr :=
|
|
d.to_declaration_val.type
|
|
|
|
def value : constant_info → option expr
|
|
| (defn_info {value := r, ..}) := some r
|
|
| (thm_info {value := r, ..}) := some r
|
|
| _ := none
|
|
|
|
def hints : constant_info → reducibility_hints
|
|
| (defn_info {hints := r, ..}) := r
|
|
| _ := reducibility_hints.opaque
|
|
|
|
end constant_info
|
|
|
|
structure constructor :=
|
|
(id : name) (type : expr)
|
|
|
|
structure inductive_type :=
|
|
(id : name) (type : expr) (cnstrs : list constructor)
|
|
|
|
/-- A (mutual) inductive declaration. This declaration created by the frontend is compiled by the kernel
|
|
into a set of `declaration.induct_decl`, `declaration.cnstr_decl` and `declaration.rec_decl`. -/
|
|
structure inductive_decl :=
|
|
(lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool)
|
|
|
|
end lean
|