1
2-- | Pattern synonym utilities: folding pattern synonym definitions for
3--   printing and merging pattern synonym definitions to handle overloaded
4--   pattern synonyms.
5module Agda.Syntax.Abstract.PatternSynonyms
6  ( matchPatternSyn
7  , matchPatternSynP
8  , mergePatternSynDefs
9  ) where
10
11import Control.Applicative ( Alternative(empty) )
12import Control.Monad.Writer hiding (forM)
13
14import Data.Map (Map)
15import qualified Data.Map as Map
16import Data.Traversable (forM)
17import Data.List
18import Data.Void
19
20import Agda.Syntax.Common
21import Agda.Syntax.Abstract
22import Agda.Syntax.Abstract.Views
23
24import Agda.Utils.List1 (List1, pattern (:|))
25import qualified Agda.Utils.List1 as List1
26
27-- | Merge a list of pattern synonym definitions. Fails unless all definitions
28--   have the same shape (i.e. equal up to renaming of variables and constructor
29--   names).
30mergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn
31mergePatternSynDefs (def :| defs) = foldM mergeDef def defs
32
33mergeDef :: PatternSynDefn -> PatternSynDefn -> Maybe PatternSynDefn
34mergeDef (xs, p) (ys, q) = do
35  guard $ map getArgInfo xs == map getArgInfo ys
36  let ren = zip (map unArg xs) (map unArg ys)
37  (xs,) <$> merge ren p q
38  where
39    merge ren p@(VarP x) (VarP y)   = p <$ guard ((unBind x, unBind y) `elem` ren)
40    merge ren p@(LitP _ l) (LitP _ l') = p <$ guard (l == l')
41    merge ren p@(WildP _) (WildP _) = return p
42    merge ren (ConP i (AmbQ cs) ps) (ConP _ (AmbQ cs') qs) = do
43      guard $ map getArgInfo ps == map getArgInfo qs
44      ConP i (AmbQ $ List1.union cs cs') <$> zipWithM (mergeArg ren) ps qs
45    merge _ _ _ = empty
46
47    mergeArg ren p q = setNamedArg p <$> merge ren (namedArg p) (namedArg q)
48
49-- | Match an expression against a pattern synonym.
50matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [Arg Expr]
51matchPatternSyn = runMatch match
52  where
53    match (VarP x) e = unBind x ==> e
54    match (LitP _ l) (Lit _ l') = guard (l == l')
55    match (ConP _ (AmbQ cs) ps) e = do
56      Application (Con (AmbQ cs')) args <- return (appView e)
57      guard $ all (`elem` cs) cs'                       -- check all possible constructors appear in the synonym
58      guard $ map getArgInfo ps == map getArgInfo args  -- check that we agree on the hiding (TODO: too strict?)
59      zipWithM_ match (map namedArg ps) (map namedArg args)
60    match _ _ = empty
61
62-- | Match a pattern against a pattern synonym.
63matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
64matchPatternSynP = runMatch match
65  where
66    match (VarP x) q = unBind x ==> q
67    match (LitP _ l) (LitP _ l') = guard (l == l')
68    match (WildP _) (WildP _) = return ()
69    match (ConP _ (AmbQ cs) ps) (ConP _ (AmbQ cs') qs) = do
70      guard $ all (`elem` cs) cs'
71      guard $ map getArgInfo ps == map getArgInfo qs
72      zipWithM_ match (map namedArg ps) (map namedArg qs)
73    match _ _ = empty
74
75type Match e = WriterT (Map Name e) Maybe
76
77(==>) :: Name -> e -> Match e ()
78x ==> e = tell (Map.singleton x e)
79
80runMatch :: (Pattern' Void -> e -> Match e ()) -> PatternSynDefn -> e -> Maybe [Arg e]
81runMatch match (xs, pat) e = do
82  sub <- execWriterT (match pat e)
83  forM xs $ \ x -> (<$ x) <$> Map.lookup (unArg x) sub
84