diff options
| -rw-r--r-- | compiler/Extract.ml | 23 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 9 |
2 files changed, 21 insertions, 11 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1fb34af0..7da5610e 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1734,7 +1734,9 @@ let extract_trait_self_clause (insert_req_space : unit -> unit) F.pp_print_string fmt "("; let self_clause = ctx_get_trait_self_clause ctx in F.pp_print_string fmt self_clause; + F.pp_print_space fmt (); F.pp_print_string fmt ":"; + F.pp_print_space fmt (); let with_opaque_pre = false in let trait_id = ctx_get_trait_decl with_opaque_pre trait_decl.def_id ctx in F.pp_print_string fmt trait_id; @@ -2648,17 +2650,20 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) (i.e., when we do not use a trait parameter) are desugared to regular function calls. *) - let fun_name = - match fun_id with - | FromLlbc - (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id, rg_id) - -> - assert (lp_id = None); + (match fun_id with + | FromLlbc + (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id, rg_id) -> + assert (lp_id = None); + extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref; + let fun_name = ctx_get_trait_method trait_ref.trait_decl_ref.trait_decl_id method_name rg_id ctx - | _ -> ctx_get_function with_opaque_pre fun_id ctx - in - F.pp_print_string fmt fun_name; + in + F.pp_print_string fmt ("." ^ fun_name) + | _ -> + let fun_name = ctx_get_function with_opaque_pre fun_id ctx in + F.pp_print_string fmt fun_name); + (* Sanity check: HOL4 doesn't support const generics *) assert (generics.const_generics = [] || !backend <> HOL4); (* Print the generics *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 88e20a92..b00aca7e 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1201,7 +1201,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) | A.FunId (A.Assumed _) -> (* Unreachable: must be a transparent function *) raise (Failure "Unreachable") - | A.TraitMethod (trait_ref, method_name, _) -> ( + | A.TraitMethod (trait_ref, method_name, method_decl_id) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call @@ -1230,6 +1230,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) in match method_id with | Some (_, id) -> + (* This is a required method *) let method_def = C.ctx_lookup_fun_decl ctx id in (* Instantiate *) let tr_self = @@ -1239,7 +1240,11 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) instantiate_fun_sig ctx generics tr_self method_def.A.signature in - (call.func, method_def, None, inst_sg) + (* Also update the function identifier: we want to forget + the fact that we called a trait method, and treat it as + a regular function acll. *) + let func = A.FunId (A.Regular method_decl_id) in + (func, method_def, None, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) |