    {-# LANGUAGE ImplicitParams #-}

    -- | Termination checker, based on
    --     \"A Predicative Analysis of Structural Recursion\" by
    --     Andreas Abel and Thorsten Altenkirch (JFP'01),
    --   and
    --     \"The Size-Change Principle for Program Termination\" by
    --     Chin Soon Lee, Neil Jones, and Amir Ben-Amram (POPL'01).

    module Agda.Termination.Termination
      ( terminates
      , terminatesFilter
      , endos
      , idempotent
      ) where

    import Agda.Termination.CutOff
    import Agda.Termination.CallGraph
    import Agda.Termination.CallMatrix hiding (toList)
    import qualified Agda.Termination.CallMatrix as CMSet
    import Agda.Termination.Order
    import Agda.Termination.SparseMatrix

    import Agda.Utils.Either
    import Agda.Utils.List
    import Agda.Utils.Maybe

    import Data.Monoid

    -- | TODO: This comment seems to be partly out of date.
    --
    -- @'terminates' cs@ checks if the functions represented by @cs@
    -- terminate. The call graph @cs@ should have one entry ('Call') per
    -- recursive function application.
    --
    -- @'Right' perms@ is returned if the functions are size-change terminating.
    --
    -- If termination can not be established, then @'Left' problems@ is
    -- returned instead. Here @problems@ contains an
    -- indication of why termination cannot be established. See 'lexOrder'
    -- for further details.
    --
    -- Note that this function assumes that all data types are strictly
    -- positive.
    --
    -- The termination criterion is taken from Jones et al.
    -- In the completed call graph, each idempotent call-matrix
    -- from a function to itself must have a decreasing argument.
    -- Idempotency is wrt. matrix multiplication.
    --
    -- This criterion is strictly more liberal than searching for a
    -- lexicographic order (and easier to implement, but harder to justify).

    terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Either cinfo ()
    terminates cs = checkIdems $ endos $ toList $ complete cs

    terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) =>
      (Node -> Bool) -> CallGraph cinfo -> Either cinfo ()
    terminatesFilter f cs = checkIdems $ endos $ filter f' $ toList $ complete cs
      where f' c = f (source c) && f (target c)

    endos :: [Call cinfo] -> [CallMatrixAug cinfo]
    endos cs = [ m | c <- cs, source c == target c
                   , m <- CMSet.toList $ callMatrixSet c
               ]

    checkIdems :: (?cutoff :: CutOff) => [CallMatrixAug cinfo] -> Either cinfo ()
    checkIdems calls = caseMaybe (headMaybe offending) (Right ()) $ Left . augCallInfo
      where
        -- Every idempotent call must have decrease, otherwise it offends us.
        offending = filter (not . hasDecrease) $ filter idempotent calls

    checkIdem :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool
    checkIdem c = if idempotent c then hasDecrease c else True

    -- | A call @c@ is idempotent if it is an endo (@'source' == 'target'@)
    --   of order 1.
    --   (Endo-calls of higher orders are e.g. argument permutations).
    --   We can test idempotency by self-composition.
    --   Self-composition @c >*< c@ should not make any parameter-argument relation
    --   worse.
    idempotent  :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool
    idempotent (CallMatrixAug m _) = (m >*< m) `notWorse` m

    hasDecrease :: CallMatrixAug cinfo -> Bool
    hasDecrease = any isDecr . diagonal