diff --git a/lib/pqtree/pqTree.ml b/lib/pqtree/pqTree.ml
index 5e70190c7a51a8c42d0f72c6d851f5e2238814eb..8f6436c3a72eed5b3beb045a4b709796020468a0 100644
--- a/lib/pqtree/pqTree.ml
+++ b/lib/pqtree/pqTree.ml
@@ -233,7 +233,7 @@ module type CanonicalSig =
val canonical : elt t -> elt t
val compare : elt t -> elt t -> int
val compare' : elt t -> elt t -> int
- type nonrec t = elt t
+ type nonrec t = elt t
end
diff --git a/lib/pqtree/pqTree.mli b/lib/pqtree/pqTree.mli
index 2d60bea665faca39acd349ead026e93c45d19fa1..3fe47b2050e62caaec8e0360071e386a128a9d5c 100644
--- a/lib/pqtree/pqTree.mli
+++ b/lib/pqtree/pqTree.mli
@@ -1,65 +1,241 @@
+(** This module defines what is a PQ-tree over some set, as an
+ inductive data type. A PQ-tree is a data structure encoding a
+ subset of permutations. Not every subset of permutations can be
+ encoded as a PQ-tree. It will be convenient to interpret
+ permutations as ordered sequences of elements.
+
+ Pq-trees where introduced in: Kellogg S. Booth, George S. Lueker,
+ {i Testing for the consecutive ones property, interval graphs, and
+ graph planarity using PQ-tree algorithms}, Journal of Computer and
+ System Sciences, Volume 13, Issue 3, 1976, Pages 335-379, ISSN
+ 0022-0000, {{:https://doi.org/10.1016/S0022-0000(76)80045-1}}.
+
+This module also defines some operations on PQ-trees, in particular on
+ permutations encoded by a PQ-tree, and other convenience
+ functions. *)
+
+
+(** The type of PQ-tree, over a set of elements of type 'elt.
+
+ A leaf [Leaf a] encodes the permutation {%$(a)$%} on the singleton set {%$\{a\}$%}.
+
+ A P-node [P [t1;...;tn]] encodes all the permutations that can be
+ obtained by concatenating {%$\sigma_1,\ldots,\sigma_n$%} in an
+ arbitrary order, where each {%$\sigma_i$%} is a permutation
+ encoded by [ti].
+
+ A Q-node [Q [t1,...tn]] encodes all the permutations {%$\sigma_1
+ \sigma_2 \ldots \sigma_n$%} and
+ {%$\sigma_n,\ldots,\sigma_2,\sigma_1$%} where each {%$\sigma_i$%}
+ is a permutation encoded by [ti].
+*)
type 'elt t =
| Leaf of 'elt
| P of 'elt t list
| Q of 'elt t list
+
+(** [length tree] is the number of elements in the PQ-tree [tree], that is
+ the length of permutations encoded by the PQ-tree.
+
+ @param tree a PQ-tree
+ @return the number of elements in the permutations encoded by [tree]
+*)
val length : 'elt t -> int
+(** An enumeration of the permutations encoded by a given PQ-tree.
+
+ @param tree a PQ-tree
+ @return the sequence of all the permutations encoded by [tree]
+*)
val enumerate_permutation : 'elt t -> 'elt list Seq.t
+
+(** The number of permutations encoded by a given PQ-tree.
+
+ @param tree a PQ-tree
+ return the number of permutations encoded by [tree]
+ *)
val count_permutations : 'elt t -> Big_int_Z.big_int
+(** A random permutation among those encoded by a given PQ-tree.
+
+ @param tree a PQ-tree
+ @return a random permutation, as a list of elements, chosen uniformly randomly among all permutations encoded by [tree]
+*)
val sample_permutation : 'elt t -> 'elt list
+(** A random interval for the set of permutations encoded by a given
+ PQ-tree. An {i interval} for a set of permutation
+ {%$\mathcal{P}$%} is a subset of elements that appears
+ consecutively in any permutation in the set {%$\mathcal{P}$%}. The
+ interval is sampled by first sampling a uniformly chosen
+ permutation, then sampling in this permutation a random
+ subsequence of elemnts. This sampling is not uniform in general.
+
+ @param tree a PQ-tree
+ @return a random interval for the set of permutations encoded by [tree]
+*)
val sample_interval : 'elt t -> 'elt list
+(** The set of elements in a PQ-tree, in left-to-right order. In
+ particular, the frontier is one of the encoded permutation of the
+ PQ-tree.
+
+ @param tree a PQ-tree
+ @return the frontier of [tree]: its elements in left-to-right order.
+*)
val frontier : 'elt t -> 'elt list
+
+(** A shrinking function that can be used for property testing: given
+ a PQ-tree [tree], it returns a sequence of PQ-trees obtained each
+ by contracting one node of [tree].
+
+ @param tree a PQ-tree
+ @return a sequence of smaller PQ-trees.
+*)
val shrink : 'elt t -> 'elt t Seq.t
+
+(** A PQ-tree that encodes the same set of permutations, obtained by
+ reordering the children of each P-node in a uniformly random
+ order, and reversing the order of children under Q-nodes with
+ probability 1/2.
+
+ @param tree a PQ-tree
+ @return a random PQ-tree encoding the same set of permutations
+*)
val shuffle : 'elt t -> 'elt t
+
+(** Checks whether a PQ-tree is well-formed, that is each P-node has
+ at least two children (otherwise it can be contracted), and each
+ Q-node has a least three children (otherwise it can be replaced by
+ a P-node or contracted).
+
+ @param tree a PQ-tree
+ @return [true] if [tree] is well-formed.
+*)
val is_well_formed : 'elt t -> bool
+
+(** A skeleton of a PQ-tree defines the structure of the PQ-tree in
+ terms of P-node and Q-node, by there is no specified elements.
+ Each element is replaced by a {i hole}. This is equivalent to
+ quotienting the set of PQ-trees by the ground set on which the
+ permutations are defined (thus abstracting the ground set).
+*)
module Skeleton :
sig
+
+ (** The type of a PQ-tree skeleton, made of leafs ([Hole]), P-nodes and Q-nodes. *)
type skeleton =
| Hole
| HoledP of skeleton list
| HoledQ of skeleton list
+ (** Derive a PQ-tree on an interval {%$\{0,1,\ldots,n-1\}$%}, from a
+ skeleton, by replacing each node by a distinct integer, in
+ increasing order from left to right.
+
+ @param skeleton a skeleton of PQ-tree
+ @return a PQ-tree whose skeleton is [skeleton] and whose
+ frontier is {%$\{0,1,\ldots,n-1\}$%}
+ *)
val to_pqtree : skeleton -> int t
end
+(** A type for modules providing enumeration capabilities, as defined
+ by the Feat library, enriched with the capability to enumerate
+ over PQ-trees over a given type of elements.
+ *)
module type EnumerateSig =
sig
+
+ (** The type of elements of the encoded permutations. *)
type elt
+
include FeatCore.EnumSig.ENUM
+
+ (** An enumeration of all PQ-trees over some type of elements *)
val enumeration : elt t enum
end
-module MakeEnumerate : functor (RND : FeatCore.RandomSig.S) -> EnumerateSig with type elt = int
+(** A functor to build a function to enumerate over PQ-trees. *)
+module MakeEnumerate :
+ functor (RND : FeatCore.RandomSig.S) -> EnumerateSig with type elt = int
+
+(** A pre-application of the [MakeEnumerate] functor, to enumerate of
+ PQ-trees over integers.
+*)
module Enum : EnumerateSig with type elt = int
-val sample : int -> int t
+(** Sample a uniformly random PQ-tree over an interval
+ {%$\{0,1,\ldots,n-1\}$%} of integers.
+
+ @param n the length of permutations encoded by the sampled PQ-tree
+ return the sampled PQ-tree over permutations of length [n]
+*)
+val sample : int -> int t
+(** A type for modules providing functions to define a canonical
+ representation of equivalent PQ-trees, where two PQ-trees are
+ equivalent when they encode the same set of permutations.
+*)
module type CanonicalSig =
sig
+
+ (** The type of elements of the permutations encoded by the PQ-trees *)
type elt
+
+ (** Finds the canonical representation of a subset of permutations
+ encoded by a PQ-tree.
+
+ @param [tree] a PQ-tree
+ @return A canonical PQ-tree representing the set of
+ permutation encoded by [tree]
+ *)
val canonical : elt t -> elt t
+
+ (** Compares the set of permutations encoded by two PQ-trees. This
+ is done by comparing the two canonical PQ-tree representations for
+ each set of permutations.
+
+ @param tree1 A PQ-tree
+ @param tree2 A PQ-tree
+ @return the result of comparing the two subsets of
+ permutations encoded by [tree1] and [tree2]
+ *)
val compare : elt t -> elt t -> int
+
+ (** Compares two PQ-trees. Two different PQ-trees encoding the
+ same set of permutations will be considered different under
+ this comparison.
+
+ @param tree1 A PQ-tree
+ @param tree2 A PQ-tree
+ @return the result of comparing [tree1] and [tree2]
+ *)
val compare' : elt t -> elt t -> int
- type nonrec t = elt t
- end
+ (** The type of PQ-trees with elements of type [elt]. This allows
+ a module with this type to be used in a functor expecting an
+ ordered type. *)
+ type nonrec t = elt t
+ end
+(** A functor to make comparison and canonization function for
+ PQ-trees, given an ordered type of elements.
+*)
module MakeCanonical : functor (C : Map.OrderedType) -> CanonicalSig with type elt = C.t
+(** The type of modules proposing minimal [Map] functionalities. *)
module type EltMap =
sig
type key
@@ -72,24 +248,65 @@ sig
end
+(** The type of modules allowing to check whether a permutation is
+ contained in the set of permutations represented by a PQ-tree. *)
module type CheckPermutationSig =
sig
+
+ (** The type of elements on which the permutations are defined. *)
type elt
+
+ (** Checks whether a permutation is contained in the subset of
+ permutations encoded by a PQ-tree.
+
+ @param tree a PQ-tree
+ @param permutation a permutation
+ @return [true] if [permutation] is contained in the set of
+ permutations represented by [tree].
+ *)
+ val contains_permutation : elt t -> elt list -> bool
+
+
+ (** A checker for a PQ-tree is able to check whether any
+ permutation is contained in the set of permuttaions
+ represented by the PQ-tree. This allows to build a checker
+ once and use it multiple times for many permutations. *)
type checker
+
+
+ (** Computes a checker for a given PQ-tree.
+
+ @param tree a PQ-tree
+ @return a checker for [tree]
+ *)
val checker : elt t -> checker
+
+
+ (** Decides whether a permutation is contained in the set of
+ permutations represented by a PQ-tree
+
+ @param checker a checker for a PQ-tree [tree]
+ @param permutation a permutation
+ @return [true] if [permutation] is contained in the set of
+ permutations represented by [tree]
+ *)
val checks : checker -> elt list -> bool
- val contains_permutation : elt t -> elt list -> bool
end
-module MakeCheckPermutation : functor(M : EltMap) -> CheckPermutationSig with type elt = M.key
-
+(** A functor to derive functions to check whether a permutation is
+ contained in the set of permutations represented by a PQ-tree. *)
+module MakeCheckPermutation :
+ functor(M : EltMap) -> CheckPermutationSig with type elt = M.key
+(** The type of modules encoding a formattable type. *)
module type PrintableType = sig
type t
val print : Format.formatter -> t -> unit
end
-module MakePrinter : functor (Prt : PrintableType) -> PrintableType with type t = Prt.t t
+(** A functor to derive a function to format a PQ-tree. *)
+module MakePrinter :
+ functor (Prt : PrintableType) -> PrintableType with type t = Prt.t t