-- | 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) = 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
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo [Arg Name]
xs forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo [Arg Name]
ys
  let ren :: [(Name, Name)]
ren = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
xs) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
ys)
  ([Arg Name]
xs,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((BindName -> Name
unBind BindName
x, BindName -> Name
unBind BindName
y) 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l')
    merge t (Name, Name)
ren p :: Pattern' e
p@(WildP PatInfo
_) (WildP PatInfo
_) = 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
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NAPs e
ps forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NAPs e
qs
      forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i (List1 QName -> AmbiguousQName
AmbQ forall a b. (a -> b) -> a -> b
$ forall a. Eq a => List1 a -> List1 a -> List1 a
List1.union List1 QName
cs List1 QName
cs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_ = 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 = forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' e)
p 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 (forall a. NamedArg a -> a
namedArg NamedArg (Pattern' e)
p) (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 = forall e.
(Pattern' Void -> e -> Match e ())
-> PatternSynDefn -> e -> Maybe [Arg e]
runMatch forall {e}. Pattern' e -> Expr -> WriterT (Map Name Expr) Maybe ()
match
  where
    match :: Pattern' e -> Expr -> WriterT (Map Name Expr) Maybe ()
match (VarP BindName
x) Expr
e = BindName -> Name
unBind BindName
x forall e. Name -> e -> Match e ()
==> Expr
e
    match (LitP PatInfo
_ Literal
l) (Lit ExprInfo
_ Literal
l') = forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Literal
l 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 <- forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> AppView' Expr
appView Expr
e)
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NAPs e
ps forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo [NamedArg Expr]
args  -- check that we agree on the hiding (TODO: too strict?)
      forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Pattern' e -> Expr -> WriterT (Map Name Expr) Maybe ()
match (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs e
ps) (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Expr]
args)
    match Pattern' e
_ 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 = forall e.
(Pattern' Void -> e -> Match e ())
-> PatternSynDefn -> e -> Maybe [Arg e]
runMatch 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 forall e. Name -> e -> Match e ()
==> Pattern' e
q
    match (LitP PatInfo
_ Literal
l) (LitP PatInfo
_ Literal
l') = forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l')
    match (WildP PatInfo
_) (WildP PatInfo
_) = 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
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` List1 QName
cs) List1 QName
cs'
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NAPs e
ps forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NAPs e
qs
      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 (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs e
ps) (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs e
qs)
    match Pattern' e
_ Pattern' e
_ = 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (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 <- forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (Pattern' Void -> e -> Match e ()
match Pattern' Void
pat e
e)
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Arg Name]
xs forall a b. (a -> b) -> a -> b
$ \ Arg Name
x -> (forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Name
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall e. Arg e -> e
unArg Arg Name
x) Map Name e
sub