Start working on json deserialization

4 files changed, 47 insertions, 4 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 90eb41cb..1fd8ccd4 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -33,7 +33,7 @@ type statement =
   | Assert of assertion
   | Call of call
   | Panic
-  | Return
+  | Returna
   | Break of int
       (** Break to (outer) loop. The [int] identifies the loop to break to:
           * 0: break to the first outer loop (the current loop)
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index abbca35c..5cf92c09 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,5 +1,11 @@
 exception IntegerOverflow of unit
 
+type gen_int = int [@@deriving of_yojson]
+(** This definition is used only to derive a proper int deserialization function *)
+
+type 'a gen_list = 'a list [@@deriving of_yojson]
+(** This definition is used only to derive a proper list deserialization function *)
+
 (** Signature for a module describing an identifier.
     
     We often need identifiers (for definitions, variables, etc.) and in
@@ -17,6 +23,13 @@ module type Id = sig
 
   val to_string : id -> string
 
+  val id_of_yojson : Yojson.Safe.t -> (id, string) Result.result
+
+  val vector_of_yojson :
+    (Yojson.Safe.t -> ('a, string) Result.result) ->
+    Yojson.Safe.t ->
+    ('a vector, string) Result.result
+
   (* TODO: remove *)
   (* module Map : Map.S with type key = id *)
 end
@@ -40,6 +53,10 @@ module IdGen () : Id = struct
 
   let to_string = string_of_int
 
+  let id_of_yojson json = gen_int_of_yojson json
+
+  let vector_of_yojson a_of_yojson json = gen_list_of_yojson a_of_yojson json
+
   (* TODO: how to make this work? *)
   (* (module Ord : Map.OrderedType = struct
        type t = id
@@ -54,7 +71,17 @@ module IdGen () : Id = struct
 
        let compare = Stdlib.compare
      end) *)
+
+  (* let ord =
+        (module struct
+          type t = id
+
+          let compare = Stdlib.compare
+        end)
+
+     module Map = Map.Make (ord) *)
 end
 
 type name = string list
-(** A name such as: `std::collections::vector` *)
+(** A name such as: `std::collections::vector` (which would be represented as
+    [["std"; "collections"; "vector"]]) *)
diff --git a/src/dune b/src/dune
index 6ab09aa4..2c07ec16 100644
--- a/src/dune
+++ b/src/dune
@@ -1,2 +1,4 @@
 (executable
- (name main))
\ No newline at end of file
+ (name main)
+ (libraries yojson)
+ (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 03522106..3fd2a311 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,5 +1,5 @@
 open Identifiers
-open CfimAst
+(*open CfimAst*)
 
 module Id0 = IdGen ()
 
@@ -13,3 +13,17 @@ let () =
   let _ = print_endline "Hello, world!" in
   let _ = print_endline (Id0.to_string x1) in
   ()
+
+type 'a test_struct = { x : 'a } [@@deriving of_yojson]
+
+type id0_t = Id0.id [@@deriving of_yojson]
+
+let id0_t_test_struct_of_yojson = test_struct_of_yojson id0_t_of_yojson
+
+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
+  ()