Cleanup a bit

5 files changed, 58 insertions, 85 deletions

diff --git a/Makefile b/Makefile
index 33f98089..3d318ebc 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ build:
 test: build translate-no_nested_borrows translate-hashmap
 
 # Add specific options to some tests
-translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decrease-clauses
+translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
 translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
 
 # Generic rule to extract the CFIM from a rust file
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a481affd..83eaae9d 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -274,12 +274,12 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
     fname ^ suffix
   in
 
-  let decrease_clause_name (_fid : FunDefId.id) (fname : name) : string =
+  let decreases_clause_name (_fid : FunDefId.id) (fname : name) : string =
     let fname = get_fun_name fname in
     (* Converting to snake case should be a no-op, but it doesn't cost much *)
     let fname = to_snake_case fname in
     (* Compute the suffix *)
-    let suffix = "_decrease" in
+    let suffix = "_decreases" in
     (* Concatenate *)
     fname ^ suffix
   in
@@ -352,7 +352,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
     struct_constructor;
     type_name;
     fun_name;
-    decrease_clause_name;
+    decreases_clause_name;
     var_basename;
     type_var_basename;
     append_index;
@@ -644,11 +644,12 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
     (forward function and backward functions).
  *)
 let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool)
-    (has_decrease_clause : bool) (def : pure_fun_translation) : extraction_ctx =
+    (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx
+    =
   let fwd, back_ls = def in
   (* Register the decrease clause, if necessary *)
   let ctx =
-    if has_decrease_clause then ctx_add_decrase_clause fwd ctx else ctx
+    if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx
   in
   (* Register the forward function name *)
   let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in
@@ -997,15 +998,15 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
     let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
     ```
  *)
-let extract_template_decrease_clause (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_def) : unit =
   (* Retrieve the function name *)
-  let def_name = ctx_get_decrease_clause def.def_id ctx in
+  let def_name = ctx_get_decreases_clause def.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   F.pp_print_string fmt
-    ("(** [" ^ Print.name_to_string def.basename ^ "]: decrease clause *)");
+    ("(** [" ^ Print.name_to_string def.basename ^ "]: decreases clause *)");
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line - TODO: remove? *)
@@ -1043,7 +1044,7 @@ let extract_template_decrease_clause (ctx : extraction_ctx) (fmt : F.formatter)
     it is useful for the decrease clause.
  *)
 let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_def_qualif) (has_decrease_clause : bool) (fwd_def : fun_def)
+    (qualif : fun_def_qualif) (has_decreases_clause : bool) (fwd_def : fun_def)
     (def : fun_def) : unit =
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
@@ -1066,36 +1067,6 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
   in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   let ctx, ctx_body = extract_fun_parameters ctx fmt def in
-  (*(* Print the parameters - rk.: we should have filtered the functions
-   * with no input parameters *)
-  (* The type parameters *)
-  if def.signature.type_params <> [] then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "(";
-    List.iter
-      (fun (p : type_var) ->
-        let pname = ctx_get_type_var p.index ctx in
-        F.pp_print_string fmt pname;
-        F.pp_print_space fmt ())
-      def.signature.type_params;
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0)");
-  (* The input parameters - note that doing this adds bindings to the context *)
-  let ctx_body =
-    List.fold_left
-      (fun ctx (lv : typed_lvalue) ->
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt "(";
-        let ctx = extract_typed_lvalue ctx fmt false lv in
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt ":";
-        F.pp_print_space fmt ();
-        extract_ty ctx fmt false lv.ty;
-        F.pp_print_string fmt ")";
-        ctx)
-      ctx def.inputs_lvs
-  in*)
   (* Print the return type - note that we have to be careful when
    * printing the input values for the decrease clause, because
    * it introduces bindings in the context... We thus "forget"
@@ -1109,15 +1080,15 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
     (* `Tot` *)
-    if has_decrease_clause then (
+    if has_decreases_clause then (
       F.pp_print_string fmt "Tot";
       F.pp_print_space fmt ());
-    extract_ty ctx fmt has_decrease_clause
+    extract_ty ctx fmt has_decreases_clause
       (Collections.List.to_cons_nil def.signature.outputs);
     (* Close the box for the return type *)
     F.pp_close_box fmt ();
     (* Print the decrease clause *)
-    if has_decrease_clause then (
+    if has_decreases_clause then (
       F.pp_print_space fmt ();
       (* Open a box for the decrease clause *)
       F.pp_open_hovbox fmt 0;
@@ -1126,7 +1097,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       F.pp_print_string fmt "(";
       (* The name of the decrease clause *)
-      let decr_name = ctx_get_decrease_clause def.def_id ctx in
+      let decr_name = ctx_get_decreases_clause def.def_id ctx in
       F.pp_print_string fmt decr_name;
       (* Print the type parameters *)
       List.iter
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 4d29d517..04f3c8b9 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -81,7 +81,7 @@ type formatter = {
             (`None` if forward function)
           TODO: use the fun id for the assumed functions.
        *)
-  decrease_clause_name : FunDefId.id -> name -> string;
+  decreases_clause_name : FunDefId.id -> name -> 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.
@@ -174,8 +174,8 @@ type formatter = {
 (** We use identifiers to look for name clashes *)
 type id =
   | FunId of A.fun_id * RegionGroupId.id option
-  | DecreaseClauseId of A.fun_id
-      (** The definition which provides the decrease/termination clause.
+  | DecreasesClauseId of A.fun_id
+      (** The definition which provides the decreases/termination clause.
           We insert calls to this clause to prove/reason about termination:
           the body of those clauses must be defined by the user, in the
           proper files.
@@ -337,14 +337,14 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
         | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
       in
       "fun name (" ^ fun_kind ^ "): " ^ fun_name
-  | DecreaseClauseId fid ->
+  | DecreasesClauseId fid ->
       let fun_name =
         match fid with
         | A.Local fid ->
             Print.name_to_string (FunDefId.Map.find fid fun_defs).name
         | A.Assumed aid -> A.show_assumed_fun_id aid
       in
-      "decrease clause for function: " ^ fun_name
+      "decreases clause for function: " ^ fun_name
   | TypeId id -> "type name: " ^ get_type_name id
   | StructId id -> "struct constructor of: " ^ get_type_name id
   | VariantId (id, variant_id) ->
@@ -446,9 +446,9 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
     (ctx : extraction_ctx) : string =
   ctx_get (VariantId (def_id, variant_id)) ctx
 
-let ctx_get_decrease_clause (def_id : FunDefId.id) (ctx : extraction_ctx) :
+let ctx_get_decreases_clause (def_id : FunDefId.id) (ctx : extraction_ctx) :
     string =
-  ctx_get (DecreaseClauseId (A.Local def_id)) ctx
+  ctx_get (DecreasesClauseId (A.Local def_id)) ctx
 
 (** Generate a unique type variable name and add it to the context *)
 let ctx_add_type_var (basename : string) (id : TypeVarId.id)
@@ -532,10 +532,10 @@ let ctx_add_struct (def : type_def) (ctx : extraction_ctx) :
   let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
   (ctx, name)
 
-let ctx_add_decrase_clause (def : fun_def) (ctx : extraction_ctx) :
+let ctx_add_decrases_clause (def : fun_def) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = ctx.fmt.decrease_clause_name def.def_id def.basename in
-  ctx_add (DecreaseClauseId (A.Local def.def_id)) name ctx
+  let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
+  ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx
 
 let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
     (ctx : extraction_ctx) : extraction_ctx =
diff --git a/src/Translate.ml b/src/Translate.ml
index 82b9f9cc..5a00db64 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -29,12 +29,12 @@ type config = {
           let _ = assert_norm (FUNCTION () = Success ())
           ```
        *)
-  extract_decrease_clauses : bool;
-      (** If true, insert `decrease` clauses for all the recursive definitions.
+  extract_decreases_clauses : bool;
+      (** If true, insert `decreases` clauses for all the recursive definitions.
 
           The body of such clauses must be defined by the user.
        *)
-  extract_template_decrease_clauses : bool;
+  extract_template_decreases_clauses : bool;
       (** In order to help the user, we can generate "template" decrease clauses
           (i.e., definitions with proper signatures but dummy bodies) in a
           dedicated file.
@@ -306,14 +306,14 @@ type gen_ctx = {
   extract_ctx : PureToExtract.extraction_ctx;
   trans_types : Pure.type_def Pure.TypeDefId.Map.t;
   trans_funs : (bool * pure_fun_translation) Pure.FunDefId.Map.t;
-  functions_with_decrease_clause : Pure.FunDefId.Set.t;
+  functions_with_decreases_clause : Pure.FunDefId.Set.t;
 }
 (** Extraction context *)
 
 type gen_config = {
   extract_types : bool;
-  extract_decrease_clauses : bool;
-  extract_template_decrease_clauses : bool;
+  extract_decreases_clauses : bool;
+  extract_template_decreases_clauses : bool;
   extract_fun_defs : bool;
   test_unit_functions : bool;
 }
@@ -332,8 +332,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   in
 
   (* Utility to check a function has a decrease clause *)
-  let has_decrease_clause (def : Pure.fun_def) : bool =
-    Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decrease_clause
+  let has_decreases_clause (def : Pure.fun_def) : bool =
+    Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decreases_clause
   in
 
   (* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -353,12 +353,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            pure_ls)
     in
     (* Extract the decrease clauses template bodies *)
-    if config.extract_template_decrease_clauses then
+    if config.extract_template_decreases_clauses then
       List.iter
         (fun (_, (fwd, _)) ->
-          let has_decr_clause = has_decrease_clause fwd in
+          let has_decr_clause = has_decreases_clause fwd in
           if has_decr_clause then
-            ExtractToFStar.extract_template_decrease_clause ctx.extract_ctx fmt
+            ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
               fwd)
         pure_ls;
     (* Extract the function definitions *)
@@ -382,7 +382,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            else ExtractToFStar.LetRec
          in
          let has_decr_clause =
-           has_decrease_clause def && config.extract_decrease_clauses
+           has_decreases_clause def && config.extract_decreases_clauses
          in
          ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif
            has_decr_clause fwd_def def)
@@ -571,7 +571,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       extract_ctx = ctx;
       trans_types;
       trans_funs;
-      functions_with_decrease_clause = rec_functions;
+      functions_with_decreases_clause = rec_functions;
     }
   in
 
@@ -580,8 +580,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     let base_gen_config =
       {
         extract_types = false;
-        extract_decrease_clauses = config.extract_decrease_clauses;
-        extract_template_decrease_clauses = false;
+        extract_decreases_clauses = config.extract_decreases_clauses;
+        extract_template_decreases_clauses = false;
         extract_fun_defs = false;
         test_unit_functions = false;
       }
@@ -596,15 +596,17 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
     (* Extract the template clauses *)
     (if
-     config.extract_decrease_clauses && config.extract_template_decrease_clauses
+     config.extract_decreases_clauses
+     && config.extract_template_decreases_clauses
     then
      let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
      let clauses_module = module_name ^ ".Clauses.Template" in
      let clauses_config =
-       { base_gen_config with extract_template_decrease_clauses = true }
+       { base_gen_config with extract_template_decreases_clauses = true }
      in
      extract_file clauses_config gen_ctx clauses_filename m.M.name
-       clauses_module ": templates for the decrease clauses" [ types_module ] []);
+       clauses_module ": templates for the decreases clauses" [ types_module ]
+       []);
 
     (* Extract the functions *)
     let fun_filename = extract_filebasename ^ ".Funs.fst" in
@@ -624,9 +626,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     let gen_config =
       {
         extract_types = true;
-        extract_decrease_clauses = config.extract_decrease_clauses;
-        extract_template_decrease_clauses =
-          config.extract_template_decrease_clauses;
+        extract_decreases_clauses = config.extract_decreases_clauses;
+        extract_template_decreases_clauses =
+          config.extract_template_decreases_clauses;
         extract_fun_defs = true;
         test_unit_functions = config.test_unit_functions;
       }
diff --git a/src/main.ml b/src/main.ml
index fdd0576e..7bec093d 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -30,8 +30,8 @@ let () =
   let filter_useless_functions = ref true in
   let test_units = ref false in
   let test_trans_units = ref false in
-  let no_decrease_clauses = ref false in
-  let template_decrease_clauses = ref false in
+  let no_decreases_clauses = ref false in
+  let template_decreases_clauses = ref false in
   let no_split = ref false in
 
   let spec =
@@ -64,15 +64,15 @@ let () =
         Arg.Set test_trans_units,
         " Test the translated unit functions with the target theorem\n\
         \                        prover's normalizer" );
-      ( "-no-decrease-clauses",
-        Arg.Set no_decrease_clauses,
+      ( "-no-decreases-clauses",
+        Arg.Set no_decreases_clauses,
         " Do not add decrease clauses to the recursive definitions" );
       ( "-template-clauses",
-        Arg.Set template_decrease_clauses,
-        " Generate templates for the required decrease clauses, in a\n\
+        Arg.Set template_decreases_clauses,
+        " Generate templates for the required decreases clauses, in a\n\
          `\n\
         \                                dedicated file. Incompatible with \
-         -no-decrease-clauses" );
+         -no-decreases-clauses" );
       ( "-no-split",
         Arg.Set no_split,
         " Don't split the definitions between different files for types, \
@@ -80,7 +80,7 @@ let () =
     ]
   in
   (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
-  assert ((not !no_decrease_clauses) || not !template_decrease_clauses);
+  assert ((not !no_decreases_clauses) || not !template_decreases_clauses);
 
   let spec = Arg.align spec in
   let filenames = ref [] in
@@ -176,8 +176,8 @@ let () =
           mp_config = micro_passes_config;
           split_files = not !no_split;
           test_unit_functions;
-          extract_decrease_clauses = not !no_decrease_clauses;
-          extract_template_decrease_clauses = !template_decrease_clauses;
+          extract_decreases_clauses = not !no_decreases_clauses;
+          extract_template_decreases_clauses = !template_decreases_clauses;
         }
       in
       Translate.translate_module filename dest_dir trans_config m