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