{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 ([WithHiding Name]
xs, Pattern' Void
p) ([WithHiding 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
$ (WithHiding Name -> Hiding) -> [WithHiding Name] -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> Hiding
forall a. WithHiding a -> Hiding
whHiding [WithHiding Name]
xs [Hiding] -> [Hiding] -> Bool
forall a. Eq a => a -> a -> Bool
== (WithHiding Name -> Hiding) -> [WithHiding Name] -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> Hiding
forall a. WithHiding a -> Hiding
whHiding [WithHiding Name]
ys
  let ren :: [(Name, Name)]
ren = [Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((WithHiding Name -> Name) -> [WithHiding Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> Name
forall a. WithHiding a -> a
whThing [WithHiding Name]
xs) ((WithHiding Name -> Name) -> [WithHiding Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> Name
forall a. WithHiding a -> a
whThing [WithHiding Name]
ys)
  ([WithHiding 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 a b. a -> f b -> f a
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 a. Eq a => a -> t a -> 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 a b. a -> f b -> f a
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 a. a -> f a
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 a. f a
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 [WithHiding Expr]
matchPatternSyn :: PatternSynDefn -> Expr -> Maybe [WithHiding Expr]
matchPatternSyn = (Pattern' Void -> Expr -> Match Expr ())
-> PatternSynDefn -> Expr -> Maybe [WithHiding Expr]
forall e.
(Pattern' Void -> e -> Match e ())
-> PatternSynDefn -> e -> Maybe [WithHiding 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 cs')) args <- AppView -> WriterT (Map Name Expr) Maybe AppView
forall a. a -> WriterT (Map Name Expr) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> AppView
appView Expr
e)
      guard $ all (`elem` cs) cs'                       -- check all possible constructors appear in the synonym
      guard $ map getArgInfo ps == map getArgInfo args  -- check that we agree on the hiding (TODO: too strict?)
      zipWithM_ match (map namedArg ps) (map namedArg args)
    match Pattern' e
_ Expr
_ = Match Expr ()
forall a. WriterT (Map Name Expr) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Match a pattern against a pattern synonym.
matchPatternSynP :: PatternSynDefn -> Pattern' e -> Maybe [WithHiding (Pattern' e)]
matchPatternSynP :: forall e.
PatternSynDefn -> Pattern' e -> Maybe [WithHiding (Pattern' e)]
matchPatternSynP = (Pattern' Void -> Pattern' e -> Match (Pattern' e) ())
-> PatternSynDefn -> Pattern' e -> Maybe [WithHiding (Pattern' e)]
forall e.
(Pattern' Void -> e -> Match e ())
-> PatternSynDefn -> e -> Maybe [WithHiding 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 a. a -> WriterT (Map Name (Pattern' e)) Maybe a
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 a. Eq a => a -> NonEmpty a -> 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 a. WriterT (Map Name (Pattern' e)) Maybe a
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 [WithHiding e]
runMatch :: forall e.
(Pattern' Void -> e -> Match e ())
-> PatternSynDefn -> e -> Maybe [WithHiding e]
runMatch Pattern' Void -> e -> Match e ()
match ([WithHiding Name]
xs, Pattern' Void
pat) e
e = do
  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)
  forM xs $ \ WithHiding Name
x -> (e -> WithHiding Name -> WithHiding e
forall a b. a -> WithHiding b -> WithHiding a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ WithHiding Name
x) (e -> WithHiding e) -> Maybe e -> Maybe (WithHiding 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 (WithHiding Name -> Name
forall a. WithHiding a -> a
whThing WithHiding Name
x) Map Name e
sub