summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/PrintPure.ml115
-rw-r--r--src/Pure.ml2
-rw-r--r--src/SymbolicToPure.ml1
3 files changed, 117 insertions, 1 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
new file mode 100644
index 00000000..000a85d8
--- /dev/null
+++ b/src/PrintPure.ml
@@ -0,0 +1,115 @@
+(** This module defines printing functions for the types defined in Pure.ml *)
+
+open Identifiers
+open Pure
+module T = Types
+module V = Values
+module E = Expressions
+module A = CfimAst
+module TypeDefId = T.TypeDefId
+module TypeVarId = T.TypeVarId
+module RegionId = T.RegionId
+module VariantId = T.VariantId
+module FieldId = T.FieldId
+module SymbolicValueId = V.SymbolicValueId
+module FunDefId = A.FunDefId
+
+type type_formatter = {
+ type_var_id_to_string : T.TypeVarId.id -> string;
+ type_def_id_to_string : T.TypeDefId.id -> string;
+}
+
+type value_formatter = {
+ type_var_id_to_string : T.TypeVarId.id -> string;
+ type_def_id_to_string : T.TypeDefId.id -> string;
+ adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
+ adt_field_names :
+ T.TypeDefId.id -> T.VariantId.id option -> string list option;
+}
+
+let value_to_type_formatter (fmt : value_formatter) : type_formatter =
+ {
+ type_var_id_to_string = fmt.type_var_id_to_string;
+ type_def_id_to_string = fmt.type_def_id_to_string;
+ }
+
+type ast_formatter = {
+ type_var_id_to_string : T.TypeVarId.id -> string;
+ type_def_id_to_string : T.TypeDefId.id -> string;
+ adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
+ adt_field_to_string :
+ T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string;
+ adt_field_names :
+ T.TypeDefId.id -> T.VariantId.id option -> string list option;
+ fun_def_id_to_string : A.FunDefId.id -> string;
+}
+
+let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
+ {
+ type_var_id_to_string = fmt.type_var_id_to_string;
+ type_def_id_to_string = fmt.type_def_id_to_string;
+ adt_variant_to_string = fmt.adt_variant_to_string;
+ adt_field_names = fmt.adt_field_names;
+ }
+
+let ast_to_type_formatter (fmt : ast_formatter) : type_formatter =
+ let fmt = ast_to_value_formatter fmt in
+ value_to_type_formatter fmt
+
+(* TODO: there is a bit of duplication with Print.fun_def_to_ast_formatter *)
+let fun_def_to_ast_formatter (type_defs : T.type_def T.TypeDefId.Map.t)
+ (fun_defs : A.fun_def A.FunDefId.Map.t) (fdef : A.fun_def) : ast_formatter =
+ let type_var_id_to_string vid =
+ let var = T.TypeVarId.nth fdef.signature.type_params vid in
+ Print.Types.type_var_to_string var
+ in
+ let type_def_id_to_string def_id =
+ let def = T.TypeDefId.Map.find def_id type_defs in
+ Print.name_to_string def.name
+ in
+ let adt_variant_to_string =
+ Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_defs
+ in
+ let adt_field_names =
+ Print.Contexts.type_ctx_to_adt_field_names_fun type_defs
+ in
+ let adt_field_to_string =
+ Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_defs
+ in
+ let fun_def_id_to_string def_id =
+ let def = A.FunDefId.Map.find def_id fun_defs in
+ Print.name_to_string def.name
+ in
+ {
+ type_var_id_to_string;
+ type_def_id_to_string;
+ adt_variant_to_string;
+ adt_field_names;
+ adt_field_to_string;
+ fun_def_id_to_string;
+ }
+
+let type_id_to_string (fmt : type_formatter) (id : T.type_id) : string =
+ match id with
+ | T.AdtId id -> fmt.type_def_id_to_string id
+ | T.Tuple -> ""
+ | T.Assumed aty -> (
+ match aty with
+ | Box -> (* Boxes should have been eliminated *) failwith "Unreachable")
+
+let rec ty_to_string (fmt : type_formatter) (ty : ty) : string =
+ match ty with
+ | Adt (id, tys) -> (
+ let tys = List.map (ty_to_string fmt) tys in
+ match id with
+ | T.Tuple -> "(" ^ String.concat " * " tys ^ ")"
+ | T.AdtId _ | T.Assumed _ ->
+ let tys = if tys = [] then "" else " " ^ String.concat " " tys in
+ type_id_to_string fmt id ^ tys)
+ | TypeVar tv -> fmt.type_var_id_to_string tv
+ | Bool -> "bool"
+ | Char -> "char"
+ | Integer int_ty -> Print.Types.integer_type_to_string int_ty
+ | Str -> "str"
+ | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]"
+ | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
diff --git a/src/Pure.ml b/src/Pure.ml
index fc00095f..ba763767 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -20,7 +20,7 @@ module VarId = IdGen ()
type ty =
| Adt of T.type_id * ty list
- (** [Adt] encodes ADTs, tuples and assumed types.
+ (** [Adt] encodes ADTs and tuples and assumed types.
TODO: what about the ended regions? (ADTs may be parameterized
with several region variables. When giving back an ADT value, we may
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 80d08ac4..e246e804 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -10,6 +10,7 @@ module M = Modules
module S = SymbolicAst
module TA = TypesAnalysis
module L = Logging
+module PP = PrintPure
(** The local logger *)
let log = L.symbolic_to_pure_log