Source

ocaml-lib / logdag.mli

Full commit
(**
Logical DAG (Directed Acyclic Graphs) with objects.

Object descriptions and features represented by formulas are
represented as a DAG. The nodes are labeled by a logical formula, and
a set of objects (extent). The nodes are ordered according to the
entailment relation of the logic. This logic is specified as a
functorial parameter.

The nodes are persistent in a Dbm database, and can be partially
represented in memory, thus allowing for very large DAGs.
*)

(** The first input signature of the functor {!Logdag.Make} specifying various paramters. *)
module type PARAM =
  sig
    val dbname : string (** File name of the Dbm database. Files {i dbname}[.dir] and {i dbname}[.pag] are created if necessary. *)
    val max_mem : float  (** Number of bytes beyond which nodes are removed from memory. *)
    val node_chunk : int  (** Number of nodes that are removed from memory when more than [max_mem] is used. *) 
    val log_file : string option  (** Optional filename for printing a log of internal messages. *)
  end

(** The second input signature of the functor {!Logdag.Make} specifying the logic. *)
module type LOG =
  sig
    type t  (** Abstract type of formulas. *)
    val top : unit -> t  (** Most general formula. *)
    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
    val parse : Syntax.t_stream -> t  (** Parsing of formulas from token streams. *)
    val print : t -> Syntax.t_list  (** Printing of formulas to token lists. *)
    val gen : t -> t -> t list -> t list  (** Dichotomic operator for generating new features. *)
    val simpl : t -> t Stream.t  (** Simplifications of a formula. *)
  end

(** The signature of implementations of logical diagrams. *)
module type T =
  sig
    module Log : LOG
    (** The logic module passed as a parameter. *)

    val some_log : bool
    (** True if a log file is open. *)

    val log_fmt : Format.formatter
    (** The formatter associated to the log file when it exists. *)

    val db : Dbm.t
    (** The database used for persistency and swapping. *)

    type nid = int
    (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)

    val nil : nid
    (** Nil id referencing no node. *)

    val top : nid
    (** Id of the most general node. *)

    type node
    (** Abstract type of nodes.

       {e Warning}: values of this type are relevant at the time they are
	retrieved, but are not guarenteed to remain consistent after changes are
	made. *)

    val feat : node -> Log.t
    (** [feat node] gets the formula label of [node]. *)

    val ext : node -> Ext.t
    (** [ext node] gets the extent label of [node]. *)

    val inf : node -> nid LSet.t
    (** [inf node] gets the inferior (more specific) neighbours of [node]. *)

    val sup : node -> nid LSet.t
    (** [sup node] gets the superior (more general) neighbours of [node]. *)

    val is_obj : node -> bool
    (** [is_obj node] test whether [node] is labeled by an object. *)

    val get : nid -> node
    (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
        @raise Not_found when the node [nid] does not exist in the diagram. *)

    val insert : Log.t -> bool -> nid * bool
    (** [insert f obj] returns the node id whose formula label is
	logically equivalent to [f]. If such a node does not yet exist in the
	diagram, it is inserted and the second result is [true]; otherwise the second result is [false]. 
        If [obj] is true, then a new object is
	associated to this node, and extents of existing nodes are updated
	accordingly. *)

    val remove : nid -> unit
    (** [remove nid] removes the node identified by [nid] from the diagram (both in memory and the database). *)

    val fold : (nid * node Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> 'a -> 'a
    (** [fold f_next (nid,node) e] computes a result through a traversal of
	the diagram. The starting node is specified by [(nid,node)], where
	[node] is the lazy evaluation of [get nid]. The application [f_next (nid,node)
	res] to the current node [(nid,node)] and the current result [res]
	returns a pair [(res',next_nids)], where [res'] is the new result, and
	[next_nids] are the ids of the next nodes to be visited. The traversal
	order is not specified, but each node is ensured to be visited at most
	once. *)

    val first : pred_next:(bool -> nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
    (** [first ~pred_next ~start:(nid,node)] looks for the first nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. The
	first parameter can be used for optimization as, when it is false,
	[None] can be returned in all cases. *)

    val last : pred_next:(nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
    (** [last ~pred_next ~start:(nid,node)] looks for the last nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. *)

    val glbs : pred:(nid * node Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) list
    (** [glbs ~pred nodes] returns the {e glbs} (greatest lower bounds) of the nodes [nodes] among the nodes satisfying [pred]. *)

    val lubs : pred:(nid * node Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) list -> 'a list
    (** [lubs ~pred ~suppmin nodes] returns the [suppmin]-approximate {e lubs}
	(least upper bounds) of the nodes [nodes] among the nodes satisfying
	[pred]. A node is a [suppmin]-approximate lub if it has at least
	[suppmin] more specific nodes in [nodes]. The second argument of
	[pred] is the support of the node (number of more specific nodes in
	[nodes]). *)

  end

(** Functor building an implementation of logical DAGs. *)
module Make (Param : PARAM) (Log : LOG) : T