Add Values.ml and Expressions.ml

2 files changed, 118 insertions, 0 deletions

diff --git a/src/Expressions.ml b/src/Expressions.ml
new file mode 100644
index 00000000..f890f9c4
--- /dev/null
+++ b/src/Expressions.ml
@@ -0,0 +1,78 @@
+open Types
+open Values
+
+type field_proj_kind =
+  | Adt of TypeDefId.id * VariantId.id option
+  | Tuple of int
+
+type projection_elem =
+  | Deref
+  | DerefBox
+  | Field of field_proj_kind * FieldId.id
+  | Downcast of VariandId.id
+
+type projection = projection_elem list
+
+type place = { var_id : VarId.id; projection : projection }
+
+type borrow_kind = Shared | Mut | TwoPhaseMut
+
+type unop = Not | Neg
+
+(** A binary operation
+
+    Note that we merge checked binops and unchecked binops: we perform a
+    micro-pass on the MIR AST to remove the assertions introduced by rustc,
+    and use monadic functions for the binops which can fail (addition,
+    substraction, etc.) or have preconditions (division, remainder...)
+ *)
+type binop =
+  | BitXor
+  | BitAnd
+  | BitOr
+  | Eq
+  | Lt
+  | Le
+  | Ne
+  | Ge
+  | Gt
+  | Div
+  | Rem
+  | Add
+  | Sub
+  | Mul
+  | Shl
+  | Shr
+
+(** Constant value for an operand
+
+    It is a bit annoying, but Rust treats some ADT and tuple instances as
+    constants.
+    For instance, an enumeration with one variant and no fields is a constant.
+    A structure with no field is a constant.
+
+    For our translation, we use the following enumeration to encode those
+    special cases in assignments. They are converted to "normal" values
+    when evaluating the assignment (which is why we don't put them in the
+    [ConstantValue] enumeration.
+
+ *)
+type operand_constant_value =
+  | ConstantValue of constant_value
+  | Adt of TypeDefId.id
+  | Unit
+
+type operand =
+  | Copy of place
+  | Move of place
+  | Constant of ety * operand_constant_value
+
+type aggregate_kind = Tuple | Adt of TypeDefId.id * VariantId.id list
+
+type rvalue =
+  | Use of operand
+  | Ref of place * borrow_kind
+  | UnaryOp of unop * operand
+  | BinaryOp of binop * operand * operand
+  | Discriminant of place
+  | Aggregate of aggregate_kind * operand list
diff --git a/src/Values.ml b/src/Values.ml
new file mode 100644
index 00000000..006cc8da
--- /dev/null
+++ b/src/Values.ml
@@ -0,0 +1,40 @@
+open Identifiers
+open Types
+
+module VarId = IdGen ()
+
+module FunDefId = IdGen ()
+
+type var = {
+  index : VarId.id;  (** Unique variable identifier *)
+  name : string option;
+  ty : ety;
+      (** The variable type - erased type, because variables are not used
+       ** in function signatures *)
+}
+(** A variable *)
+
+(** A scalar value
+
+    Note that we use unbounded integers everywhere.
+    We then harcode the boundaries for the different types.
+ *)
+type scalar_value =
+  | Isize of Big_int.big_int
+  | I8 of Big_int.big_int
+  | I16 of Big_int.big_int
+  | I32 of Big_int.big_int
+  | I64 of Big_int.big_int
+  | I128 of Big_int.big_int
+  | Usize of Big_int.big_int
+  | U8 of Big_int.big_int
+  | U16 of Big_int.big_int
+  | U32 of Big_int.big_int
+  | U64 of Big_int.big_int
+  | U128 of Big_int.big_int
+
+type constant_value =
+  | Scalar of scalar_value
+  | Bool of bool
+  | Char of char
+  | String of string