Leonardo de Moura
|
955d7d2659
|
fix(library/aliases): namespace and constant have the same name, and 'using' produces the 'empty' alias
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-07 08:32:21 -07:00 |
|
Leonardo de Moura
|
4ad7e709aa
|
feat(frontends/lean): default for inductive types, closes #32
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-07 07:52:37 -07:00 |
|
Leonardo de Moura
|
b56233cbe3
|
fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 23:15:05 -07:00 |
|
Leonardo de Moura
|
c6f3232f81
|
feat(frontends/lean): provide 'partial' type information even when there are type errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 21:56:57 -07:00 |
|
Leonardo de Moura
|
1cbf40a5d2
|
fix(frontends/lean): remove duplicate info entries, fix bug in save_overload
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 21:23:37 -07:00 |
|
Leonardo de Moura
|
0af4a67881
|
feat(frontends/lean): save type information after elaboration, remove --flyinfo option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 19:35:26 -07:00 |
|
Leonardo de Moura
|
0276f4c1c0
|
feat(frontends/lean): store 'overload' information, remove #setline
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 19:13:09 -07:00 |
|
Leonardo de Moura
|
1ba9a92df2
|
feat(frontends/lean/parser): save snapshots
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 18:31:53 -07:00 |
|
Leonardo de Moura
|
9b765a2a06
|
chore(frontends/lean): fix style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 18:10:33 -07:00 |
|
Leonardo de Moura
|
1a725574b1
|
refactor(frontends/lean): add 'server' module as a replacement for 'interactive'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 18:07:04 -07:00 |
|
Leonardo de Moura
|
2c3737bcc6
|
feat(frontends/lean): add info_manager
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-06 15:25:28 -07:00 |
|
Leonardo de Moura
|
069f217215
|
fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-05 17:21:21 -07:00 |
|
Leonardo de Moura
|
d14cbfd7e9
|
refactor(frontends/lean/elaborator): local context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-05 16:25:54 -07:00 |
|
Leonardo de Moura
|
9cc2015caa
|
feat(library/unifier): better error message for invalid local context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-05 16:25:22 -07:00 |
|
Leonardo de Moura
|
56d151ef7f
|
feat(frontends/lean): 'partial' aliases. closes #24
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-04 22:08:10 -07:00 |
|
Leonardo de Moura
|
d5bb7d45ec
|
fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-04 13:58:47 -07:00 |
|
Leonardo de Moura
|
2dca68e645
|
chore(util/list): add inline functions for commonly used patterns in list processing code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-03 13:51:38 -07:00 |
|
Leonardo de Moura
|
bae9700260
|
fix(frontends/lean/dependencies): take relative paths into account when computing dependencies
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 20:03:51 -07:00 |
|
Leonardo de Moura
|
4b030c5d5f
|
feat(library/module): relative module path
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 19:47:55 -07:00 |
|
Leonardo de Moura
|
8c37a95164
|
fix(frontends/lean/scanner): typo reported by clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 15:24:04 -07:00 |
|
Leonardo de Moura
|
249c878597
|
fix(frontends/lean/elaborator): warning message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 15:21:23 -07:00 |
|
Leonardo de Moura
|
a62e6f84e3
|
feat(frontends/lean/scanner): allow letter-like unicode characters and sub/super-scripts in identifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 00:47:58 -07:00 |
|
Leonardo de Moura
|
52e3505599
|
feat(frontends/lean): display warning message when importing file that uses 'sorry'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-02 00:47:58 -07:00 |
|
Leonardo de Moura
|
0465c6ef53
|
fix(frontends/lean): flyinfo for identifiers defined in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 21:15:02 -07:00 |
|
Leonardo de Moura
|
3795d466c1
|
fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 20:57:24 -07:00 |
|
Leonardo de Moura
|
0c9317b167
|
feat(frontends/lean/elaborator): add flyinfo for placeholders
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 20:25:06 -07:00 |
|
Leonardo de Moura
|
8bd36dabce
|
refactor(kernel/pos_info_provider): get_pos_info return none if position is not available
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 20:17:26 -07:00 |
|
Leonardo de Moura
|
df57043861
|
fix(frontends/lean/scanner): decode utf8
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 19:58:02 -07:00 |
|
Leonardo de Moura
|
4b604521a0
|
fix(frontends/lean): add hack for flycheck
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 16:26:04 -07:00 |
|
Leonardo de Moura
|
bd766d8b0e
|
fix(frontends/lean/elaborator): remove duplicate entries in flyinfo data
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 14:40:26 -07:00 |
|
Leonardo de Moura
|
4cb8fb20fe
|
fix(frontends/lean/elaborator): bug when mixing string and non-strict implict arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 10:58:20 -07:00 |
|
Leonardo de Moura
|
466dd11d1b
|
fix(frontends/lean/dependencies): warning message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 19:59:05 -07:00 |
|
Leonardo de Moura
|
f39b2eb70f
|
feat(frontends/lean): add --flyinfo option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 19:54:21 -07:00 |
|
Leonardo de Moura
|
c01b4bd636
|
fix(frontends/lean/parser): generate flycheck-friendly import error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 19:03:54 -07:00 |
|
Leonardo de Moura
|
6ca80b5000
|
feat(frontends/lean): add 'sorry'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 18:35:57 -07:00 |
|
Leonardo de Moura
|
9cf93c8299
|
feat(library/error_handling): add helpers classes for creating WARNING and INFO annotations for flycheck
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 17:41:39 -07:00 |
|
Leonardo de Moura
|
ba98634a7a
|
feat(frontends/lean/pp): do not display metavariable arguments by default, add option pp.metavar_args to control whether they are displayed or not
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 16:46:16 -07:00 |
|
Leonardo de Moura
|
92e90fbd07
|
feat(library/error_handling): add flycheck_scope helper class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 12:45:54 -07:00 |
|
Soonho Kong
|
14a406d4d7
|
feat: add "--flycheck" option to print out error msgs for flycheck
|
2014-07-31 11:18:51 -07:00 |
|
Soonho Kong
|
82afcfac9c
|
fix(frontends/lean/parser.cpp): fix typo
|
2014-07-31 10:15:45 -07:00 |
|
Leonardo de Moura
|
1d62a614e7
|
fix(frontends/lean): remove keywords 'class' and '[class]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-30 15:05:44 -07:00 |
|
Leonardo de Moura
|
9637ceb86e
|
feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-30 15:04:44 -07:00 |
|
Leonardo de Moura
|
5238da9ac7
|
refactor(frontends/lean): rename action::is_compatible to action::is_equal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-30 12:37:35 -07:00 |
|
Leonardo de Moura
|
936bb2744b
|
fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 17:32:55 -07:00 |
|
Leonardo de Moura
|
6e135832d8
|
feat(frontends/lean/pp): pretty print '@' explict operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 14:26:27 -07:00 |
|
Leonardo de Moura
|
320bc55e85
|
fix(frontends/lean/elaborator): use preprocessed expression when displaying errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 14:25:50 -07:00 |
|
Leonardo de Moura
|
634363c5ec
|
fix(frontends/lean/dependencies): dependency generation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 14:13:31 -07:00 |
|
Leonardo de Moura
|
b15f1bb8c7
|
fix(frontends/lean/elaborator): apply coercions in definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 13:55:39 -07:00 |
|
Leonardo de Moura
|
501cae37e5
|
fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-29 13:04:58 -07:00 |
|
Leonardo de Moura
|
33c77afc29
|
feat(frontends/lean/structure): add 'structure' command skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-28 19:59:38 -07:00 |
|