Don't need extra variables for the decreases clauses

2 files changed, 24 insertions, 14 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index eb96cd48..64069cb0 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2130,6 +2130,7 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
   F.pp_print_space fmt ();
   (* Tuple of the arguments *)
   let vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+
   if List.length vars = 1 then
     F.pp_print_string fmt (ctx_get_var (List.hd vars) ctx_body)
   else begin
@@ -2345,12 +2346,17 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   if has_decreases_clause && !backend = Lean then begin
     let def_body = Option.get def.body in
     let vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+    let num_fwd_inputs =
+      def.signature.info.num_fwd_inputs_with_fuel_with_state
+    in
+    let vars = Collections.List.prefix num_fwd_inputs vars in
+
     (* terminates_by *)
     let terminates_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in
     F.pp_print_break fmt 0 0;
-    F.pp_open_hvbox fmt ctx.indent_incr;
+    F.pp_open_hovbox fmt ctx.indent_incr;
     F.pp_print_string fmt "termination_by";
-    F.pp_open_hvbox fmt ctx.indent_incr;
+    F.pp_open_hovbox fmt 0;
     F.pp_print_space fmt ();
     F.pp_print_string fmt def_name;
     F.pp_print_space fmt ();
@@ -2361,7 +2367,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_space fmt ();
     F.pp_print_string fmt "=>";
     F.pp_close_box fmt ();
-    F.pp_open_hbox fmt ();
+    F.pp_open_hovbox fmt 0;
     F.pp_print_space fmt ();
     F.pp_print_string fmt terminates_name;
     F.pp_print_space fmt ();
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 6cdc6bd8..f9d4a8c5 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -21,7 +21,9 @@ def hashmap_hash_map_allocate_slots_loop_fwd
       let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) 
       hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0
   else result.ret slots
-termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => hashmap_hash_map_allocate_slots_loop_terminates T slots n 
+termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n =>
+                                                                  hashmap_hash_map_allocate_slots_loop_terminates
+                                                                  T slots n 
 decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n
 
 /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
@@ -71,7 +73,9 @@ def hashmap_hash_map_clear_slots_loop_fwd_back
           hashmap_list_t.HashmapListNil 
       hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1
   else result.ret slots
-termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => hashmap_hash_map_clear_slots_loop_terminates T slots i 
+termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i =>
+                                                                    hashmap_hash_map_clear_slots_loop_terminates
+                                                                    T slots i 
 decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i
 
 /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
@@ -210,11 +214,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back
         hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
     | hashmap_list_t.HashmapListNil => result.ret ntable
     
-  termination_by
-                  hashmap_hash_map_move_elements_from_list_loop_fwd_back
-                  ntable
-                  ls
-                  => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls 
+  termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable
+                ls => hashmap_hash_map_move_elements_from_list_loop_terminates
+                     T ntable ls 
   decreasing_by
     hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls
   
@@ -344,7 +346,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back
         else hashmap_hash_map_get_in_list_loop_fwd T key tl
       | hashmap_list_t.HashmapListNil => result.fail error.panic
       
-    termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls 
+    termination_by hashmap_hash_map_get_in_list_loop_fwd key ls =>
+                                                                  hashmap_hash_map_get_in_list_loop_terminates
+                                                                  T key ls 
     decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls
     
     /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
@@ -397,9 +401,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back
             result.ret (hashmap_list_t.HashmapListCons ckey cvalue l)
       | hashmap_list_t.HashmapListNil => result.fail error.panic
       
-    termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 =>
-       hashmap_hash_map_get_mut_in_list_loop_terminates T ls key ret0 
-    decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key ret0
+    termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key =>
+       hashmap_hash_map_get_mut_in_list_loop_terminates T ls key 
+    decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
     
     /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
     def hashmap_hash_map_get_mut_in_list_back