    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# 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(..)
      , GuardednessHelps(..)
      , terminates
      , terminatesFilter
      , endos
      , idempotent
      ) where

    import Prelude hiding ((&&), null)

    import Control.DeepSeq (NFData)
    import GHC.Generics (Generic)

    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.Boolean
    import Agda.Utils.Null
    import Agda.Utils.Three

    -- | Would termination go through with guardedness?
    data GuardednessHelps
      = GuardednessHelpsYes  -- ^ Guardedness would provide termination evidence.
      | GuardednessHelpsNot  -- ^ Guardedness does not help with termination.
      deriving (GuardednessHelps -> GuardednessHelps -> Bool
    (GuardednessHelps -> GuardednessHelps -> Bool)
    -> (GuardednessHelps -> GuardednessHelps -> Bool)
    -> Eq GuardednessHelps
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: GuardednessHelps -> GuardednessHelps -> Bool
    == :: GuardednessHelps -> GuardednessHelps -> Bool
    $c/= :: GuardednessHelps -> GuardednessHelps -> Bool
    /= :: GuardednessHelps -> GuardednessHelps -> Bool
    Eq, Int -> GuardednessHelps -> ShowS
    [GuardednessHelps] -> ShowS
    GuardednessHelps -> String
    (Int -> GuardednessHelps -> ShowS)
    -> (GuardednessHelps -> String)
    -> ([GuardednessHelps] -> ShowS)
    -> Show GuardednessHelps
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> GuardednessHelps -> ShowS
    showsPrec :: Int -> GuardednessHelps -> ShowS
    $cshow :: GuardednessHelps -> String
    show :: GuardednessHelps -> String
    $cshowList :: [GuardednessHelps] -> ShowS
    showList :: [GuardednessHelps] -> ShowS
    Show, (forall x. GuardednessHelps -> Rep GuardednessHelps x)
    -> (forall x. Rep GuardednessHelps x -> GuardednessHelps)
    -> Generic GuardednessHelps
    forall x. Rep GuardednessHelps x -> GuardednessHelps
    forall x. GuardednessHelps -> Rep GuardednessHelps x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. GuardednessHelps -> Rep GuardednessHelps x
    from :: forall x. GuardednessHelps -> Rep GuardednessHelps x
    $cto :: forall x. Rep GuardednessHelps x -> GuardednessHelps
    to :: forall x. Rep GuardednessHelps x -> GuardednessHelps
    Generic, Int -> GuardednessHelps
    GuardednessHelps -> Int
    GuardednessHelps -> [GuardednessHelps]
    GuardednessHelps -> GuardednessHelps
    GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    GuardednessHelps
    -> GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    (GuardednessHelps -> GuardednessHelps)
    -> (GuardednessHelps -> GuardednessHelps)
    -> (Int -> GuardednessHelps)
    -> (GuardednessHelps -> Int)
    -> (GuardednessHelps -> [GuardednessHelps])
    -> (GuardednessHelps -> GuardednessHelps -> [GuardednessHelps])
    -> (GuardednessHelps -> GuardednessHelps -> [GuardednessHelps])
    -> (GuardednessHelps
        -> GuardednessHelps -> GuardednessHelps -> [GuardednessHelps])
    -> Enum GuardednessHelps
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: GuardednessHelps -> GuardednessHelps
    succ :: GuardednessHelps -> GuardednessHelps
    $cpred :: GuardednessHelps -> GuardednessHelps
    pred :: GuardednessHelps -> GuardednessHelps
    $ctoEnum :: Int -> GuardednessHelps
    toEnum :: Int -> GuardednessHelps
    $cfromEnum :: GuardednessHelps -> Int
    fromEnum :: GuardednessHelps -> Int
    $cenumFrom :: GuardednessHelps -> [GuardednessHelps]
    enumFrom :: GuardednessHelps -> [GuardednessHelps]
    $cenumFromThen :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    enumFromThen :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    $cenumFromTo :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    enumFromTo :: GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    $cenumFromThenTo :: GuardednessHelps
    -> GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    enumFromThenTo :: GuardednessHelps
    -> GuardednessHelps -> GuardednessHelps -> [GuardednessHelps]
    Enum, GuardednessHelps
    GuardednessHelps -> GuardednessHelps -> Bounded GuardednessHelps
    forall a. a -> a -> Bounded a
    $cminBound :: GuardednessHelps
    minBound :: GuardednessHelps
    $cmaxBound :: GuardednessHelps
    maxBound :: GuardednessHelps
    Bounded)

    -- | Result of running the termination checker.
    data Terminates cinfo
      = Terminates
          -- ^ Termination proved without considering guardedness.
      | TerminatesNot GuardednessHelps cinfo
          -- ^ Termination could not be proven,
          --   witnessed by the supplied problematic call path.
          --   Guardedness could help, though.

    -- | @'terminates' cs@ checks if the functions represented by @cs@
    -- terminate. The call graph @cs@ should have one entry ('Call') per
    -- recursive function application.
    --
    -- 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 -> Terminates cinfo
    terminates :: forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    CallGraph cinfo -> Terminates cinfo
    terminates = (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
    forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
    terminatesFilter ((Int -> Bool) -> CallGraph cinfo -> Terminates cinfo)
    -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Bool
    forall a b. a -> b -> a
    const Bool
    True

    terminatesFilter ::
         (Monoid cinfo, ?cutoff :: CutOff)
      => (Node -> Bool)    -- ^ Only consider calls whose source and target satisfy this predicate.
      -> CallGraph cinfo   -- ^ Callgraph augmented with @cinfo@.
      -> Terminates cinfo  -- ^ A bad call path of type @cinfo@, if termination could not be proven.
    terminatesFilter :: forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
    terminatesFilter Int -> Bool
    f CallGraph cinfo
    cs
      | CallMatrixAug cinfo
    cm:[CallMatrixAug cinfo]
    _ <- [CallMatrixAug cinfo]
    bad             = GuardednessHelps -> cinfo -> Terminates cinfo
    forall cinfo. GuardednessHelps -> cinfo -> Terminates cinfo
    TerminatesNot GuardednessHelps
    GuardednessHelpsNot (cinfo -> Terminates cinfo) -> cinfo -> Terminates cinfo
    forall a b. (a -> b) -> a -> b
    $ CallMatrixAug cinfo -> cinfo
    forall cinfo. CallMatrixAug cinfo -> cinfo
    augCallInfo CallMatrixAug cinfo
    cm
      | CallMatrixAug cinfo
    cm:[CallMatrixAug cinfo]
    _ <- [CallMatrixAug cinfo]
    needGuardedness = GuardednessHelps -> cinfo -> Terminates cinfo
    forall cinfo. GuardednessHelps -> cinfo -> Terminates cinfo
    TerminatesNot GuardednessHelps
    GuardednessHelpsYes (cinfo -> Terminates cinfo) -> cinfo -> Terminates cinfo
    forall a b. (a -> b) -> a -> b
    $ CallMatrixAug cinfo -> cinfo
    forall cinfo. CallMatrixAug cinfo -> cinfo
    augCallInfo CallMatrixAug cinfo
    cm
      | Bool
    otherwise               = Terminates cinfo
    forall cinfo. Terminates cinfo
    Terminates
      where
        f' :: Edge Int (CMSet cinfo) -> Bool
    f' = Int -> Bool
    f (Int -> Bool)
    -> (Edge Int (CMSet cinfo) -> Int)
    -> Edge Int (CMSet cinfo)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Edge Int (CMSet cinfo) -> Int
    forall n e. Edge n e -> n
    source (Edge Int (CMSet cinfo) -> Bool)
    -> (Edge Int (CMSet cinfo) -> Bool)
    -> Edge Int (CMSet cinfo)
    -> Bool
    forall a. Boolean a => a -> a -> a
    && Int -> Bool
    f (Int -> Bool)
    -> (Edge Int (CMSet cinfo) -> Int)
    -> Edge Int (CMSet cinfo)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Edge Int (CMSet cinfo) -> Int
    forall n e. Edge n e -> n
    target
        -- Every idempotent call must have decrease in the diagonal.
        idems :: [CallMatrixAug cinfo]
    idems = (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] -> [CallMatrixAug cinfo])
    -> [CallMatrixAug cinfo] -> [CallMatrixAug cinfo]
    forall a b. (a -> b) -> a -> b
    $ [Edge Int (CMSet cinfo)] -> [CallMatrixAug cinfo]
    forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
    endos ([Edge Int (CMSet cinfo)] -> [CallMatrixAug cinfo])
    -> [Edge Int (CMSet cinfo)] -> [CallMatrixAug cinfo]
    forall a b. (a -> b) -> a -> b
    $ (Edge Int (CMSet cinfo) -> Bool)
    -> [Edge Int (CMSet cinfo)] -> [Edge Int (CMSet cinfo)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Edge Int (CMSet cinfo) -> Bool
    f' ([Edge Int (CMSet cinfo)] -> [Edge Int (CMSet cinfo)])
    -> [Edge Int (CMSet cinfo)] -> [Edge Int (CMSet cinfo)]
    forall a b. (a -> b) -> a -> b
    $ CallGraph cinfo -> [Edge Int (CMSet cinfo)]
    forall cinfo. CallGraph cinfo -> [Call cinfo]
    toList (CallGraph cinfo -> [Edge Int (CMSet cinfo)])
    -> CallGraph cinfo -> [Edge Int (CMSet 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
        hasDecr :: c -> Either3 () c c
    hasDecr c
    cm = case c -> [Order]
    forall m e. Diagonal m e => m -> [e]
    diagonal c
    cm of
          Order
    g : [Order]
    xs
            | (Order -> Bool) -> [Order] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Order -> Bool
    isDecr [Order]
    xs -> () -> Either3 () c c
    forall a b c. a -> Either3 a b c
    In1 ()        -- Evidence found without guardedness.
            | Order -> Bool
    isDecr Order
    g      -> c -> Either3 () c c
    forall a b c. b -> Either3 a b c
    In2 c
    cm        -- Evidence found in guardedness.
            | Bool
    otherwise     -> c -> Either3 () c c
    forall a b c. c -> Either3 a b c
    In3 c
    cm        -- No evidence found.
          []                -> c -> Either3 () c c
    forall a b c. c -> Either3 a b c
    In3 c
    cm        -- No information means no evidence for termination.
        ([()]
    good, [CallMatrixAug cinfo]
    needGuardedness, [CallMatrixAug cinfo]
    bad) = [Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo)]
    -> ([()], [CallMatrixAug cinfo], [CallMatrixAug cinfo])
    forall a b c. [Either3 a b c] -> ([a], [b], [c])
    partitionEithers3 ([Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo)]
     -> ([()], [CallMatrixAug cinfo], [CallMatrixAug cinfo]))
    -> [Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo)]
    -> ([()], [CallMatrixAug cinfo], [CallMatrixAug cinfo])
    forall a b. (a -> b) -> a -> b
    $ (CallMatrixAug cinfo
     -> Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo))
    -> [CallMatrixAug cinfo]
    -> [Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo)]
    forall a b. (a -> b) -> [a] -> [b]
    map CallMatrixAug cinfo
    -> Either3 () (CallMatrixAug cinfo) (CallMatrixAug cinfo)
    forall {c}. Diagonal c Order => c -> Either3 () c c
    hasDecr [CallMatrixAug cinfo]
    idems

    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 -> Int
    forall n e. Edge n e -> n
    source Call cinfo
    c Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Call cinfo -> Int
    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
               ]

    -- | 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

    -- Instances

    instance Null GuardednessHelps where
      empty :: GuardednessHelps
    empty = GuardednessHelps
    GuardednessHelpsNot

    instance Boolean GuardednessHelps where
      fromBool :: Bool -> GuardednessHelps
    fromBool = \case
        Bool
    True  -> GuardednessHelps
    GuardednessHelpsYes
        Bool
    False -> GuardednessHelps
    GuardednessHelpsNot

    instance IsBool GuardednessHelps where
      toBool :: GuardednessHelps -> Bool
    toBool = \case
        GuardednessHelps
    GuardednessHelpsYes -> Bool
    True
        GuardednessHelps
    GuardednessHelpsNot -> Bool
    False

    instance NFData GuardednessHelps