diff options
| -rw-r--r-- | compiler/Extract.ml | 4 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 17 | ||||
| -rw-r--r-- | compiler/Translate.ml | 46 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml | 2 |
4 files changed, 35 insertions, 34 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index f911290e..73a081a7 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2329,7 +2329,7 @@ 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 (fwd, loop_fwds), back_ls = def in + let { f = fwd; loops = loop_fwds }, back_ls = def in (* Register the decrease clauses, if necessary *) let register_decreases ctx def = if has_decreases_clause def then @@ -2350,7 +2350,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (* Register the backward functions' names *) let ctx = List.fold_left - (fun ctx (back, loop_backs) -> + (fun ctx { f = back; loops = loop_backs } -> let ctx = register_fun ctx back in register_funs ctx loop_backs) ctx back_ls diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 93609695..72e3d05e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1461,7 +1461,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = altogether. *) let keep_forward (trans : pure_fun_translation) : bool = - let (fwd, _), backs = trans in + let { f = 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 @@ -1908,7 +1908,7 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl = [ctx]: used only for printing. *) let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : - (fun_decl * fun_decl list) option = + fun_and_loops option = (* Debug *) log#ldebug (lazy @@ -1949,9 +1949,9 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : let def, loops = decompose_loops def in (* Apply the remaining passes *) - let def = apply_end_passes_to_def ctx def in + let f = apply_end_passes_to_def ctx def in let loops = List.map (apply_end_passes_to_def ctx) loops in - Some (def, loops) + Some { f; loops } (** Small utility for {!filter_loop_inputs} *) let filter_prefix (keep : bool list) (ls : 'a list) : 'a list = @@ -1996,10 +1996,11 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) : (List.concat (List.concat (List.map - (fun (_, ((fwd, loops_fwd), backs)) -> + (fun (_, ({ f = fwd; loops = loops_fwd }, backs)) -> [ fwd :: loops_fwd ] :: List.map - (fun (back, loops_back) -> [ back :: loops_back ]) + (fun { f = back; loops = loops_back } -> + [ back :: loops_back ]) backs) transl))) in @@ -2246,8 +2247,8 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) : let transl = List.map (fun (b, (fwd, backs)) -> - let filter_fun_and_loops (f, fl) = - (filter_in_one f, List.map filter_in_one fl) + 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 diff --git a/compiler/Translate.ml b/compiler/Translate.ml index b26ce23b..2f751693 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 _ ((_, ((t_fwd, _), _)) : bool * pure_fun_translation) -> - Option.is_none t_fwd.body) + (fun _ ((_, (fwd, _)) : bool * pure_fun_translation) -> + Option.is_none fwd.f.body) ctx.trans_funs in (has_opaque_types, has_opaque_funs) @@ -552,7 +552,7 @@ 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 _, ((body, loop_fwds), body_backs) = + let _, ({ f = body; loops = loop_fwds }, body_backs) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in assert (body_backs = []); @@ -676,7 +676,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, loop_fwds), _)) -> + (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 @@ -702,8 +702,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) raise (Failure "HOL4 doesn't have decreases/termination clauses") in - extract_decrease fwd; - List.iter extract_decrease loop_fwds) + extract_decrease fwd.f; + List.iter extract_decrease fwd.loops) pure_ls; (* Concatenate the function definitions, filtering the useless forward @@ -711,12 +711,12 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let decls = List.concat (List.map - (fun (keep_fwd, ((fwd, fwd_loops), (back_ls : fun_and_loops list))) -> - let fwd = if keep_fwd then List.append fwd_loops [ fwd ] else [] in + (fun (keep_fwd, (fwd, (back_ls : fun_and_loops list))) -> + let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in let back : Pure.fun_decl list = List.concat (List.map - (fun (back, loop_backs) -> List.append loop_backs [ back ]) + (fun back -> List.append back.loops [ back.f ]) back_ls) in List.append fwd back) @@ -737,8 +737,8 @@ 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) + (fun (keep_fwd, (fwd, _)) -> + if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd.f) pure_ls (** Export a trait declaration. *) @@ -790,7 +790,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 (fst (snd pure_fun))).Pure.kind with + match (fst (snd pure_fun)).f.Pure.kind with | TraitMethodDecl _ -> () | _ -> (* Translate *) @@ -995,18 +995,18 @@ 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, loop_fwds), _)) -> - let fwd = - if fwd.Pure.signature.info.effect_info.is_rec then - [ (fwd.def_id, None) ] + (fun (_, (fwd, _)) -> + let fwd_f = + if fwd.f.Pure.signature.info.effect_info.is_rec then + [ (fwd.f.def_id, None) ] else [] in let loop_fwds = List.map (fun (def : Pure.fun_decl) -> [ (def.def_id, def.loop_id) ]) - loop_fwds + fwd.loops in - fwd :: loop_fwds) + fwd_f :: loop_fwds) trans_funs in let rec_functions : PureUtils.fun_loop_id list = @@ -1019,11 +1019,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : Pure.TypeDeclId.Map.of_list (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in - let trans_funs = + let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t = A.FunDeclId.Map.of_list (List.map - (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) -> - ((fst fd).def_id, (keep_fwd, (fd, bdl)))) + (fun ((keep_fwd, (fwd, bdl)) : bool * pure_fun_translation) -> + (fwd.f.def_id, (keep_fwd, (fwd, bdl)))) trans_funs) in @@ -1074,10 +1074,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : let ctx = List.fold_left - (fun ctx (keep_fwd, defs) -> + (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 (fst defs) in + let fwd_def = (fst defs).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 34a6434f..9694c95e 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -31,7 +31,7 @@ type trans_ctx = { trait_impls_context : trait_impls_context; } -type fun_and_loops = Pure.fun_decl * Pure.fun_decl list +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 |