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

770 commits

Author SHA1 Message Date
Leonardo de Moura
811f46e97b feat(frontends/lean/pp): add option for displaying internal names associated with private declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:03:54 -07:00
Leonardo de Moura
0c668a31fe fix(frontends/lean/pp): display private 'internal' names in a human readable way 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 10:58:13 -07:00
Leonardo de Moura
a59eec39b8 feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:44:40 -07:00
Leonardo de Moura
022a151cf7 feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:33:31 -07:00
Leonardo de Moura
736b219e65 fix(frontends/lean/elaborator): pretty print placeholders as '_' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:46:03 -07:00
Leonardo de Moura
e7c7d5718a fix(frontends/lean/pp): fix bug in the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:30:30 -07:00
Leonardo de Moura
15c1e39f88 feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:43:40 -07:00
Leonardo de Moura
13fe28dd1c perf(library/unifier): delay the instantiation of metavariables occurring in the types of local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 14:31:30 -07:00
Leonardo de Moura
61661478ad refactor(kernel/metavar): simplify substitution class, and remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 10:03:03 -07:00
Leonardo de Moura
90189f8eb6 chore(frontends/lean/elaborator): fix outdated comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 17:50:13 -07:00
Leonardo de Moura
35e7302d8a perf(frontends/lean/elaborator): fix performance bottleneck 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 17:45:45 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:43:18 -07:00
Leonardo de Moura
ad87c0b3e1 fix(frontends/lean): race condition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-21 09:32:13 -07:00
Leonardo de Moura
9ef4d44a86 chore(frontends/lean): add 'replace' auxiliary funcs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-20 01:10:49 +01:00
Leonardo de Moura
e39a6e732a refactor(kernel/error_msgs): move pp_type_mismatch to error_msgs module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-20 00:19:31 +01:00
Leonardo de Moura
d69db172a1 chore(kernel/replace_fn): add syntax sugar for replace function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-19 12:53:37 +01:00
Leonardo de Moura
6b60db7b93 fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-19 09:55:34 +01:00
Leonardo de Moura
66ba3c8a0b fix(frontends/lean/elaborator): bug in the elaborator reported by Jeremy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-18 23:48:27 +01:00
Leonardo de Moura
661e681ac9 feat(frontends/lean/decl_cmds): allow parameters with different types to be declared using the same 'parameters' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-17 20:47:33 +01:00
Leonardo de Moura
0f44e3c9f4 fix(frontends/lean): calc configuration commands, add check_constant_next auxiliary method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-15 01:19:47 +01:00
Leonardo de Moura
7ed373811d perf(frontends/lean/elaborator): improve visit_binding performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 17:08:32 +01:00
Leonardo de Moura
91e8f0b8fa chore(frontends/lean/elaborator): replace ... withe exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 16:37:55 +01:00
Leonardo de Moura
2e6184a721 fix(frontends/lean): more bugs in section management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 06:27:36 +01:00
Leonardo de Moura
b53e6eda58 refactor(frontends/lean): eliminate the abstract method 'family' from parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 05:44:06 +01:00
Leonardo de Moura
8167ad329f fix(frontends/lean): bug in section management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 05:04:01 +01:00
Leonardo de Moura
195429611b refactor(frontends/lean/builtin_cmds): cleanup 'check' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 04:25:53 +01:00
Leonardo de Moura
5c51be4585 refactor(frontends/lean): use expr_struct_set when collecting locals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 04:12:58 +01:00
Leonardo de Moura
6c442b250c refactor(frontends/lean): minor code reorg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 03:47:49 +01:00
Leonardo de Moura
43fa75f7a9 fix(frontends/lean/decl_cmds): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 03:36:06 +01:00
Leonardo de Moura
fab7934265 refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 02:53:02 +01:00
Leonardo de Moura
bdfd219246 feat(frontends/lean): improve error message for placeholder that can't be synthesized 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 22:35:57 +01:00
Leonardo de Moura
943092eaf0 refactor(frontends/lean/elaborator): reorg class elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 14:50:52 +01:00
Leonardo de Moura
c03ae24d22 fix(frontends/lean/elaborator): option name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 14:03:47 +01:00
Leonardo de Moura
1d16b5d2ad fix(frontends/lean/elaborator): propagate tags for getting better error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 11:10:26 +01:00
Leonardo de Moura
8da44f1cd5 feat(frontends/lean/parser): disable quasie-hash consing in new threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 04:11:17 +01:00
Leonardo de Moura
a31457efde fix(frontends/lean/parser): copy rec and initial fields when processing Exprs and ScopedExpr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 01:24:55 +01:00
Leonardo de Moura
7ccb9a389c feat(frontends/lean): process theorems in parallel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 22:50:57 +01:00
Leonardo de Moura
cb93d194ed perf(frontends/lean/elaborator): improve performance of pi_abstract_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 17:49:14 +01:00
Leonardo de Moura
03bbec08e5 perf(frontends/lean/elaborator): replace abstract with abstract_local 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 09:54:22 +01:00
Leonardo de Moura
1d273fcfdd chore(frontends/lean): rename 'obtains' to 'obtain' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 06:35:24 +01:00
Leonardo de Moura
024299f56b fix(frontends/lean): name of auxiliary hypothesis in 'obtains' expression, and also marked them as non-contextual 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-11 04:50:53 +01:00
Leonardo de Moura
cf34f75ab5 feat(frontends/lean): add 'obtains' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-11 04:08:51 +01:00
Leonardo de Moura
9a3227344e fix(library/tactic): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 23:23:48 +01:00
Leonardo de Moura
b62abf0f06 refactor(library/tactic/goal): remove redundance, goal pp method was duplicating some of the functionality provided by the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 18:59:03 +01:00
Leonardo de Moura
405e57eb2d refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 18:32:00 +01:00
Leonardo de Moura
c13c75b93e feat(frontends/lean/pp): add option for displaying fully qualified names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 15:55:19 +01:00
Leonardo de Moura
49bc3fffbd fix(frontends/lean/pp): purify procedure for local names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 14:13:51 +01:00
Leonardo de Moura
fc8ddcb0ce feat(frontends/lean): improve 'check' command when used inside sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 14:07:41 +01:00
Leonardo de Moura
1a6d0784f2 feat(kernel/level): improve universe level normalization procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:49:41 +01:00
Leonardo de Moura
313c7066e7 feat(frontends/lean): add Type' as notation for Type.{_+1} 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:28:36 +01:00
Leonardo de Moura
d9b2801eeb feat(frontends/lean): use the same universe in declarations such as (A B : Type) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:18:52 +01:00
Leonardo de Moura
0ec6fa02de feat(frontends/lean/pp_options): remove the 'lean.' prefix 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 19:19:35 -07:00
Leonardo de Moura
aff766430d fix(frontends/lean/pp): universe pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 19:17:28 -07:00
Leonardo de Moura
43eba857cb feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 18:47:10 -07:00
Leonardo de Moura
d31cde473e fix(util/sexpr): nested Lua objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 11:13:17 -07:00
Leonardo de Moura
2ef7b9be2f feat(frontends/lean): add basic pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 01:12:36 -07:00
Leonardo de Moura
4505016154 feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
5e836092cc feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
a3be63af73 feat(frontends/lean): add tactic_hint command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
2fa2589220 feat(frontends/lean): add pretty printer configuration options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
da4c1922e3 feat(frontends/lean): add '_root_' prefix for referencing names in the root namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 19:15:46 -07:00
Leonardo de Moura
b43fb7448c feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 19:00:06 -07:00
Leonardo de Moura
e6d4c01b88 feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 18:17:10 -07:00
Leonardo de Moura
bd1873f6b1 feat(frontends/lean): add coercion modifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 17:48:20 -07:00
Leonardo de Moura
08465f049a feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 16:09:30 -07:00
Leonardo de Moura
112353861c feat(frontends/lean): rename command 'reset_proof_qed' to 'set_proof_qed' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 15:48:16 -07:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior 
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 15:40:55 -07:00
Leonardo de Moura
b9d08ff28c feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 14:53:06 -07:00
Leonardo de Moura
10b0dfeb37 feat(frontends/lean/class): allow many instances to provided with a single 'instance' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 14:41:14 -07:00
Leonardo de Moura
b956ce68d2 feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 12:50:43 -07:00
Leonardo de Moura
831de22bcd fix(frontends/lean): bugs in notation management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 09:31:42 -07:00
Leonardo de Moura
e8bd267a00 fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 21:54:16 -07:00
Leonardo de Moura
67363c893e chore(frontends/lean/elaborator): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 21:41:19 -07:00
Leonardo de Moura
9a13bef4f3 fix(frontends/lean): fix (and simplify) parameter universe inference 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 16:56:54 -07:00
Leonardo de Moura
b3de4bb061 fix(frontends/lean/decl_cmds): modifiers should be after universe parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 21:49:32 -07:00
Leonardo de Moura
55894f01e3 feat(frontends/lean): add 'opaque_hint' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 18:58:20 -07:00
Leonardo de Moura
32a605e793 fix(frontends/lean/builtin_cmds): allow 'check' command to unfold the current module opaque definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 17:39:49 -07:00
Leonardo de Moura
ab929d7201 refactor(library/unifier): store the unifier_plugin in the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 10:25:58 -07:00
Leonardo de Moura
a52c9f4e2b feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 09:43:16 -07:00
Leonardo de Moura
4af474010a fix(frontends/lean/elaborator): unintended use of local instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:49:05 -07:00
Leonardo de Moura
99fb6431a6 fix(frontends/lean/elaborator): support for local instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:38:08 -07:00
Leonardo de Moura
6ea7bb3ea4 feat(frontends/lean/builtin_exprs): add 'including' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:37:09 -07:00
Leonardo de Moura
8ab0b5bee3 feat(frontends/lean/elaborator): use local declarations as class instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:18:25 -07:00
Leonardo de Moura
00e1a7db23 feat(frontends/lean/elaborator): add class instance elaboration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 15:45:50 -07:00
Leonardo de Moura
079672f6f9 feat(frontends/lean): add 'class' and 'instances' infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 14:28:09 -07:00
Leonardo de Moura
f1884ee5f9 chore(frontends/lean): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 13:22:32 -07:00
Leonardo de Moura
d7cb1952ae feat(kernel): simplify choice_fn, and make its interface closer to the unifier_plugin interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 12:47:33 -07:00
Leonardo de Moura
ce282a549a feat(frontends/lean): add 'prefix' notation declaration command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 21:37:56 -07:00
Leonardo de Moura
b5f63e78ca feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 17:23:29 -07:00
Leonardo de Moura
fa1857e6a9 fix(frontends/lean/notation_cmd): fix default, add 'prev' action 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 16:44:44 -07:00
Leonardo de Moura
e3ab0a1d10 feat(frontends/lean): improve error messages when users forget to import 'tactic' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 08:33:29 -07:00
Leonardo de Moura
a7d660f875 feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 20:45:10 -07:00
Leonardo de Moura
5527955ba8 feat(frontends/lean): add 'proof-qed' notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 19:30:48 -07:00
Leonardo de Moura
138267b53a feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 18:58:32 -07:00
Leonardo de Moura
04b2a620f8 fix(frontends/lean/elaborator): instantiate metavariables before displaying error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 18:07:11 -07:00
Leonardo de Moura
3809a3cc2c chore(frontends/lean): code cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 17:32:13 -07:00
Leonardo de Moura
181a739a5e feat(frontends/lean/elaborator): report unassigned metavariables as goals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 16:26:06 -07:00
Leonardo de Moura
6a6ebd5c2d refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 15:39:25 -07:00
Leonardo de Moura
d46ade94a7 refactor(frontends/lean): remove unnecessary code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 14:47:41 -07:00
Leonardo de Moura
ee531ec0e2 feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact] 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 14:09:01 -07:00
Leonardo de Moura
0f27856e4a feat(library/tactic): new apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 13:14:50 -07:00
Leonardo de Moura
e1d909455c refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 10:45:09 -07:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 10:00:55 -07:00
Leonardo de Moura
f464775af6 fix(frontends/lean/parser): bug when parsing identifiers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 08:36:25 -07:00
Leonardo de Moura
0198dfc7c5 feat(frontends/lean): parse numerals as expressions of type 'num.num' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 08:09:33 -07:00
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
7abe2e7242 fix(frontends/lean/token_table): precedence for '@' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 17:06:09 -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
ec3743dede fix(frontends/lean/parser): avoid nontermination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:46:58 -07:00
Leonardo de Moura
8cdf44b87b feat(frontends/lean/notation_cmd): allow 'max' to use as a precedence level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:46:32 -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
c84218e24a chore(frontends/lean/inductive_cmd): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 17:16:10 -07:00
Leonardo de Moura
3e299a1d5a refactor(frontends/lean/parser): move parser Lua bindings to a separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 17:00:10 -07:00
Leonardo de Moura
bccc3df1aa chore(frontends/lean): reduce code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 16:52:20 -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
ccdb96775f feat(frontends/lean/parser): allow 'assume'/'take'/'fun' as notation for apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 23:00:41 -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
6891f48c67 fix(library/module): do not store full path of imported modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 10:48:57 -07:00
Leonardo de Moura
1f0171cd57 fix(frontends/lean/dependencies): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:55:30 -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
ec18bd93f9 feat(frontends/lean): send tactic hint table to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 07:03:25 -07:00
Leonardo de Moura
65c63e146f feat(frontends/lean): add display_deps function, and --deps command line option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 18:35:18 -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
0e015974ca fix(library/unifier): bug in process_flex_rigid, also cleanup the code and break it into different cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 11:19:56 -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
cf9b486179 feat(frontends/lean): automatically import lua modules imported by imported lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 23:23:51 -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
e769121c2a fix(frontends/lean/elaborator): memory leaks that only occur when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 16:02:54 -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
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
0480dab986 feat(frontends/lean/parse_table): avoid duplicates in the parse table 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:19 -07:00
Leonardo de Moura
2d2f23cda6 feat(library/lean/lean): improve overload error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:52:40 -07:00
Leonardo de Moura
656bcd55ed fix(frontends/lean): save 'choice' position 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:50:44 -07:00
Leonardo de Moura
52ff29a6f7 feat(frontends/lean): add 'coercion' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:08:39 -07:00
Leonardo de Moura
06f9e7bfdd fix(build): add missing file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 18:12:23 -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
9f83ef8f6c chore(frontends/lean/elaborator): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:13:03 -07:00
Leonardo de Moura
543b1003a6 fix(frontends/lean/elaborator): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 13:11:35 -07:00
Leonardo de Moura
f2b41312fb feat(frontends/lean): add '@' explicit notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 12:50:47 -07:00
Leonardo de Moura
905209df1c fix(frontends/lean/elaborator): to cache values, we must push/pop whenever we update the m_ctx 
Thus, we are disabling the cache for now.
It is also unclear whether it is useful or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 11:05:14 -07:00
Leonardo de Moura
0791c83731 fix(frontends/lean/parser): add missing save_pos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 10:32:43 -07:00
Leonardo de Moura
6db6048bf8 feat(library/error_handling): pretty print unifier exceptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 09:41:25 -07:00
Leonardo de Moura
5b6589709c fix(frontends/lean/decl_cmds): allow binders but no type in definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 09:00:57 -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
fe0cee7536 feat(frontends/lean): add frontend elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 18:25:56 -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
61595f516c fix(frontends/lean/notation_cmd): initialization bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 16:20:28 -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
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
c7c5e41653 fix(frontends/lean/parser): warning when compiling in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:58:05 -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
16412daf39 feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
2cc8172d61 refactor(frontends/lean): remove m_pos field from parameter object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 23:06:49 -07:00
Leonardo de Moura
05d1832425 refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 22:33:58 -07:00
Leonardo de Moura
0cc8117fb4 fix(frontends/lean): add missing file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 06:10:15 -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
461689f758 refactor(frontends/lean/builtin_cmds): move declaration commands to new file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 15:55:52 -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
3ea24c0f32 fix(library/kernel_bindings): set_environment and set_io_state objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:36:47 -07:00
Leonardo de Moura
06002c5312 feat(frontends/lean/parser): use system_import when processing Lean import command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:09:42 -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
f17e8a853a feat(frontends/lean): allow parser actions to be implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 21:56:16 -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
037cfcf622 refactor(frontends/lean/notation_cmd): add register_notation_cmds procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 13:39:44 -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
ddba6b222a feat(frontends/lean): add calculational proof environment extension, it stores transitivity, reflexivity (and substitution) rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 13:13:13 -07:00
Leonardo de Moura
28c904abea feat(frontends/lean/parser): add 'flag' for disabling 'unknown identifier' errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 10:30:03 -07:00
Leonardo de Moura
4be05e1d8c refactor(frontends/lean): expose notation_entry and token_entry structures, and add functions for parsing notation without affecting the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 10:12:04 -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
82e79d9c78 fix(frontends/lean/parser): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 16:54:44 -07:00
Leonardo de Moura
a964ceb0e2 feat(frontends/lean): add 'import' command, add command line option for setting number of threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 16:37:46 -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
07f2379dec refactor(kernel): add mk_local function that has only two arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:27:26 -07:00
Leonardo de Moura
f1e3449aae fix(frontends/lean): propagate position information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 13:20:10 -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
775e10186d refactor(parser): use 'scope objects' for creating local scopes and setting m_type_use_placeholder flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 09:24:41 -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