diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 7 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 32 | ||||
| -rw-r--r-- | compiler/Translate.ml | 10 |
3 files changed, 37 insertions, 12 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index b3d7b49e..518e8979 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -427,13 +427,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ suffix in - let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string - = + let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) + (num_loops : int) (loop_id : LoopId.id option) : string = let fname = fun_name_to_snake_case fname in + let lp_suffix = default_fun_loop_suffix num_loops loop_id in (* Compute the suffix *) let suffix = "_decreases" in (* Concatenate *) - fname ^ suffix + fname ^ lp_suffix ^ suffix in let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index a9b44017..3ad55d37 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -189,7 +189,8 @@ type formatter = { filtered some of them. TODO: use the fun id for the assumed functions. *) - decreases_clause_name : A.FunDeclId.id -> fun_name -> string; + decreases_clause_name : + A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string; (** Generates the name of the definition used to prove/reason about termination. The generated code uses this clause where needed, but its body must be defined by the user. @@ -198,6 +199,9 @@ type formatter = { - function id: this is especially useful to identify whether the function is an assumed function or a local function - function basename + - the number of loops in the parent function. This is used for + the same purpose as in {!field:fun_name}. + - loop identifier, if this is for a loop *) var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. @@ -678,7 +682,10 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) : let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = - let name = ctx.fmt.decreases_clause_name def.def_id def.basename in + let name = + ctx.fmt.decreases_clause_name def.def_id def.basename def.num_loops + def.loop_id + in ctx_add (DecreasesClauseId (Regular def.def_id, def.loop_id)) name ctx let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : @@ -801,6 +808,18 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map = let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = fmt.type_name def.name +(** Helper function: generate a suffix for a function name, i.e., generates + a suffix like "_loop", "loop1", etc. to append to a function name. + *) +let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) : + string = + match loop_id with + | None -> "" + | Some loop_id -> + (* If this is for a loop, generally speaking, we append the loop index. + If this function admits only one loop, we omit it. *) + if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id + (** A helper function: generates a function suffix from a region group information. TODO: move all those helpers. @@ -808,6 +827,8 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) (num_region_groups : int) (rg : region_group_info option) ((keep_fwd, num_backs) : bool * int) : string = + let lp_suff = default_fun_loop_suffix num_loops loop_id in + (* There are several cases: - [rg] is [Some]: this is a forward function: - we add "_fwd" @@ -823,13 +844,6 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) we could not add the "_fwd" suffix) to prevent name clashes between definitions (in particular between type and function definitions). *) - let lp_suff = - match loop_id with - | None -> "" - | Some loop_id -> - if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id - in - let rg_suff = match rg with | None -> "_fwd" diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 66280ed7..966ccf70 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -545,6 +545,16 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) if config.extract_template_decreases_clauses then List.iter (fun (_, ((fwd, loop_fwds), _)) -> + (* 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 + forward function. + + Rem.: we might filter backward functions in {!PureMicroPasses}, but + we don't remove forward functions. Instead, we remember if we should + filter those functions at extraction time with a boolean (see the + type of the [pure_ls] input parameter). + *) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then |