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#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#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#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#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#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