diff options
| -rw-r--r-- | .gitignore | 4 | ||||
| -rw-r--r-- | src/CfimAst.ml | 2 | ||||
| -rw-r--r-- | src/Values.ml | 2 | ||||
| -rw-r--r-- | src/main.ml | 46 |
4 files changed, 26 insertions, 28 deletions
@@ -27,3 +27,7 @@ setup.log # Local OPAM switch _opam/ + +# Misc +*~ +nohup.out
\ No newline at end of file diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 66e3fb0c..bb821bb7 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -3,6 +3,8 @@ open Types open Values open Expressions +module FunDefId = IdGen () + type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree [@@deriving of_yojson] diff --git a/src/Values.ml b/src/Values.ml index bc917d85..992b43ea 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -3,8 +3,6 @@ open Types module VarId = IdGen () -module FunDefId = IdGen () - type var = { index : VarId.id; (** Unique variable identifier *) name : string option; diff --git a/src/main.ml b/src/main.ml index 850c7bcf..3a1d56ed 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,29 +1,23 @@ -open Identifiers -(*open CfimAst*) - -module Id0 = IdGen () - -module Id1 = IdGen () - -let x0 = Id0.zero - -let x1 = Id0.incr x0 - -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] +open Types +open CfimAst + +type declaration = + | Type of TypeDefId.id + | 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_file "../charon/charon/tests/test1.cfim" in *) - let _json = Yojson.Safe.from_file "../charon/charon/tests/test1.cfim" in - let _test = CfimAst.fun_def_of_yojson _json in - () + let json = Yojson.Safe.from_file "../charon/charon/tests/test1.cfim" in + match rust_module_of_yojson json with + | Error s -> Printf.printf "error: %s\n" s + | Ok _ast -> print_endline "ast" |