max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
15391 commits 1 branch 0 tags 5.3 GiB
Commit graph

10610 commits

Author SHA1 Message Date
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
afd30d73c1 chore(library/compiler/compiler): generate Lean IR with explicit boxing and RC instructions 
This is just for testing. These two steps are not used by `emit_bytecode`,
but they will be used to generate C++ code.
We can now compile the whole corelib in debug mode with these two extra
transformation without any assertion violation.
 2019-01-18 16:01:47 -08:00
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
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
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
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
3d66e7dbe1 fix(library/pos_info_provider): row and column were swapped 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
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
Leonardo de Moura
e0da13128e refactor(library/compiler/llnf): explicit_rc_fn 2019-01-09 16:57:38 -08:00
Leonardo de Moura
7b4b92702f feat(library/compiler/llnf): cancel _unbox over _box and _box over _unbox 2019-01-09 16:57:38 -08:00
Leonardo de Moura
78379e2224 fix(library/compiler/llnf): avoid unnecessary let-decl at cast_if_needed 2019-01-09 16:57:38 -08:00
Leonardo de Moura
c1fd3e6062 fix(library/compiler/llnf): unnecessary let-decl 2019-01-09 16:57:38 -08:00
Leonardo de Moura
8111aaad8a fix(library/compiler/llnf): missing case 2019-01-09 16:57:37 -08:00