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