    -- | Pattern synonym utilities: folding pattern synonym definitions for
    --   printing and merging pattern synonym definitions to handle overloaded
    --   pattern synonyms.
    module Agda.Syntax.Abstract.PatternSynonyms
      ( matchPatternSyn
      , matchPatternSynP
      , mergePatternSynDefs
      ) where

    import Control.Applicative  ( Alternative(empty) )
    import Control.Monad        ( foldM, guard, zipWithM, zipWithM_ )
    import Control.Monad.Writer ( MonadWriter(..), WriterT, execWriterT )

    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Traversable (forM)
    import Data.Void

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract
    import Agda.Syntax.Abstract.Views

    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1

    -- | Merge a list of pattern synonym definitions. Fails unless all definitions
    --   have the same shape (i.e. equal up to renaming of variables and constructor
    --   names).
    mergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn
    mergePatternSynDefs :: List1 PatternSynDefn -> Maybe PatternSynDefn
    mergePatternSynDefs (PatternSynDefn
    def :| [PatternSynDefn]
    defs) = (PatternSynDefn -> PatternSynDefn -> Maybe PatternSynDefn)
    -> PatternSynDefn -> [PatternSynDefn] -> Maybe PatternSynDefn
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM PatternSynDefn -> PatternSynDefn -> Maybe PatternSynDefn
    mergeDef PatternSynDefn
    def [PatternSynDefn]
    defs

    mergeDef :: PatternSynDefn -> PatternSynDefn -> Maybe PatternSynDefn
    mergeDef :: PatternSynDefn -> PatternSynDefn -> Maybe PatternSynDefn
    mergeDef ([Arg Name]
    xs, Pattern' Void
    p) ([Arg Name]
    ys, Pattern' Void
    q) = do
      Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ (Arg Name -> ArgInfo) -> [Arg Name] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo [Arg Name]
    xs [ArgInfo] -> [ArgInfo] -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Arg Name -> ArgInfo) -> [Arg Name] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo [Arg Name]
    ys
      let ren :: [(Name, Name)]
    ren = [Name] -> [Name] -> [(Name, Name)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((Arg Name -> Name) -> [Arg Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> Name
    forall e. Arg e -> e
    unArg [Arg Name]
    xs) ((Arg Name -> Name) -> [Arg Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> Name
    forall e. Arg e -> e
    unArg [Arg Name]
    ys)
      ([Arg Name]
    xs,) (Pattern' Void -> PatternSynDefn)
    -> Maybe (Pattern' Void) -> Maybe PatternSynDefn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Name, Name)]
    -> Pattern' Void -> Pattern' Void -> Maybe (Pattern' Void)
    forall {f :: * -> *} {t :: * -> *} {e} {e}.
    (Alternative f, Foldable t, Monad f) =>
    t (Name, Name) -> Pattern' e -> Pattern' e -> f (Pattern' e)
    merge [(Name, Name)]
    ren Pattern' Void
    p Pattern' Void
    q
      where
        merge :: t (Name, Name) -> Pattern' e -> Pattern' e -> f (Pattern' e)
    merge t (Name, Name)
    ren p :: Pattern' e
    p@(VarP BindName
    x) (VarP BindName
    y)   = Pattern' e
    p Pattern' e -> f () -> f (Pattern' e)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> f ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ((BindName -> Name
    unBind BindName
    x, BindName -> Name
    unBind BindName
    y) (Name, Name) -> t (Name, Name) -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` t (Name, Name)
    ren)
        merge t (Name, Name)
    ren p :: Pattern' e
    p@(LitP PatInfo
    _ Literal
    l) (LitP PatInfo
    _ Literal
    l') = Pattern' e
    p Pattern' e -> f () -> f (Pattern' e)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> f ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l')
        merge t (Name, Name)
    ren p :: Pattern' e
    p@(WildP PatInfo
    _) (WildP PatInfo
    _) = Pattern' e -> f (Pattern' e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' e
    p
        merge t (Name, Name)
    ren (ConP ConPatInfo
    i (AmbQ List1 QName
    cs) NAPs e
    ps) (ConP ConPatInfo
    _ (AmbQ List1 QName
    cs') NAPs e
    qs) = do
          Bool -> f ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> f ()) -> Bool -> f ()
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' e) -> ArgInfo) -> NAPs e -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NAPs e
    ps [ArgInfo] -> [ArgInfo] -> Bool
    forall a. Eq a => a -> a -> Bool
    == (NamedArg (Pattern' e) -> ArgInfo) -> NAPs e -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NAPs e
    qs
          ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    ConP ConPatInfo
    i (List1 QName -> AmbiguousQName
    AmbQ (List1 QName -> AmbiguousQName) -> List1 QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ List1 QName -> List1 QName -> List1 QName
    forall a. Eq a => List1 a -> List1 a -> List1 a
    List1.union List1 QName
    cs List1 QName
    cs') (NAPs e -> Pattern' e) -> f (NAPs e) -> f (Pattern' e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamedArg (Pattern' e)
     -> NamedArg (Pattern' e) -> f (NamedArg (Pattern' e)))
    -> NAPs e -> NAPs e -> f (NAPs e)
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (t (Name, Name)
    -> NamedArg (Pattern' e)
    -> NamedArg (Pattern' e)
    -> f (NamedArg (Pattern' e))
    mergeArg t (Name, Name)
    ren) NAPs e
    ps NAPs e
    qs
        merge t (Name, Name)
    _ Pattern' e
    _ Pattern' e
    _ = f (Pattern' e)
    forall (f :: * -> *) a. Alternative f => f a
    empty

        mergeArg :: t (Name, Name)
    -> NamedArg (Pattern' e)
    -> NamedArg (Pattern' e)
    -> f (NamedArg (Pattern' e))
    mergeArg t (Name, Name)
    ren NamedArg (Pattern' e)
    p NamedArg (Pattern' e)
    q = NamedArg (Pattern' e) -> Pattern' e -> NamedArg (Pattern' e)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' e)
    p (Pattern' e -> NamedArg (Pattern' e))
    -> f (Pattern' e) -> f (NamedArg (Pattern' e))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t (Name, Name) -> Pattern' e -> Pattern' e -> f (Pattern' e)
    merge t (Name, Name)
    ren (NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' e)
    p) (NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' e)
    q)

    -- | Match an expression against a pattern synonym.
    matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [Arg Expr]
    matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [Arg Expr]
    matchPatternSyn = (Pattern' Void -> Expr -> Match Expr ())
    -> PatternSynDefn -> Expr -> Maybe [Arg Expr]
    forall e.
    (Pattern' Void -> e -> Match e ())
    -> PatternSynDefn -> e -> Maybe [Arg e]
    runMatch Pattern' Void -> Expr -> Match Expr ()
    forall {e}. Pattern' e -> Expr -> Match Expr ()
    match
      where
        match :: Pattern' e -> Expr -> Match Expr ()
    match (VarP BindName
    x) Expr
    e = BindName -> Name
    unBind BindName
    x Name -> Expr -> Match Expr ()
    forall e. Name -> e -> Match e ()
    ==> Expr
    e
        match (LitP PatInfo
    _ Literal
    l) (Lit ExprInfo
    _ Literal
    l') = Bool -> Match Expr ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l')
        match (ConP ConPatInfo
    _ (AmbQ List1 QName
    cs) NAPs e
    ps) Expr
    e = do
          Application (Con (AmbQ List1 QName
    cs')) [NamedArg Expr]
    args <- AppView' Expr -> WriterT (Map Name Expr) Maybe (AppView' Expr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> AppView' Expr
    appView Expr
    e)
          Bool -> Match Expr ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Match Expr ()) -> Bool -> Match Expr ()
    forall a b. (a -> b) -> a -> b
    $ (QName -> Bool) -> List1 QName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (QName -> List1 QName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` List1 QName
    cs) List1 QName
    cs'                       -- check all possible constructors appear in the synonym
          Bool -> Match Expr ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Match Expr ()) -> Bool -> Match Expr ()
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' e) -> ArgInfo) -> NAPs e -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NAPs e
    ps [ArgInfo] -> [ArgInfo] -> Bool
    forall a. Eq a => a -> a -> Bool
    == (NamedArg Expr -> ArgInfo) -> [NamedArg Expr] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo [NamedArg Expr]
    args  -- check that we agree on the hiding (TODO: too strict?)
          (Pattern' e -> Expr -> Match Expr ())
    -> [Pattern' e] -> [Expr] -> Match Expr ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ Pattern' e -> Expr -> Match Expr ()
    match ((NamedArg (Pattern' e) -> Pattern' e) -> NAPs e -> [Pattern' e]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NAPs e
    ps) ((NamedArg Expr -> Expr) -> [NamedArg Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> Expr
    forall a. NamedArg a -> a
    namedArg [NamedArg Expr]
    args)
        match Pattern' e
    _ Expr
    _ = Match Expr ()
    forall (f :: * -> *) a. Alternative f => f a
    empty

    -- | Match a pattern against a pattern synonym.
    matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
    matchPatternSynP :: forall e. PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
    matchPatternSynP = (Pattern' Void -> Pattern' e -> Match (Pattern' e) ())
    -> PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
    forall e.
    (Pattern' Void -> e -> Match e ())
    -> PatternSynDefn -> e -> Maybe [Arg e]
    runMatch Pattern' Void -> Pattern' e -> Match (Pattern' e) ()
    forall {e} {e}.
    Pattern' e
    -> Pattern' e -> WriterT (Map Name (Pattern' e)) Maybe ()
    match
      where
        match :: Pattern' e
    -> Pattern' e -> WriterT (Map Name (Pattern' e)) Maybe ()
    match (VarP BindName
    x) Pattern' e
    q = BindName -> Name
    unBind BindName
    x Name -> Pattern' e -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall e. Name -> e -> Match e ()
    ==> Pattern' e
    q
        match (LitP PatInfo
    _ Literal
    l) (LitP PatInfo
    _ Literal
    l') = Bool -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l')
        match (WildP PatInfo
    _) (WildP PatInfo
    _) = () -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        match (ConP ConPatInfo
    _ (AmbQ List1 QName
    cs) NAPs e
    ps) (ConP ConPatInfo
    _ (AmbQ List1 QName
    cs') NAPs e
    qs) = do
          Bool -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> WriterT (Map Name (Pattern' e)) Maybe ())
    -> Bool -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall a b. (a -> b) -> a -> b
    $ (QName -> Bool) -> List1 QName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (QName -> List1 QName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` List1 QName
    cs) List1 QName
    cs'
          Bool -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> WriterT (Map Name (Pattern' e)) Maybe ())
    -> Bool -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' e) -> ArgInfo) -> NAPs e -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NAPs e
    ps [ArgInfo] -> [ArgInfo] -> Bool
    forall a. Eq a => a -> a -> Bool
    == (NamedArg (Pattern' e) -> ArgInfo) -> NAPs e -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NAPs e
    qs
          (Pattern' e
     -> Pattern' e -> WriterT (Map Name (Pattern' e)) Maybe ())
    -> [Pattern' e]
    -> [Pattern' e]
    -> WriterT (Map Name (Pattern' e)) Maybe ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ Pattern' e
    -> Pattern' e -> WriterT (Map Name (Pattern' e)) Maybe ()
    match ((NamedArg (Pattern' e) -> Pattern' e) -> NAPs e -> [Pattern' e]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NAPs e
    ps) ((NamedArg (Pattern' e) -> Pattern' e) -> NAPs e -> [Pattern' e]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NAPs e
    qs)
        match Pattern' e
    _ Pattern' e
    _ = WriterT (Map Name (Pattern' e)) Maybe ()
    forall (f :: * -> *) a. Alternative f => f a
    empty

    type Match e = WriterT (Map Name e) Maybe

    (==>) :: Name -> e -> Match e ()
    Name
    x ==> :: forall e. Name -> e -> Match e ()
    ==> e
    e = Map Name e -> WriterT (Map Name e) Maybe ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Name -> e -> Map Name e
    forall k a. k -> a -> Map k a
    Map.singleton Name
    x e
    e)

    runMatch :: (Pattern' Void -> e -> Match e ()) -> PatternSynDefn -> e -> Maybe [Arg e]
    runMatch :: forall e.
    (Pattern' Void -> e -> Match e ())
    -> PatternSynDefn -> e -> Maybe [Arg e]
    runMatch Pattern' Void -> e -> Match e ()
    match ([Arg Name]
    xs, Pattern' Void
    pat) e
    e = do
      Map Name e
    sub <- Match e () -> Maybe (Map Name e)
    forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
    execWriterT (Pattern' Void -> e -> Match e ()
    match Pattern' Void
    pat e
    e)
      [Arg Name] -> (Arg Name -> Maybe (Arg e)) -> Maybe [Arg e]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Arg Name]
    xs ((Arg Name -> Maybe (Arg e)) -> Maybe [Arg e])
    -> (Arg Name -> Maybe (Arg e)) -> Maybe [Arg e]
    forall a b. (a -> b) -> a -> b
    $ \ Arg Name
    x -> (e -> Arg Name -> Arg e
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Name
    x) (e -> Arg e) -> Maybe e -> Maybe (Arg e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> Map Name e -> Maybe e
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Arg Name -> Name
    forall e. Arg e -> e
    unArg Arg Name
    x) Map Name e
    sub