From feb60683216a6d9193d6353605560c6c80a1ab41 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 7 Mar 2023 08:41:57 +0100 Subject: Make minor modifications and regenerate the Lean files --- tests/lean/misc/paper/Paper.lean | 118 +++++++++++++++++++-------------------- 1 file changed, 59 insertions(+), 59 deletions(-) (limited to 'tests/lean/misc/paper/Paper.lean') diff --git a/tests/lean/misc/paper/Paper.lean b/tests/lean/misc/paper/Paper.lean index adcd1eae..4faf36ee 100644 --- a/tests/lean/misc/paper/Paper.lean +++ b/tests/lean/misc/paper/Paper.lean @@ -5,56 +5,56 @@ import Base.Primitives structure OpaqueDefs where /- [paper::ref_incr] -/ - def ref_incr_fwd_back (x : Int32) : result Int32 := + def ref_incr_fwd_back (x : Int32) : Result Int32 := Int32.checked_add x (Int32.ofNatCore 1 (by intlit)) /- [paper::test_incr] -/ - def test_incr_fwd : result Unit := + def test_incr_fwd : Result Unit := do - let x <- ref_incr_fwd_back (Int32.ofNatCore 0 (by intlit)) - if not (x = (Int32.ofNatCore 1 (by intlit))) - then result.fail error.panic - else result.ret () + let x ← ref_incr_fwd_back (Int32.ofNatCore 0 (by intlit)) + if h: not (x = (Int32.ofNatCore 1 (by intlit))) + then Result.fail Error.panic + else Result.ret () /- Unit test for [paper::test_incr] -/ - #assert (test_incr_fwd = .ret ()) + #assert (test_incr_fwd == .ret ()) /- [paper::choose] -/ - def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : result T := - if b - then result.ret x - else result.ret y + def choose_fwd (T : Type) (b : Bool) (x : T) (y : T) : Result T := + if h: b + then Result.ret x + else Result.ret y /- [paper::choose] -/ def choose_back - (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : result (T × T) := - if b - then result.ret (ret0, y) - else result.ret (x, ret0) + (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) := + if h: b + then Result.ret (ret0, y) + else Result.ret (x, ret0) /- [paper::test_choose] -/ - def test_choose_fwd : result Unit := + def test_choose_fwd : Result Unit := do - let z <- + let z ← choose_fwd Int32 true (Int32.ofNatCore 0 (by intlit)) (Int32.ofNatCore 0 (by intlit)) - let z0 <- Int32.checked_add z (Int32.ofNatCore 1 (by intlit)) - if not (z0 = (Int32.ofNatCore 1 (by intlit))) - then result.fail error.panic + let z0 ← Int32.checked_add z (Int32.ofNatCore 1 (by intlit)) + if h: not (z0 = (Int32.ofNatCore 1 (by intlit))) + then Result.fail Error.panic else do - let (x, y) <- + let (x, y) ← choose_back Int32 true (Int32.ofNatCore 0 (by intlit)) (Int32.ofNatCore 0 (by intlit)) z0 - if not (x = (Int32.ofNatCore 1 (by intlit))) - then result.fail error.panic + if h: not (x = (Int32.ofNatCore 1 (by intlit))) + then Result.fail Error.panic else - if not (y = (Int32.ofNatCore 0 (by intlit))) - then result.fail error.panic - else result.ret () + if h: not (y = (Int32.ofNatCore 0 (by intlit))) + then Result.fail Error.panic + else Result.ret () /- Unit test for [paper::test_choose] -/ - #assert (test_choose_fwd = .ret ()) + #assert (test_choose_fwd == .ret ()) /- [paper::List] -/ inductive list_t (T : Type) := @@ -62,67 +62,67 @@ structure OpaqueDefs where | ListNil : list_t T /- [paper::list_nth_mut] -/ - def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : result T := - match l with + def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T := + match h: l with | list_t.ListCons x tl => - if i = (UInt32.ofNatCore 0 (by intlit)) - then result.ret x + if h: i = (UInt32.ofNatCore 0 (by intlit)) + then Result.ret x else do - let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) + let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_fwd T tl i0 - | list_t.ListNil => result.fail error.panic + | list_t.ListNil => Result.fail Error.panic /- [paper::list_nth_mut] -/ def list_nth_mut_back - (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : result (list_t T) := - match l with + (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) := + match h: l with | list_t.ListCons x tl => - if i = (UInt32.ofNatCore 0 (by intlit)) - then result.ret (list_t.ListCons ret0 tl) + if h: i = (UInt32.ofNatCore 0 (by intlit)) + then Result.ret (list_t.ListCons ret0 tl) else do - let i0 <- UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) - let tl0 <- list_nth_mut_back T tl i0 ret0 - result.ret (list_t.ListCons x tl0) - | list_t.ListNil => result.fail error.panic + let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) + let tl0 ← list_nth_mut_back T tl i0 ret0 + Result.ret (list_t.ListCons x tl0) + | list_t.ListNil => Result.fail Error.panic /- [paper::sum] -/ - def sum_fwd (l : list_t Int32) : result Int32 := - match l with + def sum_fwd (l : list_t Int32) : Result Int32 := + match h: l with | list_t.ListCons x tl => do - let i <- sum_fwd tl + let i ← sum_fwd tl Int32.checked_add x i - | list_t.ListNil => result.ret (Int32.ofNatCore 0 (by intlit)) + | list_t.ListNil => Result.ret (Int32.ofNatCore 0 (by intlit)) /- [paper::test_nth] -/ - def test_nth_fwd : result Unit := + def test_nth_fwd : Result Unit := do let l := list_t.ListNil let l0 := list_t.ListCons (Int32.ofNatCore 3 (by intlit)) l let l1 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l0 - let x <- + let x ← list_nth_mut_fwd Int32 (list_t.ListCons (Int32.ofNatCore 1 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit)) - let x0 <- Int32.checked_add x (Int32.ofNatCore 1 (by intlit)) - let l2 <- + let x0 ← Int32.checked_add x (Int32.ofNatCore 1 (by intlit)) + let l2 ← list_nth_mut_back Int32 (list_t.ListCons (Int32.ofNatCore 1 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit)) x0 - let i <- sum_fwd l2 - if not (i = (Int32.ofNatCore 7 (by intlit))) - then result.fail error.panic - else result.ret () + let i ← sum_fwd l2 + if h: not (i = (Int32.ofNatCore 7 (by intlit))) + then Result.fail Error.panic + else Result.ret () /- Unit test for [paper::test_nth] -/ - #assert (test_nth_fwd = .ret ()) + #assert (test_nth_fwd == .ret ()) /- [paper::call_choose] -/ - def call_choose_fwd (p : (UInt32 × UInt32)) : result UInt32 := + def call_choose_fwd (p : (UInt32 × UInt32)) : Result UInt32 := do let (px, py) := p - let pz <- choose_fwd UInt32 true px py - let pz0 <- UInt32.checked_add pz (UInt32.ofNatCore 1 (by intlit)) - let (px0, _) <- choose_back UInt32 true px py pz0 - result.ret px0 + let pz ← choose_fwd UInt32 true px py + let pz0 ← UInt32.checked_add pz (UInt32.ofNatCore 1 (by intlit)) + let (px0, _) ← choose_back UInt32 true px py pz0 + Result.ret px0 -- cgit v1.2.3