(**
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