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.
119 lines
5.9 KiB
Text
119 lines
5.9 KiB
Text
/-
|
||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import init.meta.declaration init.meta.expr init.meta.exceptional init.data.option.basic
|
||
|
||
meta constant environment : Type
|
||
|
||
namespace environment
|
||
/--
|
||
Information for a projection declaration
|
||
- `cname` is the name of the constructor associated with the projection.
|
||
- `nparams` is the number of constructor parameters
|
||
- `idx` is the parameter being projected by this projection
|
||
- `is_class` is tt iff this is a class projection.
|
||
-/
|
||
structure projection_info :=
|
||
(cname : name)
|
||
(nparams : nat)
|
||
(idx : nat)
|
||
(is_class : bool)
|
||
|
||
/-- Create a standard environment using the given trust level -/
|
||
meta constant mk_std : nat → environment
|
||
/-- Return the trust level of the given environment -/
|
||
meta constant trust_lvl : environment → nat
|
||
-- /-- Add a new declaration to the environment -/
|
||
-- meta constant add : environment → declaration → exceptional environment
|
||
/-- Retrieve a declaration from the environment -/
|
||
meta constant get : environment → name → exceptional constant_info
|
||
meta def contains (env : environment) (d : name) : bool :=
|
||
match env.get d with
|
||
| exceptional.success _ := tt
|
||
| exceptional.exception _ _ := ff
|
||
|
||
/-- Register the given name as a namespace, making it available to the `open` command -/
|
||
meta constant add_namespace : environment → name → environment
|
||
/-- Return tt iff the given name is a namespace -/
|
||
meta constant is_namespace : environment → name → bool
|
||
/-- Add a new inductive datatype to the environment
|
||
name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
|
||
meta constant add_inductive : environment → name → list name → nat → expr → list (name × expr) → bool →
|
||
exceptional environment
|
||
/-- Return tt iff the given name is an inductive datatype -/
|
||
meta constant is_inductive : environment → name → bool
|
||
/-- Return tt iff the given name is a constructor -/
|
||
meta constant is_constructor : environment → name → bool
|
||
/-- Return tt iff the given name is a recursor -/
|
||
meta constant is_recursor : environment → name → bool
|
||
/-- Return tt iff the given name is a recursive inductive datatype -/
|
||
meta constant is_recursive : environment → name → bool
|
||
/-- Return the name of the inductive datatype of the given constructor. -/
|
||
meta constant inductive_type_of : environment → name → option name
|
||
/-- Return the constructors of the inductive datatype with the given name -/
|
||
meta constant constructors_of : environment → name → list name
|
||
/-- Return the recursor of the given inductive datatype -/
|
||
meta constant recursor_of : environment → name → option name
|
||
/-- Return the number of parameters of the inductive datatype -/
|
||
meta constant inductive_num_params : environment → name → nat
|
||
/-- Return the number of indices of the inductive datatype -/
|
||
meta constant inductive_num_indices : environment → name → nat
|
||
/-- Return tt iff the inductive datatype recursor supports dependent elimination -/
|
||
meta constant inductive_dep_elim : environment → name → bool
|
||
/-- Return tt iff the given name is a generalized inductive datatype -/
|
||
meta constant is_ginductive : environment → name → bool
|
||
meta constant is_projection : environment → name → option projection_info
|
||
/-- Fold over declarations in the environment -/
|
||
meta constant fold {α :Type} : environment → α → (constant_info → α → α) → α
|
||
/-- `relation_info env n` returns some value if n is marked as a relation in the given environment.
|
||
the tuple contains: total number of arguments of the relation, lhs position and rhs position. -/
|
||
meta constant relation_info : environment → name → option (nat × nat × nat)
|
||
/-- `refl_for env R` returns the name of the reflexivity theorem for the relation R -/
|
||
meta constant refl_for : environment → name → option name
|
||
/-- `symm_for env R` returns the name of the symmetry theorem for the relation R -/
|
||
meta constant symm_for : environment → name → option name
|
||
/-- `trans_for env R` returns the name of the transitivity theorem for the relation R -/
|
||
meta constant trans_for : environment → name → option name
|
||
/-- `decl_olean env d` returns the name of the .olean file where d was defined.
|
||
The result is none if d was not defined in an imported file. -/
|
||
meta constant decl_olean : environment → name → option string
|
||
/-- `decl_pos env d` returns the source location of d if available. -/
|
||
meta constant decl_pos : environment → name → option pos
|
||
/-- Return the fields of the structure with the given name, or `none` if it is not a structure -/
|
||
meta constant structure_fields : environment → name → option (list name)
|
||
meta constant fingerprint : environment → nat
|
||
open lean.expr
|
||
|
||
meta constant unfold_untrusted_macros : environment → expr → expr
|
||
meta constant unfold_all_macros : environment → expr → expr
|
||
|
||
meta def is_constructor_app (env : environment) (e : expr) : bool :=
|
||
is_constant (get_app_fn e) && is_constructor env (const_name (get_app_fn e))
|
||
|
||
meta def is_refl_app (env : environment) (e : expr) : option (name × expr × expr) :=
|
||
match (refl_for env (const_name (get_app_fn e))) with
|
||
| (some n) :=
|
||
if get_app_num_args e ≥ 2
|
||
then some (n, app_arg (app_fn e), app_arg e)
|
||
else none
|
||
| none := none
|
||
|
||
/-- Return true if 'n' has been declared in the current file -/
|
||
meta def in_current_file (env : environment) (n : name) : bool :=
|
||
(env.decl_olean n).is_none && env.contains n
|
||
|
||
meta def is_definition (env : environment) (n : name) : bool :=
|
||
match env.get n with
|
||
| exceptional.success (lean.constant_info.defn_info _) := tt
|
||
| _ := ff
|
||
|
||
end environment
|
||
|
||
meta instance : has_repr environment :=
|
||
⟨λ e, "[environment]"⟩
|
||
|
||
meta instance : inhabited environment :=
|
||
⟨environment.mk_std 0⟩
|