module Agda.Termination.Termination
( terminates
, terminatesFilter
, Agda.Termination.Termination.tests
) where
import Agda.Termination.Lexicographic
import Agda.Termination.CallGraph
import Agda.Termination.SparseMatrix
import Agda.Utils.Either
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
import Control.Arrow
import Data.Array (Array)
import qualified Data.Array as Array
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
terminates :: (Ord meta, Monoid meta, ?cutoff :: Int) => CallGraph meta -> Either meta ()
terminates cs = let ccs = complete cs
in
checkIdems $ toList ccs
terminatesFilter :: (Ord meta, Monoid meta, ?cutoff :: Int) =>
(Index -> Bool) -> CallGraph meta -> Either meta ()
terminatesFilter f cs = checkIdems $ filter f' $ toList $ complete cs
where f' (c,m) = f (source c) && f (target c)
checkIdems :: (Ord meta, Monoid meta, ?cutoff :: Int) => [(Call,meta)] -> Either meta ()
checkIdems [] = Right ()
checkIdems ((c,m):xs) = if (checkIdem c) then checkIdems xs else Left m
checkIdem :: (?cutoff :: Int) => Call -> Bool
checkIdem c = let
b = target c == source c
idem = (c >*< c) == c
diag = Array.elems $ diagonal (mat (cm c))
hasDecr = any isDecr $ diag
in
(not b) || (not idem) || hasDecr
isDecr :: Order -> Bool
isDecr (Mat m) = any isDecr $ Array.elems $ diagonal m
isDecr o = decreasing o
type CG = CallGraph (Set Integer)
buildCallGraph :: [Call] -> CG
buildCallGraph = fromList . flip zip (map Set.singleton [1 ..])
example1 :: CG
example1 = buildCallGraph [c1, c2, c3]
where
flat = 1
aux = 2
c1 = Call { source = flat, target = aux
, cm = CallMatrix $ fromLists (Size 2 1) [[lt], [lt]]
}
c2 = Call { source = aux, target = aux
, cm = CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le]]
}
c3 = Call { source = aux, target = flat
, cm = CallMatrix $ fromLists (Size 1 2) [[unknown, le]]
}
prop_terminates_example1 :: (?cutoff :: Int) => Bool
prop_terminates_example1 = isRight $ terminates example1
example2 :: CG
example2 = buildCallGraph [c]
where
plus = 1
c = Call { source = plus, target = plus
, cm = CallMatrix $ fromLists (Size 2 2) [ [unknown, le]
, [lt, unknown] ]
}
prop_terminates_example2 :: (?cutoff :: Int) => 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 = Call { source = f, target = g
, cm = CallMatrix $ fromLists (Size 2 2) [ [unknown, le]
, [lt, unknown] ]
}
prop_terminates_example3 :: (?cutoff :: Int) => Bool
prop_terminates_example3 = isRight $ terminates example3
example4 :: CG
example4 = buildCallGraph [c1, c2, c3]
where
f = 1
g = 2
c1 = Call { source = f, target = f
, cm = CallMatrix $ fromLists (Size 2 2) [ [le, unknown]
, [unknown, le] ]
}
c2 = Call { source = f, target = g
, cm = CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le] ]
}
c3 = Call { source = g, target = f
, cm = CallMatrix $ fromLists (Size 2 2) [ [le, unknown]
, [unknown, le] ]
}
prop_terminates_example4 :: (?cutoff :: Int) => Bool
prop_terminates_example4 = isLeft $ terminates example4
example5 :: CG
example5 = buildCallGraph [c1, c2, c3, c4]
where
f = 1
g = 2
c1 = Call { source = f, target = g
, cm = CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le] ]
}
c2 = Call { source = f, target = f
, cm = CallMatrix $ fromLists (Size 2 2) [ [unknown, unknown]
, [unknown, lt] ]
}
c3 = Call { source = g, target = f
, cm = CallMatrix $ fromLists (Size 2 2) [ [le, unknown]
, [unknown, le] ]
}
c4 = Call { source = g, target = g
, cm = CallMatrix $ fromLists (Size 2 2) [ [lt, unknown]
, [unknown, le] ]
}
prop_terminates_example5 :: (?cutoff :: Int) => Bool
prop_terminates_example5 = isRight $ terminates example5
example6 :: CG
example6 = buildCallGraph [c1, c2, c3]
where
f = 1
c1 = Call { source = f, target = f
, cm = CallMatrix $ fromLists (Size 1 1) [ [lt] ]
}
c2 = Call { source = f, target = f
, cm = CallMatrix $ fromLists (Size 1 1) [ [le] ]
}
c3 = Call { source = f, target = f
, cm = CallMatrix $ fromLists (Size 1 1) [ [le] ]
}
prop_terminates_example6 :: (?cutoff :: Int) => Bool
prop_terminates_example6 = isLeft $ terminates example6
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
]
where ?cutoff = 0