Leonardo de Moura
|
e5666b3464
|
feat(library/compiler): remove another reference to vm.h
|
2018-11-15 16:38:01 -08:00 |
|
Sebastian Ullrich
|
2f8e6cc975
|
chore(frontends/lean/elaborator,library/compiler/compiler): avoid error recovery errors
|
2018-11-14 09:52:22 +01:00 |
|
Leonardo de Moura
|
7365b9ed30
|
feat(library/compiler/lambda_lifting): cache names for lifted lambdas
We were creating hundreds of different names for simple lambdas. Example:
```
λ a, @coroutine.done a
```
|
2018-11-13 15:13:55 -08:00 |
|
Leonardo de Moura
|
4136bad252
|
feat(library/compiler): insert boxing/unboxing instructions
|
2018-11-12 17:17:09 -08:00 |
|
Leonardo de Moura
|
3ae908f8de
|
feat(library/compiler): add _jmp instruction, and skeleton for explicit boxing introduction step
|
2018-11-12 10:51:42 -08:00 |
|
Leonardo de Moura
|
7c86a4dae7
|
feat(library/compiler): add reduce_arity compilation step
|
2018-11-09 14:30:33 -08:00 |
|
Leonardo de Moura
|
d3ad1cbfe1
|
feat(library/compiler): add type inference for ENF and LLNF
|
2018-11-09 13:17:11 -08:00 |
|
Leonardo de Moura
|
df39be927d
|
feat(library/compiler): make sure application arguments are free variables or neutral terms in LLNF
|
2018-11-07 17:25:20 -08:00 |
|
Leonardo de Moura
|
17679799a2
|
fix(library/compiler/cse): must take a flag indicating whether we are applying optimization after/before erasure
|
2018-11-07 16:38:24 -08:00 |
|
Leonardo de Moura
|
330e2700b1
|
chore(library/compiler/compiler): add trace.compiler.boxed option for debugging purposes
|
2018-11-06 16:55:02 -08:00 |
|
Leonardo de Moura
|
d871c4f7d8
|
feat(library/compiler): replace simp_inductive with llnf
|
2018-10-29 13:07:46 -07:00 |
|
Leonardo de Moura
|
388b4ea6ac
|
feat(library/compiler/llnf): basic llnf module with support for unboxed types
TODO: support for reusing memory cells
|
2018-10-29 11:02:04 -07:00 |
|
Leonardo de Moura
|
a161eec8f2
|
feat(library/compiler): add llnf (low level normal form) skeleton
|
2018-10-27 12:36:30 -07:00 |
|
Leonardo de Moura
|
01229425a2
|
feat(library/compiler/compiler): inline "small" stage2 declarations at csimp after erasure
|
2018-10-22 15:49:07 -07:00 |
|
Leonardo de Moura
|
0bcd07f076
|
feat(library/compiler/compiler): cache "stage2"
|
2018-10-22 10:19:39 -07:00 |
|
Leonardo de Moura
|
e0bb21ba0b
|
chore(library): remove noncomputable module
|
2018-10-22 09:39:03 -07:00 |
|
Leonardo de Moura
|
4929af1dd3
|
feat(library/compiler/extract_closed): extract_closed is working
|
2018-10-19 18:32:49 -07:00 |
|
Leonardo de Moura
|
356928c873
|
feat(library/compiler): add extract_closed skeleton
|
2018-10-19 16:14:59 -07:00 |
|
Leonardo de Moura
|
eb02add3de
|
feat(library/compiler): simplify again after lambda lifting
Motivation: we avoid the creation of closures at join point declarations.
|
2018-10-19 15:17:07 -07:00 |
|
Leonardo de Moura
|
17b9b21555
|
feat(library/compiler/csimp): allow csimp to be used after erasure
|
2018-10-19 12:02:29 -07:00 |
|
Leonardo de Moura
|
611f6ae780
|
feat(library/compiler/specialize): code specialization
TODO:
- Cache results at `specialize_ext`
- Cleanup
It is not feasible to run code specializer without cache: code explosion.
|
2018-10-16 15:50:42 -07:00 |
|
Leonardo de Moura
|
42c056862d
|
feat(library/compiler/compiler): cache stage1 result before specialization
|
2018-10-15 13:08:48 -07:00 |
|
Leonardo de Moura
|
9ca4c362ae
|
feat(library/compiler/specialize): add spec_info
Store which arguments can be specialized.
|
2018-10-15 12:54:34 -07:00 |
|
Leonardo de Moura
|
27e6f7f424
|
feat(library/compiler): invoke specialize skeleton
|
2018-10-09 15:23:42 -07: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
|
662c0ebb31
|
feat(library/compiler/compiler): cache stage1
|
2018-10-08 17:06:45 -07:00 |
|
Leonardo de Moura
|
124b4d37fe
|
feat(library/compiler): port simp_inductive to the new compiler stack
This commit also fixes a bug in the old `simp_inductive` module, and
removes now obsolete files (`compiler_step_visitor` and `old_util`).
|
2018-10-08 16:58:43 -07:00 |
|
Leonardo de Moura
|
d2fcb7af39
|
chore(library/compiler/compiler): add tracing to new compiler frontend
|
2018-10-08 15:22:36 -07:00 |
|
Leonardo de Moura
|
787d1ecb93
|
feat(library/compiler/lambda_lifting): new lambda lifting
|
2018-10-08 15:04:59 -07:00 |
|
Leonardo de Moura
|
fc62e8f3a4
|
chore(library/compiler): cdecl ==> comp_decl
|
2018-10-05 17:30:27 -07:00 |
|
Leonardo de Moura
|
6b8008a222
|
feat(library/compiler): new compiler entry point (skeleton)
|
2018-10-05 17:30:27 -07:00 |
|