diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 0b444862..45b2cce8 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -69,6 +69,17 @@ let mk_box_value (v : V.typed_value) : V.typed_value = let box_v = V.Adt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v +(** Create a fresh symbolic value (as a complementary projector) *) +let mk_fresh_symbolic_comp_proj (ended_regions : T.RegionId.set_t) (ty : T.rty) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + let ctx, sv_id = C.fresh_symbolic_value_id ctx in + let svalue = { V.sv_id; V.sv_ty = ty } in + let sv = { V.svalue; rset_ended = ended_regions } in + let value : V.value = V.Symbolic sv in + let ty : T.ety = Subst.erase_regions ty in + let sv : V.typed_value = { V.value; ty } in + (ctx, sv) + (** TODO: change the name *) type eval_error = Panic @@ -2667,14 +2678,7 @@ let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) (* Generate the field values *) let ctx, fields = List.fold_left_map - (fun ctx sv_ty -> - let ctx, sv_id = C.fresh_symbolic_value_id ctx in - let svalue = { V.sv_id; V.sv_ty } in - let sv = { V.svalue; rset_ended = ended_regions } in - let value : V.value = V.Symbolic sv in - let ty : T.ety = Subst.erase_regions sv_ty in - let sv : V.typed_value = { V.value; ty } in - (ctx, sv)) + (fun ctx sv_ty -> mk_fresh_symbolic_comp_proj ended_regions sv_ty ctx) ctx field_types in let v = V.Adt { variant_id = None; field_values = fields } in @@ -2685,12 +2689,8 @@ let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = (* Introduce a fresh symbolic value *) - let ctx, boxed_sv_id = C.fresh_symbolic_value_id ctx in - let boxed_sv = { V.sv_id = boxed_sv_id; V.sv_ty = boxed_ty } in - let boxed_sv = { V.svalue = boxed_sv; rset_ended = ended_regions } in - let boxed_value = V.Symbolic boxed_sv in - let boxed_value : V.typed_value = - { V.value = boxed_value; V.ty = Subst.erase_regions boxed_ty } + let ctx, boxed_value = + mk_fresh_symbolic_comp_proj ended_regions boxed_ty ctx in let box_value = mk_box_value boxed_value in (ctx, box_value) |