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