Sebastian Ullrich
cbc297e5c5
feat(frontends/lean/vm_elaborator): resolve names in constants' types
...
This is just a stop-gap solution. We need to move name resolution to Lean to
correctly handle names preresolved by the macro expander.
2018-12-19 18:49:33 +01:00
Sebastian Ullrich
0a5af76f1a
feat(frontends/lean/vm_elaborator): capture and pass all elab messages to Lean
2018-12-19 16:22:30 +01:00
Sebastian Ullrich
ead4e8998d
feat(library/init/lean/elaborator): elaborate constants
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
c5dfe7f86e
refactor(frontends/lean/decl_cmds): factor out and expose elaboration of variables and constants
2018-12-19 15:04:48 +01:00
Sebastian Ullrich
4f7be93e87
feat(library/init/lean): remove support for section aliases
2018-12-18 17:04:04 +01:00
Sebastian Ullrich
db6b1d6e85
feat(frontends/lean/vm_elaborator,library/init/lean/elaborator): pass parser_state between languages, create parser object on C++ side to existing functions (that don't actually parse anything)
2018-12-18 15:30:38 +01:00
Sebastian Ullrich
861136d290
feat(frontends/lean/decl_cmds): universe(s) now behaves like universe variable(s)
2018-12-17 23:30:28 +01:00
Sebastian Ullrich
4e96f092f9
feat(library/init/lean/elaborator): delegate elaboration of attribute
2018-12-14 17:38:19 +01:00
Sebastian Ullrich
d9a22d43b2
feat(library/vm/vm_aux): add primitive for calling old elaborator
2018-12-14 17:36:56 +01:00
Sebastian Ullrich
c8eaee74b4
feat(frontends/lean,library/init/lean/parser/combinators): add node_longest_choice! macro
2018-11-19 18:02:28 +01:00
Sebastian Ullrich
7d7d15f8f7
chore(frontends/lean/elaborator): improve error positions
2018-11-19 15:28:23 +01:00
Sebastian Ullrich
774d776133
feat(frontends/lean/builtin_exprs): pattern let with type
2018-11-19 14:15:25 +01:00
Sebastian Ullrich
2f8e6cc975
chore(frontends/lean/elaborator,library/compiler/compiler): avoid error recovery errors
2018-11-14 09:52:22 +01:00
Sebastian Ullrich
090c4c0ce7
feat(library/init/lean/syntax): add lazily propagated macro scopes to syntax_node
2018-11-06 16:46:50 +01:00
Sebastian Ullrich
8c27f0aac6
refactor(frontends/lean/elaborator,library/init/lean): finish no_kind refactoring
2018-11-04 20:24:40 +01:00
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
