diff options
| -rw-r--r-- | compiler/Extract.ml | 3 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 20 | ||||
| -rw-r--r-- | compiler/Translate.ml | 40 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml | 2 |
5 files changed, 33 insertions, 34 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 73a081a7..5c0a08ad 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2329,7 +2329,8 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) : extraction_ctx = - let { f = fwd; loops = loop_fwds }, back_ls = def in + let { f = fwd; loops = loop_fwds } = def.fwd in + let back_ls = def.backs in (* Register the decrease clauses, if necessary *) let register_decreases ctx def = if has_decreases_clause def then diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 26940c0c..7a21d42d 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1197,7 +1197,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let sg = llbc_def.signature in let num_rgs = List.length sg.regions_hierarchy in - let keep_fwd, (_, backs) = trans_group in + let keep_fwd, { fwd = _; backs } = trans_group in let num_backs = List.length backs in let rg_info = match def.back_id with diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 72e3d05e..e97a9cd7 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1461,12 +1461,12 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = altogether. *) let keep_forward (trans : pure_fun_translation) : bool = - let { f = fwd; _ }, backs = trans in + let { fwd; backs } = trans in (* Note that at this point, the output types are no longer seen as tuples: * they should be lists of length 1. *) if !Config.filter_useless_functions - && fwd.signature.output = mk_result_ty mk_unit_ty + && fwd.f.signature.output = mk_result_ty mk_unit_ty && backs <> [] then false else true @@ -1996,8 +1996,8 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) : (List.concat (List.concat (List.map - (fun (_, ({ f = fwd; loops = loops_fwd }, backs)) -> - [ fwd :: loops_fwd ] + (fun (_, { fwd; backs }) -> + [ fwd.f :: fwd.loops ] :: List.map (fun { f = back; loops = loops_back } -> [ back :: loops_back ]) @@ -2246,13 +2246,13 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) : in let transl = List.map - (fun (b, (fwd, backs)) -> + (fun (b, { fwd; backs }) -> let filter_fun_and_loops f = { f = filter_in_one f.f; loops = List.map filter_in_one f.loops } in let fwd = filter_fun_and_loops fwd in let backs = List.map filter_fun_and_loops backs in - (b, (fwd, backs))) + (b, { fwd; backs })) transl in @@ -2278,10 +2278,10 @@ let apply_passes_to_pure_fun_translations (ctx : trans_ctx) let apply_to_one (trans : fun_decl * fun_decl list) : bool * pure_fun_translation = (* Apply the passes to the individual functions *) - let forward, backwards = trans in - let forward = Option.get (apply_passes_to_def ctx forward) in - let backwards = List.filter_map (apply_passes_to_def ctx) backwards in - let trans = (forward, backwards) in + let fwd, backs = trans in + let fwd = Option.get (apply_passes_to_def ctx fwd) in + let backs = List.filter_map (apply_passes_to_def ctx) backs in + let trans = { fwd; backs } in (* Compute whether we need to filter the forward function or not *) (keep_forward trans, trans) in diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 2f751693..7122e462 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -439,8 +439,8 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = in let has_opaque_funs = A.FunDeclId.Map.exists - (fun _ ((_, (fwd, _)) : bool * pure_fun_translation) -> - Option.is_none fwd.f.body) + (fun _ ((_, trans) : bool * pure_fun_translation) -> + Option.is_none trans.fwd.f.body) ctx.trans_funs in (has_opaque_types, has_opaque_funs) @@ -552,11 +552,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : A.GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_context.global_decls in let global = A.GlobalDeclId.Map.find id global_decls in - let _, ({ f = body; loops = loop_fwds }, body_backs) = - A.FunDeclId.Map.find global.body_id ctx.trans_funs - in - assert (body_backs = []); - assert (loop_fwds = []); + let _, trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + assert (trans.fwd.loops = []); + assert (trans.backs = []); + let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in if @@ -676,7 +675,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (* Extract the decrease clauses template bodies *) if config.extract_template_decreases_clauses then List.iter - (fun (_, (fwd, _)) -> + (fun (_, { fwd; _ }) -> (* We only generate decreases clauses for the forward functions, because the termination argument should only depend on the forward inputs. The backward functions thus use the same decreases clauses as the @@ -711,15 +710,13 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let decls = List.concat (List.map - (fun (keep_fwd, (fwd, (back_ls : fun_and_loops list))) -> + (fun (keep_fwd, { fwd; backs }) -> let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in - let back : Pure.fun_decl list = + let backs : Pure.fun_decl list = List.concat - (List.map - (fun back -> List.append back.loops [ back.f ]) - back_ls) + (List.map (fun back -> List.append back.loops [ back.f ]) backs) in - List.append fwd back) + List.append fwd backs) pure_ls) in @@ -737,8 +734,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (* Insert unit tests if necessary *) if config.test_trans_unit_functions then List.iter - (fun (keep_fwd, (fwd, _)) -> - if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd.f) + (fun (keep_fwd, trans) -> + if keep_fwd then + Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f) pure_ls (** Export a trait declaration. *) @@ -790,7 +788,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) extract their type directly in the records we generate for the trait declarations themselves, there is no point in having separate type definitions) *) - match (fst (snd pure_fun)).f.Pure.kind with + match (snd pure_fun).fwd.f.Pure.kind with | TraitMethodDecl _ -> () | _ -> (* Translate *) @@ -995,7 +993,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : * whether we should generate a decrease clause or not. *) let rec_functions = List.map - (fun (_, (fwd, _)) -> + (fun (_, { fwd; _ }) -> let fwd_f = if fwd.f.Pure.signature.info.effect_info.is_rec then [ (fwd.f.def_id, None) ] @@ -1022,8 +1020,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t = A.FunDeclId.Map.of_list (List.map - (fun ((keep_fwd, (fwd, bdl)) : bool * pure_fun_translation) -> - (fwd.f.def_id, (keep_fwd, (fwd, bdl)))) + (fun ((keep_fwd, { fwd; backs }) : bool * pure_fun_translation) -> + (fwd.f.def_id, (keep_fwd, { fwd; backs }))) trans_funs) in @@ -1077,7 +1075,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (fun ctx ((keep_fwd, defs) : bool * pure_fun_translation) -> (* If requested by the user, register termination measures and decreases proofs for all the recursive functions *) - let fwd_def = (fst defs).f in + let fwd_def = defs.fwd.f in let gen_decr_clause (def : Pure.fun_decl) = !Config.extract_decreases_clauses && PureUtils.FunLoopIdSet.mem diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index 9694c95e..9fd27c59 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -33,7 +33,7 @@ type trans_ctx = { type fun_and_loops = { f : Pure.fun_decl; loops : Pure.fun_decl list } type pure_fun_translation_no_loops = Pure.fun_decl * Pure.fun_decl list -type pure_fun_translation = fun_and_loops * fun_and_loops list +type pure_fun_translation = { fwd : fun_and_loops; backs : fun_and_loops list } let trans_ctx_to_type_formatter (ctx : trans_ctx) (type_params : Pure.type_var list) |