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

1236 commits

Author SHA1 Message Date
Leonardo de Moura
b2b76b078f feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 20:43:53 -07:00
Leonardo de Moura
5b69f88664 feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:55:41 -07:00
Leonardo de Moura
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:11:19 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
8d584e54da feat(frontends/lean): add exact_apply 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 00:51:11 -07:00
Leonardo de Moura
33cb9382aa feat(frontends/lean): add beta-reduction tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 19:41:54 -07:00
Leonardo de Moura
360e9b9486 feat(library/tactic): add apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 18:33:53 -07:00
Leonardo de Moura
6645fdeae0 feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:24:13 -07:00
Leonardo de Moura
2510d5722a feat(frontends/lean): add unfold tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:05:45 -07:00
Leonardo de Moura
6d09d82a7c feat(frontends/lean): add notation for orelse tactic, add show and now tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:39:18 -07:00
Leonardo de Moura
a1bbb09de4 feat(frontends/lean): add notation for then tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:24:56 -07:00
Leonardo de Moura
ffa175009b feat(frontends/lean): use tactics for solving unassigned metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:50:16 -07:00
Leonardo de Moura
1e39a21823 feat(frontends/lean): add basic tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:51 -07:00
Leonardo de Moura
7d5522e36a chore(tests): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:51 -07:00
Leonardo de Moura
f5f3816596 chore(tests): cleanup test scripts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:39 -07:00
Leonardo de Moura
cf28981f45 feat(tests/lean/run): add test_single script that sets the LEAN_PATH 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 07:47:46 -07:00
Leonardo de Moura
193ce35419 refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 15:33:56 -07:00
Leonardo de Moura
0adacb5191 feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 13:57:36 -07:00
Leonardo de Moura
47ff300d1a fix(frontends/lean): '@' explicit mark 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 07:30:36 -07:00
Leonardo de Moura
9fb8fd0e7b test(tests/lua): add simple tactic framework test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 18:51:55 -07:00
Leonardo de Moura
5524c6c3d8 refactor(library/tactic/proof_state): simplify proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 14:49:48 -07:00
Leonardo de Moura
aaa7960b75 refactor(library/tactic/goal): use local names for hypotheses 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 11:11:12 -07:00
Leonardo de Moura
e55b4bf86d fix(library/unifier): bug in flex_rigid case: binding imitation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 20:43:49 -07:00
Leonardo de Moura
ccce9d90a4 feat(frontends/lean/elaborator): add 'delayed coercions', add example demonstrating why the new feature is useful 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 18:39:23 -07:00
Leonardo de Moura
340dc622c6 fix(kernel/formatter): make sure simple formatter output is not sensitive to internal names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 14:58:59 -07:00
Leonardo de Moura
150d285b39 fix (library/unifier): occurs_context_check 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 14:45:36 -07:00
Leonardo de Moura
16bdc51fc4 refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 13:36:31 -07:00
Leonardo de Moura
a70f8dd98e feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 11:05:14 -07:00
Leonardo de Moura
5e0e737213 feat(library/scoped_ext): do not import 'children' namespace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:32:34 -07:00
Leonardo de Moura
a7623845f9 test(tests/lean/run): add another example on how to deal with ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:18:35 -07:00
Leonardo de Moura
930960c54d fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:06:50 -07:00
Leonardo de Moura
cc21bfd01d test(tests/lean/run): more tests on how to deal with ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:26 -07:00
Leonardo de Moura
dc5553ea5c test(tests/lean/run): add test demonstrating how to control ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:19 -07:00
Leonardo de Moura
da6e92787a test(tests/lean/run): add simple overloading test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:12 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:50:49 -07:00
Leonardo de Moura
1da4ed5d80 fix(tests/lua/test.sh): update old script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:47:07 -07:00
Leonardo de Moura
d027c90bd0 fix(tests/lua/tc_bug1): update test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:50:30 -07:00
Leonardo de Moura
4bc1f3cf81 test(lean/run): add elaborator tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:15:01 -07:00
Leonardo de Moura
49a6048060 test(lean/run): add another test for new elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 13:18:32 -07:00
Leonardo de Moura
3e7dfa6212 fix(frontends/lean): infer type of definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:39:14 -07:00
Leonardo de Moura
d055c4880f feat(frontends/lean): connect new elaborator to frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:31:00 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
2c0f596665 fix(library/choice): avoid assertion violation when Lua API is misused 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:14:38 -07:00
Leonardo de Moura
3169f8c126 feat(library): add mk_explicit/is_explicit procedures for '@'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:11:27 -07:00
Leonardo de Moura
d915f0cc32 refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 09:00:14 -07:00
Leonardo de Moura
aa8b5655dd feat(frontends/lean): add notation overwrite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 16:10:36 -07:00
Leonardo de Moura
7df397fe63 test(lua): add universe constraint unifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 14:19:02 -07:00
Leonardo de Moura
60c60c6cf5 feat(library/kernel_bindings): add mk_choice_cnstr to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 13:39:21 -07:00
Leonardo de Moura
2fa5b17592 feat(library/unifier): add unifier.max_steps unifier.use_exceptions options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:38:57 -07:00
Leonardo de Moura
7b188ea37e feat(library/unifier): implement flex-rigid case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 11:00:35 -07:00
Leonardo de Moura
5bd86754af feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 17:51:00 -07:00
Leonardo de Moura
c8a07dee53 feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:27:04 -07:00
Leonardo de Moura
b936c4d860 test(lua): add type checker test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 14:13:30 -07:00
Leonardo de Moura
29a00c46d0 feat(library/unifier): add main loop and resolve_conflict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 11:57:10 -07:00
Leonardo de Moura
644c387cfe refactor(kernel/constraint): rename: level constraints are also equality constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:50:47 -07:00
Leonardo de Moura
1c47bd4847 fix(kernel/converter): remove temporary workaround, and temporarily disable unit test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:39:22 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:58:05 -07:00
Leonardo de Moura
eca22edda3 fix(kernel/type_checker): restore type checker cache when a failure occurs, do not send constraints to add_cnstr_fn when a type checker failure occurrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:00:32 -07:00
Leonardo de Moura
9c745057b4 feat(library/unifier): add unify_fn skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 20:08:39 -07:00
Leonardo de Moura
bf8f3318d8 feat(library): add unifier module skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 13:38:17 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
67088b130e refactor(kernel/constraint): simplify constraint interface, and add choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
2589d60bfd feat(frontends/lean): add nameless 'have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 17:18:18 -07:00
Leonardo de Moura
4b227409bf feat(frontends/lean): add 'then have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 14:27:21 -07:00
Leonardo de Moura
4560413a92 feat(frontends/lean): add '[fact]' modifier for 'have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
39177ec10a feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
5c17411a86 fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 09:46:58 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 16:00:59 -07:00
Leonardo de Moura
3bb53810c5 test(lean/run): add notation test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 09:48:47 -07:00
Leonardo de Moura
08845be2fc feat(frontends/lean/notation_cmd): improve 'notation' cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 09:28:01 -07:00
Leonardo de Moura
3e3c4ee5ed feat(frontends/lean/parser): add local_scope object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 08:38:23 -07:00
Leonardo de Moura
6259d20218 feat(frontends/lean/parser): expand Lua parser API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 08:03:17 -07:00
Leonardo de Moura
813e033f54 test(lean): add simple example of notation implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:37:22 -07:00
Leonardo de Moura
32d54ef9a3 fix(tests/lua): remove os.exit(0), it does not work if it is executed in the scope of a lock 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:17:06 -07:00
Leonardo de Moura
1378fa5cbb refactor(util/script_state): remove support for threads and communication channels from the Lua API, the goal is to keep is simple, and use one Lua state object per thread 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 21:56:45 -07:00
Leonardo de Moura
4cbc429192 feat(frontends/lean/calc): add parse_calc function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 17:16:15 -07:00
Leonardo de Moura
e178979061 feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 13:35:31 -07:00
Leonardo de Moura
819c8276f2 feat(frontends/lean/builtin_cmds): add 'variables' command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 08:25:00 -07:00
Leonardo de Moura
ea49176043 feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 18:42:39 -07:00
Leonardo de Moura
639d58f4c7 feat(frontends/lean/builtin_cmds): add 'print options' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 17:31:28 -07:00
Leonardo de Moura
3e377a9732 feat(frontends/lean/builtin_cmds): add 'set_option' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 17:27:43 -07:00
Leonardo de Moura
4f3da90443 feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 15:04:29 -07:00
Leonardo de Moura
2c4175341c feat(library/placeholder): allow types to be attached to placeholders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:35:55 -07:00
Leonardo de Moura
873a5c8605 test(lean): add 'let' expression test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:11:26 -07:00
Leonardo de Moura
21c54755a9 fix(kernel/converter): bug in is_def_eq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:09:12 -07:00
Leonardo de Moura
f70b1b028a feat(frontends/lean): provide position to parse_fn external function, add 'by' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 12:28:58 -07:00
Leonardo de Moura
34dfacc10e refactor(frontends/lean): Bool does not need to be a reserved keyword 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 10:52:12 -07:00
Leonardo de Moura
6db265e7ab feat(frontends/lean/builtin_exprs): parse '_' placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 10:41:08 -07:00
Leonardo de Moura
5ce0502a36 feat(frontends/lean/builtin_exprs): add parser for 'let' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 09:50:34 -07:00
Leonardo de Moura
27130c9499 feat(frontends/lean): local notation 'shadows' global one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 11:50:41 -07:00
Leonardo de Moura
28047a33ae feat(frontends/lean): add local notation support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 11:30:52 -07:00
Leonardo de Moura
64cafd6875 feat(frontends/lean/notation_cmd): add 'notation' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 10:49:05 -07:00
Leonardo de Moura
9b389a96d5 feat(frontends/lean/notation_cmd): modify infixl/infixr/postfix command syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 08:28:49 -07:00
Leonardo de Moura
e7019ec840 feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 22:13:25 -07:00
Leonardo de Moura
891a3fb48b feat(frontends/lean): add command block reader with snapshot and resume 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 14:13:32 -07:00
Leonardo de Moura
5fee6fd140 feat(shell/lean): add '-o' command line option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 08:10:43 -07:00
Leonardo de Moura
282a35bd1b feat(frontends/lean): add '#setline' directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 07:28:56 -07:00
Leonardo de Moura
fad4780d72 test(lean/run): add overload test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 18:06:44 -07:00
Leonardo de Moura
48c58af9b5 feat(frontends/lean/parser): allow explicit universe level to be provided to aliases and locals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 18:00:52 -07:00
Leonardo de Moura
a65c43c0db feat(frontends/lean/builtin_cmds): add definition command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 17:30:35 -07:00
Leonardo de Moura
01cecb76db feat(frontends/lean/builtin_cmds): add 'variable' command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 15:13:50 -07:00
Leonardo de Moura
ce259e6265 feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 11:34:43 -07:00
Leonardo de Moura
5aca452439 feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 08:26:05 -07:00
Leonardo de Moura
cccec51c1e test(lua): add get_user_coercions test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 22:18:27 -07:00
Leonardo de Moura
a914345d29 feat(library): new scoping framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 19:33:02 -07:00
Leonardo de Moura
d50376249f feat(library/aliases): add level aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:35:02 -07:00
Leonardo de Moura
3bde699fbe feat(frontends/lean/parser): add parse_level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:34:55 -07:00
Leonardo de Moura
cffbae3667 test(tests/lean/run): add new test group, where we just execute Lean (and don't check output) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 21:07:23 -07:00
Leonardo de Moura
05edbe00ad chore(shell): re-activate .lean tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:36:42 -07:00
Leonardo de Moura
4f83b1a50b feat(library): add choice expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:35:34 -07:00
Leonardo de Moura
1972a09021 feat(frontends/lean/builtin_cmds): add simple 'print' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:35:34 -07:00
Leonardo de Moura
2e8ebb6d9e feat(frontends/lean/parser): add 'parse_commands' and 'parse_script' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:32:07 -07:00
Leonardo de Moura
637eae40ad feat(library/aliases): add support for alias overloading 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 10:05:51 -07:00
Leonardo de Moura
d81df2efe2 feat(frontends/lean/parse_table): add use_lambda_abstraction flag to scoped_expr_actions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 09:39:01 -07:00
Leonardo de Moura
546f9dc00b chore(frontends/lean): use consistent name conventions, rename token_set to token_table 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 09:18:57 -07:00
Leonardo de Moura
00e0cc15ba feat(frontends/lean/token_set): add token_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-09 16:49:22 -07:00
Leonardo de Moura
439b6c1e96 feat(frontends/lean/parse_table): add parse_table Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-09 15:33:39 -07:00
Leonardo de Moura
1c96373c1a feat(library/kernel_bindings): expose replace_fn in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-04 15:26:55 -07:00
Leonardo de Moura
4a25e7442a feat(kernel/expr): add optional expression caching (aka "partial" hash-consing) 
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 15:35:47 -07:00
Leonardo de Moura
45a3ab5141 refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value 
Moreover, we could create type incorrect aliases by "accident".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 15:20:14 -07:00
Leonardo de Moura
076414693a feat(library/kernel_bindings): improve argument validation in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 10:17:12 -07:00
Leonardo de Moura
ab5f570924 refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 00:46:28 -07:00
Leonardo de Moura
712c10f818 fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 15:39:57 -07:00
Leonardo de Moura
b6d2328c1d fix(library/scope): make sure local levels are added in the beginning of the universe parameter list 
The idea is to make sure it is consistent with the behavior used for regular local parameters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 14:06:31 -07:00
Leonardo de Moura
e9664cb042 fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 13:57:43 -07:00
Leonardo de Moura
9b6b162a7c fix(library/scope): bug when abstracting inductive declaration in the end of a section 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 13:46:16 -07:00
Leonardo de Moura
2a101657c8 test(lua): add section+inductive_family test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 13:07:13 -07:00
Leonardo de Moura
6ee272477a fix(library/private): bug when preserving private names at end_section 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 11:32:14 -07:00
Leonardo de Moura
936ca80b9b fix(library/scope): bug in add_definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 11:04:34 -07:00
Leonardo de Moura
e56307f006 fix(library/scope): bug in end_scope procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 10:43:28 -07:00
Leonardo de Moura
6e113206b6 feat(library/scope): add support for inductive datatypes in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 10:28:07 -07:00
Leonardo de Moura
d36ef5dcbe feat(library/private): preserve 'hidden/private name => user name' map when section is closed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-01 18:09:11 -07:00
Leonardo de Moura
585f3adde1 feat(library/scope): add sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-01 17:55:11 -07:00
Leonardo de Moura
286d7f0e64 feat(library): add namespace management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 15:41:01 -07:00
Leonardo de Moura
3145cee51f refactor(library/aliases): move replace_prefix to util/name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 15:11:22 -07:00
Leonardo de Moura
37b5570e99 test(lua): add .olean corrupted file tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 12:51:33 -07:00
Leonardo de Moura
7bd10c2d2d feat(library/module): export global universe level declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 12:12:41 -07:00
Leonardo de Moura
1b5366cfb7 feat(library): add module for implementing aliases and 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 21:42:40 -07:00
Leonardo de Moura
6902d8cb05 feat(library): add simple placeholder module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 20:28:28 -07:00
Leonardo de Moura
72f9e26dab refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 17:52:01 -07:00
Leonardo de Moura
cba52b76c7 test(lua): add integer datatype test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 16:30:33 -07:00
Leonardo de Moura
6587d0f8f3 test(lua): add is_sorted inductive predicate example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 16:30:32 -07:00
Leonardo de Moura
128d668f03 feat(library): add support for creating 'private/hidden' names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 18:37:09 -07:00
Leonardo de Moura
bfa9b90af0 feat(library/kernel_bindings): used 'named' parameters in import_modules API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 11:03:44 -07:00
Leonardo de Moura
ade5d99023 feat(library/modules): add option for discarding the proof of imported theorems (after checking them) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 10:56:28 -07:00
Leonardo de Moura
0f894f4618 chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 17:47:53 -07:00
Leonardo de Moura
162fa25250 test(lua): move slow tests to tests/lua/slow 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 10:24:18 -07:00
Leonardo de Moura
3608826e4c test(lua): add inductive decl serialization test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 15:54:41 -07:00
Leonardo de Moura
bb9830f10c test(shell): add command line tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 04:53:04 -07:00
Leonardo de Moura
dbe55bf84a test(lua): add Lua State tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 04:43:44 -07:00
Leonardo de Moura
701b60d2d9 test(lua): add Lua 'yield' test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 04:39:53 -07:00
Leonardo de Moura
38a826013c test(lua): add import Lua file test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 04:34:34 -07:00
Leonardo de Moura
2d31c6c0b2 feat(library/coercion): improve get_user_coercions API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 11:35:47 -07:00
Leonardo de Moura
bb6db41414 test(lua): add 'multiple inheritance' test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 11:15:25 -07:00
Leonardo de Moura
e058839d24 fix(library/coercion): allow cycles in the coercion graph 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 11:08:49 -07:00
Leonardo de Moura
71b555ab15 test(lua): coercion module error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 10:01:04 -07:00
Leonardo de Moura
ef14c3d67e fix(library/coercion): coercion replacement 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 09:49:26 -07:00
Leonardo de Moura
fc1819aadd test(lua): coercion serialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:38:50 -07:00
Leonardo de Moura
0d02f933cb test(lua): add coercion sort-class tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:29:47 -07:00
Leonardo de Moura
e28446710e test(lua): add coercion to function-class tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:22:28 -07:00
Leonardo de Moura
a9a5f8628f test(lua): add coercion module tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 07:45:49 -07:00
Leonardo de Moura
69e5156034 test(lua): add import 'diamond' tst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 16:49:43 -07:00
Leonardo de Moura
879572ee7e fix(kernel/module): non-termination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 15:12:47 -07:00
Leonardo de Moura
e4f09335ce test(lua): new module system test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 14:54:20 -07:00
Leonardo de Moura
46c292be71 test(lua): add simple module export/import test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:26:28 -07:00
Leonardo de Moura
69f6930bd7 test(lua): add Acc datatype declaration test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:26:02 -07:00
Leonardo de Moura
ce634d4459 test(lua): well-founded induction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-22 14:10:25 -07:00
Leonardo de Moura
1447d7e765 test(lua): add another inductive datatype example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-22 14:10:25 -07:00
Leonardo de Moura
6246fae32c fix(kernel/inductive): inductive datatype declaration validation bug pointed out by Cody Roux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 16:29:25 -07:00
Leonardo de Moura
b9d7f8e867 test(lua): make sure bug reported by Floris does not happen in Lean 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 13:34:04 -07:00
Leonardo de Moura
203a59b682 test(lua): add more tests for the environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 12:36:04 -07:00
Leonardo de Moura
9f4bae6856 feat(library/kernel_bindings): add hott_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:49:30 -07:00
Leonardo de Moura
4d1fecb21d refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:24:24 -07:00
Leonardo de Moura
f08a852da8 feat(library/kernel_bindings): expose environment::add(declaration) method in the Lua API, and add example to demonstrate its usage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:12:55 -07:00
Leonardo de Moura
3726688711 test(lua): add test to demonstrate the different between list(A) where A is a parameter, and where A is an index 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 12:17:16 -07:00
Leonardo de Moura
11fc917102 test(lua): add tests for improving kernel_bindings coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 12:16:12 -07:00
Leonardo de Moura
c5e8c10c9d fix(library/normalize): bug in normalize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 11:53:58 -07:00
Leonardo de Moura
fae07771ec test(lua): add more universe level expression tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 11:41:17 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration 
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:41:38 -07:00
Leonardo de Moura
00b1a84051 feat(library/kernel_bindings): expose environment::for_each method in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:16:19 -07:00
Leonardo de Moura
9e55c8766f test(lua): add normalize and type_check tests for terms containing metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:56:27 -07:00
Leonardo de Moura
ddccca529a test(lua): add test for mutually recursive inductive type recursor/eliminator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:41:50 -07:00
Leonardo de Moura
eb6807e1d3 test(lua): add another add_inductive example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:48:35 -07:00
Leonardo de Moura
4f15240a71 test(lua): add tests for new Pi/Fun notation in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:17:15 -07:00
Leonardo de Moura
a72be5eea4 test(lua): add example suggested by Cody 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:06:19 -07:00
Leonardo de Moura
3e3d3c8380 feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:44:15 -07:00
Leonardo de Moura
a7aacaa782 feat(library/kernel_bindings): improve list_level support in the Lua interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:18:48 -07:00
Leonardo de Moura
48b436c1c8 test(lua): add Martin-lof identity type test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 13:42:49 -07:00
Leonardo de Moura
f3ed20a229 feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 12:52:25 -07:00
Leonardo de Moura
2aacb769dd feat(kernel/inductive): generate computational rules RHS for inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:08:19 -07:00
Leonardo de Moura
28b70b4e04 feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 15:39:48 -07:00
Leonardo de Moura
45252e2229 feat(kernel/inductive): add eliminator/recursor for inductive datatype declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 14:17:57 -07:00
Leonardo de Moura
f53254b389 test(lua): fix n6.lua, and add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:52:16 -07:00
Leonardo de Moura
405b24861c feat(util/name): add methods append_after and append_before 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:49:24 -07:00
Leonardo de Moura
fcf94ad7c2 test(lua): add test for inductive datatype positivity check 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 20:12:55 -07:00
Leonardo de Moura
950d69b977 test(lua): add tests for exercising datatype validation code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 20:10:45 -07:00
Leonardo de Moura
b5d07bec2e test(lua): add some comments to inductive datatype test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:30:43 -07:00
Leonardo de Moura
8fcb84c8f2 feat(kernel/inductive): finish inductive datatype declaration validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:32 -07:00
Leonardo de Moura
d03e35aaac feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:59:06 -07:00
Leonardo de Moura
53e02a902c test(lua): add is_geq (for universe level) tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:42:12 -07:00
Leonardo de Moura
a85a6b685b feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 12:30:03 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:37:27 -07:00
Leonardo de Moura
3a0861bca7 test(lean): remove old test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:42:10 -07:00
Leonardo de Moura
9f06cd553e test(lean): remove tests using Lean old syntax and kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:38:53 -07:00
Leonardo de Moura
989bcdc7ad test(lua): add inductive datatype simple tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 09:25:03 -07:00
Leonardo de Moura
4ec89e8561 feat(library/kernel_bindings): add sugar for level expressions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 08:10:36 -07:00
Leonardo de Moura
755fac8114 test(lua): add test simulating HoTT compatible environment 
Type.{0} is predicative
   Type.{0} is proof relevant
   Id       is proof irrelevant
   Path     is proof relevant

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:32:01 -07:00
Leonardo de Moura
69e72c278d feat(kernel): add proof irrelevance for classes 
We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:30:32 -07:00
Leonardo de Moura
193aa4a83f feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 14:09:00 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:28:05 -07:00
Leonardo de Moura
924b2344af fix(lua/res1): make sure the test works with Lua 5.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 14:47:42 -07:00
Leonardo de Moura
da31e60b02 test(lua): add more tests for type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 14:17:58 -07:00
Leonardo de Moura
90c4957071 test(lua): add tests for resolve macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
7c0cc3111a fix(kernel/type_checker): we must use different caches for infer_type and check 
The new test tc4.lua exposes the problem being fixed.
We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
6e78256b87 feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:24:49 -07:00
Leonardo de Moura
606e6226c2 fix(kernel/type_checker): the type checker cache was not taking into account binder information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:14:57 -07:00
Leonardo de Moura
2e1a0bd50c feat(kernel/expr): add is_contextual binder info 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:54:27 -07:00
Leonardo de Moura
52d682b832 test(lua): unit tests for let expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:29:44 -07:00
Leonardo de Moura
e57b943adf test(lua): add constraint generation test when type checking with metavars 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 11:06:48 -07:00
Leonardo de Moura
eea561c74b test(lua): add more expr API unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 09:20:25 -07:00
Leonardo de Moura
cfa9520655 test(lua): add more level API unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 09:20:10 -07:00
Leonardo de Moura
9ed700a5a6 feat(kernel/environment): add forget method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 08:40:46 -07:00
Leonardo de Moura
7b15e558a2 refactor(kernel/converter): implement eta in whnf instead of is_def_eq. 
Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
     (fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
     (fun x : Type.{1}, f x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 17:49:53 -07:00
Leonardo de Moura
c883c638d6 feat(library/kernel_bindings): expose expression tags in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:50:43 -07:00
Leonardo de Moura
20947de2f1 test(lua): add replace method test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 15:51:22 -07:00
Leonardo de Moura
9f86aa73c8 test(lua): add basic universe level tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:51:18 -07:00
Leonardo de Moura
ff9004dae2 refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-11 18:05:02 -07:00
Leonardo de Moura
9d96f24766 refactor(kernel): remove convertability constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:25:27 -07:00
Leonardo de Moura
7b6d555433 refactor(kernel): remove level constraints from definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:11:50 -07:00
Leonardo de Moura
a650a4f9b5 fix(library/kernel_bindings): bug in mk_app, add expr_lt tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:54:52 -07:00
Leonardo de Moura
21e3e22017 test(lua/threads): re-activate Lua thread examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:52:15 -07:00
Leonardo de Moura
129d108d0b test(lua): add example for testing is_descendant 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:50:24 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:08:32 -07:00
Leonardo de Moura
5a7f181efc feat(util/name_set): improve name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:17:00 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 19:04:15 -07:00
Leonardo de Moura
1a8d75c4f0 feat(util): name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 18:32:53 -07:00
Leonardo de Moura
7fe61bc69c feat(util): name_generator Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:28:11 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:45 -07:00
Leonardo de Moura
8ae0e46e9d feat(library/kernel_bindings): add new global level methods to environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:17:04 -07:00
Leonardo de Moura
9bf83390dc test(lua): add definition API tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:01:22 -07:00
Leonardo de Moura
dc627c9965 test(lua): add constraint API tests, and fix minor bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:46 -07:00
Leonardo de Moura
7b4b862faa test(lua): add justification API tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:16:24 -07:00
Leonardo de Moura
340c0e0945 feat(library/kernel_bindings): substitution Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:30:30 -07:00
Leonardo de Moura
305815cb56 feat(library/kernel_bindings): expose expr_binder_info in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 11:23:37 -07:00
Leonardo de Moura
97e7e4e762 test(lua): remove obsolete test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 17:08:50 -07:00
Leonardo de Moura
fd034521dc feat(library/kernel_bindings): cleanup level Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 17:05:25 -07:00
Leonardo de Moura
93a61748e9 fix(kernel/level): bug in optional<level>() constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 17:00:57 -07:00
Leonardo de Moura
984048f40d feat(library/kernel_bindings): new level Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 15:08:58 -07:00
Leonardo de Moura
a6116e3156 test(lua): reactivate some of the Lua unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 10:36:57 -07:00
Leonardo de Moura
e9dada5e14 refactor(builtin/kernel): use standard definition for 'or' and 'and' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-17 12:05:34 -08:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:43:01 -08:00
Leonardo de Moura
368fcb5ff9 refactor(builtin/kernel): rename refute to by_contradiction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 08:49:19 -08:00
Leonardo de Moura
b7b868de85 fix(library/elaborator): bug reported by Jeremy Avigad 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 14:01:22 -08:00
Leonardo de Moura
a2d2e36f04 refactor(frontends/lean): remove notation for creating tuples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 09:03:42 -08:00
Leonardo de Moura
4317f67bd2 fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 18:57:33 -08:00
Leonardo de Moura
c45c1748d8 refactor(builtin/kernel): reorder congr1 arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 16:15:44 -08:00
Leonardo de Moura
8df7c7b02d feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker 
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 11:31:24 -08:00
Leonardo de Moura
1ec01f5757 refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 16:04:44 -08:00
Leonardo de Moura
ad7b13104f feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 15:03:16 -08:00
Leonardo de Moura
d4b08fcf96 feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator 
Unification constraints of the form

         ctx |- ?m[inst:i v] == T

         and

         ctx |- (?m a1 ... an) == T

are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.

The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 21:08:00 -08:00
Leonardo de Moura
593f1f2ebd fix(frontends/lean): allow user set constants defined in other namespaces as opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
363c4dc5c2 feat(library/elaborator): improve support for dependent pairs in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
ea06bb2885 feat(frontends/lean/pp): change how lift local entries are pretty printed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
a51139e63b feat(frontends/lean): position information in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
e4579b93e4 fix(library/elaborator): try first projection before imitation in the higher-order unifier 
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 13:35:05 -08:00
Leonardo de Moura
ef321e730f feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 12:47:23 -08:00
Leonardo de Moura
eab0456b27 test(tests/lean): test super opaque style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 11:33:27 -08:00
Leonardo de Moura
fdc4c9b53c test(tests/lean): add nested 'have' expression test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 08:13:04 -08:00
Leonardo de Moura
1d23d93e60 feat(frontends/lean): new 'have' expression 
Add 'have' notation suggested by Jeremy Avigad.
Add his example to the test suite.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 08:03:59 -08:00
Leonardo de Moura
ba9a8f9d98 feat(frontends/lean): add 'show' expression syntax sugar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 07:50:22 -08:00
Leonardo de Moura
419fb7464e fix(tests/lean): adjust tests to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-05 21:04:06 -08:00
Leonardo de Moura
aec9c84d0d fix(util/lua): deadlock 
Errors in the Lua library produce longjmps.
The longjmp will not unwind the C++ stack.
In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 15:16:29 -08:00
Leonardo de Moura
f4ec874c6e refactor(builtin): remove dead module heq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:42:28 -08:00
Leonardo de Moura
0283887ee9 refactor(builtin/kernel): move the heq axioms into kernel.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:17:34 -08:00
Leonardo de Moura
f03c09c10b feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 13:53:30 -08:00
Leonardo de Moura
413391b2b4 chore(tests/lean/sig2): remove unnecessary parenthesis from test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:37:08 -08:00
Leonardo de Moura
c9b72df34b fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:36:26 -08:00
Leonardo de Moura
96c9c7505a test(tests/lean): add another sigma-type test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 10:12:39 -08:00
Leonardo de Moura
9dc86e3cf5 fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 10:06:29 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 22:10:01 -08:00
Leonardo de Moura
cc96b50644 feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 20:53:11 -08:00
Leonardo de Moura
5c991f8fbf feat(frontends/lean): parse and pretty print tuples/pairs 
This commit also fixes a bug in the type checker when processing dependent pairs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 20:10:30 -08:00
Leonardo de Moura
640ebcc040 test(tests/lean/exp): add example for Steve 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 11:35:40 -08:00
Leonardo de Moura
e4afa3dc43 fix(tests/lean/map): incorrect output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 00:05:19 -08:00
Leonardo de Moura
87f9c9b27e fix(tests/lean/map): make sure the unit test produce the same result in different platforms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 20:29:34 -08:00
Leonardo de Moura
e2add5c9f2 test(tests/lean): add heterogeneous equality simplification example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 20:27:39 -08:00
Leonardo de Moura
6be50f0133 refactor(builtin/heq): merge cast and heq modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 15:01:48 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 14:48:27 -08:00
Leonardo de Moura
2b7bc7b673 test(tests/lean/exp): simulating HOL constructions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 17:59:57 -08:00
Leonardo de Moura
e3dc552c39 fix(library/simplifier): nontermination 
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:55:21 -08:00
Leonardo de Moura
1d85267d26 fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:38:22 -08:00
Leonardo de Moura
110ca84984 feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 13:49:24 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 19:28:42 -08:00
Leonardo de Moura
b45ab9dc30 feat(library/elaborator): use equality constraints instead of convertability constraints on definitions 
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 14:13:21 -08:00
Leonardo de Moura
8c1f6b9055 fix(kernel/typechecker): allow elaborator to infer (Type U+1) 
In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 14:00:01 -08:00
Leonardo de Moura
41f5e2a067 feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 18:32:40 -08:00
Leonardo de Moura
01259b1e84 feat(kernel): make sure U is the maximal universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 16:31:00 -08:00
Leonardo de Moura
ea6bf224e5 feat(frontends/lean): make the parser accept (Type -> ...) 
Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 15:23:20 -08:00
Leonardo de Moura
4f3127d3d5 fix(library/simplifier): check if the given types are convertible to ceq expected types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 15:15:55 -08:00
Leonardo de Moura
0bb8fe75b3 test(tests/lean): new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 14:21:18 -08:00
Leonardo de Moura
a19f9d4846 feat(library/simplifier): discard conditional equations that are clearly non-terminating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:56:45 -08:00
Leonardo de Moura
dd6aae378f fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:29:20 -08:00
Leonardo de Moura
4dc3aa46c3 feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:02:12 -08:00
Leonardo de Moura
069e5edf6b fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:01:01 -08:00
Leonardo de Moura
62408a6adc test(tests/lean): move simp_loop test to slow subdirectory 
This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 10:32:48 -08:00
Leonardo de Moura
92ba4e8b2d feat(library/simplifier): add support for metavariables in conditional rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 08:34:04 -08:00
Leonardo de Moura
ee4344076e feat(library/simplifier): improve error message when simplifier is looping 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 19:36:31 -08:00
Leonardo de Moura
72c607846a test(tests/lean): add Jeremy's proof to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 16:05:46 -08:00
Leonardo de Moura
7f53cb9601 feat(frontends/lean/parser): add_rewrite take the 'using' command into account 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 01:15:28 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with = 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:21:05 -08:00
Leonardo de Moura
db45d02078 fix(tests/lean): test discrepancy on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:31:35 -08:00
Leonardo de Moura
7b88d68afb test(tests/lean): add test using simplifier monitor for tracking failures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:11:16 -08:00
Leonardo de Moura
8bccfb947a feat(library/simplifier): expose simplier and simplifier_monitor objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:02:05 -08:00
Leonardo de Moura
b26035fcf6 feat(kernel/type_checker): improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 09:45:17 -08:00
Leonardo de Moura
4d25cb7f47 feat(library/tactic): add simplify_tactic based on the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 18:53:18 -08:00
Leonardo de Moura
844572c382 feat(library/simplifier): support for dependent simplification in Pi/forall expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 00:32:05 -08:00
Leonardo de Moura
e8bba1ebf3 fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f 
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 20:34:28 -08:00
Leonardo de Moura
9fb3ccb4c0 feat(library/simplifier): support for dependent simplification in lambda expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 16:54:42 -08:00
Leonardo de Moura
5b13ef1b90 test(tests/lean): new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:56:49 -08:00
Leonardo de Moura
7015089734 fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:49:44 -08:00
Leonardo de Moura
7a4eb4b8ed feat(library/simplifier): contextual simplification for A -> B 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 22:32:55 -08:00
Leonardo de Moura
c2381e43f1 fix(library/simplifier): bug in cast elimination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 21:25:09 -08:00
Leonardo de Moura
35ad156a46 fix(tests/lean): make sure pretty print and parse test passes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:23:55 -08:00
Leonardo de Moura
8f455f5965 fix(frontends/lean): bug in scope construct 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:23:29 -08:00
Leonardo de Moura
7f3e2b3ef4 fix(frontends/lean/parser): bug in 'using' construct 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
8e0888828d fix(library/simplifier): missing check in mk_hcongr_th 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
1a3660180e test(tests/lean): add new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
26bea77721 fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
dbc100cc2e feat(library/simplifier): cast elimination in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 17:28:14 -08:00
Leonardo de Moura
cd87cb3de4 test(tests/lean): add test for congruence theorem that uses an argument before simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 13:26:09 -08:00
Leonardo de Moura
180be5c4a2 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 13:11:58 -08:00
Leonardo de Moura
5ba2525eab test(tests/lean): add test disabling contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:57:05 -08:00
Leonardo de Moura
33193e1ab3 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:54:29 -08:00
Leonardo de Moura
d6692264e8 feat(library/simplifier): contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:23:22 -08:00
Leonardo de Moura
1638a7bb02 fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 21:44:24 -08:00
Leonardo de Moura
17cce340f6 fix(library/elaborator): in optimization for metavariable free terms 
The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 18:06:00 -08:00
Leonardo de Moura
8214c7add4 feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer 
Before this commit, the elaborator was solving constraints of the form

       ctx |- (?m x) == (f x)
as
       ?m <- (fun x : A, f x)    where A is the domain of f.

In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is

       ?m  <- f

Depending of the circumstances we want  ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
       ?m <- (fun x : A, f x)

When we are elaborating the axiom_of_choice theorem, we need to use the second one:
       ?m <- f

Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.

This commit addresses this issue by creating a case-split
       ?m <- (fun x : A, f x)
       OR
       ?m <- f

Another solution is to implement eta-expanded normal forms in the Kernel.

With this change, we were able to cleanup the following "hacks" in kernel.lean:
     @eps_ax A (nonempty_ex_intro H) P w Hw
     @axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments

This commit also improves the imitation step for Pi-terms that are actually arrows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 13:28:54 -08:00
Leonardo de Moura
331b5846c6 test(library/simplifier): add test for the single_pass option in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 13:47:54 -08:00
Leonardo de Moura
ead54bbf57 feat(library/simplifier): enforce max_steps option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 12:12:17 -08:00
Leonardo de Moura
1ccfac5873 feat(library/simplifier): conditional rewriting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 21:15:46 -08:00
Leonardo de Moura
1ef75a9ba6 test(tests/lua): add test/example that demonstrates how to collect statistics of used theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 18:04:22 -08:00
Leonardo de Moura
6bcd8e3ee5 fix(library/expr_lt): use expression depth instead of size to obtain a monotonic total order on terms 
It is not incorrect to use size, but it can easily overflow due to sharing.
The following script demonstrates the problem:

local f = Const("f")
local a = Const("a")
function mk_shared(d)
   if d == 0 then
      return a
   else
      local c = mk_shared(d-1)
      return f(c, c)
   end
end
print(mk_shared(33):size())

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 17:40:49 -08:00
Leonardo de Moura
cd19d4da01 feat(library/simplifier): memoize intermediate results 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 17:03:44 -08:00
Leonardo de Moura
97ead50a3e feat(builtin/Nat): flip orientation of associativity axioms for + and * 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 15:38:00 -08:00
Leonardo de Moura
d1bd56b3d3 fix(tests/lean): adjust test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 14:47:03 -08:00
Leonardo de Moura
ad219d43d9 refactor(*): semantic attachment parsing and simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 14:44:45 -08:00
Leonardo de Moura
ac9f8f340d feat(kernel/expr): add efficient get_size() function for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 12:28:37 -08:00
Leonardo de Moura
5224df56a3 test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 08:36:48 -08:00
Leonardo de Moura
913d893204 feat(library/simplifier): add support for 'permutation' rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 08:29:31 -08:00
Leonardo de Moura
69d7ee316f feat(library/simplifier): improve simplification by evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 23:26:34 -08:00
Leonardo de Moura
bcede6925f fix(tests/lean): add expected result file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 16:31:35 -08:00
Leonardo de Moura
19f3c281c3 test(tests/lean): matrix multiplication example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 16:29:32 -08:00
Leonardo de Moura
999984e701 fix(tests/lean): remove unnecessary theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 12:55:33 -08:00
Leonardo de Moura
cc11b9e125 test(tests/lean): rewriting proof example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 12:53:21 -08:00
Leonardo de Moura
d322f63113 feat(frontends/lea): add commands for creating and managing rewrite rule sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 12:03:59 -08:00
Leonardo de Moura
bbf6e6a256 feat(builtin/kernel): create default rule set in the kernel, and adjust unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 11:24:20 -08:00
Leonardo de Moura
7492fd5a2c feat(library/simplifier): add support for simplification by evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 10:34:55 -08:00
Leonardo de Moura
11719713ec feat(library/hop_match): optionally unfold constants when performing higher order matching 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 10:32:06 -08:00
Leonardo de Moura
39c3b17eb7 feat(library/simplifier): add support for Eta-reduction in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 00:40:35 -08:00
Leonardo de Moura
ed009f4c88 feat(kernel/simplifier): add support for Beta-reduction in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 00:40:20 -08:00
Leonardo de Moura
7a3aab60c6 chore(builtin/kernel): remove \bowtie as notation for transitivity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 21:11:12 -08:00
Leonardo de Moura
32c5bc25e3 refactor(library/simplifier): cleanup rewrite_rule_set, and use it in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 20:52:33 -08:00
Leonardo de Moura
feea96e84d feat(library/simplifier): add rewrite_rule_set extension for managing rewrite rules in an environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 15:43:24 -08:00
Leonardo de Moura
40b7ed13c2 fix(tests/lean): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 19:27:32 -08:00
Leonardo de Moura
fc4c6454a7 chore(tests/lean): adjust tests to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 14:36:55 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 17:39:12 -08:00
Leonardo de Moura
5453a8f2f1 test(tests/lua): hop_match experiment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 00:15:31 -08:00
Leonardo de Moura
3238c7e2a0 feat(library/simplifier): add is_permutation_ceq predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 19:53:52 -08:00
Leonardo de Moura
2368c936d3 test(tests/lua): exercise fields method for semantic attachments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:24:18 -08:00
Leonardo de Moura
57e58c598c fix(tests/lean): adjust tests to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:35:33 -08:00
Leonardo de Moura
c73398a0b8 refactor(library/simplifier): relax rule for conditional equalities 
The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:06:00 -08:00
Leonardo de Moura
3daac17ea8 feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 15:30:16 -08:00
Leonardo de Moura
f67b5c4d00 test(tests/lua): more to_ceqs tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 13:50:35 -08:00
Leonardo de Moura
c651d3ea2d feat(library/simplifier): filter out propositions that cannot be used as conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 12:06:27 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool 
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 11:02:52 -08:00
Leonardo de Moura
91e1f9fc02 fix(tests/lean): adjust test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 10:20:35 -08:00
Leonardo de Moura
3ab2d2a441 fix(frontends/lean/parser): memory leak due to g++ bug 
g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html

This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 10:15:04 -08:00
Leonardo de Moura
97d9765992 fix(tests/lua/threads): increase timeout to make sure it passes the test on slow machines 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 08:46:14 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:41:40 -08:00
Leonardo de Moura
8217a544cc fix(library/hop_match): bugs in the higher-order matching procedure, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:37:28 -08:00
Leonardo de Moura
485ca842c9 test(tests/lua): extra tests for Lua hierachical name API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 11:38:10 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3 feat(frontends/lean): improve error message for expressions containing unsolved metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 13:21:44 -08:00
Leonardo de Moura
12451e4a35 feat(frontends/lean/pp): display implicit arguments when expression contains metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 12:42:05 -08:00
Leonardo de Moura
84f017f127 chore(tests/lua): use default environment instead of creating a new one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:24:04 -08:00
Leonardo de Moura
35bacf95fc feat(shell): provide the default environment when parsing Lua files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:21:14 -08:00
Leonardo de Moura
7f818ecd92 feat(library): match procedure for higher-order patterns 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:45:24 -08:00
Leonardo de Moura
b85b45b40f test(tests/lean): When and Cond tactical tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 20:43:39 -08:00
Leonardo de Moura
65bdb9c7e0 fix(frontends/lean): unprotected call to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 19:56:20 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 18:09:53 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 15:31:58 -08:00
Leonardo de Moura
2179e57db3 refactor(builtin): move if_then_else to its own module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 14:08:39 -08:00
Leonardo de Moura
52e11dbbee test(tests/lean): 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 12:21:14 -08:00
Leonardo de Moura
fdeb457a81 feat(kernel/pos_info_provider): add support for file names in pos_info_provider 
The idea is to include the file name when displaying justification objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 12:19:30 -08:00
Leonardo de Moura
84e211b81b fix(frontends/lean): missing ':' in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:01:27 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 08:33:52 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments 
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 19:10:30 -08:00
Leonardo de Moura
a4b3d6d6c8 refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 17:25:14 -08:00
Leonardo de Moura
a6e0dcc96c fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 16:19:11 -08:00
Leonardo de Moura
2b2aa228e3 refactor(builtin/kernel): start with small universes 
The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 12:35:00 -08:00
Leonardo de Moura
abf61be8f6 chore(library/tactic): remove imp_tac, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:57:04 -08:00
Leonardo de Moura
048151487e feat(kernel): use Pi as forall/implication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:38:39 -08:00
Leonardo de Moura
d12d0f036f feat(kernel/environment): universe variables now live in their own namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 15:57:36 -08:00
Leonardo de Moura
d29d23cade test(tests/lean): alias command error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 15:29:16 -08:00
Leonardo de Moura
9f4959fb64 test(tests/lean): kernel exception pp method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 15:19:52 -08:00
Leonardo de Moura
0363faeec8 fix(frontends/lean/scanner): assertion violation, and add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 15:12:34 -08:00
Leonardo de Moura
29db6accb8 test(tests/lean): new tests for exercising the environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 14:34:21 -08:00
Leonardo de Moura
0a20356a51 fix(kernel/environment): we should not add an universe contraint object to the set of object when an integer overflow occurs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 13:43:22 -08:00
Leonardo de Moura
17c4cce89c fix(library/elaborator): remove_detail procedure was keeping a lot of details when typeof_mvar_justification was being used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 13:24:46 -08:00
Leonardo de Moura
0f1737d62c fix(frontends/lean): more precise position information for infix operators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 13:19:26 -08:00
Leonardo de Moura
8f3c97ca98 test(tests/lean): standard induction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 10:18:31 -08:00
Leonardo de Moura
abb9b8af83 fix(frontends/lean): bug in pop::context command, and add new tests for the universe command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 17:14:07 -08:00
Leonardo de Moura
5fe8c32da9 feat(kernel): use new universe contraints in the environment, allow new constraints to be added 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 16:46:11 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:41:03 -08:00
Leonardo de Moura
7222a2d1a9 feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 21:39:31 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 13:06:36 -08:00
Leonardo de Moura
6569b07b7c feat(frontends/lean/parser): rename 'show' expression to 'have' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 11:25:58 -08:00
Leonardo de Moura
0b4bdceb10 feat(builtin/macros): rename 'For' macro to 'take' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 11:08:55 -08:00
Leonardo de Moura
9f08156a73 feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 11:03:35 -08:00
Leonardo de Moura
ce1213a020 feat(frontends/lean): use '(* ... *)' instead of '(** ... **)' for script code blocks 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 10:32:47 -08:00
Leonardo de Moura
028a9bd9bd feat(frontends/lean/scanner): use Lua style comments in Lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 08:53:27 -08:00
Leonardo de Moura
fbe0bccf51 chore(*): name convention, proof construnction functions/macros start with upper-case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 18:11:01 -08:00
Leonardo de Moura
9eb4dc4a81 feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend 
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.

3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 17:18:23 -08:00
Leonardo de Moura
502d9f47ac test(tests/lean): new test full of holes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 16:31:52 -08:00
Leonardo de Moura
9620b00e24 feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. 
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 16:08:38 -08:00
Leonardo de Moura
430b75f38f test(tests/lean): add version of the Nat library full of holes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 12:31:13 -08:00
Leonardo de Moura
e714bd7982 feat(frontends/lean): add syntax sugar for applying Subst in calculational proofs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 11:23:55 -08:00
Leonardo de Moura
111949b9be feat(frontends/lean): calculational proofs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 10:53:14 -08:00
Leonardo de Moura
b2a8f4118d feat(library/elaborator): process ho-match before normalizing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 14:46:19 -08:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:52:25 -08:00
Leonardo de Moura
d633622d90 feat(frontends/lean/parser): namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 12:28:18 -08:00
Leonardo de Moura
c423198a69 feat(builtin/kernel): add Not.*Elim theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 11:35:21 -08:00
Leonardo de Moura
a8bc9fb4e0 refactor(builtin/kernel): mark exists as opaque after proving key theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 11:00:32 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:02:41 -08:00
Leonardo de Moura
cd3bbb1ebf fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-31 10:14:17 -08:00
Leonardo de Moura
390a78a8d2 chore(frontends/lean/parser): remove 'Skipped' message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 15:35:12 -08:00
Leonardo de Moura
08718e33dc refactor(builtin): only load the kernel and natural numbers by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:35:37 -08:00
Leonardo de Moura
ecd62a1783 refactor(builtin/basic): rename basic.lean to kernel.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:46:03 -08:00
Leonardo de Moura
4401b390fe refactor(library/arith): do not load specialfn by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:25:43 -08:00
Leonardo de Moura
46a8300a2d refactor(library/arith): move real and special function declarations to .lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:02:22 -08:00
Leonardo de Moura
c3bc6afb12 refactor(library/arith): move int and nat declarations to .lean files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 10:32:14 -08:00
Leonardo de Moura
15621610e9 refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments 
This commit also fixes bugs in the Alias command.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 17:04:36 -08:00
Leonardo de Moura
a1a5fb101d feat(frontends/lean): add Alias command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 16:25:45 -08:00
Leonardo de Moura
dfe46b9d25 refactor(kernel/builtin): move definition and axioms to basic.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 14:01:30 -08:00
Leonardo de Moura
f8b82d854e feat(builtin/basic): add TypeM alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 13:03:32 -08:00
Leonardo de Moura
411ebbc3c1 refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file 
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>
 2013-12-29 03:04:49 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 19:20:04 -08:00
Leonardo de Moura
1fd81dd3a1 feat(frontends/lean/parser): disable verbose messages when importing files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 12:24:13 -08:00
Leonardo de Moura
44a31dd8fb feat(frontends/lean/parser): improve Import command 
- 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>
 2013-12-28 12:05:01 -08:00
Leonardo de Moura
8e86d6578c fix(tests/lean): adjust tests to reflect modifications in the pp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 18:38:45 -08:00
Leonardo de Moura
3f0279b88c refactor(frontends/lua): replace lean.lua.h with util.lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 19:49:26 -08:00
Leonardo de Moura
40eca048e0 feat(extra): replace parse_lean_tpl with improved parse_template, that is based on macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 19:28:02 -08:00
Leonardo de Moura
275f022d79 fix(tests/lean): ignore lines containing 'executing external script' in test scripts, these lines contain references to the path where Lean was built 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 18:41:01 -08:00
Leonardo de Moura
f1b97b18b4 refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 15:54:53 -08:00
Leonardo de Moura
ef18cc4a92 fix(frontends/lean/parser): add existing command macros when creating parser object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 13:38:14 -08:00
Leonardo de Moura
8e4560a866 feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 13:21:36 -08:00
Leonardo de Moura
ba02132a90 feat(frontends/lean/parser): add command macros 
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>
 2013-12-26 13:00:28 -08:00
Leonardo de Moura
480781d13e feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 11:15:45 -08:00
Leonardo de Moura
3673f2ac1d feat(frontends/lean/parser): add Find command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 18:31:52 -08:00
Leonardo de Moura
a3dde29f3c feat(frontends/lua/parser): allow users to specify the precedence of macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 12:27:56 -08:00
Leonardo de Moura
88235d2922 feat(library/tactic/apply_tactic): try other solutions produced by the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 11:51:27 -08:00
Leonardo de Moura
8e45064f25 feat(library/tactic/apply_tactic): improved parametric apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 22:40:34 -08:00
Leonardo de Moura
c87e965f86 fix(tests/lean/tactic14.lean): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 21:36:49 -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
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
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
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
2c30b87f30 test(tests/lean): ExistsElim test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 12:57:25 -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
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
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
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
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
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
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
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
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
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
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
42cb5d1d3c fix(tests/lean): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 20:11:49 -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
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
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
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
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
5b29fd8d93 test(tests/lean): add ExistsElim test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:43:09 -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
2972fb9d8c test(tests/lean): new elaborator tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 22:00:26 -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
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
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
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
6b1b6c7bd1 feat(tests/lean): include standard error in the expected output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:52:57 -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
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
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
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
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
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
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
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
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
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
a75d05fdb4 fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 17:03:12 -08:00
Leonardo de Moura
daadff548e fix(tests/lean): update expected result to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:31:13 -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
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
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
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
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
74a8b5f2f4 test(tests/lean/interactive): add back command test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 17:19:53 -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