1
2-- | Auxiliary functions to handle patterns in the abstract syntax.
3--
4--   Generic and specific traversals.
5
6module Agda.Syntax.Abstract.Pattern where
7
8import Prelude hiding (null)
9
10import Control.Arrow ((***), second)
11import Control.Monad.Identity
12import Control.Applicative (liftA2)
13
14
15import Data.Maybe
16import Data.Monoid
17
18import Agda.Syntax.Abstract as A
19import Agda.Syntax.Common
20import Agda.Syntax.Concrete (FieldAssignment')
21import qualified Agda.Syntax.Concrete as C
22import Agda.Syntax.Concrete.Pattern (IsWithP(..))
23import Agda.Syntax.Info
24import Agda.Syntax.Position
25
26import Agda.Utils.Functor
27import Agda.Utils.List
28import Agda.Utils.Null
29
30import Agda.Utils.Impossible
31
32-- * Generic traversals
33------------------------------------------------------------------------
34
35type NAP = NamedArg Pattern
36
37class MapNamedArgPattern a  where
38  mapNamedArgPattern :: (NAP -> NAP) -> a -> a
39
40  default mapNamedArgPattern
41     :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a
42  mapNamedArgPattern = fmap . mapNamedArgPattern
43
44instance MapNamedArgPattern NAP where
45  mapNamedArgPattern f p =
46    case namedArg p of
47      -- no sub patterns:
48      VarP{}    -> f p
49      WildP{}   -> f p
50      DotP{}    -> f p
51      EqualP{}  -> f p
52      LitP{}    -> f p
53      AbsurdP{} -> f p
54      ProjP{}   -> f p
55      -- list of NamedArg subpatterns:
56      ConP i qs ps       -> f $ setNamedArg p $ ConP i qs $ mapNamedArgPattern f ps
57      DefP i qs ps       -> f $ setNamedArg p $ DefP i qs $ mapNamedArgPattern f ps
58      PatternSynP i x ps -> f $ setNamedArg p $ PatternSynP i x $ mapNamedArgPattern f ps
59      -- Pattern subpattern(s):
60      -- RecP: we copy the NamedArg info to the subpatterns but discard it after recursion
61      RecP i fs          -> f $ setNamedArg p $ RecP i $ map (fmap namedArg) $ mapNamedArgPattern f $ map (fmap (setNamedArg p)) fs
62      -- AsP: we hand the NamedArg info to the subpattern
63      AsP i x p0         -> f $ updateNamedArg (AsP i x) $ mapNamedArgPattern f $ setNamedArg p p0
64      -- WithP: like AsP
65      WithP i p0         -> f $ updateNamedArg (WithP i) $ mapNamedArgPattern f $ setNamedArg p p0
66      AnnP i a p0        -> f $ updateNamedArg (AnnP i a) $ mapNamedArgPattern f $ setNamedArg p p0
67
68instance MapNamedArgPattern a => MapNamedArgPattern [a]                  where
69instance MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) where
70instance MapNamedArgPattern a => MapNamedArgPattern (Maybe a)            where
71
72instance (MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a,b) where
73  mapNamedArgPattern f (a, b) = (mapNamedArgPattern f a, mapNamedArgPattern f b)
74
75-- | Generic pattern traversal.
76
77class APatternLike p where
78  type ADotT p
79
80  -- | Fold pattern.
81  foldrAPattern
82    :: Monoid m
83    => (Pattern' (ADotT p) -> m -> m)
84         -- ^ Combine a pattern and the value computed from its subpatterns.
85    -> p -> m
86
87  default foldrAPattern
88    :: (Monoid m, Foldable f, APatternLike b, (ADotT p) ~ (ADotT b), f b ~ p)
89    => (Pattern' (ADotT p) -> m -> m) -> p -> m
90  foldrAPattern = foldMap . foldrAPattern
91
92  -- | Traverse pattern.
93  traverseAPatternM
94    :: Monad m
95    => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @pre@: Modification before recursion.
96    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @post@: Modification after recursion.
97    -> p -> m p
98
99  default traverseAPatternM
100    :: (Traversable f, APatternLike q, (ADotT p) ~ (ADotT q), f q ~ p, Monad m)
101    => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
102    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
103    -> p -> m p
104  traverseAPatternM pre post = traverse $ traverseAPatternM pre post
105
106-- | Compute from each subpattern a value and collect them all in a monoid.
107
108foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m
109foldAPattern f = foldrAPattern $ \ p m -> f p `mappend` m
110
111-- | Traverse pattern(s) with a modification before the recursive descent.
112
113preTraverseAPatternM
114  :: (APatternLike p, Monad m )
115  => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @pre@: Modification before recursion.
116  -> p -> m p
117preTraverseAPatternM pre p = traverseAPatternM pre return p
118
119-- | Traverse pattern(s) with a modification after the recursive descent.
120
121postTraverseAPatternM
122  :: (APatternLike p, Monad m )
123  => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @post@: Modification after recursion.
124  -> p -> m p
125postTraverseAPatternM post p = traverseAPatternM return post p
126
127-- | Map pattern(s) with a modification after the recursive descent.
128
129mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
130mapAPattern f = runIdentity . postTraverseAPatternM (Identity . f)
131
132-- Interesting instance:
133
134instance APatternLike (Pattern' a) where
135  type ADotT (Pattern' a) = a
136
137  foldrAPattern f p = f p $
138    case p of
139      AsP _ _ p          -> foldrAPattern f p
140      ConP _ _ ps        -> foldrAPattern f ps
141      DefP _ _ ps        -> foldrAPattern f ps
142      RecP _ ps          -> foldrAPattern f ps
143      PatternSynP _ _ ps -> foldrAPattern f ps
144      WithP _ p          -> foldrAPattern f p
145      VarP _             -> mempty
146      ProjP _ _ _        -> mempty
147      WildP _            -> mempty
148      DotP _ _           -> mempty
149      AbsurdP _          -> mempty
150      LitP _ _           -> mempty
151      EqualP _ _         -> mempty
152      AnnP _ _ p         -> foldrAPattern f p
153
154  traverseAPatternM pre post = pre >=> recurse >=> post
155    where
156    recurse = \case
157      -- Non-recursive cases:
158      p@A.VarP{}            -> return p
159      p@A.WildP{}           -> return p
160      p@A.DotP{}            -> return p
161      p@A.LitP{}            -> return p
162      p@A.AbsurdP{}         -> return p
163      p@A.ProjP{}           -> return p
164      p@A.EqualP{}          -> return p
165      -- Recursive cases:
166      A.ConP        i ds ps -> A.ConP        i ds <$> traverseAPatternM pre post ps
167      A.DefP        i q  ps -> A.DefP        i q  <$> traverseAPatternM pre post ps
168      A.AsP         i x  p  -> A.AsP         i x  <$> traverseAPatternM pre post p
169      A.RecP        i    ps -> A.RecP        i    <$> traverseAPatternM pre post ps
170      A.PatternSynP i x  ps -> A.PatternSynP i x  <$> traverseAPatternM pre post ps
171      A.WithP       i p     -> A.WithP       i    <$> traverseAPatternM pre post p
172      A.AnnP        i a  p  -> A.AnnP        i a  <$> traverseAPatternM pre post p
173
174instance APatternLike a => APatternLike (Arg a) where
175  type ADotT (Arg a) = ADotT a
176
177instance APatternLike a => APatternLike (Named n a) where
178  type ADotT (Named n a) = ADotT a
179
180instance APatternLike a => APatternLike [a] where
181  type ADotT [a] = ADotT a
182
183instance APatternLike a => APatternLike (Maybe a) where
184  type ADotT (Maybe a) = ADotT a
185
186instance APatternLike a => APatternLike (FieldAssignment' a) where
187  type ADotT (FieldAssignment' a) = ADotT a
188
189instance (APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b) where
190  type ADotT (a, b) = ADotT a
191
192  foldrAPattern f (p, p') =
193    foldrAPattern f p `mappend` foldrAPattern f p'
194
195  traverseAPatternM pre post (p, p') =
196    liftA2 (,)
197      (traverseAPatternM pre post p)
198      (traverseAPatternM pre post p')
199
200
201-- * Specific folds
202------------------------------------------------------------------------
203
204-- | Collect pattern variables in left-to-right textual order.
205
206patternVars :: APatternLike p => p -> [A.Name]
207patternVars p = foldAPattern f p `appEndo` []
208  where
209  -- We use difference lists @[A.Name] -> [A.Name]@ to avoid reconcatenation.
210  f :: Pattern' a -> Endo [A.Name]
211  f = \case
212    A.VarP x         -> Endo (unBind x :)
213    A.AsP _ x _      -> Endo (unBind x :)
214    A.LitP        {} -> mempty
215    A.ConP        {} -> mempty
216    A.RecP        {} -> mempty
217    A.DefP        {} -> mempty
218    A.ProjP       {} -> mempty
219    A.WildP       {} -> mempty
220    A.DotP        {} -> mempty
221    A.AbsurdP     {} -> mempty
222    A.EqualP      {} -> mempty
223    A.PatternSynP {} -> mempty
224    A.WithP _ _      -> mempty
225    A.AnnP        {} -> mempty
226
227-- | Check if a pattern contains a specific (sub)pattern.
228
229containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool
230containsAPattern f = getAny . foldAPattern (Any . f)
231
232-- | Check if a pattern contains an absurd pattern.
233--   For instance, @suc ()@, does so.
234--
235--   Precondition: contains no pattern synonyms.
236
237containsAbsurdPattern :: APatternLike p => p -> Bool
238containsAbsurdPattern = containsAPattern $ \case
239    A.PatternSynP{} -> __IMPOSSIBLE__
240    A.AbsurdP{}     -> True
241    _               -> False
242
243-- | Check if a pattern contains an @-pattern.
244--
245containsAsPattern :: APatternLike p => p -> Bool
246containsAsPattern = containsAPattern $ \case
247    A.AsP{}         -> True
248    _               -> False
249
250-- | Check if any user-written pattern variables occur more than once,
251--   and throw the given error if they do.
252checkPatternLinearity :: (Monad m, APatternLike p)
253                      => p -> ([C.Name] -> m ()) -> m ()
254checkPatternLinearity ps err =
255  unlessNull (duplicates $ map nameConcrete $ patternVars ps) $ \ys -> err ys
256
257
258-- * Specific traversals
259------------------------------------------------------------------------
260
261-- | Pattern substitution.
262--
263-- For the embedded expression, the given pattern substitution is turned into
264-- an expression substitution.
265
266substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
267substPattern s = substPattern' (substExpr $ map (second patternToExpr) s) s
268
269-- | Pattern substitution, parametrized by substitution function for embedded expressions.
270
271substPattern'
272  :: (e -> e)              -- ^ Substitution function for expressions.
273  -> [(Name, Pattern' e)]  -- ^ (Parallel) substitution.
274  -> Pattern' e            -- ^ Input pattern.
275  -> Pattern' e
276substPattern' subE s = mapAPattern $ \ p -> case p of
277  VarP x            -> fromMaybe p $ lookup (A.unBind x) s
278  DotP i e          -> DotP i $ subE e
279  EqualP i es       -> EqualP i $ map (subE *** subE) es
280  AnnP i a p        -> AnnP i (subE a) p
281  -- No action on the other patterns (besides the recursion):
282  ConP _ _ _        -> p
283  RecP _ _          -> p
284  ProjP _ _ _       -> p
285  WildP _           -> p
286  AbsurdP _         -> p
287  LitP _ _          -> p
288  DefP _ _ _        -> p
289  AsP _ _ _         -> p -- Note: cannot substitute into as-variable
290  PatternSynP _ _ _ -> p
291  WithP _ _         -> p
292
293
294-- * Other pattern utilities
295------------------------------------------------------------------------
296
297-- | Check for with-pattern.
298instance IsWithP (Pattern' e) where
299  isWithP = \case
300    WithP _ p -> Just p
301    _ -> Nothing
302
303-- | Split patterns into (patterns, trailing with-patterns).
304splitOffTrailingWithPatterns :: A.Patterns -> (A.Patterns, A.Patterns)
305splitOffTrailingWithPatterns = spanEnd (isJust . isWithP)
306
307-- | Get the tail of with-patterns of a pattern spine.
308trailingWithPatterns :: Patterns -> Patterns
309trailingWithPatterns = snd . splitOffTrailingWithPatterns
310
311-- | The next patterns are ...
312--
313-- (This view discards 'PatInfo'.)
314data LHSPatternView e
315  = LHSAppP  (NAPs e)
316      -- ^ Application patterns (non-empty list).
317  | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
318      -- ^ A projection pattern.  Is also stored unmodified here.
319  | LHSWithP [Pattern' e]
320      -- ^ With patterns (non-empty list).
321      --   These patterns are not prefixed with 'WithP'.
322  deriving (Show)
323
324-- | Construct the 'LHSPatternView' of the given list (if not empty).
325--
326-- Return the view and the remaining patterns.
327
328lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
329lhsPatternView [] = Nothing
330lhsPatternView (p0 : ps) =
331  case namedArg p0 of
332    ProjP _i o d -> Just (LHSProjP o d p0, ps)
333    -- If the next pattern is a with-pattern, collect more with-patterns
334    WithP _i p   -> Just (LHSWithP (p : map namedArg ps1), ps2)
335      where
336      (ps1, ps2) = spanJust isWithP ps
337    -- If the next pattern is an application pattern, collect more of these
338    _ -> Just (LHSAppP (p0 : ps1), ps2)
339      where
340      (ps1, ps2) = span (\ p -> isNothing (isProjP p) && isNothing (isWithP p)) ps
341
342-- * Left-hand-side manipulation
343------------------------------------------------------------------------
344
345-- | Convert a focused lhs to spine view and back.
346class LHSToSpine a b where
347  lhsToSpine :: a -> b
348  spineToLhs :: b -> a
349
350-- | Clause instance.
351instance LHSToSpine Clause SpineClause where
352  lhsToSpine = fmap lhsToSpine
353  spineToLhs = fmap spineToLhs
354
355-- | List instance (for clauses).
356instance LHSToSpine a b => LHSToSpine [a] [b] where
357  lhsToSpine = map lhsToSpine
358  spineToLhs = map spineToLhs
359
360-- | LHS instance.
361instance LHSToSpine LHS SpineLHS where
362  lhsToSpine (LHS i core) = SpineLHS i f ps
363    where QNamed f ps = lhsCoreToSpine core
364  spineToLhs (SpineLHS i f ps) = LHS i (spineToLhsCore $ QNamed f ps)
365
366lhsCoreToSpine :: LHSCore' e -> A.QNamed [NamedArg (Pattern' e)]
367lhsCoreToSpine = \case
368  LHSHead f ps     -> QNamed f ps
369  LHSProj d h ps   -> lhsCoreToSpine (namedArg h) <&> (++ (p : ps))
370    where p = updateNamedArg (const $ ProjP empty ProjPrefix d) h
371  LHSWith h wps ps -> lhsCoreToSpine h <&> (++ map fromWithPat wps ++ ps)
372    where
373      fromWithPat :: Arg (Pattern' e) -> NamedArg (Pattern' e)
374      fromWithPat = fmap (unnamed . mkWithP)
375      mkWithP p   = WithP (PatRange $ getRange p) p
376
377spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
378spineToLhsCore (QNamed f ps) = lhsCoreAddSpine (LHSHead f []) ps
379
380-- | Add applicative patterns (non-projection / non-with patterns) to the right.
381lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
382lhsCoreApp core ps = core { lhsPats = lhsPats core ++ ps }
383
384-- | Add with-patterns to the right.
385lhsCoreWith :: LHSCore' e -> [Arg (Pattern' e)] -> LHSCore' e
386lhsCoreWith (LHSWith core wps []) wps' = LHSWith core (wps ++ wps') []
387lhsCoreWith core                  wps' = LHSWith core wps' []
388
389lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
390lhsCoreAddChunk core = \case
391  LHSAppP ps               -> lhsCoreApp core ps
392  LHSWithP wps             -> lhsCoreWith core (defaultArg <$> wps)
393  LHSProjP ProjPrefix d np -> LHSProj d (setNamedArg np core) []  -- Prefix projection pattern.
394  LHSProjP _          _ np -> lhsCoreApp core [np]       -- Postfix projection pattern.
395
396-- | Add projection, with, and applicative patterns to the right.
397lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
398lhsCoreAddSpine core ps =
399  -- Recurse on lhsPatternView until no patterns left.
400  case lhsPatternView ps of
401    Nothing       -> core
402    Just (v, ps') -> lhsCoreAddChunk core chunk `lhsCoreAddSpine` ps'
403      where
404      -- Andreas, 2016-06-13
405      -- If the projection was written prefix by the user
406      -- or it is a fully applied operator
407      -- we turn it to prefix projection form.
408      chunk = case v of
409        LHSProjP ProjPrefix _ _
410          -> v
411        LHSProjP _ d np | let nh = C.numHoles d, nh > 0, nh <= 1 + length ps'
412          -> LHSProjP ProjPrefix d np
413        _ -> v
414
415-- | Used for checking pattern linearity.
416lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
417lhsCoreAllPatterns = map namedArg . qnamed . lhsCoreToSpine
418
419-- | Used in ''Agda.Syntax.Translation.AbstractToConcrete''.
420--   Returns a 'DefP'.
421lhsCoreToPattern :: LHSCore -> Pattern
422lhsCoreToPattern lc =
423  case lc of
424    LHSHead f aps         -> DefP noInfo (unambiguous f) aps
425    LHSProj d lhscore aps -> DefP noInfo d $
426      fmap (fmap lhsCoreToPattern) lhscore : aps
427    LHSWith h wps aps     -> case lhsCoreToPattern h of
428      DefP r q ps         -> DefP r q $ ps ++ map fromWithPat wps ++ aps
429        where
430          fromWithPat :: Arg Pattern -> NamedArg Pattern
431          fromWithPat = fmap (unnamed . mkWithP)
432          mkWithP p   = WithP (PatRange $ getRange p) p
433      _ -> __IMPOSSIBLE__
434  where noInfo = empty -- TODO, preserve range!
435
436mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
437mapLHSHead f = \case
438  LHSHead x ps     -> f x ps
439  LHSProj d h ps   -> LHSProj d (fmap (fmap (mapLHSHead f)) h) ps
440  LHSWith h wps ps -> LHSWith (mapLHSHead f h) wps ps
441