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

2708 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Soonho Kong
e6df417440 chore(travis): use another repository to fix luajit problem on ubuntu 2013-12-23 16:43:22 -05: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
2c30b87f30 test(tests/lean): ExistsElim test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 12:57:25 -08:00
Soonho Kong
2cdd06b182 chore(travis): use ppa to install LuaJit-2.0.1 on Ubuntu 2013-12-23 15:35:51 -05: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
65f7217935 fix(tests/lean/norm_tac): display implicit parameters to make sure output can be parsed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 17:11:36 -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
55d46b2f88 test(tests/lean): add new normalizer/elaborator test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:43:25 -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
9444c1f47f test(tests/lean): add example that cannot be elaborated 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 04:19:53 -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
66f106da8c test(tests/lean): new error msg test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 03:20:04 -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