Fix some issues and start printing modules

3 files changed, 27 insertions, 7 deletions

diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 90067038..bb0e9b69 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -87,7 +87,7 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
         let* regions = list_of_json r_of_json regions in
         let* types = list_of_json (ty_of_json r_of_json) types in
         Ok (T.Adt (id, regions, types))
-    | `Assoc [ ("T.TypeVar", `List [ id ]) ] ->
+    | `Assoc [ ("TypeVar", `List [ id ]) ] ->
         let* id = T.TypeVarId.id_of_json id in
         Ok (T.TypeVar id)
     | `String "Bool" -> Ok Bool
@@ -283,7 +283,7 @@ let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
     (match js with
     | `String "Deref" -> Ok E.Deref
     | `String "DerefBox" -> Ok E.DerefBox
-    | `Assoc [ ("T.Field", `List [ proj_kind; field_id ]) ] ->
+    | `Assoc [ ("Field", `List [ proj_kind; field_id ]) ] ->
         let* proj_kind = field_proj_kind_of_json proj_kind in
         let* field_id = T.FieldId.id_of_json field_id in
         Ok (E.Field (proj_kind, field_id))
diff --git a/src/Print.ml b/src/Print.ml
index 22774c2a..218b59ba 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -6,6 +6,7 @@ module V = Values
 module E = Expressions
 module A = CfimAst
 module C = Contexts
+module M = Modules
 
 (** Pretty-printing for types *)
 module Types = struct
@@ -821,7 +822,7 @@ end
 module PA = CfimAst (* local module *)
 
 (** Pretty-printing for ASTs (functions based on a definition context) *)
-module DefCtxCfimAst = struct
+module Module = struct
   (** This function pretty-prints a type definition by using a definition
       context *)
   let type_def_to_string (type_context : T.type_def T.TypeDefId.vector)
@@ -881,6 +882,25 @@ module DefCtxCfimAst = struct
       (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) : string =
     let fmt = def_ctx_to_ast_formatter type_context fun_context def in
     PA.fun_def_to_string fmt "" "  " def
+
+  let module_to_string (m : M.cfim_module) : string =
+    (* The types *)
+    let type_defs =
+      List.map
+        (type_def_to_string m.M.types)
+        (T.TypeDefId.vector_to_list m.M.types)
+    in
+
+    (* The functions *)
+    let fun_defs =
+      List.map
+        (fun_def_to_string m.M.types m.M.functions)
+        (A.FunDefId.vector_to_list m.M.functions)
+    in
+
+    (* Put everything together *)
+    let all_defs = List.append type_defs fun_defs in
+    String.concat "\n\n" all_defs
 end
 
 (** Pretty-printing for ASTs (functions based on an evaluation context) *)
diff --git a/src/main.ml b/src/main.ml
index dfa4025c..d2779657 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -4,8 +4,6 @@ open Print
 module T = Types
 module A = CfimAst
 
-(*let print_type_definition =*)
-
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work *)
 let () = Printexc.record_backtrace true
@@ -13,5 +11,7 @@ let () = Printexc.record_backtrace true
 let () =
   let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in
   match cfim_module_of_json json with
-  | Error s -> Printf.printf "error: %s\n" s
-  | Ok _ast -> print_endline "Ok"
+  | Error s -> log#error "error: %s\n" s
+  | Ok m ->
+      (* Print the module *)
+      log#ldebug (lazy (Print.Module.module_to_string m))