module Agda.Termination.Termination
( terminates
, Agda.Termination.Termination.tests
) where
import Agda.Termination.Lexicographic
import Agda.Termination.CallGraph
import Agda.Termination.Matrix
import Agda.Utils.Either
import Agda.Utils.TestHelpers
import Control.Arrow
import Agda.Utils.QuickCheck
import qualified Data.Set as Set
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
import Data.Array (Array)
terminates :: (Ord meta, Monoid meta) => CallGraph meta -> Either meta ()
terminates cs = let ccs = complete cs
in
checkIdems $ toList ccs
checkIdems :: (Ord meta,Monoid meta) => [(Call,meta)] -> Either meta ()
checkIdems [] = Right ()
checkIdems ((c,m):xs) = if (checkIdem c) then checkIdems xs else Left m
checkIdem :: 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 Lt = True
isDecr (Mat m) = any isDecr $ Array.elems $ diagonal m
isDecr _ = False
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 = 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 = 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 = 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 = 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 = 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 = 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
]