Commit graph

16584 commits

Author SHA1 Message Date
Leonardo de Moura
c6c46df285 feat(library/init/lean/compiler/ir): develop expandresetreuse 2019-05-23 12:42:31 -07:00
Leonardo de Moura
f9f4e6c14b feat(library/init/lean/compiler/ir): add expandresetreuse 2019-05-23 08:58:16 -07:00
Leonardo de Moura
aede2476de chore(stage0): update
We changed the IR representation, and the C++ code interacts with both
stage0 and stage1.
2019-05-23 08:22:36 -07:00
Leonardo de Moura
8ba7dd4cff feat(library/init/lean/compiler/ir): add del instruction for releasing memory 2019-05-23 08:01:15 -07:00
Leonardo de Moura
c6433460fb chore(library/init/lean/compiler/ir/format): naming consistency 2019-05-22 18:46:50 -07:00
Leonardo de Moura
013f0c9edb feat(library/init/lean/compiler/ir/rc): missing optimization 2019-05-22 18:46:43 -07:00
Leonardo de Moura
6bed0ca5b5 chore(library/compiler): style 2019-05-22 18:46:37 -07:00
Leonardo de Moura
5ee7a211cf chore(tests/lean/run/rc_tests): fix test 2019-05-22 18:46:30 -07:00
Leonardo de Moura
3e76e43843 fix(library/init/lean/compiler/ir/borrow): visit join point body 2019-05-22 17:31:56 -07:00
Leonardo de Moura
fe0141918a fix(library/init/lean/compiler/ir) bug at addDecAfterFullApp 2019-05-22 16:30:42 -07:00
Sebastian Ullrich
7106c7d15e feat(tests/playground/Makefile): measure Lean GC% as lean::del/dealloc execution times via perf
It looks like the Nix CXX wrapper did this for me so far
2019-05-22 23:32:33 +02:00
Sebastian Ullrich
e5ed96798b fix(tests/playground/Makefile): actually compile Lean code with optimizations 2019-05-22 23:23:30 +02:00
Sebastian Ullrich
29623cd2c5 fix(shell/lean): --cpp on stand-alone files 2019-05-22 23:23:30 +02:00
Sebastian Ullrich
c3eed47cdb feat(tests/playground/Makefile): replace bench with temci 2019-05-22 23:23:29 +02:00
Leonardo de Moura
a570e35161 chore(stage0): update 2019-05-22 11:45:58 -07:00
Leonardo de Moura
568bd1c269 fix(library/init/lean/compiler/ir/borrow): do not perform borrow inference for @[export] declarations 2019-05-22 11:44:34 -07:00
Leonardo de Moura
a8f8df1475 chore(library/init/lean/compiler): add export.lean 2019-05-22 11:27:25 -07:00
Leonardo de Moura
2408d6dd80 fix(library/init/lean/compiler/ir/boxing): created boxed version for externs 2019-05-22 10:56:51 -07:00
Leonardo de Moura
fa3079f04e chore(stage0): update 2019-05-22 10:36:36 -07:00
Leonardo de Moura
b8a32eed88 chore(tests/playground): add (temporary) scripts for testing new IR compiler 2019-05-22 08:47:38 -07:00
Leonardo de Moura
99d2f9931d fix(library/init/lean/compiler/ir/resetreuse): typo 2019-05-22 08:45:29 -07:00
Leonardo de Moura
ef89945ea0 fix(library/init/lean/compiler/ir/emitcpp): tail call
Implement fix used at 4d2837430a in the new IR compiler.
2019-05-22 07:58:33 -07:00
Leonardo de Moura
4d2837430a fix(library/compiler/emit_cpp): tail call
Add temporary hack to fix `emit_tail_call`.
TODO: find a cleaner solution for the new IR compiler.
2019-05-21 23:07:10 -07:00
Leonardo de Moura
64525116f5 fix(library/init/lean/compiler/ir): avoid compilation warning 2019-05-21 20:19:45 -07:00
Leonardo de Moura
c391bff33c fix(library/init/lean/compiler/ir/emitcpp): misssing condition 2019-05-21 20:09:27 -07:00
Leonardo de Moura
f1fbe5cd61 feat(library/compiler/ir): add boxed version for extern constants 2019-05-21 17:55:58 -07:00
Leonardo de Moura
d90cfe5a1c feat(library/init/lean/compiler/ir/boxing): generate boxed version 2019-05-21 17:35:43 -07:00
Leonardo de Moura
89259d012b fix(stage0): missing files 2019-05-21 16:39:07 -07:00
Leonardo de Moura
91745cd16b fix(library/init/lean): remove hard coded file 2019-05-21 16:26:08 -07:00
Leonardo de Moura
40b890f220 fix(library/init/lean/compiler/ir/emitcpp): typo 2019-05-21 16:21:21 -07:00
Leonardo de Moura
8003ccec13 chore(stage0): update 2019-05-21 16:12:26 -07:00
Leonardo de Moura
5b3aec088e feat(library/init/lean/compiler/ir/emitcpp): emit module initialization code 2019-05-21 16:06:10 -07:00
Leonardo de Moura
baa99aa4a5 fix(library/init/lean/compiler/ir/emitcpp): small bugs 2019-05-21 15:34:05 -07:00
Leonardo de Moura
ba9a10265e feat(library/init/lean/compiler/ir/emitcpp): implement emitVDecl remaining cases 2019-05-21 14:55:11 -07:00
Leonardo de Moura
88cf3aa5e8 feat(library/init/lean/compiler/ir/emitcpp): emit different kinds of application 2019-05-21 14:30:45 -07:00
Leonardo de Moura
ae8a51c718 feat(library/init/lean/runtime): expose runtime limit 2019-05-21 14:24:16 -07:00
Leonardo de Moura
db6933e3a4 chore(stage0): update
Make sure the new IR checker is used to validate generated code.
2019-05-21 13:45:49 -07:00
Leonardo de Moura
9f604ee0a1 fix(library/compiler/extern_attribute): register @[extern] projections in the new IR compiler 2019-05-21 13:42:42 -07:00
Leonardo de Moura
3b5093ebe0 fix(library/compiler/ir): fix ret irrelevant 2019-05-21 13:32:11 -07:00
Leonardo de Moura
5a72368967 feat(library/init/lean/compiler/ir): improve checker 2019-05-21 13:18:56 -07:00
Leonardo de Moura
63d2c03403 fix(library/compiler/ir): lambda IR translator 2019-05-21 13:01:43 -07:00
Leonardo de Moura
5aa8647b18 feat(library/init/lean/compiler/ir/emitcpp): more cases 2019-05-21 10:54:58 -07:00
Leonardo de Moura
f3e13c18f8 fix(library/init/lean/compiler/ir): reset 2019-05-21 10:28:50 -07:00
Leonardo de Moura
cc4c26e8ab feat(library/init/lean/compiler/ir/emitcpp): add some missing cases 2019-05-21 10:21:52 -07:00
Leonardo de Moura
510de7a3a9 feat(library/init/lean/compiler/ir/emitcpp): emitBlock 2019-05-21 09:20:19 -07:00
Leonardo de Moura
636415f645 chore(library/init/lean/compiler/ir/emitcpp): minor 2019-05-21 08:46:20 -07:00
Leonardo de Moura
49ef6e474a feat(library/init/lean/compiler/ir/emitcpp): better error messages 2019-05-21 08:17:55 -07:00
Leonardo de Moura
f84ea28923 fix(library/init/lean/compiler/ir/emitutil): missing FnBody.case 2019-05-21 08:11:48 -07:00
Leonardo de Moura
dbe2bebc06 fix(library/compiler/extern_attribute): register extern constructors in the new IR compiler 2019-05-21 08:09:05 -07:00
Leonardo de Moura
4ed803c564 feat(library/init/lean/compiler/ir/emitcpp): emit skeletons 2019-05-20 19:08:21 -07:00