Use [@@ëerive of_json] on all the types

7 files changed, 61 insertions, 25 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 1fd8ccd4..66e3fb0c 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -4,10 +4,12 @@ open Values
 open Expressions
 
 type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
+[@@deriving of_yojson]
 
 type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
+[@@deriving of_yojson]
 
-type assertion = { cond : operand; expected : bool }
+type assertion = { cond : operand; expected : bool } [@@deriving of_yojson]
 
 type fun_sig = {
   region_params : region_var RegionVarId.vector;
@@ -16,6 +18,7 @@ type fun_sig = {
   inputs : rty VarId.vector;
   output : rty;
 }
+[@@deriving of_yojson]
 
 type call = {
   func : fun_id;
@@ -24,6 +27,7 @@ type call = {
   args : operand list;
   dest : place;
 }
+[@@deriving of_yojson]
 
 type statement =
   | Assign of place * rvalue
@@ -44,12 +48,14 @@ type statement =
       (** Continue to (outer) loop. The loop identifier works
           the same way as for [Break] *)
   | Nop
+[@@deriving of_yojson]
 
 type expression =
   | Statement of statement
   | Sequence of expression * expression
   | Switch of operand * switch_targets
   | Loop of expression
+[@@deriving of_yojson]
 
 and switch_targets =
   | If of expression * expression  (** Gives the "if" and "else" blocks *)
@@ -59,6 +65,7 @@ and switch_targets =
           - the "otherwise" expression.
           Also note that we precise the type of the integer (uint32, int64, etc.)
           which we switch on. *)
+[@@deriving of_yojson]
 
 type fun_def = {
   def_id : FunDefId.id;
@@ -69,3 +76,4 @@ type fun_def = {
   locals : var VarId.vector;
   body : expression;
 }
+[@@deriving of_yojson]
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6eb5531b..d8fe8d78 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -4,20 +4,23 @@ open Values
 type field_proj_kind =
   | Adt of TypeDefId.id * VariantId.id option
   | Tuple of int
+[@@deriving of_yojson]
 
 type projection_elem =
   | Deref
   | DerefBox
   | Field of field_proj_kind * FieldId.id
   | Downcast of VariantId.id
+[@@deriving of_yojson]
 
-type projection = projection_elem list
+type projection = projection_elem list [@@deriving of_yojson]
 
 type place = { var_id : VarId.id; projection : projection }
+[@@deriving of_yojson]
 
-type borrow_kind = Shared | Mut | TwoPhaseMut
+type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving of_yojson]
 
-type unop = Not | Neg
+type unop = Not | Neg [@@deriving of_yojson]
 
 (** A binary operation
 
@@ -43,6 +46,7 @@ type binop =
   | Mul
   | Shl
   | Shr
+[@@deriving of_yojson]
 
 (** Constant value for an operand
 
@@ -61,13 +65,16 @@ type operand_constant_value =
   | ConstantValue of constant_value
   | Adt of TypeDefId.id
   | Unit
+[@@deriving of_yojson]
 
 type operand =
   | Copy of place
   | Move of place
   | Constant of ety * operand_constant_value
+[@@deriving of_yojson]
 
 type aggregate_kind = Tuple | Adt of TypeDefId.id * VariantId.id list
+[@@deriving of_yojson]
 
 type rvalue =
   | Use of operand
@@ -76,3 +83,4 @@ type rvalue =
   | BinaryOp of binop * operand * operand
   | Discriminant of place
   | Aggregate of aggregate_kind * operand list
+[@@deriving of_yojson]
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 6140b7d4..51b6e473 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -33,6 +33,7 @@ end
     See [Id].
 *)
 module IdGen () : Id = struct
+  (* TODO: use Int64.t *)
   type id = int [@@deriving of_yojson]
 
   type 'a vector = 'a list [@@deriving of_yojson]
@@ -72,6 +73,6 @@ module IdGen () : Id = struct
      module Map = Map.Make (ord) *)
 end
 
-type name = string list
+type name = string list [@@deriving of_yojson]
 (** A name such as: `std::collections::vector` (which would be represented as
     [["std"; "collections"; "vector"]]) *)
diff --git a/src/Types.ml b/src/Types.ml
index d435863e..16cb519d 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -14,11 +14,13 @@ type type_var = {
   index : TypeVarId.id;  (** Unique index identifying the variable *)
   name : string;  (** Variable name *)
 }
+[@@deriving of_yojson]
 
 type region_var = {
   index : RegionVarId.id;  (** Unique index identifying the region *)
   name : string option;  (** Region name *)
 }
+[@@deriving of_yojson]
 
 (** A region.
     
@@ -29,12 +31,13 @@ type region_var = {
 type 'rid region =
   | Static  (** Static region *)
   | Var of 'rid  (** Non-static region *)
+[@@deriving of_yojson]
 
 (** The type of erased regions.
     
     We could use unit, but having a dedicated type makes things more explicit.
  *)
-type erased_region = Erased
+type erased_region = Erased [@@deriving of_yojson]
 
 type integer_type =
   | Isize
@@ -49,10 +52,11 @@ type integer_type =
   | U32
   | U64
   | U128
+[@@deriving of_yojson]
 
-type ref_kind = Mut | Shared
+type ref_kind = Mut | Shared [@@deriving of_yojson]
 
-type assumed_ty = Box
+type assumed_ty = Box [@@deriving of_yojson]
 
 type 'r ty =
   | Adt of TypeDefId.id * 'r list * 'r ty list
@@ -67,26 +71,29 @@ type 'r ty =
   | Ref of 'r * 'r ty * ref_kind
   | Tuple of 'r ty list
   | Assumed of assumed_ty * 'r list * 'r ty
+[@@deriving of_yojson]
 
-type rty = RegionVarId.id region ty
+type rty = RegionVarId.id region ty [@@deriving of_yojson]
 (** Type with *R*egions.
 
     Used in function signatures and type definitions.
  *)
 
-type ety = erased_region ty
+type ety = erased_region ty [@@deriving of_yojson]
 (** Type with *E*rased regions.
     
     Used in function bodies, "general" value types, etc.
  *)
 
-type field = { name : string; ty : rty }
+type field = { name : string; ty : rty } [@@deriving of_yojson]
 
 type variant = { name : string; fields : field FieldId.vector }
+[@@deriving of_yojson]
 
 type type_def_kind =
   | Struct of field FieldId.vector
   | Enum of variant VariantId.vector
+[@@deriving of_yojson]
 
 type type_def = {
   def_id : TypeDefId.id;
@@ -95,3 +102,4 @@ type type_def = {
   type_params : type_var TypeVarId.vector;
   kind : type_def_kind;
 }
+[@@deriving of_yojson]
diff --git a/src/Values.ml b/src/Values.ml
index 006cc8da..bc917d85 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -12,29 +12,40 @@ type var = {
       (** The variable type - erased type, because variables are not used
        ** in function signatures *)
 }
+[@@deriving of_yojson]
 (** A variable *)
 
+type big_int = Z.t
+
+let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
+  match json with
+  | `Int i -> Ok (Z.of_int i)
+  | `Intlit is -> Ok (Z.of_string is)
+  | _ -> Error "not an integer or an integer literal"
+
 (** A scalar value
 
     Note that we use unbounded integers everywhere.
     We then harcode the boundaries for the different types.
  *)
 type scalar_value =
-  | Isize of Big_int.big_int
-  | I8 of Big_int.big_int
-  | I16 of Big_int.big_int
-  | I32 of Big_int.big_int
-  | I64 of Big_int.big_int
-  | I128 of Big_int.big_int
-  | Usize of Big_int.big_int
-  | U8 of Big_int.big_int
-  | U16 of Big_int.big_int
-  | U32 of Big_int.big_int
-  | U64 of Big_int.big_int
-  | U128 of Big_int.big_int
+  | Isize of big_int
+  | I8 of big_int
+  | I16 of big_int
+  | I32 of big_int
+  | I64 of big_int
+  | I128 of big_int
+  | Usize of big_int
+  | U8 of big_int
+  | U16 of big_int
+  | U32 of big_int
+  | U64 of big_int
+  | U128 of big_int
+[@@deriving of_yojson]
 
 type constant_value =
   | Scalar of scalar_value
   | Bool of bool
   | Char of char
   | String of string
+[@@deriving of_yojson]
diff --git a/src/dune b/src/dune
index 2c07ec16..2611eb6e 100644
--- a/src/dune
+++ b/src/dune
@@ -1,4 +1,4 @@
 (executable
  (name main)
- (libraries yojson)
+ (libraries yojson zarith)
  (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving_yojson)))
\ No newline at end of file
diff --git a/src/main.ml b/src/main.ml
index 3fd2a311..850c7bcf 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -25,5 +25,5 @@ type ty1 = int Id0.vector [@@deriving of_yojson]
 let () =
   (*  let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in *)
   let _json = Yojson.Safe.from_file "../charon/charon/tests/test1.cfim" in
-  let _test = ty1_of_yojson _json in
+  let _test = CfimAst.fun_def_of_yojson _json in
   ()