{-# LANGUAGE GADTs #-}

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

module Agda.TypeChecking.Patterns.Internal where

import Control.Monad

import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce (reduce)
import Agda.TypeChecking.Substitute.DeBruijn

import Agda.Utils.Impossible

-- | Convert a term (from a dot pattern) to a DeBruijn pattern.

class TermToPattern a b where
  termToPattern :: a -> TCM b

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

instance TermToPattern a b => TermToPattern [a] [b] where
instance TermToPattern a b => TermToPattern (Arg a) (Arg b) where
instance TermToPattern a b => TermToPattern (Named c a) (Named c b) where

instance (DeBruijn (Pattern' a)) => TermToPattern Term (Pattern' a) where
  termToPattern :: Term -> TCM (Pattern' a)
termToPattern Term
t = (Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term)
-> (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm) Term
t TCMT IO Term -> (Term -> TCM (Pattern' a)) -> TCM (Pattern' a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Constructors.
    Con ConHead
c ConInfo
_ Elims
args -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo ([NamedArg (Pattern' a)] -> Pattern' a)
-> ([Arg (Pattern' a)] -> [NamedArg (Pattern' a)])
-> [Arg (Pattern' a)]
-> Pattern' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg (Pattern' a) -> NamedArg (Pattern' a))
-> [Arg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' a -> Named NamedName (Pattern' a))
-> Arg (Pattern' a) -> NamedArg (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed) ([Arg (Pattern' a)] -> Pattern' a)
-> TCMT IO [Arg (Pattern' a)] -> TCM (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term] -> TCMT IO [Arg (Pattern' a)]
forall a b. TermToPattern a b => a -> TCM b
termToPattern ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
args)
    Var Int
i []    -> Pattern' a -> TCM (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Int -> Pattern' a
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i
    Lit Literal
l       -> Pattern' a -> TCM (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Literal -> Pattern' a
forall a. Literal -> Pattern' a
litP Literal
l
    Term
t           -> Pattern' a -> TCM (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
t

dotPatternsToPatterns :: forall a. (DeBruijn (Pattern' a))
                      => Pattern' a -> TCM (Pattern' a)
dotPatternsToPatterns :: Pattern' a -> TCM (Pattern' a)
dotPatternsToPatterns = (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM Pattern' a -> TCM (Pattern' a)
dotToPat
  where
    dotToPat :: Pattern' a -> TCM (Pattern' a)
    dotToPat :: Pattern' a -> TCM (Pattern' a)
dotToPat = \case
      DotP PatternInfo
o Term
t -> Term -> TCM (Pattern' a)
forall a b. TermToPattern a b => a -> TCM b
termToPattern Term
t
      Pattern' a
p        -> Pattern' a -> TCM (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p