Make progress on Interpreter.ml

2 files changed, 27 insertions, 17 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 63d10894..7e4722b8 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -317,14 +317,17 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id)
       in
       Subst.erase_regions_substitute_types tsubst sg.output
 
-let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
-    =
+let move_return_value (config : C.config) (pop_return_value : bool)
+    (cf : V.typed_value option -> m_fun) : m_fun =
  fun ctx ->
-  let ret_vid = E.VarId.zero in
-  let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
-  cc cf ctx
-
-let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
+  if pop_return_value then
+    let ret_vid = E.VarId.zero in
+    let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
+    cc (fun v ctx -> cf (Some v) ctx) ctx
+  else cf None ctx
+
+let pop_frame (config : C.config) (pop_return_value : bool)
+    (cf : V.typed_value option -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx));
@@ -350,15 +353,18 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
       ^ "]"));
 
   (* Move the return value out of the return variable *)
-  let cc = move_return_value config in
+  let cc = move_return_value config pop_return_value in
   (* Sanity check *)
   let cc =
     comp_check_value cc (fun ret_value ctx ->
-        assert (not (bottom_in_value ctx.ended_regions ret_value)))
+        match ret_value with
+        | None -> ()
+        | Some ret_value ->
+            assert (not (bottom_in_value ctx.ended_regions ret_value)))
   in
 
   (* Drop the outer *loans* we find in the local variables *)
-  let cf_drop_loans_in_locals cf (ret_value : V.typed_value) : m_fun =
+  let cf_drop_loans_in_locals cf (ret_value : V.typed_value option) : m_fun =
     (* Drop the loans *)
     let locals = List.rev locals in
     let cf_drop =
@@ -392,7 +398,7 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
         C.Var (C.DummyBinder vid, v) :: pop env
     | C.Frame :: env -> (* Stop here *) env
   in
-  let cf_pop cf (ret_value : V.typed_value) : m_fun =
+  let cf_pop cf (ret_value : V.typed_value option) : m_fun =
    fun ctx ->
     let env = pop ctx.env in
     let ctx = { ctx with env } in
@@ -403,9 +409,9 @@ let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
 
 (** Pop the current frame and assign the returned value to its destination. *)
 let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
-  let cf_pop = pop_frame config in
+  let cf_pop = pop_frame config true in
   let cf_assign cf ret_value : m_fun =
-    assign_to_place config ret_value dest cf
+    assign_to_place config (Option.get ret_value) dest cf
   in
   comp cf_pop cf_assign
 
@@ -845,8 +851,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
           (* Evaluation successful: evaluate the second statement *)
           | Unit -> eval_statement config st2 cf
           (* Control-flow break: transmit. We enumerate the cases on purpose *)
-          | Panic | Break _ | Continue _ | Return | EndEnterLoop | EndContinue
-            ->
+          | Panic | Break _ | Continue _ | Return | LoopReturn | EndEnterLoop _
+          | EndContinue _ ->
               cf res
         in
         (* Compose and apply *)
@@ -1094,7 +1100,8 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
         (* Pop the stack frame, retrieve the return value, move it to
          * its destination and continue *)
         pop_frame_assign config dest (cf Unit)
-    | Break _ | Continue _ | Unit | EndEnterLoop | EndContinue ->
+    | Break _ | Continue _ | Unit | LoopReturn | EndEnterLoop _ | EndContinue _
+      ->
         raise (Failure "Unreachable")
   in
   let cc = comp cc cf_finish in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 46afa782..789804b1 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -18,8 +18,11 @@ open InterpreterExpressions
     variable, move the return value out of the return variable, remove all the
     local variables (but preserve the abstractions!), remove the {!C.Frame} indicator
     delimiting the current frame and handle the return value to the continuation.
+
+    If the boolean is false, we don't move the return value, and call the
+    continuation with [None].
  *)
-val pop_frame : C.config -> (V.typed_value -> m_fun) -> m_fun
+val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun
 
 (** Instantiate a function signature, introducing **fresh** abstraction ids and
     region ids. This is mostly used in preparation of function calls, when