1{-# LANGUAGE ImplicitParams #-} 2{-# LANGUAGE CPP #-} 3 4module Agda.Termination.CallMatrix where 5 6-- module Agda.Termination.CallMatrix 7-- ( CallMatrix'(..), CallMatrix 8-- , callMatrix 9-- , CallComb(..) 10-- , tests 11-- ) where 12 13#if __GLASGOW_HASKELL__ < 804 14import Data.Semigroup 15#endif 16 17import Agda.Termination.CutOff 18import Agda.Termination.Order as Order 19import Agda.Termination.SparseMatrix as Matrix 20import Agda.Termination.Semiring (HasZero(..)) 21 22import Agda.Utils.Favorites (Favorites) 23import qualified Agda.Utils.Favorites as Fav 24 25import Agda.Utils.Null 26import Agda.Utils.PartialOrd 27import Agda.Utils.Pretty 28import Agda.Utils.Singleton 29 30------------------------------------------------------------------------ 31-- * Call matrices 32------------------------------------------------------------------------ 33 34-- | Call matrix indices = function argument indices. 35-- 36-- Machine integer 'Int' is sufficient, since we cannot index more arguments 37-- than we have addresses on our machine. 38 39type ArgumentIndex = Int 40 41-- | Call matrices. 42-- 43-- A call matrix for a call @f --> g@ has dimensions @ar(g) × ar(f)@. 44-- 45-- Each column corresponds to one formal argument of caller @f@. 46-- Each row corresponds to one argument in the call to @g@. 47-- 48-- In the presence of dot patterns, a call argument can be related 49-- to /several/ different formal arguments of @f@. 50-- 51-- See e.g. @test/succeed/DotPatternTermination.agda@: 52-- 53-- @ 54-- data D : Nat -> Set where 55-- cz : D zero 56-- c1 : forall n -> D n -> D (suc n) 57-- c2 : forall n -> D n -> D n 58-- 59-- f : forall n -> D n -> Nat 60-- f .zero cz = zero 61-- f .(suc n) (c1 n d) = f n (c2 n d) 62-- f n (c2 .n d) = f n d 63-- @ 64-- 65-- Call matrices (without guardedness) are 66-- 67-- @ 68-- -1 -1 n < suc n and n < c1 n d 69-- ? = c2 n d <= c1 n d 70-- 71-- = -1 n <= n and n < c2 n d 72-- ? -1 d < c2 n d 73-- @ 74-- 75-- Here is a part of the original documentation for call matrices 76-- (kept for historical reasons): 77-- 78-- This datatype encodes information about a single recursive 79-- function application. The columns of the call matrix stand for 80-- 'source' function arguments (patterns). The rows of the matrix stand for 81-- 'target' function arguments. Element @(i, j)@ in the matrix should 82-- be computed as follows: 83-- 84-- * 'Order.lt' (less than) if the @j@-th argument to the 'target' 85-- function is structurally strictly smaller than the @i@-th 86-- pattern. 87-- 88-- * 'Order.le' (less than or equal) if the @j@-th argument to the 89-- 'target' function is structurally smaller than the @i@-th 90-- pattern. 91-- 92-- * 'Order.unknown' otherwise. 93 94 95newtype CallMatrix' a = CallMatrix { mat :: Matrix ArgumentIndex a } 96 deriving (Eq, Ord, Show, Functor, Foldable, Traversable, PartialOrd) 97 98type CallMatrix = CallMatrix' Order 99 100deriving instance NotWorse CallMatrix 101 102instance HasZero a => Diagonal (CallMatrix' a) a where 103 diagonal = diagonal . mat 104 105 106-- | Call matrix multiplication and call combination. 107 108class CallComb a where 109 (>*<) :: (?cutoff :: CutOff) => a -> a -> a 110 111-- | Call matrix multiplication. 112-- 113-- @f --(m1)--> g --(m2)--> h@ is combined to @f --(m2 `mul` m1)--> h@ 114-- 115-- Note the reversed order of multiplication: 116-- The matrix @c1@ of the second call @g-->h@ in the sequence 117-- @f-->g-->h@ is multiplied with the matrix @c2@ of the first call. 118-- 119-- Preconditions: 120-- @m1@ has dimensions @ar(g) × ar(f)@. 121-- @m2@ has dimensions @ar(h) × ar(g)@. 122-- 123-- Postcondition: 124-- @m1 >*< m2@ has dimensions @ar(h) × ar(f)@. 125 126instance CallComb CallMatrix where 127 CallMatrix m1 >*< CallMatrix m2 = CallMatrix $ mul orderSemiring m2 m1 128 129{- UNUSED, BUT DON'T REMOVE! 130-- | Call matrix addition = minimum = pick worst information. 131addCallMatrices :: (?cutoff :: CutOff) => CallMatrix -> CallMatrix -> CallMatrix 132addCallMatrices cm1 cm2 = CallMatrix $ 133 add (Semiring.add orderSemiring) (mat cm1) (mat cm2) 134-} 135 136------------------------------------------------------------------------ 137-- * Call matrix augmented with path information. 138------------------------------------------------------------------------ 139 140-- | Call matrix augmented with path information. 141 142data CallMatrixAug cinfo = CallMatrixAug 143 { augCallMatrix :: CallMatrix -- ^ The matrix of the (composed call). 144 , augCallInfo :: cinfo -- ^ Meta info, like call path. 145 } 146 deriving (Eq, Show) 147 148instance Diagonal (CallMatrixAug cinfo) Order where 149 diagonal = diagonal . augCallMatrix 150 151instance PartialOrd (CallMatrixAug cinfo) where 152 comparable m m' = comparable (augCallMatrix m) (augCallMatrix m') 153 154instance NotWorse (CallMatrixAug cinfo) where 155 c1 `notWorse` c2 = augCallMatrix c1 `notWorse` augCallMatrix c2 156 157-- | Augmented call matrix multiplication. 158 159instance Monoid cinfo => CallComb (CallMatrixAug cinfo) where 160 CallMatrixAug m1 p1 >*< CallMatrixAug m2 p2 = 161 CallMatrixAug (m1 >*< m2) (mappend p1 p2) 162 163-- | Non-augmented call matrix. 164 165noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo 166noAug m = CallMatrixAug m mempty 167 168------------------------------------------------------------------------ 169-- * Sets of incomparable call matrices augmented with path information. 170------------------------------------------------------------------------ 171 172-- | Sets of incomparable call matrices augmented with path information. 173-- Use overloaded 'null', 'empty', 'singleton', 'mappend'. 174newtype CMSet cinfo = CMSet { cmSet :: Favorites (CallMatrixAug cinfo) } 175 deriving ( Show, Semigroup, Monoid, Null, Singleton (CallMatrixAug cinfo) ) 176 177-- | Call matrix set product is the Cartesian product. 178 179instance Monoid cinfo => CallComb (CMSet cinfo) where 180 CMSet as >*< CMSet bs = CMSet $ Fav.fromList $ 181 [ a >*< b | a <- Fav.toList as, b <- Fav.toList bs ] 182 183-- | Insert into a call matrix set. 184 185insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo 186insert a (CMSet as) = CMSet $ Fav.insert a as 187 188-- | Union two call matrix sets. 189 190union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo 191union = mappend 192-- union (CMSet as) (CMSet bs) = CMSet $ Fav.union as bs 193 194-- | Convert into a list of augmented call matrices. 195 196toList :: CMSet cinfo -> [CallMatrixAug cinfo] 197toList (CMSet as) = Fav.toList as 198 199------------------------------------------------------------------------ 200-- * Printing 201------------------------------------------------------------------------ 202 203instance Pretty CallMatrix where 204 pretty (CallMatrix m) = pretty m 205 206instance Pretty cinfo => Pretty (CallMatrixAug cinfo) where 207 pretty (CallMatrixAug m cinfo) = pretty cinfo $$ pretty m 208 209instance Pretty cinfo => Pretty (CMSet cinfo) where 210 pretty = vcat . punctuate newLine . map pretty . toList 211 where newLine = "\n" 212