Leonardo de Moura
bd9df3b08f
fix(library/tactic/goal): null hypothesis being added by to_goal
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:03:06 -08:00
Leonardo de Moura
872434e632
fix(kernel/has_free_vars): return false for null expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:01:57 -08:00
Leonardo de Moura
147626c906
fix(kernel/printer): memory access violation when printing contexts
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:50:29 -08:00
Leonardo de Moura
0390f3c39b
feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:01:54 -08:00
Leonardo de Moura
1df9d18891
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 14:49:39 -08:00
Leonardo de Moura
2ddcc32c1d
fix(frontends/lean/notation): change the precedence of '->'
...
It should match the precedence of the implication '=>'.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:23:24 -08:00
Leonardo de Moura
d79a626523
fix(kernel/type_checker): Pi with metavariables case
...
The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:07:59 -08:00
Leonardo de Moura
fa03ae2a26
fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints
...
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:04:34 -08:00
Leonardo de Moura
d46cf5fdd5
fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 05:13:29 -08:00
Leonardo de Moura
c841763a05
feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 04:51:07 -08:00
Leonardo de Moura
4e4fea1eca
fix(examples/lean): add all examples to test suite
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 21:54:55 -08:00
Leonardo de Moura
13f9454fe1
feat(library/tactic/proof_state): add option tactic::proof_state::goal_names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 21:18:22 -08:00
Leonardo de Moura
e6fb6f7d1e
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:08:51 -08:00
Leonardo de Moura
0c059a9917
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:06:32 -08:00
Leonardo de Moura
1b176204b4
feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 19:03:12 -08:00
Leonardo de Moura
c1afefb873
feat(library/fo_unify): unify heterogeneous - homogeneous equality
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 19:00:31 -08:00
Leonardo de Moura
e1d44eec6b
fix(frontends/lean/parser): bug in parse_tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:40:55 -08:00
Leonardo de Moura
a564795fe6
fix(frontends/lean/parser): remove unnecessary '#' after error
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:27:08 -08:00
Leonardo de Moura
e069ce640b
feat(frontends/lean/parser): add tactic abort command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:15:19 -08:00
Leonardo de Moura
34654ad06b
feat(tests/lean/interactive): add interactive mode test script
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 16:56:20 -08:00
Leonardo de Moura
e3848d43a2
feat(frontends/lean): improve tactic command parsing in interactive mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 16:28:08 -08:00
Leonardo de Moura
a1b5a8e50f
fix(frontends/lean): check wheter the synthesized proof term has metavars or not
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 14:22:19 -08:00
Leonardo de Moura
873a07d34c
feat(kernel/replace_visitor): check interrupted flag and stackoverflow
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 05:42:12 -08:00
Leonardo de Moura
43ef8b9a4b
refactor(library/tactic): rename boolean.* to boolean_tactics.*
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 05:03:18 -08:00
Leonardo de Moura
fa98c1358f
feat(library/tactic): add disj_tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 04:49:06 -08:00
Leonardo de Moura
056759880c
feat(frontends/lean): add back (backtracking) command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 04:39:08 -08:00
Leonardo de Moura
029ef57abd
feat(library/tactic): add apply_tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 03:22:12 -08:00
Leonardo de Moura
7b4ea75dee
fix(frontends/lean): do not display Ctrl-D message on Windows
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 11:39:30 -08:00
Leonardo de Moura
d949dfd46d
fix(util/stackinfo): compilation warning on cygwin/mingw
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 11:32:39 -08:00
Leonardo de Moura
1e5518002b
feat(shell/lean): add git hash to executable
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 11:23:15 -08:00
Leonardo de Moura
e60e20a11d
feat(frontends/lean): add Exit command
...
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>
2013-12-04 10:40:22 -08:00
Leonardo de Moura
fa35fd6989
chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly
...
When LEAN_THREAD_UNSAFE=ON, we:
- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 10:27:22 -08:00
Leonardo de Moura
1a02abf7b2
feat(util/script_state): add a lua hook function that checks for the interrupt flag
...
This is a very convenient feature for interrupting non-terminating user scripts.
Before this commit, the user had to manually invoke check_interrupt() in potentially expensive loops. Now, this is not needed anymore.
Remark: we still have to check whether this trick works with LuaJIT or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 09:57:36 -08:00
Leonardo de Moura
ef6a27fe84
feat(util/script_state): add join method to Lua threads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 09:15:09 -08:00
Leonardo de Moura
def186a9cd
fix(util/stackinfo): try to fix incorrect main thread stack size on OSX
...
This fix tries to fix two failures on our unit tests.
tests/kernel/normalizer
tests/kernel/type_checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 08:56:46 -08:00
Leonardo de Moura
d481cb251d
chore(memcheck): add another suppression for LuaJIT
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 08:32:44 -08:00
Leonardo de Moura
fd9781d58d
fix(util/stackinfo): compilation warning on mingw and cygwin
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 08:26:50 -08:00
Leonardo de Moura
ef069e39b0
chore(*): replace to_expr with to_nonnull_expr (when appropriate)
...
The goal is to make the Lua API more robust.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:53:53 -08:00
Leonardo de Moura
bcc8b67592
chore(*): consistent file name convention
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:40:52 -08:00
Leonardo de Moura
8e53643b61
feat(library/fo_unify): first order unification
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:21:21 -08:00
Leonardo de Moura
f80106a895
chore(*): use 'explicit operator bool' everywhere.
...
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.
...
object const & obj = find_object(const_name(n));
if (obj && obj.is_builtin() && obj.get_name() == n)
...
obj.get_name() has type lean::name
n has type lean::expr
Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.
After this commit, the compiler correctly signs the error.
The correct code is
...
object const & obj = find_object(const_name(n));
if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 23:02:45 -08:00
Leonardo de Moura
d79b2babd3
fix(*): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 08:46:47 -08:00
Leonardo de Moura
dd62af1641
feat(frontends/parser): simplified theorem definition using tactical proof
...
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>
2013-12-02 08:20:18 -08:00
Leonardo de Moura
25978118df
feat(library/tactic): add beta-reduction tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 08:10:51 -08:00
Leonardo de Moura
39b99683a8
fix(util/stackinfo): handle error codes in the Linux version
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 07:56:53 -08:00
Soonho Kong
31b26f53ad
fix(util/stackinfo): fix typo
2013-12-02 00:03:57 -05:00
Soonho Kong
7776f4b24b
fix(util/stackinfo): fix preprocessor directive
2013-12-01 23:44:58 -05:00
Soonho Kong
4de3b772fd
feat(util/stackinfo): implement get_stack_size (Mac OSX version)
2013-12-01 22:24:12 -05:00
Soonho Kong
a2d6918348
fix(library/rewriter): use Abst axiom in lambda_body RW
2013-12-01 22:24:12 -05:00
Soonho Kong
0553d29078
test(library/rewriter): add lambda_rewrite tests
2013-12-01 22:24:12 -05:00