From 807c590113718d8c20419ab31782dd0368e2b045 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 18 Nov 2021 15:24:27 +0100
Subject: Start working on the values for the interpreter

---
 src/Identifiers.ml | 12 ++++++++++--
 src/Values.ml      | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 2 deletions(-)

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 28ed1909..7d440f4d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -17,7 +17,9 @@ module type Id = sig
 
   val to_string : id -> string
 
-  val empty : 'a vector
+  val empty_vector : 'a vector
+
+  module Set : Set.S with type elt = id
 
   val id_of_json : Yojson.Basic.t -> (id, string) result
 
@@ -47,7 +49,13 @@ module IdGen () : Id = struct
 
   let to_string = string_of_int
 
-  let empty = []
+  let empty_vector = []
+
+  module Set = Set.Make (struct
+    type t = id
+
+    let compare = compare
+  end)
 
   let id_of_json js =
     match js with
diff --git a/src/Values.ml b/src/Values.ml
index e1205efc..051949fc 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -3,6 +3,8 @@ open Types
 
 module VarId = IdGen ()
 
+module BorrowId = IdGen ()
+
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
@@ -42,8 +44,53 @@ type scalar_value =
   | U64 of big_int
   | U128 of big_int
 
+(** A constant value *)
 type constant_value =
   | Scalar of scalar_value
   | Bool of bool
   | Char of char
   | String of string
+
+type symbolic_value = unit
+(** Symbolic value - TODO *)
+
+(** An untyped value, used in the environments *)
+type value =
+  | Adt of adt_value  (** Enumerations and structures *)
+  | Symbolic of symbolic_value  (** Unknown value *)
+  | Concrete of constant_value  (** Concrete (non-symbolic) value *)
+  | Tuple of value FieldId.vector
+      (** Tuple - note that units are encoded as 0-tuples *)
+  | Borrow of borrow_content  (** A borrowed value *)
+  | Loan of loan_content  (** A loaned value *)
+  | Bottom  (** No value (uninitialized or moved value) *)
+  | Assumed of assumed_value  (** Assumed types (Box, Vec, Cell...) *)
+
+and adt_value = {
+  def_id : TypeDefId.id;
+  variant_id : VariantId.id option;
+  regions : erased_region list;
+  types : rty list;
+  field_values : value FieldId.vector;
+}
+
+and borrow_content =
+  | SharedBorrow of BorrowId.id  (** A shared value *)
+  | MutBorrow of BorrowId.id * value  (** A mutably borrowed value *)
+  | InactivatedMutBorrow of BorrowId.id
+      (** An inactivated mut borrow.
+
+          This is used to model two-phase borrows. When evaluating a two-phase
+          mutable borrow, we first introduce an inactivated borrow which behaves
+          like a shared borrow, until the moment we actually *use* the borrow:
+          at this point, we end all the other shared borrows (or inactivated borrows
+          - though there shouldn't be any other inactivated borrows if the program
+          is well typed) of this value and replace the inactivated borrow with a
+          mutable borrow.
+       *)
+
+and loan_content =
+  | SharedLoan of BorrowId.Set.t * value
+  | MutLoan of BorrowId.id
+
+and assumed_value = Box of value
-- 
cgit v1.2.3