Start working on the generation of decrease clauses

3 files changed, 63 insertions, 2 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a28d8c6d..9ad3c94c 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -274,6 +274,16 @@ 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 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
+    (* Concatenate *)
+    fname ^ suffix
+  in
+
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
       : string =
     (* If there is a basename, we use it *)
@@ -342,6 +352,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
     struct_constructor;
     type_name;
     fun_name;
+    decrease_clause_name;
     var_basename;
     type_var_basename;
     append_index;
@@ -633,8 +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)
-    (def : pure_fun_translation) : extraction_ctx =
+    (has_decrease_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
+  in
   (* Register the forward function name *)
   let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in
   (* Register the backward functions' names *)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index c61338b9..bb010a05 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -79,6 +79,17 @@ type formatter = {
               some of them)
           - region group information in case of a backward function
             (`None` if forward function)
+          TODO: use the fun id for the assumed functions.
+       *)
+  decrease_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.
+      
+          Inputs:
+          - function id: this is especially useful to identify whether the
+            function is an assumed function or a local function
+          - function basename
        *)
   var_basename : StringSet.t -> string option -> ty -> string;
       (** Generates a variable basename.
@@ -163,6 +174,12 @@ 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.
+          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.
+       *)
   | TypeId of type_id
   | StructId of type_id
       (** We use this when we manipulate the names of the structure
@@ -320,6 +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 ->
+      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
   | TypeId id -> "type name: " ^ get_type_name id
   | StructId id -> "struct constructor of: " ^ get_type_name id
   | VariantId (id, variant_id) ->
@@ -503,6 +528,11 @@ 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) :
+    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 ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
     (ctx : extraction_ctx) : extraction_ctx =
   (* Lookup the CFIM def to compute the region group information *)
@@ -531,6 +561,7 @@ let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
   let name =
     ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
   in
+  (* Add the function name *)
   let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
   ctx
 
diff --git a/src/Translate.ml b/src/Translate.ml
index ba3effc5..8d9c0270 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -306,6 +306,16 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
   in
 
+  (* We need to compute which functions are recursive, in order to know
+   * whether we should generate a decrease clause or not. *)
+  let rec_functions =
+    Pure.FunDefId.Set.of_list
+      (List.concat
+         (List.map
+            (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
+            m.declarations))
+  in
+
   (* Register unique names for all the top-level types and functions.
    * Note that the order in which we generate the names doesn't matter:
    * we just need to generate a mapping from identifier to name, and make
@@ -320,7 +330,12 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   let extract_ctx =
     List.fold_left
       (fun extract_ctx (keep_fwd, def) ->
-        ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd def)
+        (* Note that we generate a decrease clause for all the recursive functions *)
+        let gen_decr_clause =
+          Pure.FunDefId.Set.mem (fst def).Pure.def_id rec_functions
+        in
+        ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd
+          gen_decr_clause def)
       extract_ctx trans_funs
   in