max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(runtime/serializer): support for tasks

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-18 14:52:29 -07:00
parent 684085d93f
commit ce504b4c21
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/runtime/serializer.cpp
View file

@ -105,6 +105,11 @@ void serializer::write_thunk(object * o) {
write_object(r);
}
void serializer::write_task(object * o) {
object * r = task_get(o);
write_object(r);
}
void serializer::write_array(object * o) {
lean_assert(is_array(o));
size_t sz = sarray_size(o);
@ -167,6 +172,7 @@ void serializer::write_object(object * o) {
switch (k) {
case object_kind::Constructor: write_constructor(o); break;
case object_kind::Closure: write_closure(o); break;
case object_kind::Task: write_task(o); break;
case object_kind::Thunk: write_thunk(o); break;
case object_kind::Array: write_array(o); break;
case object_kind::ScalarArray: write_scalar_array(o); break;
@ -294,6 +300,12 @@ object * deserializer::read_thunk() {
return mk_thunk_from_value(v);
}
object * deserializer::read_task() {
object * v = read_object();
inc(v);
return task_pure(v);
}
object * deserializer::read_array() {
size_t sz = read_size_t();
object * r = alloc_array(sz, sz);
@ -347,6 +359,7 @@ object * deserializer::read_object() {
case object_kind::Constructor: r = read_constructor(); break;
case object_kind::Closure: r = read_closure(); break;
case object_kind::Thunk: r = read_thunk(); break;
case object_kind::Task: r = read_task(); break;
case object_kind::Array: r = read_array(); break;
case object_kind::ScalarArray: r = read_scalar_array(); break;
case object_kind::String: r = read_string_object(); break;

2
src/runtime/serializer.h
View file

@ -24,6 +24,7 @@ class serializer {
void write_constructor(object * o);
void write_closure(object * o);
void write_thunk(object * o);
void write_task(object * o);
void write_array(object * o);
void write_scalar_array(object * o);
void write_string_object(object * o);
@ -64,6 +65,7 @@ class deserializer {
object * read_constructor();
object * read_closure();
object * read_thunk();
object * read_task();
object * read_array();
object * read_scalar_array();
object * read_string_object();