summaryrefslogtreecommitdiff
path: root/compiler/PrimitiveValues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PrimitiveValues.ml')
-rw-r--r--compiler/PrimitiveValues.ml42
1 files changed, 1 insertions, 41 deletions
diff --git a/compiler/PrimitiveValues.ml b/compiler/PrimitiveValues.ml
index 0bf37256..0eacca9e 100644
--- a/compiler/PrimitiveValues.ml
+++ b/compiler/PrimitiveValues.ml
@@ -1,41 +1 @@
-(** The primitive values. *)
-
-open Types
-
-(** We use big integers to store the integer values (this way we don't have
- to think about the bounds, nor architecture issues - Rust allows to
- manipulate 128-bit integers for instance).
- *)
-type big_int = Z.t
-
-let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
- match json with
- | `Int i -> Ok (Z.of_int i)
- | `Intlit is -> Ok (Z.of_string is)
- | _ -> Error "not an integer or an integer literal"
-
-let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
-
-let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
- Format.pp_print_string fmt (Z.to_string bi)
-
-let show_big_int (bi : big_int) : string = Z.to_string bi
-
-(** A scalar value
-
- Note that we use unbounded integers everywhere.
- We then harcode the boundaries for the different types.
- *)
-type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
-
-(** A primitive value.
-
- Can be used by operands (in which case it represents a constant) or by
- the interpreter to represent a concrete, primitive value.
- *)
-type primitive_value =
- | Scalar of scalar_value
- | Bool of bool
- | Char of char
- | String of string
-[@@deriving show]
+include Charon.PrimitiveValues