Clean json generation

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.183"
+let supported_charon_version = "0.1.184"

charon-ml/src/GAst.ml

@@ -4,6 +4,7 @@ open Types
 open Meta
 open Expressions
 include Generated_GAst
+include Generated_FullAst
 
 (* FIXME(#287): Avoid derives triggering deprecation warnings *)
 [@@@alert "-deprecated"]
@@ -26,43 +27,16 @@ type trait_declaration_group = TraitDeclId.id g_declaration_group
 type trait_impl_group = TraitImplId.id g_declaration_group [@@deriving show]
 type mixed_declaration_group = item_id g_declaration_group [@@deriving show]
 
-(* Hand-written because the rust equivalent isn't generic *)
-type 'body body =
-  | Body of 'body gexpr_body
-  | TraitMethodWithoutDefault
-  | Extern of string
-  | Intrinsic of { name : string; arg_names : string list }
-  | TargetDispatch of (string * fun_decl_ref) list
-  | Opaque
-  | Missing
-  | Error of error
-[@@deriving show]
-
-(* Hand-written because the rust equivalent isn't generic *)
-type 'body gfun_decl = {
-  def_id : FunDeclId.id;
-  item_meta : item_meta;
-  generics : generic_params;
-  signature : fun_sig;
-  src : item_source;
-  is_global_initializer : GlobalDeclId.id option;
-  body : 'body body;
-}
-[@@deriving show]
-
-type target_info = { target_pointer_size : int; is_little_endian : bool }
-[@@deriving show]
-
 (* Hand-written because the rust equivalent isn't generic *)
 
 (** A crate *)
-type 'fun_body gcrate = {
+type crate = {
   name : string;
   options : cli_options;
   target_information : (string * target_info) list;
   declarations : declaration_group list;
   type_decls : type_decl TypeDeclId.Map.t;
-  fun_decls : 'fun_body gfun_decl FunDeclId.Map.t;
+  fun_decls : fun_decl FunDeclId.Map.t;
   global_decls : global_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;

charon-ml/src/GAstUtils.ml

@@ -50,7 +50,7 @@ let fun_body_get_input_vars (fbody : 'body gexpr_body) : local list =
 
 (** Get the signature of this function as a bound value, i.e. including its
     generics parameters. *)
-let bound_fun_sig_of_decl (def : 'a gfun_decl) : bound_fun_sig =
+let bound_fun_sig_of_decl (def : fun_decl) : bound_fun_sig =
   { item_binder_params = def.generics; item_binder_value = def.signature }
 
 (** Lookup a method in this trait decl. The two levels of binders in the output
@@ -112,6 +112,32 @@ let declaration_group_to_list (g : declaration_group) : item_id list =
       List.map (fun id -> IdTraitImpl id) (g_declaration_group_to_list g)
   | MixedGroup g -> g_declaration_group_to_list g
 
+let body_as_structured : body -> LlbcAst.expr_body option = function
+  | StructuredBody body -> Some body
+  | _ -> None
+
+let body_as_structured_exn : body -> LlbcAst.expr_body = function
+  | StructuredBody body -> body
+  | _ -> failwith "Expected a structured body"
+
+let body_as_unstructured : body -> UllbcAst.expr_body option = function
+  | UnstructuredBody body -> Some body
+  | _ -> None
+
+let body_as_unstructured_exn : body -> UllbcAst.expr_body = function
+  | UnstructuredBody body -> body
+  | _ -> failwith "Expected an unstructured body"
+
+let has_body : body -> bool = function
+  | StructuredBody _ | UnstructuredBody _ -> true
+  | IntrinsicBody _
+  | ExternBody _
+  | OpaqueBody
+  | TraitMethodWithoutDefaultBody
+  | TargetDispatchBody _
+  | MissingBody
+  | ErrorBody _ -> false
+
 (** Split a module's declarations between types, functions and globals *)
 let split_declarations (decls : declaration_group list) :
     type_declaration_group list

charon-ml/src/LlbcAst.ml

@@ -6,11 +6,7 @@ include GAst
 include Generated_LlbcAst
 
 type expr_body = block gexpr_body [@@deriving show]
-type fun_body = block body [@@deriving show]
-type fun_decl = block gfun_decl [@@deriving show]
-
-(** LLBC crate *)
-type crate = block gcrate [@@deriving show]
+type fun_body = expr_body [@@deriving show]
 
 (* Ancestors for the type_decl visitors *)
 class ['self] iter_statement =