Skip to content
Snippets Groups Projects
Select Git revision
  • e53f1eb7d887f9343af5612e1d05b876fa18c96d
  • develop default protected
  • feature/xfce
  • master
4 results

Dockerfile

Blame
  • pqTree.mli 10.47 KiB
    (** 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 elements. 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 
    
      (** A sequence of all compatible orders of a PQ-tree. *)
      val compatible_orders : 'elt t -> 'elt list IFSeq.seq
    end
    
    (** A functor to build a function to enumerate over PQ-trees. *)
    module MakeEnumerate : 
      functor (_ : 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
    
    
    (** 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 
    
    
    (** Sample a uniformly random compatible order from a PQ-tree. 
        
        @param pqtree the pqtree from which a compatible order must be sampled.
        @return A uniformly random compatible order of [pqtree].
    *)
    val sample_compatible_order : 'elt t -> 'elt list 
    
    
    (** 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 
    
        (** 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 
      type 'value t
    
      val empty : 'value t
      val add : key -> 'value -> 'value t -> 'value t
      val find_opt : key -> 'value t -> 'value option 
      val equal : ('value -> 'value -> bool) -> 'value t -> 'value t -> bool
    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 
      end 
    
    (** 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
    
    (** A functor to derive a function to format a PQ-tree. *)
    module MakePrinter : 
      functor (Prt : PrintableType) -> PrintableType with type t = Prt.t t