From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:20:20 +0200
Subject: Regenerate the test files

---
 tests/lean/BetreeMain/Funs.lean | 122 ++++++++++++++++++++--------------------
 1 file changed, 61 insertions(+), 61 deletions(-)

(limited to 'tests/lean/BetreeMain/Funs.lean')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 2fbcd6a4..0c31b9bc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -42,12 +42,12 @@ def betree.store_leaf_node
 def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
   let counter1 ← counter + 1#u64
-  Result.ret (counter, counter1)
+  Result.ok (counter, counter1)
 
 /- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
    Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
-  Result.ret { next_node_id := 0#u64 }
+  Result.ok { next_node_id := 0#u64 }
 
 /- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
    Source: 'src/betree.rs', lines 210:4-210:36 -/
@@ -55,7 +55,7 @@ def betree.NodeIdCounter.fresh_id
   (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
   do
   let i ← self.next_node_id + 1#u64
-  Result.ret (self.next_node_id, { next_node_id := i })
+  Result.ok (self.next_node_id, { next_node_id := i })
 
 /- [betree_main::betree::upsert_update]:
    Source: 'src/betree.rs', lines 234:0-234:70 -/
@@ -64,8 +64,8 @@ def betree.upsert_update
   match prev with
   | none =>
     match st with
-    | betree.UpsertFunState.Add v => Result.ret v
-    | betree.UpsertFunState.Sub _ => Result.ret 0#u64
+    | betree.UpsertFunState.Add v => Result.ok v
+    | betree.UpsertFunState.Sub _ => Result.ok 0#u64
   | some prev1 =>
     match st with
     | betree.UpsertFunState.Add v =>
@@ -73,11 +73,11 @@ def betree.upsert_update
       let margin ← core_u64_max - prev1
       if margin >= v
       then prev1 + v
-      else Result.ret core_u64_max
+      else Result.ok core_u64_max
     | betree.UpsertFunState.Sub v =>
       if prev1 >= v
       then prev1 - v
-      else Result.ret 0#u64
+      else Result.ok 0#u64
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
@@ -86,7 +86,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   | betree.List.Cons _ tl => do
                              let i ← betree.List.len T tl
                              1#u64 + i
-  | betree.List.Nil => Result.ret 0#u64
+  | betree.List.Nil => Result.ok 0#u64
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
    Source: 'src/betree.rs', lines 284:4-284:51 -/
@@ -95,7 +95,7 @@ divergent def betree.List.split_at
   Result ((betree.List T) × (betree.List T))
   :=
   if n = 0#u64
-  then Result.ret (betree.List.Nil, self)
+  then Result.ok (betree.List.Nil, self)
   else
     match self with
     | betree.List.Cons hd tl =>
@@ -103,7 +103,7 @@ divergent def betree.List.split_at
       let i ← n - 1#u64
       let p ← betree.List.split_at T tl i
       let (ls0, ls1) := p
-      Result.ret (betree.List.Cons hd ls0, ls1)
+      Result.ok (betree.List.Cons hd ls0, ls1)
     | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
@@ -111,7 +111,7 @@ divergent def betree.List.split_at
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
-  Result.ret (betree.List.Cons x tl)
+  Result.ok (betree.List.Cons x tl)
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -119,14 +119,14 @@ def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
   let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
-  | betree.List.Cons x tl => Result.ret (x, tl)
+  | betree.List.Cons x tl => Result.ok (x, tl)
   | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
-  | betree.List.Cons hd _ => Result.ret hd
+  | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
@@ -135,8 +135,8 @@ def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
   | betree.List.Cons hd _ => let (i, _) := hd
-                             Result.ret (i = key)
-  | betree.List.Nil => Result.ret false
+                             Result.ok (i = key)
+  | betree.List.Nil => Result.ok false
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
@@ -148,13 +148,13 @@ divergent def betree.ListPairU64T.partition_at_pivot
   | betree.List.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
-    then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
+    then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
       let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
       let (ls0, ls1) := p
-      Result.ret (betree.List.Cons (i, t) ls0, ls1)
-  | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
+      Result.ok (betree.List.Cons (i, t) ls0, ls1)
+  | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
 
 /- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
    Source: 'src/betree.rs', lines 359:4-364:17 -/
@@ -174,7 +174,7 @@ def betree.Leaf.split
   let (st2, _) ← betree.store_leaf_node id1 content1 st1
   let n := betree.Node.Leaf { id := id0, size := params.split_size }
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
-  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
+  Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
@@ -187,7 +187,7 @@ divergent def betree.Node.lookup_first_message_for_key
   | betree.List.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
-    then Result.ret (betree.List.Cons (i, m) next_msgs, Result.ret)
+    then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
     else
       do
       let (l, lookup_first_message_for_key_back) ←
@@ -196,9 +196,9 @@ divergent def betree.Node.lookup_first_message_for_key
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_for_key_back ret
-          Result.ret (betree.List.Cons (i, m) next_msgs1)
-      Result.ret (l, back)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (i, m) next_msgs1)
+      Result.ok (l, back)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 636:4-636:80 -/
@@ -208,12 +208,12 @@ divergent def betree.Node.lookup_in_bindings
   | betree.List.Cons hd tl =>
     let (i, i1) := hd
     if i = key
-    then Result.ret (some i1)
+    then Result.ok (some i1)
     else
       if i > key
-      then Result.ret none
+      then Result.ok none
       else betree.Node.lookup_in_bindings key tl
-  | betree.List.Nil => Result.ret none
+  | betree.List.Nil => Result.ok none
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -242,7 +242,7 @@ divergent def betree.Node.apply_upserts
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ret (st1, (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 -/
@@ -255,11 +255,11 @@ mutual divergent def betree.Internal.lookup_in_children
   then
     do
     let (st1, (o, n2)) ← betree.Node.lookup n key st
-    Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1))
+    Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
   else
     do
     let (st1, (o, n2)) ← betree.Node.lookup n1 key st
-    Result.ret (st1, (o, betree.Internal.mk i i1 n n2))
+    Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
@@ -285,7 +285,7 @@ divergent def betree.Node.lookup
             st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
-        Result.ret (st2, (o, betree.Node.Internal node1))
+        Result.ok (st2, (o, betree.Node.Internal node1))
       else
         match msg with
         | betree.Message.Insert v =>
@@ -293,14 +293,14 @@ divergent def betree.Node.lookup
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Insert v) l)
-          Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i
+          Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
             i1 n n1)))
         | betree.Message.Delete =>
           do
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Delete) l)
-          Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
+          Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
             n n1)))
         | betree.Message.Upsert ufs =>
           do
@@ -313,20 +313,20 @@ divergent def betree.Node.lookup
           let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
           let (st4, _) ← betree.store_internal_node i2 msgs1 st3
-          Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
-            i2 i3 n2 n3)))
+          Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2
+            i3 n2 n3)))
     | betree.List.Nil =>
       do
       let (st2, (o, node1)) ←
         betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
           st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
-      Result.ret (st2, (o, betree.Node.Internal node1))
+      Result.ok (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
     do
     let (st1, bindings) ← betree.load_leaf_node node.id st
     let o ← betree.Node.lookup_in_bindings key bindings
-    Result.ret (st1, (o, betree.Node.Leaf node))
+    Result.ok (st1, (o, betree.Node.Leaf node))
 
 end
 
@@ -346,8 +346,8 @@ divergent def betree.Node.filter_messages_for_key
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
       betree.Node.filter_messages_for_key key msgs1
-    else Result.ret (betree.List.Cons (k, m) l)
-  | betree.List.Nil => Result.ret betree.List.Nil
+    else Result.ok (betree.List.Cons (k, m) l)
+  | betree.List.Nil => Result.ok betree.List.Nil
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 689:4-692:34 -/
@@ -368,10 +368,10 @@ divergent def betree.Node.lookup_first_message_after_key
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_after_key_back ret
-          Result.ret (betree.List.Cons (k, m) next_msgs1)
-      Result.ret (l, back)
-    else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (k, m) next_msgs1)
+      Result.ok (l, back)
+    else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
    Source: 'src/betree.rs', lines 521:4-521:89 -/
@@ -450,7 +450,7 @@ divergent def betree.Node.apply_messages_to_internal
     let (i, m) := new_msg
     let msgs1 ← betree.Node.apply_to_internal msgs i m
     betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
-  | betree.List.Nil => Result.ret msgs
+  | betree.List.Nil => Result.ok msgs
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 653:4-656:32 -/
@@ -463,7 +463,7 @@ divergent def betree.Node.lookup_mut_in_bindings
   | betree.List.Cons hd tl =>
     let (i, i1) := hd
     if i >= key
-    then Result.ret (betree.List.Cons (i, i1) tl, Result.ret)
+    then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
     else
       do
       let (l, lookup_mut_in_bindings_back) ←
@@ -472,9 +472,9 @@ divergent def betree.Node.lookup_mut_in_bindings
         fun ret =>
           do
           let tl1 ← lookup_mut_in_bindings_back ret
-          Result.ret (betree.List.Cons (i, i1) tl1)
-      Result.ret (l, back)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (i, i1) tl1)
+      Result.ok (l, back)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
    Source: 'src/betree.rs', lines 460:4-460:87 -/
@@ -529,7 +529,7 @@ divergent def betree.Node.apply_messages_to_leaf
     let (i, m) := new_msg
     let bindings1 ← betree.Node.apply_to_leaf bindings i m
     betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
-  | betree.List.Nil => Result.ret bindings
+  | betree.List.Nil => Result.ok bindings
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
    Source: 'src/betree.rs', lines 410:4-415:26 -/
@@ -558,17 +558,17 @@ mutual divergent def betree.Internal.flush
       let (st2, p2) ←
         betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
       let (n3, node_id_cnt2) := p2
-      Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
+      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
         node_id_cnt2)))
     else
-      Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
+      Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
         node_id_cnt1)))
   else
     do
     let (st1, p1) ←
       betree.Node.apply_messages n1 params node_id_cnt msgs_right st
     let (n2, node_id_cnt1) := p1
-    Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+    Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
@@ -594,12 +594,12 @@ divergent def betree.Node.apply_messages
       let (node1, node_id_cnt1) := p
       let ⟨ i2, i3, n2, n3 ⟩ := node1
       let (st3, _) ← betree.store_internal_node i2 content2 st2
-      Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
+      Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
         node_id_cnt1))
     else
       do
       let (st2, _) ← betree.store_internal_node i content1 st1
-      Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
+      Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
         node_id_cnt))
   | betree.Node.Leaf node =>
     do
@@ -613,11 +613,11 @@ divergent def betree.Node.apply_messages
       let (st2, (new_node, node_id_cnt1)) ←
         betree.Leaf.split node content1 params node_id_cnt st1
       let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
-      Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1))
+      Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1))
     else
       do
       let (st2, _) ← betree.store_leaf_node node.id content1 st1
-      Result.ret (st2, (betree.Node.Leaf { node with size := len },
+      Result.ok (st2, (betree.Node.Leaf { node with size := len },
         node_id_cnt))
 
 end
@@ -635,7 +635,7 @@ def betree.Node.apply
     betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key,
       new_msg) betree.List.Nil) st
   let (self1, node_id_cnt1) := p
-  Result.ret (st1, (self1, node_id_cnt1))
+  Result.ok (st1, (self1, node_id_cnt1))
 
 /- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
    Source: 'src/betree.rs', lines 849:4-849:60 -/
@@ -647,7 +647,7 @@ def betree.BeTree.new
   let node_id_cnt ← betree.NodeIdCounter.new
   let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
   let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
-  Result.ret (st1,
+  Result.ok (st1,
     {
       params := { min_flush_size := min_flush_size, split_size := split_size },
       node_id_cnt := node_id_cnt1,
@@ -664,7 +664,7 @@ def betree.BeTree.apply
   let (st1, p) ←
     betree.Node.apply self.root self.params self.node_id_cnt key msg st
   let (n, nic) := p
-  Result.ret (st1, { self with node_id_cnt := nic, root := n })
+  Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
 /- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
    Source: 'src/betree.rs', lines 874:4-874:52 -/
@@ -699,14 +699,14 @@ def betree.BeTree.lookup
   :=
   do
   let (st1, (o, n)) ← betree.Node.lookup self.root key st
-  Result.ret (st1, (o, { self with root := n }))
+  Result.ok (st1, (o, { self with root := n }))
 
 /- [betree_main::main]:
    Source: 'src/betree_main.rs', lines 5:0-5:9 -/
 def main : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [betree_main::main] -/
-#assert (main == Result.ret ())
+#assert (main == Result.ok ())
 
 end betree_main
-- 
cgit v1.2.3

