module Agda.Termination.Termination
( terminates
, terminatesFilter
, endos
, idempotent
, Agda.Termination.Termination.tests
) where
import Agda.Termination.CutOff
import Agda.Termination.CallGraph hiding (tests)
import Agda.Termination.CallMatrix hiding (tests, toList)
import qualified Agda.Termination.CallMatrix as CMSet
import Agda.Termination.Order hiding (tests)
import Agda.Termination.SparseMatrix
import Agda.Utils.Either
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.TestHelpers hiding (idempotent)
import Agda.Utils.QuickCheck
import Data.Monoid
terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Either cinfo ()
terminates cs = checkIdems $ endos $ toList $ complete cs
terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) =>
(Node -> Bool) -> CallGraph cinfo -> Either cinfo ()
terminatesFilter f cs = checkIdems $ endos $ filter f' $ toList $ complete cs
where f' c = f (source c) && f (target c)
endos :: [Call cinfo] -> [CallMatrixAug cinfo]
endos cs = [ m | c <- cs, source c == target c
, m <- CMSet.toList $ callMatrixSet c
]
checkIdems :: (?cutoff :: CutOff) => [CallMatrixAug cinfo] -> Either cinfo ()
checkIdems calls = caseMaybe (headMaybe offending) (Right ()) $ Left . augCallInfo
where
offending = filter (not . hasDecrease) $ filter idempotent calls
checkIdem :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool
checkIdem c = if idempotent c then hasDecrease c else True
idempotent :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool
idempotent (CallMatrixAug m _) = (m >*< m) `notWorse` m
hasDecrease :: CallMatrixAug cinfo -> Bool
hasDecrease = any isDecr . diagonal
type CG = CallGraph ()
buildCallGraph :: [Call ()] -> CG
buildCallGraph = fromList
example1 :: CG
example1 = buildCallGraph [c1, c2, c3]
where
flat = 1
aux = 2
c1 = mkCall' flat aux $ CallMatrix $ fromLists (Size 2 1) [ [lt]
, [lt]]
c2 = mkCall' aux aux $ CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le]]
c3 = mkCall' aux flat $ CallMatrix $ fromLists (Size 1 2) [ [unknown, le]]
prop_terminates_example1 :: (?cutoff :: CutOff) => Bool
prop_terminates_example1 = isRight $ terminates example1
example2 :: CG
example2 = buildCallGraph [c]
where
plus = 1
c = mkCall' plus plus $ CallMatrix $ fromLists (Size 2 2) [ [unknown, le]
, [lt, unknown] ]
prop_terminates_example2 :: (?cutoff :: CutOff) => Bool
prop_terminates_example2 = isRight $ terminates example2
example3 :: CG
example3 = buildCallGraph [c plus plus', c plus' plus]
where
plus = 1
plus' = 2
c f g = mkCall' f g $ CallMatrix $ fromLists (Size 2 2) [ [unknown, le]
, [lt, unknown] ]
prop_terminates_example3 :: (?cutoff :: CutOff) => Bool
prop_terminates_example3 = isRight $ terminates example3
example4 :: CG
example4 = buildCallGraph [c1, c2, c3]
where
f = 1
g = 2
c1 = mkCall' f f $ CallMatrix $ fromLists (Size 2 2) $
[ [le, unknown]
, [unknown, le] ]
c2 = mkCall' f g $ CallMatrix $ fromLists (Size 2 2) $
[ [lt, unknown]
, [unknown, le] ]
c3 = mkCall' g f $ CallMatrix $ fromLists (Size 2 2) $
[ [le, unknown]
, [unknown, le] ]
prop_terminates_example4 :: (?cutoff :: CutOff) => Bool
prop_terminates_example4 = isLeft $ terminates example4
example5 :: CG
example5 = buildCallGraph [c1, c2, c3, c4]
where
f = 1
g = 2
c1 = mkCall' f g $ CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le] ]
c2 = mkCall' f f $ CallMatrix $ fromLists (Size 2 2) [ [unknown, unknown]
, [unknown, lt] ]
c3 = mkCall' g f $ CallMatrix $ fromLists (Size 2 2) [ [le, unknown]
, [unknown, le] ]
c4 = mkCall' g g $ CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le] ]
prop_terminates_example5 :: (?cutoff :: CutOff) => Bool
prop_terminates_example5 = isRight $ terminates example5
example6 :: CG
example6 = buildCallGraph [c1, c2, c3]
where
f = 1
c1 = mkCall' f f $ CallMatrix $ fromLists (Size 1 1) [ [lt] ]
c2 = mkCall' f f $ CallMatrix $ fromLists (Size 1 1) [ [le] ]
c3 = mkCall' f f $ CallMatrix $ fromLists (Size 1 1) [ [le] ]
prop_terminates_example6 :: (?cutoff :: CutOff) => Bool
prop_terminates_example6 = isLeft $ terminates example6
example7 :: CG
example7 = buildCallGraph [call1, call2]
where
call1 = mkCall' 1 1 $ CallMatrix $ fromLists (Size 3 3)
[ [le, le, le]
, [un, lt, un]
, [le, un, un]
]
call2 = mkCall' 1 1 $ CallMatrix $ fromLists (Size 3 3)
[ [le, un, un]
, [un, un, lt]
, [un, le, un]
]
un = unknown
prop_terminates_example7 :: (?cutoff :: CutOff) => Bool
prop_terminates_example7 = isRight $ terminates example7
tests :: IO Bool
tests = runTests "Agda.Termination.Termination"
[ quickCheck' prop_terminates_example1
, quickCheck' prop_terminates_example2
, quickCheck' prop_terminates_example3
, quickCheck' prop_terminates_example4
, quickCheck' prop_terminates_example5
, quickCheck' prop_terminates_example6
, quickCheck' prop_terminates_example7
]
where ?cutoff = CutOff 0