Module `Isa_btree`

Isabelle B-tree definitions, as an OCaml lib

include Isa_btree__.Summary

(** Argument to Make functor *)
module type S = sig 
  type k
  type v
  type r
  type t
  val k_cmp     : k -> k -> int
  val monad_ops : t monad_ops
  val cs        : constants
end


(** Result of Make functor *)
module type T = sig
  module S : S
  open S

  type leaf 
  type node
  type leaf_stream

  (** NOTE leaf_ops and node_ops are used externally to convert
     to/from lists *)
  val leaf_ops: (k,v,leaf)leaf_ops
  val node_ops: (k,r,node)node_ops

  val make_btree_ops: 
    store_ops:(r, (node, leaf) dnode, t) store_ops ->
    (k, v, r, t, leaf, node, leaf_stream) pre_btree_ops
end


  (** 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) store_ops = {
    read    : 'r -> ('dnode,'t) m;
    wrte    : 'dnode -> ('r,'t) m;
    rewrite : 'r -> 'dnode -> ('r option, 't) m;
    free    : 'r list -> (unit,'t) m
  }


  (** 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 *)
  type ('k,'v,'r,'ls_state,'t) leaf_stream_ops = {
    make_leaf_stream : 'r -> ('ls_state,'t) m;
    ls_step          : 'ls_state -> ('ls_state option,'t) m;
    ls_kvs           : 'ls_state -> ('k*'v)list;
  }


  (** Pre-map ops, with root passing, exposing leaf and frame *)
  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) m;
    insert      : r:'r -> k:'k -> v:'v -> ('r option,'t) m;
    delete      : r:'r -> k:'k -> ('r,'t) m;
  }


  type ('k,'v,'r,'t,'leaf,'node,'ls) pre_btree_ops = {
    find   : r:'r -> k:'k -> ('r * 'leaf * ('k, 'r, 'node) frame list, 't) m;
    insert : r:'r -> k:'k -> v:'v -> ('r option, 't) m;
    delete : r:'r -> k:'k -> ('r, 't) 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;

    (* FIXME pre_map_ops seems to reproduce find, ... *)
    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
  }

Assertion checking etc

include Isa_export_wrapper.Isa_export_assert_flag

val enable_isa_checks : unit -> unit
val disable_isa_checks : unit -> unit

Code exported from Isabelle, and a wrapper

module Isa_export : sig ... end: This file is exported from Isabelle, and lightly patched (eg to include this comment!). The OCaml interfaces wrap this basic functionality.

module Isa_export_wrapper : sig ... end

Constants

type constants = Constants.constants = { min_leaf_size : int; max_leaf_size : int; min_node_keys : int; max_node_keys : int; }

module Constants : sig ... end: B-tree constants: minimum leaf size etc. These constants should be chosen so that nodes and leaves fit in a block. Clearly this depends on the block size, the size of keys and values, the on-disk format etc.

Main types and interfaces

module Isa_btree_intf : sig ... end: Jane Street-style interface file

type ('node, 'leaf) dnode = ('node, 'leaf) Isa_btree_intf.Dnode_type.dnode

module Store_ops = Isa_btree_intf.Store_ops

type ('r, 'dnode, 't) store_ops = ('r, 'dnode, 't) Store_ops.store_ops
type ('k, 'v, 'leaf) leaf_ops = ('k, 'v, 'leaf) Isa_btree_intf.leaf_ops
type ('k, 'r, 'node) node_ops = ('k, 'r, 'node) Isa_btree_intf.node_ops
type ('k, 'v, 'r, 'ls, 't) leaf_stream_ops = ('k, 'v, 'r, 'ls, 't) Isa_btree_intf.leaf_stream_ops
type ('k, 'v, 'r, 'leaf, 'frame, 't) pre_map_ops = ('k, 'v, 'r, 'leaf, 'frame, 't) Isa_btree_intf.pre_map_ops
type ('k, 'v, 'r, 't, 'leaf, 'node, 'ls) pre_btree_ops = ('k, 'v, 'r, 't, 'leaf, 'node, 'ls) Isa_btree_intf.pre_btree_ops

Main functionality: make a B-tree

module Make : sig ... end: This functor takes various types and constants (including, in particular, the type of keys and the value for the comparison on keys) and generates extra types leaf,node,leaf_stream... for the map implementations. Then there is a function make_btree_ops which takes a store_ops and returns the B-tree operations.

Internal interfaces

module Comparator_to_map_ops = Isa_btree_util.Comparator_to_map_ops

val make_with_k_maps : monad_ops:'a Tjr_monad.monad_ops -> cs:Isa_btree__.Constants_type.constants -> k_cmp:('b -> 'b -> int) -> k_map:('b, 'c, 'd) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> kopt_map:('b option, 'e, 'f) Isa_btree_intf.Leaf_node_frame_map_ops_type.map_ops -> dbg_tree_at_r:('e -> (unit, 'a) Tjr_monad.m) -> ('b, 'c, 'e, 'a, 'd, 'f, ('e, 'd, ('b, 'e, 'f) Isa_btree_intf.frame) Isa_btree__Isa_btree_intf.Internal_leaf_stream_impl_t._t, ('e, ('f, 'd) Isa_btree_intf.dnode, 'a) Isa_btree_intf.store_ops) Isa_export_wrapper.t2: This is the "most general" interface

module Make_with_first_class_module : sig ... end

module Leaf_node_frame_impls : sig ... end

module Isa_btree_util : sig ... end: Given a value k_cmp, construct the corresponding map_ops, with keys: k, k option

module Profilers : sig ... end: Various profilers.