summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterExpansion.ml1
-rw-r--r--compiler/InterpreterExpansion.mli1
-rw-r--r--compiler/InterpreterExpressions.ml3
-rw-r--r--compiler/InterpreterStatements.ml1
-rw-r--r--compiler/Invariants.ml3
-rw-r--r--compiler/PrimitiveValues.ml1
-rw-r--r--compiler/PrimitiveValuesUtils.ml1
-rw-r--r--compiler/Print.ml3
-rw-r--r--compiler/PrintPure.ml8
-rw-r--r--compiler/SymbolicToPure.ml4
-rw-r--r--compiler/SynthesizeSymbolic.ml1
-rw-r--r--compiler/Values.ml4
-rw-r--r--compiler/ValuesUtils.ml2
-rw-r--r--compiler/dune2
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