content: {-# 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 { mat :: Matrix ArgumentIndex a }
    deriving (Eq, Ord, Show, Functor, Foldable, Traversable, PartialOrd)
  
  type CallMatrix = CallMatrix' Order
  
  deriving instance NotWorse CallMatrix
  
  instance HasZero a => Diagonal (CallMatrix' a) a where
    diagonal = diagonal . 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 m1 >*< CallMatrix m2 = CallMatrix $ mul orderSemiring m2 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
    { augCallMatrix :: CallMatrix -- ^ The matrix of the (composed call).
    , augCallInfo   :: cinfo      -- ^ Meta info, like call path.
    }
    deriving (Eq, Show)
  
  instance Diagonal (CallMatrixAug cinfo) Order where
    diagonal = diagonal . augCallMatrix
  
  instance PartialOrd (CallMatrixAug cinfo) where
    comparable m m' = comparable (augCallMatrix m) (augCallMatrix m')
  
  instance NotWorse (CallMatrixAug cinfo) where
    c1 `notWorse` c2 = augCallMatrix c1 `notWorse` augCallMatrix c2
  
  -- | Augmented call matrix multiplication.
  
  instance Monoid cinfo => CallComb (CallMatrixAug cinfo) where
    CallMatrixAug m1 p1 >*< CallMatrixAug m2 p2 =
      CallMatrixAug (m1 >*< m2) (mappend p1 p2)
  
  -- | Non-augmented call matrix.
  
  noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo
  noAug m = CallMatrixAug m 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 :: Favorites (CallMatrixAug cinfo) }
    deriving ( Show, Semigroup, Monoid, Null, Singleton (CallMatrixAug cinfo) )
  
  -- | Call matrix set product is the Cartesian product.
  
  instance Monoid cinfo => CallComb (CMSet cinfo) where
    CMSet as >*< CMSet bs = CMSet $ Fav.fromList $
      [ a >*< b | a <- Fav.toList as, b <- Fav.toList bs ]
  
  -- | Insert into a call matrix set.
  
  insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
  insert a (CMSet as) = CMSet $ Fav.insert a as
  
  -- | Union two call matrix sets.
  
  union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
  union = 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 as) = Fav.toList as
  
  ------------------------------------------------------------------------
  -- * Printing
  ------------------------------------------------------------------------
  
  instance Pretty CallMatrix where
    pretty (CallMatrix m) = pretty m
  
  instance Pretty cinfo => Pretty (CallMatrixAug cinfo) where
    pretty (CallMatrixAug m cinfo) = pretty cinfo $$ pretty m
  
  instance Pretty cinfo => Pretty (CMSet cinfo) where
    pretty = vcat . punctuate newLine . map pretty . toList
      where newLine = "\n"
  