Consistently use the names TerminationMeasure and DecreasesProof

5 files changed, 108 insertions, 61 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1c3d14ff..1baed7fa 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -9,7 +9,11 @@ let backend_names = [ "fstar"; "coq"; "lean" ]
 
 (** Utility to compute the backend from an input parameter *)
 let backend_of_string (b : string) : backend option =
-  match b with "fstar" -> Some FStar | "coq" -> Some Coq | "lean" -> Some Lean | _ -> None
+  match b with
+  | "fstar" -> Some FStar
+  | "coq" -> Some Coq
+  | "lean" -> Some Lean
+  | _ -> None
 
 let opt_backend : backend option ref = ref None
 
@@ -174,16 +178,21 @@ let test_unit_functions = ref false
  *)
 let test_trans_unit_functions = ref false
 
-(** If [true], insert [decreases] clauses for all the recursive definitions.
+(** If [true], use decreases clauses/termination measures for all the recursive definitions.
 
-    The body of such clauses must be defined by the user.
+    More precisely:
+    - for F*, we generate definitions which use decreases clauses
+    - for Lean, we generate definitions which use termination measures and
+      decreases proofs
+
+    The body of such clauses/proofs must be defined by the user.
  *)
 let extract_decreases_clauses = ref false
 
-(** 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.
- *)
+(** In order to help the user, we can generate "template" decrease clauses/ termination
+   measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
+   file.
+*)
 let extract_template_decreases_clauses = ref false
 
 (** {1 Micro passes} *)
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 149e2aad..e0504903 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -66,24 +66,26 @@ let () =
     [
       ( "-backend",
         Arg.Symbol (backend_names, set_backend),
-        " Specify the backend to which to extract" );
+        " Specify the target backend" );
       ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
       ( "-no-filter-useless-calls",
         Arg.Clear filter_useless_monadic_calls,
-        " Do not filter the useless function calls, when possible" );
+        " Do not filter the useless function calls" );
       ( "-no-filter-useless-funs",
         Arg.Clear filter_useless_functions,
         " Do not filter the useless forward/backward functions" );
       ( "-test-units",
         Arg.Set test_unit_functions,
-        " Test the unit functions with the concrete interpreter" );
+        " Test the unit functions with the concrete (i.e., not symbolic) \
+         interpreter" );
       ( "-test-trans-units",
         Arg.Set test_trans_unit_functions,
-        " Test the translated unit functions with the target theorem\n\
-        \                             prover's normalizer" );
+        " Test the translated unit functions with the target theorem prover's \
+         normalizer" );
       ( "-decreases-clauses",
         Arg.Set extract_decreases_clauses,
-        " Use decreases clauses for the recursive definitions" );
+        " Use decreases clauses/termination measures for the recursive \
+         definitions" );
       ( "-no-state",
         Arg.Clear use_state,
         " Do not use state-error monads, simply use error monads" );
@@ -95,16 +97,16 @@ let () =
         " Forbid backward functions from updating the state" );
       ( "-template-clauses",
         Arg.Set extract_template_decreases_clauses,
-        " Generate templates for the required decreases clauses, in a \
-         dedicated file. Implies -decreases-clauses" );
+        " Generate templates for the required decreases clauses/termination \
+         measures, in a dedicated file. Implies -decreases-clauses" );
       ( "-no-split-files",
         Arg.Clear split_files,
-        " Don't split the definitions between different files for types, \
+        " Do not split the definitions between different files for types, \
          functions, etc." );
       ( "-no-check-inv",
         Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every step of \
-         evaluation. Dramatically saves speed." );
+        " Deactivate the invariant sanity checks performed at every evaluation \
+         step. Dramatically increases speed." );
     ]
   in
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 35e5d64c..95ba2f02 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -492,22 +492,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name)
+  let termination_measure_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
+    let suffix =
+      match !Config.backend with
+      | FStar -> "_decreases"
+      | Lean -> "_terminates"
+      | Coq -> raise (Failure "Unexpected")
+    in
     (* Concatenate *)
     fname ^ lp_suffix ^ suffix
   in
 
-  let terminates_clause_name (_fid : A.FunDeclId.id) (fname : fun_name)
+  let decreases_proof_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 = "_terminates" in
+    let suffix =
+      match !Config.backend with
+      | Lean -> "_decreases"
+      | FStar | Coq -> raise (Failure "Unexpected")
+    in
     (* Concatenate *)
     fname ^ lp_suffix ^ suffix
   in
@@ -640,8 +649,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     type_name;
     global_name;
     fun_name;
-    decreases_clause_name;
-    terminates_clause_name;
+    termination_measure_name;
+    decreases_proof_name;
     var_basename;
     type_var_basename;
     append_index;
@@ -1370,8 +1379,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
   (* Register the decrease clauses, if necessary *)
   let register_decreases ctx def =
     if has_decreases_clause def then
-      let ctx = ctx_add_decreases_clause def ctx in
-      ctx_add_terminates_clause def ctx
+      (* Add the termination measure *)
+      let ctx = ctx_add_termination_measure def ctx in
+      (* Add the decreases proof for Lean only *)
+      match !Config.backend with
+      | Coq | FStar -> ctx
+      | Lean -> ctx_add_decreases_proof def ctx
     else ctx
   in
   let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
@@ -2085,7 +2098,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   assert (!backend = FStar);
 
   (* Retrieve the function name *)
-  let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+  let def_name = ctx_get_termination_measure def.def_id def.loop_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 *)
@@ -2142,9 +2155,11 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
 let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) : unit =
   assert (!backend = Lean);
-
+  (*
+   * Extract a template for the termination measure
+   *)
   (* Retrieve the function name *)
-  let def_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in
+  let def_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
   let def_body = Option.get def.body in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
@@ -2197,8 +2212,10 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0;
 
-  (* Now extract a template for the termination proof *)
-  let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+  (*
+   * Extract a template for the decreases proof
+   *)
+  let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
   extract_comment fmt
@@ -2329,7 +2346,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       (* Open a box for the decreases term *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* The name of the decrease clause *)
-      let decr_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+      let decr_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
       F.pp_print_string fmt decr_name;
       (* Print the type parameters *)
       List.iter
@@ -2401,7 +2418,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* termination_by *)
     let terminates_name =
-      ctx_get_terminates_clause def.def_id def.loop_id ctx
+      ctx_get_termination_measure def.def_id def.loop_id ctx
     in
     F.pp_print_break fmt 0 0;
     (* Open a box for the whole [termination_by CALL => DECREASES] *)
@@ -2443,7 +2460,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_break fmt 0 0;
     (* Open a box for the [decreasing by ...] *)
     F.pp_open_hvbox fmt ctx.indent_incr;
-    let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+    let decreases_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
     F.pp_print_string fmt "decreasing_by";
     F.pp_print_space fmt ();
     F.pp_open_hvbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index e96a80f9..55963289 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -189,12 +189,14 @@ type formatter = {
               filtered some of them.
           TODO: use the fun id for the assumed functions.
        *)
-  decreases_clause_name :
+  termination_measure_name :
     A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
-      (** Generates the name of the definition used to prove/reason about
+      (** Generates the name of the termination measure used to prove/reason about
           termination. The generated code uses this clause where needed,
           but its body must be defined by the user.
 
+          F* and Lean only.
+
           Inputs:
           - function id: this is especially useful to identify whether the
             function is an assumed function or a local function
@@ -203,11 +205,13 @@ type formatter = {
             the same purpose as in {!field:fun_name}.
           - loop identifier, if this is for a loop
        *)
-  terminates_clause_name :
+  decreases_proof_name :
     A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
-      (** Generates the name of the measure used to prove/reason about
+      (** Generates the name of the proof used to prove/reason about
           termination. The generated code uses this clause where needed,
-          but its body must be defined by the user. Lean only.
+          but its body must be defined by the user.
+
+          Lean only.
 
           Inputs:
           - function id: this is especially useful to identify whether the
@@ -294,17 +298,30 @@ type id =
   | GlobalId of A.GlobalDeclId.id
   | FunId of fun_id
   | DeclaredId of fun_id
-  | DecreasesClauseId of (A.fun_id * LoopId.id option)
-      (** The definition which provides the decreases/termination clause.
+  | TerminationMeasureId of (A.fun_id * LoopId.id option)
+      (** The definition which provides the decreases/termination measure.
           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.
+
+          More specifically:
+          - in F*, this is the content of the [decreases] clause.
+            Example:
+            ========
+            {[
+              let rec sum (ls : list nat) : Tot nat (decreases ls) = ...
+            ]}
+          - in Lean, this is the content of the [termination_by] clause.
        *)
-  | TerminatesClauseId of (A.fun_id * LoopId.id option)
-      (** The definition which provides the decreases/termination measure.
+  | DecreasesProofId of (A.fun_id * LoopId.id option)
+      (** The definition which provides the decreases/termination proof.
           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.
+
+          More specifically:
+          - F* doesn't use this.
+          - in Lean, this is the tactic used by the [decreases_by] annotations.
        *)
   | TypeId of type_id
   | StructId of type_id
@@ -494,7 +511,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
           in
           "fun name (" ^ lp_kind ^ fwd_back_kind ^ "): " ^ fun_name
       | Pure fid -> PrintPure.pure_assumed_fun_id_to_string fid)
-  | DecreasesClauseId (fid, lid) ->
+  | DecreasesProofId (fid, lid) ->
       let fun_name =
         match fid with
         | Regular fid ->
@@ -506,8 +523,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
         | None -> ""
         | Some lid -> ", loop: " ^ LoopId.to_string lid
       in
-      "decreases clause for function: " ^ fun_name ^ loop
-  | TerminatesClauseId (fid, lid) ->
+      "decreases proof for function: " ^ fun_name ^ loop
+  | TerminationMeasureId (fid, lid) ->
       let fun_name =
         match fid with
         | Regular fid ->
@@ -519,7 +536,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
         | None -> ""
         | Some lid -> ", loop: " ^ LoopId.to_string lid
       in
-      "terminates clause for function: " ^ fun_name ^ loop
+      "termination measure for function: " ^ fun_name ^ loop
   | TypeId id -> "type name: " ^ get_type_name id
   | StructId id -> "struct constructor of: " ^ get_type_name id
   | VariantId (id, variant_id) ->
@@ -629,13 +646,13 @@ 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_decreases_clause (def_id : A.FunDeclId.id)
+let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get (DecreasesClauseId (Regular def_id, loop_id)) ctx
+  ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
 
-let ctx_get_terminates_clause (def_id : A.FunDeclId.id)
+let ctx_get_termination_measure (def_id : A.FunDeclId.id)
     (loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
-  ctx_get (TerminatesClauseId (Regular def_id, loop_id)) ctx
+  ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
 
 (** Generate a unique type variable name and add it to the context *)
 let ctx_add_type_var (basename : string) (id : TypeVarId.id)
@@ -721,21 +738,21 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
   let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
   (ctx, name)
 
-let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) :
+let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx.fmt.decreases_clause_name def.def_id def.basename def.num_loops
+    ctx.fmt.decreases_proof_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
+  ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
 
-let ctx_add_terminates_clause (def : fun_decl) (ctx : extraction_ctx) :
+let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name =
-    ctx.fmt.terminates_clause_name def.def_id def.basename def.num_loops
+    ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
       def.loop_id
   in
-  ctx_add (TerminatesClauseId (Regular def.def_id, def.loop_id)) name ctx
+  ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
 
 let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
     extraction_ctx =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index b2cab4c2..139f8891 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -825,12 +825,14 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
   let ctx =
     List.fold_left
       (fun ctx (keep_fwd, defs) ->
-        (* We generate a decrease clause for all the recursive functions *)
+        (* If requested by the user, register termination measures and decreases
+           proofs for all the recursive functions *)
         let fwd_def = fst (fst defs) in
         let gen_decr_clause (def : Pure.fun_decl) =
-          PureUtils.FunLoopIdSet.mem
-            (def.Pure.def_id, def.Pure.loop_id)
-            rec_functions
+          !Config.extract_decreases_clauses
+          && PureUtils.FunLoopIdSet.mem
+               (def.Pure.def_id, def.Pure.loop_id)
+               rec_functions
         in
         (* Register the names, only if the function is not a global body -
          * those are handled later *)