diff options
| author | Pierre-Marie Pédrot | 2019-05-20 11:51:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | b245a6c46bc3ef70142e8a165f6cde54265b941e (patch) | |
| tree | f042b65df5510e2a1551c5ffb33b5c1cc64f5d0d /checker/values.ml | |
| parent | ca4b15c2ba733bdff783762bbfc4b53f88014320 (diff) | |
Statically ensure the content of delayed proofs in vio file.
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/checker/values.ml b/checker/values.ml index 5cbf0ff298..4b651cafb6 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||]) let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 let v_unit = v_enum "unit" 1 -let v_ref v = v_tuple "ref" [|v|] let v_set v = let rec s = Sum ("Set.t",1, @@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd) let v_pred v = v_pair v_bool (v_set v) -(* lib/future *) -let v_computation f = - Annot ("Future.computation", - v_ref - (v_sum "Future.comput" 0 - [| [| Fail "Future.ongoing" |]; [| f |] |])) - (** kernel/names *) let v_id = String @@ -391,6 +383,6 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_opaques = Array (v_computation v_constr) +let v_opaques = Array (Opt v_constr) let v_univopaques = - Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) + Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|])) |