Merge pull request #265 from Nadrieril/declarationgroup-mixed

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.14"
+let supported_charon_version = "0.1.15"

charon-ml/src/GAst.ml

@@ -9,6 +9,14 @@ module TraitDeclId = Types.TraitDeclId
 module TraitImplId = Types.TraitImplId
 module TraitClauseId = Types.TraitClauseId
 
+type any_decl_id =
+  | IdFun of FunDeclId.id
+  | IdGlobal of GlobalDeclId.id
+  | IdType of TypeDeclId.id
+  | IdTraitDecl of TraitDeclId.id
+  | IdTraitImpl of TraitImplId.id
+[@@deriving show, ord]
+
 type fun_decl_id = FunDeclId.id [@@deriving show, ord]
 type assumed_fun_id = Expressions.assumed_fun_id [@@deriving show, ord]
 type fun_id = Expressions.fun_id [@@deriving show, ord]
@@ -187,13 +195,16 @@ type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
 type trait_declaration_group = TraitDeclId.id g_declaration_group
 [@@deriving show]
 
+type mixed_declaration_group = any_decl_id g_declaration_group [@@deriving show]
+
 (** Module declaration. Globals cannot be mutually recursive. *)
 type declaration_group =
   | TypeGroup of type_declaration_group
   | FunGroup of fun_declaration_group
   | GlobalGroup of GlobalDeclId.id
   | TraitDeclGroup of trait_declaration_group
   | TraitImplGroup of TraitImplId.id
+  | MixedGroup of mixed_declaration_group
 [@@deriving show]
 
 type 'body gglobal_decl = {

charon-ml/src/GAstOfJson.ml

@@ -1345,6 +1345,31 @@ let trait_implementation_group_of_json (js : json) :
      | NonRecGroup id -> Ok id
      | RecGroup _ -> Error "got mutually dependent trait impls")
 
+let any_decl_id_of_json (js : json) : (any_decl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("Fun", id) ] ->
+        let* id = FunDeclId.id_of_json id in
+        Ok (IdFun id)
+    | `Assoc [ ("Global", id) ] ->
+        let* id = GlobalDeclId.id_of_json id in
+        Ok (IdGlobal id)
+    | `Assoc [ ("Type", id) ] ->
+        let* id = TypeDeclId.id_of_json id in
+        Ok (IdType id)
+    | `Assoc [ ("TraitDecl", id) ] ->
+        let* id = TraitDeclId.id_of_json id in
+        Ok (IdTraitDecl id)
+    | `Assoc [ ("TraitImpl", id) ] ->
+        let* id = TraitImplId.id_of_json id in
+        Ok (IdTraitImpl id)
+    | _ -> Error "")
+
+let mixed_group_of_json (js : json) :
+    (any_decl_id g_declaration_group, string) result =
+  combine_error_msgs js __FUNCTION__
+    (g_declaration_group_of_json any_decl_id_of_json js)
+
 let declaration_group_of_json (js : json) : (declaration_group, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -1363,6 +1388,9 @@ let declaration_group_of_json (js : json) : (declaration_group, string) result =
     | `Assoc [ ("TraitImpl", decl) ] ->
         let* id = trait_implementation_group_of_json decl in
         Ok (TraitImplGroup id)
+    | `Assoc [ ("Mixed", decl) ] ->
+        let* id = mixed_group_of_json decl in
+        Ok (MixedGroup id)
     | _ -> Error "")
 
 let length_of_json_list (js : json) : (int, string) result =

charon-ml/src/GAstUtils.ml

@@ -41,29 +41,37 @@ let gexpr_body_get_input_vars (fbody : 'body gexpr_body) : var list =
 let fun_body_get_input_vars (fbody : 'body gexpr_body) : var list =
   gexpr_body_get_input_vars fbody
 
+let g_declaration_group_to_list (g : 'a g_declaration_group) : 'a list =
+  match g with RecGroup ids -> ids | NonRecGroup id -> [ id ]
+
 (** Split a module's declarations between types, functions and globals *)
 let split_declarations (decls : declaration_group list) :
     type_declaration_group list
     * fun_declaration_group list
     * GlobalDeclId.id list
     * trait_declaration_group list
-    * TraitImplId.id list =
+    * TraitImplId.id list
+    * mixed_declaration_group list =
   let rec split decls =
     match decls with
-    | [] -> ([], [], [], [], [])
+    | [] -> ([], [], [], [], [], [])
     | d :: decls' -> (
-        let types, funs, globals, trait_decls, trait_impls = split decls' in
+        let types, funs, globals, trait_decls, trait_impls, mixeds =
+          split decls'
+        in
         match d with
         | TypeGroup decl ->
-            (decl :: types, funs, globals, trait_decls, trait_impls)
+            (decl :: types, funs, globals, trait_decls, trait_impls, mixeds)
         | FunGroup decl ->
-            (types, decl :: funs, globals, trait_decls, trait_impls)
+            (types, decl :: funs, globals, trait_decls, trait_impls, mixeds)
         | GlobalGroup decl ->
-            (types, funs, decl :: globals, trait_decls, trait_impls)
+            (types, funs, decl :: globals, trait_decls, trait_impls, mixeds)
         | TraitDeclGroup decl ->
-            (types, funs, globals, decl :: trait_decls, trait_impls)
+            (types, funs, globals, decl :: trait_decls, trait_impls, mixeds)
         | TraitImplGroup decl ->
-            (types, funs, globals, trait_decls, decl :: trait_impls))
+            (types, funs, globals, trait_decls, decl :: trait_impls, mixeds)
+        | MixedGroup decls ->
+            (types, funs, globals, trait_decls, trait_impls, decls :: mixeds))
   in
   split decls
 
@@ -88,9 +96,11 @@ let split_declarations_to_group_maps (decls : declaration_group list) :
         M.key g_declaration_group M.t =
       List.fold_left add_group M.empty groups
   end in
-  let types, funs, globals, trait_decls, trait_impls =
+  let types, funs, globals, trait_decls, trait_impls, mixed_groups =
     split_declarations decls
   in
+  if List.length mixed_groups <> 0 then
+    raise (Failure "Mixed declaration groups cannot be indexed by declaration");
   let module TG = G (TypeDeclId.Map) in
   let types = TG.create_map types in
   let module FG = G (FunDeclId.Map) in

charon-ml/src/LlbcAstUtils.ml

@@ -82,5 +82,9 @@ let compute_fun_decl_groups_map (c : crate) : FunDeclId.Set.t FunDeclId.Map.t =
                 Some (List.map (fun id -> (id, idset)) ids)
             | TypeGroup _ | GlobalGroup _ | TraitDeclGroup _ | TraitImplGroup _
               ->
-                None)
+                None
+            | MixedGroup _ ->
+                raise
+                  (Failure
+                     "Mixed declaration groups cannot be indexed by declaration"))
           c.declarations))

charon-ml/src/PrintGAst.ml

@@ -7,6 +7,14 @@ open PrintUtils
 open PrintTypes
 open PrintExpressions
 
+let any_decl_id_to_string (id : any_decl_id) : string =
+  match id with
+  | IdFun id -> FunDeclId.to_string id
+  | IdGlobal id -> GlobalDeclId.to_string id
+  | IdType id -> TypeDeclId.to_string id
+  | IdTraitDecl id -> TraitDeclId.to_string id
+  | IdTraitImpl id -> TraitImplId.to_string id
+
 let fn_operand_to_string (env : ('a, 'b) fmt_env) (op : fn_operand) : string =
   match op with
   | FnOpRegular func -> fn_ptr_to_string env func

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.14"
+version = "0.1.15"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 

charon/src/pretty/fmt_with_ctx.rs

@@ -130,6 +130,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for DeclarationGroup {
             Global(g) => format!("Global decls group: {}", g.fmt_with_ctx(ctx)),
             TraitDecl(g) => format!("Trait decls group: {}", g.fmt_with_ctx(ctx)),
             TraitImpl(g) => format!("Trait impls group: {}", g.fmt_with_ctx(ctx)),
+            Mixed(g) => format!("Mixed group: {}", g.fmt_with_ctx(ctx)),
         }
     }
 }

charon/src/pretty/formatter.rs

@@ -4,7 +4,7 @@ use crate::ids::Vector;
 use crate::llbc_ast;
 use crate::llbc_ast::*;
 use crate::pretty::{fmt_with_ctx, FmtWithCtx};
-use crate::translate_ctx::TranslatedCrate;
+use crate::translate_ctx::{AnyTransId, TranslatedCrate};
 use crate::types::*;
 use crate::ullbc_ast;
 use crate::ullbc_ast as ast;
@@ -174,6 +174,7 @@ pub trait AstFormatter = Formatter<TypeVarId>
     + Formatter<BodyId>
     + Formatter<TraitDeclId>
     + Formatter<TraitImplId>
+    + Formatter<AnyTransId>
     + Formatter<TraitClauseId>
     + Formatter<(DeBruijnId, RegionId)>
     + Formatter<VarId>
@@ -214,6 +215,16 @@ impl<'a> FmtCtx<'a> {
             locals: None,
         }
     }
+
+    pub fn format_decl_id(&self, id: AnyTransId) -> String {
+        match id {
+            AnyTransId::Type(id) => self.format_decl(id),
+            AnyTransId::Fun(id) => self.format_decl(id),
+            AnyTransId::Global(id) => self.format_decl(id),
+            AnyTransId::TraitDecl(id) => self.format_decl(id),
+            AnyTransId::TraitImpl(id) => self.format_decl(id),
+        }
+    }
 }
 
 impl<'a> Default for FmtCtx<'a> {
@@ -294,6 +305,18 @@ impl<'a> Formatter<ast::TraitImplId> for FmtCtx<'a> {
     }
 }
 
+impl<'a> Formatter<AnyTransId> for FmtCtx<'a> {
+    fn format_object(&self, id: AnyTransId) -> String {
+        match id {
+            AnyTransId::Type(x) => self.format_object(x),
+            AnyTransId::Fun(x) => self.format_object(x),
+            AnyTransId::Global(x) => self.format_object(x),
+            AnyTransId::TraitDecl(x) => self.format_object(x),
+            AnyTransId::TraitImpl(x) => self.format_object(x),
+        }
+    }
+}
+
 impl<'a> Formatter<(DeBruijnId, RegionId)> for FmtCtx<'a> {
     fn format_object(&self, (grid, id): (DeBruijnId, RegionId)) -> String {
         match self.region_vars.get(grid.index) {