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

65 commits

Author SHA1 Message Date
Leonardo de Moura
7a322340cb fix(library/compiler/llnf): in LLNF, the _box.n argument must be a variable 2019-01-31 17:54:06 -08:00
Leonardo de Moura
39f45beec0 chore(library/compiler/llnf): fix typo 2019-01-31 17:52:59 -08:00
Leonardo de Moura
0f47787a06 fix(library/compiler/llnf): remove bad optimization 
It may destroy boxed value information. Moreover, we want
terminals to be jmp, variable or cases.
 2019-01-31 17:52:28 -08:00
Leonardo de Moura
4166851574 feat(library/compiler/emit_cpp): emit_box and emit_unbox 2019-01-31 16:16:30 -08:00
Leonardo de Moura
80754e84c5 feat(library/compiler/emit_cpp): emit_closure 2019-01-31 15:06:04 -08:00
Leonardo de Moura
909a8d7c6d fix(library/compiler/llnf): bug at to_llnf when boxing is enabled 2019-01-30 16:48:04 -08:00
Leonardo de Moura
9f8760d936 fix(library/compiler/llnf): LLNF terminal is variable, jmp, or cases 2019-01-29 14:59:12 -08:00
Leonardo de Moura
61e51ba402 fix(library/compiler/llnf): adjust code, now type must match arity 
We recently modified the type of closures in LLNF.
This commit fixes a mismatch.
 2019-01-28 15:55:01 -08:00
Leonardo de Moura
d3756fd915 feat(library/compiler): add _void type for LLNF format 2019-01-28 13:06:25 -08:00
Leonardo de Moura
2016e1bce5 feat(library/compiler/llnf): unique names for lambda arguments 2019-01-25 14:26:32 -08:00
Leonardo de Moura
8bcc965dc0 feat(library/compiler): make sure we emit bytecode and C++ 2019-01-23 14:13:04 -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
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
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
579d462776 feat(library/compiler/llnf): add process_app 2019-01-15 12:49:08 -08: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
Leonardo de Moura
eae421c506 feat(library/compiler/llnf): explicit_rc skeleton 2018-11-28 15:44:55 -08:00
Leonardo de Moura
05d25d92c0 feat(library/compiler): only create _boxed version if needed 2018-11-28 09:46:48 -08:00
Leonardo de Moura
3d24c6466b feat(library/compiler/llnf): generate _boxed version eagerly 2018-11-15 18:10:20 -08:00
Leonardo de Moura
db5d976278 feat(library/compiler): use new builtin module 2018-11-15 16:30:42 -08:00
Sebastian Ullrich
8d25c6edc5 fix(library/compiler/llnf): fix out-of-bounds access 
@leodemoura is this correct?
 2018-11-14 09:52:22 +01:00
Leonardo de Moura
2271d4bccc chore(library/compiler): fix debug build 2018-11-13 15:26:25 -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
f9236592cc chore(library/compiler/llnf): remove dead code 2018-11-07 16:48:32 -08:00
Leonardo de Moura
474c743d8a fix(library/compiler/llnf): do not expand atomic values 2018-11-07 16:43:46 -08:00
Leonardo de Moura
687e9d076d feat(library/compiler): add _apply and _closure instructions to LLNF 2018-11-07 13:30:28 -08:00
Leonardo de Moura
5acb5e63b1 feat(library/compiler): revise llnf instructions 
Motivation: make sure we can generate "portable" C++ code. "Portable"
here means we can compile the generated code using 32 and 64 bit machines.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
6f03df871b chore(library/compiler): remove whnf_upto_runtime_type 
It is not needed anymore.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
e63721958b refactor(library/compiler): add is_enum_type auxiliary function 2018-11-06 16:55:02 -08:00
Leonardo de Moura
216a3632cc refactor(library/compiler/llnf): simplify llnf primitive instructions 2018-11-06 16:55:02 -08:00
Leonardo de Moura
39850d3b84 chore(library/compiler/llnf): remove dead global 2018-11-06 16:55:02 -08:00
Leonardo de Moura
5d89347241 feat(library/compiler/llnf): improve memory cell reuse heuristic 2018-10-31 14:44:33 -07:00
Leonardo de Moura
39c2ee2931 chore(library/compiler/llnf): typo 2018-10-31 13:22:14 -07:00
Leonardo de Moura
12a01d101c refactor(library/compiler/llnf): memory cell reuse instruction set 2018-10-31 09:35:22 -07:00
Leonardo de Moura
67a78d1c76 chore(library/compiler/llnf): cleanup 2018-10-31 08:36:09 -07:00