Merge branch 'main' into core-option-unwrap

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