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
|
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 |
|