Module Isa_btree.Isa_btree_intf

Jane Street-style interface file

type ('a, 'b) ty_eq = ('a, 'b) Base.Type_equal.t
module Dnode_type : sig ... end
include Dnode_type
type ('node, 'leaf) dnode = ('node, 'leaf) Isa_export.Disk_node.dnode =
| Disk_node of 'node
| Disk_leaf of 'leaf

Recall dnode type

Node, leaf and frame types

Frames

module Frame_type : sig ... end
type ('k, 'r, 'node) frame = ('k, 'r, 'node) Frame_type.frame
module Internal_leaf_node : sig ... end
module Abstract_leaf_node_frame_types : sig ... end
include Abstract_leaf_node_frame_types
type nonrec ('k, 'r, 'cmp) node = ('k, 'r, 'cmp) Internal_leaf_node.node
type nonrec ('k, 'v, 'cmp) leaf = ('k, 'v, 'cmp) Internal_leaf_node.leaf
module Internal_leaf_stream_impl_t : sig ... end
module Abstract_leaf_stream : sig ... end
module Leaf_ops_type : sig ... end
include Leaf_ops_type
type ('k, 'v, 'leaf) leaf_ops = {
leaf_lookup : 'k -> 'leaf -> 'v option;
leaf_insert : 'k -> 'v -> 'leaf -> 'leaf * 'v option;
leaf_remove : 'k -> 'leaf -> 'leaf;
leaf_length : 'leaf -> int;
leaf_steal_right : ('leaf * 'leaf) -> 'leaf * 'k * 'leaf;
leaf_steal_left : ('leaf * 'leaf) -> 'leaf * 'k * 'leaf;
leaf_merge : ('leaf * 'leaf) -> 'leaf;
split_large_leaf : int -> 'leaf -> 'leaf * 'k * 'leaf;
leaf_to_kvs : 'leaf -> ('k * 'v) list;
kvs_to_leaf : ('k * 'v) list -> 'leaf;
}

As Isabelle def. See \doc(doc:leaf_ops). Note: the empty leaf can be obtained by calling kvs_to_leaf on the empty list.

module Node_ops_type : sig ... end
include Node_ops_type
type ('k, 'r, 'node) node_ops = {
split_node_at_k_index : int -> 'node -> 'node * 'k * 'node;
node_merge : ('node * 'k * 'node) -> 'node;
node_steal_right : ('node * 'k * 'node) -> 'node * 'k * 'node;
node_steal_left : ('node * 'k * 'node) -> 'node * 'k * 'node;
node_keys_length : 'node -> int;
node_make_small_root : ('r * 'k * 'r) -> 'node;
node_get_single_r : 'node -> 'r;
node_to_krs : 'node -> 'k list * 'r list;
krs_to_node : ('k list * 'r list) -> 'node;
}
module Frame_ops_type : sig ... end
include Frame_ops_type
module Internal_bottom_or_top = Frame_ops_type.Internal_bottom_or_top
type ('k, 'r) segment = 'k Internal_bottom_or_top.or_bottom * 'r * ('k * 'r) list * 'k Internal_bottom_or_top.or_top
type ('k, 'r, 'frame, 'node) frame_ops = {
split_node_on_key : 'r -> 'k -> 'node -> 'frame;
midpoint : 'frame -> 'r;
get_focus : 'frame -> 'k Internal_bottom_or_top.or_bottom * 'r * 'k Internal_bottom_or_top.or_top;
get_focus_and_right_sibling : 'frame -> ('k Internal_bottom_or_top.or_bottom * 'r * 'k * 'r * 'k Internal_bottom_or_top.or_top) option;
get_left_sibling_and_focus : 'frame -> ('k Internal_bottom_or_top.or_bottom * 'r * 'k * 'r * 'k Internal_bottom_or_top.or_top) option;
replace : ('k, 'r) segment -> ('k, 'r) segment -> 'frame -> 'frame;
frame_to_node : 'frame -> 'node;
get_midpoint_bounds : 'frame -> 'k option * 'k option;
backing_node_blk_ref : 'frame -> 'r;
split_node_for_leaf_stream : 'r -> 'node -> 'frame;
step_frame_for_leaf_stream : 'frame -> 'frame option;
dbg_frame : 'frame -> unit;
}

See Isabelle defn. See \doc(doc:frame_ops)

type ('a, 'b, 'c) leaf_node_frame_ops = {
leaf_ops : 'a;
node_ops : 'b;
frame_ops : 'c;
}

For packaging

Store operations

module Store_ops : sig ... end
include Store_ops
type ('r, 'dnode, 't) store_ops = {
read : 'r -> ('dnode, 't) Tjr_monad.m;
wrte : 'dnode -> ('r, 't) Tjr_monad.m;
rewrite : 'r -> 'dnode -> ('r option, 't) Tjr_monad.m;
free : 'r list -> (unit, 't) Tjr_monad.m;
}

store_ops are like a blk device, but allowing read/writes of leafs and nodes rather than blks (so, marshalling is done in a lower layer)

NOTE rewrite attempts to rewrite a block; this may not be allowed (CoW) and instead a new block is allocated and written

NOTE also that 'dnode is either leaf or node

type ('r, 'dnode, 't) t = ('r, 'dnode, 't) store_ops

Pre-map operations

module Pre_map_ops_type : sig ... end
include Pre_map_ops_type
type ('k, 'v, 'r, 'leaf, 'frame, 't) pre_map_ops = {
leaf_lookup : 'k -> 'leaf -> 'v option;
find : r:'r -> k:'k -> ('r * 'leaf * 'frame list, 't) Tjr_monad.m;
insert : r:'r -> k:'k -> v:'v -> ('r option, 't) Tjr_monad.m;
delete : r:'r -> k:'k -> ('r, 't) Tjr_monad.m;
}

Pre-map ops, with root passing, exposing leaf and frame

Leaf stream operations

module Leaf_stream_ops_type : sig ... end
include Leaf_stream_ops_type
type ('k, 'v, 'r, 'ls_state, 't) leaf_stream_ops = {
make_leaf_stream : 'r -> ('ls_state, 't) Tjr_monad.m;
ls_step : 'ls_state -> ('ls_state option, 't) Tjr_monad.m;
ls_kvs : 'ls_state -> ('k * 'v) list;
}

Leaf-stream ops. Note that ls_leaf always returns a leaf i.e. each step transitions from one leaf to the next. FIXME not concurrent safe- may need CoW or detailed analysis of concurrent mutations on B-tree or at worst blocking of conc mutation or ls failure

Insert many

The semantics of this operation is: for a list of (k,v), the operation inserts some kvs, and returns the rest.

module Insert_many_type : sig ... end
include Insert_many_type
type ('k, 'v, 'r, 't) insert_many_type = {
insert_many : r:'r -> k:'k -> v:'v -> kvs:('k * 'v) list -> (('k * 'v) list * 'r option, 't) Tjr_monad.m;
}

Insert all

The semantics of this operation is: for a list of (k,v), the operation inserts all kvs, and returns the updated root (or the original root if tree was updated in place).

module Insert_all_type : sig ... end
include Insert_all_type
type ('k, 'v, 'r, 't) insert_all_type = {
insert_all : r:'r -> kvs:('k * 'v) list -> ('r, 't) Tjr_monad.m;
}

B-tree (pre-) ops

module Pre_btree_ops_type : sig ... end

A record of operations provided by the B-tree

include Pre_btree_ops_type
type ('k, 'v, 'r, 't, 'leaf, 'node, 'ls) pre_btree_ops = {
find : r:'r -> k:'k -> ('r * 'leaf * ('k, 'r, 'node) frame list, 't) Tjr_monad.m;
insert : r:'r -> k:'k -> v:'v -> ('r option, 't) Tjr_monad.m;
delete : r:'r -> k:'k -> ('r, 't) Tjr_monad.m;
leaf_stream_ops : ('k, 'v, 'r, 'ls, 't) leaf_stream_ops;
leaf_ops : ('k, 'v, 'leaf) leaf_ops;
node_ops : ('k, 'r, 'node) node_ops;
pre_map_ops : ('k, 'v, 'r, 'leaf, ('k, 'r, 'node) frame, 't) pre_map_ops;
insert_many : ('k, 'v, 'r, 't) insert_many_type;
insert_all : ('k, 'v, 'r, 't) insert_all_type;
}
module Leaf_node_frame_map_ops_type : sig ... end
type ('s, 't) type_conversions = {
s_to_t : 's -> 't;
t_to_s : 't -> 's;
}