diff options
Diffstat (limited to '')
-rw-r--r-- | tests/lean/misc-paper/Paper.lean | 240 |
1 files changed, 118 insertions, 122 deletions
diff --git a/tests/lean/misc-paper/Paper.lean b/tests/lean/misc-paper/Paper.lean index 05fde52c..0b16fb8e 100644 --- a/tests/lean/misc-paper/Paper.lean +++ b/tests/lean/misc-paper/Paper.lean @@ -2,126 +2,122 @@ -- [paper] import Base.Primitives -structure OpaqueDefs where - - /- [paper::ref_incr] -/ - 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 := - do - 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 ()) - - /- [paper::choose] -/ - 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 h: b - then Result.ret (ret0, y) - else Result.ret (x, ret0) - - /- [paper::test_choose] -/ - def test_choose_fwd : Result Unit := - do - 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 h: not (z0 = (Int32.ofNatCore 1 (by intlit))) - then Result.fail Error.panic - else - do - let (x, y) ← - choose_back Int32 true (Int32.ofNatCore 0 (by intlit)) - (Int32.ofNatCore 0 (by intlit)) z0 - if h: not (x = (Int32.ofNatCore 1 (by intlit))) +/- [paper::ref_incr] -/ +def ref_incr_fwd_back (x : I32) : Result I32 := + x + (I32.ofInt 1 (by intlit)) + +/- [paper::test_incr] -/ +def test_incr_fwd : Result Unit := + do + let x ← ref_incr_fwd_back (I32.ofInt 0 (by intlit)) + if h: not (x = (I32.ofInt 1 (by intlit))) + then Result.fail Error.panic + else Result.ret () + +/- Unit test for [paper::test_incr] -/ +#assert (test_incr_fwd == .ret ()) + +/- [paper::choose] -/ +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 h: b + then Result.ret (ret0, y) + else Result.ret (x, ret0) + +/- [paper::test_choose] -/ +def test_choose_fwd : Result Unit := + do + let z ← + choose_fwd I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit)) + let z0 ← z + (I32.ofInt 1 (by intlit)) + if h: not (z0 = (I32.ofInt 1 (by intlit))) + then Result.fail Error.panic + else + do + let (x, y) ← + choose_back I32 true (I32.ofInt 0 (by intlit)) + (I32.ofInt 0 (by intlit)) z0 + if h: not (x = (I32.ofInt 1 (by intlit))) + then Result.fail Error.panic + else + if h: not (y = (I32.ofInt 0 (by intlit))) then Result.fail Error.panic - else - 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 ()) - - /- [paper::List] -/ - inductive list_t (T : Type) := - | Cons : T -> list_t T -> list_t T - | Nil : list_t T - - /- [paper::list_nth_mut] -/ - def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T := - match h: l with - | list_t.Cons x tl => - 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)) - list_nth_mut_fwd T tl i0 - | list_t.Nil => 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 h: l with - | list_t.Cons x tl => - if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.Cons 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.Cons x tl0) - | list_t.Nil => Result.fail Error.panic - - /- [paper::sum] -/ - def sum_fwd (l : list_t Int32) : Result Int32 := - match h: l with - | list_t.Cons x tl => do - let i ← sum_fwd tl - Int32.checked_add x i - | list_t.Nil => Result.ret (Int32.ofNatCore 0 (by intlit)) - - /- [paper::test_nth] -/ - def test_nth_fwd : Result Unit := - do - let l := list_t.Nil - let l0 := list_t.Cons (Int32.ofNatCore 3 (by intlit)) l - let l1 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l0 - let x ← - list_nth_mut_fwd Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) l1) - (UInt32.ofNatCore 2 (by intlit)) - let x0 ← Int32.checked_add x (Int32.ofNatCore 1 (by intlit)) - let l2 ← - list_nth_mut_back Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) - l1) (UInt32.ofNatCore 2 (by intlit)) x0 - 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 ()) - - /- [paper::call_choose] -/ - 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 - + else Result.ret () + +/- Unit test for [paper::test_choose] -/ +#assert (test_choose_fwd == .ret ()) + +/- [paper::List] -/ +inductive list_t (T : Type) := +| Cons : T -> list_t T -> list_t T +| Nil : list_t T + +/- [paper::list_nth_mut] -/ +def list_nth_mut_fwd (T : Type) (l : list_t T) (i : U32) : Result T := + match h: l with + | list_t.Cons x tl => + if h: i = (U32.ofInt 0 (by intlit)) + then Result.ret x + else do + let i0 ← i - (U32.ofInt 1 (by intlit)) + list_nth_mut_fwd T tl i0 + | list_t.Nil => Result.fail Error.panic + +/- [paper::list_nth_mut] -/ +def list_nth_mut_back + (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) := + match h: l with + | list_t.Cons x tl => + if h: i = (U32.ofInt 0 (by intlit)) + then Result.ret (list_t.Cons ret0 tl) + else + do + let i0 ← i - (U32.ofInt 1 (by intlit)) + let tl0 ← list_nth_mut_back T tl i0 ret0 + Result.ret (list_t.Cons x tl0) + | list_t.Nil => Result.fail Error.panic + +/- [paper::sum] -/ +def sum_fwd (l : list_t I32) : Result I32 := + match h: l with + | list_t.Cons x tl => do + let i ← sum_fwd tl + x + i + | list_t.Nil => Result.ret (I32.ofInt 0 (by intlit)) + +/- [paper::test_nth] -/ +def test_nth_fwd : Result Unit := + do + let l := list_t.Nil + let l0 := list_t.Cons (I32.ofInt 3 (by intlit)) l + let l1 := list_t.Cons (I32.ofInt 2 (by intlit)) l0 + let x ← + list_nth_mut_fwd I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1) + (U32.ofInt 2 (by intlit)) + let x0 ← x + (I32.ofInt 1 (by intlit)) + let l2 ← + list_nth_mut_back I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1) + (U32.ofInt 2 (by intlit)) x0 + let i ← sum_fwd l2 + if h: not (i = (I32.ofInt 7 (by intlit))) + then Result.fail Error.panic + else Result.ret () + +/- Unit test for [paper::test_nth] -/ +#assert (test_nth_fwd == .ret ()) + +/- [paper::call_choose] -/ +def call_choose_fwd (p : (U32 × U32)) : Result U32 := + do + let (px, py) := p + let pz ← choose_fwd U32 true px py + let pz0 ← pz + (U32.ofInt 1 (by intlit)) + let (px0, _) ← choose_back U32 true px py pz0 + Result.ret px0 + |