summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Extract.ml23
-rw-r--r--compiler/InterpreterStatements.ml9
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) *)