Fix an issue with the names of the loop decreases clauses

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