{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams             #-}
{-# LANGUAGE CPP                        #-}

module Agda.Termination.CallMatrix where

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

#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)

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.Utils.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 { 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
/= :: CallMatrix' a -> CallMatrix' a -> Bool
$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
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
min :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a
$cmin :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> CallMatrix' a
max :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a
$cmax :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> CallMatrix' a
>= :: 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
$c< :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Bool
compare :: CallMatrix' a -> CallMatrix' a -> Ordering
$ccompare :: forall a. Ord a => CallMatrix' a -> CallMatrix' a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (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
showList :: [CallMatrix' a] -> ShowS
$cshowList :: forall a. (HasZero a, Show a) => [CallMatrix' a] -> ShowS
show :: CallMatrix' a -> String
$cshow :: forall a. (HasZero a, Show a) => CallMatrix' a -> String
showsPrec :: ArgumentIndex -> CallMatrix' a -> ShowS
$cshowsPrec :: forall a.
(HasZero a, Show a) =>
ArgumentIndex -> CallMatrix' a -> ShowS
Show, a -> CallMatrix' b -> CallMatrix' a
(a -> b) -> CallMatrix' a -> CallMatrix' b
(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
<$ :: a -> CallMatrix' b -> CallMatrix' a
$c<$ :: forall a b. a -> CallMatrix' b -> CallMatrix' a
fmap :: (a -> b) -> CallMatrix' a -> CallMatrix' b
$cfmap :: forall a b. (a -> b) -> CallMatrix' a -> CallMatrix' b
Functor, a -> CallMatrix' a -> Bool
CallMatrix' m -> m
CallMatrix' a -> [a]
CallMatrix' a -> Bool
CallMatrix' a -> ArgumentIndex
CallMatrix' a -> a
CallMatrix' a -> a
CallMatrix' a -> a
CallMatrix' a -> a
(a -> m) -> CallMatrix' a -> m
(a -> m) -> CallMatrix' a -> m
(a -> b -> b) -> b -> CallMatrix' a -> b
(a -> b -> b) -> b -> CallMatrix' a -> b
(b -> a -> b) -> b -> CallMatrix' a -> b
(b -> a -> b) -> b -> CallMatrix' a -> b
(a -> a -> a) -> CallMatrix' a -> a
(a -> a -> a) -> CallMatrix' a -> a
(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
product :: CallMatrix' a -> a
$cproduct :: forall a. Num a => CallMatrix' a -> a
sum :: CallMatrix' a -> a
$csum :: forall a. Num a => CallMatrix' a -> a
minimum :: CallMatrix' a -> a
$cminimum :: forall a. Ord a => CallMatrix' a -> a
maximum :: CallMatrix' a -> a
$cmaximum :: forall a. Ord a => CallMatrix' a -> a
elem :: a -> CallMatrix' a -> Bool
$celem :: forall a. Eq a => a -> CallMatrix' a -> Bool
length :: CallMatrix' a -> ArgumentIndex
$clength :: forall a. CallMatrix' a -> ArgumentIndex
null :: CallMatrix' a -> Bool
$cnull :: forall a. CallMatrix' a -> Bool
toList :: CallMatrix' a -> [a]
$ctoList :: forall a. CallMatrix' a -> [a]
foldl1 :: (a -> a -> a) -> CallMatrix' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
foldr1 :: (a -> a -> a) -> CallMatrix' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> CallMatrix' a -> a
foldl' :: (b -> a -> b) -> b -> CallMatrix' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
foldl :: (b -> a -> b) -> b -> CallMatrix' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> CallMatrix' a -> b
foldr' :: (a -> b -> b) -> b -> CallMatrix' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
foldr :: (a -> b -> b) -> b -> CallMatrix' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> CallMatrix' a -> b
foldMap' :: (a -> m) -> CallMatrix' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
foldMap :: (a -> m) -> CallMatrix' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> CallMatrix' a -> m
fold :: CallMatrix' m -> m
$cfold :: forall m. Monoid m => CallMatrix' m -> m
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'
(a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
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)
sequence :: CallMatrix' (m a) -> m (CallMatrix' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
CallMatrix' (m a) -> m (CallMatrix' a)
mapM :: (a -> m b) -> CallMatrix' a -> m (CallMatrix' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> CallMatrix' a -> m (CallMatrix' b)
sequenceA :: CallMatrix' (f a) -> f (CallMatrix' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
CallMatrix' (f a) -> f (CallMatrix' a)
traverse :: (a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CallMatrix' a -> f (CallMatrix' b)
$cp2Traversable :: Foldable CallMatrix'
$cp1Traversable :: Functor CallMatrix'
Traversable, Comparable (CallMatrix' a)
Comparable (CallMatrix' a) -> PartialOrd (CallMatrix' a)
forall a. PartialOrd a => Comparable (CallMatrix' a)
forall a. Comparable a -> PartialOrd a
comparable :: Comparable (CallMatrix' a)
$ccomparable :: forall a. PartialOrd a => 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 >*< :: 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
  { CallMatrixAug cinfo -> CallMatrix
augCallMatrix :: CallMatrix -- ^ The matrix of the (composed call).
  , 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
/= :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool
$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
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
showList :: [CallMatrixAug cinfo] -> ShowS
$cshowList :: forall cinfo. Show cinfo => [CallMatrixAug cinfo] -> ShowS
show :: CallMatrixAug cinfo -> String
$cshow :: forall cinfo. Show cinfo => CallMatrixAug cinfo -> String
showsPrec :: ArgumentIndex -> CallMatrixAug cinfo -> ShowS
$cshowsPrec :: forall cinfo.
Show cinfo =>
ArgumentIndex -> 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 >*< :: 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 :: 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 { 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
showList :: [CMSet cinfo] -> ShowS
$cshowList :: forall cinfo. Show cinfo => [CMSet cinfo] -> ShowS
show :: CMSet cinfo -> String
$cshow :: forall cinfo. Show cinfo => CMSet cinfo -> String
showsPrec :: ArgumentIndex -> CMSet cinfo -> ShowS
$cshowsPrec :: forall cinfo. Show cinfo => ArgumentIndex -> CMSet cinfo -> ShowS
Show, b -> CMSet cinfo -> CMSet cinfo
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
stimes :: b -> CMSet cinfo -> CMSet cinfo
$cstimes :: forall cinfo b. Integral b => b -> CMSet cinfo -> CMSet cinfo
sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo
$csconcat :: forall cinfo. NonEmpty (CMSet cinfo) -> CMSet cinfo
<> :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
$c<> :: forall cinfo. CMSet cinfo -> 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
mconcat :: [CMSet cinfo] -> CMSet cinfo
$cmconcat :: forall cinfo. [CMSet cinfo] -> CMSet cinfo
mappend :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
$cmappend :: forall cinfo. CMSet cinfo -> CMSet cinfo -> CMSet cinfo
mempty :: CMSet cinfo
$cmempty :: forall cinfo. CMSet cinfo
$cp1Monoid :: forall cinfo. Semigroup (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
null :: CMSet cinfo -> Bool
$cnull :: forall cinfo. CMSet cinfo -> Bool
empty :: CMSet cinfo
$cempty :: forall cinfo. CMSet cinfo
Null, Singleton (CallMatrixAug cinfo) )

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

instance Monoid cinfo => CallComb (CMSet cinfo) where
  CMSet Favorites (CallMatrixAug cinfo)
as >*< :: 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 :: 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 :: 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 :: 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
$$ 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
vcat ([Doc] -> Doc) -> (CMSet cinfo -> [Doc]) -> CMSet cinfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [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"