summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CfimAst.ml2
-rw-r--r--src/Values.ml2
-rw-r--r--src/main.ml46
3 files changed, 22 insertions, 28 deletions
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"