Leonardo de Moura
13f0a7cd81
chore(frontends/lean, library/vm): save some debugging help code
2018-10-03 13:20:24 -07:00
Sebastian Ullrich
25b9deab15
fix(frontends/lean/elaborator): fix try_monad_coercion
2018-10-02 14:55:28 -07:00
Sebastian Ullrich
da04491df1
fix(frontends/lean/builtin_exprs): trim view field names
2018-10-02 14:55:28 -07:00
Leonardo de Moura
b4c2861939
refactor(library/compiler): rename "erasure normal form" functions
2018-10-01 14:17:11 -07:00
Leonardo de Moura
81e9e95570
chore(library/compiler): erase_irrelevant ==> old_erase_irrelevant
2018-10-01 14:17:11 -07:00
Leonardo de Moura
990fbe3c30
feat(library/compiler): provide options to vm_compile
2018-09-30 08:50:40 -07:00
Sebastian Ullrich
6cbb77c068
fix(frontends/lean/elaborator): node!: fix view code of try block
2018-09-28 13:08:24 -07:00
Leonardo de Moura
c746783c0d
fix(frontends/lean/pp): bug when pretty printing kernel projections
2018-09-27 17:09:02 -07:00
Sebastian Ullrich
e661aaeacf
refactor(library/init/lean/parser): store registered parsers in configs, use config hierarchy to avoid mutually recursive types
...
And other refactorings along the way
2018-09-27 10:05:10 -07:00
Leonardo de Moura
ae81ac2768
chore(frontends/lean): remove parameter command from old parser
...
We still have a lot of leftover code, but it is not worth removing it
since we will delete the old parser.
2018-09-26 17:54:11 -07:00
Sebastian Ullrich
18cf4d50bb
chore(frontends/lean/elaborator): ignore error caused by synthetic sorry
2018-09-25 16:48:01 -07:00
Sebastian Ullrich
90984a63e8
chore(frontends/lean/elaborator): improve application error positions
2018-09-25 16:08:57 -07:00
Sebastian Ullrich
11259b62d2
chore(frontends/lean/elaborator): try to make error positions a bit more accurate
2018-09-25 14:48:57 -07:00
Sebastian Ullrich
ac7b70c555
fix(frontends/lean/token_table): add missing built-in token
...
`::` is used not only by `list` but also the built-in `structure` command
2018-09-25 12:20:08 -07:00
Sebastian Ullrich
f29a866cb4
perf(frontends/lean/elaborator): do not inline views for now
2018-09-24 18:24:27 -07:00
Sebastian Ullrich
32f4d52e1c
refactor(library/init/lean): revert introduction of tysyntax; push syntax.missing through views
2018-09-24 18:24:27 -07:00
Sebastian Ullrich
aac3627ce1
fix(frontends/lean/elaborator): restore better field notation error message
2018-09-24 18:24:27 -07:00
Sebastian Ullrich
f0a983fe30
fix(frontends/lean/pp): function with implicits in structure instance
2018-09-24 09:53:28 -07:00
Sebastian Ullrich
9a0b1c7a7f
feat(library/init/lean/parser/basic): allow views to specify default value used with opt_param when nested in other views
2018-09-24 09:53:28 -07:00
Leonardo de Moura
a31f12d8cd
chore(library/init/core): revert ite+thunks modification
...
We don't need it since we marked `ite` as `[macro_inline]`
2018-09-23 19:27:06 -07:00
Sebastian Ullrich
41c0bc87fd
refactor(library/init/lean/parser): make views shallow via tysyntax
2018-09-22 21:24:38 -07:00
Sebastian Ullrich
15d11cc483
feat(library/module_mgr): profile .olean serialization/deserialization
2018-09-20 13:54:17 -07:00
Leonardo de Moura
0ff1f16bf0
feat(frontends/lean/pp): add pp.compact_let option
...
It helps to debug the new compiler stack.
2018-09-20 12:05:48 -07:00
Sebastian Ullrich
0a8d0a6870
feat(library/init/lean/parser/term): projection notation
2018-09-20 09:40:21 -07:00
Leonardo de Moura
4f53e505b0
fix(library/compiler): we need to unfold auxiliary nested _match applications eagerly
2018-09-18 14:17:37 -07:00
Leonardo de Moura
b07c718425
refactor(library/init/core): change ite signature
2018-09-17 14:27:28 -07:00
Sebastian Ullrich
98e09c274f
feat(library/init/lean/parser/{pratt,level}): factor out pratt combinator, implement level parsers
2018-09-13 16:38:40 -07:00
Sebastian Ullrich
b7c3f517a9
feat(frontends/lean/builtin_exprs): support for precedence annotations in node!/node_choice!
2018-09-13 16:38:40 -07:00
Leonardo de Moura
df9d0b2211
fix(frontends/lean/elaborator): avoid internal identifiers leaking as "user names" in equations
2018-09-12 15:09:44 -07:00
Leonardo de Moura
3ba777e709
fix(frontends/lean/pp): do not pp let type when m_binder_types == false
2018-09-11 18:10:10 -07:00
Leonardo de Moura
3feae112bc
chore(frontends/lean/parser): unused var warning
2018-09-11 13:55:44 -07:00
Sebastian Ullrich
78ced9ffcf
refactor(library/module_mgr): minimize parser interface
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af99f153f8
refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
904d7c4a88
chore(*): remove old task API and task queues
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af55cb13e7
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6
refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
99ab0e9d67
refactor(library/messages): make an object_ref
2018-09-11 13:55:25 -07:00
Leonardo de Moura
f5ac6875a6
chore(frontends/lean/json): style
2018-09-08 16:23:48 -07:00
Leonardo de Moura
81a694e73c
chore(frontends/lean): remove dead code
2018-09-08 15:44:49 -07:00
Leonardo de Moura
fabfe32ca5
chore(*): remove unnecessary scoped_ext dependencies
2018-09-08 15:42:48 -07:00
Leonardo de Moura
dacc4c9cd6
chore(kernel): move abstract_type_context to library
2018-09-08 08:29:51 -07:00
Leonardo de Moura
3e5f59d6df
chore(kernel): remove expr.quote constructor
...
In Lean4, we will reify expressions.
2018-09-07 22:08:08 -07:00
Leonardo de Moura
13fbd8304e
chore(library,frontends/lean): use is_constructor, is_recursor, is_inductive helper functions
...
They do not throw exception if the constant is not declared in the environment.
2018-09-07 20:36:42 -07:00
Leonardo de Moura
85465885f3
chore(library/type_context): remove "frozen local instances"
...
We will re-implement the type class resolution algorithm, and the new
implementation will not rely on a persistent cache. We will improve
performance by:
1) Using better indexing data-structures.
2) Using a local cache during the search.
2018-09-07 13:17:37 -07:00
Leonardo de Moura
49b5216604
chore(library): remove fingerprint
2018-09-07 12:54:19 -07:00
Leonardo de Moura
2315bc4653
chore(library): remove documentation environment extension
2018-09-07 12:09:41 -07:00
Leonardo de Moura
5d00936a8f
chore(*): remove some old_type_checker dependencies
2018-09-07 08:48:21 -07:00
Leonardo de Moura
130b419371
chore(frontends/lean): remove break_at_pos support
...
We have already removed auto-completion support.
This change allowed me to remove another old_type_checker dependency.
2018-09-07 08:34:19 -07:00
Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -07:00
Leonardo de Moura
3c521960c8
chore(library/class): remove attribute tracking symbols
2018-09-05 18:42:19 -07:00
