diff options
| author | Son Ho | 2024-02-08 13:21:26 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-17 04:53:07 +0100 |
| commit | 72db1ad2eb5835b00c45daa06257e46962000af5 (patch) | |
| tree | d5f3070615122defcb8262a3495e448b0a5d316d /compiler | |
| parent | 91d62c6e73cd67236848c3efa85f85ae152d0d4e (diff) | |
Fix a small issue ollowing updates in Charon
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 0cf8b88a..c17c1563 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -772,9 +772,6 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ^ "\n- trait and method generics:\n" ^ generic_args_to_string ctx (Option.get func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get func.trait_and_method_generic_args in (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -794,6 +791,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in + (* We have to concatenate the generics for the impl + and the generics for the method *) + let generics = + merge_generic_args trait_ref.generics func.generics + in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in @@ -898,6 +900,9 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + (* When instantiating, we need to group the generics for the trait ref + and the method *) + let generics = Option.get func.trait_and_method_generic_args in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies |