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.
While `cmdline_args` has no side-effects, it is certainly not a pure function.
The `stdin` etc. should have been safe since all accessors are in `io`, but
better be safe than sorry.
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.
f a =?= f b
-----------
a =?= b
This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.
The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
in the Lean2 codebase when we were not caching failures and
the kernel type checker was also used during elaboration.
- Lean strings (like std::string) may contain null characters. The
codebase was ignoring this issue.
- We now have a wrapper `string_ref` for wrapping Lean string objects in
C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
Remark: I also found a few places where the code relies on the
following property which is not true
Forall s : std::string, std::string(s.c_str()) == s
- `name` object wrapper was assuming that all numerals were small
`nat` values. This is true in most cases, but the system would
crash when processing if it is a big number.
- The commit tries to make sure runtime/util/kernel are correct.
Modules that will be deleted contain many `TODO` comments
indicating they may crash and/or produce incorrect results
when strings contain null characters and numerals are big.
cc @kha
@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.
After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.
I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
