{-# 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 Mikan.Termination.Termination
  ( Terminates(..)
  , terminates
  , terminatesFilter
  , terminationCounterexample
  , idempotentEndos
  ) where

import Prelude hiding ((&&), null)

import Data.Maybe (catMaybes)

import Mikan.Termination.CutOff
import Mikan.Termination.CallGraph
import Mikan.Termination.CallMatrix hiding (toList)
import Mikan.Termination.CallMatrix qualified as CMSet
import Mikan.Termination.Order
import Mikan.Termination.SparseMatrix

import Mikan.Utils.Maybe (boolToMaybe)
import Mikan.Utils.Null

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


-- | @'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 = (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
forall cinfo.
(Monoid cinfo, ?cutoff::CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminatesFilter ((Node -> Bool) -> CallGraph cinfo -> Terminates cinfo)
-> (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
forall a b. (a -> b) -> a -> b
$ Bool -> Node -> 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)
  => (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) =>
(Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminatesFilter Node -> 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 (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
forall cinfo.
(?cutoff::CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminationCounterexample Node -> 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 :: (?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.
terminationCounterexample :: forall cinfo.
(?cutoff::CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
terminationCounterexample Node -> Bool
f CallGraph cinfo
cs
  | CallMatrixAug cinfo
cm:[CallMatrixAug cinfo]
_ <- [CallMatrixAug cinfo]
bad = cinfo -> Terminates cinfo
forall cinfo. cinfo -> Terminates cinfo
TerminatesNot (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.
    bad :: [CallMatrixAug cinfo]
bad = [Maybe (CallMatrixAug cinfo)] -> [CallMatrixAug cinfo]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (CallMatrixAug cinfo)] -> [CallMatrixAug cinfo])
-> [Maybe (CallMatrixAug cinfo)] -> [CallMatrixAug cinfo]
forall a b. (a -> b) -> a -> b
$ (CallMatrixAug cinfo -> Maybe (CallMatrixAug cinfo))
-> [CallMatrixAug cinfo] -> [Maybe (CallMatrixAug cinfo)]
forall a b. (a -> b) -> [a] -> [b]
map CallMatrixAug cinfo -> Maybe (CallMatrixAug cinfo)
forall {a}. Diagonal a Order => a -> Maybe a
noDecr [CallMatrixAug cinfo]
idems
    idems :: [CallMatrixAug cinfo]
idems = (Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall cinfo.
(?cutoff::CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter Node -> Bool
f CallGraph cinfo
cs
    noDecr :: a -> Maybe a
noDecr a
cm = Bool -> a -> Maybe a
forall a. Bool -> a -> Maybe a
boolToMaybe (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Order -> Bool) -> [Order] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Order -> Bool
isDecr ([Order] -> Bool) -> [Order] -> Bool
forall a b. (a -> b) -> a -> b
$ a -> [Order]
forall m e. Diagonal m e => m -> [e]
diagonal a
cm) a
cm

-- | 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) =>
(Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter Node -> 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
. ((Node, CMSet cinfo) -> [CallMatrixAug cinfo])
-> [(Node, 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])
-> ((Node, CMSet cinfo) -> CMSet cinfo)
-> (Node, CMSet cinfo)
-> [CallMatrixAug cinfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node, CMSet cinfo) -> CMSet cinfo
forall a b. (a, b) -> b
snd) ([(Node, CMSet cinfo)] -> [CallMatrixAug cinfo])
-> (CallGraph cinfo -> [(Node, CMSet cinfo)])
-> CallGraph cinfo
-> [CallMatrixAug cinfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Node, CMSet cinfo) -> Bool)
-> [(Node, CMSet cinfo)] -> [(Node, CMSet cinfo)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Node -> Bool
f (Node -> Bool)
-> ((Node, CMSet cinfo) -> Node) -> (Node, CMSet cinfo) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node, CMSet cinfo) -> Node
forall a b. (a, b) -> a
fst) ([(Node, CMSet cinfo)] -> [(Node, CMSet cinfo)])
-> (CallGraph cinfo -> [(Node, CMSet cinfo)])
-> CallGraph cinfo
-> [(Node, CMSet cinfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallGraph cinfo -> [(Node, CMSet cinfo)]
forall cinfo. CallGraph cinfo -> [(Node, 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 = (Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall cinfo.
(?cutoff::CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
idempotentEndosFilter ((Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo])
-> (Node -> Bool) -> CallGraph cinfo -> [CallMatrixAug cinfo]
forall a b. (a -> b) -> a -> b
$ Bool -> Node -> 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