Sebastian Ullrich
09aa4f9ab3
chore(frontends/lean/elaborator): don't try to recover from errors in patterns
2018-11-04 19:03:00 +01:00
Sebastian Ullrich
0d7ea62f9a
perf(frontends/lean/elaborator,library/init/lean): put out_params first to benefit from instance pre-filtering
2018-10-30 17:43:05 +01:00
Sebastian Ullrich
8a3e7821d7
fix(frontends/lean/elaborator): weaken assertion
...
There are still some cases like errors in nested equations that leak
metavariables, but as long as we report at least one error, that probably isn't
a high-priority issue.
2018-10-30 17:43:05 +01:00
Leonardo de Moura
9256618d67
chore(library/vm): remove vm_name
2018-10-23 11:32:56 -07:00
Leonardo de Moura
4cb6b1f9d5
chore(library/tactic): reduce dependencies
2018-10-23 11:32:56 -07:00
Leonardo de Moura
e0bb21ba0b
chore(library): remove noncomputable module
2018-10-22 09:39:03 -07:00
Leonardo de Moura
77e3c18cb0
feat(library/module): noncomputable keyword is now used only to disable code generation
...
We do not try to check whether code generation will succeed or not for
some declaration. In the future, we should probably rename it to
`nocode` or something similar.
cc @kha
2018-10-22 09:35:05 -07:00
Sebastian Ullrich
d9208e2b8b
feat(library/vm/vm): add profiler.perf_script_file option
...
sample usage:
$ lean -Dprofiler.perf_script_file=parser1.script parser1.lean
$ gprof2dot -f perf < parser1.script > parser1.dot
2018-10-22 15:01:49 +02:00
Leonardo de Moura
5d726eb210
feat(library/compiler/compiler): switch to new compiler frontend
...
We also rename `vm_compiler` module to `emit_bytecode`.
We will eventually replace this module with the new IR emitter.
2018-10-08 17:38:17 -07:00
Leonardo de Moura
e75d8eacb6
fix(frontends/lean/elaborator): compilation erros with g++ 4.9
2018-10-08 11:54:28 -07:00
Sebastian Ullrich
305984bab5
feat(frontends/lean/elaborator): show context of unassigned mvars
2018-10-08 09:32:41 -07:00
Sebastian Ullrich
50e6b42f8c
fix(frontends/lean/elaborator): ensure_no_unassigned_metavars: only check mvars in parameter
...
Had forgotten to re-check the standard lib...
2018-10-07 21:11:02 -07:00
Sebastian Ullrich
aea86eb828
feat(frontends/lean/elaborator): simple, accurate mvar error position tracking
...
The accuracy of `m_last_pos` still needs to be improved at some point
2018-10-05 21:25:39 -07:00
Leonardo de Moura
135a8d7508
chore(library/compiler): remove old compiler steps that have already been replaced
2018-10-05 17:30:27 -07:00
Sebastian Ullrich
c50b89a318
fix(frontends/lean/elaborator): node!/node_choice!: use constant options for printing-parsing
2018-10-04 14:27:24 -07:00
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
