{-# 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 = forall cinfo.
(?cutoff::CutOff) =>
[CallMatrixAug cinfo] -> Either cinfo ()
checkIdems forall a b. (a -> b) -> a -> b
$ forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
endos forall a b. (a -> b) -> a -> b
$ forall cinfo. CallGraph cinfo -> [Call cinfo]
toList forall a b. (a -> b) -> a -> b
$ 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 = forall cinfo.
(?cutoff::CutOff) =>
[CallMatrixAug cinfo] -> Either cinfo ()
checkIdems forall a b. (a -> b) -> a -> b
$ forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
endos forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Call cinfo -> Bool
f' forall a b. (a -> b) -> a -> b
$ forall cinfo. CallGraph cinfo -> [Call cinfo]
toList forall a b. (a -> b) -> a -> b
$ 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 (forall n e. Edge n e -> n
source Call cinfo
c) Bool -> Bool -> Bool
&& Node -> Bool
f (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, forall n e. Edge n e -> n
source Call cinfo
c forall a. Eq a => a -> a -> Bool
== forall n e. Edge n e -> n
target Call cinfo
c
               , CallMatrixAug cinfo
m <- forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
CMSet.toList forall a b. (a -> b) -> a -> b
$ 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 = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall a. [a] -> Maybe a
listToMaybe [CallMatrixAug cinfo]
offending) (forall a b. b -> Either a b
Right ()) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall cinfo. CallMatrixAug cinfo -> cinfo
augCallInfo
  where
    -- Every idempotent call must have decrease, otherwise it offends us.
    offending :: [CallMatrixAug cinfo]
offending = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall cinfo. CallMatrixAug cinfo -> Bool
hasDecrease) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter 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 forall a. (CallComb a, ?cutoff::CutOff) => a -> a -> a
>*< CallMatrix
m) forall a. NotWorse a => a -> a -> Bool
`notWorse` CallMatrix
m

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