Commit graph

38 commits

Author SHA1 Message Date
Leonardo de Moura
30571f12d4 chore: adjust runtime to new EState 2019-10-21 17:05:16 -07:00
Leonardo de Moura
5902ef30d6 refactor: prepare to change EState 2019-10-21 16:51:48 -07:00
Leonardo de Moura
3d7a7c7e91 feat(library/init/util): add panic primitive 2019-09-30 16:23:18 -07:00
Leonardo de Moura
a4b860b92a fix(runtime): missing Array.data primitive 2019-09-19 10:27:10 -07:00
Leonardo de Moura
a7d616605a fix(runtime/lean): missing primitive 2019-09-19 09:54:03 -07:00
Leonardo de Moura
4ac235212a fix(runtime/lean): incorrect assertion 2019-08-28 15:50:11 -03:00
Leonardo de Moura
f40617d8dd feat(CMakeLists, runtime): add CHECK_RC_OVERFLOW cmake option 2019-08-28 15:35:46 -03:00
Leonardo de Moura
a944d158a3 feat(CMakeLists.txt): add SMALL_RC cmake option
When used with `COMPRESSED_OBJECT_HEADER`, Lean uses a compressed
object header where only 32-bits are reserved for the RC.
The motivation is performance, in our experiments, it is faster to
access a 32-bit counter than a 45-bit one.
With a smaller RC, we can use 8-bits for the memory kind information,
and speedup its access.
2019-08-28 14:54:08 -03:00
Leonardo de Moura
2d103caa76 perf(runtime/lean): use the low level hack we used in the previous runtime 2019-08-24 11:05:28 -07:00
Leonardo de Moura
358f8c5483 fix(runtime/lean): missing "static" 2019-08-24 07:40:56 -07:00
Leonardo de Moura
140708fe8d chore(runtime): style 2019-08-24 07:40:56 -07:00
Leonardo de Moura
70f3537a29 feat(runtime): add lean_panic and variants 2019-08-24 07:40:39 -07:00
Leonardo de Moura
cee0264363 feat(CMakeLists.txt): add "COMPRESSED_OBJECT_HEADER" cmake option 2019-08-24 07:40:38 -07:00
Leonardo de Moura
6553c5531c fix(runtime): bugs at compact.cpp and object size calculation 2019-08-24 07:40:38 -07:00
Leonardo de Moura
79f4eeea62 fix(runtime/lean): incorrect assertion 2019-08-24 07:40:38 -07:00
Leonardo de Moura
124c5da414 fix(runtime): disable compressed headers and fix bugs 2019-08-24 07:40:38 -07:00
Leonardo de Moura
3b762d4dc0 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Leonardo de Moura
dcd15f3424 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Leonardo de Moura
166eff9525 fix(runtime/lean): missing details 2019-08-21 09:37:36 -07:00
Leonardo de Moura
9e8ac5ae27 chore(runtime/lean): style 2019-08-20 19:46:53 -07:00
Leonardo de Moura
1dc1bcf521 fix(runtime/lean): stdatomic.h vs atomic issue 2019-08-20 17:56:24 -07:00
Leonardo de Moura
e002c96654 chore(runtime/lean): style 2019-08-20 10:20:55 -07:00
Leonardo de Moura
6d6cb14f9e feat(library/init/lean/compiler/ir/emitc,shell/lean): add --c=<filename> option 2019-08-20 10:13:40 -07:00
Leonardo de Moura
a8d6bed95f feat(runtime/lean): add lean_apply_* 2019-08-20 09:24:02 -07:00
Leonardo de Moura
a98095ad4f feat(runtime/lean): missing APIs 2019-08-20 09:19:28 -07:00
Leonardo de Moura
5eafa7e391 feat(runtime/lean): UInt8/UInt16/UInt32/UInt64/USize APIs 2019-08-20 09:06:35 -07:00
Leonardo de Moura
af634536bd feat(runtime/lean): Int API 2019-08-20 07:47:41 -07:00
Leonardo de Moura
44dd77a739 feat(runtime/lean): ByteArray API 2019-08-19 10:12:36 -07:00
Leonardo de Moura
1fc9f09bef feat(runtime/lean): Nat API 2019-08-19 09:48:13 -07:00
Leonardo de Moura
43705872fd feat(runtime/lean): Task and External APIs 2019-08-19 09:21:16 -07:00
Leonardo de Moura
750748440e feat(runtime/lean): Thunk API 2019-08-19 08:56:41 -07:00
Leonardo de Moura
70f832727f feat(runtime/lean): string API 2019-08-18 08:44:01 -07:00
Leonardo de Moura
d0dab47877 feat(runtime/lean): array of objects API 2019-08-18 08:31:57 -07:00
Leonardo de Moura
57fd302f84 chore(runtime/lean): style 2019-08-16 21:01:14 -07:00
Leonardo de Moura
2758681d78 feat(runtime/lean): closures 2019-08-16 16:14:34 -07:00
Leonardo de Moura
4a24b400c8 feat(runtime/lean): constructor API 2019-08-16 15:53:35 -07:00
Leonardo de Moura
d4ef508722 chore(runtime/lean): style 2019-08-16 09:57:34 -07:00
Leonardo de Moura
216d6fc6aa feat(runtime): start C runtime 2019-08-15 20:15:35 -07:00