This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.
example showing that the approach for caching metavar_env is broken in the type_checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
environment rw_env(env);
Now, f can use rw_env to update env.
To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.
ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.
The function check_system() is syntax sugar for
check_interrupted();
check_stack();
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
There was a bug in the app_rewriter1_tst. If we apply the ADD_COMM RW to
f(0), then the result should be f(0) since there is nothing to do for
ADD_COMM.
f(0) = f(0)
The proof for this equality should be Refl(Nat, f(0)). But it was
Refl(Nat -> Nat, f)
which is wrong. Somehow, the previous kernel didn't detect this type
mismatch and recent changes of the kernel found the problem.
I fixed the bug and re-enable the test as it was.
The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:
Theorem Th : a = a := Refl b
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
