diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimOfJson.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 22 | ||||
| -rw-r--r-- | src/main.ml | 8 |
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)) |