diff options
author | Son Ho | 2023-03-07 13:46:55 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 051e2a19f3268d272a0acd0425d2107ebea020c5 (patch) | |
tree | 2ad36d00054ac891e48cb35c4dc1940433c5e707 /tests/lean/misc-external/External | |
parent | 463cbb90c93ac2e825048d685c254431b99c4d96 (diff) |
Reorganize the Lean tests and extract the Polonius tests to Lean
Diffstat (limited to 'tests/lean/misc-external/External')
-rw-r--r-- | tests/lean/misc-external/External/Funs.lean | 93 | ||||
-rw-r--r-- | tests/lean/misc-external/External/Opaque.lean | 28 | ||||
-rw-r--r-- | tests/lean/misc-external/External/Types.lean | 8 |
3 files changed, 129 insertions, 0 deletions
diff --git a/tests/lean/misc-external/External/Funs.lean b/tests/lean/misc-external/External/Funs.lean new file mode 100644 index 00000000..4e1f36a1 --- /dev/null +++ b/tests/lean/misc-external/External/Funs.lean @@ -0,0 +1,93 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [external]: function definitions +import Base.Primitives +import External.Types +import External.Opaque + +section variable (opaque_defs: OpaqueDefs) + +/- [external::swap] -/ +def swap_fwd + (T : Type) (x : T) (y : T) (st : State) : Result (State × Unit) := + do + let (st0, _) ← opaque_defs.core_mem_swap_fwd T x y st + let (st1, _) ← opaque_defs.core_mem_swap_back0 T x y st st0 + let (st2, _) ← opaque_defs.core_mem_swap_back1 T x y st st1 + Result.ret (st2, ()) + +/- [external::swap] -/ +def swap_back + (T : Type) (x : T) (y : T) (st : State) (st0 : State) : + Result (State × (T × T)) + := + do + let (st1, _) ← opaque_defs.core_mem_swap_fwd T x y st + let (st2, x0) ← opaque_defs.core_mem_swap_back0 T x y st st1 + let (_, y0) ← opaque_defs.core_mem_swap_back1 T x y st st2 + Result.ret (st0, (x0, y0)) + +/- [external::test_new_non_zero_u32] -/ +def test_new_non_zero_u32_fwd + (x : UInt32) (st : State) : + Result (State × core_num_nonzero_non_zero_u32_t) + := + do + let (st0, opt) ← opaque_defs.core_num_nonzero_non_zero_u32_new_fwd x st + opaque_defs.core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t + opt st0 + +/- [external::test_vec] -/ +def test_vec_fwd : Result Unit := + do + let v := vec_new UInt32 + let _ ← vec_push_back UInt32 v (UInt32.ofNatCore 0 (by intlit)) + Result.ret () + +/- Unit test for [external::test_vec] -/ +#assert (test_vec_fwd == .ret ()) + +/- [external::custom_swap] -/ +def custom_swap_fwd + (T : Type) (x : T) (y : T) (st : State) : Result (State × T) := + do + let (st0, _) ← opaque_defs.core_mem_swap_fwd T x y st + let (st1, x0) ← opaque_defs.core_mem_swap_back0 T x y st st0 + let (st2, _) ← opaque_defs.core_mem_swap_back1 T x y st st1 + Result.ret (st2, x0) + +/- [external::custom_swap] -/ +def custom_swap_back + (T : Type) (x : T) (y : T) (st : State) (ret0 : T) (st0 : State) : + Result (State × (T × T)) + := + do + let (st1, _) ← opaque_defs.core_mem_swap_fwd T x y st + let (st2, _) ← opaque_defs.core_mem_swap_back0 T x y st st1 + let (_, y0) ← opaque_defs.core_mem_swap_back1 T x y st st2 + Result.ret (st0, (ret0, y0)) + +/- [external::test_custom_swap] -/ +def test_custom_swap_fwd + (x : UInt32) (y : UInt32) (st : State) : Result (State × Unit) := + do + let (st0, _) ← custom_swap_fwd UInt32 x y st + Result.ret (st0, ()) + +/- [external::test_custom_swap] -/ +def test_custom_swap_back + (x : UInt32) (y : UInt32) (st : State) (st0 : State) : + Result (State × (UInt32 × UInt32)) + := + custom_swap_back UInt32 x y st (UInt32.ofNatCore 1 (by intlit)) st0 + +/- [external::test_swap_non_zero] -/ +def test_swap_non_zero_fwd + (x : UInt32) (st : State) : Result (State × UInt32) := + do + let (st0, _) ← swap_fwd UInt32 x (UInt32.ofNatCore 0 (by intlit)) st + let (st1, (x0, _)) ← + swap_back UInt32 x (UInt32.ofNatCore 0 (by intlit)) st st0 + if h: x0 = (UInt32.ofNatCore 0 (by intlit)) + then Result.fail Error.panic + else Result.ret (st1, x0) + diff --git a/tests/lean/misc-external/External/Opaque.lean b/tests/lean/misc-external/External/Opaque.lean new file mode 100644 index 00000000..d3582de3 --- /dev/null +++ b/tests/lean/misc-external/External/Opaque.lean @@ -0,0 +1,28 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [external]: opaque function definitions +import Base.Primitives +import External.Types + +structure OpaqueDefs where + + /- [core::mem::swap] -/ + core_mem_swap_fwd (T : Type) : T -> T -> State -> Result (State × Unit) + + /- [core::mem::swap] -/ + core_mem_swap_back0 + (T : Type) : T -> T -> State -> State -> Result (State × T) + + /- [core::mem::swap] -/ + core_mem_swap_back1 + (T : Type) : T -> T -> State -> State -> Result (State × T) + + /- [core::num::nonzero::NonZeroU32::{14}::new] -/ + core_num_nonzero_non_zero_u32_new_fwd + : + UInt32 -> State -> Result (State × (Option + core_num_nonzero_non_zero_u32_t)) + + /- [core::option::Option::{0}::unwrap] -/ + core_option_option_unwrap_fwd + (T : Type) : Option T -> State -> Result (State × T) + diff --git a/tests/lean/misc-external/External/Types.lean b/tests/lean/misc-external/External/Types.lean new file mode 100644 index 00000000..386832f4 --- /dev/null +++ b/tests/lean/misc-external/External/Types.lean @@ -0,0 +1,8 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [external]: type definitions +import Base.Primitives + +/- [core::num::nonzero::NonZeroU32] -/ +axiom core_num_nonzero_non_zero_u32_t : Type +/- The state type used in the state-error monad -/ axiom State : Type + |