diff options
| -rw-r--r-- | checker/values.ml | 12 | ||||
| -rw-r--r-- | lib/future.ml | 4 |
2 files changed, 12 insertions, 4 deletions
diff --git a/checker/values.ml b/checker/values.ml index eb18bf34b..f8244e06d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 1e607e046b15faeee5912eda83dbb1ba checker/cic.mli +MD5 43e0b61e2a549058ae0a59bbadbb9d61 checker/cic.mli *) @@ -64,6 +64,14 @@ let v_map vk vd = [|[|m; Annot("key",vk); Annot("data",vd); m; Annot("bal",Int)|]|]) in m +(* lib/future *) +let v_computation f = + Annot ("Future.computation", + v_ref + (v_sum "computation" 2 + [| [| Fail "Closure" |]; + [| f ; v_sum "option" 1 [| [| Fail "Val(_,Some _)" |] |] |]; + [| Fail "Exn" |] |])) (** kernel/names *) @@ -186,7 +194,7 @@ let v_cst_type = let v_cst_def = v_sum "constant_def" 0 - [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_computation v_lazy_constr|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; diff --git a/lib/future.ml b/lib/future.ml index b1b960718..9333089fb 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -29,11 +29,11 @@ let _ = Errors.register_handler (function (* Val is not necessarily a final state, so the computation restarts from the state stocked into Val *) type 'a comp = + | Delegated + | Dropped | Closure of (unit -> 'a) | Val of 'a * Dyn.t option | Exn of exn - | Delegated - | Dropped type 'a computation = 'a comp ref |