diff options
author | Son HO | 2023-11-28 08:04:43 +0100 |
---|---|---|
committer | GitHub | 2023-11-28 08:04:43 +0100 |
commit | b78850a81dfea78bc280f1b5b6d2fdcb421e386a (patch) | |
tree | 3a4807b26856c0c2e21f1a8a4cdf80da136c26ec /tests/lean/Paper.lean | |
parent | bacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (diff) | |
parent | a3a3ab9723348e24f83073a52145128f34022265 (diff) |
Merge pull request #46 from AeneasVerif/son_improves
Minor improvements for the extraction
Diffstat (limited to 'tests/lean/Paper.lean')
-rw-r--r-- | tests/lean/Paper.lean | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 37e0e70e..08386bb7 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -17,11 +17,11 @@ def test_incr : Result Unit := do let x ← ref_incr 0#i32 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_incr] -/ -#assert (test_incr == .ret ()) +#assert (test_incr == Result.ret ()) /- [paper::choose]: forward function Source: 'src/paper.rs', lines 15:0-15:70 -/ @@ -33,10 +33,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T := /- [paper::choose]: backward function 0 Source: 'src/paper.rs', lines 15:0-15:70 -/ def choose_back - (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) := + (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) := if b - then Result.ret (ret0, y) - else Result.ret (x, ret0) + then Result.ret (ret, y) + else Result.ret (x, ret) /- [paper::test_choose]: forward function Source: 'src/paper.rs', lines 23:0-23:20 -/ @@ -45,18 +45,18 @@ def test_choose : Result Unit := let z ← choose I32 true 0#i32 0#i32 let z0 ← z + 1#i32 if not (z0 = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else do let (x, y) ← choose_back I32 true 0#i32 0#i32 z0 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else if not (y = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_choose] -/ -#assert (test_choose == .ret ()) +#assert (test_choose == Result.ret ()) /- [paper::List] Source: 'src/paper.rs', lines 35:0-35:16 -/ @@ -74,22 +74,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T := else do let i0 ← i - 1#u32 list_nth_mut T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [paper::list_nth_mut]: backward function 0 Source: 'src/paper.rs', lines 42:0-42:67 -/ divergent def list_nth_mut_back - (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := + (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) := match l with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_back T tl i0 ret0 + let tl0 ← list_nth_mut_back T tl i0 ret Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [paper::sum]: forward function Source: 'src/paper.rs', lines 57:0-57:32 -/ @@ -112,11 +112,11 @@ def test_nth : Result Unit := let l2 ← list_nth_mut_back I32 (List.Cons 1#i32 l1) 2#u32 x0 let i ← sum l2 if not (i = 7#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_nth] -/ -#assert (test_nth == .ret ()) +#assert (test_nth == Result.ret ()) /- [paper::call_choose]: forward function Source: 'src/paper.rs', lines 76:0-76:44 -/ |