From d376bd5633ed8bdd51861d5bede1888d0958d73c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 10:59:51 +0100
Subject: Change the signatures of the eval_rvalue_... functions

---
 src/Interpreter.ml | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 7940908c..c32e7d63 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3247,7 +3247,7 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
   | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
 
 let eval_rvalue_discriminant (config : C.config) (ctx : C.eval_ctx)
-    (p : E.place) : (C.eval_ctx * V.typed_value) eval_result =
+    (p : E.place) : C.eval_ctx * V.typed_value =
   S.synthesize_eval_rvalue_discriminant p;
   (* Note that discriminant values have type `isize` *)
   (* Access the value *)
@@ -3265,14 +3265,15 @@ let eval_rvalue_discriminant (config : C.config) (ctx : C.eval_ctx)
               failwith "Disciminant id out of range"
               (* Should really never happen *)
           | Ok sv ->
-              Ok
-                (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize })
-          ))
-  | Symbolic _ -> raise Unimplemented
+              (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
+      )
+  | Symbolic sv ->
+      (* We need to perform a symbolic expansion *)
+      raise Unimplemented
   | _ -> failwith "Invalid input for `discriminant`"
 
 let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
-    (bkind : E.borrow_kind) : (C.eval_ctx * V.typed_value) eval_result =
+    (bkind : E.borrow_kind) : C.eval_ctx * V.typed_value =
   S.synthesize_eval_rvalue_ref p bkind;
   match bkind with
   | E.Shared | E.TwoPhaseMut ->
@@ -3305,7 +3306,7 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
       (* Update the value in the context *)
       let ctx = write_place_unwrap config access p nv ctx in
       (* Return *)
-      Ok (ctx, rv)
+      (ctx, rv)
   | E.Mut ->
       (* Access the value *)
       let access = Write in
@@ -3321,11 +3322,11 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
       (* Update the value in the context *)
       let ctx = write_place_unwrap config access p nv ctx in
       (* Return *)
-      Ok (ctx, rv)
+      (ctx, rv)
 
 let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
     (aggregate_kind : E.aggregate_kind) (ops : E.operand list) :
-    (C.eval_ctx * V.typed_value) eval_result =
+    C.eval_ctx * V.typed_value =
   S.synthesize_eval_rvalue_aggregate aggregate_kind ops;
   (* Evaluate the operands *)
   let ctx, values = eval_operands config ctx ops in
@@ -3335,7 +3336,7 @@ let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
       let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
       let v = V.Adt { variant_id = None; field_values = values } in
       let ty = T.Adt (T.Tuple, [], tys) in
-      Ok (ctx, { V.value = v; ty })
+      (ctx, { V.value = v; ty })
   | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
       (* Sanity checks *)
       let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -3352,7 +3353,7 @@ let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
         { V.variant_id = opt_variant_id; V.field_values = values }
       in
       let aty = T.Adt (T.AdtId def_id, regions, types) in
-      Ok (ctx, { V.value = Adt av; ty = aty })
+      (ctx, { V.value = Adt av; ty = aty })
 
 (** Evaluate an rvalue in a given context: return the updated context and
     the computed value
@@ -3361,12 +3362,12 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
     (C.eval_ctx * V.typed_value) eval_result =
   match rvalue with
   | E.Use op -> Ok (eval_operand config ctx op)
-  | E.Ref (p, bkind) -> eval_rvalue_ref config ctx p bkind
+  | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind)
   | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op
   | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
-  | E.Discriminant p -> eval_rvalue_discriminant config ctx p
+  | E.Discriminant p -> Ok (eval_rvalue_discriminant config ctx p)
   | E.Aggregate (aggregate_kind, ops) ->
-      eval_rvalue_aggregate config ctx aggregate_kind ops
+      Ok (eval_rvalue_aggregate config ctx aggregate_kind ops)
 
 (** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return
-- 
cgit v1.2.3