summaryrefslogtreecommitdiff
path: root/tests/lean/External
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/External/Funs.lean89
-rw-r--r--tests/lean/External/FunsExternal_Template.lean19
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)