-- | 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.Writer hiding (forM)

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

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


-- | 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 :: NonEmpty PatternSynDefn -> Maybe PatternSynDefn
mergePatternSynDefs :: NonEmpty 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 ((Name, Name) -> t (Name, Name) -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (BindName -> Name
unBind BindName
x, BindName -> Name
unBind BindName
y) t (Name, Name)
ren)
    merge t (Name, Name)
ren p :: Pattern' e
p@(LitP Literal
l) (LitP 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 NonEmpty QName
cs) NAPs e
ps) (ConP ConPatInfo
_ (AmbQ NonEmpty 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 (NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> NonEmpty QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> NonEmpty QName -> NonEmpty QName
forall a. Eq a => NonEmpty a -> NonEmpty a -> NonEmpty a
unionNe NonEmpty QName
cs NonEmpty 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)

    unionNe :: NonEmpty a -> NonEmpty a -> NonEmpty a
unionNe NonEmpty a
xs NonEmpty a
ys = [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
NonEmpty.fromList ([a] -> NonEmpty a) -> [a] -> NonEmpty a
forall a b. (a -> b) -> a -> b
$ NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty a
xs [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`union` NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty a
ys

-- | 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 Literal
l) (Lit 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 NonEmpty QName
cs) NAPs e
ps) Expr
e = do
      Application (Con (AmbQ NonEmpty 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
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
cs' [QName] -> [QName] -> [QName]
forall a. Eq a => [a] -> [a] -> [a]
\\ NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty 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 :: 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 Literal
l) (LitP 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 NonEmpty QName
cs) NAPs e
ps) (ConP ConPatInfo
_ (AmbQ NonEmpty 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
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty QName
cs' [QName] -> [QName] -> [QName]
forall a. Eq a => [a] -> [a] -> [a]
\\ NonEmpty QName -> [QName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty 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 ==> :: Name -> e -> Match e ()
==> e
e = Map Name e -> Match e ()
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 :: (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