{-# 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
  , terminationCounterexample
  , idempotentEndos
  ) where

import Prelude hiding ((&&), not, 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' does not use guardedness, 'terminatesFilter' is more general.
terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Terminates cinfo
terminates :: forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo -> Terminates cinfo
terminates = Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminatesFilter Bool
False ((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

-- | While no counterexample to termination is found,
--   complete the given call graph step-by-step.
terminatesFilter :: forall cinfo. (Monoid cinfo, ?cutoff :: CutOff)
  => Bool              -- ^ Use guardedness?
  -> (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) =>
Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminatesFilter Bool
useGuardedness Int -> Bool
f CallGraph cinfo
cs0 = (CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo
loop (CallGraph cinfo
cs0, CallGraph cinfo
cs0)
  where
    loop :: (CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo
    loop :: (CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo
loop (CallGraph cinfo
new, CallGraph cinfo
cs)
      -- If we have no new calls, the call graph is complete,
      -- and we have not found a counterexample.
      | CallGraph cinfo -> Bool
forall a. Null a => a -> Bool
null CallGraph cinfo
new  = Terminates cinfo
forall cinfo. Terminates cinfo
Terminates
      -- Otherwise the new calls might contain a counterexample.
      | Bool
otherwise = case Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminationCounterexample Bool
useGuardedness Int -> Bool
f CallGraph cinfo
new of
          -- If we have a counterexample already, we can stop the search for one.
          result :: Terminates cinfo
result@TerminatesNot{} -> Terminates cinfo
result
          -- Otherwise, we continue to complete the call-graph one step and look again.
          Terminates cinfo
Terminates -> (CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo
loop ((CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo)
-> (CallGraph cinfo, CallGraph cinfo) -> Terminates cinfo
forall a b. (a -> b) -> a -> b
$ CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
CallGraph cinfo
-> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
completionStep CallGraph cinfo
cs0 CallGraph cinfo
cs

-- | Does the given callgraph contain a counterexample to termination?
terminationCounterexample :: (Monoid cinfo, ?cutoff :: CutOff)
  => Bool              -- ^ Use guardedness?
  -> (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.
terminationCounterexample :: forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
Bool -> (Int -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminationCounterexample Bool
useGuardedness 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
  , Bool -> Bool
forall a. Boolean a => a -> a
not Bool
useGuardedness      = 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
    -- Every idempotent call must have decrease in the diagonal.
    ([()]
_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
    idems :: [CallMatrixAug cinfo]
idems = (Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall cinfo.
(?cutoff::CutOff) =>
(Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter Int -> Bool
f 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.

-- | Get all idempotent call-matrixes of loops in the call graph that match the given node-filter.
idempotentEndosFilter :: (?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter :: forall cinfo.
(?cutoff::CutOff) =>
(Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter Int -> Bool
f = (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])
-> (CallGraph cinfo -> [CallMatrixAug cinfo])
-> CallGraph cinfo
-> [CallMatrixAug cinfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, CMSet cinfo) -> [CallMatrixAug cinfo])
-> [(Int, CMSet cinfo)] -> [CallMatrixAug cinfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (CMSet cinfo -> [CallMatrixAug cinfo]
forall cinfo. CMSet cinfo -> [CallMatrixAug cinfo]
CMSet.toList (CMSet cinfo -> [CallMatrixAug cinfo])
-> ((Int, CMSet cinfo) -> CMSet cinfo)
-> (Int, CMSet cinfo)
-> [CallMatrixAug cinfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, CMSet cinfo) -> CMSet cinfo
forall a b. (a, b) -> b
snd) ([(Int, CMSet cinfo)] -> [CallMatrixAug cinfo])
-> (CallGraph cinfo -> [(Int, CMSet cinfo)])
-> CallGraph cinfo
-> [CallMatrixAug cinfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, CMSet cinfo) -> Bool)
-> [(Int, CMSet cinfo)] -> [(Int, CMSet cinfo)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Bool
f (Int -> Bool)
-> ((Int, CMSet cinfo) -> Int) -> (Int, CMSet cinfo) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, CMSet cinfo) -> Int
forall a b. (a, b) -> a
fst) ([(Int, CMSet cinfo)] -> [(Int, CMSet cinfo)])
-> (CallGraph cinfo -> [(Int, CMSet cinfo)])
-> CallGraph cinfo
-> [(Int, CMSet cinfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> [(Int, CMSet cinfo)]
forall cinfo. CallGraph cinfo -> [(Int, CMSet cinfo)]
loops

-- | Get all idempotent call-matrixes of loops in the call graph.
idempotentEndos :: (?cutoff :: CutOff) => CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndos :: forall cinfo.
(?cutoff::CutOff) =>
CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndos = (Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall cinfo.
(?cutoff::CutOff) =>
(Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter ((Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo])
-> (Int -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
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

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