Rename PrimitiveValues to Values

14 files changed, 11 insertions, 24 deletions

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index ff21cd77..d7f5fcd5 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -4,7 +4,6 @@
  * using indices to identify the values for instance). *)
 
 open Types
-open PrimitiveValues
 open Values
 open Contexts
 open TypesUtils
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 6ea75d0b..4be1fd24 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -1,4 +1,3 @@
-open PrimitiveValues
 open Values
 open Contexts
 open Cps
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 38620be0..cc0580be 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -1,4 +1,3 @@
-open PrimitiveValues
 open Types
 open Values
 open LlbcAst
@@ -96,7 +95,7 @@ let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value =
   log#ldebug
     (lazy
       ("literal_to_typed_value:" ^ "\n- cv: "
-      ^ Print.PrimitiveValues.literal_to_string cv));
+      ^ Print.Values.literal_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
   | TBool, VBool v -> { value = VLiteral (VBool v); ty = TLiteral ty }
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 88130f21..e8069e31 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1,6 +1,5 @@
 open Types
 open TypesUtils
-open PrimitiveValues
 open Values
 open ValuesUtils
 open Expressions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 49ba8370..e0e3f354 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -2,7 +2,6 @@
  * are always maintained by evaluation contexts *)
 
 open Types
-open PrimitiveValues
 open Values
 open Contexts
 open Cps
@@ -465,7 +464,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
                     inner_values);
                 (* The length is necessarily concrete *)
                 let len =
-                  (PrimitiveValuesUtils.literal_as_scalar
+                  (ValuesUtils.literal_as_scalar
                      (TypesUtils.const_generic_as_literal cg))
                     .value
                 in
diff --git a/compiler/PrimitiveValues.ml b/compiler/PrimitiveValues.ml
deleted file mode 100644
index 0eacca9e..00000000
--- a/compiler/PrimitiveValues.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.PrimitiveValues
diff --git a/compiler/PrimitiveValuesUtils.ml b/compiler/PrimitiveValuesUtils.ml
deleted file mode 100644
index 0000916d..00000000
--- a/compiler/PrimitiveValuesUtils.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.PrimitiveValuesUtils
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 48a5a20b..92ce6f23 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -10,7 +10,6 @@ open ValuesUtils
 open Expressions
 open LlbcAst
 open Contexts
-module PrimitiveValues = Charon.PrintPrimitiveValues
 module Types = Charon.PrintTypes
 module Expressions = Charon.PrintExpressions
 
@@ -21,6 +20,8 @@ let bool_to_string (b : bool) : string = if b then "true" else "false"
 
 (** Pretty-printing for values *)
 module Values = struct
+  include Charon.PrintValues
+
   let symbolic_value_id_to_pretty_string (id : SymbolicValueId.id) : string =
     "s@" ^ SymbolicValueId.to_string id
 
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index a7ec9336..49e74b6c 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -102,10 +102,10 @@ let adt_field_names (env : fmt_env) =
 let option_to_string = Print.option_to_string
 let type_var_to_string = Print.Types.type_var_to_string
 let const_generic_var_to_string = Print.Types.const_generic_var_to_string
-let integer_type_to_string = Print.PrimitiveValues.integer_type_to_string
-let literal_type_to_string = Print.PrimitiveValues.literal_type_to_string
-let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string
-let literal_to_string = Print.PrimitiveValues.literal_to_string
+let integer_type_to_string = Print.Values.integer_type_to_string
+let literal_type_to_string = Print.Values.literal_type_to_string
+let scalar_value_to_string = Print.Values.scalar_value_to_string
+let literal_to_string = Print.Values.literal_to_string
 
 let assumed_ty_to_string (aty : assumed_ty) : string =
   match aty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6983a0e8..f25ff2f6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,16 +2,14 @@ open Utils
 open LlbcAstUtils
 open Pure
 open PureUtils
-open PrimitiveValues
 open InterpreterUtils
 open FunsAnalysis
 open TypesAnalysis
 module T = Types
-module Id = Identifiers
+module V = Values
 module C = Contexts
 module A = LlbcAst
 module S = SymbolicAst
-module TA = TypesAnalysis
 module PP = PrintPure
 
 (** The local logger *)
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 38efc53a..9e14a4d6 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -1,6 +1,5 @@
 open Types
 open TypesUtils
-open PrimitiveValues
 open Expressions
 open Values
 open SymbolicAst
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 6b1a782c..c1ff9804 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -1,5 +1,6 @@
 open Identifiers
 open Types
+include Charon.Values
 
 (* TODO(SH): I often write "abstract" (value, borrow content, etc.) while I should
  * write "abstraction" (because those values are not abstract, they simply are
@@ -11,9 +12,6 @@ module AbstractionId = IdGen ()
 module FunCallId = IdGen ()
 module LoopId = IdGen ()
 
-type big_int = PrimitiveValues.big_int [@@deriving show, ord]
-type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
-type literal = PrimitiveValues.literal [@@deriving show, ord]
 type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
 type symbolic_value_id_set = SymbolicValueId.Set.t [@@deriving show, ord]
 type loop_id = LoopId.id [@@deriving show, ord]
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 0d3533c2..2c7d213f 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -2,7 +2,7 @@ open Utils
 open TypesUtils
 open Types
 open Values
-include PrimitiveValuesUtils
+include Charon.ValuesUtils
 
 (** Utility exception *)
 exception FoundSymbolicValue of symbolic_value
diff --git a/compiler/dune b/compiler/dune
index 39ad6260..4bba6a08 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -51,8 +51,6 @@
   PrePasses
   Print
   PrintPure
-  PrimitiveValues
-  PrimitiveValuesUtils
   PureMicroPasses
   Pure
   PureTypeCheck