diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 1 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 1 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 1 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 3 | ||||
| -rw-r--r-- | compiler/PrimitiveValues.ml | 1 | ||||
| -rw-r--r-- | compiler/PrimitiveValuesUtils.ml | 1 | ||||
| -rw-r--r-- | compiler/Print.ml | 3 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 8 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 1 | ||||
| -rw-r--r-- | compiler/Values.ml | 4 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/dune | 2 |
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 |