Leonardo de Moura
|
fe68547086
|
fix(library/compiler/llnf): missing instruction _uproj at explicit_rc_fn
|
2019-01-18 16:00:08 -08:00 |
|
Leonardo de Moura
|
1293d976f7
|
fix(library/compiler/util): usize case was missing at to_uint_type
|
2019-01-18 15:50:14 -08:00 |
|
Leonardo de Moura
|
a001806996
|
feat(library/compiler/compiler): generate boxed version of builtin constants
|
2019-01-18 15:43:06 -08:00 |
|
Leonardo de Moura
|
aaf1966a87
|
fix(library/compiler/llnf): explicit boxing should treat variables with function type (e.g., _obj -> _obj) as _obj
|
2019-01-18 15:07:01 -08:00 |
|
Leonardo de Moura
|
9ea7b77fe0
|
fix(library/compiler/llnf): typo
|
2019-01-17 17:10:52 -08:00 |
|
Leonardo de Moura
|
1d0d17d4ae
|
fix(library/compiler/llnf): bug at explicit boxing transformation
|
2019-01-17 16:58:22 -08:00 |
|
Leonardo de Moura
|
c3dfb613d5
|
test(tests/lean/run/rc_tests): basic explicit_rc_fn tests
|
2019-01-17 15:25:27 -08:00 |
|
Leonardo de Moura
|
1b59fed1d9
|
fix(library/compiler/llnf): bug at x := _proj y
We must increment `x`'s RC before (if needed) we decrement `y`'s RC
|
2019-01-17 15:23:52 -08:00 |
|
Leonardo de Moura
|
10456f1607
|
fix(library/compiler/llnf): constructors are not global constants
|
2019-01-17 14:18:58 -08:00 |
|
Leonardo de Moura
|
a82731fb23
|
fix(library/compiler/llnf): literals are created with RC = 1
|
2019-01-17 14:08:40 -08:00 |
|
Leonardo de Moura
|
ad13d04b1d
|
chore(library/compiler/llnf): use _ to name _inc and _dec instructions
|
2019-01-17 14:04:05 -08:00 |
|
Leonardo de Moura
|
0f28d3187a
|
fix(library/compiler/llnf): avoid unnecessary _dec instruction
|
2019-01-17 13:57:13 -08:00 |
|
Leonardo de Moura
|
f315823bee
|
fix(library/compiler/llnf): missing ensure_terminal
|
2019-01-17 13:51:39 -08:00 |
|
Leonardo de Moura
|
244079a4cc
|
feat(library/compiler/llnf): add process_cases
|
2019-01-17 13:29:38 -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
|
85cad3a7f1
|
fix(library/init/lean/elaborator): equation heads
|
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
|
a29d33485c
|
feat(util/list_ref): to_list_ref, which I didn't need in the end
|
2019-01-17 17:06:52 +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
|
c338245536
|
feat(library/init/lean/elaborator): implement the only part of open/export
|
2019-01-16 19:49:44 +01:00 |
|
Sebastian Ullrich
|
13781ed114
|
feat(library/init/lean/parser/token): numeric literals of more exotic bases
|
2019-01-16 19:39:30 +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 |
|
Sebastian Ullrich
|
a6d5af7387
|
feat(library/init/lean/expander): expand class and class inductive
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
246eecf155
|
fix(library/init/lean/elaborator): do not mangle attribute names (since they are not environment identifiers)
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
ca058a6d8e
|
chore(library/init/lean/expander): simplify constant normalization
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
5ef30a9300
|
fix(library/init/lean/elaborator): have serialization
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
dce62fc190
|
fix(library/init/lean/expander): structural substitution instead of abstraction-application when applying notations
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
3d66e7dbe1
|
fix(library/pos_info_provider): row and column were swapped
|
2019-01-16 19:12:40 +01:00 |
|
Sebastian Ullrich
|
c17ba349f3
|
refactor(library/init/lean/parser/syntax): factor out syntax.(m)replace
|
2019-01-16 19:12:40 +01:00 |
|
Leonardo de Moura
|
0451a53b54
|
doc(library/compiler/llnf): document explicit_rc_fn
|
2019-01-15 16:26:09 -08:00 |
|
Leonardo de Moura
|
54fe7e7be9
|
feat(library/compiler/llnf): explicit_rc_fn
TODO: cases_on terms
|
2019-01-15 15:54:38 -08:00 |
|
Leonardo de Moura
|
c268796545
|
fix(frontends/lean): clang errors and warnings
cc @kha
|
2019-01-15 13:48:08 -08:00 |
|
Leonardo de Moura
|
579d462776
|
feat(library/compiler/llnf): add process_app
|
2019-01-15 12:49:08 -08:00 |
|
Sebastian Ullrich
|
31588a1013
|
fix(library/init/lean/elaborator): do not attach position to app, nodes without pos data
|
2019-01-15 18:51:24 +01:00 |
|
Sebastian Ullrich
|
5660a8e690
|
feat(library/init/lean/elaborator): transmit position information
|
2019-01-15 18:28:35 +01:00 |
|
Sebastian Ullrich
|
1b565fcaa0
|
feat(library/init/lean/elaborator): simplistic support of export
|
2019-01-15 17:44:14 +01:00 |
|
Sebastian Ullrich
|
d444b5ef49
|
chore(library/init/core): move sorry_ax up (temporarily) to get error recovery sooner
|
2019-01-15 17:42:09 +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
|
7dd21df59f
|
fix(library/init/lean/elaborator): C++ expects the oldest variable first
|
2019-01-15 16:20:46 +01:00 |
|
Sebastian Ullrich
|
d0062691de
|
feat(library/init/lean): implement init_quot
|
2019-01-15 15:06:51 +01:00 |
|