Module KTSizedChainSource

Sourcetype __ = Obj.t
Sourceval app : 'a1 list -> 'a1 list -> 'a1 list
Sourcetype ('a, 'p) sigT =
  1. | ExistT of 'a * 'p
Sourceval projT1 : ('a1, 'a2) sigT -> 'a1
Sourceval projT2 : ('a1, 'a2) sigT -> 'a2
Sourcemodule Nat : sig ... end
Sourcetype 'a xpow = __
Sourceval xflat : int -> 'a1 xpow -> 'a1 list
Sourcemodule ElementTree : sig ... end
Sourcetype 'x buf5 =
  1. | B0
  2. | B1 of 'x
  3. | B2 of 'x * 'x
  4. | B3 of 'x * 'x * 'x
  5. | B4 of 'x * 'x * 'x * 'x
  6. | B5 of 'x * 'x * 'x * 'x * 'x
Sourceval buf5_seq : ('a1 -> 'a2 list) -> 'a1 buf5 -> 'a2 list
Sourceval buf5_push_naive : 'a1 -> 'a1 buf5 -> 'a1 buf5 option
Sourceval buf5_inject_naive : 'a1 buf5 -> 'a1 -> 'a1 buf5 option
Sourceval buf5_pop_naive : 'a1 buf5 -> ('a1 * 'a1 buf5) option
Sourceval buf5_eject_naive : 'a1 buf5 -> ('a1 buf5 * 'a1) option
Sourcetype color =
  1. | Green
  2. | Yellow
  3. | Red
Sourcemodule E : sig ... end
Sourcetype 'a packet =
  1. | Hole
  2. | PNode of 'a E.t buf5 * 'a packet * 'a E.t buf5
Sourcetype 'a chain =
  1. | Ending of 'a E.t buf5
  2. | ChainCons of 'a packet * 'a chain
Sourceval buf_seq_E : 'a1 E.t buf5 -> 'a1 list
Sourceval packet_seq : 'a1 packet -> 'a1 list -> 'a1 list
Sourceval chain_seq : 'a1 chain -> 'a1 list
Sourceval chain_to_list : 'a1 chain -> 'a1 list
Sourcemodule Coq_E : sig ... end
Sourceval green_push : 'a1 -> 'a1 buf5 -> 'a1 buf5 option
Sourceval green_inject : 'a1 buf5 -> 'a1 -> 'a1 buf5 option
Sourceval yellow_push : 'a1 -> 'a1 buf5 -> 'a1 buf5 option
Sourceval yellow_inject : 'a1 buf5 -> 'a1 -> 'a1 buf5 option
Sourceval green_pop : 'a1 buf5 -> ('a1 * 'a1 buf5) option
Sourceval green_eject : 'a1 buf5 -> ('a1 buf5 * 'a1) option
Sourceval yellow_pop : 'a1 buf5 -> ('a1 * 'a1 buf5) option
Sourceval yellow_eject : 'a1 buf5 -> ('a1 buf5 * 'a1) option
Sourceval prefix23 : 'a1 option -> ('a1 * 'a1) -> 'a1 buf5
Sourceval suffix23 : ('a1 * 'a1) -> 'a1 option -> 'a1 buf5
Sourceval suffix12 : 'a1 -> 'a1 option -> 'a1 buf5
Sourcetype 'x bdecomp_pre =
  1. | BD_pre_underflow of 'x option
  2. | BD_pre_ok of 'x buf5
  3. | BD_pre_overflow of 'x buf5 * 'x * 'x
Sourcetype 'x bdecomp_suf =
  1. | BD_suf_underflow of 'x option
  2. | BD_suf_ok of 'x buf5
  3. | BD_suf_overflow of 'x buf5 * 'x * 'x
Sourceval prefix_decompose : 'a1 buf5 -> 'a1 bdecomp_pre
Sourceval suffix_decompose : 'a1 buf5 -> 'a1 bdecomp_suf
Sourcetype 'x bsandwich =
  1. | BS_alone of 'x option
  2. | BS_sandwich of 'x * 'x buf5 * 'x
Sourceval buffer_unsandwich : 'a1 buf5 -> 'a1 bsandwich
Sourceval prefix_rot : 'a1 -> 'a1 buf5 -> 'a1 buf5 * 'a1
Sourceval suffix_rot : 'a1 buf5 -> 'a1 -> 'a1 * 'a1 buf5
Sourceval buffer_halve : 'a1 buf5 -> 'a1 option * ('a1 * 'a1) buf5
Sourceval green_prefix_concat : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> ('a1 Coq_E.t buf5 * 'a1 Coq_E.t buf5) option
Sourceval green_suffix_concat : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> ('a1 Coq_E.t buf5 * 'a1 Coq_E.t buf5) option
Sourceval prefix_concat : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> ('a1 Coq_E.t buf5 * 'a1 Coq_E.t buf5) option
Sourceval suffix_concat : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> ('a1 Coq_E.t buf5 * 'a1 Coq_E.t buf5) option
Sourceval buffer_push_chain : 'a1 Coq_E.t -> 'a1 Coq_E.t buf5 -> 'a1 chain
Sourceval buffer_inject_chain : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t -> 'a1 chain
Sourceval pair_one : ('a1 Coq_E.t * 'a1 Coq_E.t) -> 'a1 Coq_E.t option
Sourceval pair_each_buf : ('a1 Coq_E.t * 'a1 Coq_E.t) buf5 -> 'a1 Coq_E.t buf5 option
Sourceval mk_ending_from_options : 'a1 Coq_E.t option -> ('a1 Coq_E.t * 'a1 Coq_E.t) option -> 'a1 Coq_E.t option -> 'a1 chain
Sourceval make_small : 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> 'a1 Coq_E.t buf5 -> 'a1 chain option
Sourcetype 'a kChain =
  1. | KEnding of 'a Coq_E.t buf5
  2. | KCons of color * 'a packet * 'a kChain
Sourceval chain_to_kchain_g : 'a1 chain -> 'a1 kChain
Sourceval kchain_to_chain : 'a1 kChain -> 'a1 chain
Sourceval kchain_to_list : 'a1 kChain -> 'a1 list
Sourceval green_of_red_k : 'a1 kChain -> 'a1 kChain option
Sourcemodule Coq0_E : sig ... end
Sourcetype 'a sChain =
  1. | SEnding of int * 'a Coq0_E.t buf5
  2. | SCons of int * color * 'a packet * 'a kChain
Sourceval s_empty : 'a1 sChain
Sourceval s_size : 'a1 sChain -> int
Sourceval s_erase : 'a1 sChain -> 'a1 kChain
Sourceval s_of : int -> 'a1 kChain -> 'a1 sChain
Sourceval s_to_list : 'a1 sChain -> 'a1 list
Sourceval yellow_wrap_s : 'a1 sChain -> int -> 'a1 Coq0_E.t buf5 -> 'a1 packet -> 'a1 Coq0_E.t buf5 -> 'a1 kChain -> 'a1 sChain
Sourceval push_s : 'a1 Coq0_E.t -> 'a1 sChain -> 'a1 sChain
Sourceval inject_s : 'a1 sChain -> 'a1 Coq0_E.t -> 'a1 sChain
Sourcetype 'a spop_result =
  1. | SPopFail
  2. | SPopOk of 'a Coq0_E.t * 'a sChain
Sourceval pop_s : 'a1 sChain -> 'a1 spop_result
Sourceval eject_s : 'a1 sChain -> 'a1 spop_result