diff options
| -rw-r--r-- | src/CfimAst.ml | 10 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 4 | ||||
| -rw-r--r-- | src/Expressions.ml | 15 | ||||
| -rw-r--r-- | src/Identifiers.ml | 21 | ||||
| -rw-r--r-- | src/Types.ml | 20 | ||||
| -rw-r--r-- | src/Values.ml | 4 | ||||
| -rw-r--r-- | src/dune | 3 | ||||
| -rw-r--r-- | src/main.ml | 2 |
8 files changed, 20 insertions, 59 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 80165371..85d4c56e 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -6,12 +6,10 @@ open Expressions module FunDefId = IdGen () type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree -[@@deriving yojson] type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id -[@@deriving yojson] -type assertion = { cond : operand; expected : bool } [@@deriving yojson] +type assertion = { cond : operand; expected : bool } type fun_sig = { region_params : region_var RegionVarId.vector; @@ -20,7 +18,6 @@ type fun_sig = { inputs : rty VarId.vector; output : rty; } -[@@deriving yojson] type call = { func : fun_id; @@ -29,7 +26,6 @@ type call = { args : operand list; dest : place; } -[@@deriving yojson] type statement = | Assign of place * rvalue @@ -50,14 +46,12 @@ type statement = (** Continue to (outer) loop. The loop identifier works the same way as for [Break] *) | Nop -[@@deriving yojson] type expression = | Statement of statement | Sequence of expression * expression | Switch of operand * switch_targets | Loop of expression -[@@deriving yojson] and switch_targets = | If of expression * expression (** Gives the "if" and "else" blocks *) @@ -67,7 +61,6 @@ and switch_targets = - the "otherwise" expression. Also note that we precise the type of the integer (uint32, int64, etc.) which we switch on. *) -[@@deriving yojson] type fun_def = { def_id : FunDefId.id; @@ -78,4 +71,3 @@ type fun_def = { locals : var VarId.vector; body : expression; } -[@@deriving yojson] diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index b60c2247..cfe408f7 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -103,7 +103,7 @@ let region_var_of_json (js : json) : (region_var, string) result = let region_of_json (js : json) : (RegionVarId.id region, string) result = combine_error_msgs js "region_of_json" (match js with - | `String "Static" -> Ok Static (* TODO *) + | `String "Static" -> Ok Static | `Assoc [ ("Var", rid) ] -> let* rid = RegionVarId.id_of_json rid in Ok (Var rid) @@ -115,7 +115,7 @@ let erased_region_of_json (js : json) : (erased_region, string) result = let integer_type_of_json (js : json) : (integer_type, string) result = match js with - | `String "Isize" -> Ok Isize (* TODO *) + | `String "Isize" -> Ok Isize | `String "I8" -> Ok I8 | `String "I16" -> Ok I16 | `String "I32" -> Ok I32 diff --git a/src/Expressions.ml b/src/Expressions.ml index 0a8c9d35..66cf5197 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -4,22 +4,20 @@ open Values type field_proj_kind = | ProjAdt of TypeDefId.id * VariantId.id option | ProjTuple of int -[@@deriving yojson] type projection_elem = | Deref | DerefBox | Field of field_proj_kind * FieldId.id | Downcast of VariantId.id -[@@deriving yojson] -type projection = projection_elem list [@@deriving yojson] +type projection = projection_elem list -type place = { var_id : VarId.id; projection : projection } [@@deriving yojson] +type place = { var_id : VarId.id; projection : projection } -type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving yojson] +type borrow_kind = Shared | Mut | TwoPhaseMut -type unop = Not | Neg [@@deriving yojson] +type unop = Not | Neg (** A binary operation @@ -45,7 +43,6 @@ type binop = | Mul | Shl | Shr -[@@deriving yojson] (** Constant value for an operand @@ -64,18 +61,15 @@ type operand_constant_value = | ConstantValue of constant_value | ConstantAdt of TypeDefId.id | Unit -[@@deriving yojson] type operand = | Copy of place | Move of place | Constant of ety * operand_constant_value -[@@deriving yojson] type aggregate_kind = | AggregatedTuple | AggregatedAdt of TypeDefId.id * VariantId.id option -[@@deriving yojson] type rvalue = | Use of operand @@ -84,4 +78,3 @@ type rvalue = | BinaryOp of binop * operand * operand | Discriminant of place | Aggregate of aggregate_kind * operand list -[@@deriving yojson] diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 627c67cc..825e0e40 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -19,23 +19,12 @@ module type Id = sig val empty : 'a vector - val id_of_yojson : Yojson.Safe.t -> (id, string) Result.result - - val id_of_json : Yojson.Basic.t -> (id, string) Result.result - - val id_to_yojson : id -> Yojson.Safe.t - - val vector_of_yojson : - (Yojson.Safe.t -> ('a, string) Result.result) -> - Yojson.Safe.t -> - ('a vector, string) Result.result + val id_of_json : Yojson.Basic.t -> (id, string) result val vector_of_json : - (Yojson.Basic.t -> ('a, string) Result.result) -> + (Yojson.Basic.t -> ('a, string) result) -> Yojson.Basic.t -> - ('a vector, string) Result.result - - val vector_to_yojson : ('a -> Yojson.Safe.t) -> 'a vector -> Yojson.Safe.t + ('a vector, string) result (* TODO: remove *) (* module Map : Map.S with type key = id *) @@ -47,9 +36,9 @@ end *) module IdGen () : Id = struct (* TODO: use Int64.t *) - type id = int [@@deriving yojson] + type id = int - type 'a vector = 'a list [@@deriving yojson] + type 'a vector = 'a list let zero = 0 diff --git a/src/Types.ml b/src/Types.ml index 826531f6..ef8eccf1 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -14,13 +14,11 @@ type type_var = { tv_index : TypeVarId.id; (** Unique index identifying the variable *) tv_name : string; (** Variable name *) } -[@@deriving yojson] type region_var = { rv_index : RegionVarId.id; (** Unique index identifying the region *) rv_name : string option; (** Region name *) } -[@@deriving yojson] (** A region. @@ -31,13 +29,12 @@ type region_var = { type 'rid region = | Static (** Static region *) | Var of 'rid (** Non-static region *) -[@@deriving yojson] (** The type of erased regions. We could use unit, but having a dedicated type makes things more explicit. *) -type erased_region = Erased [@@deriving yojson] +type erased_region = Erased type integer_type = | Isize @@ -52,11 +49,10 @@ type integer_type = | U32 | U64 | U128 -[@@deriving yojson] -type ref_kind = Mut | Shared [@@deriving yojson] +type ref_kind = Mut | Shared -type assumed_ty = Box [@@deriving yojson] +type assumed_ty = Box type 'r ty = | Adt of TypeDefId.id * 'r list * 'r ty list @@ -71,29 +67,26 @@ type 'r ty = | Ref of 'r * 'r ty * ref_kind | Tuple of 'r ty list | Assumed of assumed_ty * 'r list * 'r ty list -[@@deriving yojson] -type rty = RegionVarId.id region ty [@@deriving yojson] +type rty = RegionVarId.id region ty (** Type with *R*egions. Used in function signatures and type definitions. *) -type ety = erased_region ty [@@deriving yojson] +type ety = erased_region ty (** Type with *E*rased regions. Used in function bodies, "general" value types, etc. *) -type field = { field_name : string; field_ty : rty } [@@deriving yojson] +type field = { field_name : string; field_ty : rty } type variant = { variant_name : string; fields : field FieldId.vector } -[@@deriving yojson] type type_def_kind = | Struct of field FieldId.vector | Enum of variant VariantId.vector -[@@deriving yojson] type type_def = { def_id : TypeDefId.id; @@ -102,4 +95,3 @@ type type_def = { type_params : type_var TypeVarId.vector; kind : type_def_kind; } -[@@deriving yojson] diff --git a/src/Values.ml b/src/Values.ml index ba5c7628..e1205efc 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -10,7 +10,7 @@ type var = { (** The variable type - erased type, because variables are not used ** in function signatures *) } -[@@deriving yojson] + (** A variable *) type big_int = Z.t @@ -41,11 +41,9 @@ type scalar_value = | U32 of big_int | U64 of big_int | U128 of big_int -[@@deriving yojson] type constant_value = | Scalar of scalar_value | Bool of bool | Char of char | String of string -[@@deriving yojson] @@ -1,4 +1,3 @@ (executable (name main) - (libraries yojson zarith) - (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving_yojson)))
\ No newline at end of file + (libraries yojson zarith))
\ No newline at end of file diff --git a/src/main.ml b/src/main.ml index d32d9d42..444a416e 100644 --- a/src/main.ml +++ b/src/main.ml @@ -7,14 +7,12 @@ type declaration = | Fun of FunDefId.id | RecTypes of TypeDefId.id list | RecFuns of FunDefId.id list -[@@deriving of_yojson] type rust_module = { declarations : declaration list; types : type_def TypeDefId.vector; functions : fun_def FunDefId.vector; } -[@@deriving of_yojson] let () = (* let json = Yojson.Basic.from_string "{\"Return\"}" in |