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>
- The extension does not have to be provided.
- It can also import Lua files.
- Hierachical names can be used instead of strings.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The parser had a nasty ambiguity. For example,
f Type 1
had two possible interpretations
(f (Type) (1))
or
(f (Type 1))
To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
(Type 1)
(Type U)
(Type M + 1)
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>
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.
TODO: do the same for kernel objects, sexprs, etc.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remark: on Windows, Ctrl-D does not seem to work.
So, this commit also changes the Lean startup message.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
When using tactics for proving theorems, a common pattern is
Theorem T : <proposition> := _.
apply <tactic>.
...
done.
This commit allows the user to write the simplified form:
Theorem T : <proposition>.
apply <tactic>.
...
done.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write
apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
instead of
apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
For example, after this commit, we can write
simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic
instead of
simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++
The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.
Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.
The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:
try-for (T1 ORELSE T2) 5
It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
