Update the code following a refactor on Charon's side

4 files changed, 27 insertions, 12 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index d819768b..b646a53d 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -214,7 +214,9 @@ let () =
 
       (* Print a warning if the crate contains loops (loops are experimental for now) *)
       let has_loops =
-        List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions
+        A.FunDeclId.Map.exists
+          (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops)
+          m.functions
       in
       if has_loops then log#lwarning (lazy "Support for loops is experimental");
 
@@ -222,7 +224,9 @@ let () =
          whenever there are opaque functions *)
       if
         !backend = Lean
-        && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions
+        && A.FunDeclId.Map.exists
+             (fun _ (d : A.fun_decl) -> d.body = None)
+             m.functions
         && not !split_files
       then (
         log#error
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 449463c8..154c5a21 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -15,7 +15,9 @@ let log = L.interpreter_log
 let compute_type_fun_global_contexts (m : A.crate) :
     C.type_context * C.fun_context * C.global_context =
   let type_decls_list, _, _ = split_declarations m.declarations in
-  let type_decls, fun_decls, global_decls = compute_defs_maps m in
+  let type_decls = m.types in
+  let fun_decls = m.functions in
+  let global_decls = m.globals in
   let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
     split_declarations_to_group_maps m.declarations
   in
@@ -488,7 +490,7 @@ module Test = struct
    *)
   let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDeclId.nth crate.functions fid in
+    let fdef = A.FunDeclId.Map.find fid crate.functions in
     let body = Option.get fdef.body in
 
     (* Debug *)
@@ -541,11 +543,15 @@ module Test = struct
 
   (** Test all the unit functions in a list of function definitions *)
   let test_unit_functions (crate : A.crate) : unit =
-    let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
-    let test_unit_fun (def : A.fun_decl) : unit =
+    let unit_funs =
+      A.FunDeclId.Map.filter
+        (fun _ -> fun_decl_is_transparent_unit)
+        crate.functions
+    in
+    let test_unit_fun _ (def : A.fun_decl) : unit =
       test_unit_function crate def.A.def_id
     in
-    List.iter test_unit_fun unit_funs
+    A.FunDeclId.Map.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
   let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 8b193ee2..b348ba1d 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -426,7 +426,9 @@ let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
 let apply_passes (crate : A.crate) : A.crate =
   let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
   let functions =
-    List.fold_left (fun fl pass -> List.map pass fl) crate.functions passes
+    List.fold_left
+      (fun fl pass -> A.FunDeclId.Map.map pass fl)
+      crate.functions passes
   in
   let crate = { crate with functions } in
   log#ldebug
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6c6435c5..70ef5e3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -291,7 +291,9 @@ let translate_crate_to_pure (crate : A.crate) :
   let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
-  let type_decls = SymbolicToPure.translate_type_decls crate.types in
+  let type_decls =
+    SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
+  in
 
   (* Compute the type definition map *)
   let type_decls_map =
@@ -318,7 +320,7 @@ let translate_crate_to_pure (crate : A.crate) :
                 (LlbcAstUtils.fun_body_get_input_vars body)
         in
         (A.Regular fdef.def_id, input_names, fdef.signature))
-      crate.functions
+      (A.FunDeclId.Map.values crate.functions)
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
@@ -330,7 +332,7 @@ let translate_crate_to_pure (crate : A.crate) :
   let pure_translations =
     List.map
       (translate_function_to_pure trans_ctx fun_sigs type_decls_map)
-      crate.functions
+      (A.FunDeclId.Map.values crate.functions)
   in
 
   (* Apply the micro-passes *)
@@ -989,7 +991,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
 
   let ctx =
-    List.fold_left Extract.extract_global_decl_register_names ctx crate.globals
+    List.fold_left Extract.extract_global_decl_register_names ctx
+      (A.GlobalDeclId.Map.values crate.globals)
   in
 
   (* Open the output file *)