From 6ee26448d36ee5ff49eeb4a1246f164e3a33ff50 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 24 Nov 2021 16:52:21 +0100
Subject: Implement the discriminant case of eval_rvalue

---
 src/Identifiers.ml |  4 ++++
 src/Interpreter.ml | 26 +++++++++++++++++++++-----
 2 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 22b52119..6f74e062 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -20,6 +20,8 @@ module type Id = sig
 
   val to_string : id -> string
 
+  val to_int : id -> int
+
   val empty_vector : 'a vector
 
   val vector_to_list : 'a vector -> 'a list
@@ -80,6 +82,8 @@ module IdGen () : Id = struct
 
   let to_string = string_of_int
 
+  let to_int x = x
+
   let empty_vector = []
 
   let vector_to_list v = v
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ebb4f2ee..5c5a9617 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1640,9 +1640,25 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
           Ok ({ ctx3 with env = env4 }, rv))
   | UnaryOp (unop, op) -> eval_unary_op config ctx unop op
   | BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
-  | Discriminant p -> raise Unimplemented
+  | Discriminant p -> (
+      (* Note that discriminant values have type `isize` *)
+      (* Access the value *)
+      let access = Read in
+      let ctx1, v = prepare_rplace config access p ctx in
+      match v.value with
+      | Adt av -> (
+          match av.variant_id with
+          | None ->
+              failwith
+                "Invalid input for `discriminant`: structure instead of enum"
+          | Some variant_id -> (
+              let id = Z.of_int (VariantId.to_int variant_id) in
+              match mk_scalar Isize id with
+              | Error _ ->
+                  failwith "Disciminant id out of range"
+                  (* Should really never happen *)
+              | Ok sv ->
+                  Ok (ctx1, { value = Concrete (Scalar sv); ty = Integer Isize })
+              ))
+      | _ -> failwith "Invalid input for `discriminant`")
   | Aggregate (aggregate_kind, ops) -> raise Unimplemented
-
-(* TODO:
-   update write_value
- *)
-- 
cgit v1.2.3