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
|
614d8a768b
|
fix(library/unifier): flex_rigid case (?M ...) =?= (f ...), where f is not a constant nor a local
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 02:46:04 +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
|
585127ef66
|
fix(util/worker_queue): bug in join method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 23:25:43 +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
|
0a556c4a91
|
feat(util): add worker queue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 21:59:22 +01:00 |
|
Leonardo de Moura
|
6d95250d4b
|
fix(library/kernel_serializer): make sure temporary (internal) binder names do not leak into .olean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 20:23:38 +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
|
a38dc76b37
|
feat(kernel/metavar): add option to instantiate only expr metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 05:54:05 +01:00 |
|
Leonardo de Moura
|
80d1a6b993
|
perf(kernel/converter): do not cache easy cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 05:39:14 +01:00 |
|
Leonardo de Moura
|
391e5e2bc2
|
perf(library/unifier): use d_instantiate_metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 05:12:09 +01:00 |
|
Leonardo de Moura
|
9517f31a71
|
refactor(kernel/metavar): remove unnecessary functionality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 04:45:50 +01:00 |
|
Leonardo de Moura
|
50f76fd138
|
perf(library/unifier): improve m_mvar_occs management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 04:23:02 +01:00 |
|
Leonardo de Moura
|
c3e8e83e50
|
perf(library/unifier): simple optimization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-11 20:21:41 +01:00 |
|
Leonardo de Moura
|
1230e942aa
|
feat(library/unifier): handle 'first-order' flex-flex constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-11 04:51:28 +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
|
eeedb6fb18
|
fix(kernel/expr_eq_fn): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-10 23:21:24 +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
|
6af7e7f794
|
fix(kernel/expr_eq_fn): take local pp name into account when annotations are considered in the equality test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-10 18:56:50 +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
|
12d89ea0b9
|
fix(kernel/level): is_geq predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-10 13:18:41 +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
|
91b0dcad0f
|
fix(library/tactic): avoid 'unknown' message in trace_tac when position information is not available
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-08 17:48:41 -07:00 |
|