Update the interpreter so that it is not written in CPS style (#120)

* Start turning the compiler in a style which is less CPS

* Update a function in InterpreterExpressions.ml

* WIP work on cps

* WIP

* WIP, currently on InterpreterStatements.ml

* WIP

* Finished CPS-related modification

* Fixed some warning related to documentation comments

* Finished loop support, fixed a loop

* fixed a typed value

* Fixed check_disappeared related error

* cleaned check_disappeared related error

* Start cleaning up

* Do more cleanup

* Make some cleanup and fix an issue

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Rename a function

* Do more cleanup

* Cleanup the loops code and fix some bugs

* Cleanup assign_to_place

* Make a minor cleanup

---------

Co-authored-by: Son Ho <hosonmarc@gmail.com>

2 files changed, 652 insertions, 638 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 9ad6487b..66677eff 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -20,7 +20,7 @@ let log = L.statements_log
 
 (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
 let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   log#ldebug
     (lazy
       ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
@@ -29,11 +29,11 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
   let access = Write in
   (* First make sure we can access the place, by ending loans or expanding
    * symbolic values along the path, for instance *)
-  let cc = update_ctx_along_read_place config meta access p in
+  let ctx, cc = update_ctx_along_read_place config meta access p ctx in
   (* Prepare the place (by ending the outer loans *at* the place). *)
-  let cc = comp cc (prepare_lplace config meta p) in
+  let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in
   (* Replace the value with {!Bottom} *)
-  let replace cf (v : typed_value) ctx =
+  let ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows it may contain *)
     let mv = InterpreterPaths.read_place meta access p ctx in
@@ -46,47 +46,41 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
       (lazy
         ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
         ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-    cf ctx
+    ctx
   in
   (* Compose and apply *)
-  comp cc replace cf ctx
+  (ctx, cc)
 
 (** Push a dummy variable to the environment *)
-let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun =
- fun cf ctx ->
-  let ctx = ctx_push_dummy_var ctx vid v in
-  cf ctx
+let push_dummy_var (vid : DummyVarId.id) (v : typed_value) (ctx : eval_ctx) :
+    eval_ctx =
+  ctx_push_dummy_var ctx vid v
 
 (** Remove a dummy variable from the environment *)
-let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id)
-    (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) (ctx : eval_ctx) :
+    typed_value * eval_ctx =
   let ctx, v = ctx_remove_dummy_var meta ctx vid in
-  cf v ctx
+  (v, ctx)
 
 (** Push an uninitialized variable to the environment *)
-let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun =
- fun cf ctx ->
-  let ctx = ctx_push_uninitialized_var meta ctx var in
-  cf ctx
+let push_uninitialized_var (meta : Meta.meta) (var : var) (ctx : eval_ctx) :
+    eval_ctx =
+  ctx_push_uninitialized_var meta ctx var
 
 (** Push a list of uninitialized variables to the environment *)
-let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun =
- fun cf ctx ->
-  let ctx = ctx_push_uninitialized_vars meta ctx vars in
-  cf ctx
+let push_uninitialized_vars (meta : Meta.meta) (vars : var list)
+    (ctx : eval_ctx) : eval_ctx =
+  ctx_push_uninitialized_vars meta ctx vars
 
 (** Push a variable to the environment *)
-let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun =
- fun cf ctx ->
-  let ctx = ctx_push_var meta ctx var v in
-  cf ctx
+let push_var (meta : Meta.meta) (var : var) (v : typed_value) (ctx : eval_ctx) :
+    eval_ctx =
+  ctx_push_var meta ctx var v
 
 (** Push a list of variables to the environment *)
-let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun =
- fun cf ctx ->
-  let ctx = ctx_push_vars meta ctx vars in
-  cf ctx
+let push_vars (meta : Meta.meta) (vars : (var * typed_value) list)
+    (ctx : eval_ctx) : eval_ctx =
+  ctx_push_vars meta ctx vars
 
 (** Assign a value to a given place.
 
@@ -97,7 +91,7 @@ let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun =
  *)
 let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value)
     (p : place) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   log#ldebug
     (lazy
       ("assign_to_place:" ^ "\n- rv: "
@@ -106,58 +100,51 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value)
       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Push the rvalue to a dummy variable, for bookkeeping *)
   let rvalue_vid = fresh_dummy_var_id () in
-  let cc = push_dummy_var rvalue_vid rv in
+  let ctx = push_dummy_var rvalue_vid rv ctx in
   (* Prepare the destination *)
-  let cc = comp cc (prepare_lplace config meta p) in
+  let _, ctx, cc = prepare_lplace config meta p ctx in
   (* Retrieve the rvalue from the dummy variable *)
-  let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in
+  let rv, ctx = remove_dummy_var meta rvalue_vid ctx in
+  (* Move the value at destination (that we will overwrite) to a dummy variable
+     to preserve the borrows *)
+  let mv = InterpreterPaths.read_place meta Write p ctx in
+  let dest_vid = fresh_dummy_var_id () in
+  let ctx = ctx_push_dummy_var ctx dest_vid mv in
+  (* Write to the destination *)
+  (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
+  exec_assert __FILE__ __LINE__
+    (not (bottom_in_value ctx.ended_regions rv))
+    meta "The value to move contains bottom";
   (* Update the destination *)
-  let move_dest cf (rv : typed_value) : m_fun =
-   fun ctx ->
-    (* Move the value at destination (that we will overwrite) to a dummy variable
-     * to preserve the borrows *)
-    let mv = InterpreterPaths.read_place meta Write p ctx in
-    let dest_vid = fresh_dummy_var_id () in
-    let ctx = ctx_push_dummy_var ctx dest_vid mv in
-    (* Write to the destination *)
-    (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
-    exec_assert __FILE__ __LINE__
-      (not (bottom_in_value ctx.ended_regions rv))
-      meta "The value to move contains bottom";
-    (* Update the destination *)
-    let ctx = write_place meta Write p rv ctx in
-    (* Debug *)
-    log#ldebug
-      (lazy
-        ("assign_to_place:" ^ "\n- rv: "
-        ^ typed_value_to_string ~meta:(Some meta) ctx rv
-        ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n"
-        ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-    (* Continue *)
-    cf ctx
-  in
-  (* Compose and apply *)
-  comp cc move_dest cf ctx
+  let ctx = write_place meta Write p rv ctx in
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("assign_to_place:" ^ "\n- rv: "
+      ^ typed_value_to_string ~meta:(Some meta) ctx rv
+      ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+  (* Return *)
+  (ctx, cc)
 
 (** Evaluate an assertion, when the scrutinee is not symbolic *)
 let eval_assertion_concrete (config : config) (meta : Meta.meta)
     (assertion : assertion) : st_cm_fun =
- fun cf ctx ->
+ fun ctx ->
   (* There won't be any symbolic expansions: fully evaluate the operand *)
-  let eval_op = eval_operand config meta assertion.cond in
-  let eval_assert cf (v : typed_value) : m_fun =
-   fun ctx ->
+  let v, ctx, eval_op = eval_operand config meta assertion.cond ctx in
+  let st =
     match v.value with
     | VLiteral (VBool b) ->
         (* Branch *)
-        if b = assertion.expected then cf Unit ctx else cf Panic ctx
+        if b = assertion.expected then Unit else Panic
     | _ ->
         craise __FILE__ __LINE__ meta
           ("Expected a boolean, got: "
           ^ typed_value_to_string ~meta:(Some meta) ctx v)
   in
   (* Compose and apply *)
-  comp eval_op eval_assert cf ctx
+  ((ctx, st), eval_op)
 
 (** Evaluates an assertion.
     
@@ -167,13 +154,12 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta)
  *)
 let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
     : st_cm_fun =
- fun cf ctx ->
+ fun ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand config meta assertion.cond in
+  let v, ctx, cf_eval_op = eval_operand config meta assertion.cond ctx in
   (* Evaluate the assertion *)
-  let eval_assert cf (v : typed_value) : m_fun =
-   fun ctx ->
-    sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta;
+  sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta;
+  let st, cf_eval_assert =
     (* We make a choice here: we could completely decouple the concrete and
      * symbolic executions here but choose not to. In the case where we
      * know the concrete value of the boolean we test, we use this value
@@ -182,7 +168,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
     match v.value with
     | VLiteral (VBool _) ->
         (* Delegate to the concrete evaluation function *)
-        eval_assertion_concrete config meta assertion cf ctx
+        eval_assertion_concrete config meta assertion ctx
     | VSymbolic sv ->
         sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta;
         sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) meta;
@@ -191,20 +177,18 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
          * We will of course synthesize an assertion in the generated code
          * (see below). *)
         let ctx =
-          apply_symbolic_expansion_non_borrow config meta sv
-            (SeLiteral (VBool true)) ctx
+          apply_symbolic_expansion_non_borrow config meta sv ctx
+            (SeLiteral (VBool true))
         in
-        (* Continue *)
-        let expr = cf Unit ctx in
         (* Add the synthesized assertion *)
-        S.synthesize_assertion ctx v expr
+        ((ctx, Unit), S.synthesize_assertion ctx v)
     | _ ->
         craise __FILE__ __LINE__ meta
           ("Expected a boolean, got: "
           ^ typed_value_to_string ~meta:(Some meta) ctx v)
   in
   (* Compose and apply *)
-  comp eval_op eval_assert cf ctx
+  (st, cc_comp cf_eval_op cf_eval_assert)
 
 (** Updates the discriminant of a value at a given place.
 
@@ -219,7 +203,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
  *)
 let set_discriminant (config : config) (meta : Meta.meta) (p : place)
     (variant_id : VariantId.id) : st_cm_fun =
- fun cf ctx ->
+ fun ctx ->
   log#ldebug
     (lazy
       ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p
@@ -229,69 +213,67 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place)
       ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Access the value *)
   let access = Write in
-  let cc = update_ctx_along_read_place config meta access p in
-  let cc = comp cc (prepare_lplace config meta p) in
+  let ctx, cc = update_ctx_along_read_place config meta access p ctx in
+  let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in
   (* Update the value *)
-  let update_value cf (v : typed_value) : m_fun =
-   fun ctx ->
-    match (v.ty, v.value) with
-    | TAdt ((TAdtId _ as type_id), generics), VAdt av -> (
-        (* There are two situations:
-           - either the discriminant is already the proper one (in which case we
-             don't do anything)
-           - or it is not the proper one, in which case we replace the value with
-             a variant with all its fields set to {!Bottom}
-        *)
-        match av.variant_id with
-        | None ->
-            craise __FILE__ __LINE__ meta
-              "Found a struct value while expected an enum"
-        | Some variant_id' ->
-            if variant_id' = variant_id then (* Nothing to do *)
-              cf Unit ctx
-            else
-              (* Replace the value *)
-              let bottom_v =
-                match type_id with
-                | TAdtId def_id ->
-                    compute_expanded_bottom_adt_value meta ctx def_id
-                      (Some variant_id) generics
-                | _ -> craise __FILE__ __LINE__ meta "Unreachable"
-              in
-              assign_to_place config meta bottom_v p (cf Unit) ctx)
-    | TAdt ((TAdtId _ as type_id), generics), VBottom ->
-        let bottom_v =
-          match type_id with
-          | TAdtId def_id ->
-              compute_expanded_bottom_adt_value meta ctx def_id
-                (Some variant_id) generics
-          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
-        in
-        assign_to_place config meta bottom_v p (cf Unit) ctx
-    | _, VSymbolic _ ->
-        sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta;
-        (* This is a bit annoying: in theory we should expand the symbolic value
-         * then set the discriminant, because in the case the discriminant is
-         * exactly the one we set, the fields are left untouched, and in the
-         * other cases they are set to Bottom.
-         * For now, we forbid setting the discriminant of a symbolic value:
-         * setting a discriminant should only be used to initialize a value,
-         * or reset an already initialized value, really. *)
-        craise __FILE__ __LINE__ meta "Unexpected value"
-    | _, (VAdt _ | VBottom) ->
-        craise __FILE__ __LINE__ meta "Inconsistent state"
-    | _, (VLiteral _ | VBorrow _ | VLoan _) ->
-        craise __FILE__ __LINE__ meta "Unexpected value"
-  in
-  (* Compose and apply *)
-  comp cc update_value cf ctx
+  match (v.ty, v.value) with
+  | TAdt ((TAdtId _ as type_id), generics), VAdt av -> (
+      (* There are two situations:
+         - either the discriminant is already the proper one (in which case we
+           don't do anything)
+         - or it is not the proper one, in which case we replace the value with
+           a variant with all its fields set to {!Bottom}
+      *)
+      match av.variant_id with
+      | None ->
+          craise __FILE__ __LINE__ meta
+            "Found a struct value while expecting an enum"
+      | Some variant_id' ->
+          if variant_id' = variant_id then (* Nothing to do *)
+            ((ctx, Unit), cc)
+          else
+            (* Replace the value *)
+            let bottom_v =
+              match type_id with
+              | TAdtId def_id ->
+                  compute_expanded_bottom_adt_value meta ctx def_id
+                    (Some variant_id) generics
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+            in
+            let ctx, cc =
+              comp cc (assign_to_place config meta bottom_v p ctx)
+            in
+            ((ctx, Unit), cc))
+  | TAdt ((TAdtId _ as type_id), generics), VBottom ->
+      let bottom_v =
+        match type_id with
+        | TAdtId def_id ->
+            compute_expanded_bottom_adt_value meta ctx def_id (Some variant_id)
+              generics
+        | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+      in
+      let ctx, cc = comp cc (assign_to_place config meta bottom_v p ctx) in
+      ((ctx, Unit), cc)
+  | _, VSymbolic _ ->
+      sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta;
+      (* This is a bit annoying: in theory we should expand the symbolic value
+       * then set the discriminant, because in the case the discriminant is
+       * exactly the one we set, the fields are left untouched, and in the
+       * other cases they are set to Bottom.
+       * For now, we forbid setting the discriminant of a symbolic value:
+       * setting a discriminant should only be used to initialize a value,
+       * or reset an already initialized value, really. *)
+      craise __FILE__ __LINE__ meta "Unexpected value"
+  | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ meta "Inconsistent state"
+  | _, (VLiteral _ | VBorrow _ | VLoan _) ->
+      craise __FILE__ __LINE__ meta "Unexpected value"
 
 (** Push a frame delimiter in the context's environment *)
 let ctx_push_frame (ctx : eval_ctx) : eval_ctx =
   { ctx with env = EFrame :: ctx.env }
 
 (** Push a frame delimiter in the context's environment *)
-let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
+let push_frame (ctx : eval_ctx) : eval_ctx = ctx_push_frame ctx
 
 (** Small helper: compute the type of the return value for a specific
     instantiation of an assumed function.
@@ -323,17 +305,19 @@ let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx)
       AssociatedTypes.ctx_normalize_erase_ty meta ctx ty
 
 let move_return_value (config : config) (meta : Meta.meta)
-    (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun =
- fun ctx ->
+    (pop_return_value : bool) (ctx : eval_ctx) :
+    typed_value option * eval_ctx * (eval_result -> eval_result) =
   if pop_return_value then
     let ret_vid = VarId.zero in
-    let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in
-    cc (fun v ctx -> cf (Some v) ctx) ctx
-  else cf None ctx
+    let v, ctx, cc =
+      eval_operand config meta (Move (mk_place_from_var_id ret_vid)) ctx
+    in
+    (Some v, ctx, cc)
+  else (None, ctx, fun e -> e)
 
 let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
-    (cf : typed_value option -> m_fun) : m_fun =
- fun ctx ->
+    (ctx : eval_ctx) :
+    typed_value option * eval_ctx * (eval_result -> eval_result) =
   (* Debug *)
   log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
@@ -358,40 +342,31 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
       ^ "]"));
 
   (* Move the return value out of the return variable *)
-  let cc = move_return_value config meta pop_return_value in
-  (* Sanity check *)
-  let cc =
-    comp_check_value cc (fun ret_value ctx ->
-        match ret_value with
-        | None -> ()
-        | Some ret_value ->
-            sanity_check __FILE__ __LINE__
-              (not (bottom_in_value ctx.ended_regions ret_value))
-              meta)
+  let v, ctx, cc = move_return_value config meta pop_return_value ctx in
+  let _ =
+    match v with
+    | None -> ()
+    | Some ret_value ->
+        sanity_check __FILE__ __LINE__
+          (not (bottom_in_value ctx.ended_regions ret_value))
+          meta
   in
 
   (* Drop the outer *loans* we find in the local variables *)
-  let cf_drop_loans_in_locals cf (ret_value : typed_value option) : m_fun =
-    (* Drop the loans *)
-    let locals = List.rev locals in
-    let cf_drop =
-      List.fold_left
-        (fun cf lid ->
-          drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf)
-        (cf ret_value) locals
-    in
-    (* Apply *)
-    cf_drop
+  let ctx, cc =
+    comp cc
+      ((* Drop the loans *)
+       let locals = List.rev locals in
+       fold_left_apply_continuation
+         (fun lid ctx ->
+           drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) ctx)
+         locals ctx)
   in
-  let cc = comp cc cf_drop_loans_in_locals in
   (* Debug *)
-  let cc =
-    comp_check_value cc (fun _ ctx ->
-        log#ldebug
-          (lazy
-            ("pop_frame: after dropping outer loans in local variables:\n"
-            ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
-  in
+  log#ldebug
+    (lazy
+      ("pop_frame: after dropping outer loans in local variables:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
   (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all
    * the local variables (which may still contain borrow permissions - but
@@ -405,28 +380,22 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
         EBinding (BDummy vid, v) :: pop env
     | EFrame :: env -> (* Stop here *) env
   in
-  let cf_pop cf (ret_value : typed_value option) : m_fun =
-   fun ctx ->
-    let env = pop ctx.env in
-    let ctx = { ctx with env } in
-    cf ret_value ctx
-  in
-  (* Compose and apply *)
-  comp cc cf_pop cf ctx
+  let env = pop ctx.env in
+  let ctx = { ctx with env } in
+  (* Return *)
+  (v, ctx, cc)
 
 (** Pop the current frame and assign the returned value to its destination. *)
 let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) :
     cm_fun =
-  let cf_pop = pop_frame config meta true in
-  let cf_assign cf ret_value : m_fun =
-    assign_to_place config meta (Option.get ret_value) dest cf
-  in
-  comp cf_pop cf_assign
+ fun ctx ->
+  let v, ctx, cc = pop_frame config meta true ctx in
+  comp cc (assign_to_place config meta (Option.get v) dest ctx)
 
 (** Auxiliary function - see {!eval_assumed_function_call} *)
 let eval_box_new_concrete (config : config) (meta : Meta.meta)
     (generics : generic_args) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   (* Check and retrieve the arguments *)
   match
     (generics.regions, generics.types, generics.const_generics, ctx.env)
@@ -443,30 +412,22 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta)
         meta "The input given to Box::new doesn't have the proper type";
 
       (* Move the input value *)
-      let cf_move =
-        eval_operand config meta (Move (mk_place_from_var_id input_var.index))
+      let v, ctx, cc =
+        eval_operand config meta
+          (Move (mk_place_from_var_id input_var.index))
+          ctx
       in
 
       (* Create the new box *)
-      let cf_create cf (moved_input_value : typed_value) : m_fun =
-        (* Create the box value *)
-        let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in
-        let box_ty = TAdt (TAssumed TBox, generics) in
-        let box_v =
-          VAdt { variant_id = None; field_values = [ moved_input_value ] }
-        in
-        let box_v = mk_typed_value meta box_ty box_v in
-
-        (* Move this value to the return variable *)
-        let dest = mk_place_from_var_id VarId.zero in
-        let cf_assign = assign_to_place config meta box_v dest in
-
-        (* Continue *)
-        cf_assign cf
-      in
-
-      (* Compose and apply *)
-      comp cf_move cf_create cf ctx
+      (* Create the box value *)
+      let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in
+      let box_ty = TAdt (TAssumed TBox, generics) in
+      let box_v = VAdt { variant_id = None; field_values = [ v ] } in
+      let box_v = mk_typed_value meta box_ty box_v in
+
+      (* Move this value to the return variable *)
+      let dest = mk_place_from_var_id VarId.zero in
+      comp cc (assign_to_place config meta box_v dest ctx)
   | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
 
 (** Auxiliary function - see {!eval_assumed_function_call}.
@@ -490,7 +451,7 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta)
 *)
 let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args)
     (args : operand list) (dest : place) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   match (generics.regions, generics.types, generics.const_generics, args) with
   | [], [ boxed_ty ], [], [ Move input_box_place ] ->
       (* Required type checking *)
@@ -502,18 +463,16 @@ let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args)
         meta;
 
       (* Drop the value *)
-      let cc = drop_value config meta input_box_place in
+      let ctx, cc = drop_value config meta input_box_place ctx in
 
       (* Update the destination by setting it to [()] *)
-      let cc = comp cc (assign_to_place config meta mk_unit_value dest) in
-
-      (* Continue *)
-      cc cf ctx
+      comp cc (assign_to_place config meta mk_unit_value dest ctx)
   | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
 
 (** Evaluate a non-local function call in concrete mode *)
 let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta)
     (fid : assumed_fun_id) (call : call) : cm_fun =
+ fun ctx ->
   let args = call.args in
   let dest = call.dest in
   match call.func with
@@ -533,12 +492,12 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta)
       match fid with
       | BoxFree ->
           (* Degenerate case: box_free *)
-          eval_box_free config meta generics args dest
+          eval_box_free config meta generics args dest ctx
       | _ ->
           (* "Normal" case: not box_free *)
           (* Evaluate the operands *)
           (*      let ctx, args_vl = eval_operands config ctx args in *)
-          let cf_eval_ops = eval_operands config meta args in
+          let args_vl, ctx, cc = eval_operands config meta args ctx in
 
           (* Evaluate the call
            *
@@ -547,53 +506,42 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta)
            * below, without having to introduce an intermediary function call,
            * but it made it less clear where the computed values came from,
            * so we reversed the modifications. *)
-          let cf_eval_call cf (args_vl : typed_value list) : m_fun =
-           fun ctx ->
-            (* Push the stack frame: we initialize the frame with the return variable,
-               and one variable per input argument *)
-            let cc = push_frame in
-
-            (* Create and push the return variable *)
-            let ret_vid = VarId.zero in
-            let ret_ty =
-              get_assumed_function_return_type meta ctx fid generics
-            in
-            let ret_var = mk_var ret_vid (Some "@return") ret_ty in
-            let cc = comp cc (push_uninitialized_var meta ret_var) in
-
-            (* Create and push the input variables *)
-            let input_vars =
-              VarId.mapi_from1
-                (fun id (v : typed_value) -> (mk_var id None v.ty, v))
-                args_vl
-            in
-            let cc = comp cc (push_vars meta input_vars) in
-
-            (* "Execute" the function body. As the functions are assumed, here we call
-             * custom functions to perform the proper manipulations: we don't have
-             * access to a body. *)
-            let cf_eval_body : cm_fun =
-              match fid with
-              | BoxNew -> eval_box_new_concrete config meta generics
-              | BoxFree ->
-                  (* Should have been treated above *)
-                  craise __FILE__ __LINE__ meta "Unreachable"
-              | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
-              | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
-                ->
-                  craise __FILE__ __LINE__ meta "Unimplemented"
-            in
-
-            let cc = comp cc cf_eval_body in
-
-            (* Pop the frame *)
-            let cc = comp cc (pop_frame_assign config meta dest) in
-
-            (* Continue *)
-            cc cf ctx
+          (* Push the stack frame: we initialize the frame with the return variable,
+             and one variable per input argument *)
+          let ctx = push_frame ctx in
+
+          (* Create and push the return variable *)
+          let ret_vid = VarId.zero in
+          let ret_ty = get_assumed_function_return_type meta ctx fid generics in
+          let ret_var = mk_var ret_vid (Some "@return") ret_ty in
+          let ctx = push_uninitialized_var meta ret_var ctx in
+
+          (* Create and push the input variables *)
+          let input_vars =
+            VarId.mapi_from1
+              (fun id (v : typed_value) -> (mk_var id None v.ty, v))
+              args_vl
           in
-          (* Compose and apply *)
-          comp cf_eval_ops cf_eval_call)
+          let ctx = push_vars meta input_vars ctx in
+
+          (* "Execute" the function body. As the functions are assumed, here we call
+           * custom functions to perform the proper manipulations: we don't have
+           * access to a body. *)
+          let ctx, cf_eval_body =
+            match fid with
+            | BoxNew -> eval_box_new_concrete config meta generics ctx
+            | BoxFree ->
+                (* Should have been treated above *)
+                craise __FILE__ __LINE__ meta "Unreachable"
+            | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
+            | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
+              ->
+                craise __FILE__ __LINE__ meta "Unimplemented"
+          in
+          let cc = cc_comp cc cf_eval_body in
+
+          (* Pop the frame *)
+          comp cc (pop_frame_assign config meta dest ctx))
 
 (** Helper
  
@@ -947,8 +895,8 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta)
                 inst_sg )))
 
 (** Evaluate a statement *)
-let rec eval_statement (config : config) (st : statement) : st_cm_fun =
- fun cf ctx ->
+let rec eval_statement (config : config) (st : statement) : stl_cm_fun =
+ fun ctx ->
   (* Debugging *)
   log#ldebug
     (lazy
@@ -959,16 +907,15 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
       ^ "\n\n"));
 
   (* Take a snapshot of the current context for the purpose of generating pretty names *)
-  let cc = S.cf_save_snapshot in
+  let cc = S.save_snapshot ctx in
   (* Expand the symbolic values if necessary - we need to do that before
-   * checking the invariants *)
-  let cc = comp cc (greedy_expand_symbolic_values config st.meta) in
+     checking the invariants *)
+  let ctx, cc = comp cc (greedy_expand_symbolic_values config st.meta ctx) in
   (* Sanity check *)
-  let cc = comp cc (Invariants.cf_check_invariants st.meta) in
+  Invariants.check_invariants st.meta ctx;
 
   (* Evaluate *)
-  let cf_eval_st cf : m_fun =
-   fun ctx ->
+  let stl, cf_eval_st =
     log#ldebug
       (lazy
         ("\neval_statement: cf_eval_st: statement:\n"
@@ -980,96 +927,118 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
         match rvalue with
         | Global (gid, generics) ->
             (* Evaluate the global *)
-            eval_global config p gid generics cf ctx
+            eval_global config st.meta p gid generics ctx
         | _ ->
             (* Evaluate the rvalue *)
-            let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in
+            let res, ctx, cc =
+              eval_rvalue_not_global config st.meta rvalue ctx
+            in
             (* Assign *)
-            let cf_assign cf (res : (typed_value, eval_error) result) ctx =
-              log#ldebug
-                (lazy
-                  ("about to assign to place: " ^ place_to_string ctx p
-                 ^ "\n- Context:\n"
-                  ^ eval_ctx_to_string ~meta:(Some st.meta) ctx));
+            log#ldebug
+              (lazy
+                ("about to assign to place: " ^ place_to_string ctx p
+               ^ "\n- Context:\n"
+                ^ eval_ctx_to_string ~meta:(Some st.meta) ctx));
+            let (ctx, res), cf_assign =
               match res with
-              | Error EPanic -> cf Panic ctx
-              | Ok rv -> (
-                  let expr =
-                    assign_to_place config st.meta rv p (cf Unit) ctx
-                  in
-                  (* Update the synthesized AST - here we store meta-information.
+              | Error EPanic -> ((ctx, Panic), fun e -> e)
+              | Ok rv ->
+                  (* Update the synthesized AST - here we store additional meta-information.
                    * We do it only in specific cases (it is not always useful, and
                    * also it can lead to issues - for instance, if we borrow a
                    * reserved borrow, we later can't translate it to pure values...) *)
-                  match rvalue with
-                  | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable"
-                  | Use _
-                  | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
-                  | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ ->
-                      let rp = rvalue_get_place rvalue in
-                      let rp =
-                        match rp with
-                        | Some rp -> Some (S.mk_mplace st.meta rp ctx)
-                        | None -> None
-                      in
-                      S.synthesize_assignment ctx
-                        (S.mk_mplace st.meta p ctx)
-                        rv rp expr)
+                  let cc =
+                    match rvalue with
+                    | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable"
+                    | Use _
+                    | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
+                    | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ ->
+                        let rp = rvalue_get_place rvalue in
+                        let rp =
+                          match rp with
+                          | Some rp -> Some (S.mk_mplace st.meta rp ctx)
+                          | None -> None
+                        in
+                        S.synthesize_assignment ctx
+                          (S.mk_mplace st.meta p ctx)
+                          rv rp
+                  in
+                  let ctx, cc =
+                    comp cc (assign_to_place config st.meta rv p ctx)
+                  in
+                  ((ctx, Unit), cc)
             in
-
+            let cc = cc_comp cc cf_assign in
             (* Compose and apply *)
-            comp cf_eval_rvalue cf_assign cf ctx)
-    | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx
+            ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc))
+    | FakeRead p ->
+        let ctx, cc = eval_fake_read config st.meta p ctx in
+        ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc)
     | SetDiscriminant (p, variant_id) ->
-        set_discriminant config st.meta p variant_id cf ctx
-    | Drop p -> drop_value config st.meta p (cf Unit) ctx
-    | Assert assertion -> eval_assertion config st.meta assertion cf ctx
-    | Call call -> eval_function_call config st.meta call cf ctx
-    | Panic -> cf Panic ctx
-    | Return -> cf Return ctx
-    | Break i -> cf (Break i) ctx
-    | Continue i -> cf (Continue i) ctx
-    | Nop -> cf Unit ctx
+        let (ctx, res), cc = set_discriminant config st.meta p variant_id ctx in
+        ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Drop p ->
+        let ctx, cc = drop_value config st.meta p ctx in
+        ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Assert assertion ->
+        let (ctx, res), cc = eval_assertion config st.meta assertion ctx in
+        ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Call call -> eval_function_call config st.meta call ctx
+    | Panic -> ([ (ctx, Panic) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Return -> ([ (ctx, Return) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Break i -> ([ (ctx, Break i) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Continue i ->
+        ([ (ctx, Continue i) ], cc_singleton __FILE__ __LINE__ st.meta cc)
+    | Nop -> ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc)
     | Sequence (st1, st2) ->
         (* Evaluate the first statement *)
-        let cf_st1 = eval_statement config st1 in
-        (* Evaluate the sequence *)
-        let cf_st2 cf res =
-          match res with
-          (* 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 | LoopReturn _
-          | EndEnterLoop _ | EndContinue _ ->
-              cf res
+        let ctx_resl, cf_st1 = eval_statement config st1 ctx in
+        (* Evaluate the sequence (evaluate the second statement if the first
+           statement successfully evaluated, otherwise transfmit the control-flow
+           break) *)
+        let ctx_res_cfl =
+          List.map
+            (fun (ctx, res) ->
+              match res with
+              (* Evaluation successful: evaluate the second statement *)
+              | Unit -> eval_statement config st2 ctx
+              (* Control-flow break: transmit. We enumerate the cases on purpose *)
+              | Panic | Break _ | Continue _ | Return | LoopReturn _
+              | EndEnterLoop _ | EndContinue _ ->
+                  ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc))
+            ctx_resl
+        in
+        (* Put everything together:
+           - we return the flattened list of contexts and results
+           - we need to build the continuation which will build the whole
+             expression from the continuations for the individual branches
+        *)
+        let ctx_resl, cf_st2 =
+          comp_seqs __FILE__ __LINE__ st.meta ctx_res_cfl
         in
-        (* Compose and apply *)
-        comp cf_st1 cf_st2 cf ctx
+        (ctx_resl, cc_comp cf_st1 cf_st2)
     | Loop loop_body ->
-        InterpreterLoops.eval_loop config st.meta
-          (eval_statement config loop_body)
-          cf ctx
-    | Switch switch -> eval_switch config st.meta switch cf ctx
+        let eval_loop_body = eval_statement config loop_body in
+        InterpreterLoops.eval_loop config st.meta eval_loop_body ctx
+    | Switch switch -> eval_switch config st.meta switch ctx
   in
   (* Compose and apply *)
-  comp cc cf_eval_st cf ctx
+  (stl, cc_comp cc cf_eval_st)
 
-and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
-    (generics : generic_args) : st_cm_fun =
- fun cf ctx ->
+and eval_global (config : config) (meta : Meta.meta) (dest : place)
+    (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun =
+ fun ctx ->
   let global = ctx_lookup_global_decl ctx gid in
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body *)
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
-      (eval_transparent_function_call_concrete config global.item_meta.meta
-         global.body call)
-        cf ctx
-  | SymbolicMode ->
+      eval_transparent_function_call_concrete config meta global.body call ctx
+  | SymbolicMode -> (
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
-      cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta
+      cassert __FILE__ __LINE__ (ty_no_regions global.ty) meta
         "Const globals should not contain regions";
       (* Instantiate the type  *)
       (* There shouldn't be any reference to Self *)
@@ -1082,19 +1051,24 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
         Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
           global.ty
       in
-      let sval = mk_fresh_symbolic_value global.item_meta.meta ty in
-      let cc =
-        assign_to_place config global.item_meta.meta
+      let sval = mk_fresh_symbolic_value meta ty in
+      let ctx, cc =
+        assign_to_place config meta
           (mk_typed_value_from_symbolic_value sval)
-          dest
+          dest ctx
       in
-      let e = cc (cf Unit) ctx in
-      S.synthesize_global_eval gid generics sval e
+      ( [ (ctx, Unit) ],
+        fun el ->
+          match el with
+          | Some [ e ] ->
+              (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e)
+          | Some _ -> internal_error __FILE__ __LINE__ meta
+          | _ -> None ))
 
 (** Evaluate a switch *)
 and eval_switch (config : config) (meta : Meta.meta) (switch : switch) :
-    st_cm_fun =
- fun cf ctx ->
+    stl_cm_fun =
+ fun ctx ->
   (* We evaluate the operand in two steps:
    * first we prepare it, then we check if its value is concrete or
    * symbolic. If it is concrete, we can then evaluate the operand
@@ -1104,130 +1078,147 @@ and eval_switch (config : config) (meta : Meta.meta) (switch : switch) :
    * (and would thus floating in thin air...)!
    * *)
   (* Match on the targets *)
-  let cf_match : st_cm_fun =
-   fun cf ctx ->
-    match switch with
-    | If (op, st1, st2) ->
-        (* Evaluate the operand *)
-        let cf_eval_op = eval_operand config meta op in
-        (* Switch on the value *)
-        let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun =
-         fun ctx ->
-          match op_v.value with
-          | VLiteral (VBool b) ->
-              (* Evaluate the if and the branch body *)
-              let cf_branch cf : m_fun =
-                (* Branch *)
-                if b then eval_statement config st1 cf
-                else eval_statement config st2 cf
-              in
-              (* Compose the continuations *)
-              cf_branch cf ctx
-          | VSymbolic sv ->
-              (* Expand the symbolic boolean, and continue by evaluating
-               * the branches *)
-              let cf_true : st_cm_fun = eval_statement config st1 in
-              let cf_false : st_cm_fun = eval_statement config st2 in
+  match switch with
+  | If (op, st1, st2) ->
+      (* Evaluate the operand *)
+      let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in
+      (* Switch on the value *)
+      let ctx_resl, cf_if =
+        match op_v.value with
+        | VLiteral (VBool b) ->
+            (* Branch *)
+            if b then eval_statement config st1 ctx
+            else eval_statement config st2 ctx
+        | VSymbolic sv ->
+            (* Expand the symbolic boolean, and continue by evaluating
+               the branches *)
+            let (ctx_true, ctx_false), cf_bool =
               expand_symbolic_bool config meta sv
                 (S.mk_opt_place_from_op meta op ctx)
-                cf_true cf_false cf ctx
-          | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
-        in
-        (* Compose *)
-        comp cf_eval_op cf_if cf ctx
-    | SwitchInt (op, int_ty, stgts, otherwise) ->
-        (* Evaluate the operand *)
-        let cf_eval_op = eval_operand config meta op in
-        (* Switch on the value *)
-        let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun =
-         fun ctx ->
-          match op_v.value with
-          | VLiteral (VScalar sv) ->
-              (* Evaluate the branch *)
-              let cf_eval_branch cf =
-                (* Sanity check *)
-                sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta;
-                (* Find the branch *)
-                match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
-                | None -> eval_statement config otherwise cf
-                | Some (_, tgt) -> eval_statement config tgt cf
-              in
-              (* Compose *)
-              cf_eval_branch cf ctx
-          | VSymbolic sv ->
-              (* Expand the symbolic value and continue by evaluating the
-               * proper branches *)
-              let stgts =
-                List.map
-                  (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st))
-                  stgts
-              in
-              (* Several branches may be grouped together: every branch is described
-               * by a pair (list of values, branch expression).
-               * In order to do a symbolic evaluation, we make this "flat" by
-               * de-grouping the branches. *)
-              let stgts =
-                List.concat
-                  (List.map
-                     (fun (vl, st) -> List.map (fun v -> (v, st)) vl)
-                     stgts)
-              in
-              (* Translate the otherwise branch *)
-              let otherwise = eval_statement config otherwise in
-              (* Expand and continue *)
+                ctx
+            in
+            let resl_true = eval_statement config st1 ctx_true in
+            let resl_false = eval_statement config st2 ctx_false in
+            let ctx_resl, cf_branches =
+              comp_seqs __FILE__ __LINE__ meta [ resl_true; resl_false ]
+            in
+            let cc el =
+              match cf_branches el with
+              | None -> None
+              | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false))
+              | _ -> internal_error __FILE__ __LINE__ meta
+            in
+            (ctx_resl, cc)
+        | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
+      in
+      (* Compose *)
+      (ctx_resl, cc_comp cf_eval_op cf_if)
+  | SwitchInt (op, int_ty, stgts, otherwise) ->
+      (* Evaluate the operand *)
+      let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in
+      (* Switch on the value *)
+      let ctx_resl, cf_switch =
+        match op_v.value with
+        | VLiteral (VScalar sv) -> (
+            (* Sanity check *)
+            sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta;
+            (* Find the branch *)
+            match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
+            | None -> eval_statement config otherwise ctx
+            | Some (_, tgt) -> eval_statement config tgt ctx)
+        | VSymbolic sv ->
+            (* Several branches may be grouped together: every branch is described
+               by a pair (list of values, branch expression).
+               In order to do a symbolic evaluation, we make this "flat" by
+               de-grouping the branches. *)
+            let values, branches =
+              List.split
+                (List.concat
+                   (List.map
+                      (fun (vl, st) -> List.map (fun v -> (v, st)) vl)
+                      stgts))
+            in
+            (* Expand the symbolic value *)
+            let (ctx_branches, ctx_otherwise), cf_int =
               expand_symbolic_int config meta sv
                 (S.mk_opt_place_from_op meta op ctx)
-                int_ty stgts otherwise cf ctx
-          | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
-        in
-        (* Compose *)
-        comp cf_eval_op cf_switch cf ctx
-    | Match (p, stgts, otherwise) ->
-        (* Access the place *)
-        let access = Read in
-        let expand_prim_copy = false in
-        let cf_read_p cf : m_fun =
-          access_rplace_reorganize_and_read config meta expand_prim_copy access
-            p cf
-        in
-        (* Match on the value *)
-        let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun =
-         fun ctx ->
-          (* The value may be shared: we need to ignore the shared loans
-             to read the value itself *)
-          let p_v = value_strip_shared_loans p_v in
-          (* Match *)
-          match p_v.value with
-          | VAdt adt -> (
-              (* Evaluate the discriminant *)
-              let dv = Option.get adt.variant_id in
-              (* Find the branch, evaluate and continue *)
-              match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with
-              | None -> (
-                  match otherwise with
-                  | None -> craise __FILE__ __LINE__ meta "No otherwise branch"
-                  | Some otherwise -> eval_statement config otherwise cf ctx)
-              | Some (_, tgt) -> eval_statement config tgt cf ctx)
-          | VSymbolic sv ->
-              (* Expand the symbolic value - may lead to branching *)
-              let cf_expand =
-                expand_symbolic_adt config meta sv
-                  (Some (S.mk_mplace meta p ctx))
-              in
-              (* Re-evaluate the switch - the value is not symbolic anymore,
-                 which means we will go to the other branch *)
-              cf_expand (eval_switch config meta switch) cf ctx
-          | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
-        in
-        (* Compose *)
-        comp cf_read_p cf_match cf ctx
-  in
-  (* Compose the continuations *)
-  cf_match cf ctx
+                int_ty values ctx
+            in
+            (* Evaluate the branches: first the "regular" branches *)
+            let resl_branches =
+              List.map
+                (fun (ctx, branch) -> eval_statement config branch ctx)
+                (List.combine ctx_branches branches)
+            in
+            (* Then evaluate the "otherwise" branch *)
+            let resl_otherwise =
+              eval_statement config otherwise ctx_otherwise
+            in
+            (* Compose the continuations *)
+            let resl, cf =
+              comp_seqs __FILE__ __LINE__ meta
+                (resl_branches @ [ resl_otherwise ])
+            in
+            let cc el =
+              match el with
+              | None -> None
+              | Some el ->
+                  let el, e_otherwise = Collections.List.pop_last el in
+                  cf_int (Some (el, e_otherwise))
+            in
+            (resl, cc_comp cc cf)
+        | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
+      in
+      (* Compose *)
+      (ctx_resl, cc_comp cf_eval_op cf_switch)
+  | Match (p, stgts, otherwise) ->
+      (* Access the place *)
+      let access = Read in
+      let expand_prim_copy = false in
+      let p_v, ctx, cf_read_p =
+        access_rplace_reorganize_and_read config meta expand_prim_copy access p
+          ctx
+      in
+      (* Match on the value *)
+      let ctx_resl, cf_match =
+        (* The value may be shared: we need to ignore the shared loans
+           to read the value itself *)
+        let p_v = value_strip_shared_loans p_v in
+        (* Match *)
+        match p_v.value with
+        | VAdt adt -> (
+            (* Evaluate the discriminant *)
+            let dv = Option.get adt.variant_id in
+            (* Find the branch, evaluate and continue *)
+            match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with
+            | None -> (
+                match otherwise with
+                | None -> craise __FILE__ __LINE__ meta "No otherwise branch"
+                | Some otherwise -> eval_statement config otherwise ctx)
+            | Some (_, tgt) -> eval_statement config tgt ctx)
+        | VSymbolic sv ->
+            (* Expand the symbolic value - may lead to branching *)
+            let ctxl, cf_expand =
+              expand_symbolic_adt config meta sv
+                (Some (S.mk_mplace meta p ctx))
+                ctx
+            in
+            (* Re-evaluate the switch - the value is not symbolic anymore,
+               which means we will go to the other branch *)
+            let resl =
+              List.map (fun ctx -> (eval_switch config meta switch) ctx) ctxl
+            in
+            (* Compose the continuations *)
+            let ctx_resl, cf = comp_seqs __FILE__ __LINE__ meta resl in
+            (ctx_resl, cc_comp cf_expand cf)
+        | _ -> craise __FILE__ __LINE__ meta "Inconsistent state"
+      in
+      (* Compose *)
+      (ctx_resl, cc_comp cf_read_p cf_match)
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
 and eval_function_call (config : config) (meta : Meta.meta) (call : call) :
-    st_cm_fun =
+    stl_cm_fun =
   (* There are several cases:
      - this is a local function, in which case we execute its body
      - this is an assumed function, in which case there is a special treatment
@@ -1238,24 +1229,32 @@ and eval_function_call (config : config) (meta : Meta.meta) (call : call) :
   | SymbolicMode -> eval_function_call_symbolic config meta call
 
 and eval_function_call_concrete (config : config) (meta : Meta.meta)
-    (call : call) : st_cm_fun =
- fun cf ctx ->
+    (call : call) : stl_cm_fun =
+ fun ctx ->
   match call.func with
   | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet"
   | FnOpRegular func -> (
       match func.func with
       | FunId (FRegular fid) ->
-          eval_transparent_function_call_concrete config meta fid call cf ctx
-      | FunId (FAssumed fid) ->
+          eval_transparent_function_call_concrete config meta fid call ctx
+      | FunId (FAssumed fid) -> (
           (* 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 meta fid call (cf Unit) ctx
+          let ctx, cc =
+            eval_assumed_function_call_concrete config meta fid call ctx
+          in
+          ( [ (ctx, Unit) ],
+            fun el ->
+              match el with
+              | Some [ e ] -> cc (Some e)
+              | Some _ -> internal_error __FILE__ __LINE__ meta
+              | _ -> None ))
       | TraitMethod _ -> craise __FILE__ __LINE__ meta "Unimplemented")
 
 and eval_function_call_symbolic (config : config) (meta : Meta.meta)
-    (call : call) : st_cm_fun =
+    (call : call) : stl_cm_fun =
   match call.func with
   | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet"
   | FnOpRegular func -> (
@@ -1267,7 +1266,8 @@ and eval_function_call_symbolic (config : config) (meta : Meta.meta)
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
-    (fid : FunDeclId.id) (call : call) : st_cm_fun =
+    (fid : FunDeclId.id) (call : call) : stl_cm_fun =
+ fun ctx ->
   let args = call.args in
   let dest = call.dest in
   match call.func with
@@ -1277,91 +1277,96 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
       (* Sanity check: we don't fully handle the const generic vars environment
          in concrete mode yet *)
       sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
-      fun cf ctx ->
-        (* Retrieve the (correctly instantiated) body *)
-        let def = ctx_lookup_fun_decl ctx fid in
-        (* We can evaluate the function call only if it is not opaque *)
-        let body =
-          match def.body with
-          | None ->
-              craise __FILE__ __LINE__ meta
-                ("Can't evaluate a call to an opaque function: "
-                ^ name_to_string ctx def.name)
-          | Some body -> body
-        in
-        (* TODO: we need to normalize the types if we want to correctly support traits *)
-        cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta
-          "Traits are not supported yet in concrete mode";
-        (* There shouldn't be any reference to Self *)
-        let tr_self = UnknownTrait __FUNCTION__ in
-        let subst =
-          Subst.make_subst_from_generics def.signature.generics generics tr_self
-        in
-        let locals, body_st = Subst.fun_body_substitute_in_body subst body in
-
-        (* Evaluate the input operands *)
-        sanity_check __FILE__ __LINE__
-          (List.length args = body.arg_count)
-          body.meta;
-        let cc = eval_operands config body.meta args in
-
-        (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
-         * of the operands evaluation from above to the functions afterwards, while
-         * ignoring it in this function *)
-        let cc = comp_transmit cc push_frame in
-
-        (* Compute the initial values for the local variables *)
-        (* 1. Push the return value *)
-        let ret_var, locals =
-          match locals with
-          | ret_ty :: locals -> (ret_ty, locals)
-          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
-        in
-        let input_locals, locals =
-          Collections.List.split_at locals body.arg_count
-        in
+      (* Retrieve the (correctly instantiated) body *)
+      let def = ctx_lookup_fun_decl ctx fid in
+      (* We can evaluate the function call only if it is not opaque *)
+      let body =
+        match def.body with
+        | None ->
+            craise __FILE__ __LINE__ meta
+              ("Can't evaluate a call to an opaque function: "
+              ^ name_to_string ctx def.name)
+        | Some body -> body
+      in
+      (* TODO: we need to normalize the types if we want to correctly support traits *)
+      cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta
+        "Traits are not supported yet in concrete mode";
+      (* There shouldn't be any reference to Self *)
+      let tr_self = UnknownTrait __FUNCTION__ in
+      let subst =
+        Subst.make_subst_from_generics def.signature.generics generics tr_self
+      in
+      let locals, body_st = Subst.fun_body_substitute_in_body subst body in
+
+      (* Evaluate the input operands *)
+      sanity_check __FILE__ __LINE__
+        (List.length args = body.arg_count)
+        body.meta;
+      let vl, ctx, cc = eval_operands config body.meta args ctx in
+
+      (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
+       * of the operands evaluation from above to the functions afterwards, while
+       * ignoring it in this function *)
+      let ctx = push_frame ctx in
+
+      (* Compute the initial values for the local variables *)
+      (* 1. Push the return value *)
+      let ret_var, locals =
+        match locals with
+        | ret_ty :: locals -> (ret_ty, locals)
+        | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+      in
+      let input_locals, locals =
+        Collections.List.split_at locals body.arg_count
+      in
 
-        let cc =
-          comp_transmit cc
-            (push_var meta ret_var (mk_bottom meta ret_var.var_ty))
-        in
+      let ctx = push_var meta ret_var (mk_bottom meta ret_var.var_ty) ctx in
 
-        (* 2. Push the input values *)
-        let cf_push_inputs cf args =
-          let inputs = List.combine input_locals args in
-          (* Note that this function checks that the variables and their values
-           * have the same type (this is important) *)
-          push_vars meta inputs cf
-        in
-        let cc = comp cc cf_push_inputs in
-
-        (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
-        let cc = comp cc (push_uninitialized_vars meta locals) in
-
-        (* Execute the function body *)
-        let cc = comp cc (eval_function_body config body_st) in
-
-        (* Pop the stack frame and move the return value to its destination *)
-        let cf_finish cf res =
-          match res with
-          | Panic -> cf Panic
-          | Return ->
-              (* Pop the stack frame, retrieve the return value, move it to
-               * its destination and continue *)
-              pop_frame_assign config meta dest (cf Unit)
-          | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
-          | EndContinue _ ->
-              craise __FILE__ __LINE__ meta "Unreachable"
-        in
-        let cc = comp cc cf_finish in
+      (* 2. Push the input values *)
+      let ctx =
+        let inputs = List.combine input_locals vl in
+        (* Note that this function checks that the variables and their values
+         * have the same type (this is important) *)
+        push_vars meta inputs ctx
+      in
 
-        (* Continue *)
-        cc cf ctx
+      (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
+      let ctx = push_uninitialized_vars meta locals ctx in
+
+      (* Execute the function body *)
+      let ctx_resl, cc = comp cc (eval_function_body config body_st ctx) in
+
+      (* Pop the stack frame and move the return value to its destination *)
+      let ctx_resl_cfl =
+        List.map
+          (fun (ctx, res) ->
+            match res with
+            | Panic -> ((ctx, Panic), fun e -> e)
+            | Return ->
+                (* Pop the stack frame, retrieve the return value, move it to
+                   its destination and continue *)
+                let ctx, cf = pop_frame_assign config meta dest ctx in
+                ((ctx, Unit), cf)
+            | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
+            | EndContinue _ ->
+                craise __FILE__ __LINE__ meta "Unreachable")
+          ctx_resl
+      in
+      let ctx_resl, cfl = List.split ctx_resl_cfl in
+      let cf_pop el =
+        match el with
+        | None -> None
+        | Some el ->
+            Some
+              (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
+      in
+      (* Continue *)
+      (ctx_resl, cc_comp cc cf_pop)
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
 and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
-    (call : call) : st_cm_fun =
- fun cf ctx ->
+    (call : call) : stl_cm_fun =
+ fun ctx ->
   let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg =
     eval_transparent_function_call_symbolic_inst meta call ctx
   in
@@ -1383,7 +1388,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func
     def.signature regions_hierarchy inst_sg generics trait_method_generics
-    call.args call.dest cf ctx
+    call.args call.dest ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1401,8 +1406,8 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
     (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig)
     (generics : generic_args)
     (trait_method_generics : (generic_args * trait_instance_id) option)
-    (args : operand list) (dest : place) : st_cm_fun =
- fun cf ctx ->
+    (args : operand list) (dest : place) : stl_cm_fun =
+ fun ctx ->
   log#ldebug
     (lazy
       ("eval_function_call_symbolic_from_inst_sig:\n- fid: "
@@ -1428,70 +1433,65 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
   let dest_place = Some (S.mk_mplace meta dest ctx) in
 
   (* Evaluate the input operands *)
-  let cc = eval_operands config meta args in
+  let args, ctx, cc = eval_operands config meta args ctx in
 
   (* Generate the abstractions and insert them in the context *)
   let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in
-  let cf_call cf (args : typed_value list) : m_fun =
-   fun ctx ->
-    let args_with_rtypes = List.combine args inst_sg.inputs in
-
-    (* Check the type of the input arguments *)
-    cassert __FILE__ __LINE__
-      (List.for_all
-         (fun ((arg, rty) : typed_value * rty) ->
-           arg.ty = Subst.erase_regions rty)
-         args_with_rtypes)
-      meta "The input arguments don't have the proper type";
-    (* Check that the input arguments don't contain symbolic values that can't 
-     * be fed to functions (i.e., symbolic values output from function return
-     * values and which contain borrows of borrows can't be used as function
-     * inputs *)
-    sanity_check __FILE__ __LINE__
-      (List.for_all
-         (fun arg ->
-           not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg))
-         args)
-      meta;
-
-    (* Initialize the abstractions and push them in the context.
-     * First, we define the function which, given an initialized, empty
-     * abstraction, computes the avalues which should be inserted inside.
-     *)
-    let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
-        eval_ctx * typed_avalue list =
-      (* Project over the input values *)
-      let ctx, args_projs =
-        List.fold_left_map
-          (fun ctx (arg, arg_rty) ->
-            apply_proj_borrows_on_input_value config meta ctx abs.regions
-              abs.ancestors_regions arg arg_rty)
-          ctx args_with_rtypes
-      in
-      (* Group the input and output values *)
-      (ctx, List.append args_projs [ ret_av abs.regions ])
-    in
-    (* Actually initialize and insert the abstractions *)
-    let call_id = fresh_fun_call_id () in
-    let region_can_end _ = true in
-    let ctx =
-      create_push_abstractions_from_abs_region_groups
-        (fun rg_id -> FunCall (call_id, rg_id))
-        inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx
-    in
+  let args_with_rtypes = List.combine args inst_sg.inputs in
 
-    (* Apply the continuation *)
-    let expr = cf ctx in
+  (* Check the type of the input arguments *)
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ((arg, rty) : typed_value * rty) ->
+         arg.ty = Subst.erase_regions rty)
+       args_with_rtypes)
+    meta "The input arguments don't have the proper type";
+  (* Check that the input arguments don't contain symbolic values that can't
+   * be fed to functions (i.e., symbolic values output from function return
+   * values and which contain borrows of borrows can't be used as function
+   * inputs *)
+  sanity_check __FILE__ __LINE__
+    (List.for_all
+       (fun arg ->
+         not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg))
+       args)
+    meta;
 
-    (* Synthesize the symbolic AST *)
-    S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy
-      abs_ids generics trait_method_generics args args_places ret_spc dest_place
-      expr
+  (* Initialize the abstractions and push them in the context.
+   * First, we define the function which, given an initialized, empty
+   * abstraction, computes the avalues which should be inserted inside.
+   *)
+  let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
+      eval_ctx * typed_avalue list =
+    (* Project over the input values *)
+    let ctx, args_projs =
+      List.fold_left_map
+        (fun ctx (arg, arg_rty) ->
+          apply_proj_borrows_on_input_value config meta ctx abs.regions
+            abs.ancestors_regions arg arg_rty)
+        ctx args_with_rtypes
+    in
+    (* Group the input and output values *)
+    (ctx, List.append args_projs [ ret_av abs.regions ])
+  in
+  (* Actually initialize and insert the abstractions *)
+  let call_id = fresh_fun_call_id () in
+  let region_can_end _ = true in
+  let ctx =
+    create_push_abstractions_from_abs_region_groups
+      (fun rg_id -> FunCall (call_id, rg_id))
+      inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx
+  in
+  (* Synthesize the symbolic AST *)
+  let cc =
+    cc_comp cc
+      (S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy
+         abs_ids generics trait_method_generics args args_places ret_spc
+         dest_place)
   in
-  let cc = comp cc cf_call in
 
   (* Move the return value to its destination *)
-  let cc = comp cc (assign_to_place config meta ret_value dest) in
+  let ctx, cc = comp cc (assign_to_place config meta ret_value dest ctx) in
 
   (* End the abstractions which don't contain loans and don't have parent
    * abstractions.
@@ -1499,8 +1499,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
    * retry (because then we might end their children abstractions)
    *)
   let abs_ids = ref abs_ids in
-  let rec end_abs_with_no_loans cf : m_fun =
-   fun ctx ->
+  let rec end_abs_with_no_loans ctx =
     (* Find the abstractions which don't contain loans *)
     let no_loans_abs, with_loans_abs =
       List.partition
@@ -1521,35 +1520,36 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
       abs_ids := with_loans_abs;
       (* End the abstractions which can be ended *)
       let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in
-      let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in
+      let ctx, cc =
+        InterpreterBorrows.end_abstractions config meta no_loans_abs ctx
+      in
       (* Recursive call *)
-      let cc = comp cc end_abs_with_no_loans in
-      (* Continue *)
-      cc cf ctx)
+      comp cc (end_abs_with_no_loans ctx))
     else (* No abstractions to end: continue *)
-      cf ctx
+      (ctx, fun e -> e)
   in
   (* Try to end the abstractions with no loans if:
    * - the option is enabled
    * - the function returns unit
    * (see the documentation of {!config} for more information)
    *)
-  let cc =
-    if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output
-    then comp cc end_abs_with_no_loans
-    else cc
+  let ctx, cc =
+    comp cc
+      (if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output
+       then end_abs_with_no_loans ctx
+       else (ctx, fun e -> e))
   in
 
   (* 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... *)
-  cc (cf Unit) ctx
+  ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc)
 
 (** Evaluate a non-local function call in symbolic mode *)
 and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta)
-    (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun =
- fun cf ctx ->
+    (fid : assumed_fun_id) (call : call) (func : fn_ptr) : stl_cm_fun =
+ fun ctx ->
   let generics = func.generics in
   let args = call.args in
   let dest = call.dest in
@@ -1570,7 +1570,8 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta)
   | BoxFree ->
       (* Degenerate case: box_free - note that this is not really a function
        * call: no need to call a "synthesize_..." function *)
-      eval_box_free config meta generics args dest (cf Unit) ctx
+      let ctx, cc = eval_box_free config meta generics args dest ctx in
+      ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc)
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1598,25 +1599,34 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta)
       (* Evaluate the function call *)
       eval_function_call_symbolic_from_inst_sig config meta
         (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args
-        dest cf ctx
+        dest ctx
 
 (** Evaluate a statement seen as a function body *)
-and eval_function_body (config : config) (body : statement) : st_cm_fun =
- fun cf ctx ->
+and eval_function_body (config : config) (body : statement) : stl_cm_fun =
+ fun ctx ->
   log#ldebug (lazy "eval_function_body:");
-  let cc = eval_statement config body in
-  let cf_finish cf res =
-    log#ldebug (lazy "eval_function_body: cf_finish");
-    (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we
-     * delegate the check to the caller. *)
-    (* Expand the symbolic values if necessary - we need to do that before
-     * checking the invariants *)
-    let cc = greedy_expand_symbolic_values config body.meta in
-    (* Sanity check *)
-    let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in
-    (* Check if right meta *)
-    (* Continue *)
-    cc (cf res)
+  let ctx_resl, cf_body = eval_statement config body ctx in
+  let ctx_res_cfl =
+    List.map
+      (fun (ctx, res) ->
+        log#ldebug (lazy "eval_function_body: cf_finish");
+        (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we
+           * delegate the check to the caller. *)
+        (* Expand the symbolic values if necessary - we need to do that before
+           * checking the invariants *)
+        let ctx, cf = greedy_expand_symbolic_values config body.meta ctx in
+        (* Sanity check *)
+        Invariants.check_invariants body.meta ctx;
+        (* Continue *)
+        ((ctx, res), cf))
+      ctx_resl
+  in
+  let ctx_resl, cfl = List.split ctx_res_cfl in
+  let cf_end el =
+    match el with
+    | None -> None
+    | Some el ->
+        Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
   in
   (* Compose and continue *)
-  comp cc cf_finish cf ctx
+  (ctx_resl, cc_comp cf_body cf_end)
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 7a2783bb..79ce1f73 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -17,7 +17,11 @@ open Cps
     continuation with [None].
  *)
 val pop_frame :
-  config -> Meta.meta -> bool -> (typed_value option -> m_fun) -> m_fun
+  config ->
+  Meta.meta ->
+  bool ->
+  eval_ctx ->
+  typed_value option * eval_ctx * (eval_result -> eval_result)
 
 (** Helper.
 
@@ -46,7 +50,7 @@ val create_push_abstractions_from_abs_region_groups :
   eval_ctx
 
 (** Evaluate a statement *)
-val eval_statement : config -> statement -> st_cm_fun
+val eval_statement : config -> statement -> stl_cm_fun
 
 (** Evaluate a statement seen as a function body *)
-val eval_function_body : config -> statement -> st_cm_fun
+val eval_function_body : config -> statement -> stl_cm_fun