diff options
| author | Son Ho | 2022-11-25 08:13:37 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | 59596561873162d632f3d3091485b32a76427ee9 (patch) | |
| tree | 2bdeb89950981306bacff00a1e8e68b92ec0f9db /compiler/Interpreter.ml | |
| parent | bbdd0da25b974b03d58489d3bbc2654f4f774644 (diff) | |
Start implementing support for loops
Diffstat (limited to '')
| -rw-r--r-- | compiler/Interpreter.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index dc203105..d1241b9d 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -93,7 +93,8 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) in let region_can_end _ = true in let ctx = - create_push_abstractions_from_abs_region_groups call_id V.SynthInput + create_push_abstractions_from_abs_region_groups + (fun rg_id -> V.SynthInput rg_id) inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx in (* Split the variables between return var, inputs and remaining locals *) @@ -151,7 +152,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return (* Insert the return value in the return abstractions (by applying * borrow projections) *) let cf_consume_ret ret_value ctx = - let ret_call_id = C.fresh_fun_call_id () in let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_avalue list = let ctx, avalue = @@ -172,7 +172,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return in assert (region_can_end back_id); let ctx = - create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet + create_push_abstractions_from_abs_region_groups + (fun rg_id -> V.SynthRet rg_id) ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx in |