Implement handling of trait method function calls

1 files changed, 115 insertions, 66 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 3a483b80..5791a359 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -582,8 +582,10 @@ let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
 
 (** Evaluate a non-local function call in concrete mode *)
 let eval_assumed_function_call_concrete (config : C.config)
-    (fid : A.assumed_fun_id) (generics : T.egeneric_args)
-    (args : E.operand list) (dest : E.place) : cm_fun =
+    (fid : A.assumed_fun_id) (call : A.call) : cm_fun =
+  let generics = call.generics in
+  let args = call.args in
+  let dest = call.dest in
   (* Sanity check: we don't fully handle the const generic vars environment
      in concrete mode yet *)
   assert (generics.const_generics = []);
@@ -906,9 +908,16 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      let generics = TypesUtils.mk_empty_generic_args in
-      (eval_transparent_function_call_concrete config global.body_id generics []
-         dest)
+      let call =
+        {
+          A.func = A.FunId (A.Regular global.body_id);
+          generics = TypesUtils.mk_empty_generic_args;
+          trait_and_method_generic_args = None;
+          args = [];
+          dest;
+        }
+      in
+      (eval_transparent_function_call_concrete config global.body_id call)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -1057,18 +1066,38 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
      - this is an assumed function, in which case there is a special treatment
      - this is a trait method
   *)
+  match config.mode with
+  | C.ConcreteMode -> eval_function_call_concrete config call
+  | C.SymbolicMode -> eval_function_call_symbolic config call
+
+and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun
+    =
+ fun cf ctx ->
   match call.func with
   | A.FunId (A.Regular fid) ->
-      eval_transparent_function_call config fid call.generics call.args
-        call.dest
+      eval_transparent_function_call_concrete config fid call cf ctx
   | A.FunId (A.Assumed fid) ->
-      eval_assumed_function_call config fid call.generics call.args call.dest
-  | A.TraitMethod _ -> raise (Failure "Unimplemented")
+      (* Continue - note that we do as if the function call has been successful,
+       * by giving {!Unit} to the continuation, because we place us in the case
+       * where we haven't panicked. Of course, the translation needs to take the
+       * panic case into account... *)
+      eval_assumed_function_call_concrete config fid call (cf Unit) ctx
+  | A.TraitMethod (_, _) -> raise (Failure "Unimplemented")
+
+and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun
+    =
+  match call.func with
+  | A.FunId (A.Regular _) | A.TraitMethod (_, _) ->
+      eval_transparent_function_call_symbolic config call
+  | A.FunId (A.Assumed fid) ->
+      eval_assumed_function_call_symbolic config fid call
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_transparent_function_call_concrete (config : C.config)
-    (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list)
-    (dest : E.place) : st_cm_fun =
+    (fid : A.FunDeclId.id) (call : A.call) : st_cm_fun =
+  let generics = call.A.generics in
+  let args = call.A.args in
+  let dest = call.A.dest in
   (* Sanity check: we don't fully handle the const generic vars environment
      in concrete mode yet *)
   assert (generics.const_generics = []);
@@ -1149,23 +1178,73 @@ and eval_transparent_function_call_concrete (config : C.config)
     cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_transparent_function_call_symbolic (config : C.config)
-    (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list)
-    (dest : E.place) : st_cm_fun =
+and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
+    : st_cm_fun =
  fun cf ctx ->
-  (* Retrieve the (correctly instantiated) signature *)
-  let def = C.ctx_lookup_fun_decl ctx fid in
-  let sg = def.A.signature in
-  (* Instantiate the signature and introduce fresh abstraction and region ids
-   * while doing so *)
-  (* There shouldn't be any reference to Self *)
-  let tr_self = T.UnknownTrait __FUNCTION__ in
-  let inst_sg = instantiate_fun_sig ctx generics tr_self sg in
+  (* Instantiate the signature and introduce fresh abstractions and region ids while doing so *)
+  let def, inst_sg =
+    match call.func with
+    | A.FunId (A.Regular fid) ->
+        let def = C.ctx_lookup_fun_decl ctx fid in
+        let tr_self = T.UnknownTrait __FUNCTION__ in
+        let inst_sg =
+          instantiate_fun_sig ctx call.generics tr_self def.A.signature
+        in
+        (def, inst_sg)
+    | A.FunId (A.Assumed _) ->
+        (* Unreachable: must be a transparent function *)
+        raise (Failure "Unreachable")
+    | A.TraitMethod (trait_ref, method_name) -> (
+        (* When instantiating, we need to group the generics for the trait ref
+           and the method *)
+        let generics = Option.get call.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 *)
+        match trait_ref.trait_id with
+        | TraitImpl impl_id ->
+            (* Lookup the trait impl *)
+            let trait_impl = C.ctx_lookup_trait_impl ctx impl_id in
+            let _, method_id =
+              List.find
+                (fun (s, _) -> s = method_name)
+                trait_impl.required_methods
+            in
+            let method_def = C.ctx_lookup_fun_decl ctx method_id in
+            (* Instantiate *)
+            let tr_self = T.UnknownTrait __FUNCTION__ in
+            let inst_sg =
+              instantiate_fun_sig ctx generics tr_self method_def.A.signature
+            in
+            (method_def, inst_sg)
+        | _ ->
+            (* We are using a local clause - we lookup the trait decl *)
+            let trait_decl =
+              C.ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id
+            in
+            (* Lookup the method decl *)
+            let _, method_id =
+              List.find
+                (fun (s, _) -> s = method_name)
+                trait_decl.required_methods
+            in
+            let method_def = C.ctx_lookup_fun_decl ctx method_id in
+            (* Instantiate *)
+            let tr_self = T.TraitRef trait_ref in
+            let tr_self =
+              TypesUtils.etrait_instance_id_no_regions_to_gr_trait_instance_id
+                tr_self
+            in
+            let inst_sg =
+              instantiate_fun_sig ctx generics tr_self method_def.A.signature
+            in
+            (method_def, inst_sg))
+  in
   (* Sanity check *)
-  assert (List.length args = List.length def.A.signature.inputs);
+  assert (List.length call.args = List.length def.A.signature.inputs);
   (* Evaluate the function call *)
-  eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
-    generics args dest cf ctx
+  eval_function_call_symbolic_from_inst_sig config call.func inst_sg
+    call.generics call.args call.dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1173,9 +1252,12 @@ and eval_transparent_function_call_symbolic (config : C.config)
     calls in symbolic mode: only their signatures matter.
  *)
 and eval_function_call_symbolic_from_inst_sig (config : C.config)
-    (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (generics : T.egeneric_args)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (fid : A.fun_id_or_trait_method_ref) (inst_sg : A.inst_fun_sig)
+    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
+    st_cm_fun =
  fun cf ctx ->
+  (* TODO: trait methods are not supported yet *)
+  let fid = match fid with A.FunId fid -> fid | _ -> raise (Failure "TODO") in
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
   let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
@@ -1304,9 +1386,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
 
 (** Evaluate a non-local function call in symbolic mode *)
 and eval_assumed_function_call_symbolic (config : C.config)
-    (fid : A.assumed_fun_id) (generics : T.egeneric_args)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (fid : A.assumed_fun_id) (call : A.call) : st_cm_fun =
  fun cf ctx ->
+  let generics = call.generics in
+  let args = call.args in
+  let dest = call.dest in
   (* Sanity check: make sure the type parameters don't contain regions -
    * this is a current limitation of our synthesis *)
   assert (
@@ -1342,43 +1426,8 @@ and eval_assumed_function_call_symbolic (config : C.config)
       in
 
       (* Evaluate the function call *)
-      eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
-        generics args dest cf ctx
-
-(** Evaluate a non-local (i.e, assumed) function call such as [Box::deref]
-    (auxiliary helper for [eval_statement]) *)
-and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id)
-    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
- fun cf ctx ->
-  (* Debug *)
-  log#ldebug
-    (lazy
-      (let generics = PCtx.egeneric_args_to_string ctx generics in
-       let args =
-         "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]"
-       in
-       let dest = place_to_string ctx dest in
-       "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
-       ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest));
-
-  match config.mode with
-  | C.ConcreteMode ->
-      eval_assumed_function_call_concrete config fid generics args dest
-        (cf Unit) ctx
-  | C.SymbolicMode ->
-      eval_assumed_function_call_symbolic config fid generics args dest cf ctx
-
-(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
-    [eval_statement]) *)
-and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id)
-    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
-  match config.mode with
-  | ConcreteMode ->
-      eval_transparent_function_call_concrete config fid generics args dest
-  | SymbolicMode ->
-      eval_transparent_function_call_symbolic config fid generics args dest
+      eval_function_call_symbolic_from_inst_sig config (A.FunId (A.Assumed fid))
+        inst_sig generics args dest cf ctx
 
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =