{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.Syntax.Internal.Pattern where

import Control.Monad       ( (>=>), forM )
import Control.DeepSeq

import GHC.Generics (Generic)

import Data.Text.Short (ShortText)
import Data.Monoid
import Data.Maybe
import Data.List qualified as List

import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Position
import Mikan.Syntax.Literal
import Mikan.Syntax.Common
import Mikan.Syntax.Internal.Term

import Mikan.Utils.List
import Mikan.Utils.Permutation
import Mikan.Utils.Size (size)
import Mikan.Utils.Impossible

-- | Pattern variables.
type PatVarName = ArgName

patVarNameToString :: PatVarName -> ShortText
patVarNameToString :: PatVarName -> PatVarName
patVarNameToString = PatVarName -> PatVarName
argNameToString

nameToPatVarName :: Name -> PatVarName
nameToPatVarName :: Name -> PatVarName
nameToPatVarName = Name -> PatVarName
nameToArgName

data PatternInfo = PatternInfo
  { PatternInfo -> PatOrigin
patOrigin :: PatOrigin
  , PatternInfo -> [Name]
patAsNames :: [Name]
  } deriving (Int -> PatternInfo -> ShowS
[PatternInfo] -> ShowS
PatternInfo -> String
(Int -> PatternInfo -> ShowS)
-> (PatternInfo -> String)
-> ([PatternInfo] -> ShowS)
-> Show PatternInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PatternInfo -> ShowS
showsPrec :: Int -> PatternInfo -> ShowS
$cshow :: PatternInfo -> String
show :: PatternInfo -> String
$cshowList :: [PatternInfo] -> ShowS
showList :: [PatternInfo] -> ShowS
Show, PatternInfo -> PatternInfo -> Bool
(PatternInfo -> PatternInfo -> Bool)
-> (PatternInfo -> PatternInfo -> Bool) -> Eq PatternInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PatternInfo -> PatternInfo -> Bool
== :: PatternInfo -> PatternInfo -> Bool
$c/= :: PatternInfo -> PatternInfo -> Bool
/= :: PatternInfo -> PatternInfo -> Bool
Eq, (forall x. PatternInfo -> Rep PatternInfo x)
-> (forall x. Rep PatternInfo x -> PatternInfo)
-> Generic PatternInfo
forall x. Rep PatternInfo x -> PatternInfo
forall x. PatternInfo -> Rep PatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PatternInfo -> Rep PatternInfo x
from :: forall x. PatternInfo -> Rep PatternInfo x
$cto :: forall x. Rep PatternInfo x -> PatternInfo
to :: forall x. Rep PatternInfo x -> PatternInfo
Generic)

defaultPatternInfo :: PatternInfo
defaultPatternInfo :: PatternInfo
defaultPatternInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSystem []

-- | Origin of the pattern: what did the user write in this position?
data PatOrigin
  = PatOSystem         -- ^ Pattern inserted by the system
  | PatOSplit          -- ^ Pattern generated by case split
  | PatOSplitArg ArgName -- ^ Argument to pattern generated by case split
  | PatOVar Name       -- ^ User wrote a variable pattern
  | PatODot            -- ^ User wrote a dot pattern
  | PatOWild           -- ^ User wrote a wildcard pattern
  | PatOCon            -- ^ User wrote a constructor pattern
  | PatORec            -- ^ User wrote a record pattern
  | PatOLit            -- ^ User wrote a literal pattern
  | PatOAbsurd         -- ^ User wrote an absurd pattern
  deriving (Int -> PatOrigin -> ShowS
[PatOrigin] -> ShowS
PatOrigin -> String
(Int -> PatOrigin -> ShowS)
-> (PatOrigin -> String)
-> ([PatOrigin] -> ShowS)
-> Show PatOrigin
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PatOrigin -> ShowS
showsPrec :: Int -> PatOrigin -> ShowS
$cshow :: PatOrigin -> String
show :: PatOrigin -> String
$cshowList :: [PatOrigin] -> ShowS
showList :: [PatOrigin] -> ShowS
Show, PatOrigin -> PatOrigin -> Bool
(PatOrigin -> PatOrigin -> Bool)
-> (PatOrigin -> PatOrigin -> Bool) -> Eq PatOrigin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PatOrigin -> PatOrigin -> Bool
== :: PatOrigin -> PatOrigin -> Bool
$c/= :: PatOrigin -> PatOrigin -> Bool
/= :: PatOrigin -> PatOrigin -> Bool
Eq, (forall x. PatOrigin -> Rep PatOrigin x)
-> (forall x. Rep PatOrigin x -> PatOrigin) -> Generic PatOrigin
forall x. Rep PatOrigin x -> PatOrigin
forall x. PatOrigin -> Rep PatOrigin x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PatOrigin -> Rep PatOrigin x
from :: forall x. PatOrigin -> Rep PatOrigin x
$cto :: forall x. Rep PatOrigin x -> PatOrigin
to :: forall x. Rep PatOrigin x -> PatOrigin
Generic)

-- | Patterns are variables, constructors, or wildcards.
--   @QName@ is used in @ConP@ rather than @Name@ since
--     a constructor might come from a particular namespace.
--     This also meshes well with the fact that values (i.e.
--     the arguments we are matching with) use @QName@.
--
data Pattern' x
  = VarP PatternInfo x
    -- ^ @x@
  | DotP PatternInfo Term
    -- ^ @.t@
  | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
    -- ^ @c ps@
    --   The subpatterns do not contain any projection copatterns.
  | LitP PatternInfo Literal
    -- ^ E.g. @5@, @"hello"@.
  | ProjP ProjOrigin QName
    -- ^ Projection copattern.  Can only appear by itself.
  | IApplyP PatternInfo Term Term x
    -- ^ Path elimination pattern, like @VarP@ but keeps track of endpoints.
  | DefP PatternInfo QName [NamedArg (Pattern' x)]
    -- ^ Used for HITs, the QName should be the one from primHComp.
  | MaskP (Pattern' x)
    -- ^ Only used during termination checking of clause right-hand
    -- sides: a pattern guarded by 'MaskP' is not usable for structural
    -- recursion.
    --
    -- 'MaskP' should be '__IMPOSSIBLE__' everywhere outside of the
    -- termination checker and the structural functions on patterns
    -- (e.g. applySubst).
  deriving (Int -> Pattern' x -> ShowS
[Pattern' x] -> ShowS
Pattern' x -> String
(Int -> Pattern' x -> ShowS)
-> (Pattern' x -> String)
-> ([Pattern' x] -> ShowS)
-> Show (Pattern' x)
forall x. Show x => Int -> Pattern' x -> ShowS
forall x. Show x => [Pattern' x] -> ShowS
forall x. Show x => Pattern' x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> Pattern' x -> ShowS
showsPrec :: Int -> Pattern' x -> ShowS
$cshow :: forall x. Show x => Pattern' x -> String
show :: Pattern' x -> String
$cshowList :: forall x. Show x => [Pattern' x] -> ShowS
showList :: [Pattern' x] -> ShowS
Show, (forall a b. (a -> b) -> Pattern' a -> Pattern' b)
-> (forall a b. a -> Pattern' b -> Pattern' a) -> Functor Pattern'
forall a b. a -> Pattern' b -> Pattern' a
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
<$ :: forall a b. a -> Pattern' b -> Pattern' a
Functor, (forall m. Monoid m => Pattern' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
-> (forall a. (a -> a -> a) -> Pattern' a -> a)
-> (forall a. (a -> a -> a) -> Pattern' a -> a)
-> (forall a. Pattern' a -> [a])
-> (forall a. Pattern' a -> Bool)
-> (forall a. Pattern' a -> Int)
-> (forall a. Eq a => a -> Pattern' a -> Bool)
-> (forall a. Ord a => Pattern' a -> a)
-> (forall a. Ord a => Pattern' a -> a)
-> (forall a. Num a => Pattern' a -> a)
-> (forall a. Num a => Pattern' a -> a)
-> Foldable Pattern'
forall a. Eq a => a -> Pattern' a -> Bool
forall a. Num a => Pattern' a -> a
forall a. Ord a => Pattern' a -> a
forall m. Monoid m => Pattern' m -> m
forall a. Pattern' a -> Bool
forall a. Pattern' a -> Int
forall a. Pattern' a -> [a]
forall a. (a -> a -> a) -> Pattern' a -> a
forall m a. Monoid m => (a -> m) -> Pattern' a -> m
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall a b. (a -> b -> b) -> b -> Pattern' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Pattern' m -> m
fold :: forall m. Monoid m => Pattern' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$ctoList :: forall a. Pattern' a -> [a]
toList :: forall a. Pattern' a -> [a]
$cnull :: forall a. Pattern' a -> Bool
null :: forall a. Pattern' a -> Bool
$clength :: forall a. Pattern' a -> Int
length :: forall a. Pattern' a -> Int
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$cmaximum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
product :: forall a. Num a => Pattern' a -> a
Foldable, Functor Pattern'
Foldable Pattern'
(Functor Pattern', Foldable Pattern') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Pattern' a -> f (Pattern' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Pattern' (f a) -> f (Pattern' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Pattern' a -> m (Pattern' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Pattern' (m a) -> m (Pattern' a))
-> Traversable Pattern'
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
Traversable, (forall x. Pattern' x -> Rep (Pattern' x) x)
-> (forall x. Rep (Pattern' x) x -> Pattern' x)
-> Generic (Pattern' x)
forall x. Rep (Pattern' x) x -> Pattern' x
forall x. Pattern' x -> Rep (Pattern' x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall x x. Rep (Pattern' x) x -> Pattern' x
forall x x. Pattern' x -> Rep (Pattern' x) x
$cfrom :: forall x x. Pattern' x -> Rep (Pattern' x) x
from :: forall x. Pattern' x -> Rep (Pattern' x) x
$cto :: forall x x. Rep (Pattern' x) x -> Pattern' x
to :: forall x. Rep (Pattern' x) x -> Pattern' x
Generic)

instance Pretty a => Pretty (Pattern' a) where
  prettyPrec :: Int -> Pattern' a -> Doc
prettyPrec Int
n (VarP PatternInfo
_o a
x)   = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x
  prettyPrec Int
_ (DotP PatternInfo
_o Term
t)   = Doc
"." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> Term -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Term
t
  prettyPrec Int
n (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
nps)= Bool -> Doc -> Doc
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    (Doc
lazy Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> QName -> Doc
forall a. Pretty a => a -> Doc
pretty (ConHead -> QName
conName ConHead
c)) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Arg (Pattern' a) -> Doc) -> [Arg (Pattern' a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Arg (Pattern' a) -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
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' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
          lazy :: Doc
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Doc
"~"
               | Bool
otherwise  = Doc
forall a. Monoid a => a
mempty
  prettyPrec Int
n (DefP PatternInfo
_o QName
q [NamedArg (Pattern' a)]
nps) = Bool -> Doc -> Doc
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Arg (Pattern' a) -> Doc) -> [Arg (Pattern' a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Arg (Pattern' a) -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Arg (Pattern' a)]
ps)
    where ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
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' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
  prettyPrec Int
n (MaskP Pattern' a
ps) = Bool -> Doc -> Doc
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> Doc -> Doc
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    Pattern' a -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern' a
ps
  prettyPrec Int
_ (LitP PatternInfo
_ Literal
l)    = Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
  prettyPrec Int
_ (ProjP ProjOrigin
_o QName
q)  = String -> Doc
forall a. String -> Doc a
text (String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++! QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q)
  prettyPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
n a
x

instance KillRange a => KillRange (Pattern' a) where
  killRange :: KillRangeT (Pattern' a)
killRange Pattern' a
p =
    case Pattern' a
p of
      VarP PatternInfo
o a
x         -> (PatternInfo -> a -> Pattern' a) -> PatternInfo -> a -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o a
x
      DotP PatternInfo
o Term
v         -> (PatternInfo -> Term -> Pattern' a)
-> PatternInfo -> Term -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
v
      ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps -> (ConHead
 -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
-> ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' a)]
-> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
info [NamedArg (Pattern' a)]
ps
      LitP PatternInfo
o Literal
l         -> (PatternInfo -> Literal -> Pattern' a)
-> PatternInfo -> Literal -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
      ProjP ProjOrigin
o QName
q        -> (QName -> Pattern' a) -> QName -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ProjOrigin -> QName -> Pattern' a
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o) QName
q
      IApplyP PatternInfo
o Term
u Term
t a
x  -> (Term -> Term -> a -> Pattern' a)
-> Term -> Term -> a -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (PatternInfo -> Term -> Term -> a -> Pattern' a
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o) Term
u Term
t a
x
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps      -> (QName -> [NamedArg (Pattern' a)] -> Pattern' a)
-> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o) QName
q [NamedArg (Pattern' a)]
ps
      MaskP Pattern' a
p          -> KillRangeT (Pattern' a) -> KillRangeT (Pattern' a)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN KillRangeT (Pattern' a)
forall x. Pattern' x -> Pattern' x
MaskP Pattern' a
p

type Pattern = Pattern' PatVarName
    -- ^ The @PatVarName@ is a name suggestion.

varP :: a -> Pattern' a
varP :: forall a. a -> Pattern' a
varP = PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo

dotP :: Term -> Pattern' a
dotP :: forall a. Term -> Pattern' a
dotP = PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo

litP :: Literal -> Pattern' a
litP :: forall a. Literal -> Pattern' a
litP = PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
defaultPatternInfo

-- | Type used when numbering pattern variables.
data DBPatVar = DBPatVar
  { DBPatVar -> PatVarName
dbPatVarName  :: PatVarName
  , DBPatVar -> Int
dbPatVarIndex :: !Int
  } deriving (Int -> DBPatVar -> ShowS
[DBPatVar] -> ShowS
DBPatVar -> String
(Int -> DBPatVar -> ShowS)
-> (DBPatVar -> String) -> ([DBPatVar] -> ShowS) -> Show DBPatVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DBPatVar -> ShowS
showsPrec :: Int -> DBPatVar -> ShowS
$cshow :: DBPatVar -> String
show :: DBPatVar -> String
$cshowList :: [DBPatVar] -> ShowS
showList :: [DBPatVar] -> ShowS
Show, DBPatVar -> DBPatVar -> Bool
(DBPatVar -> DBPatVar -> Bool)
-> (DBPatVar -> DBPatVar -> Bool) -> Eq DBPatVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DBPatVar -> DBPatVar -> Bool
== :: DBPatVar -> DBPatVar -> Bool
$c/= :: DBPatVar -> DBPatVar -> Bool
/= :: DBPatVar -> DBPatVar -> Bool
Eq, (forall x. DBPatVar -> Rep DBPatVar x)
-> (forall x. Rep DBPatVar x -> DBPatVar) -> Generic DBPatVar
forall x. Rep DBPatVar x -> DBPatVar
forall x. DBPatVar -> Rep DBPatVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DBPatVar -> Rep DBPatVar x
from :: forall x. DBPatVar -> Rep DBPatVar x
$cto :: forall x. Rep DBPatVar x -> DBPatVar
to :: forall x. Rep DBPatVar x -> DBPatVar
Generic)

instance Pretty DBPatVar where
  prettyPrec :: Int -> DBPatVar -> Doc
prettyPrec Int
_ DBPatVar
x = PatVarName -> Doc
forall a. Pretty a => a -> Doc
pretty (DBPatVar -> PatVarName
dbPatVarName DBPatVar
x) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> Doc
forall a. Pretty a => a -> Doc
pretty (DBPatVar -> Int
dbPatVarIndex DBPatVar
x)

instance KillRange DBPatVar where
  killRange :: KillRangeT DBPatVar
killRange (DBPatVar PatVarName
x Int
i) = (PatVarName -> Int -> DBPatVar) -> PatVarName -> Int -> DBPatVar
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
i

type DeBruijnPattern = Pattern' DBPatVar
type PatternSubstitution = Substitution' DeBruijnPattern

-- | Named pattern arguments.
type NAPs = [NamedArg DeBruijnPattern]

namedVarP :: PatVarName -> Named_ Pattern
namedVarP :: PatVarName -> Named_ Pattern
namedVarP PatVarName
x = Maybe NamedName -> Pattern -> Named_ Pattern
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
named (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
forall a b. (a -> b) -> a -> b
$ PatVarName -> Pattern
forall a. a -> Pattern' a
varP PatVarName
x
  where named :: Maybe NamedName
named = if PatVarName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore PatVarName
x then Maybe NamedName
forall a. Maybe a
Nothing else NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged PatVarName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged PatVarName -> NamedName) -> Ranged PatVarName -> NamedName
forall a b. (a -> b) -> a -> b
$ PatVarName -> Ranged PatVarName
forall a. a -> Ranged a
unranged PatVarName
x

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP Int
m = ((Pattern -> DeBruijnPattern)
-> Named_ Pattern -> Named_ DeBruijnPattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> DeBruijnPattern)
 -> Named_ Pattern -> Named_ DeBruijnPattern)
-> ((PatVarName -> DBPatVar) -> Pattern -> DeBruijnPattern)
-> (PatVarName -> DBPatVar)
-> Named_ Pattern
-> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PatVarName -> DBPatVar) -> Pattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\PatVarName
x -> PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
m) (Named_ Pattern -> Named_ DeBruijnPattern)
-> (PatVarName -> Named_ Pattern)
-> PatVarName
-> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Named_ Pattern
namedVarP

-- | Make an absurd pattern with the given de Bruijn index.
absurdP :: Int -> DeBruijnPattern
absurdP :: Int -> DeBruijnPattern
absurdP = PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) (DBPatVar -> DeBruijnPattern)
-> (Int -> DBPatVar) -> Int -> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
absurdPatternName

-- | The @ConPatternInfo@ states whether the constructor belongs to
--   a record type (@True@) or data type (@False@).
--   In the former case, the @PatOrigin@ of the @conPInfo@ says
--   whether the record pattern orginates from the expansion of an
--   implicit pattern.
--   The @Type@ is the type of the whole record pattern.
--   The scope used for the type is given by any outer scope
--   plus the clause's telescope ('clauseTel').
data ConPatternInfo = ConPatternInfo
  { ConPatternInfo -> PatternInfo
conPInfo   :: PatternInfo
    -- ^ Information on the origin of the pattern.
  , ConPatternInfo -> Bool
conPRecord :: Bool
    -- ^ @False@ if data constructor.
    --   @True@ if record constructor.
  , ConPatternInfo -> Bool
conPFallThrough :: Bool
    -- ^ Should the match block on non-canonical terms or can it
    --   proceed to the catch-all clause?
  , ConPatternInfo -> Maybe (Arg Type)
conPType   :: Maybe (Arg Type)
    -- ^ The type of the whole constructor pattern.
    --   Should be present (@Just@) if constructor pattern is
    --   is generated ordinarily by type-checking.
    --   Could be absent (@Nothing@) if pattern comes from some
    --   plugin (like Agsy).
    --   Needed e.g. for with-clause stripping.
  , ConPatternInfo -> Bool
conPLazy :: Bool
    -- ^ Lazy patterns are generated by the forcing translation in the unifier
    --   ('Agda.TypeChecking.Rules.LHS.Unify.unifyStep') and are dropped by
    --   the clause compiler (TODO: not yet)
    --   ('Agda.TypeChecking.CompiledClause.Compile.compileClauses') when the
    --   variables they bind are unused.
  }
  deriving (Int -> ConPatternInfo -> ShowS
[ConPatternInfo] -> ShowS
ConPatternInfo -> String
(Int -> ConPatternInfo -> ShowS)
-> (ConPatternInfo -> String)
-> ([ConPatternInfo] -> ShowS)
-> Show ConPatternInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConPatternInfo -> ShowS
showsPrec :: Int -> ConPatternInfo -> ShowS
$cshow :: ConPatternInfo -> String
show :: ConPatternInfo -> String
$cshowList :: [ConPatternInfo] -> ShowS
showList :: [ConPatternInfo] -> ShowS
Show, (forall x. ConPatternInfo -> Rep ConPatternInfo x)
-> (forall x. Rep ConPatternInfo x -> ConPatternInfo)
-> Generic ConPatternInfo
forall x. Rep ConPatternInfo x -> ConPatternInfo
forall x. ConPatternInfo -> Rep ConPatternInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConPatternInfo -> Rep ConPatternInfo x
from :: forall x. ConPatternInfo -> Rep ConPatternInfo x
$cto :: forall x. Rep ConPatternInfo x -> ConPatternInfo
to :: forall x. Rep ConPatternInfo x -> ConPatternInfo
Generic)

noConPatternInfo :: ConPatternInfo
noConPatternInfo :: ConPatternInfo
noConPatternInfo = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False Maybe (Arg Type)
forall a. Maybe a
Nothing Bool
False

-- | Build partial 'ConPatternInfo' from 'ConInfo'
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ConORec = ConPatternInfo
noConPatternInfo{ conPInfo = PatternInfo PatORec [] , conPRecord = True }
toConPatternInfo ConInfo
_ = ConPatternInfo
noConPatternInfo

-- | Build 'ConInfo' from 'ConPatternInfo'.
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
i = PatOrigin -> ConInfo
patToConO (PatOrigin -> ConInfo) -> PatOrigin -> ConInfo
forall a b. (a -> b) -> a -> b
$ PatternInfo -> PatOrigin
patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i
  where
    patToConO :: PatOrigin -> ConOrigin
    patToConO :: PatOrigin -> ConInfo
patToConO = \case
      PatOrigin
PatOSystem -> ConInfo
ConOSystem
      PatOrigin
PatOSplit  -> ConInfo
ConOSplit
      PatOSplitArg{} -> ConInfo
ConOSystem
      PatOVar{}  -> ConInfo
ConOSystem
      PatOrigin
PatODot    -> ConInfo
ConOSystem
      PatOrigin
PatOWild   -> ConInfo
ConOSystem
      PatOrigin
PatOCon    -> ConInfo
ConOCon
      PatOrigin
PatORec    -> ConInfo
ConORec
      PatOrigin
PatOLit    -> ConInfo
ConOCon
      PatOrigin
PatOAbsurd -> ConInfo
ConOSystem

-- | Extract pattern variables in left-to-right order.
--   A 'DotP' is also treated as variable (see docu for 'Clause').
class PatternVars a where
  type PatternVarOut a
  patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]

instance PatternVars (Arg (Pattern' a)) where
  type PatternVarOut (Arg (Pattern' a)) = a

  -- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
  patternVars :: Arg (Pattern' a)
-> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
patternVars (Arg ArgInfo
i (VarP PatternInfo
_ a
x)   ) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ PatternVarOut (Arg (Pattern' a))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. a -> Either a b
Left a
PatternVarOut (Arg (Pattern' a))
x]
  patternVars (Arg ArgInfo
i (DotP PatternInfo
_ Term
t)   ) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. b -> Either a b
Right Term
t]
  patternVars (Arg ArgInfo
_ (ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps)) = [NamedArg (Pattern' a)]
-> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
  patternVars (Arg ArgInfo
_ (DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps)) = [NamedArg (Pattern' a)]
-> [Arg (Either (PatternVarOut [NamedArg (Pattern' a)]) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars [NamedArg (Pattern' a)]
ps
  patternVars (Arg ArgInfo
_ (LitP PatternInfo
_ Literal
_)   ) = []
  patternVars (Arg ArgInfo
i (MaskP Pattern' a
p)    ) = Arg (Pattern' a)
-> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars (ArgInfo -> Pattern' a -> Arg (Pattern' a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i Pattern' a
p)
  patternVars (Arg ArgInfo
_ ProjP{}      ) = []
  patternVars (Arg ArgInfo
i (IApplyP PatternInfo
_ Term
_ Term
_ a
x)) = [ArgInfo
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (Either (PatternVarOut (Arg (Pattern' a))) Term
 -> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
-> Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)
forall a b. (a -> b) -> a -> b
$ PatternVarOut (Arg (Pattern' a))
-> Either (PatternVarOut (Arg (Pattern' a))) Term
forall a b. a -> Either a b
Left a
PatternVarOut (Arg (Pattern' a))
x]


instance PatternVars (NamedArg (Pattern' a)) where
  type PatternVarOut (NamedArg (Pattern' a)) = a

  patternVars :: NamedArg (Pattern' a)
-> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)]
patternVars = Arg (Pattern' a) -> [Arg (Either a Term)]
Arg (Pattern' a)
-> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars (Arg (Pattern' a) -> [Arg (Either a Term)])
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> [Arg (Either a Term)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing

instance PatternVars a => PatternVars [a] where
  type PatternVarOut [a] = PatternVarOut a

  patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)]
patternVars = (a -> [Arg (Either (PatternVarOut a) Term)])
-> [a] -> [Arg (Either (PatternVarOut a) Term)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [Arg (Either (PatternVarOut a) Term)]
forall a.
PatternVars a =>
a -> [Arg (Either (PatternVarOut a) Term)]
patternVars

-- | Retrieve the PatternInfo from a pattern
patternInfo :: Pattern' x -> Maybe PatternInfo
patternInfo :: forall x. Pattern' x -> Maybe PatternInfo
patternInfo (VarP PatternInfo
i x
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DotP PatternInfo
i Term
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (LitP PatternInfo
i Literal
_)        = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (ConP ConHead
_ ConPatternInfo
ci [NamedArg (Pattern' x)]
_)     = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just (PatternInfo -> Maybe PatternInfo)
-> PatternInfo -> Maybe PatternInfo
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
ci
patternInfo ProjP{}           = Maybe PatternInfo
forall a. Maybe a
Nothing
patternInfo (IApplyP PatternInfo
i Term
_ Term
_ x
_) = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (DefP PatternInfo
i QName
_ [NamedArg (Pattern' x)]
_)      = PatternInfo -> Maybe PatternInfo
forall a. a -> Maybe a
Just PatternInfo
i
patternInfo (MaskP Pattern' x
p)         = Pattern' x -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo Pattern' x
p

-- | Retrieve the origin of a pattern
patternOrigin :: Pattern' x -> Maybe PatOrigin
patternOrigin :: forall x. Pattern' x -> Maybe PatOrigin
patternOrigin = (PatternInfo -> PatOrigin) -> Maybe PatternInfo -> Maybe PatOrigin
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PatternInfo -> PatOrigin
patOrigin (Maybe PatternInfo -> Maybe PatOrigin)
-> (Pattern' x -> Maybe PatternInfo)
-> Pattern' x
-> Maybe PatOrigin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' x -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo

instance IsProjP (Pattern' a) where
  isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP = \case
    ProjP ProjOrigin
o QName
d -> (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. a -> Maybe a
Just (ProjOrigin
o, QName -> AmbiguousQName
unambiguous QName
d)
    Pattern' a
_ -> Maybe (ProjOrigin, AmbiguousQName)
forall a. Maybe a
Nothing

---------------------------------------------------------------------------
-- * Absurd Lambda
---------------------------------------------------------------------------

absurdPatternName :: PatVarName
absurdPatternName :: PatVarName
absurdPatternName = PatVarName
"()"

---------------------------------------------------------------------------
-- * Tools for patterns
---------------------------------------------------------------------------

dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm = Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
True

-- | Computes the permutation from the clause telescope
--   to the pattern variables.
--
--   Use as @fromMaybe __IMPOSSIBLE__ . dbPatPerm@ to crash
--   in a controlled way if a de Bruijn index is out of scope here.
--
--   The first argument controls whether dot patterns counts as variables or
--   not.
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
countDots [NamedArg DeBruijnPattern]
ps = Int -> [Int] -> Permutation
Perm ([Maybe Int] -> Int
forall a. Sized a => a -> Int
size [Maybe Int]
ixs) ([Int] -> Permutation) -> Maybe [Int] -> Maybe Permutation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Int]
picks where
  ixs :: [Maybe Int]
ixs   = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named_ DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named_ DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named_ DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
  n :: Int
n     = [Int] -> Int
forall a. Sized a => a -> Int
size ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
ixs
  picks :: Maybe [Int]
picks = [Int] -> (Int -> Maybe Int) -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ((Int -> Maybe Int) -> Maybe [Int])
-> (Int -> Maybe Int) -> Maybe [Int]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> Maybe Int -> [Maybe Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) [Maybe Int]
ixs

  getIndices :: DeBruijnPattern -> [Maybe Int]
  getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP PatternInfo
_ DBPatVar
x)    = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]
  getIndices (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named_ DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named_ DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named_ DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
  getIndices (DefP PatternInfo
_ QName
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named_ DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named_ DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named_ DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
  getIndices (MaskP DeBruijnPattern
ps)    = DeBruijnPattern -> [Maybe Int]
getIndices DeBruijnPattern
ps
  getIndices (DotP PatternInfo
_ Term
_)    = [Maybe Int
forall a. Maybe a
Nothing | Bool
countDots]
  getIndices (LitP PatternInfo
_ Literal
_)    = []
  getIndices ProjP{}       = []
  getIndices (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x) = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]

-- | Turn a pattern into a term.
--   Projection patterns are turned into projection eliminations,
--   other patterns into apply elimination.
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim (Arg ArgInfo
ai (VarP PatternInfo
o DBPatVar
x)) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternToElim (Arg ArgInfo
ai (ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps)) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$
      (NamedArg DeBruijnPattern -> Elim)
-> [NamedArg DeBruijnPattern] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' (Arg DeBruijnPattern -> Elim
patternToElim (Arg DeBruijnPattern -> Elim)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
  where ci :: ConInfo
ci = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi
patternToElim (Arg ArgInfo
ai (DefP PatternInfo
o QName
q [NamedArg DeBruijnPattern]
ps)) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$
      (NamedArg DeBruijnPattern -> Elim)
-> [NamedArg DeBruijnPattern] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' (Arg DeBruijnPattern -> Elim
patternToElim (Arg DeBruijnPattern -> Elim)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
patternToElim (Arg ArgInfo
ai (DotP PatternInfo
o Term
t)   ) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
t
patternToElim (Arg ArgInfo
ai (LitP PatternInfo
o Literal
l)    ) = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
patternToElim (Arg ArgInfo
ai (ProjP ProjOrigin
o QName
dest)) = ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
dest
patternToElim (Arg ArgInfo
ai (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x)) = Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
t Term
u (Term -> Elim) -> Term -> Elim
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternToElim (Arg ArgInfo
ai (MaskP DeBruijnPattern
ps))        = Arg DeBruijnPattern -> Elim
patternToElim (ArgInfo -> DeBruijnPattern -> Arg DeBruijnPattern
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai DeBruijnPattern
ps)

patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
patternsToElims :: [NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ps = (NamedArg DeBruijnPattern -> Elim)
-> [NamedArg DeBruijnPattern] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' NamedArg DeBruijnPattern -> Elim
build [NamedArg DeBruijnPattern]
ps
  where
    build :: NamedArg DeBruijnPattern -> Elim
    build :: NamedArg DeBruijnPattern -> Elim
build = Arg DeBruijnPattern -> Elim
patternToElim (Arg DeBruijnPattern -> Elim)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing

patternToTerm :: DeBruijnPattern -> Term
patternToTerm :: DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p = case Arg DeBruijnPattern -> Elim
patternToElim (DeBruijnPattern -> Arg DeBruijnPattern
forall a. a -> Arg a
defaultArg DeBruijnPattern
p) of
  Apply Arg Term
x -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
  Proj{}  -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  IApply Term
_ Term
_ Term
x -> Term
x

class MapNamedArgPattern a p where
  mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p

  default mapNamedArgPattern
    :: (Functor f, MapNamedArgPattern a p', p ~ f p')
    => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
  mapNamedArgPattern = (p' -> p') -> p -> p
(p' -> p') -> f p' -> f p'
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((p' -> p') -> p -> p)
-> ((NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p')
-> (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> p
-> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p'
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern

-- | Modify the content of @VarP@, and the closest surrounding @NamedArg@.
--
--   Note: the @mapNamedArg@ for @Pattern'@ is not expressible simply
--   by @fmap@ or @traverse@ etc., since @ConP@ has @NamedArg@ subpatterns,
--   which are taken into account by @mapNamedArg@.

instance MapNamedArgPattern a (NamedArg (Pattern' a)) where
  mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np =
    case NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
np of
      VarP PatternInfo
o a
x    -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      DotP  PatternInfo
o Term
t   -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      LitP PatternInfo
o Literal
l    -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      ProjP ProjOrigin
o QName
q   -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      MaskP Pattern' a
ps    -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
i ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
      IApplyP PatternInfo
o Term
u Term
t a
x -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np

instance MapNamedArgPattern a p => MapNamedArgPattern a [p] where


-- | Generic pattern traversal.
--
--   Pre-applies a pattern modification, recurses, and post-applies another one.

class PatternLike a b where

  -- | Fold pattern.
  foldrPattern
    :: Monoid m
    => (Pattern' a -> m -> m)
         -- ^ Combine a pattern and the value computed from its subpatterns.
    -> b -> m

  {-# INLINE foldrPattern #-}
  default foldrPattern
    :: (Monoid m, Foldable f, PatternLike a p, f p ~ b)
    => (Pattern' a -> m -> m) -> b -> m
  foldrPattern = (p -> m) -> b -> m
(p -> m) -> f p -> m
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((p -> m) -> b -> m)
-> ((Pattern' a -> m -> m) -> p -> m)
-> (Pattern' a -> m -> m)
-> b
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> m -> m) -> p -> m
forall m. Monoid m => (Pattern' a -> m -> m) -> p -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern

  -- | Traverse pattern.
  traversePatternM
    :: Monad m
    => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
    -> (Pattern' a -> m (Pattern' a))  -- ^ @post@: Modification after recursion.
    -> b -> m b

  default traversePatternM
    :: (Traversable f, PatternLike a p, f p ~ b, Monad m)
    => (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a))
    -> b -> m b

  traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = (p -> m p) -> f p -> m (f p)
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 ((p -> m p) -> f p -> m (f p)) -> (p -> m p) -> f p -> m (f p)
forall a b. (a -> b) -> a -> b
$ (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post

-- | Compute from each subpattern a value and collect them all in a monoid.

foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m
foldPattern :: forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern Pattern' a -> m
f = (Pattern' a -> m -> m) -> b -> m
forall m. Monoid m => (Pattern' a -> m -> m) -> b -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern ((Pattern' a -> m -> m) -> b -> m)
-> (Pattern' a -> m -> m) -> b -> m
forall a b. (a -> b) -> a -> b
$ \ Pattern' a
p m
m -> Pattern' a -> m
f Pattern' a
p m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` m
m

-- | Traverse pattern(s) with a modification before the recursive descent.

preTraversePatternM
  :: (PatternLike a b, Monad m)
  => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
  -> b -> m b
preTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM Pattern' a -> m (Pattern' a)
pre = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- | Traverse pattern(s) with a modification after the recursive descent.

postTraversePatternM :: (PatternLike a b, Monad m)
                     => (Pattern' a -> m (Pattern' a))  -- ^ @post@: Modification after recursion.
                     -> b -> m b
postTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- This is where the action is:

instance PatternLike a (Pattern' a) where

  foldrPattern :: forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
foldrPattern Pattern' a -> m -> m
f Pattern' a
p = Pattern' a -> m -> m
f Pattern' a
p (m -> m) -> m -> m
forall a b. (a -> b) -> a -> b
$ case Pattern' a
p of
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall m.
Monoid m =>
(Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
    DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall m.
Monoid m =>
(Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
    MaskP Pattern' a
p     -> (Pattern' a -> m -> m) -> Pattern' a -> m
forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f Pattern' a
p
    VarP PatternInfo
_ a
_    -> m
forall a. Monoid a => a
mempty
    LitP PatternInfo
_ Literal
_    -> m
forall a. Monoid a => a
mempty
    DotP PatternInfo
_ Term
_    -> m
forall a. Monoid a => a
mempty
    ProjP ProjOrigin
_ QName
_   -> m
forall a. Monoid a => a
mempty
    IApplyP{}   -> m
forall a. Monoid a => a
mempty

  traversePatternM :: forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = Pattern' a -> m (Pattern' a)
pre (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
recurse (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
post
    where
    recurse :: Pattern' a -> m (Pattern' a)
recurse Pattern' a
p = case Pattern' a
p of
      ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)]
ps -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (Pattern' a)] -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps  -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (Pattern' a)] -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
      MaskP Pattern' a
p      -> Pattern' a -> Pattern' a
forall x. Pattern' x -> Pattern' x
MaskP (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post Pattern' a
p
      VarP  PatternInfo
_ a
_    -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      LitP  PatternInfo
_ Literal
_    -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      DotP  PatternInfo
_ Term
_    -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      ProjP ProjOrigin
_ QName
_    -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      IApplyP{}    -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p

-- Boilerplate instances:

instance PatternLike a b => PatternLike a [b]         where
instance PatternLike a b => PatternLike a (Arg b)     where
instance PatternLike a b => PatternLike a (Named x b) where

-- Counting pattern variables ---------------------------------------------

class CountPatternVars a where
  countPatternVars :: a -> Int

  default countPatternVars :: (Foldable f, CountPatternVars b, f b ~ a) =>
                              a -> Int
  countPatternVars = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (a -> Sum Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Sum Int) -> f b -> Sum Int
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (b -> Int) -> b -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars)

instance CountPatternVars a => CountPatternVars [a] where
instance CountPatternVars a => CountPatternVars (Arg a) where
instance CountPatternVars a => CountPatternVars (Named x a) where

instance CountPatternVars (Pattern' x) where
  countPatternVars :: Pattern' x -> Int
countPatternVars = \case
    MaskP{}     -> Int
forall a. HasCallStack => a
__IMPOSSIBLE__
    VarP{}      -> Int
1
    DotP{}      -> Int
1 -- dot patterns are treated as variables in the clauses
    IApplyP{}   -> Int
1
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars [NamedArg (Pattern' x)]
ps
    DefP PatternInfo
_ QName
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> Int
forall a. CountPatternVars a => a -> Int
countPatternVars [NamedArg (Pattern' x)]
ps
    LitP{}      -> Int
0
    ProjP{}     -> Int
0

class HasDefP a where
  -- | Check whether any of the patterns in the given thing are 'DefP's.
  hasDefP :: a -> Bool

  default hasDefP :: (Foldable f, HasDefP b, a ~ f b) => a -> Bool
  hasDefP = (b -> Bool) -> f b -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any b -> Bool
forall a. HasDefP a => a -> Bool
hasDefP

instance HasDefP a => HasDefP [a]
instance HasDefP a => HasDefP (Named_ a)
instance HasDefP a => HasDefP (Arg a)

instance HasDefP (Pattern' a) where
  hasDefP :: Pattern' a -> Bool
hasDefP = \case
    VarP{}      -> Bool
False
    DotP{}      -> Bool
False
    LitP{}      -> Bool
False
    ProjP{}     -> Bool
False
    IApplyP{}   -> Bool
False
    DefP{}      -> Bool
True
    MaskP{}     -> Bool
True
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
as -> [NamedArg (Pattern' a)] -> Bool
forall a. HasDefP a => a -> Bool
hasDefP [NamedArg (Pattern' a)]
as

instance KillRange PatOrigin where
  killRange :: KillRangeT PatOrigin
killRange = \case
    PatOrigin
PatOSystem     -> PatOrigin
PatOSystem
    PatOrigin
PatOSplit      -> PatOrigin
PatOSplit
    PatOSplitArg PatVarName
n -> (PatVarName -> PatOrigin) -> PatVarName -> PatOrigin
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatVarName -> PatOrigin
PatOSplitArg PatVarName
n
    PatOVar Name
n      -> (Name -> PatOrigin) -> Name -> PatOrigin
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> PatOrigin
PatOVar Name
n
    PatOrigin
PatODot        -> PatOrigin
PatODot
    PatOrigin
PatOWild       -> PatOrigin
PatOWild
    PatOrigin
PatOCon        -> PatOrigin
PatOCon
    PatOrigin
PatORec        -> PatOrigin
PatORec
    PatOrigin
PatOLit        -> PatOrigin
PatOLit
    PatOrigin
PatOAbsurd     -> PatOrigin
PatOAbsurd

instance KillRange PatternInfo where
  killRange :: KillRangeT PatternInfo
killRange (PatternInfo PatOrigin
o [Name]
xs) = (PatOrigin -> [Name] -> PatternInfo)
-> PatOrigin -> [Name] -> PatternInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
o [Name]
xs

instance KillRange ConPatternInfo where
  killRange :: KillRangeT ConPatternInfo
killRange (ConPatternInfo PatternInfo
i Bool
mr Bool
b Maybe (Arg Type)
mt Bool
lz) = (Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Maybe (Arg Type) -> Bool -> ConPatternInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
i Bool
mr Bool
b) Maybe (Arg Type)
mt Bool
lz

instance NFData PatternInfo
instance NFData PatOrigin
instance NFData x => NFData (Pattern' x)
instance NFData DBPatVar
instance NFData ConPatternInfo