diff options
| author | Son HO | 2023-12-05 16:47:51 +0100 |
|---|---|---|
| committer | GitHub | 2023-12-05 16:47:51 +0100 |
| commit | 4795e5f823bc89504855d8eb946b111d9314f4d5 (patch) | |
| tree | 4c35c707e74c14ad7a554147cff20b2e17c28659 /compiler/InterpreterUtils.ml | |
| parent | 789ba1473acd287814a0d659b5f5a0e480e4e9d7 (diff) | |
| parent | a212ab42927e0f9ffa3ed0dfa0140b231e725008 (diff) | |
Merge pull request #48 from AeneasVerif/son_closures
Prepare support for function pointers and closures
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterUtils.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index bba88e9f..d3f8f4fa 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -273,8 +273,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx) raise Found else () | SynthInput | SynthInputGivenBack | FunCallGivenBack - | SynthRetGivenBack | Global | LoopGivenBack | Aggregate | ConstGeneric - | TraitConst -> + | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack + | Aggregate | ConstGeneric | TraitConst -> () end in @@ -455,7 +455,7 @@ let initialize_eval_context (ctx : decls_ctx) *) let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args) (tr_self : trait_instance_id) (sg : fun_sig) - (regions_hierarchy : region_groups) : inst_fun_sig = + (regions_hierarchy : region_var_groups) : inst_fun_sig = log#ldebug (lazy ("instantiate_fun_sig:" ^ "\n- generics: " @@ -484,7 +484,11 @@ let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args) RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = Substitute.fresh_regions_with_substs sg.generics.regions in + let _, rsubst, _ = + Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true + sg.generics.regions + in + let rsubst r = Option.get (rsubst r) in (* Generate the type substitution Note that for now we don't support instantiating the type parameters with types containing regions. *) |