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/misc/Constants.v | 12 ++++++++---- tests/coq/misc/NoNestedBorrows.v | 39 ++++++++++++++++++++++++++------------- tests/coq/misc/Paper.v | 3 ++- tests/coq/misc/_CoqProject | 6 +++--- 4 files changed, 39 insertions(+), 21 deletions(-) (limited to 'tests/coq/misc') 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