summaryrefslogtreecommitdiff
path: root/src/full/Agda/Termination/Termination.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Termination/Termination.hs')
-rw-r--r--src/full/Agda/Termination/Termination.hs198
1 files changed, 3 insertions, 195 deletions
diff --git a/src/full/Agda/Termination/Termination.hs b/src/full/Agda/Termination/Termination.hs
index 9b5ffc0..94b7de9 100644
--- a/src/full/Agda/Termination/Termination.hs
+++ b/src/full/Agda/Termination/Termination.hs
@@ -12,21 +12,18 @@ module Agda.Termination.Termination
, 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 Agda.Termination.CallGraph
+import Agda.Termination.CallMatrix hiding (toList)
import qualified Agda.Termination.CallMatrix as CMSet
-import Agda.Termination.Order hiding (tests)
+import Agda.Termination.Order
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
@@ -87,192 +84,3 @@ idempotent (CallMatrixAug m _) = (m >*< m) `notWorse` m
hasDecrease :: CallMatrixAug cinfo -> Bool
hasDecrease = any isDecr . diagonal
-
-------------------------------------------------------------------------
--- Some examples
-
-{- Convention (see TermCheck):
- Guardedness flag is in position (0,0) of the matrix,
- it is always present even if the functions are all recursive.
- The examples below do not include the guardedness flag, though.
- -}
-
--- | The call graph instantiation used by the examples below.
-
-type CG = CallGraph ()
-
--- | Constructs a call graph. No meta info.
-
-buildCallGraph :: [Call ()] -> CG
-buildCallGraph = fromList
-
--- | The example from the JFP'02 paper.
-
-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
-
--- | An example which is now handled by this algorithm: argument
--- swapping addition.
---
--- @S x + y = S (y + x)@
---
--- @Z + y = y@
-
-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
-
--- | A related example which is anyway handled: argument swapping addition
--- using two alternating functions.
---
--- @S x + y = S (y +' x)@
---
--- @Z + y = y@
---
--- @S x +' y = S (y + x)@
---
--- @Z +' y = y@
-
-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
-
--- | A contrived example.
---
--- @f (S x) y = f (S x) y + g x y@
---
--- @f Z y = y@
---
--- @g x y = f x y@
---
--- TODO: This example checks that the meta information is reported properly
--- when an error is encountered.
-
-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
-
--- | This should terminate.
---
--- @f (S x) (S y) = g x (S y) + f (S (S x)) y@
---
--- @g (S x) (S y) = f (S x) (S y) + g x (S y)@
-
-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
-
--- | Another example which should fail.
---
--- @f (S x) = f x + f (S x)@
---
--- @f x = f x@
---
--- TODO: This example checks that the meta information is reported properly
--- when an error is encountered.
-
-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
-
--- See issue 1055.
--- (The following function was adapted from Lee, Jones, and Ben-Amram,
--- POPL '01).
---
--- p : ℕ → ℕ → ℕ → ℕ
--- p m n (succ r) = p m r n
--- p m (succ n) zero = p zero n m
--- p m zero zero = m
-
-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
-
-------------------------------------------------------------------------
--- All tests
-
-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 -- all these examples are with just lt,le,unknown