summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-24 17:43:43 +0100
committerSon Ho2022-01-24 17:43:43 +0100
commit87920de32e7704be6b490462b241626f18cc96f7 (patch)
treee8ac77ecba0ea5696a7744529986267473624e12
parente5dce61f35fcc0e716f7aadc32f254c8ba103887 (diff)
Start working on translation of the type definitions
-rw-r--r--src/Identifiers.ml2
-rw-r--r--src/Pure.ml19
-rw-r--r--src/SymbolicToPure.ml82
3 files changed, 102 insertions, 1 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 4880a19a..0a3e1c9d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -151,7 +151,7 @@ type name = string list [@@deriving show, ord]
(** A name such as: `std::collections::vector` (which would be represented as
[["std"; "collections"; "vector"]]) *)
-module NameOrderedType : C.OrderedType = struct
+module NameOrderedType : C.OrderedType with type t = name = struct
type t = name
let compare = compare_name
diff --git a/src/Pure.ml b/src/Pure.ml
index 4201c4b6..fcf8e6f0 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -3,6 +3,7 @@ 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
@@ -30,6 +31,24 @@ type ty =
| Str
| Array of ty (* TODO: there should be a constant with the array *)
| Slice of ty
+[@@deriving show]
+
+type field = { field_name : string; field_ty : ty } [@@deriving show]
+
+type variant = { variant_name : string; fields : field list } [@@deriving show]
+
+type type_def_kind = Struct of field list | Enum of variant list
+[@@deriving show]
+
+type type_var = T.type_var [@@deriving show]
+
+type type_def = {
+ def_id : TypeDefId.id;
+ name : name;
+ type_params : type_var list;
+ kind : type_def_kind;
+}
+[@@deriving show]
type scalar_value = V.scalar_value
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 7792db4b..8980361a 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -4,7 +4,9 @@ module T = Types
module V = Values
module E = Expressions
module A = CfimAst
+module M = Modules
module S = SymbolicAst
+open Pure
type name =
| FunName of A.FunDefId.id * V.BackwardFunctionId.id option
@@ -89,3 +91,83 @@ let fun_to_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) :
| x :: n -> x :: add_to_last n
in
add_to_last fdef.name
+
+(** Generates a name for a type (simply reuses the name in the definition) *)
+let type_to_name (def : T.type_def) : Id.name = def.T.name
+
+type type_context = { type_defs : type_def TypeDefId.Map.t }
+
+type fun_context = unit
+(** TODO *)
+
+type synth_ctx = {
+ names : NameMap.t;
+ type_context : type_context;
+ fun_context : fun_context;
+ declarations : M.declaration_group list;
+}
+
+let rec translate_sty (ctx : synth_ctx) (ty : T.sty) : ty =
+ let translate = translate_sty ctx in
+ match ty with
+ | T.Adt (type_id, regions, tys) ->
+ assert (regions = []);
+ let tys = List.map translate tys in
+ Adt (type_id, tys)
+ | TypeVar vid -> TypeVar vid
+ | Bool -> Bool
+ | Char -> Char
+ | Never -> failwith "Unreachable"
+ | Integer int_ty -> Integer int_ty
+ | Str -> Str
+ | Array ty -> Array (translate ty)
+ | Slice ty -> Slice (translate ty)
+ | Ref (_, rty, _) -> translate rty
+
+let translate_field (ctx : synth_ctx) (f : T.field) : field =
+ let field_name = f.field_name in
+ let field_ty = translate_sty ctx f.field_ty in
+ { field_name; field_ty }
+
+let translate_fields (ctx : synth_ctx) (fl : T.field list) : field list =
+ List.map (translate_field ctx) fl
+
+let translate_variant (ctx : synth_ctx) (v : T.variant) : variant =
+ let variant_name = v.variant_name in
+ let fields = translate_fields ctx v.fields in
+ { variant_name; fields }
+
+let translate_variants (ctx : synth_ctx) (vl : T.variant list) : variant list =
+ List.map (translate_variant ctx) vl
+
+(** Translate a type def kind to IM *)
+let translate_type_def_kind (ctx : synth_ctx) (kind : T.type_def_kind) :
+ type_def_kind =
+ match kind with
+ | T.Struct fields -> Struct (translate_fields ctx fields)
+ | T.Enum variants -> Enum (translate_variants ctx variants)
+
+(** Translate a type definition from IM
+
+ TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
+ point of moving this definition for now.
+ *)
+let translate_type_def (ctx : synth_ctx) (def : T.type_def) :
+ synth_ctx * type_def =
+ (* Translate *)
+ let def_id = def.T.def_id in
+ let name = type_to_name def in
+ let type_params = def.type_params in
+ let kind = translate_type_def_kind ctx def.T.kind in
+ let def = { def_id; name; type_params; kind } in
+ (* Insert in the context *)
+ (* type context *)
+ let type_context = ctx.type_context in
+ let type_defs = type_context.type_defs in
+ let type_defs = TypeDefId.Map.add def_id def type_defs in
+ let type_context = { type_defs } in
+ (* names map *)
+ let names = NameMap.add (TypeName def_id) name ctx.names in
+ (* update the fields *)
+ let ctx = { ctx with type_context; names } in
+ (ctx, def)