summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 18:38:53 +0100
committerSon Ho2022-01-05 18:38:53 +0100
commiteb16147150d72642c6dc86ee2427b5378bf3f140 (patch)
tree82be8b97530b2c80a671ca46fdb80e443a62d43f
parentd22f5d1ae5155c53b9cd0daf165dccb5d5563c1f (diff)
Cleanup a bit
-rw-r--r--src/Interpreter.ml26
-rw-r--r--src/Substitute.ml2
2 files changed, 14 insertions, 14 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2192c491..f753206c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -4185,7 +4185,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
A.RegionGroupId.Map.find rg_id asubst_map
in
(* Generate fresh regions and their substitutions *)
- let ctx, fresh_regions, rsubst, _ =
+ let ctx, _, rsubst, _ =
Subst.fresh_regions_with_substs sg.region_params ctx
in
(* Generate the type substitution
@@ -4204,15 +4204,15 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
in
(* Substitute the signature *)
let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
- (* Generate a fresh symbolic value for the result *)
- let res_sv_ty = inst_sg.A.output in
- let ctx, res_spc =
- mk_fresh_symbolic_proj_comp T.RegionId.Set.empty res_sv_ty ctx
+ (* Generate a fresh symbolic value for the return value *)
+ let ret_sv_ty = inst_sg.A.output in
+ let ctx, ret_spc =
+ mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx
in
- let res_value = mk_typed_value_from_proj_comp res_spc in
- let res_av = V.ASymbolic (V.AProjLoans res_spc.V.svalue) in
- let res_av : V.typed_avalue =
- { V.value = res_av; V.ty = res_spc.V.svalue.V.sv_ty }
+ let ret_value = mk_typed_value_from_proj_comp ret_spc in
+ let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in
+ let ret_av : V.typed_avalue =
+ { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty }
in
(* Evaluate the input operands *)
let ctx, args = eval_operands config ctx args in
@@ -4241,7 +4241,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
ctx args_with_rtypes
in
(* Group the input and output values *)
- let avalues = List.append args_projs [ res_av ] in
+ let avalues = List.append args_projs [ ret_av ] in
(* Create the abstraction *)
let abs = { V.abs_id; parents; regions; avalues } in
(* Insert the abstraction in the context *)
@@ -4251,10 +4251,10 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
in
let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in
(* Move the return value to its destination *)
- let ctx = assign_to_place config ctx res_value dest in
+ let ctx = assign_to_place config ctx ret_value dest in
(* Synthesis *)
S.synthesize_local_function_call fid region_params type_params args dest
- res_spc.V.svalue;
+ ret_spc.V.svalue;
(* Return *)
ctx
@@ -4264,8 +4264,6 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
(fid : A.FunDefId.id) (region_params : T.erased_region list)
(type_params : T.ety list) (args : E.operand list) (dest : E.place) :
C.eval_ctx eval_result list =
- (* Retrieve the (correctly instantiated) body *)
- let def = C.ctx_lookup_fun_def ctx fid in
match config.mode with
| ConcreteMode ->
eval_local_function_call_concrete config ctx fid region_params type_params
diff --git a/src/Substitute.ml b/src/Substitute.ml
index dd89025b..d3c3c430 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -39,6 +39,8 @@ let erase_regions (ty : T.rty) : T.ety =
Return the list of new regions and appropriate substitutions from the
original region variables to the fresh regions.
+
+ TODO: simplify? we only need the subst `T.RegionVarId.id -> T.RegionId.id`
*)
let fresh_regions_with_substs (region_vars : T.region_var list)
(ctx : C.eval_ctx) :