{-# 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 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
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"