From c6913b8bf90689d8961c47f59896443e7fae164d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 5 Feb 2023 22:03:41 +0100
Subject: Make sure let-bindings in Lean end with line breaks and improve
 formatting

---
 tests/coq/betree/BetreeMain_Funs.v           |  3 ++-
 tests/coq/betree/_CoqProject                 |  2 +-
 tests/coq/hashmap/Hashmap_Funs.v             |  3 ++-
 tests/coq/hashmap/_CoqProject                |  2 +-
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v |  6 +++--
 tests/coq/misc/Constants.v                   | 12 ++++++---
 tests/coq/misc/NoNestedBorrows.v             | 39 ++++++++++++++++++----------
 tests/coq/misc/Paper.v                       |  3 ++-
 tests/coq/misc/_CoqProject                   |  6 ++---
 9 files changed, 49 insertions(+), 27 deletions(-)

(limited to 'tests/coq')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 10cdedd1..fe22b029 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -1156,6 +1156,7 @@ Definition betree_be_tree_lookup_back
 .
 
 (** [betree_main::main] *)
-Definition main_fwd : result unit := Return tt.
+Definition main_fwd : result unit :=
+  Return tt.
 
 End BetreeMain_Funs .
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 42c62421..e5a3f799 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,7 +3,7 @@
 -arg -w
 -arg all
 
-BetreeMain_Types.v
 Primitives.v
+BetreeMain_Types.v
 BetreeMain_Funs.v
 BetreeMain_Opaque.v
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index f1af0c21..b952e60c 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -9,7 +9,8 @@ Import Hashmap_Types.
 Module Hashmap_Funs.
 
 (** [hashmap::hash_key] *)
-Definition hash_key_fwd (k : usize) : result usize := Return k.
+Definition hash_key_fwd (k : usize) : result usize :=
+  Return k.
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hash_map_allocate_slots_loop_fwd
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index 7f80afbf..daa9b2ba 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -3,6 +3,6 @@
 -arg -w
 -arg all
 
-Hashmap_Types.v
 Primitives.v
+Hashmap_Types.v
 Hashmap_Funs.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 7c86dbe1..2a3ad87c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -11,7 +11,8 @@ Import HashmapMain_Opaque.
 Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key] *)
-Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
+Definition hashmap_hash_key_fwd (k : usize) : result usize :=
+  Return k.
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
@@ -598,7 +599,8 @@ Definition insert_on_disk_fwd
 .
 
 (** [hashmap_main::main] *)
-Definition main_fwd : result unit := Return tt.
+Definition main_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [hashmap_main::main] *)
 Check (main_fwd )%return.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index acc15a13..0a72558d 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -23,7 +23,8 @@ Definition x2_body : result u32 := Return (3%u32).
 Definition x2_c : u32 := x2_body%global.
 
 (** [constants::incr] *)
-Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32.
+Definition incr_fwd (n : u32) : result u32 :=
+  u32_add n 1%u32.
 
 (** [constants::X3] *)
 Definition x3_body : result u32 := incr_fwd (32%u32).
@@ -80,7 +81,8 @@ Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32).
 Definition y_c : Wrap_t i32 := y_body%global.
 
 (** [constants::unwrap_y] *)
-Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val).
+Definition unwrap_y_fwd : result i32 :=
+  Return y_c.(Wrap_val).
 
 (** [constants::YVAL] *)
 Definition yval_body : result i32 := unwrap_y_fwd.
@@ -91,10 +93,12 @@ Definition get_z1_z1_body : result i32 := Return (3%i32).
 Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
 
 (** [constants::get_z1] *)
-Definition get_z1_fwd : result i32 := Return get_z1_z1_c.
+Definition get_z1_fwd : result i32 :=
+  Return get_z1_z1_c.
 
 (** [constants::add] *)
-Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b.
+Definition add_fwd (a : i32) (b : i32) : result i32 :=
+  i32_add a b.
 
 (** [constants::Q1] *)
 Definition q1_body : result i32 := Return (5%i32).
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 10654887..98ed1cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -46,28 +46,36 @@ Arguments SumLeft {T1} {T2} _.
 Arguments SumRight {T1} {T2} _.
 
 (** [no_nested_borrows::neg_test] *)
-Definition neg_test_fwd (x : i32) : result i32 := i32_neg x.
+Definition neg_test_fwd (x : i32) : result i32 :=
+  i32_neg x.
 
 (** [no_nested_borrows::add_test] *)
-Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y.
+Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_add x y.
 
 (** [no_nested_borrows::subs_test] *)
-Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y.
+Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_sub x y.
 
 (** [no_nested_borrows::div_test] *)
-Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y.
+Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_div x y.
 
 (** [no_nested_borrows::div_test1] *)
-Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32.
+Definition div_test1_fwd (x : u32) : result u32 :=
+  u32_div x 2%u32.
 
 (** [no_nested_borrows::rem_test] *)
-Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
+Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
+  u32_rem x y.
 
 (** [no_nested_borrows::cast_test] *)
-Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
+Definition cast_test_fwd (x : u32) : result i32 :=
+  scalar_cast U32 I32 x.
 
 (** [no_nested_borrows::test2] *)
-Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt.
+Definition test2_fwd : result unit :=
+  _ <- u32_add 23%u32 44%u32; Return tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2_fwd )%return.
@@ -122,7 +130,8 @@ Definition refs_test2_fwd : result unit :=
 Check (refs_test2_fwd )%return.
 
 (** [no_nested_borrows::test_list1] *)
-Definition test_list1_fwd : result unit := Return tt.
+Definition test_list1_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [no_nested_borrows::test_list1] *)
 Check (test_list1_fwd )%return.
@@ -138,7 +147,8 @@ Definition test_box1_fwd : result unit :=
 Check (test_box1_fwd )%return.
 
 (** [no_nested_borrows::copy_int] *)
-Definition copy_int_fwd (x : i32) : result i32 := Return x.
+Definition copy_int_fwd (x : i32) : result i32 :=
+  Return x.
 
 (** [no_nested_borrows::test_unreachable] *)
 Definition test_unreachable_fwd (b : bool) : result unit :=
@@ -468,7 +478,8 @@ Definition test_constants_fwd : result unit :=
 Check (test_constants_fwd )%return.
 
 (** [no_nested_borrows::test_weird_borrows1] *)
-Definition test_weird_borrows1_fwd : result unit := Return tt.
+Definition test_weird_borrows1_fwd : result unit :=
+  Return tt.
 
 (** Unit test for [no_nested_borrows::test_weird_borrows1] *)
 Check (test_weird_borrows1_fwd )%return.
@@ -485,7 +496,8 @@ Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 :=
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool2] *)
-Definition test_shared_borrow_bool2_fwd : result u32 := Return (0%u32).
+Definition test_shared_borrow_bool2_fwd : result u32 :=
+  Return (0%u32).
 
 (** [no_nested_borrows::test_shared_borrow_enum1] *)
 Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
@@ -496,6 +508,7 @@ Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
 .
 
 (** [no_nested_borrows::test_shared_borrow_enum2] *)
-Definition test_shared_borrow_enum2_fwd : result u32 := Return (0%u32).
+Definition test_shared_borrow_enum2_fwd : result u32 :=
+  Return (0%u32).
 
 End NoNestedBorrows .
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index cb4486c6..8045222d 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -7,7 +7,8 @@ Local Open Scope Primitives_scope.
 Module Paper.
 
 (** [paper::ref_incr] *)
-Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32.
+Definition ref_incr_fwd_back (x : i32) : result i32 :=
+  i32_add x 1%i32.
 
 (** [paper::test_incr] *)
 Definition test_incr_fwd : result unit :=
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index db6c2742..87dea3e6 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,12 +3,12 @@
 -arg -w
 -arg all
 
-Loops.v
+Constants.v
+External_Types.v
 Primitives.v
+Loops.v
 External_Funs.v
-Constants.v
 PoloniusList.v
-External_Types.v
 NoNestedBorrows.v
 External_Opaque.v
 Paper.v
-- 
cgit v1.2.3