{-# 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 :: 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 :: (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 :: [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 :: [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 :: 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 :: 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