Source

ocaml-lib / logdag.mli

(**
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. *) 
  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 : t  (** Most general formula. *)
    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
  end

(** Functor building an implementation of logical DAGs. *)
module Make (Param : PARAM) (Log : LOG) :
  sig
    module Log : LOG
    (** The logic module passed as a parameter. *)

    type nid
    (** 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 top : nid
    (** Id of the most general node. *)

    (** Module for the representation of extents (sets of objects). *)
    module Ext :
      sig
        type t  (** Abstract type of extents. *)
        val empty : t  (** The empty extent. *)
        val is_empty : t -> bool  (** [is_empty ext] tests whether [ext] is empty. *)
        val cardinal : t -> int  (** [cardinal ext] returns the size of the extent [ext]. *)
        val mem : nid -> t -> bool  (** [mem o ext] tests whether [o] belongs to [ext]. *)
        val contains : t -> t -> bool  (** [contains ext1 ext2] tests whether [ext1] contains [ext2]. *)
        val add : nid -> t -> t  (** [add o ext] returns the addition of [o] to [ext]. *)
        val remove : nid -> t -> t  (** [remove o ext] returns the removal of [o] from [ext]. *)
        val union : t -> t -> t  (** [union ext1 ext2] returns the set union of [ext1] and [ext2]. *)
        val union_r : t list -> t  (** [union_r exts] returns the union of all extents in [exts]. *)
        val inter : t -> t -> t  (** [inter ext1 ext2] returns the set intersection of [ext1] and [ext2]. *)
        val inter_r : t list -> t  (** [inter_r exts] returns the intersection of all extents in [exts].
                                       @raise Invalid_argument if [exts] is the empty list. *)
        val subtract : t -> t -> t  (** [subtract ext1 ext2] returns the set subtraction of [ext1] and [ext2]. *)
        val inter_difsym : t -> t -> t * t * t
          (** [inter_difsym ext1 ext2] returns the extent triplet [(subtract ext1 ext2, inter ext1 ext2, subtract ext2 ext1)]. *)
        val iter : (nid -> unit) -> t -> unit
          (** Iteration on the objects of an extent (see [List.iter]). Objects visited from low ids to high ids. *)
        val fold_left : ('a -> nid -> 'a) -> 'a -> t -> 'a
          (** Folding on an extent from low ids to high ids (see List.fold_left). *)
        val fold_right : (nid -> 'a -> 'a) -> t -> 'a -> 'a
          (** Folding on an extent from high ids to low ids (see List.fold_right). *)
      end

    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 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 forget : nid -> unit
    (** [forget nid] removes the node identified by [nid] from the memory, after saving it in the database. *)

    val sync : unit -> unit
    (** [sync ()] synchronizes the database with the memory contents. *)

    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 -> 'a -> 'a * nid list) -> nid * node -> '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] must be equal to [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 -> 'a option * nid list) -> start:(nid * node) -> '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 -> 'a option * nid list) -> start:(nid * node) -> '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 -> bool) -> (nid * node) list -> (nid * node) 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 -> int -> 'a option) -> suppmin:int -> (nid * node) 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
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.