    {-# 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.Maybe

    -- | 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 :: forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    CallGraph cinfo -> Either cinfo ()
    terminates CallGraph cinfo
    cs = [CallMatrixAug cinfo] -> Either cinfo ()
    forall cinfo.
    (?cutoff::CutOff) =>
    [CallMatrixAug cinfo] -> Either cinfo ()
    checkIdems ([CallMatrixAug cinfo] -> Either cinfo ())
    -> [CallMatrixAug cinfo] -> Either cinfo ()
    forall a b. (a -> b) -> a -> b
    $ [Call cinfo] -> [CallMatrixAug cinfo]
    forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
    endos ([Call cinfo] -> [CallMatrixAug cinfo])
    -> [Call cinfo] -> [CallMatrixAug cinfo]
    forall a b. (a -> b) -> a -> b
    $ CallGraph cinfo -> [Call cinfo]
    forall cinfo. CallGraph cinfo -> [Call cinfo]
    toList (CallGraph cinfo -> [Call cinfo])
    -> CallGraph cinfo -> [Call cinfo]
    forall a b. (a -> b) -> a -> b
    $ CallGraph cinfo -> CallGraph cinfo
    forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo -> CallGraph cinfo
    complete CallGraph cinfo
    cs

    terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) =>
      (Node -> Bool) -> CallGraph cinfo -> Either cinfo ()
    terminatesFilter :: forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    (Node -> Bool) -> CallGraph cinfo -> Either cinfo ()
    terminatesFilter Node -> Bool
    f CallGraph cinfo
    cs = [CallMatrixAug cinfo] -> Either cinfo ()
    forall cinfo.
    (?cutoff::CutOff) =>
    [CallMatrixAug cinfo] -> Either cinfo ()
    checkIdems ([CallMatrixAug cinfo] -> Either cinfo ())
    -> [CallMatrixAug cinfo] -> Either cinfo ()
    forall a b. (a -> b) -> a -> b
    $ [Call cinfo] -> [CallMatrixAug cinfo]
    forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
    endos ([Call cinfo] -> [CallMatrixAug cinfo])
    -> [Call cinfo] -> [CallMatrixAug cinfo]
    forall a b. (a -> b) -> a -> b
    $ (Call cinfo -> Bool) -> [Call cinfo] -> [Call cinfo]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Call cinfo -> Bool
    f' ([Call cinfo] -> [Call cinfo]) -> [Call cinfo] -> [Call cinfo]
    forall a b. (a -> b) -> a -> b
    $ CallGraph cinfo -> [Call cinfo]
    forall cinfo. CallGraph cinfo -> [Call cinfo]
    toList (CallGraph cinfo -> [Call cinfo])
    -> CallGraph cinfo -> [Call cinfo]
    forall a b. (a -> b) -> a -> b
    $ CallGraph cinfo -> CallGraph cinfo
    forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo -> CallGraph cinfo
    complete CallGraph cinfo
    cs
      where f' :: Call cinfo -> Bool
    f' Call cinfo
    c = Node -> Bool
    f (Call cinfo -> Node
    forall n e. Edge n e -> n
    source Call cinfo
    c) Bool -> Bool -> Bool
    && Node -> Bool
    f (Call cinfo -> Node
    forall n e. Edge n e -> n
    target Call cinfo
    c)

    endos :: [Call cinfo] -> [CallMatrixAug cinfo]
    endos :: forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
    endos [Call cinfo]
    cs = [ CallMatrixAug cinfo
    m | Call cinfo
    c <- [Call cinfo]
    cs, Call cinfo -> Node
    forall n e. Edge n e -> n
    source Call cinfo
    c Node -> Node -> Bool
    forall a. Eq a => a -> a -> Bool
    == Call cinfo -> Node
    forall n e. Edge n e -> n
    target Call cinfo
    c
                   , CallMatrixAug cinfo
    m <- CMSet cinfo -> [CallMatrixAug cinfo]
    forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
    CMSet.toList (CMSet cinfo -> [CallMatrixAug cinfo])
    -> CMSet cinfo -> [CallMatrixAug cinfo]
    forall a b. (a -> b) -> a -> b
    $ Call cinfo -> CMSet cinfo
    forall cinfo. Call cinfo -> CMSet cinfo
    callMatrixSet Call cinfo
    c
               ]

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

    -- UNUSED Liang-Ting 2019-07-15
    --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 :: forall cinfo. (?cutoff::CutOff) => CallMatrixAug cinfo -> Bool
    idempotent (CallMatrixAug CallMatrix
    m cinfo
    _) = (CallMatrix
    m CallMatrix -> CallMatrix -> CallMatrix
    forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
    >*< CallMatrix
    m) CallMatrix -> CallMatrix -> Bool
    forall a. NotWorse a => a -> a -> Bool
    `notWorse` CallMatrix
    m

    hasDecrease :: CallMatrixAug cinfo -> Bool
    hasDecrease :: forall cinfo. CallMatrixAug cinfo -> Bool
    hasDecrease = (Order -> Bool) -> [Order] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Order -> Bool
    isDecr ([Order] -> Bool)
    -> (CallMatrixAug cinfo -> [Order]) -> CallMatrixAug cinfo -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallMatrixAug cinfo -> [Order]
    forall m e. Diagonal m e => m -> [e]
    diagonal