Remove the cps.eval_result type

10 files changed, 73 insertions, 38 deletions

diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index c414652d..7138477b 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -35,9 +35,6 @@ type statement_eval_res =
        *)
 [@@deriving show]
 
-(* TODO: remove *)
-type eval_result = SymbolicAst.expression
-
 (** Function which takes a context as input, and evaluates to:
     - a new context
     - a continuation with which to build the execution trace, provided the
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 3c264c6e..5a3d6f10 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -446,8 +446,7 @@ let expand_symbolic_value_borrow (config : config) (span : Meta.span)
 let expand_symbolic_bool (config : config) (span : Meta.span)
     (sv : symbolic_value) (sv_place : SA.mplace option) :
     eval_ctx ->
-    (eval_ctx * eval_ctx)
-    * (SymbolicAst.expression * SymbolicAst.expression -> eval_result) =
+    (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression) =
  fun ctx ->
   (* Compute the expanded value *)
   let original_sv = sv in
@@ -533,7 +532,7 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span)
 
 let expand_symbolic_adt (config : config) (span : Meta.span)
     (sv : symbolic_value) (sv_place : SA.mplace option) :
-    eval_ctx -> eval_ctx list * (SymbolicAst.expression list -> eval_result) =
+    eval_ctx -> eval_ctx list * (SA.expression list -> SA.expression) =
  fun ctx ->
   (* Debug *)
   log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
@@ -568,7 +567,7 @@ let expand_symbolic_int (config : config) (span : Meta.span)
     (int_type : integer_type) (tgts : scalar_value list) :
     eval_ctx ->
     (eval_ctx list * eval_ctx)
-    * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result) =
+    * (SA.expression list * SA.expression -> SA.expression) =
  fun ctx ->
   (* Sanity check *)
   sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) span;
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 9b5ebed3..50554490 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -38,7 +38,7 @@ val expand_symbolic_adt :
   symbolic_value ->
   SA.mplace option ->
   eval_ctx ->
-  eval_ctx list * (SymbolicAst.expression list -> eval_result)
+  eval_ctx list * (SA.expression list -> SA.expression)
 
 (** Expand a symbolic boolean.
 
@@ -50,8 +50,7 @@ val expand_symbolic_bool :
   symbolic_value ->
   SA.mplace option ->
   eval_ctx ->
-  (eval_ctx * eval_ctx)
-  * (SymbolicAst.expression * SymbolicAst.expression -> eval_result)
+  (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression)
 
 (** Symbolic integers are expanded upon evaluating a [SwitchInt].
 
@@ -76,7 +75,7 @@ val expand_symbolic_int :
   scalar_value list ->
   eval_ctx ->
   (eval_ctx list * eval_ctx)
-  * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result)
+  * (SA.expression list * SA.expression -> SA.expression)
 
 (** If this mode is activated through the [config], greedily expand the symbolic
     values which need to be expanded. See {!type:Contexts.config} for more information.
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 51c8108e..32c1cda5 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -67,7 +67,9 @@ let read_place_check (span : Meta.span) (access : access_kind) (p : place)
 
 let access_rplace_reorganize_and_read (config : config) (span : Meta.span)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Make sure we can evaluate the path *)
   let ctx, cc = update_ctx_along_read_place config span access p ctx in
   (* End the proper loans at the place itself *)
@@ -264,7 +266,8 @@ let prepare_eval_operand_reorganize (config : config) (span : Meta.span)
 (** Evaluate an operand, without reorganizing the context before *)
 let eval_operand_no_reorganize (config : config) (span : Meta.span)
     (op : operand) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Debug *)
   log#ldebug
     (lazy
@@ -363,7 +366,9 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
       (v, ctx, fun e -> e)
 
 let eval_operand (config : config) (span : Meta.span) (op : operand)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Debug *)
   log#ldebug
     (lazy
@@ -385,7 +390,9 @@ let prepare_eval_operands_reorganize (config : config) (span : Meta.span)
 (** Evaluate several operands. *)
 let eval_operands (config : config) (span : Meta.span) (ops : operand list)
     (ctx : eval_ctx) :
-    typed_value list * eval_ctx * (eval_result -> eval_result) =
+    typed_value list
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Prepare the operands *)
   let ctx, cc = prepare_eval_operands_reorganize config span ops ctx in
   (* Evaluate the operands *)
@@ -394,7 +401,9 @@ let eval_operands (config : config) (span : Meta.span) (ops : operand list)
 
 let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
     (op2 : operand) (ctx : eval_ctx) :
-    (typed_value * typed_value) * eval_ctx * (eval_result -> eval_result) =
+    (typed_value * typed_value)
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   let res, ctx, cc = eval_operands config span [ op1; op2 ] ctx in
   let res =
     match res with
@@ -405,7 +414,9 @@ let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
 
 let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operand *)
   let v, ctx, cc = eval_operand config span op ctx in
   (* Apply the unop *)
@@ -455,7 +466,9 @@ let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
 
 let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operand *)
   let v, ctx, cc = eval_operand config span op ctx in
   (* Generate a fresh symbolic value to store the result *)
@@ -481,7 +494,9 @@ let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
 
 let eval_unary_op (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   match config.mode with
   | ConcreteMode -> eval_unary_op_concrete config span unop op ctx
   | SymbolicMode -> eval_unary_op_symbolic config span unop op ctx
@@ -565,7 +580,9 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop)
 
 let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operands *)
   let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
   (* Compute the result of the binop *)
@@ -575,7 +592,9 @@ let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
 
 let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operands *)
   let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
   (* Generate a fresh symbolic value to store the result *)
@@ -623,7 +642,9 @@ let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
 
 let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   match config.mode with
   | ConcreteMode -> eval_binary_op_concrete config span binop op1 op2 ctx
   | SymbolicMode -> eval_binary_op_symbolic config span binop op1 op2 ctx
@@ -632,7 +653,8 @@ let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
     `&p` or `&mut p` or `&two-phase p`) *)
 let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
     (bkind : borrow_kind) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   match bkind with
   | BShared | BTwoPhaseMut | BShallow ->
       (* **REMARK**: we initially treated shallow borrows like shared borrows.
@@ -715,7 +737,8 @@ let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
 
 let eval_rvalue_aggregate (config : config) (span : Meta.span)
     (aggregate_kind : aggregate_kind) (ops : operand list) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Evaluate the operands *)
   let values, ctx, cc = eval_operands config span ops ctx in
   (* Compute the value *)
@@ -787,7 +810,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
 
 let eval_rvalue_not_global (config : config) (span : Meta.span)
     (rvalue : rvalue) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   log#ldebug (lazy "eval_rvalue");
   (* Small helper *)
   let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index feb641d1..29234ea9 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -25,7 +25,7 @@ val access_rplace_reorganize_and_read :
   access_kind ->
   place ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate an operand.
 
@@ -41,7 +41,7 @@ val eval_operand :
   Meta.span ->
   operand ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate several operands at once. *)
 val eval_operands :
@@ -49,7 +49,9 @@ val eval_operands :
   Meta.span ->
   operand list ->
   eval_ctx ->
-  typed_value list * eval_ctx * (eval_result -> eval_result)
+  typed_value list
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
@@ -63,7 +65,9 @@ val eval_rvalue_not_global :
   Meta.span ->
   rvalue ->
   eval_ctx ->
-  (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result)
+  (typed_value, eval_error) result
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate a fake read (update the context so that we can read a place) *)
 val eval_fake_read : config -> Meta.span -> place -> cm_fun
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 4755f0e9..90a3afe8 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -105,7 +105,9 @@ let eval_loop_symbolic (config : config) (span : span)
      will end with a call to the loop translation
   *)
   let ((res_fun_end, cf_fun_end), fp_bl_corresp) :
-      ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ =
+      ((eval_ctx * statement_eval_res)
+      * (SymbolicAst.expression -> SymbolicAst.expression))
+      * _ =
     (* First, preemptively end borrows/move values by matching the current
        context with the target context *)
     let ctx, cf_prepare =
@@ -158,7 +160,7 @@ let eval_loop_symbolic (config : config) (span : span)
   (* Synthesize the loop body *)
   let (resl_loop_body, cf_loop_body) :
       (eval_ctx * statement_eval_res) list
-      * (SymbolicAst.expression list -> eval_result) =
+      * (SymbolicAst.expression list -> SymbolicAst.expression) =
     (* First, evaluate the loop body starting from the **fixed-point** context *)
     let ctx_resl, cf_loop = eval_loop_body fp_ctx in
 
@@ -198,7 +200,7 @@ let eval_loop_symbolic (config : config) (span : span)
 
     (* Apply and compose *)
     let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in
-    let cc (el : SymbolicAst.expression list) : eval_result =
+    let cc (el : SymbolicAst.expression list) : SymbolicAst.expression =
       let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in
       cf_loop el
     in
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index faba1088..f201b84d 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -523,7 +523,8 @@ let rec update_ctx_along_write_place (config : config) (span : Meta.span)
       comp cc (update_ctx_along_write_place config span access p ctx)
 
 (** Small utility used to break control-flow *)
-exception UpdateCtx of (eval_ctx * (eval_result -> eval_result))
+exception
+  UpdateCtx of (eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression))
 
 let rec end_loans_at_place (config : config) (span : Meta.span)
     (access : access_kind) (p : place) : cm_fun =
@@ -629,7 +630,9 @@ let drop_outer_loans_at_lplace (config : config) (span : Meta.span) (p : place)
   (ctx, cc)
 
 let prepare_lplace (config : config) (span : Meta.span) (p : place)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   log#ldebug
     (lazy
       ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 86f0dcc0..3377f612 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -104,4 +104,4 @@ val prepare_lplace :
   Meta.span ->
   place ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4b4bac62..c74a1218 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -306,7 +306,9 @@ let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx)
 
 let move_return_value (config : config) (span : Meta.span)
     (pop_return_value : bool) (ctx : eval_ctx) :
-    typed_value option * eval_ctx * (eval_result -> eval_result) =
+    typed_value option
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   if pop_return_value then
     let ret_vid = VarId.zero in
     let v, ctx, cc =
@@ -317,7 +319,9 @@ let move_return_value (config : config) (span : Meta.span)
 
 let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool)
     (ctx : eval_ctx) :
-    typed_value option * eval_ctx * (eval_result -> eval_result) =
+    typed_value option
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Debug *)
   log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx));
 
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index c70396d6..443f559e 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -21,7 +21,9 @@ val pop_frame :
   Meta.span ->
   bool ->
   eval_ctx ->
-  typed_value option * eval_ctx * (eval_result -> eval_result)
+  typed_value option
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Helper.