diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Driver.ml | 8 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 16 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 4 | ||||
| -rw-r--r-- | compiler/Translate.ml | 11 |
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 *) |