-- | Tools to manipulate patterns in abstract syntax
--   in the TCM (type checking monad).

module Agda.TypeChecking.Patterns.Abstract where

import Control.Monad.Except

import qualified Data.List as List
import Data.Functor
import Data.Void

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Concrete (FieldAssignment')
import Agda.Syntax.Common
import Agda.Syntax.Info as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Warnings (raiseWarningsOnUsage)

import Agda.Utils.Impossible

-- | Expand literal integer pattern into suc/zero constructor patterns.
--
expandLitPattern
  :: (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m)
  => A.Pattern -> m A.Pattern
expandLitPattern :: forall (m :: * -> *).
(MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
Pattern -> m Pattern
expandLitPattern = \case
  A.LitP PatInfo
info (LitNat Integer
n)
    | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     -> m Pattern
forall {a}. m a
negLit -- Andreas, issue #2365, negative literals not yet supported.
    | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
20    -> m Pattern
forall {a}. m a
tooBig
    | Bool
otherwise -> do
      Con ConHead
z ConInfo
_ Elims
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
      Con ConHead
s ConInfo
_ Elims
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc
      let r :: Range
r     = PatInfo -> Range
forall a. HasRange a => a -> Range
getRange PatInfo
info
      let zero :: Pattern
zero  = ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
cinfo (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange Range
r (QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
z) []
          suc :: Pattern -> Pattern
suc Pattern
p = ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
cinfo (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange Range
r (QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
s) [Pattern -> NamedArg Pattern
forall a. a -> NamedArg a
defaultNamedArg Pattern
p]
          cinfo :: ConPatInfo
cinfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
A.ConPatInfo ConInfo
ConOCon PatInfo
info ConPatLazy
ConPatEager
      Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ ((Pattern -> Pattern) -> Pattern -> Pattern)
-> Pattern -> [Pattern -> Pattern] -> Pattern
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
($) Pattern
zero ([Pattern -> Pattern] -> Pattern)
-> [Pattern -> Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ Integer -> (Pattern -> Pattern) -> [Pattern -> Pattern]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate Integer
n Pattern -> Pattern
suc
  Pattern
p -> Pattern -> m Pattern
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p

  where
    tooBig :: m a
tooBig = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Matching on natural number literals is done by expanding " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"the literal to the corresponding constructor pattern, so " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"you probably don't want to do it this way."
    negLit :: m a
negLit = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
      [Char]
"Negative literals are not supported in patterns"


-- | Expand away (deeply) all pattern synonyms in a pattern.

-- Unfortunately, the more general type signature
--
--   expandPatternSynonyms :: forall a p . APatternLike a p => p -> TCM p
--
-- is rejected by GHC 7.10
--
--   Could not deduce (APatternLike A.Expr p)
--     arising from a use of ‘postTraverseAPatternM’
--
-- I am mystified (Andreas, 2017-07-27)

-- expandPatternSynonyms :: forall a p . APatternLike a p => p -> TCM p

-- As a workaround, we define this function only for a = A.Exp, p = A.Pattern'
-- and keep the type class ExpandPatternSynonyms (which would otherwise be superfluous).

expandPatternSynonyms' :: forall e. A.Pattern' e -> TCM (A.Pattern' e)
expandPatternSynonyms' :: forall e. Pattern' e -> TCM (Pattern' e)
expandPatternSynonyms' = (Pattern' (ADotT (Pattern' e))
 -> TCMT IO (Pattern' (ADotT (Pattern' e))))
-> Pattern' e -> TCMT IO (Pattern' e)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
postTraverseAPatternM ((Pattern' (ADotT (Pattern' e))
  -> TCMT IO (Pattern' (ADotT (Pattern' e))))
 -> Pattern' e -> TCMT IO (Pattern' e))
-> (Pattern' (ADotT (Pattern' e))
    -> TCMT IO (Pattern' (ADotT (Pattern' e))))
-> Pattern' e
-> TCMT IO (Pattern' e)
forall a b. (a -> b) -> a -> b
$ \case

  A.PatternSynP PatInfo
i AmbiguousQName
x NAPs (ADotT (Pattern' e))
as -> PatInfo
-> TCMT IO (Pattern' (ADotT (Pattern' e)))
-> TCMT IO (Pattern' (ADotT (Pattern' e)))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange PatInfo
i (TCMT IO (Pattern' (ADotT (Pattern' e)))
 -> TCMT IO (Pattern' (ADotT (Pattern' e))))
-> TCMT IO (Pattern' (ADotT (Pattern' e)))
-> TCMT IO (Pattern' (ADotT (Pattern' e)))
forall a b. (a -> b) -> a -> b
$ do
    ([WithHiding Name]
ns, Pattern' Void
p) <- KillRangeT PatternSynDefn
forall a. KillRange a => KillRangeT a
killRange KillRangeT PatternSynDefn
-> TCMT IO PatternSynDefn -> TCMT IO PatternSynDefn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AmbiguousQName -> TCMT IO PatternSynDefn
lookupPatternSyn AmbiguousQName
x

    -- Andreas, 2020-02-11, issue #3734
    -- If lookup of ambiguous pattern synonym was successful,
    -- we are justified to complain if one of the definitions
    -- involved in the resolution is tagged with a warning.
    -- This is less than optimal, since we do not rule out
    -- the invalid alternatives by typing, but we cannot do
    -- better here.
    (QName -> TCMT IO ()) -> NonEmpty QName -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCMT IO ()
forall (m :: * -> *).
(MonadWarning m, ReadTCState m) =>
QName -> m ()
raiseWarningsOnUsage (NonEmpty QName -> TCMT IO ()) -> NonEmpty QName -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> NonEmpty QName
A.unAmbQ AmbiguousQName
x

    -- Must expand arguments before instantiating otherwise pattern
    -- synonyms could get into dot patterns (which is __IMPOSSIBLE__).
    Pattern' e
p <- Pattern' e -> TCMT IO (Pattern' e)
forall e. Pattern' e -> TCM (Pattern' e)
expandPatternSynonyms' (Pattern' Void -> Pattern' e
forall (f :: * -> *) a. Functor f => f Void -> f a
vacuous Pattern' Void
p :: A.Pattern' e)

    [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"scope.patsyn" VerboseLevel
80 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"calling insertImplicitPatSynArgs"
      , TCMT IO Doc
"- patsyn parameters: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([WithHiding Name] -> [Char])
-> [WithHiding Name]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [WithHiding Name] -> [Char]
forall a. Show a => a -> [Char]
show) (KillRangeT [WithHiding Name]
forall a. KillRange a => KillRangeT a
killRange [WithHiding Name]
ns)
      , TCMT IO Doc
"- patsyn arguments:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Arg (Named NamedName ())] -> [Char])
-> [Arg (Named NamedName ())]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg (Named NamedName ())] -> [Char]
forall a. Show a => a -> [Char]
show) ((Arg (Named NamedName (Pattern' e)) -> Arg (Named NamedName ()))
-> [Arg (Named NamedName (Pattern' e))]
-> [Arg (Named NamedName ())]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (Pattern' e) -> Named NamedName ())
-> Arg (Named NamedName (Pattern' e)) -> Arg (Named NamedName ())
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' e) -> Named NamedName ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void) [Arg (Named NamedName (Pattern' e))]
NAPs (ADotT (Pattern' e))
as)
      ]
    case (Hiding -> Range -> Pattern' e)
-> Range
-> [WithHiding Name]
-> [Arg (Named NamedName (Pattern' e))]
-> Maybe ([(Name, Pattern' e)], [WithHiding Name])
forall a.
HasRange a =>
(Hiding -> Range -> a)
-> Range
-> [WithHiding Name]
-> [NamedArg a]
-> Maybe ([(Name, a)], [WithHiding Name])
A.insertImplicitPatSynArgs (\ Hiding
_h Range
r -> PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
A.WildP (Range -> PatInfo
PatRange Range
r)) (AmbiguousQName -> Range
forall a. HasRange a => a -> Range
getRange AmbiguousQName
x) [WithHiding Name]
ns [Arg (Named NamedName (Pattern' e))]
NAPs (ADotT (Pattern' e))
as of
      Maybe ([(Name, Pattern' e)], [WithHiding Name])
Nothing       -> TypeError -> TCMT IO (Pattern' e)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Pattern' e))
-> TypeError -> TCMT IO (Pattern' e)
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> TypeError
BadArgumentsToPatternSynonym AmbiguousQName
x
      Just ([(Name, Pattern' e)]
_, WithHiding Name
_:[WithHiding Name]
_) -> TypeError -> TCMT IO (Pattern' e)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Pattern' e))
-> TypeError -> TCMT IO (Pattern' e)
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> TypeError
TooFewArgumentsToPatternSynonym AmbiguousQName
x
      Just ([(Name, Pattern' e)]
s, [])  -> do
        let subE :: p -> a
subE p
_ = a
forall a. HasCallStack => a
__IMPOSSIBLE__   -- No dot patterns in p
        Pattern' e -> TCMT IO (Pattern' e)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' e -> TCMT IO (Pattern' e))
-> Pattern' e -> TCMT IO (Pattern' e)
forall a b. (a -> b) -> a -> b
$ Range -> Pattern' e -> Pattern' e
forall a. SetRange a => Range -> a -> a
setRange (PatInfo -> Range
forall a. HasRange a => a -> Range
getRange PatInfo
i) (Pattern' e -> Pattern' e) -> Pattern' e -> Pattern' e
forall a b. (a -> b) -> a -> b
$ (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
forall e.
(e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
substPattern' e -> e
forall {p} {a}. p -> a
subE [(Name, Pattern' e)]
s Pattern' e
p

  Pattern' (ADotT (Pattern' e))
p -> Pattern' e -> TCMT IO (Pattern' e)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' e
Pattern' (ADotT (Pattern' e))
p

class ExpandPatternSynonyms a where
  expandPatternSynonyms :: a -> TCM a

  default expandPatternSynonyms
    :: (Traversable f, ExpandPatternSynonyms b, f b ~ a) => a -> TCM a
  expandPatternSynonyms = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse b -> TCMT IO b
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms

instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a)
instance ExpandPatternSynonyms a => ExpandPatternSynonyms [a]
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)
instance ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

instance ExpandPatternSynonyms (A.Pattern' e) where
  expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e)
expandPatternSynonyms = Pattern' e -> TCM (Pattern' e)
forall e. Pattern' e -> TCM (Pattern' e)
expandPatternSynonyms'