From 6cdbb77f2be6f349729e2fd075ca3c51e9365b4f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Aug 2023 17:42:30 +0200
Subject: Update the code following a refactor on Charon's side
---
compiler/Driver.ml | 8 ++++++--
compiler/Interpreter.ml | 16 +++++++++++-----
compiler/PrePasses.ml | 4 +++-
compiler/Translate.ml | 11 +++++++----
4 files changed, 27 insertions(+), 12 deletions(-)
(limited to 'compiler')
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 *)
--
cgit v1.2.3