    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE ImplicitParams             #-}

    module Agda.Termination.CallMatrix where

    -- module Agda.Termination.CallMatrix
    --   ( CallMatrix'(..), CallMatrix
    --   , callMatrix
    --   , CallComb(..)
    --   , tests
    --   ) where

    import Agda.Termination.CutOff
    import Agda.Termination.Order as Order
    import Agda.Termination.SparseMatrix as Matrix
    import Agda.Termination.Semiring (HasZero(..))

    import Agda.Utils.Favorites (Favorites)
    import qualified Agda.Utils.Favorites as Fav

    import Agda.Utils.Null
    import Agda.Utils.PartialOrd
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Singleton

    ------------------------------------------------------------------------
    --  * Call matrices
    ------------------------------------------------------------------------

    -- | Call matrix indices = function argument indices.
    --
    --   Machine integer 'Int' is sufficient, since we cannot index more arguments
    --   than we have addresses on our machine.

    type ArgumentIndex = Int

    -- | Call matrices.
    --
    --   A call matrix for a call @f --> g@ has dimensions @ar(g) × ar(f)@.
    --
    --   Each column corresponds to one formal argument of caller @f@.
    --   Each row corresponds to one argument in the call to @g@.
    --
    --   In the presence of dot patterns, a call argument can be related
    --   to /several/ different formal arguments of @f@.
    --
    --   See e.g. @test/succeed/DotPatternTermination.agda@:
    --
    --   @
    --     data D : Nat -> Set where
    --       cz : D zero
    --       c1 : forall n -> D n -> D (suc n)
    --       c2 : forall n -> D n -> D n
    --
    --     f : forall n -> D n -> Nat
    --     f .zero    cz        = zero
    --     f .(suc n) (c1  n d) = f n (c2 n d)
    --     f n        (c2 .n d) = f n d
    --   @
    --
    --   Call matrices (without guardedness) are
    --
    --   @
    --           -1 -1   n < suc n  and       n <  c1 n d
    --            ?  =                   c2 n d <= c1 n d
    --
    --            = -1   n <= n     and  n < c2 n d
    --            ? -1                   d < c2 n d
    --   @
    --
    --   Here is a part of the original documentation for call matrices
    --   (kept for historical reasons):
    --
    --   This datatype encodes information about a single recursive
    --   function application. The columns of the call matrix stand for
    --   'source' function arguments (patterns). The rows of the matrix stand for
    --   'target' function arguments. Element @(i, j)@ in the matrix should
    --   be computed as follows:
    --
    --     * 'Order.lt' (less than) if the @j@-th argument to the 'target'
    --       function is structurally strictly smaller than the @i@-th
    --       pattern.
    --
    --     * 'Order.le' (less than or equal) if the @j@-th argument to the
    --       'target' function is structurally smaller than the @i@-th
    --       pattern.
    --
    --     * 'Order.unknown' otherwise.

    newtype CallMatrix' a = CallMatrix { forall a. CallMatrix' a -> Matrix ArgumentIndex a
    mat :: Matrix ArgumentIndex a }
      deriving (CallMatrix' a -> CallMatrix' a -> Bool
    (CallMatrix' a -> CallMatrix' a -> Bool)
    -> (CallMatrix' a -> CallMatrix' a -> Bool) -> Eq (CallMatrix' a)
    forall a. Eq a => CallMatrix' a -> CallMatrix' a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => CallMatrix' a -> CallMatrix' a -> Bool
    == :: CallMatrix' a -> CallMatrix' a -> Bool
    $c/= :: forall a. Eq a => CallMatrix' a -> CallMatrix' a -> Bool
    /= :: CallMatrix' a -> CallMatrix' a -> Bool
    Eq, Eq (CallMatrix' a)
    Eq (CallMatrix' a) =>
    (CallMatrix' a -> CallMatrix' a -> Ordering)
    -> (CallMatrix' a -> CallMatrix' a -> Bool)
    -> (CallMatrix' a -> CallMatrix' a -> Bool)
    -> (CallMatrix' a -> CallMatrix' a -> Bool)
    -> (CallMatrix' a -> CallMatrix' a -> Bool)
    -> (CallMatrix' a -> CallMatrix' a -> CallMatrix' a)
    -> (CallMatrix' a -> CallMatrix' a -> CallMatrix' a)
    -> Ord (CallMatrix' a)
    CallMatrix' a -> CallMatrix' a -> Bool
    CallMatrix' a -> CallMatrix' a -> Ordering
    CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall a. Ord a => Eq (CallMatrix' a)
    forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
    forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Ordering
    forall a. Ord a => CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    $ccompare :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Ordering
    compare :: CallMatrix' a -> CallMatrix' a -> Ordering
    $c< :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
    < :: CallMatrix' a -> CallMatrix' a -> Bool
    $c<= :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
    <= :: CallMatrix' a -> CallMatrix' a -> Bool
    $c> :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
    > :: CallMatrix' a -> CallMatrix' a -> Bool
    $c>= :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
    >= :: CallMatrix' a -> CallMatrix' a -> Bool
    $cmax :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    max :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    $cmin :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    min :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a
    Ord, ArgumentIndex -> CallMatrix' a -> ShowS
    [CallMatrix' a] -> ShowS
    CallMatrix' a -> String
    (ArgumentIndex -> CallMatrix' a -> ShowS)
    -> (CallMatrix' a -> String)
    -> ([CallMatrix' a] -> ShowS)
    -> Show (CallMatrix' a)
    forall a.
    (HasZero a, Show a) =>
    ArgumentIndex -> CallMatrix' a -> ShowS
    forall a. (HasZero a, Show a) => [CallMatrix' a] -> ShowS
    forall a. (HasZero a, Show a) => CallMatrix' a -> String
    forall a.
    (ArgumentIndex -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a.
    (HasZero a, Show a) =>
    ArgumentIndex -> CallMatrix' a -> ShowS
    showsPrec :: ArgumentIndex -> CallMatrix' a -> ShowS
    $cshow :: forall a. (HasZero a, Show a) => CallMatrix' a -> String
    show :: CallMatrix' a -> String
    $cshowList :: forall a. (HasZero a, Show a) => [CallMatrix' a] -> ShowS
    showList :: [CallMatrix' a] -> ShowS
    Show, (forall a b. (a -> b) -> CallMatrix' a -> CallMatrix' b)
    -> (forall a b. a -> CallMatrix' b -> CallMatrix' a)
    -> Functor CallMatrix'
    forall a b. a -> CallMatrix' b -> CallMatrix' a
    forall a b. (a -> b) -> CallMatrix' a -> CallMatrix' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> CallMatrix' a -> CallMatrix' b
    fmap :: forall a b. (a -> b) -> CallMatrix' a -> CallMatrix' b
    $c<$ :: forall a b. a -> CallMatrix' b -> CallMatrix' a
    <$ :: forall a b. a -> CallMatrix' b -> CallMatrix' a
    Functor, (forall m. Monoid m => CallMatrix' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b)
    -> (forall a. (a -> a -> a) -> CallMatrix' a -> a)
    -> (forall a. (a -> a -> a) -> CallMatrix' a -> a)
    -> (forall a. CallMatrix' a -> [a])
    -> (forall a. CallMatrix' a -> Bool)
    -> (forall a. CallMatrix' a -> ArgumentIndex)
    -> (forall a. Eq a => a -> CallMatrix' a -> Bool)
    -> (forall a. Ord a => CallMatrix' a -> a)
    -> (forall a. Ord a => CallMatrix' a -> a)
    -> (forall a. Num a => CallMatrix' a -> a)
    -> (forall a. Num a => CallMatrix' a -> a)
    -> Foldable CallMatrix'
    forall a. Eq a => a -> CallMatrix' a -> Bool
    forall a. Num a => CallMatrix' a -> a
    forall a. Ord a => CallMatrix' a -> a
    forall m. Monoid m => CallMatrix' m -> m
    forall a. CallMatrix' a -> Bool
    forall a. CallMatrix' a -> ArgumentIndex
    forall a. CallMatrix' a -> [a]
    forall a. (a -> a -> a) -> CallMatrix' a -> a
    forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
    forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
    forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> ArgumentIndex)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => CallMatrix' m -> m
    fold :: forall m. Monoid m => CallMatrix' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
    foldr1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
    foldl1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
    $ctoList :: forall a. CallMatrix' a -> [a]
    toList :: forall a. CallMatrix' a -> [a]
    $cnull :: forall a. CallMatrix' a -> Bool
    null :: forall a. CallMatrix' a -> Bool
    $clength :: forall a. CallMatrix' a -> ArgumentIndex
    length :: forall a. CallMatrix' a -> ArgumentIndex
    $celem :: forall a. Eq a => a -> CallMatrix' a -> Bool
    elem :: forall a. Eq a => a -> CallMatrix' a -> Bool
    $cmaximum :: forall a. Ord a => CallMatrix' a -> a
    maximum :: forall a. Ord a => CallMatrix' a -> a
    $cminimum :: forall a. Ord a => CallMatrix' a -> a
    minimum :: forall a. Ord a => CallMatrix' a -> a
    $csum :: forall a. Num a => CallMatrix' a -> a
    sum :: forall a. Num a => CallMatrix' a -> a
    $cproduct :: forall a. Num a => CallMatrix' a -> a
    product :: forall a. Num a => CallMatrix' a -> a
    Foldable, Functor CallMatrix'
    Foldable CallMatrix'
    (Functor CallMatrix', Foldable CallMatrix') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> CallMatrix' a -> f (CallMatrix' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        CallMatrix' (f a) -> f (CallMatrix' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> CallMatrix' a -> m (CallMatrix' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        CallMatrix' (m a) -> m (CallMatrix' a))
    -> Traversable CallMatrix'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    CallMatrix' (m a) -> m (CallMatrix' a)
    forall (f :: * -> *) a.
    Applicative f =>
    CallMatrix' (f a) -> f (CallMatrix' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CallMatrix' a -> m (CallMatrix' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    CallMatrix' (f a) -> f (CallMatrix' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    CallMatrix' (f a) -> f (CallMatrix' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CallMatrix' a -> m (CallMatrix' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CallMatrix' a -> m (CallMatrix' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    CallMatrix' (m a) -> m (CallMatrix' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    CallMatrix' (m a) -> m (CallMatrix' a)
    Traversable, Comparable (CallMatrix' a)
    Comparable (CallMatrix' a) -> PartialOrd (CallMatrix' a)
    forall a. PartialOrd a => Comparable (CallMatrix' a)
    forall a. Comparable a -> PartialOrd a
    $ccomparable :: forall a. PartialOrd a => Comparable (CallMatrix' a)
    comparable :: Comparable (CallMatrix' a)
    PartialOrd)

    type CallMatrix = CallMatrix' Order

    deriving instance NotWorse CallMatrix

    instance HasZero a => Diagonal (CallMatrix' a) a where
      diagonal :: CallMatrix' a -> [a]
    diagonal = Matrix ArgumentIndex a -> [a]
    forall m e. Diagonal m e => m -> [e]
    diagonal (Matrix ArgumentIndex a -> [a])
    -> (CallMatrix' a -> Matrix ArgumentIndex a)
    -> CallMatrix' a
    -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallMatrix' a -> Matrix ArgumentIndex a
    forall a. CallMatrix' a -> Matrix ArgumentIndex a
    mat

    -- | Call matrix multiplication and call combination.

    class CallComb a where
      (>*<) :: (?cutoff :: CutOff) => a -> a -> a

    -- | Call matrix multiplication.
    --
    --   @f --(m1)--> g --(m2)--> h@  is combined to @f --(m2 `mul` m1)--> h@
    --
    --   Note the reversed order of multiplication:
    --   The matrix @c1@ of the second call @g-->h@ in the sequence
    --   @f-->g-->h@ is multiplied with the matrix @c2@ of the first call.
    --
    --   Preconditions:
    --   @m1@ has dimensions @ar(g) × ar(f)@.
    --   @m2@ has dimensions @ar(h) × ar(g)@.
    --
    --   Postcondition:
    --   @m1 >*< m2@ has dimensions @ar(h) × ar(f)@.

    instance CallComb CallMatrix where
      CallMatrix Matrix ArgumentIndex Order
    m1 >*< :: (?cutoff::CutOff) => CallMatrix -> CallMatrix -> CallMatrix
    >*< CallMatrix Matrix ArgumentIndex Order
    m2 = Matrix ArgumentIndex Order -> CallMatrix
    forall a. Matrix ArgumentIndex a -> CallMatrix' a
    CallMatrix (Matrix ArgumentIndex Order -> CallMatrix)
    -> Matrix ArgumentIndex Order -> CallMatrix
    forall a b. (a -> b) -> a -> b
    $ Semiring Order
    -> Matrix ArgumentIndex Order
    -> Matrix ArgumentIndex Order
    -> Matrix ArgumentIndex Order
    forall i a.
    (Ix i, Eq a) =>
    Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
    mul Semiring Order
    (?cutoff::CutOff) => Semiring Order
    orderSemiring Matrix ArgumentIndex Order
    m2 Matrix ArgumentIndex Order
    m1

    {- UNUSED, BUT DON'T REMOVE!
    -- | Call matrix addition = minimum = pick worst information.
    addCallMatrices :: (?cutoff :: CutOff) => CallMatrix -> CallMatrix -> CallMatrix
    addCallMatrices cm1 cm2 = CallMatrix $
      add (Semiring.add orderSemiring) (mat cm1) (mat cm2)
    -}

    ------------------------------------------------------------------------
    -- * Call matrix augmented with path information.
    ------------------------------------------------------------------------

    -- | Call matrix augmented with path information.

    data CallMatrixAug cinfo = CallMatrixAug
      { forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix :: CallMatrix -- ^ The matrix of the (composed call).
      , forall cinfo. CallMatrixAug cinfo -> cinfo
    augCallInfo   :: cinfo      -- ^ Meta info, like call path.
      }
      deriving (CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    (CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool)
    -> (CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool)
    -> Eq (CallMatrixAug cinfo)
    forall cinfo.
    Eq cinfo =>
    CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall cinfo.
    Eq cinfo =>
    CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    == :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    $c/= :: forall cinfo.
    Eq cinfo =>
    CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    /= :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    Eq, ArgumentIndex -> CallMatrixAug cinfo -> ShowS
    [CallMatrixAug cinfo] -> ShowS
    CallMatrixAug cinfo -> String
    (ArgumentIndex -> CallMatrixAug cinfo -> ShowS)
    -> (CallMatrixAug cinfo -> String)
    -> ([CallMatrixAug cinfo] -> ShowS)
    -> Show (CallMatrixAug cinfo)
    forall cinfo.
    Show cinfo =>
    ArgumentIndex -> CallMatrixAug cinfo -> ShowS
    forall cinfo. Show cinfo => [CallMatrixAug cinfo] -> ShowS
    forall cinfo. Show cinfo => CallMatrixAug cinfo -> String
    forall a.
    (ArgumentIndex -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall cinfo.
    Show cinfo =>
    ArgumentIndex -> CallMatrixAug cinfo -> ShowS
    showsPrec :: ArgumentIndex -> CallMatrixAug cinfo -> ShowS
    $cshow :: forall cinfo. Show cinfo => CallMatrixAug cinfo -> String
    show :: CallMatrixAug cinfo -> String
    $cshowList :: forall cinfo. Show cinfo => [CallMatrixAug cinfo] -> ShowS
    showList :: [CallMatrixAug cinfo] -> ShowS
    Show)

    instance Diagonal (CallMatrixAug cinfo) Order where
      diagonal :: CallMatrixAug cinfo -> [Order]
    diagonal = CallMatrix -> [Order]
    forall m e. Diagonal m e => m -> [e]
    diagonal (CallMatrix -> [Order])
    -> (CallMatrixAug cinfo -> CallMatrix)
    -> CallMatrixAug cinfo
    -> [Order]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallMatrixAug cinfo -> CallMatrix
    forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix

    instance PartialOrd (CallMatrixAug cinfo) where
      comparable :: Comparable (CallMatrixAug cinfo)
    comparable CallMatrixAug cinfo
    m CallMatrixAug cinfo
    m' = Comparable CallMatrix
    forall a. PartialOrd a => Comparable a
    comparable (CallMatrixAug cinfo -> CallMatrix
    forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix CallMatrixAug cinfo
    m) (CallMatrixAug cinfo -> CallMatrix
    forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix CallMatrixAug cinfo
    m')

    instance NotWorse (CallMatrixAug cinfo) where
      CallMatrixAug cinfo
    c1 notWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
    `notWorse` CallMatrixAug cinfo
    c2 = CallMatrixAug cinfo -> CallMatrix
    forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix CallMatrixAug cinfo
    c1 CallMatrix -> CallMatrix -> Bool
    forall a. NotWorse a => a -> a -> Bool
    `notWorse` CallMatrixAug cinfo -> CallMatrix
    forall cinfo. CallMatrixAug cinfo -> CallMatrix
    augCallMatrix CallMatrixAug cinfo
    c2

    -- | Augmented call matrix multiplication.

    instance Monoid cinfo => CallComb (CallMatrixAug cinfo) where
      CallMatrixAug CallMatrix
    m1 cinfo
    p1 >*< :: (?cutoff::CutOff) =>
    CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo
    >*< CallMatrixAug CallMatrix
    m2 cinfo
    p2 =
        CallMatrix -> cinfo -> CallMatrixAug cinfo
    forall cinfo. CallMatrix -> cinfo -> CallMatrixAug cinfo
    CallMatrixAug (CallMatrix
    m1 CallMatrix -> CallMatrix -> CallMatrix
    forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
    >*< CallMatrix
    m2) (cinfo -> cinfo -> cinfo
    forall a. Monoid a => a -> a -> a
    mappend cinfo
    p1 cinfo
    p2)

    -- | Non-augmented call matrix.

    noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo
    noAug :: forall cinfo. Monoid cinfo => CallMatrix -> CallMatrixAug cinfo
    noAug CallMatrix
    m = CallMatrix -> cinfo -> CallMatrixAug cinfo
    forall cinfo. CallMatrix -> cinfo -> CallMatrixAug cinfo
    CallMatrixAug CallMatrix
    m cinfo
    forall a. Monoid a => a
    mempty

    ------------------------------------------------------------------------
    -- * Sets of incomparable call matrices augmented with path information.
    ------------------------------------------------------------------------

    -- | Sets of incomparable call matrices augmented with path information.
    --   Use overloaded 'null', 'empty', 'singleton', 'mappend'.
    newtype CMSet cinfo = CMSet { forall cinfo. CMSet cinfo -> Favorites (CallMatrixAug cinfo)
    cmSet :: Favorites (CallMatrixAug cinfo) }
      deriving ( ArgumentIndex -> CMSet cinfo -> ShowS
    [CMSet cinfo] -> ShowS
    CMSet cinfo -> String
    (ArgumentIndex -> CMSet cinfo -> ShowS)
    -> (CMSet cinfo -> String)
    -> ([CMSet cinfo] -> ShowS)
    -> Show (CMSet cinfo)
    forall cinfo. Show cinfo => ArgumentIndex -> CMSet cinfo -> ShowS
    forall cinfo. Show cinfo => [CMSet cinfo] -> ShowS
    forall cinfo. Show cinfo => CMSet cinfo -> String
    forall a.
    (ArgumentIndex -> a -> ShowS)
    -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall cinfo. Show cinfo => ArgumentIndex -> CMSet cinfo -> ShowS
    showsPrec :: ArgumentIndex -> CMSet cinfo -> ShowS
    $cshow :: forall cinfo. Show cinfo => CMSet cinfo -> String
    show :: CMSet cinfo -> String
    $cshowList :: forall cinfo. Show cinfo => [CMSet cinfo] -> ShowS
    showList :: [CMSet cinfo] -> ShowS
    Show, NonEmpty (CMSet cinfo) -> CMSet cinfo
    CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
    -> (NonEmpty (CMSet cinfo) -> CMSet cinfo)
    -> (forall b. Integral b => b -> CMSet cinfo -> CMSet cinfo)
    -> Semigroup (CMSet cinfo)
    forall b. Integral b => b -> CMSet cinfo -> CMSet cinfo
    forall cinfo. NonEmpty (CMSet cinfo) -> CMSet cinfo
    forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    forall a.
    (a -> a -> a)
    -> (NonEmpty a -> a)
    -> (forall b. Integral b => b -> a -> a)
    -> Semigroup a
    forall cinfo b. Integral b => b -> CMSet cinfo -> CMSet cinfo
    $c<> :: forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    <> :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    $csconcat :: forall cinfo. NonEmpty (CMSet cinfo) -> CMSet cinfo
    sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo
    $cstimes :: forall cinfo b. Integral b => b -> CMSet cinfo -> CMSet cinfo
    stimes :: forall b. Integral b => b -> CMSet cinfo -> CMSet cinfo
    Semigroup, Semigroup (CMSet cinfo)
    CMSet cinfo
    Semigroup (CMSet cinfo) =>
    CMSet cinfo
    -> (CMSet cinfo -> CMSet cinfo -> CMSet cinfo)
    -> ([CMSet cinfo] -> CMSet cinfo)
    -> Monoid (CMSet cinfo)
    [CMSet cinfo] -> CMSet cinfo
    CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    forall cinfo. Semigroup (CMSet cinfo)
    forall cinfo. CMSet cinfo
    forall a.
    Semigroup a =>
    a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    forall cinfo. [CMSet cinfo] -> CMSet cinfo
    forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    $cmempty :: forall cinfo. CMSet cinfo
    mempty :: CMSet cinfo
    $cmappend :: forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    mappend :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    $cmconcat :: forall cinfo. [CMSet cinfo] -> CMSet cinfo
    mconcat :: [CMSet cinfo] -> CMSet cinfo
    Monoid, CMSet cinfo
    CMSet cinfo -> Bool
    CMSet cinfo -> (CMSet cinfo -> Bool) -> Null (CMSet cinfo)
    forall cinfo. CMSet cinfo
    forall a. a -> (a -> Bool) -> Null a
    forall cinfo. CMSet cinfo -> Bool
    $cempty :: forall cinfo. CMSet cinfo
    empty :: CMSet cinfo
    $cnull :: forall cinfo. CMSet cinfo -> Bool
    null :: CMSet cinfo -> Bool
    Null, Singleton (CallMatrixAug cinfo) )

    -- | Call matrix set product is the Cartesian product.

    instance Monoid cinfo => CallComb (CMSet cinfo) where
      CMSet Favorites (CallMatrixAug cinfo)
    as >*< :: (?cutoff::CutOff) => CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    >*< CMSet Favorites (CallMatrixAug cinfo)
    bs = Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    forall cinfo. Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    CMSet (Favorites (CallMatrixAug cinfo) -> CMSet cinfo)
    -> Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    forall a b. (a -> b) -> a -> b
    $ [CallMatrixAug cinfo] -> Favorites (CallMatrixAug cinfo)
    forall a. PartialOrd a => [a] -> Favorites a
    Fav.fromList ([CallMatrixAug cinfo] -> Favorites (CallMatrixAug cinfo))
    -> [CallMatrixAug cinfo] -> Favorites (CallMatrixAug cinfo)
    forall a b. (a -> b) -> a -> b
    $
        [ CallMatrixAug cinfo
    a CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo
    forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
    >*< CallMatrixAug cinfo
    b | CallMatrixAug cinfo
    a <- Favorites (CallMatrixAug cinfo) -> [CallMatrixAug cinfo]
    forall a. Favorites a -> [a]
    Fav.toList Favorites (CallMatrixAug cinfo)
    as, CallMatrixAug cinfo
    b <- Favorites (CallMatrixAug cinfo) -> [CallMatrixAug cinfo]
    forall a. Favorites a -> [a]
    Fav.toList Favorites (CallMatrixAug cinfo)
    bs ]

    -- | Insert into a call matrix set.

    insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
    insert :: forall cinfo. CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
    insert CallMatrixAug cinfo
    a (CMSet Favorites (CallMatrixAug cinfo)
    as) = Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    forall cinfo. Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    CMSet (Favorites (CallMatrixAug cinfo) -> CMSet cinfo)
    -> Favorites (CallMatrixAug cinfo) -> CMSet cinfo
    forall a b. (a -> b) -> a -> b
    $ CallMatrixAug cinfo
    -> Favorites (CallMatrixAug cinfo)
    -> Favorites (CallMatrixAug cinfo)
    forall a. PartialOrd a => a -> Favorites a -> Favorites a
    Fav.insert CallMatrixAug cinfo
    a Favorites (CallMatrixAug cinfo)
    as

    -- | Union two call matrix sets.

    union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    union :: forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    union = CMSet cinfo -> CMSet cinfo -> CMSet cinfo
    forall a. Monoid a => a -> a -> a
    mappend
    -- union (CMSet as) (CMSet bs) = CMSet $ Fav.union as bs

    -- | Convert into a list of augmented call matrices.

    toList :: CMSet cinfo -> [CallMatrixAug cinfo]
    toList :: forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
    toList (CMSet Favorites (CallMatrixAug cinfo)
    as) = Favorites (CallMatrixAug cinfo) -> [CallMatrixAug cinfo]
    forall a. Favorites a -> [a]
    Fav.toList Favorites (CallMatrixAug cinfo)
    as

    ------------------------------------------------------------------------
    -- * Printing
    ------------------------------------------------------------------------

    instance Pretty CallMatrix where
      pretty :: CallMatrix -> Doc
    pretty (CallMatrix Matrix ArgumentIndex Order
    m) = Matrix ArgumentIndex Order -> Doc
    forall a. Pretty a => a -> Doc
    pretty Matrix ArgumentIndex Order
    m

    instance Pretty cinfo => Pretty (CallMatrixAug cinfo) where
      pretty :: CallMatrixAug cinfo -> Doc
    pretty (CallMatrixAug CallMatrix
    m cinfo
    cinfo) = cinfo -> Doc
    forall a. Pretty a => a -> Doc
    pretty cinfo
    cinfo Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$ CallMatrix -> Doc
    forall a. Pretty a => a -> Doc
    pretty CallMatrix
    m

    instance Pretty cinfo => Pretty (CMSet cinfo) where
      pretty :: CMSet cinfo -> Doc
    pretty = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> (CMSet cinfo -> [Doc]) -> CMSet cinfo -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    newLine ([Doc] -> [Doc]) -> (CMSet cinfo -> [Doc]) -> CMSet cinfo -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CallMatrixAug cinfo -> Doc) -> [CallMatrixAug cinfo] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map CallMatrixAug cinfo -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([CallMatrixAug cinfo] -> [Doc])
    -> (CMSet cinfo -> [CallMatrixAug cinfo]) -> CMSet cinfo -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CMSet cinfo -> [CallMatrixAug cinfo]
    forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
    toList
        where newLine :: Doc
    newLine = Doc
    "\n"