diff options
Diffstat (limited to 'tests/lean/External')
| -rw-r--r-- | tests/lean/External/Funs.lean | 89 | ||||
| -rw-r--r-- | tests/lean/External/FunsExternal_Template.lean | 19 |
2 files changed, 33 insertions, 75 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 48ec6ad5..88ced82d 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -7,92 +7,59 @@ open Primitives namespace external -/- [external::swap]: forward function +/- [external::swap]: Source: 'src/external.rs', lines 6:0-6:46 -/ -def swap (T : Type) (x : T) (y : T) (st : State) : Result (State × Unit) := - do - let (st0, _) ← core.mem.swap T x y st - let (st1, _) ← core.mem.swap_back0 T x y st st0 - let (st2, _) ← core.mem.swap_back1 T x y st st1 - Result.ret (st2, ()) - -/- [external::swap]: backward function 0 - Source: 'src/external.rs', lines 6:0-6:46 -/ -def swap_back - (T : Type) (x : T) (y : T) (st : State) (st0 : State) : - Result (State × (T × T)) - := - do - let (st1, _) ← core.mem.swap T x y st - let (st2, x0) ← core.mem.swap_back0 T x y st st1 - let (_, y0) ← core.mem.swap_back1 T x y st st2 - Result.ret (st0, (x0, y0)) +def swap + (T : Type) (x : T) (y : T) (st : State) : Result (State × (T × T)) := + core.mem.swap T x y st -/- [external::test_new_non_zero_u32]: forward function +/- [external::test_new_non_zero_u32]: Source: 'src/external.rs', lines 11:0-11:60 -/ def test_new_non_zero_u32 (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) := do - let (st0, o) ← core.num.nonzero.NonZeroU32.new x st - core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st0 + let (st1, o) ← core.num.nonzero.NonZeroU32.new x st + core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1 -/- [external::test_vec]: forward function +/- [external::test_vec]: Source: 'src/external.rs', lines 17:0-17:17 -/ def test_vec : Result Unit := do - let v := alloc.vec.Vec.new U32 - let _ ← alloc.vec.Vec.push U32 v 0#u32 - Result.ret () + let v := alloc.vec.Vec.new U32 + let _ ← alloc.vec.Vec.push U32 v 0#u32 + Result.ret () /- Unit test for [external::test_vec] -/ #assert (test_vec == Result.ret ()) -/- [external::custom_swap]: forward function +/- [external::custom_swap]: Source: 'src/external.rs', lines 24:0-24:66 -/ def custom_swap - (T : Type) (x : T) (y : T) (st : State) : Result (State × T) := - do - let (st0, _) ← core.mem.swap T x y st - let (st1, x0) ← core.mem.swap_back0 T x y st st0 - let (st2, _) ← core.mem.swap_back1 T x y st st1 - Result.ret (st2, x0) - -/- [external::custom_swap]: backward function 0 - Source: 'src/external.rs', lines 24:0-24:66 -/ -def custom_swap_back - (T : Type) (x : T) (y : T) (st : State) (ret : T) (st0 : State) : - Result (State × (T × T)) + (T : Type) (x : T) (y : T) (st : State) : + Result (State × (T × (T → State → Result (State × (T × T))))) := do - let (st1, _) ← core.mem.swap T x y st - let (st2, _) ← core.mem.swap_back0 T x y st st1 - let (_, y0) ← core.mem.swap_back1 T x y st st2 - Result.ret (st0, (ret, y0)) + let (st1, (t, t1)) ← core.mem.swap T x y st + let back_'a := fun ret st2 => Result.ret (st2, (ret, t1)) + Result.ret (st1, (t, back_'a)) -/- [external::test_custom_swap]: forward function +/- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ def test_custom_swap - (x : U32) (y : U32) (st : State) : Result (State × Unit) := + (x : U32) (y : U32) (st : State) : Result (State × (U32 × U32)) := do - let (st0, _) ← custom_swap U32 x y st - Result.ret (st0, ()) - -/- [external::test_custom_swap]: backward function 0 - Source: 'src/external.rs', lines 29:0-29:59 -/ -def test_custom_swap_back - (x : U32) (y : U32) (st : State) (st0 : State) : - Result (State × (U32 × U32)) - := - custom_swap_back U32 x y st 1#u32 st0 + let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st + let (_, (x1, y1)) ← custom_swap_back 1#u32 st1 + Result.ret (st1, (x1, y1)) -/- [external::test_swap_non_zero]: forward function +/- [external::test_swap_non_zero]: Source: 'src/external.rs', lines 35:0-35:44 -/ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) := do - let (st0, _) ← swap U32 x 0#u32 st - let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0 - if x0 = 0#u32 - then Result.fail .panic - else Result.ret (st1, x0) + let (st1, p) ← swap U32 x 0#u32 st + let (x1, _) := p + if x1 = 0#u32 + then Result.fail .panic + else Result.ret (st1, x1) end external diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 55cd6bb5..7e237369 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -6,26 +6,17 @@ import External.Types open Primitives open external -/- [core::mem::swap]: forward function +/- [core::mem::swap]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap (T : Type) : T → T → State → Result (State × Unit) +axiom core.mem.swap + (T : Type) : T → T → State → Result (State × (T × T)) -/- [core::mem::swap]: backward function 0 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap_back0 - (T : Type) : T → T → State → State → Result (State × T) - -/- [core::mem::swap]: backward function 1 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap_back1 - (T : Type) : T → T → State → State → Result (State × T) - -/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function +/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/ axiom core.num.nonzero.NonZeroU32.new : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32)) -/- [core::option::{core::option::Option<T>}::unwrap]: forward function +/- [core::option::{core::option::Option<T>}::unwrap]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) |