We don't need to use `opaque` for `thunk` and `task`. Their recursor and
projections can be implemented in constant time. We just need to create
a closure which uses the runtime thunk_get/task_get primitive.
@kha I was working in the new declaration type and using tasks there.
Since we don't have tasks yet in Lean, I decided to start refactoring
the `thunk` type. I defined it as:
```
-- TODO(Leo): mark as opaque, it is implemented by the new runtime
structure thunk (α : Type u) : Type u :=
(fn : unit → α)
def thunk.pure {α : Type u} (a : α) : thunk α :=
⟨λ _, a⟩
def thunk.get {α : Type u} (t : thunk α) : α :=
t.fn ()
```
The idea is to use the runtime primitives to implement them.
Then, I realized the support for `thunk`s in the elaborator are quite
hacky. Given `f x`, if `f`'s domain has type `thunk A`, we elaborate
`f x` as `f (fun _, x)` even if `x` has type `thunk A`.
This is quite bad, for example, suppose we have
```
def f (x : thunk A) := ...
```
Then, the following definition is type incorrect.
```
def g (x : thunk A) := f x
```
and we are forced to write
```
def g (x : thunk A) := f (x ())
```
The term `f (x ())` will be elaborated as `f (fun _, x ())` and an
unnecessary closure is created at runtime.
This mechanism inherited from Lean 3 is also incompatible with the
new thunk definition. Given `x : thunk A`, I want to write `x.get`
to retrieve the value instead of `x ()` as in Lean 3.
However, `x.get` expands into the nonsensical `(fun _, x).get`.
So, I decided to view the mapping `A` to `thunk A` as a "coercion".
I used double quotes, because it is a macro instead of a function.
If it were a coercion, then we would be using `thunk.pure` to coerce
values but this is not we want most of the time.
For example, given `f : thunk A -> B` and a term `t : A`, when we write
`f t`, we want it to be converted into `f (fun _, t)` instead of
`f (thunk.pure t)` which would eagerly compute `t`. The transformation
`t` into `fun _, t` is syntactic.
We cannot implement it using type classes. I implemented it as
a hard-coded extra case like the one from `Prop` to `bool`.
We can also add a coercion from `thunk A` to `A` to avoid the `.get`.
That being said, I had a few breakages in the code base since we only
use coercions when the given and expected type do not contain
metavariables.
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.
Old MacDonald had a monad stack
eio = except_t io.error io
And in his stack he had I/O, io = state io.real_world
With a monad here and a monad there
Here a monad there a monad
Everywhere a monad!
Remark: the termination proofs are commented because Lean 4 is
currently ignoring them and accepting non-terminating functions.
These files are based on an experiment implemented using Lean 3.
We can find it here:
https://gist.github.com/leodemoura/f5d82426c105b5fae0880e77024f6e9c
We will use coroutines to implement the interaction between reader,
elaborator and main driver.
This change makes backtracking behavior more predictable and
matches Parsec and Megaparsec's behavior. While the original Parsec paper
motivates the old behavior by arguing it implements the "longest match" rule,
this is obviously only true in a very limited sense.
