@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.
cc @kha
Reason: `rsimp` is based on the smt framework. The smt framework
has to be reimplemented. Moreover, the smt framework is currently
not using the new cache infrastructure and we pay a substantial
performance penalty.
@kha the following idiom is not safe
```
while (is_pi(t)) {
t = whnf(binding_body(t));
}
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
while (is_pi(t)) {
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
@aqjune @nunoplopes: See new tests at tests/lean/run/random.lean
We have two actions in `io`. By default, `io` uses the C++
random number generator, but we can force it to use a `std_gen` with
the action `set_rand_gen`.
def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat
def set_rand_gen : std_gen → io unit
@aqjune @nunoplopes: This commit adds basic support for random numbers.
It defines a random number generator interface, and an basic
implementation based on the Haskell one.
We can add more implementations in the future if neeeded.
The new test program has a few examples.
BTW, this is a pure Lean implementation.
If we need more performance we can provide an implementation
using C++.
@kha We can now solve unification constraints of the form
?m unit =?= itactic
I'm not very confident this new extension will improve usuability
instead of creating new counter-intuitive behavior.
At least, in the process of implementing it, I fixed two bugs,
and removed a nasty hack that was being used in the unifier.
Thus, even if we disable this feature in the future, some good came out
of it.
Although, the new extension locally increases the number of constraints
that can be solved, it may prevent terms that could be elaborated before
from being elaborated. I am not too concerned at this point because
I could not construct a natural example. I encountered one case, but it
was due to a problem that I fixed in the previous commit.
I reconstruct it here for the record. Suppose we have a constraint
?m_1 ?m_2 =?= itactic
Without the fix from the previous commit, `itactic` would unfold too
`id_rhs Type (tactic unit)`, and the constrain would be solved as
?m_1 := (id_rhs Type)
?m_2 := (tactic unit)
It succeeds locally, but the elaboration fails later when it tries to
synthesize the type class `has_bind (id_rhs Type)`.
The previous fixes the problem by making sure `itactic` is unfolded to
`tactic unit` as expected. `id_rhs` is an auxiliary definition
used to implement smart unfolding. That being said, the user could in
principle define `itactic` as `@id Type (tactic unit)`, and the constraint
?m_1 ?m_2 =?= itactic
will be solved as
?m_1 := (@id Type)
?m_2 := (tactic unit)
which is not the solution we want.
