Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 27 insertions, 13 deletions

diff --git a/src/Modules.ml b/src/Modules.ml
index f52983c6..7f372d09 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -9,10 +9,11 @@ type type_declaration_group = TypeDeclId.id g_declaration_group
 
 type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
 
-(** Module declaration *)
+(** Module declaration. Globals cannot be mutually recursive. *)
 type declaration_group =
   | Type of type_declaration_group
   | Fun of fun_declaration_group
+  | Global of GlobalDeclId.id
 [@@deriving show]
 
 type llbc_module = {
@@ -20,11 +21,14 @@ type llbc_module = {
   declarations : declaration_group list;
   types : type_decl list;
   functions : fun_decl list;
+  globals : global_decl list;
 }
 (** LLBC module - TODO: rename to crate *)
 
 let compute_defs_maps (m : llbc_module) :
-    type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t =
+    type_decl TypeDeclId.Map.t
+    * fun_decl FunDeclId.Map.t
+    * global_decl GlobalDeclId.Map.t =
   let types_map =
     List.fold_left
       (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
@@ -35,28 +39,37 @@ let compute_defs_maps (m : llbc_module) :
       (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
       FunDeclId.Map.empty m.functions
   in
-  (types_map, funs_map)
+  let globals_map =
+    List.fold_left
+      (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
+      GlobalDeclId.Map.empty m.globals
+  in
+  (types_map, funs_map, globals_map)
 
-(** Split a module's declarations between types and functions *)
+(** 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 =
+    type_declaration_group list
+    * fun_declaration_group list
+    * GlobalDeclId.id list =
   let rec split decls =
     match decls with
-    | [] -> ([], [])
+    | [] -> ([], [], [])
     | d :: decls' -> (
-        let types, funs = split decls' in
+        let types, funs, globals = split decls' in
         match d with
-        | Type decl -> (decl :: types, funs)
-        | Fun decl -> (types, decl :: funs))
+        | Type decl -> (decl :: types, funs, globals)
+        | Fun decl -> (types, decl :: funs, globals)
+        | Global decl -> (types, funs, decl :: globals))
   in
   split decls
 
-(** Split a module's declarations into two maps from type/fun ids to
+(** Split a module's declarations into three maps from type/fun/global ids to
     declaration groups.
  *)
 let split_declarations_to_group_maps (decls : declaration_group list) :
     type_declaration_group TypeDeclId.Map.t
-    * fun_declaration_group FunDeclId.Map.t =
+    * fun_declaration_group FunDeclId.Map.t
+    * GlobalDeclId.Set.t =
   let module G (M : Map.S) = struct
     let add_group (map : M.key g_declaration_group M.t)
         (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
@@ -68,9 +81,10 @@ 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 = split_declarations decls in
+  let types, funs, globals = split_declarations decls in
   let module TG = G (TypeDeclId.Map) in
   let types = TG.create_map types in
   let module FG = G (FunDeclId.Map) in
   let funs = FG.create_map funs in
-  (types, funs)
+  let globals = GlobalDeclId.Set.of_list globals in
+  (types, funs, globals)