diff options
| -rw-r--r-- | src/CfimAst.ml | 2 | ||||
| -rw-r--r-- | src/Identifiers.ml | 29 | ||||
| -rw-r--r-- | src/dune | 4 | ||||
| -rw-r--r-- | src/main.ml | 16 |
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"]]) *) @@ -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 + () |