summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon Ho2024-04-25 16:07:56 +0200
committerSon Ho2024-04-25 16:07:56 +0200
commit078b7f59ddfcb12a7b4c69f0a51bfd57cb391ddf (patch)
treeed45664329e24d1773be6c8bcaf827e2adbd3f65 /tests/lean
parent1728dced8484befe35ef61fdf4ccd62b93fbb19d (diff)
parenta3e38d5f47e4780768902e49e28e471e38efd40a (diff)
Merge branch 'main' into core-option-unwrap
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Funs.lean4
-rw-r--r--tests/lean/External/Funs.lean73
-rw-r--r--tests/lean/External/FunsExternal.lean19
-rw-r--r--tests/lean/External/FunsExternal_Template.lean23
-rw-r--r--tests/lean/External/Types.lean6
-rw-r--r--tests/lean/External/TypesExternal.lean17
-rw-r--r--tests/lean/External/TypesExternal_Template.lean8
7 files changed, 68 insertions, 82 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 57b334fa..0c31b9bc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -238,11 +238,11 @@ divergent def betree.Node.apply_upserts
betree.Node.apply_upserts msgs1 (some v) key st
else
do
- let v ← core.option.Option.unwrap U64 prev
+ let (st1, v) ← core.option.Option.unwrap U64 prev st
let msgs1 ←
betree.List.push_front (U64 × betree.Message) msgs (key,
betree.Message.Insert v)
- Result.ok (st, (v, msgs1))
+ Result.ok (st1, (v, msgs1))
/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
Source: 'src/betree.rs', lines 395:4-395:63 -/
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 3bdd70e3..20c4b8e5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -7,59 +7,28 @@ open Primitives
namespace external
-/- [external::swap]:
- Source: 'src/external.rs', lines 6:0-6:46 -/
-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]:
- 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 (st1, o) ← core.num.nonzero.NonZeroU32.new x st
- let o1 ← core.option.Option.unwrap core.num.nonzero.NonZeroU32 o
- Result.ok (st1, o1)
-
-/- [external::test_vec]:
- Source: 'src/external.rs', lines 17:0-17:17 -/
-def test_vec : Result Unit :=
- do
- let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
- Result.ok ()
-
-/- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ok ())
-
-/- [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 × (T → State → Result (State × (T × T)))))
+/- Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+ Name pattern: core::marker::Copy<u32> -/
+def core.marker.CopyU32 : core.marker.Copy U32 := {
+ cloneCloneInst := core.clone.CloneU32
+}
+
+/- [external::use_get]:
+ Source: 'src/external.rs', lines 5:0-5:37 -/
+def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
+ core.cell.Cell.get U32 core.marker.CopyU32 rc st
+
+/- [external::incr]:
+ Source: 'src/external.rs', lines 9:0-9:31 -/
+def incr
+ (rc : core.cell.Cell U32) (st : State) :
+ Result (State × (core.cell.Cell U32))
:=
do
- let (st1, (x1, y1)) ← core.mem.swap T x y st
- let back := fun ret st2 => Result.ok (st2, (ret, y1))
- Result.ok (st1, (x1, back))
-
-/- [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 × (U32 × U32)) :=
- do
- let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
- let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
- Result.ok (st1, (x1, y1))
-
-/- [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 (st1, p) ← swap U32 x 0#u32 st
- let (x1, _) := p
- if x1 = 0#u32
- then Result.fail .panic
- else Result.ok (st1, x1)
+ let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
+ let i1 ← i + 1#u32
+ let (_, rc1) ← get_mut_back i1 st1
+ Result.ok (st1, rc1)
end external
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index 7adf0922..c3e8dd79 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -4,14 +4,13 @@ import External.Types
open Primitives
open external
--- TODO: fill those bodies
+/- [core::cell::{core::cell::Cell<T>#10}::get]: -/
+def core.cell.Cell.get
+ (T : Type) (markerCopyInst : core.marker.Copy T) (c : core.cell.Cell T) (s : State) :
+ Result (State × T) :=
+ sorry
-/- [core::mem::swap] -/
-def core.mem.swap
- (T : Type) : T → T → State → Result (State × (T × T)) :=
- fun x y s => .ok (s, (y, x))
-
-/- [core::num::nonzero::NonZeroU32::{14}::new] -/
-def core.num.nonzero.NonZeroU32.new :
- U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) :=
- fun _ _ => .fail .panic
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]: -/
+def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) :
+ Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) :=
+ sorry
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 34b0552a..a6163c96 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -6,15 +6,18 @@ import External.Types
open Primitives
open external
-/- [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
- Name pattern: core::mem::swap -/
-axiom core.mem.swap
- (T : Type) : T → T → State → Result (State × (T × T))
+/- [core::cell::{core::cell::Cell<T>#10}::get]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
+axiom core.cell.Cell.get
+ (T : Type) (markerCopyInst : core.marker.Copy T) :
+ core.cell.Cell T → State → Result (State × T)
-/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
- Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
-axiom core.num.nonzero.NonZeroU32.new
- : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+ Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
+axiom core.cell.Cell.get_mut
+ (T : Type) :
+ core.cell.Cell T → State → Result (State × (T × (T → State → Result
+ (State × (core.cell.Cell T)))))
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 961f3e8a..5d4cfc77 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -6,4 +6,10 @@ open Primitives
namespace external
+/- Trait declaration: [core::marker::Copy]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+ Name pattern: core::marker::Copy -/
+structure core.marker.Copy (Self : Type) where
+ cloneCloneInst : core.clone.Clone Self
+
end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
index 7c30f792..d0f5a0cc 100644
--- a/tests/lean/External/TypesExternal.lean
+++ b/tests/lean/External/TypesExternal.lean
@@ -1,11 +1,20 @@
-- [external]: external types.
import Base
-open Primitives
+open Lean Primitives
/- [core::num::nonzero::NonZeroU32]
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+structure core.cell.Cell (T : Type) :=
+ id : Nat
-/- The state type used in the state-error monad -/
-axiom State : Type
+def CellValue := (T:Type) × T
+
+/- The state type used in the state-error monad
+ TODO: we tried the following definition, but it makes State a Type 1, leading
+ to type errors later:
+
+ structure State :=
+ cells : AssocList Nat CellValue
+ -/
+axiom State : Type
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 84245531..2e6ed6e0 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -4,10 +4,10 @@
import Base
open Primitives
-/- [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
- Name pattern: core::num::nonzero::NonZeroU32 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+/- [core::cell::Cell]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+ Name pattern: core::cell::Cell -/
+axiom core.cell.Cell (T : Type) : Type
/- The state type used in the state-error monad -/
axiom State : Type