Module E.Stm

module C = C
type t = private {
  1. id : int;
    (*

    unique ID of the stream

    *)
  2. parents : C.t list;
    (*

    parent clauses for inference generating this stream

    *)
  3. mutable penalty : int;
    (*

    heuristic penalty

    *)
  4. mutable hits : int;
    (*

    how many attemts to retrieve unifier were there

    *)
  5. mutable stm : C.t option OSeq.t;
    (*

    the stream itself

    *)
}
exception Empty_Stream
exception Drip_n_Unfinished of C.t option list * int * int

Basics

val make : ?penalty:int -> parents:C.t list -> C.t option OSeq.t -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val id : t -> int
val is_empty : t -> bool
val penalty : t -> int
val drip : t -> C.t option

Remove the first element in the stream and return it.

val drip_n : t -> int -> int -> C.t option list

Attempt to remove the n first elements in the stream and return them. Return less if the guard is reached.

  • raises Drip_n_Unfinished(cl,n)

    where cl is the list of elements already found and n the number of elements if the stream contains less than n elements

IO