Sebastian Ullrich
74d80444ff
fix(frontends/lean/vm_elaborator): elab_attribute_cmd
2019-01-21 17:53:05 +01:00
Sebastian Ullrich
7001eee350
fix(frontends/lean/vm_elaborator): never resolve to section variables in patterns
2019-01-20 18:48:51 +01:00
Sebastian Ullrich
c22fbb5cde
feat(library/init/lean,frontends/lean/vm_elaborator): set_option
2019-01-20 18:21:41 +01:00
Sebastian Ullrich
dcd3b3dc5d
fix(library/init/lean/elaborator): section variables need to be preresolved as well
...
In
```
section binary
variables {α : Type u} {β : Type v}
variable f : α → α → α
local infix * := f
def commutative := ∀ a b, a * b = b * a
end binary
```
the expansion of `*` applies a macro scope to `f`, so we need to resolve it
before that
2019-01-20 13:22:08 +01:00
Sebastian Ullrich
543c3d21ff
fix(frontends/lean/vm_elaborator): match and equations, oof
2019-01-19 15:20:52 +01:00
Leonardo de Moura
a001806996
feat(library/compiler/compiler): generate boxed version of builtin constants
2019-01-18 15:43:06 -08:00
Sebastian Ullrich
c1534fd476
feat(frontends/lean/vm_elaborator): [recursor] arguments
2019-01-17 19:57:00 +01:00
Sebastian Ullrich
a23df570fc
fix(library/init/lean/elaborator): match
2019-01-17 19:57:00 +01:00
Sebastian Ullrich
175a9f0f5c
fix(frontends/lean/vm_elaborator): skip local refs created deep inside elab_defs
2019-01-17 19:57:00 +01:00
Sebastian Ullrich
3e8e823893
fix(frontends/lean/vm_elaborator): preserve internal name of section variables
2019-01-17 19:57:00 +01:00
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
