Sebastian Ullrich
0509cfcf99
fix(frontends/lean/vm_elaborator): name to obj
2019-01-17 19:57:00 +01:00
Sebastian Ullrich
3611eda136
fix(frontends/lean/vm_elaborator): message order
2019-01-17 19:57:00 +01:00
Sebastian Ullrich
cbed0d232d
fix(frontends/lean/definition_cmds): collect implicit locals in both frontends
2019-01-17 18:55:43 +01:00
Sebastian Ullrich
16d7ee5aff
fix(frontends/lean/vm_elaborator): pattern variables
2019-01-17 17:06:52 +01:00
Sebastian Ullrich
8cc35b854b
feat(library/init/lean/{expander,elaborator}): variable(s)
2019-01-17 17:06:52 +01:00
Sebastian Ullrich
8835a7b7d9
feat(frontends/lean/vm_elaborator): return new local context
2019-01-17 17:06:52 +01:00
Sebastian Ullrich
15cc07fe17
fix(frontends/lean/vm_elaborator): initialization
2019-01-17 13:34:28 +01:00
Sebastian Ullrich
0923a2cbae
refactor(library/init/lean/elaborator): avoid deprecated expr locals in new elaborator state
2019-01-17 12:29:44 +01:00
Sebastian Ullrich
e726c64895
feat(frontends/lean/vm_elaborator): synthesize instance names
2019-01-16 19:12:40 +01:00
Sebastian Ullrich
2c4b566038
feat(frontends/lean/vm_elaborator): implement equations
2019-01-16 19:12:40 +01:00
Leonardo de Moura
c268796545
fix(frontends/lean): clang errors and warnings
...
cc @kha
2019-01-15 13:48:08 -08:00
Sebastian Ullrich
5660a8e690
feat(library/init/lean/elaborator): transmit position information
2019-01-15 18:28:35 +01:00
Sebastian Ullrich
cead81fcea
fix(frontends/lean/inductive_cmds): set m_explicit_levels, and call collect_implicit_locals only after that
2019-01-15 16:47:28 +01:00
Sebastian Ullrich
d0062691de
feat(library/init/lean): implement init_quot
2019-01-15 15:06:51 +01:00
Sebastian Ullrich
6e64089123
feat(frontends/lean/structure_cmd): implement structure
2019-01-15 15:01:52 +01:00
Sebastian Ullrich
7aa06338c9
feat(frontends/lean/vm_elaborator): implement inductive
2019-01-14 14:49:40 +01:00
Sebastian Ullrich
93d8431d00
fix(frontends/lean/definition_cmds): fix build
2019-01-14 11:24:11 +01:00
Sebastian Ullrich
84e9dd9b1a
feat(library/init/lean/elaborator,frontends/lean/vm_elaborator): implement def/theorem/abbreviation
2019-01-12 15:10:00 +01:00
Sebastian Ullrich
49f580f190
feat(library/compiler/builtin,frontends/lean/vm_elaborator): add temporary expr.local primitive
...
This makes it possible (or at least much easier) to interface with old
parser/elaborator code using local_consts for e.g. `def` parameters.
2019-01-12 14:16:43 +01:00
Sebastian Ullrich
da865fc33a
refactor(frontends/lean/{vm_,}elaborator): move name resolution over to parser locals
...
In the end I wasn't quite sure whether this is necessary, but it's at least simpler.
2019-01-12 14:14:22 +01:00
Sebastian Ullrich
2b5f19677d
feat(frontends/lean/vm_elaborator): elaborate #check
2019-01-07 22:19:47 +01:00
Sebastian Ullrich
b17568aeff
feat(library/init/lean/elaborator): pass current namespace to C++ elaborator
...
This seems to be the only information in `scope_mng_ext` we definitely need
2019-01-06 18:10:49 +01:00
Sebastian Ullrich
d2de703e51
feat(frontends/lean/vm_elaborator): add primitive environment.contains
2019-01-06 15:47:06 +01:00
Sebastian Ullrich
9a6ae42be8
feat(frontends/lean/vm_elaborator): return new environment
2019-01-06 15:44:56 +01:00
Sebastian Ullrich
807b460e9c
feat(*/elaborator): pass preresolved names to C++ as annotations and use them for global name resolution
...
With actual preresolution still missing, the only preresolved names so far are
ones like `opt_param` from built-in macros that have been preresolved manually
(and which weren't successfully resolved before this commit because of the macro
scopes applied to them)
2019-01-01 23:59:23 +01:00
Sebastian Ullrich
5757792345
chore(library/placeholder): remove unused placeholder type and kinds
2018-12-21 15:52:56 +01:00
Sebastian Ullrich
8753491cb5
chore(library/placeholder): remove obsolete level one_placeholder
...
Remnant of the previous Type/Sort approach
2018-12-21 15:52:56 +01:00
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
