michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
1797 commits 3 branches 0 tags 28 MiB
Commit graph

1552 commits

Author SHA1 Message Date
Leonardo de Moura
6cc57cc4b5 fix(library/tactic/apply_tactic): bug in apply_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 15:54:56 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 14:23:06 -08:00
Leonardo de Moura
879ab6924a tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 12:26:53 -08:00
Soonho Kong
de018220e1 feat(*): use std::make_shared to create shared_ptr 2013-12-24 14:32:50 -05:00
Leonardo de Moura
00e89190c2 refactor(library/cast): use .lean file instead of .cpp file to define casting library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 22:04:19 -08:00
Leonardo de Moura
d5dc5cb576 feat(frontends/lean/parser): use LEAN_PATH in the Import command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 22:00:44 -08:00
Leonardo de Moura
8c8cefcb0c feat(frontends/lean/parser): compact definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 21:24:50 -08:00
Leonardo de Moura
5fd3fa1c0e chore(memcheck.supp): add suppression for readline problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 17:27:04 -08:00
Leonardo de Moura
b83b17d3ab fix(kernel/metavar): bug at cached_metavar_env::update method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 15:41:02 -08:00
Leonardo de Moura
5043cc75f6 fix(frontends/lean/parser): allow parenthesis in level expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 13:31:55 -08:00
Leonardo de Moura
5244ccafe8 fix(frontends/lean/parser): readline compilation problem on Fedora19 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 13:12:39 -08:00
Leonardo de Moura
702f0c2190 fix(tests/kernel/free_vars): reduce example stack size consumption 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 12:57:25 -08:00
Leonardo de Moura
7c05eb4695 fix(frontends/lean/parser): make sure Lean passes all tests when being compiled with the readline library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 12:57:25 -08:00
Leonardo de Moura
bcb41cd938 fix(util/lean_path): warnings produced by Valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 10:02:48 -08:00
Leonardo de Moura
f0833b6f46 chore(frontends/lua/lean.lua.h): fix style warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 21:34:20 -08:00
Leonardo de Moura
b5d23619cb feat(util/script_state): add 'import' command to Lua, it import files from the LEAN_PATH 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 21:27:12 -08:00
Leonardo de Moura
84c984a435 feat(build): copy extra files to bin directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 21:00:32 -08:00
Leonardo de Moura
e91fdaed00 refactor(frontends/lean): rename lean.lua to lean.lua.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 20:16:31 -08:00
Leonardo de Moura
e5f53595b6 fix(util/lean_path): bug at init_lean_path (it was missing last path), and add normalization function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 19:38:32 -08:00
Leonardo de Moura
50de85ee29 fix(util/lean_path): get_exe_location for Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 19:13:41 -08:00
Leonardo de Moura
cc9e16c3fc feat(util/lean_path): add function for searching for a file in the LEAN_PATH 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 18:47:49 -08:00
Leonardo de Moura
baf99779dc feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 17:57:51 -08:00
Leonardo de Moura
777582380f feat(util/lean_path): add support for LEAN_PATH 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 17:56:53 -08:00
Leonardo de Moura
df1b21a03d feat(util/exe_location): add function for finding the location of the executable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 17:12:31 -08:00
Leonardo de Moura
3e32d9bef2 feat(library/tactic): add support for Pi's at to_proof_state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 16:40:55 -08:00
Leonardo de Moura
104bd990e1 feat(library/tactic): add normalize_tac, eval_tac and trivial_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 14:10:42 -08:00
Leonardo de Moura
21d244d880 feat(frontends/lean/parser): allow tactic to be used to fill holes in definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 12:08:25 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 11:51:38 -08:00
Leonardo de Moura
9bac91f5ef fix(frontends/lean): libreadline support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 18:57:15 -08:00
Leonardo de Moura
9128a437b8 refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 18:23:37 -08:00
Leonardo de Moura
df58eb132e feat(frontends/lean): simplify explicit version names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 17:05:25 -08:00
Leonardo de Moura
36b2ec9abb fix(library/cast): bugs in Cast semantic attachment 
TODO: revise cast semantic attachment.
It should be axioms instead of semantic attachments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 16:16:54 -08:00
Leonardo de Moura
aebff0b4d3 fix(library/type_inferer): bug in get_range method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 14:55:07 -08:00
Leonardo de Moura
90dbdaec40 feat(kernel/expr): cache is_arrow result 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 13:59:45 -08:00
Leonardo de Moura
1faf42e2e1 chore(kernel/expr): remove unnecessary #if-#then-#else 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 13:36:41 -08:00
Leonardo de Moura
97145c0f88 fix(library/elaborator): bug in free variable normalization (lift was missing) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:41:09 -08:00
Leonardo de Moura
7b0b363b32 fix(kernel/normalizer): metavariable reification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:40:26 -08:00
Leonardo de Moura
fddcdb8f40 fix(library/elaborator): bug in process_lower 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 04:13:14 -08:00
Leonardo de Moura
ce84fe5d33 feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 22:00:50 -08:00
Leonardo de Moura
bb81311e0a feat(frontends/lean/parser): include proof state in exception for tactic failure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 17:15:12 -08:00
Leonardo de Moura
84df182beb refactor(kernel/instantiate): remove hackish (dead) function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:37:05 -08:00
Leonardo de Moura
4d05a8b65b fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:17:04 -08:00
Leonardo de Moura
1ed4aa391c fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality 
For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:14:20 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque 
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>
 2013-12-20 12:47:47 -08:00
Leonardo de Moura
026f666526 feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 11:22:13 -08:00
Leonardo de Moura
daef2b7b24 feat(util/sexpr/options): add is_eqp predicate for options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 10:53:53 -08:00
Leonardo de Moura
4838c055b8 feat(kernel/environment): add set_opaque method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 10:45:44 -08:00
Leonardo de Moura
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden 
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 02:16:49 -08:00
Leonardo de Moura
cb48fbf3c4 fix(library/elaborator): missing case 
The elaborator was failing in the following scenario:
- Failing constraint of the form
     ctx |- ?m1 =:= ?m2
where
     ?m2 is assigned to ?m1,
     and ?m1 is unassigned.

has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 01:39:43 -08:00
Leonardo de Moura
96ea8b81c8 feat(frontends/lean/parser): change show-expression binder name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 01:30:18 -08:00
Leonardo de Moura
c730dd7872 feat(frontends/lean/parser): propagate position information to expressions created by macro implemented in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 01:07:37 -08:00
Leonardo de Moura
3eb4de6760 fix(frontends/lean/parser): fix deadlock in macro parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 21:40:00 -08:00
Leonardo de Moura
c77464703f feat(frontends/lean): macro definition using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 19:08:10 -08:00
Leonardo de Moura
b08c606696 fix(library/io_state): bug in the io_state Lua bindings 
This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 16:39:42 -08:00
Leonardo de Moura
2648f41eaa test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 16:16:56 -08:00
Leonardo de Moura
d9e692f506 feat(frontends/lean): improve coercion manangement 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 15:45:46 -08:00
Leonardo de Moura
f43db96e1f fix(frontends/lean/pp): pretty printer for Type 
Add parenthesis around Type when it has a universe.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 15:24:45 -08:00
Leonardo de Moura
ae01d3818d fix(frontends/lean/parser): parse_type method 
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>
 2013-12-19 15:24:34 -08:00
Leonardo de Moura
46627289b8 fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 14:47:53 -08:00
Leonardo de Moura
6cc83dbe2a fix(kernel/kernel_exception): incorrect pp method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 14:46:22 -08:00
Leonardo de Moura
d3d24696f4 feat(frontends/lean): hide builtin object in the 'Show Environment' command 
The user can still display builtin objects by using

    Show Environment all

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 14:00:58 -08:00
Leonardo de Moura
ad3f771b1d feat(frontends/lean): hide 'explicit' version of objects with implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 13:12:39 -08:00
Leonardo de Moura
bff5a6bfb2 fix(frontends/lean/pp): make sure pp and parser are using the same precedences 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 12:46:14 -08:00
Leonardo de Moura
02bd166793 chore(library/basic_thms): fix typo in comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 12:22:05 -08:00
Leonardo de Moura
dd72269b13 feat(frontends/lean): rename command Set to SetOption 
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 21:18:48 -08:00
Leonardo de Moura
d7886c4f5f doc(examples/lean): new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 21:03:16 -08:00
Leonardo de Moura
8cfe5cf9ed fix(frontends/lean/pp): pretty printer was ignoring notation decls in the local scope 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 18:00:37 -08:00
Leonardo de Moura
79fa6e4940 feat(frontends/lean): Scopes in the default Lean frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 17:40:21 -08:00
Leonardo de Moura
97b872a05c refactor(frontends/lean): remove frontend class, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 14:37:55 -08:00
Leonardo de Moura
2aaa9a5273 feat(frontends/lean/parser): change function application precedence 
Now, we can write

  Pi (x y : A), R x y -> R y x

instead of

  Pi (x y : A), (R x y) -> (R y x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 12:44:15 -08:00
Leonardo de Moura
47c7bb1bde refactor(*): uses aliases for unordered_map and unordered_set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 12:30:45 -08:00
Leonardo de Moura
1e4fa76a47 feat(util/name_map): add template alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 11:34:40 -08:00
Leonardo de Moura
7b2fea3fab fix(kernel/normalizer): compilation problem with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 08:46:36 -08:00
Leonardo de Moura
418623b874 feat(kernel/replace_fn): add template replace that captures commonly used pattern 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 18:31:59 -08:00
Leonardo de Moura
23e518001a feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 18:10:13 -08:00
Leonardo de Moura
10f28c7bec feat(kernel/replace_fn): non-recursive replace_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 16:35:39 -08:00
Leonardo de Moura
af4a6c9364 fix(kernel/normalizer): cache problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:52:14 -08:00
Leonardo de Moura
33789fad4c fix(kernel/builtin): make sure the if-then-else semantic attachment is not a simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:34:40 -08:00
Leonardo de Moura
c53233ea26 fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:33:42 -08:00
Leonardo de Moura
836357c65c fix(kernel/normalizer): bug in Let normalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 12:35:25 -08:00
Leonardo de Moura
84bfe2a222 fix(library/elaborator): bug in process_meta_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 10:56:20 -08:00
Leonardo de Moura
09b51a0fb7 fix(library/elaborator): missing condition 
The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 17:13:36 -08:00
Leonardo de Moura
f09fd0fc04 feat(kernel/printer): include de Bruijn index in the debug printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:56:46 -08:00
Leonardo de Moura
91f4ced83b feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:41:20 -08:00
Leonardo de Moura
7792561b20 fix(library/type_inferer): another incorrect use of scoped_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:17:19 -08:00
Leonardo de Moura
af42078205 fix(kernel): incorrect use of scoped_map 
This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:11:39 -08:00
Leonardo de Moura
2fee2def72 feat(library/basic_thms): simplify DoubleNegElim 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 13:19:19 -08:00
Leonardo de Moura
de53e92de8 feat(library/basic_thms): add ExistsElim theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 12:43:34 -08:00
Leonardo de Moura
8f5c2b7d9f feat(library/basic_thms): add Refute theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 12:03:31 -08:00
Leonardo de Moura
8f9405c8b3 fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive 
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 09:39:02 -08:00
Leonardo de Moura
61bd27ff06 fix(library/elaborator): bug in simple_ho_match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 21:48:55 -08:00
Leonardo de Moura
19ad39159e feat(library/basic_thms): add ForallIntro theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5 feat(library/basic_thms): add ExistsIntro theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 16:26:23 -08:00
Leonardo de Moura
2253d8079b chore(util/pdeque): remove unused template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:31:44 -08:00
Leonardo de Moura
993bea8206 refactor(library/elaborator): improve elaborator state data-structure 
The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:27:08 -08:00
Leonardo de Moura
5aa9264091 feat(util/list): add remove_last template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:08:10 -08:00
Leonardo de Moura
1b1032eb99 feat(util/list): improved filter that reuses list cells 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 20:15:37 -08:00
Leonardo de Moura
bdbf85405a feat(library/elaborator): add extra occurs-check test 
The idea is to catch the inconsistency in constraints such as:

    ctx |- ?m[inst:0 v] == fun x, ?m a x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 19:47:33 -08:00
Leonardo de Moura
160a8379ef feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed 
The modifications started at commit 1852c86948 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:59:35 -08:00
Leonardo de Moura
70b7e519f8 feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:54:49 -08:00
Leonardo de Moura
02ee31b786 feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:41:50 -08:00
Leonardo de Moura
3d30664611 feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:13:56 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' 
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 12:25:00 -08:00
Leonardo de Moura
51aee83b70 refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env 
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>
 2013-12-13 18:59:15 -08:00
Soonho Kong
26afc6cf12 fix(cmake): fix problem of using LuaJit on OSX(64-bit) 
http://luajit.org/install.html

If you're building a 64 bit application on OSX which links directly or
indirectly against LuaJIT, you need to link your main executable with
these flags:

    -pagezero_size 10000 -image_base 100000000
 2013-12-13 19:52:40 -05:00
Leonardo de Moura
2e5e5e187f chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 15:01:24 -08:00
Leonardo de Moura
3416df85f8 fix(util/thread): warning 'thread.cpp.o has no symbols' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 14:00:40 -08:00
Leonardo de Moura
fa8b984e27 fix(kernel/environment): compilation warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 13:54:45 -08:00
Soonho Kong
46e7802d9a test(library/rewriter): add lambda_{body/type}_rewriter tests 2013-12-13 15:08:23 -05:00
Soonho Kong
5b95cf1e03 fix(shell/lua_repl.h): use loadstring for Lua-5.1 instead of load 2013-12-13 00:13:48 -05:00
Soonho Kong
f90a9e96d0 fix(shell/lean.cpp): fix not to overwrite optind by getopt_long 2013-12-12 23:20:47 -05:00
Leonardo de Moura
ae52c8062e chore(kernel/metavar): remove unused function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:39:14 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:27:30 -08:00
Leonardo de Moura
f97c260b0b refactor(kernel/environment): add ro_environment 
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>
 2013-12-12 16:48:34 -08:00
Leonardo de Moura
7b2cbd6926 chore(kernel/environment): remove implementation hack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:34 -08:00
Leonardo de Moura
7d184c3c4b fix(util/shared_mutex) missing pragma 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:34 -08:00
Leonardo de Moura
3457fe5935 chore(kernel): rename read_only_environment and read_write_environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
1852c86948 feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
058bdb88ac feat(kernel/context): add operator== for contexts, and new constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
38a25a1bd2 feat(kernel/metavar): (re-)enable add_lift simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
6ed62247b0 chore(memcheck.supp): generalize Memcheck:Addr4 suppression for LuaJIT, there many warnings of this kind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 09:24:15 -08:00
Leonardo de Moura
98f5ce0512 fix(kernel/context): unused var warning in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 21:24:05 -08:00
Leonardo de Moura
3e77dd0c42 fix(kernel/context): make context remove more robust 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:51:57 -08:00
Leonardo de Moura
f728f80960 fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:41:24 -08:00
Leonardo de Moura
8f67348c05 fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:27:21 -08:00
Leonardo de Moura
c29b155fdd feat(library/elaborator): use improved has_free_vars in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 16:15:20 -08:00
Leonardo de Moura
0e2b7973cf feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 16:09:33 -08:00
Leonardo de Moura
af1b0d2e81 feat(library): add function free_var_range for computing the range [0, R) of free variables occurring in an expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 15:32:50 -08:00
Leonardo de Moura
1d33d3b5db fix(library/elaborator): the context of auxiliary metavariables created in the imitation step was incorrect 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 12:35:32 -08:00
Leonardo de Moura
55389cf6e5 feat(kernel/context): add find, a version of lookup that does not throw an exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 09:54:54 -08:00
Leonardo de Moura
cdec9762ce chore(util/pvector): remove unused template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 20:32:10 -08:00
Leonardo de Moura
f8e87436a7 perf(library/elaborator): avoid exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:40:59 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:26:58 -08:00
Leonardo de Moura
5ae71e75bd perf(library/elaborator): avoid exception 
Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:31:36 -08:00
Leonardo de Moura
1fb526a3d4 perf(library/type_inferer): improve is_proposition performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:18:45 -08:00
Leonardo de Moura
b270fb0030 refactor(library/elaborator): remove synthesizer 
Synthesizer is not part of the elaborator anymore.
The elaborator fills the "easy" holes.
The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 15:55:54 -08:00
Leonardo de Moura
bbaa83e16a feat(frontends/lean): implement relaxed operator compatibility in the parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 15:42:43 -08:00
Leonardo de Moura
c0b9c7ffc4 refactor(library/io_state): simplify regular/diagnostic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 13:09:35 -08:00
Leonardo de Moura
e0eeb7c8d5 feat(frontends/lean/operator_info): add << for diagnostic and regular streams 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:52:31 -08:00
Leonardo de Moura
90f88acf42 feat(frontends/lean): relax compatible_denotation predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:42:29 -08:00
Leonardo de Moura
abe2cf2fb5 feat(frontends/lean): simplify how implicit parameters are marked 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:11:04 -08:00
Leonardo de Moura
88f80c9693 fix(shell): add 'file not found' error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 10:55:13 -08:00
Leonardo de Moura
78ec4b152b feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 09:48:24 -08:00
Leonardo de Moura
7ab321f568 chore(util): remove dead file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:32:11 -08:00
Leonardo de Moura
0cd8e3e76b feat(split-stack): add support for split-stacks (no more stackoverflows) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:30:54 -08:00
Leonardo de Moura
fd2a04e9ac fix(util/stackinfo): bug on Fedora 
Signed-off-by: Leonardo de Moura <leonardo@nod1-2008.corp.crtest.com>
 2013-12-09 18:44:14 -08:00
Leonardo de Moura
e3403492a5 feat(build): -D STATIC=ON option for building a static Lean executable 
On Linux, -D STATIC=ON does not work if MULTI_THREAD support is enabled.
If we search for "pthread static crash" we find other projects with the same problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 18:02:10 -08:00
Leonardo de Moura
0b1789edf2 feat(shell): add command line option to set thread stack size (only available if using Boost) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:33:47 -08:00
Leonardo de Moura
e7ae749221 feat(boost): implement multi-threading support using Boost 
To use Boost instead of the standard library, we must use the cmake option
    -D BOOST=ON

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:24:32 -08:00
Leonardo de Moura
533ed51f51 feat(util/shared_mutex): skip shared_mutex implementation if LEAN_MULTI_THREAD is not defined 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:42:08 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency 
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:20:26 -08:00
Leonardo de Moura
0eaa98221b fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 12:25:19 -08:00
Leonardo de Moura
0d10cba4a0 refactor(util/sexpr/format): minimize the use of recursion, combine be and layout into a single procedure (without creating a temporary potentially big sexpr) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 21:06:24 -08:00
Leonardo de Moura
25a2f5f7e0 fix(kernel/formatter): clang++ errors and warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 18:54:04 -08:00
Leonardo de Moura
445d4f6793 refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 18:11:35 -08:00
Leonardo de Moura
3ea09daf44 fix(frontends/lean/frontend): is_coercion for environment objects that have parents 
Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:47:00 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:33:18 -08:00
Leonardo de Moura
340d643d89 fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 16:55:55 -08:00
Leonardo de Moura
da613f67a8 refactor(frontends/lean/pp): replace dangerous frontend reference with a weak_ref to the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 16:42:12 -08:00
Leonardo de Moura
759fcb7b4f refactor(kernel/formatter): hide 'unsafe' constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:39:26 -08:00
Leonardo de Moura
68c2e5cc7d fix(frontends/lean/parser): reachable code 
The new test nbug1.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:22:21 -08:00
Leonardo de Moura
8add5571f1 refactor(library/tactic): remove 'null' tactic, and operator bool tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:00:16 -08:00
Leonardo de Moura
a4afdfeace refactor(kernel/expr): remove the dangerous expr::release method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:45:18 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:37:38 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:34:38 -08:00
Leonardo de Moura
25b812f1c9 feat(kernel/expr): no overhead optional<expr> template specialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:17:29 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
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>
 2013-12-07 23:21:10 -08:00
Leonardo de Moura
e4dff52d7a refactor(frontends/lean/parser): cleanup method apply_tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:44:47 -08:00
Leonardo de Moura
1ff6013594 fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes 
The test tactic14.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:37:59 -08:00
Leonardo de Moura
b6b520302d feat(kernel/replace_visitor): relax replace_visitor contract, the input expression can be null 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:35:26 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system 
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>
 2013-12-07 15:11:55 -08:00
Leonardo de Moura
33b72f1dd0 feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 13:09:39 -08:00
Leonardo de Moura
bc3a6a3185 refactor(frontends/lean/parser): cleanup tactic support in the default lean parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 12:15:03 -08:00
Leonardo de Moura
195ea24d71 refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer 
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:27:11 -08:00
Leonardo de Moura
5f3b9dbbbd fix(library/fo_unify): unify (?f ?x) with (g a b) 
We flat applications. So, (g a b) is actually ((g a) b).
So, we must be able to unify (?f ?x) with (g a b).
Solution:
        ?g <- (g a)
        ?x <- b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:25:11 -08:00
Leonardo de Moura
015bff8283 fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term 
This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form

 [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A

The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
     A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.

    Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
            let lemma1 := Conjunct1 assumption,
                lemma2 := Conjunct2 assumption
            in Conj (Conjunct2 assumption) (Conjunct1 assumption)

This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
     A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A

After this commit, the proof for theorem T1 is

Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
    let lemma1 := Conjunct1 assumption,
        lemma2 := Conjunct2 assumption
    in Conj lemma2 lemma1

as expected.

Finally, this example suggests that the encoding

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 : A := (by auto),
              lemma2 : B := (by auto)
          in (show B /\ A by auto)

is more efficient than

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:14:25 -08:00
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
Leonardo de Moura
75f8d56eb1 fix(util/stackinfo): memory leak at get_stack_size 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 19:17:28 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space 
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>
 2013-12-01 17:19:27 -08:00
Leonardo de Moura
1ec8f9d536 feat(kernel): add abstraction (aka function extensionality) axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 13:57:14 -08:00
Leonardo de Moura
09f98ecddc feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:41:05 -08:00
Leonardo de Moura
70e06f8e86 feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:27:27 -08:00
Leonardo de Moura
ca53a5a1cc feat(library/tactic): add unfold tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:56 -08:00
Leonardo de Moura
737e634556 fix(util/list): bug in map template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:24 -08:00
Leonardo de Moura
568931ccb1 refactor(library/tactic): remove duplicate code, add add_proofs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:01 -08:00
Leonardo de Moura
f91c4901e8 feat(library/tactic): add absurd_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Leonardo de Moura
bf2adb20e7 feat(library/tactic): add disj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Soonho Kong
6a6b69ddf4 test(library/rewriter): add test for depth RW 2013-12-01 01:59:21 -05:00
Soonho Kong
064e3fe20d refactor(library/rewriter): rename lc => ti 2013-12-01 01:59:20 -05:00
Soonho Kong
506cca0ac1 feat(library/rewriter): implement depth RW 2013-12-01 01:59:20 -05:00
Soonho Kong
ae0508128f refactor(library/rewriter): move apply_rewriter_fn into rewriter.h 2013-12-01 00:57:09 -05:00
Soonho Kong
d7ba5e3893 doc(library/rewriter): add doxygen annotations for rewrite_* funcs 2013-12-01 00:47:53 -05:00
Leonardo de Moura
1a221d8bbe feat(library/tactic): add focus tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
7ff791eb9f feat(util/name_set): add mk_unique (with respect to a name_set) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
6da13cc245 feat(util/list): map_append template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
fe79bbf2b7 feat(util/list): filter template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Soonho Kong
f205dd0763 fix(library/rewriter): unused variable warnings 2013-11-30 07:05:18 -05:00
Leonardo de Moura
83aaf64318 fix(library/tactic): memory leaks 
Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:44:39 -08:00
Leonardo de Moura
2372567a6e fix(util/luaref): warnings produced by valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:34:38 -08:00
Leonardo de Moura
a7027a1d00 feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:16:39 -08:00
Soonho Kong
aed8b1fc73 fix(tests/library/rewriter): app_rewriter1_tst 
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.
 2013-11-30 02:25:30 -05:00