summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/BetreeMain')
-rw-r--r--tests/lean/BetreeMain/Funs.lean328
-rw-r--r--tests/lean/BetreeMain/FunsExternal_Template.lean15
-rw-r--r--tests/lean/BetreeMain/Types.lean31
-rw-r--r--tests/lean/BetreeMain/TypesExternal.lean7
-rw-r--r--tests/lean/BetreeMain/TypesExternal_Template.lean9
5 files changed, 234 insertions, 156 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 07ef08dc..4c862225 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -7,14 +7,16 @@ open Primitives
namespace betree_main
-/- [betree_main::betree::load_internal_node]: forward function -/
+/- [betree_main::betree::load_internal_node]: forward function
+ Source: 'src/betree.rs', lines 36:0-36:52 -/
def betree.load_internal_node
(id : U64) (st : State) :
Result (State × (betree.List (U64 × betree.Message)))
:=
betree_utils.load_internal_node id st
-/- [betree_main::betree::store_internal_node]: forward function -/
+/- [betree_main::betree::store_internal_node]: forward function
+ Source: 'src/betree.rs', lines 41:0-41:60 -/
def betree.store_internal_node
(id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
Result (State × Unit)
@@ -23,12 +25,14 @@ def betree.store_internal_node
let (st0, _) ← betree_utils.store_internal_node id content st
Result.ret (st0, ())
-/- [betree_main::betree::load_leaf_node]: forward function -/
+/- [betree_main::betree::load_leaf_node]: forward function
+ Source: 'src/betree.rs', lines 46:0-46:44 -/
def betree.load_leaf_node
(id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) :=
betree_utils.load_leaf_node id st
-/- [betree_main::betree::store_leaf_node]: forward function -/
+/- [betree_main::betree::store_leaf_node]: forward function
+ Source: 'src/betree.rs', lines 51:0-51:52 -/
def betree.store_leaf_node
(id : U64) (content : betree.List (U64 × U64)) (st : State) :
Result (State × Unit)
@@ -37,125 +41,133 @@ def betree.store_leaf_node
let (st0, _) ← betree_utils.store_leaf_node id content st
Result.ret (st0, ())
-/- [betree_main::betree::fresh_node_id]: forward function -/
+/- [betree_main::betree::fresh_node_id]: forward function
+ Source: 'src/betree.rs', lines 55:0-55:48 -/
def betree.fresh_node_id (counter : U64) : Result U64 :=
do
- let _ ← counter + (U64.ofInt 1)
+ let _ ← counter + 1#u64
Result.ret counter
-/- [betree_main::betree::fresh_node_id]: backward function 0 -/
+/- [betree_main::betree::fresh_node_id]: backward function 0
+ Source: 'src/betree.rs', lines 55:0-55:48 -/
def betree.fresh_node_id_back (counter : U64) : Result U64 :=
- counter + (U64.ofInt 1)
+ counter + 1#u64
-/- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+ Source: 'src/betree.rs', lines 206:4-206:20 -/
def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
- Result.ret { next_node_id := (U64.ofInt 0) }
+ Result.ret { next_node_id := 0#u64 }
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+ Source: 'src/betree.rs', lines 210:4-210:36 -/
def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
do
- let _ ← self.next_node_id + (U64.ofInt 1)
+ let _ ← self.next_node_id + 1#u64
Result.ret self.next_node_id
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
+ Source: 'src/betree.rs', lines 210:4-210:36 -/
def betree.NodeIdCounter.fresh_id_back
(self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
do
- let i ← self.next_node_id + (U64.ofInt 1)
+ let i ← self.next_node_id + 1#u64
Result.ret { next_node_id := i }
-/- [core::num::u64::{9}::MAX] -/
-def core_num_u64_max_body : Result U64 :=
- Result.ret (U64.ofInt 18446744073709551615)
-def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
-
-/- [betree_main::betree::upsert_update]: forward function -/
+/- [betree_main::betree::upsert_update]: forward function
+ Source: 'src/betree.rs', lines 234:0-234:70 -/
def betree.upsert_update
(prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
match prev with
- | Option.none =>
+ | none =>
match st with
| betree.UpsertFunState.Add v => Result.ret v
- | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0)
- | Option.some prev0 =>
+ | betree.UpsertFunState.Sub i => Result.ret 0#u64
+ | some prev0 =>
match st with
| betree.UpsertFunState.Add v =>
do
- let margin ← core_num_u64_max_c - prev0
+ let margin ← core_u64_max - prev0
if margin >= v
then prev0 + v
- else Result.ret core_num_u64_max_c
+ else Result.ret core_u64_max
| betree.UpsertFunState.Sub v =>
if prev0 >= v
then prev0 - v
- else Result.ret (U64.ofInt 0)
+ else Result.ret 0#u64
-/- [betree_main::betree::List::{1}::len]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+ Source: 'src/betree.rs', lines 276:4-276:24 -/
divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
match self with
- | betree.List.Cons t tl =>
- do
- let i ← betree.List.len T tl
- (U64.ofInt 1) + i
- | betree.List.Nil => Result.ret (U64.ofInt 0)
+ | betree.List.Cons t tl => do
+ let i ← betree.List.len T tl
+ 1#u64 + i
+ | betree.List.Nil => Result.ret 0#u64
-/- [betree_main::betree::List::{1}::split_at]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+ Source: 'src/betree.rs', lines 284:4-284:51 -/
divergent def betree.List.split_at
(T : Type) (self : betree.List T) (n : U64) :
Result ((betree.List T) × (betree.List T))
:=
- if n = (U64.ofInt 0)
+ if n = 0#u64
then Result.ret (betree.List.Nil, self)
else
match self with
| betree.List.Cons hd tl =>
do
- let i ← n - (U64.ofInt 1)
+ let i ← n - 1#u64
let p ← betree.List.split_at T tl i
let (ls0, ls1) := p
let l := ls0
Result.ret (betree.List.Cons hd l, ls1)
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
-/- [betree_main::betree::List::{1}::push_front]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 299:4-299:34 -/
def betree.List.push_front
(T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
- let tl := mem.replace (betree.List T) self betree.List.Nil
+ let tl := core.mem.replace (betree.List T) self betree.List.Nil
let l := tl
Result.ret (betree.List.Cons x l)
-/- [betree_main::betree::List::{1}::pop_front]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
+ Source: 'src/betree.rs', lines 306:4-306:32 -/
def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
- let ls := mem.replace (betree.List T) self betree.List.Nil
+ let ls := core.mem.replace (betree.List T) self betree.List.Nil
match ls with
| betree.List.Cons x tl => Result.ret x
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
-/- [betree_main::betree::List::{1}::pop_front]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+ Source: 'src/betree.rs', lines 306:4-306:32 -/
def betree.List.pop_front_back
(T : Type) (self : betree.List T) : Result (betree.List T) :=
- let ls := mem.replace (betree.List T) self betree.List.Nil
+ let ls := core.mem.replace (betree.List T) self betree.List.Nil
match ls with
| betree.List.Cons x tl => Result.ret tl
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
-/- [betree_main::betree::List::{1}::hd]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+ 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 l => Result.ret hd
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
-/- [betree_main::betree::List::{2}::head_has_key]: forward function -/
-def betree.List.head_has_key
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+ Source: 'src/betree.rs', lines 327:4-327:44 -/
+def betree.ListTupleU64T.head_has_key
(T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
match self with
| betree.List.Cons hd l => let (i, _) := hd
Result.ret (i = key)
| betree.List.Nil => Result.ret false
-/- [betree_main::betree::List::{2}::partition_at_pivot]: forward function -/
-divergent def betree.List.partition_at_pivot
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+ Source: 'src/betree.rs', lines 339:4-339:73 -/
+divergent def betree.ListTupleU64T.partition_at_pivot
(T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
:=
@@ -166,13 +178,14 @@ divergent def betree.List.partition_at_pivot
then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
else
do
- let p ← betree.List.partition_at_pivot T tl pivot
+ let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
let (ls0, ls1) := p
let l := ls0
Result.ret (betree.List.Cons (i, t) l, ls1)
| betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
-/- [betree_main::betree::Leaf::{3}::split]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+ Source: 'src/betree.rs', lines 359:4-364:17 -/
def betree.Leaf.split
(self : betree.Leaf) (content : betree.List (U64 × U64))
(params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -192,7 +205,8 @@ def betree.Leaf.split
let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
Result.ret (st1, betree.Internal.mk self.id pivot n n0)
-/- [betree_main::betree::Leaf::{3}::split]: backward function 2 -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
+ Source: 'src/betree.rs', lines 359:4-364:17 -/
def betree.Leaf.split_back
(self : betree.Leaf) (content : betree.List (U64 × U64))
(params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -209,7 +223,8 @@ def betree.Leaf.split_back
let _ ← betree.store_leaf_node id1 content1 st0
betree.NodeIdCounter.fresh_id_back node_id_cnt0
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+ Source: 'src/betree.rs', lines 789:4-792:34 -/
divergent def betree.Node.lookup_first_message_for_key
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
@@ -222,46 +237,48 @@ divergent def betree.Node.lookup_first_message_for_key
else betree.Node.lookup_first_message_for_key key next_msgs
| betree.List.Nil => Result.ret betree.List.Nil
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
+ Source: 'src/betree.rs', lines 789:4-792:34 -/
divergent def betree.Node.lookup_first_message_for_key_back
(key : U64) (msgs : betree.List (U64 × betree.Message))
- (ret0 : betree.List (U64 × betree.Message)) :
+ (ret : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
:=
match msgs with
| betree.List.Cons x next_msgs =>
let (i, m) := x
if i >= key
- then Result.ret ret0
+ then Result.ret ret
else
do
let next_msgs0 ←
- betree.Node.lookup_first_message_for_key_back key next_msgs ret0
+ betree.Node.lookup_first_message_for_key_back key next_msgs ret
Result.ret (betree.List.Cons (i, m) next_msgs0)
- | betree.List.Nil => Result.ret ret0
+ | betree.List.Nil => Result.ret ret
-/- [betree_main::betree::Node::{5}::apply_upserts]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+ Source: 'src/betree.rs', lines 819:4-819:90 -/
divergent def betree.Node.apply_upserts
(msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
(st : State) :
Result (State × U64)
:=
do
- let b ← betree.List.head_has_key betree.Message msgs key
+ let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
if b
then
do
let msg ← betree.List.pop_front (U64 × betree.Message) msgs
let (_, m) := msg
match m with
- | betree.Message.Insert i => Result.fail Error.panic
- | betree.Message.Delete => Result.fail Error.panic
+ | betree.Message.Insert i => Result.fail .panic
+ | betree.Message.Delete => Result.fail .panic
| betree.Message.Upsert s =>
do
let v ← betree.upsert_update prev s
let msgs0 ←
betree.List.pop_front_back (U64 × betree.Message) msgs
- betree.Node.apply_upserts msgs0 (Option.some v) key st
+ betree.Node.apply_upserts msgs0 (some v) key st
else
do
let (st0, v) ← core.option.Option.unwrap U64 prev st
@@ -270,49 +287,52 @@ divergent def betree.Node.apply_upserts
betree.Message.Insert v)
Result.ret (st0, v)
-/- [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
+ Source: 'src/betree.rs', lines 819:4-819:90 -/
divergent def betree.Node.apply_upserts_back
(msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
(st : State) :
Result (betree.List (U64 × betree.Message))
:=
do
- let b ← betree.List.head_has_key betree.Message msgs key
+ let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
if b
then
do
let msg ← betree.List.pop_front (U64 × betree.Message) msgs
let (_, m) := msg
match m with
- | betree.Message.Insert i => Result.fail Error.panic
- | betree.Message.Delete => Result.fail Error.panic
+ | betree.Message.Insert i => Result.fail .panic
+ | betree.Message.Delete => Result.fail .panic
| betree.Message.Upsert s =>
do
let v ← betree.upsert_update prev s
let msgs0 ←
betree.List.pop_front_back (U64 × betree.Message) msgs
- betree.Node.apply_upserts_back msgs0 (Option.some v) key st
+ betree.Node.apply_upserts_back msgs0 (some v) key st
else
do
let (_, v) ← core.option.Option.unwrap U64 prev st
betree.List.push_front (U64 × betree.Message) msgs (key,
betree.Message.Insert v)
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+ Source: 'src/betree.rs', lines 636:4-636:80 -/
divergent def betree.Node.lookup_in_bindings
(key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
match bindings with
| betree.List.Cons hd tl =>
let (i, i0) := hd
if i = key
- then Result.ret (Option.some i0)
+ then Result.ret (some i0)
else
if i > key
- then Result.ret Option.none
+ then Result.ret none
else betree.Node.lookup_in_bindings key tl
- | betree.List.Nil => Result.ret Option.none
+ | betree.List.Nil => Result.ret none
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+ Source: 'src/betree.rs', lines 395:4-395:63 -/
mutual divergent def betree.Internal.lookup_in_children
(self : betree.Internal) (key : U64) (st : State) :
Result (State × (Option U64))
@@ -322,7 +342,8 @@ mutual divergent def betree.Internal.lookup_in_children
then betree.Node.lookup n key st
else betree.Node.lookup n0 key st
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
+ Source: 'src/betree.rs', lines 395:4-395:63 -/
divergent def betree.Internal.lookup_in_children_back
(self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
let ⟨ i, i0, n, n0 ⟩ := self
@@ -336,7 +357,8 @@ divergent def betree.Internal.lookup_in_children_back
let n1 ← betree.Node.lookup_back n0 key st
Result.ret (betree.Internal.mk i i0 n n1)
-/- [betree_main::betree::Node::{5}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+ Source: 'src/betree.rs', lines 709:4-709:58 -/
divergent def betree.Node.lookup
(self : betree.Node) (key : U64) (st : State) :
Result (State × (Option U64))
@@ -353,13 +375,13 @@ divergent def betree.Node.lookup
if k != key
then
do
- let (st1, opt) ←
+ let (st1, o) ←
betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
key st0
let _ ←
betree.Node.lookup_first_message_for_key_back key msgs
(betree.List.Cons (k, msg) l)
- Result.ret (st1, opt)
+ Result.ret (st1, o)
else
match msg with
| betree.Message.Insert v =>
@@ -367,13 +389,13 @@ divergent def betree.Node.lookup
let _ ←
betree.Node.lookup_first_message_for_key_back key msgs
(betree.List.Cons (k, betree.Message.Insert v) l)
- Result.ret (st0, Option.some v)
+ Result.ret (st0, some v)
| betree.Message.Delete =>
do
let _ ←
betree.Node.lookup_first_message_for_key_back key msgs
(betree.List.Cons (k, betree.Message.Delete) l)
- Result.ret (st0, Option.none)
+ Result.ret (st0, none)
| betree.Message.Upsert ufs =>
do
let (st1, v) ←
@@ -392,23 +414,24 @@ divergent def betree.Node.lookup
let msgs0 ←
betree.Node.lookup_first_message_for_key_back key msgs pending0
let (st3, _) ← betree.store_internal_node i1 msgs0 st2
- Result.ret (st3, Option.some v0)
+ Result.ret (st3, some v0)
| betree.List.Nil =>
do
- let (st1, opt) ←
+ let (st1, o) ←
betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
key st0
let _ ←
betree.Node.lookup_first_message_for_key_back key msgs
betree.List.Nil
- Result.ret (st1, opt)
+ Result.ret (st1, o)
| betree.Node.Leaf node =>
do
let (st0, bindings) ← betree.load_leaf_node node.id st
- let opt ← betree.Node.lookup_in_bindings key bindings
- Result.ret (st0, opt)
+ let o ← betree.Node.lookup_in_bindings key bindings
+ Result.ret (st0, o)
-/- [betree_main::betree::Node::{5}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
+ Source: 'src/betree.rs', lines 709:4-709:58 -/
divergent def betree.Node.lookup_back
(self : betree.Node) (key : U64) (st : State) : Result betree.Node :=
match self with
@@ -481,8 +504,9 @@ divergent def betree.Node.lookup_back
end
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 674:4-674:77 -/
divergent def betree.Node.filter_messages_for_key
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
@@ -500,7 +524,8 @@ divergent def betree.Node.filter_messages_for_key
else Result.ret (betree.List.Cons (k, m) l)
| betree.List.Nil => Result.ret betree.List.Nil
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+ Source: 'src/betree.rs', lines 689:4-692:34 -/
divergent def betree.Node.lookup_first_message_after_key
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
@@ -513,10 +538,11 @@ divergent def betree.Node.lookup_first_message_after_key
else Result.ret (betree.List.Cons (k, m) next_msgs)
| betree.List.Nil => Result.ret betree.List.Nil
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
+ Source: 'src/betree.rs', lines 689:4-692:34 -/
divergent def betree.Node.lookup_first_message_after_key_back
(key : U64) (msgs : betree.List (U64 × betree.Message))
- (ret0 : betree.List (U64 × betree.Message)) :
+ (ret : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
:=
match msgs with
@@ -526,13 +552,14 @@ divergent def betree.Node.lookup_first_message_after_key_back
then
do
let next_msgs0 ←
- betree.Node.lookup_first_message_after_key_back key next_msgs ret0
+ betree.Node.lookup_first_message_after_key_back key next_msgs ret
Result.ret (betree.List.Cons (k, m) next_msgs0)
- else Result.ret ret0
- | betree.List.Nil => Result.ret ret0
+ else Result.ret ret
+ | betree.List.Nil => Result.ret ret
-/- [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 521:4-521:89 -/
def betree.Node.apply_to_internal
(msgs : betree.List (U64 × betree.Message)) (key : U64)
(new_msg : betree.Message) :
@@ -540,7 +567,7 @@ def betree.Node.apply_to_internal
:=
do
let msgs0 ← betree.Node.lookup_first_message_for_key key msgs
- let b ← betree.List.head_has_key betree.Message msgs0 key
+ let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key
if b
then
match new_msg with
@@ -565,7 +592,7 @@ def betree.Node.apply_to_internal
match m with
| betree.Message.Insert prev =>
do
- let v ← betree.upsert_update (Option.some prev) s
+ let v ← betree.upsert_update (some prev) s
let msgs1 ←
betree.List.pop_front_back (U64 × betree.Message) msgs0
let msgs2 ←
@@ -574,7 +601,7 @@ def betree.Node.apply_to_internal
betree.Node.lookup_first_message_for_key_back key msgs msgs2
| betree.Message.Delete =>
do
- let v ← betree.upsert_update Option.none s
+ let v ← betree.upsert_update none s
let msgs1 ←
betree.List.pop_front_back (U64 × betree.Message) msgs0
let msgs2 ←
@@ -597,8 +624,9 @@ def betree.Node.apply_to_internal
betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg)
betree.Node.lookup_first_message_for_key_back key msgs msgs1
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 502:4-505:5 -/
divergent def betree.Node.apply_messages_to_internal
(msgs : betree.List (U64 × betree.Message))
(new_msgs : betree.List (U64 × betree.Message)) :
@@ -612,7 +640,8 @@ divergent def betree.Node.apply_messages_to_internal
betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
| betree.List.Nil => Result.ret msgs
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+ Source: 'src/betree.rs', lines 653:4-656:32 -/
divergent def betree.Node.lookup_mut_in_bindings
(key : U64) (bindings : betree.List (U64 × U64)) :
Result (betree.List (U64 × U64))
@@ -625,25 +654,27 @@ divergent def betree.Node.lookup_mut_in_bindings
else betree.Node.lookup_mut_in_bindings key tl
| betree.List.Nil => Result.ret betree.List.Nil
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
+ Source: 'src/betree.rs', lines 653:4-656:32 -/
divergent def betree.Node.lookup_mut_in_bindings_back
(key : U64) (bindings : betree.List (U64 × U64))
- (ret0 : betree.List (U64 × U64)) :
+ (ret : betree.List (U64 × U64)) :
Result (betree.List (U64 × U64))
:=
match bindings with
| betree.List.Cons hd tl =>
let (i, i0) := hd
if i >= key
- then Result.ret ret0
+ then Result.ret ret
else
do
- let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+ let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret
Result.ret (betree.List.Cons (i, i0) tl0)
- | betree.List.Nil => Result.ret ret0
+ | betree.List.Nil => Result.ret ret
-/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 460:4-460:87 -/
def betree.Node.apply_to_leaf
(bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
:
@@ -651,7 +682,7 @@ def betree.Node.apply_to_leaf
:=
do
let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
- let b ← betree.List.head_has_key U64 bindings0 key
+ let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key
if b
then
do
@@ -670,7 +701,7 @@ def betree.Node.apply_to_leaf
| betree.Message.Upsert s =>
do
let (_, i) := hd
- let v ← betree.upsert_update (Option.some i) s
+ let v ← betree.upsert_update (some i) s
let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
let bindings2 ←
betree.List.push_front (U64 × U64) bindings1 (key, v)
@@ -686,13 +717,14 @@ def betree.Node.apply_to_leaf
betree.Node.lookup_mut_in_bindings_back key bindings bindings0
| betree.Message.Upsert s =>
do
- let v ← betree.upsert_update Option.none s
+ let v ← betree.upsert_update none s
let bindings1 ←
betree.List.push_front (U64 × U64) bindings0 (key, v)
betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ())
+ Source: 'src/betree.rs', lines 444:4-447:5 -/
divergent def betree.Node.apply_messages_to_leaf
(bindings : betree.List (U64 × U64))
(new_msgs : betree.List (U64 × betree.Message)) :
@@ -706,7 +738,8 @@ divergent def betree.Node.apply_messages_to_leaf
betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
| betree.List.Nil => Result.ret bindings
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+ Source: 'src/betree.rs', lines 410:4-415:26 -/
mutual divergent def betree.Internal.flush
(self : betree.Internal) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -715,7 +748,7 @@ mutual divergent def betree.Internal.flush
:=
do
let ⟨ _, i, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i
+ let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i
let (msgs_left, msgs_right) := p
let len_left ← betree.List.len (U64 × betree.Message) msgs_left
if len_left >= params.min_flush_size
@@ -744,7 +777,8 @@ mutual divergent def betree.Internal.flush
betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
Result.ret (st0, msgs_left)
-/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
+ Source: 'src/betree.rs', lines 410:4-415:26 -/
divergent def betree.Internal.flush_back
(self : betree.Internal) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -753,7 +787,7 @@ divergent def betree.Internal.flush_back
:=
do
let ⟨ i, i0, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i0
+ let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i0
let (msgs_left, msgs_right) := p
let len_left ← betree.List.len (U64 × betree.Message) msgs_left
if len_left >= params.min_flush_size
@@ -778,7 +812,8 @@ divergent def betree.Internal.flush_back
betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
-/- [betree_main::betree::Node::{5}::apply_messages]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+ Source: 'src/betree.rs', lines 588:4-593:5 -/
divergent def betree.Node.apply_messages
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -813,7 +848,7 @@ divergent def betree.Node.apply_messages
let (st0, content) ← betree.load_leaf_node node.id st
let content0 ← betree.Node.apply_messages_to_leaf content msgs
let len ← betree.List.len (U64 × U64) content0
- let i ← (U64.ofInt 2) * params.split_size
+ let i ← 2#u64 * params.split_size
if len >= i
then
do
@@ -826,7 +861,8 @@ divergent def betree.Node.apply_messages
let (st1, _) ← betree.store_leaf_node node.id content0 st0
Result.ret (st1, ())
-/- [betree_main::betree::Node::{5}::apply_messages]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
+ Source: 'src/betree.rs', lines 588:4-593:5 -/
divergent def betree.Node.apply_messages_back
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -863,7 +899,7 @@ divergent def betree.Node.apply_messages_back
let (st0, content) ← betree.load_leaf_node node.id st
let content0 ← betree.Node.apply_messages_to_leaf content msgs
let len ← betree.List.len (U64 × U64) content0
- let i ← (U64.ofInt 2) * params.split_size
+ let i ← 2#u64 * params.split_size
if len >= i
then
do
@@ -880,7 +916,8 @@ divergent def betree.Node.apply_messages_back
end
-/- [betree_main::betree::Node::{5}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+ Source: 'src/betree.rs', lines 576:4-582:5 -/
def betree.Node.apply
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -897,7 +934,8 @@ def betree.Node.apply
(key, new_msg) l) st
Result.ret (st0, ())
-/- [betree_main::betree::Node::{5}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
+ Source: 'src/betree.rs', lines 576:4-582:5 -/
def betree.Node.apply_back
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -908,7 +946,8 @@ def betree.Node.apply_back
betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons
(key, new_msg) l) st
-/- [betree_main::betree::BeTree::{6}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+ Source: 'src/betree.rs', lines 849:4-849:60 -/
def betree.BeTree.new
(min_flush_size : U64) (split_size : U64) (st : State) :
Result (State × betree.BeTree)
@@ -923,10 +962,11 @@ def betree.BeTree.new
params :=
{ min_flush_size := min_flush_size, split_size := split_size },
node_id_cnt := node_id_cnt0,
- root := (betree.Node.Leaf { id := id, size := (U64.ofInt 0) })
+ root := (betree.Node.Leaf { id := id, size := 0#u64 })
})
-/- [betree_main::betree::BeTree::{6}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+ Source: 'src/betree.rs', lines 868:4-868:47 -/
def betree.BeTree.apply
(self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
Result (State × Unit)
@@ -938,7 +978,8 @@ def betree.BeTree.apply
betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
Result.ret (st0, ())
-/- [betree_main::betree::BeTree::{6}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
+ Source: 'src/betree.rs', lines 868:4-868:47 -/
def betree.BeTree.apply_back
(self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
Result betree.BeTree
@@ -948,7 +989,8 @@ def betree.BeTree.apply_back
betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
Result.ret { self with node_id_cnt := nic, root := n }
-/- [betree_main::betree::BeTree::{6}::insert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+ Source: 'src/betree.rs', lines 874:4-874:52 -/
def betree.BeTree.insert
(self : betree.BeTree) (key : U64) (value : U64) (st : State) :
Result (State × Unit)
@@ -960,14 +1002,16 @@ def betree.BeTree.insert
betree.BeTree.apply_back self key (betree.Message.Insert value) st
Result.ret (st0, ())
-/- [betree_main::betree::BeTree::{6}::insert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
+ Source: 'src/betree.rs', lines 874:4-874:52 -/
def betree.BeTree.insert_back
(self : betree.BeTree) (key : U64) (value : U64) (st : State) :
Result betree.BeTree
:=
betree.BeTree.apply_back self key (betree.Message.Insert value) st
-/- [betree_main::betree::BeTree::{6}::delete]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+ Source: 'src/betree.rs', lines 880:4-880:38 -/
def betree.BeTree.delete
(self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) :=
do
@@ -975,12 +1019,14 @@ def betree.BeTree.delete
let _ ← betree.BeTree.apply_back self key betree.Message.Delete st
Result.ret (st0, ())
-/- [betree_main::betree::BeTree::{6}::delete]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
+ Source: 'src/betree.rs', lines 880:4-880:38 -/
def betree.BeTree.delete_back
(self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
betree.BeTree.apply_back self key betree.Message.Delete st
-/- [betree_main::betree::BeTree::{6}::upsert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+ Source: 'src/betree.rs', lines 886:4-886:59 -/
def betree.BeTree.upsert
(self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
:
@@ -992,7 +1038,8 @@ def betree.BeTree.upsert
let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
Result.ret (st0, ())
-/- [betree_main::betree::BeTree::{6}::upsert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
+ Source: 'src/betree.rs', lines 886:4-886:59 -/
def betree.BeTree.upsert_back
(self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
:
@@ -1000,25 +1047,28 @@ def betree.BeTree.upsert_back
:=
betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
-/- [betree_main::betree::BeTree::{6}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+ Source: 'src/betree.rs', lines 895:4-895:62 -/
def betree.BeTree.lookup
(self : betree.BeTree) (key : U64) (st : State) :
Result (State × (Option U64))
:=
betree.Node.lookup self.root key st
-/- [betree_main::betree::BeTree::{6}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
+ Source: 'src/betree.rs', lines 895:4-895:62 -/
def betree.BeTree.lookup_back
(self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
do
let n ← betree.Node.lookup_back self.root key st
Result.ret { self with root := n }
-/- [betree_main::main]: forward function -/
+/- [betree_main::main]: forward function
+ Source: 'src/betree_main.rs', lines 5:0-5:9 -/
def main : Result Unit :=
Result.ret ()
/- Unit test for [betree_main::main] -/
-#assert (main == .ret ())
+#assert (main == Result.ret ())
end betree_main
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index 430d2dda..95f88873 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -6,25 +6,30 @@ import BetreeMain.Types
open Primitives
open betree_main
-/- [betree_main::betree_utils::load_internal_node]: forward function -/
+/- [betree_main::betree_utils::load_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 98:0-98:63 -/
axiom betree_utils.load_internal_node
: U64 → State → Result (State × (betree.List (U64 × betree.Message)))
-/- [betree_main::betree_utils::store_internal_node]: forward function -/
+/- [betree_main::betree_utils::store_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 115:0-115:71 -/
axiom betree_utils.store_internal_node
:
U64 → betree.List (U64 × betree.Message) → State → Result (State ×
Unit)
-/- [betree_main::betree_utils::load_leaf_node]: forward function -/
+/- [betree_main::betree_utils::load_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 132:0-132:55 -/
axiom betree_utils.load_leaf_node
: U64 → State → Result (State × (betree.List (U64 × U64)))
-/- [betree_main::betree_utils::store_leaf_node]: forward function -/
+/- [betree_main::betree_utils::store_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 145:0-145:63 -/
axiom betree_utils.store_leaf_node
: U64 → betree.List (U64 × U64) → State → Result (State × Unit)
-/- [core::option::Option::{0}::unwrap]: forward function -/
+/- [core::option::{core::option::Option<T>}::unwrap]: forward function
+ 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)
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 2f5de6a0..877508f6 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -1,60 +1,67 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [betree_main]: type definitions
import Base
+import BetreeMain.TypesExternal
open Primitives
namespace betree_main
-/- [betree_main::betree::List] -/
+/- [betree_main::betree::List]
+ Source: 'src/betree.rs', lines 17:0-17:23 -/
inductive betree.List (T : Type) :=
| Cons : T → betree.List T → betree.List T
| Nil : betree.List T
-/- [betree_main::betree::UpsertFunState] -/
+/- [betree_main::betree::UpsertFunState]
+ Source: 'src/betree.rs', lines 63:0-63:23 -/
inductive betree.UpsertFunState :=
| Add : U64 → betree.UpsertFunState
| Sub : U64 → betree.UpsertFunState
-/- [betree_main::betree::Message] -/
+/- [betree_main::betree::Message]
+ Source: 'src/betree.rs', lines 69:0-69:23 -/
inductive betree.Message :=
| Insert : U64 → betree.Message
| Delete : betree.Message
| Upsert : betree.UpsertFunState → betree.Message
-/- [betree_main::betree::Leaf] -/
+/- [betree_main::betree::Leaf]
+ Source: 'src/betree.rs', lines 167:0-167:11 -/
structure betree.Leaf where
id : U64
size : U64
mutual
-/- [betree_main::betree::Internal] -/
+/- [betree_main::betree::Internal]
+ Source: 'src/betree.rs', lines 156:0-156:15 -/
inductive betree.Internal :=
| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
-/- [betree_main::betree::Node] -/
+/- [betree_main::betree::Node]
+ Source: 'src/betree.rs', lines 179:0-179:9 -/
inductive betree.Node :=
| Internal : betree.Internal → betree.Node
| Leaf : betree.Leaf → betree.Node
end
-/- [betree_main::betree::Params] -/
+/- [betree_main::betree::Params]
+ Source: 'src/betree.rs', lines 187:0-187:13 -/
structure betree.Params where
min_flush_size : U64
split_size : U64
-/- [betree_main::betree::NodeIdCounter] -/
+/- [betree_main::betree::NodeIdCounter]
+ Source: 'src/betree.rs', lines 201:0-201:20 -/
structure betree.NodeIdCounter where
next_node_id : U64
-/- [betree_main::betree::BeTree] -/
+/- [betree_main::betree::BeTree]
+ Source: 'src/betree.rs', lines 218:0-218:17 -/
structure betree.BeTree where
params : betree.Params
node_id_cnt : betree.NodeIdCounter
root : betree.Node
-/- The state type used in the state-error monad -/
-axiom State : Type
-
end betree_main
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean
new file mode 100644
index 00000000..1701eaaf
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [betree_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..bbac7e99
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 06:19:53 +0000