diff options
author | Son Ho | 2022-01-05 19:52:07 +0100 |
---|---|---|
committer | Son Ho | 2022-01-05 19:52:07 +0100 |
commit | de4a2300b734e9ea9c29a160a968110507d7747f (patch) | |
tree | 121cd2633d91bc522bdf8dc0385730d00ec4a914 /src/InterpreterUtils.ml | |
parent | 6b9653a3f1a361c72eb841a5a9c04a374b99c8e5 (diff) |
Make progress on eval_non_local_function_call_symbolic
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterUtils.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 66ca8998..edc8594c 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -52,9 +52,15 @@ let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind = | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind) | _ -> failwith "Not a ref type" +let mk_ref_ty (r : 'r) (ty : 'r T.ty) (ref_kind : T.ref_kind) : 'r T.ty = + T.Ref (r, ty, ref_kind) + +(** Make a box type *) +let mk_box_ty (ty : 'r T.ty) : 'r T.ty = T.Adt (T.Assumed T.Box, [], [ ty ]) + (** Box a value *) let mk_box_value (v : V.typed_value) : V.typed_value = - let box_ty = T.Adt (T.Assumed T.Box, [], [ v.V.ty ]) in + let box_ty = mk_box_ty v.V.ty in let box_v = V.Adt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v |