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