{-| Given

    1. the function clauses @cs@
    2. the patterns @ps@ of the split clause

we want to compute a variable index (in the split clause) to split on next.

The matcher here checks whether the split clause is covered by one of
the given clauses @cs@ or whether further splitting is needed (and
when yes, where).
-}

module Agda.TypeChecking.Coverage.Match
  ( Match(..), match, matchClause
  , SplitPattern, SplitPatVar(..)
  , fromSplitPattern, fromSplitPatterns, toSplitPatterns
  , toSplitPSubst, applySplitPSubst
  , isTrivialPattern
  , BlockingVar(..), BlockingVars, BlockedOnResult(..)
  , setBlockingVarOverlap
  , ApplyOrIApply(..)
  ) where

import Prelude hiding ( null )

import Data.DList (DList)
import Data.Foldable (toList)
import qualified Data.List as List
import Data.Maybe (mapMaybe, fromMaybe)
import Data.Semigroup ( Semigroup, (<>))

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty ( PrettyTCM(..) )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( Pretty(..), text, (<+>), cat , prettyList_ )
import Agda.Utils.Monad
import Agda.Utils.Singleton

import Agda.Utils.Impossible

-- | If matching is inconclusive (@Block@) we want to know which
--   variables or projections are blocking the match.
data Match a
  = Yes a   -- ^ Matches unconditionally.
  | No      -- ^ Definitely does not match.
  | Block
    { forall a. Match a -> BlockedOnResult
blockedOnResult :: BlockedOnResult
      -- ^ @BlockedOnProj o@ if the clause has a result split.
    , forall a. Match a -> BlockingVars
blockedOnVars :: BlockingVars
      -- ^ @BlockingVar i cs ls o@ means variable @i@ is blocked on
      -- constructors @cs@ and literals @ls@.
    }
  deriving ((forall a b. (a -> b) -> Match a -> Match b)
-> (forall a b. a -> Match b -> Match a) -> Functor Match
forall a b. a -> Match b -> Match a
forall a b. (a -> b) -> Match a -> Match 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) -> Match a -> Match b
fmap :: forall a b. (a -> b) -> Match a -> Match b
$c<$ :: forall a b. a -> Match b -> Match a
<$ :: forall a b. a -> Match b -> Match a
Functor)

-- | Missing elimination blocking a match.
data BlockedOnResult
  = BlockedOnProj      -- ^ Blocked on unsplit projection.
     { BlockedOnResult -> Bool
blockedOnResultOverlap :: Bool
       -- ^ True if there are also matching clauses without an unsplit
       -- copattern.
     }
  | BlockedOnApply     -- ^ Blocked on unintroduced argument.
     { BlockedOnResult -> ApplyOrIApply
blockedOnResultIApply :: ApplyOrIApply
       -- ^ Is the unintroduced argument an 'IApply' pattern?
     }
  | NotBlockedOnResult

data ApplyOrIApply = IsApply | IsIApply

-- | Variable blocking a match.
data BlockingVar = BlockingVar
  { BlockingVar -> Nat
blockingVarNo  :: Nat
    -- ^ De Bruijn index of variable blocking the match.
  , BlockingVar -> [ConHead]
blockingVarCons :: [ConHead]
    -- ^ Constructors in this position.
  , BlockingVar -> [Literal]
blockingVarLits :: [Literal]
    -- ^ Literals in this position.
  , BlockingVar -> Bool
blockingVarOverlap :: Bool
    -- ^ True if at least one clause has a variable pattern in this
    --   position.
  , BlockingVar -> Bool
blockingVarLazy :: Bool
    -- ^ True if at least one clause has a lazy pattern in this position.
  } deriving (Nat -> BlockingVar -> ShowS
BlockingVars -> ShowS
BlockingVar -> String
(Nat -> BlockingVar -> ShowS)
-> (BlockingVar -> String)
-> (BlockingVars -> ShowS)
-> Show BlockingVar
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Nat -> BlockingVar -> ShowS
showsPrec :: Nat -> BlockingVar -> ShowS
$cshow :: BlockingVar -> String
show :: BlockingVar -> String
$cshowList :: BlockingVars -> ShowS
showList :: BlockingVars -> ShowS
Show)

type BlockingVars = [BlockingVar]

-- | Substitution of 'SplitPattern's for de Bruijn indices in covering
--   clause to match 'SplitClause'.
type SplitInstantiation = [(Nat,SplitPattern)]

{-# SPECIALIZE match :: [Clause] -> [NamedArg SplitPattern] -> TCM (Match (Nat, SplitInstantiation)) #-}
-- | Match the given patterns against a list of clauses.
--
-- If successful, return the index of the covering clause.
--
match :: PureTCM m
      => [Clause]                           -- ^ Search for clause that covers the patterns.
      -> [NamedArg SplitPattern]            -- ^ Patterns of the current 'SplitClause'.
      -> m (Match (Nat, SplitInstantiation))
match :: forall (m :: * -> *).
PureTCM m =>
[Clause]
-> [NamedArg SplitPattern] -> m (Match (Nat, SplitInstantiation))
match [Clause]
cs [NamedArg SplitPattern]
ps = (m (Match (Nat, SplitInstantiation))
 -> m (Match (Nat, SplitInstantiation))
 -> m (Match (Nat, SplitInstantiation)))
-> m (Match (Nat, SplitInstantiation))
-> [m (Match (Nat, SplitInstantiation))]
-> m (Match (Nat, SplitInstantiation))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr m (Match (Nat, SplitInstantiation))
-> m (Match (Nat, SplitInstantiation))
-> m (Match (Nat, SplitInstantiation))
forall (m :: * -> *) a.
Monad m =>
m (Match a) -> m (Match a) -> m (Match a)
choice (Match (Nat, SplitInstantiation)
-> m (Match (Nat, SplitInstantiation))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Match (Nat, SplitInstantiation)
forall a. Match a
No) ([m (Match (Nat, SplitInstantiation))]
 -> m (Match (Nat, SplitInstantiation)))
-> [m (Match (Nat, SplitInstantiation))]
-> m (Match (Nat, SplitInstantiation))
forall a b. (a -> b) -> a -> b
$ (Nat -> Clause -> m (Match (Nat, SplitInstantiation)))
-> [Nat] -> [Clause] -> [m (Match (Nat, SplitInstantiation))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> Clause -> m (Match (Nat, SplitInstantiation))
forall (m :: * -> *).
PureTCM m =>
Nat -> Clause -> m (Match (Nat, SplitInstantiation))
matchIt [Nat
0..] [Clause]
cs
  where
    matchIt :: PureTCM m
            => Nat  -- Clause number.
            -> Clause
            -> m (Match (Nat, SplitInstantiation))
    matchIt :: forall (m :: * -> *).
PureTCM m =>
Nat -> Clause -> m (Match (Nat, SplitInstantiation))
matchIt Nat
i Clause
c = (DList (Nat, SplitPattern) -> (Nat, SplitInstantiation))
-> Match (DList (Nat, SplitPattern))
-> Match (Nat, SplitInstantiation)
forall a b. (a -> b) -> Match a -> Match b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\DList (Nat, SplitPattern)
s -> (Nat
i, DList (Nat, SplitPattern) -> SplitInstantiation
forall a. DList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList DList (Nat, SplitPattern)
s)) (Match (DList (Nat, SplitPattern))
 -> Match (Nat, SplitInstantiation))
-> m (Match (DList (Nat, SplitPattern)))
-> m (Match (Nat, SplitInstantiation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg SplitPattern]
-> Clause -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *).
PureTCM m =>
[NamedArg SplitPattern]
-> Clause -> m (Match (DList (Nat, SplitPattern)))
matchClause [NamedArg SplitPattern]
ps Clause
c

-- | For each variable in the patterns of a split clause, we remember the
--   de Bruijn-index and the literals excluded by previous matches.

--  (See issue #708.)
data SplitPatVar = SplitPatVar
  { SplitPatVar -> String
splitPatVarName   :: PatVarName
  , SplitPatVar -> Nat
splitPatVarIndex  :: Int
  , SplitPatVar -> [Literal]
splitExcludedLits :: [Literal]
  } deriving (Nat -> SplitPatVar -> ShowS
[SplitPatVar] -> ShowS
SplitPatVar -> String
(Nat -> SplitPatVar -> ShowS)
-> (SplitPatVar -> String)
-> ([SplitPatVar] -> ShowS)
-> Show SplitPatVar
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Nat -> SplitPatVar -> ShowS
showsPrec :: Nat -> SplitPatVar -> ShowS
$cshow :: SplitPatVar -> String
show :: SplitPatVar -> String
$cshowList :: [SplitPatVar] -> ShowS
showList :: [SplitPatVar] -> ShowS
Show)

instance Pretty SplitPatVar where
  prettyPrec :: Nat -> SplitPatVar -> Doc
prettyPrec Nat
_ SplitPatVar
x =
    String -> Doc
forall a. String -> Doc a
text (ShowS
patVarNameToString (SplitPatVar -> String
splitPatVarName SplitPatVar
x)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    String -> Doc
forall a. String -> Doc a
text (String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    [Literal] -> Doc -> ([Literal] -> Doc) -> Doc
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) Doc
forall a. Null a => a
empty (\[Literal]
lits ->
      Doc
"\\{" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Literal] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_ [Literal]
lits Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"}")

instance PrettyTCM SplitPatVar where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitPatVar -> m Doc
prettyTCM = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (SplitPatVar -> Term) -> SplitPatVar -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Term
var (Nat -> Term) -> (SplitPatVar -> Nat) -> SplitPatVar -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitPatVar -> Nat
splitPatVarIndex

type SplitPattern = Pattern' SplitPatVar

toSplitVar :: DBPatVar -> SplitPatVar
toSplitVar :: DBPatVar -> SplitPatVar
toSplitVar DBPatVar
x = String -> Nat -> [Literal] -> SplitPatVar
SplitPatVar (DBPatVar -> String
dbPatVarName DBPatVar
x) (DBPatVar -> Nat
dbPatVarIndex DBPatVar
x) []

fromSplitVar :: SplitPatVar -> DBPatVar
fromSplitVar :: SplitPatVar -> DBPatVar
fromSplitVar SplitPatVar
x = String -> Nat -> DBPatVar
DBPatVar (SplitPatVar -> String
splitPatVarName SplitPatVar
x) (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x)

instance DeBruijn SplitPatVar where
  deBruijnView :: SplitPatVar -> Maybe Nat
deBruijnView SplitPatVar
x = DBPatVar -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (SplitPatVar -> DBPatVar
fromSplitVar SplitPatVar
x)
  debruijnNamedVar :: String -> Nat -> SplitPatVar
debruijnNamedVar String
n Nat
i = DBPatVar -> SplitPatVar
toSplitVar (String -> Nat -> DBPatVar
forall a. DeBruijn a => String -> Nat -> a
debruijnNamedVar String
n Nat
i)

toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns = ((NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg DeBruijnPattern -> NamedArg SplitPattern)
 -> [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern])
-> ((DBPatVar -> SplitPatVar)
    -> NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> [NamedArg DeBruijnPattern]
-> [NamedArg SplitPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> Named_ SplitPattern)
-> NamedArg DeBruijnPattern -> NamedArg SplitPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ DeBruijnPattern -> Named_ SplitPattern)
 -> NamedArg DeBruijnPattern -> NamedArg SplitPattern)
-> ((DBPatVar -> SplitPatVar)
    -> Named_ DeBruijnPattern -> Named_ SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> NamedArg DeBruijnPattern
-> NamedArg SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> SplitPattern)
-> Named_ DeBruijnPattern -> Named_ SplitPattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> SplitPattern)
 -> Named_ DeBruijnPattern -> Named_ SplitPattern)
-> ((DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> Named_ DeBruijnPattern
-> Named_ SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DBPatVar -> SplitPatVar
toSplitVar

fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern = ((Named_ SplitPattern -> Named_ DeBruijnPattern)
-> NamedArg SplitPattern -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ SplitPattern -> Named_ DeBruijnPattern)
 -> NamedArg SplitPattern -> NamedArg DeBruijnPattern)
-> ((SplitPatVar -> DBPatVar)
    -> Named_ SplitPattern -> Named_ DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> NamedArg SplitPattern
-> NamedArg DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPattern -> DeBruijnPattern)
-> Named_ SplitPattern -> 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 ((SplitPattern -> DeBruijnPattern)
 -> Named_ SplitPattern -> Named_ DeBruijnPattern)
-> ((SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> Named_ SplitPattern
-> Named_ DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) SplitPatVar -> DBPatVar
fromSplitVar

fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns = (NamedArg SplitPattern -> NamedArg DeBruijnPattern)
-> [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPattern

type SplitPSubstitution = Substitution' SplitPattern

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst = ((DeBruijnPattern -> SplitPattern)
-> PatternSubstitution -> SplitPSubstitution
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> SplitPattern)
 -> PatternSubstitution -> SplitPSubstitution)
-> ((DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern)
-> (DBPatVar -> SplitPatVar)
-> PatternSubstitution
-> SplitPSubstitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DBPatVar -> SplitPatVar) -> DeBruijnPattern -> SplitPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DBPatVar -> SplitPatVar
toSplitVar

fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst = ((SplitPattern -> DeBruijnPattern)
-> SplitPSubstitution -> PatternSubstitution
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SplitPattern -> DeBruijnPattern)
 -> SplitPSubstitution -> PatternSubstitution)
-> ((SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern)
-> (SplitPatVar -> DBPatVar)
-> SplitPSubstitution
-> PatternSubstitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitPatVar -> DBPatVar) -> SplitPattern -> DeBruijnPattern
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) SplitPatVar -> DBPatVar
fromSplitVar

applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst :: forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst = PatternSubstitution -> a -> a
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst (PatternSubstitution -> a -> a)
-> (SplitPSubstitution -> PatternSubstitution)
-> SplitPSubstitution
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitPSubstitution -> PatternSubstitution
fromSplitPSubst

-- TODO: merge this instance and the one for DeBruijnPattern in
-- Substitute.hs into one for Subst (Pattern' a) (Pattern' a).
instance Subst SplitPattern where
  type SubstArg SplitPattern = SplitPattern

  applySubst :: Substitution' (SubstArg SplitPattern)
-> SplitPattern -> SplitPattern
applySubst Substitution' (SubstArg SplitPattern)
IdS = SplitPattern -> SplitPattern
forall a. a -> a
id
  applySubst Substitution' (SubstArg SplitPattern)
rho = \case
    VarP PatternInfo
i SplitPatVar
x        ->
      PatternInfo -> SplitPattern -> SplitPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      String -> SplitPattern -> SplitPattern
useName (SplitPatVar -> String
splitPatVarName SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      SplitPSubstitution -> Nat -> SplitPattern
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho (Nat -> SplitPattern) -> Nat -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x
    DotP PatternInfo
i Term
u        -> PatternInfo -> Term -> SplitPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i (Term -> SplitPattern) -> Term -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
u
    ConP ConHead
c ConPatternInfo
ci [NamedArg SplitPattern]
ps    -> ConHead
-> ConPatternInfo -> [NamedArg SplitPattern] -> SplitPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg SplitPattern])
Substitution' (SubstArg SplitPattern)
rho [NamedArg SplitPattern]
ps
    DefP PatternInfo
i QName
q [NamedArg SplitPattern]
ps     -> PatternInfo -> QName -> [NamedArg SplitPattern] -> SplitPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg SplitPattern])
Substitution' (SubstArg SplitPattern)
rho [NamedArg SplitPattern]
ps
    p :: SplitPattern
p@LitP{}        -> SplitPattern
p
    p :: SplitPattern
p@ProjP{}       -> SplitPattern
p
    IApplyP PatternInfo
i Term
l Term
r SplitPatVar
x ->
      Term -> Term -> SplitPattern -> SplitPattern
useEndPoints (SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
l) (SplitPSubstitution -> Term -> Term
forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho Term
r) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      PatternInfo -> SplitPattern -> SplitPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      String -> SplitPattern -> SplitPattern
useName (SplitPatVar -> String
splitPatVarName SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$
      SplitPSubstitution -> Nat -> SplitPattern
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS SplitPSubstitution
Substitution' (SubstArg SplitPattern)
rho (Nat -> SplitPattern) -> Nat -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x

    where
      -- see Subst for DeBruijnPattern
      useEndPoints :: Term -> Term -> SplitPattern -> SplitPattern
      useEndPoints :: Term -> Term -> SplitPattern -> SplitPattern
useEndPoints Term
l Term
r (VarP PatternInfo
o SplitPatVar
x)        = PatternInfo -> Term -> Term -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
l Term
r SplitPatVar
x
      useEndPoints Term
l Term
r (IApplyP PatternInfo
o Term
_ Term
_ SplitPatVar
x) = PatternInfo -> Term -> Term -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
l Term
r SplitPatVar
x
      useEndPoints Term
l Term
r SplitPattern
x                 = SplitPattern
forall a. HasCallStack => a
__IMPOSSIBLE__

      useName :: PatVarName -> SplitPattern -> SplitPattern
      useName :: String -> SplitPattern -> SplitPattern
useName String
n (VarP PatternInfo
o SplitPatVar
x)
        | String -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (SplitPatVar -> String
splitPatVarName SplitPatVar
x)
        = PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar
x { splitPatVarName = n }
      useName String
_ SplitPattern
x = SplitPattern
x

      useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
      useExcludedLits :: [Literal] -> SplitPattern -> SplitPattern
useExcludedLits [Literal]
lits = \case
        (VarP PatternInfo
o SplitPatVar
x) -> PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar
x
          { splitExcludedLits = lits ++ splitExcludedLits x }
        SplitPattern
p -> SplitPattern
p


{-# SPECIALIZE isTrivialPattern :: Pattern' a -> TCM Bool #-}
-- | A pattern that matches anything (modulo eta).
isTrivialPattern :: (HasConstInfo m) => Pattern' a -> m Bool
isTrivialPattern :: forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern = \case
  VarP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  DotP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> [m Bool] -> m Bool
forall a b. (a -> b) -> a -> b
$ ((ConPatternInfo -> Bool
conPLazy ConPatternInfo
i Bool -> Bool -> Bool
||) (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaCon (ConHead -> QName
conName ConHead
c))
                      m Bool -> [m Bool] -> [m Bool]
forall a. a -> [a] -> [a]
: ((NamedArg (Pattern' a) -> m Bool)
-> [NamedArg (Pattern' a)] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' a -> m Bool
forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern (Pattern' a -> m Bool)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
  DefP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  LitP{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  ProjP{}     -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  IApplyP{}   -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | If matching succeeds, we return the instantiation of the clause pattern vector
--   to obtain the split clause pattern vector.
type MatchResult = Match (DList (Nat, SplitPattern))

instance Pretty BlockingVar where
  pretty :: BlockingVar -> Doc
pretty (BlockingVar Nat
i [ConHead]
cs [Literal]
ls Bool
o Bool
l) = [Doc] -> Doc
forall a. [Doc a] -> Doc a
cat
    [ String -> Doc
forall a. String -> Doc a
text (String
"variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show Nat
i)
    , if [ConHead] -> Bool
forall a. Null a => a -> Bool
null [ConHead]
cs then Doc
forall a. Null a => a
empty else Doc
" blocked on constructors" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [ConHead] -> Doc
forall a. Pretty a => a -> Doc
pretty [ConHead]
cs
    , if [Literal] -> Bool
forall a. Null a => a -> Bool
null [Literal]
ls then Doc
forall a. Null a => a
empty else Doc
" blocked on literals" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Literal] -> Doc
forall a. Pretty a => a -> Doc
pretty [Literal]
ls
    , if Bool
o then Doc
" (overlapping)" else Doc
forall a. Null a => a
empty
    , if Bool
l then Doc
" (lazy)" else Doc
forall a. Null a => a
empty
    ]

yes :: Monad m => a -> m (Match a)
yes :: forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> (a -> Match a) -> a -> m (Match a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Match a
forall a. a -> Match a
Yes

no :: Monad m => m (Match a)
no :: forall (m :: * -> *) a. Monad m => m (Match a)
no = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Match a
forall a. Match a
No

blockedOnConstructor :: Monad m => Nat -> ConHead -> ConPatternInfo -> m (Match a)
blockedOnConstructor :: forall (m :: * -> *) a.
Monad m =>
Nat -> ConHead -> ConPatternInfo -> m (Match a)
blockedOnConstructor Nat
i ConHead
c ConPatternInfo
ci = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block BlockedOnResult
NotBlockedOnResult [Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Nat
i [ConHead
c] [] Bool
False (Bool -> BlockingVar) -> Bool -> BlockingVar
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Bool
conPLazy ConPatternInfo
ci]

blockedOnLiteral :: Monad m => Nat -> Literal -> m (Match a)
blockedOnLiteral :: forall (m :: * -> *) a. Monad m => Nat -> Literal -> m (Match a)
blockedOnLiteral Nat
i Literal
l = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block BlockedOnResult
NotBlockedOnResult [Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Nat
i [] [Literal
l] Bool
False Bool
False]

blockedOnProjection :: Monad m => m (Match a)
blockedOnProjection :: forall (m :: * -> *) a. Monad m => m (Match a)
blockedOnProjection = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block (Bool -> BlockedOnResult
BlockedOnProj Bool
False) []

blockedOnApplication :: Monad m => ApplyOrIApply -> m (Match a)
blockedOnApplication :: forall (m :: * -> *) a. Monad m => ApplyOrIApply -> m (Match a)
blockedOnApplication ApplyOrIApply
b = Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block (ApplyOrIApply -> BlockedOnResult
BlockedOnApply ApplyOrIApply
b) []
--UNUSED Liang-Ting Chen 2019-07-16
---- | Lens for 'blockingVarCons'.
--mapBlockingVarCons :: ([ConHead] -> [ConHead]) -> BlockingVar -> BlockingVar
--mapBlockingVarCons f b = b { blockingVarCons = f (blockingVarCons b) }
--
---- | Lens for 'blockingVarLits'.
--mapBlockingVarLits :: ([Literal] -> [Literal]) -> BlockingVar -> BlockingVar
--mapBlockingVarLits f b = b { blockingVarLits = f (blockingVarLits b) }

setBlockingVarOverlap :: BlockingVar -> BlockingVar
setBlockingVarOverlap :: BlockingVar -> BlockingVar
setBlockingVarOverlap = \BlockingVar
x -> BlockingVar
x { blockingVarOverlap = True }

overlapping :: BlockingVars -> BlockingVars
overlapping :: BlockingVars -> BlockingVars
overlapping = (BlockingVar -> BlockingVar) -> BlockingVars -> BlockingVars
forall a b. (a -> b) -> [a] -> [b]
map BlockingVar -> BlockingVar
setBlockingVarOverlap

-- | Left dominant merge of blocking vars.
zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars
zipBlockingVars BlockingVars
xs BlockingVars
ys = (BlockingVar -> BlockingVar) -> BlockingVars -> BlockingVars
forall a b. (a -> b) -> [a] -> [b]
map BlockingVar -> BlockingVar
upd BlockingVars
xs
  where
    upd :: BlockingVar -> BlockingVar
upd (BlockingVar Nat
x [ConHead]
cons [Literal]
lits Bool
o Bool
l) = case (BlockingVar -> Bool) -> BlockingVars -> Maybe BlockingVar
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Nat
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
==) (Nat -> Bool) -> (BlockingVar -> Nat) -> BlockingVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockingVar -> Nat
blockingVarNo) BlockingVars
ys of
      Just (BlockingVar Nat
_ [ConHead]
cons' [Literal]
lits' Bool
o' Bool
l') -> Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Nat
x ([ConHead]
cons [ConHead] -> [ConHead] -> [ConHead]
forall a. [a] -> [a] -> [a]
++ [ConHead]
cons') ([Literal]
lits [Literal] -> [Literal] -> [Literal]
forall a. [a] -> [a] -> [a]
++ [Literal]
lits') (Bool
o Bool -> Bool -> Bool
|| Bool
o') (Bool
l Bool -> Bool -> Bool
|| Bool
l')
      Maybe BlockingVar
Nothing -> Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Nat
x [ConHead]
cons [Literal]
lits Bool
True Bool
l

setBlockedOnResultOverlap :: BlockedOnResult -> BlockedOnResult
setBlockedOnResultOverlap :: BlockedOnResult -> BlockedOnResult
setBlockedOnResultOverlap BlockedOnResult
b = case BlockedOnResult
b of
  BlockedOnProj{}      -> BlockedOnResult
b { blockedOnResultOverlap = True }
  BlockedOnApply{}     -> BlockedOnResult
b
  NotBlockedOnResult{} -> BlockedOnResult
b

anyBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
anyBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
anyBlockedOnResult BlockedOnResult
b1 BlockedOnResult
b2 = case (BlockedOnResult
b1,BlockedOnResult
b2) of
  (BlockedOnResult
NotBlockedOnResult , BlockedOnResult
b2                ) -> BlockedOnResult
b2
  (BlockedOnResult
b1                 , BlockedOnResult
NotBlockedOnResult) -> BlockedOnResult
b1
  (BlockedOnResult
_                  , BlockedOnResult
_                 ) -> BlockedOnResult
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Left dominant merge of `BlockedOnResult`.
choiceBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
choiceBlockedOnResult :: BlockedOnResult -> BlockedOnResult -> BlockedOnResult
choiceBlockedOnResult BlockedOnResult
b1 BlockedOnResult
b2 = case (BlockedOnResult
b1,BlockedOnResult
b2) of
  (BlockedOnResult
NotBlockedOnResult  , BlockedOnResult
_                 ) -> BlockedOnResult
NotBlockedOnResult
  (BlockedOnProj Bool
o1    , BlockedOnProj Bool
o2  ) -> Bool -> BlockedOnResult
BlockedOnProj (Bool
o1 Bool -> Bool -> Bool
|| Bool
o2)
  (BlockedOnProj Bool
_     , BlockedOnResult
_                 ) -> Bool -> BlockedOnResult
BlockedOnProj Bool
True
  (BlockedOnApply ApplyOrIApply
b    , BlockedOnResult
_                 ) -> ApplyOrIApply -> BlockedOnResult
BlockedOnApply ApplyOrIApply
b

-- | @choice m m'@ combines the match results @m@ of a function clause
--   with the (already combined) match results $m'$ of the later clauses.
--   It is for skipping clauses that definitely do not match ('No').
--   It is left-strict, to be used with @foldr@.
--   If one clause unconditionally matches ('Yes') we do not look further.
choice :: Monad m => m (Match a) -> m (Match a) -> m (Match a)
choice :: forall (m :: * -> *) a.
Monad m =>
m (Match a) -> m (Match a) -> m (Match a)
choice m (Match a)
m m (Match a)
m' = m (Match a)
m m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Yes a
a -> a -> m (Match a)
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes a
a
  Block BlockedOnResult
r BlockingVars
xs -> m (Match a)
m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Block BlockedOnResult
s BlockingVars
ys -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
choiceBlockedOnResult BlockedOnResult
r BlockedOnResult
s) (BlockingVars -> Match a) -> BlockingVars -> Match a
forall a b. (a -> b) -> a -> b
$ BlockingVars -> BlockingVars -> BlockingVars
zipBlockingVars BlockingVars
xs BlockingVars
ys
    Yes a
_      -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult
setBlockedOnResultOverlap BlockedOnResult
r) (BlockingVars -> Match a) -> BlockingVars -> Match a
forall a b. (a -> b) -> a -> b
$ BlockingVars -> BlockingVars
overlapping BlockingVars
xs
    Match a
No         -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block BlockedOnResult
r BlockingVars
xs
  Match a
No    -> m (Match a)
m'

{-# SPECIALIZE matchClause :: [NamedArg SplitPattern] -> Clause -> TCM MatchResult #-}
matchClause
  :: PureTCM m
  => [NamedArg SplitPattern]
     -- ^ Split clause patterns @qs@.
  -> Clause
     -- ^ Clause @c@ to cover split clause.
  -> m MatchResult
     -- ^ Result.
     --   If 'Yes' the instantiation @rs@ such that @(namedClausePats c)[rs] == qs@.
matchClause :: forall (m :: * -> *).
PureTCM m =>
[NamedArg SplitPattern]
-> Clause -> m (Match (DList (Nat, SplitPattern)))
matchClause [NamedArg SplitPattern]
qs Clause
c = [NamedArg DeBruijnPattern]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
matchPats (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
c) [NamedArg SplitPattern]
qs

{-# SPECIALIZE matchPats :: DeBruijn a => [NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> TCM MatchResult #-}
-- | @matchPats ps qs@ checks whether a function clause with patterns
--   @ps@ covers a split clause with patterns @qs@.
--
--   Issue #842 / #1986: This is accepted:
--   @
--     F : Bool -> Set1
--     F true = Set
--     F      = \ x -> Set
--   @
--   For the second clause, the split clause is @F false@,
--   so there are more patterns in the split clause than
--   in the considered clause.  These additional patterns
--   are simply dropped by @zipWith@.  This will result
--   in @mconcat []@ which is @Yes []@.

matchPats
  :: (PureTCM m, DeBruijn a)
  => [NamedArg (Pattern' a)]
     -- ^ Clause pattern vector @ps@ (to cover split clause pattern vector).
  -> [NamedArg SplitPattern]
     -- ^ Split clause pattern vector @qs@ (to be covered by clause pattern vector).
  -> m MatchResult
     -- ^ Result.
     --   If 'Yes' the instantiation @rs@ such that @ps[rs] == qs@.
matchPats :: forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
matchPats [] [] = DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes DList (Nat, SplitPattern)
forall a. Monoid a => a
mempty
matchPats (NamedArg (Pattern' a)
p:[NamedArg (Pattern' a)]
ps) (NamedArg SplitPattern
q:[NamedArg SplitPattern]
qs) =
  Pattern' a -> SplitPattern -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
Pattern' a -> SplitPattern -> m (Match (DList (Nat, SplitPattern)))
matchPat (NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p) (NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
q) m (Match (DList (Nat, SplitPattern)))
-> m (Match (DList (Nat, SplitPattern)))
-> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(Monad m, Semigroup a) =>
m (Match a) -> m (Match a) -> m (Match a)
`combine` [NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
matchPats [NamedArg (Pattern' a)]
ps [NamedArg SplitPattern]
qs

-- Patterns left in split clause:
-- Andreas, 2016-06-03, issue #1986:
-- catch-all for copatterns is inconsistent as found by Ulf.
-- Thus, if the split clause has copatterns left,
-- the current (shorter) clause is not considered covering.
matchPats [] qs :: [NamedArg SplitPattern]
qs@(NamedArg SplitPattern
_:[NamedArg SplitPattern]
_) = case (NamedArg SplitPattern -> Maybe (ProjOrigin, AmbiguousQName))
-> [NamedArg SplitPattern] -> [(ProjOrigin, AmbiguousQName)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe NamedArg SplitPattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP [NamedArg SplitPattern]
qs of
  [] -> DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes DList (Nat, SplitPattern)
forall a. Monoid a => a
mempty -- no proj. patterns left
  [(ProjOrigin, AmbiguousQName)]
_  -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no         -- proj. patterns left

-- Patterns left in candidate clause:
-- If the current clause has additional copatterns in
-- comparison to the split clause, we should split on them.
matchPats (NamedArg (Pattern' a)
p:[NamedArg (Pattern' a)]
ps) [] = case NamedArg (Pattern' a) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg (Pattern' a)
p of
  Just{}  -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
blockedOnProjection
  Maybe (ProjOrigin, AmbiguousQName)
Nothing -> ApplyOrIApply -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => ApplyOrIApply -> m (Match a)
blockedOnApplication (case NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p of IApplyP{} -> ApplyOrIApply
IsIApply; Pattern' a
_ -> ApplyOrIApply
IsApply)

-- | Combine results of checking whether function clause patterns
--   covers split clause patterns.
--
--   'No' is dominant: if one function clause pattern is disjoint to
--   the corresponding split clause pattern, then
--   the whole clauses are disjoint.
--
--   'Yes' is neutral: for a match, all patterns have to match.
--
--   'Block' accumulates variables of the split clause
--   that have to be instantiated (an projection names of copattern matches)
--   to make the split clause an instance of the function clause.
combine :: (Monad m, Semigroup a) => m (Match a) -> m (Match a) -> m (Match a)
combine :: forall (m :: * -> *) a.
(Monad m, Semigroup a) =>
m (Match a) -> m (Match a) -> m (Match a)
combine m (Match a)
m m (Match a)
m' = m (Match a)
m m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Yes a
a -> m (Match a)
m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Yes a
b -> a -> m (Match a)
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
      Match a
y     -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Match a
y
    Match a
No    -> m (Match a)
forall (m :: * -> *) a. Monad m => m (Match a)
no
    x :: Match a
x@(Block BlockedOnResult
r BlockingVars
xs) -> m (Match a)
m' m (Match a) -> (Match a -> m (Match a)) -> m (Match a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Match a
No    -> m (Match a)
forall (m :: * -> *) a. Monad m => m (Match a)
no
      Block BlockedOnResult
s BlockingVars
ys -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match a -> m (Match a)) -> Match a -> m (Match a)
forall a b. (a -> b) -> a -> b
$ BlockedOnResult -> BlockingVars -> Match a
forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
anyBlockedOnResult BlockedOnResult
r BlockedOnResult
s) (BlockingVars
xs BlockingVars -> BlockingVars -> BlockingVars
forall a. [a] -> [a] -> [a]
++ BlockingVars
ys)
      Yes{} -> Match a -> m (Match a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Match a
x

{-# SPECIALIZE matchPat :: DeBruijn a => Pattern' a -> SplitPattern -> TCM MatchResult #-}
-- | @matchPat p q@ checks whether a function clause pattern @p@
--   covers a split clause pattern @q@.  There are three results:
--
--   1. @Yes rs@ means it covers, because @p@ is a variable pattern. @rs@ collects
--      the instantiations of the variables in @p@ s.t. @p[rs] = q@.
--
--   2. @No@ means it does not cover.
--
--   3. @Block [x]@ means @p@ is a proper instance of @q@ and could become
--      a cover if @q@ was split on variable @x@.

matchPat
  :: (PureTCM m, DeBruijn a)
  => Pattern' a
     -- ^ Clause pattern @p@ (to cover split clause pattern).
  -> SplitPattern
     -- ^ Split clause pattern @q@ (to be covered by clause pattern).
  -> m MatchResult
     -- ^ Result.
     --   If 'Yes', also the instantiation @rs@ of the clause pattern variables
     --   to produce the split clause pattern, @p[rs] = q@.
matchPat :: forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
Pattern' a -> SplitPattern -> m (Match (DList (Nat, SplitPattern)))
matchPat Pattern' a
p SplitPattern
q = case Pattern' a
p of

  VarP PatternInfo
_ a
x ->
    DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes (DList (Nat, SplitPattern)
 -> m (Match (DList (Nat, SplitPattern))))
-> DList (Nat, SplitPattern)
-> m (Match (DList (Nat, SplitPattern)))
forall a b. (a -> b) -> a -> b
$ (Nat, SplitPattern) -> DList (Nat, SplitPattern)
forall el coll. Singleton el coll => el -> coll
singleton (Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
forall a. HasCallStack => a
__IMPOSSIBLE__ (a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
x), SplitPattern
q)

  DotP{} -> DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes DList (Nat, SplitPattern)
forall a. Monoid a => a
mempty
  -- Jesper, 2014-11-04: putting 'Yes [q]' here triggers issue 1333.
  -- Not checking for trivial patterns should be safe here, as dot patterns are
  -- guaranteed to match if the rest of the pattern does, so some extra splitting
  -- on them doesn't change the reduction behaviour.

  p :: Pattern' a
p@(LitP PatternInfo
_ Literal
l) -> case SplitPattern
q of
    VarP PatternInfo
_ SplitPatVar
x -> if Literal
l Literal -> [Literal] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x
                then m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
                else Nat -> Literal -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => Nat -> Literal -> m (Match a)
blockedOnLiteral (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x) Literal
l
    SplitPattern
_ -> SplitPattern -> m (Maybe Literal)
forall (m :: * -> *) a.
PureTCM m =>
Pattern' a -> m (Maybe Literal)
isLitP SplitPattern
q m (Maybe Literal)
-> (Maybe Literal -> m (Match (DList (Nat, SplitPattern))))
-> m (Match (DList (Nat, SplitPattern)))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Literal
l' -> if Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l' then DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes DList (Nat, SplitPattern)
forall a. Monoid a => a
mempty else m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
      Maybe Literal
Nothing -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no

  ProjP ProjOrigin
_ QName
d -> case SplitPattern
q of
    ProjP ProjOrigin
_ QName
d' -> do
      QName
d <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
      if QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' then DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes DList (Nat, SplitPattern)
forall a. Monoid a => a
mempty else m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    SplitPattern
_          -> m (Match (DList (Nat, SplitPattern)))
forall a. HasCallStack => a
__IMPOSSIBLE__

  IApplyP PatternInfo
_ Term
_ Term
_ a
x ->
    DList (Nat, SplitPattern) -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes (DList (Nat, SplitPattern)
 -> m (Match (DList (Nat, SplitPattern))))
-> DList (Nat, SplitPattern)
-> m (Match (DList (Nat, SplitPattern)))
forall a b. (a -> b) -> a -> b
$ (Nat, SplitPattern) -> DList (Nat, SplitPattern)
forall el coll. Singleton el coll => el -> coll
singleton (Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
forall a. HasCallStack => a
__IMPOSSIBLE__ (a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
x), SplitPattern
q)

                           --    Issue #4179: If the inferred pattern is a literal
                           -- v  we need to turn it into a constructor pattern.
  ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)]
ps -> SplitPattern -> m SplitPattern
forall (m :: * -> *) a.
(MonadReduce m, DeBruijn a) =>
Pattern' a -> m (Pattern' a)
unDotP SplitPattern
q m SplitPattern
-> (SplitPattern -> m SplitPattern) -> m SplitPattern
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SplitPattern -> m SplitPattern
forall (m :: * -> *) a.
HasBuiltins m =>
Pattern' a -> m (Pattern' a)
unLitP m SplitPattern
-> (SplitPattern -> m (Match (DList (Nat, SplitPattern))))
-> m (Match (DList (Nat, SplitPattern)))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    VarP PatternInfo
_ SplitPatVar
x -> Nat
-> ConHead
-> ConPatternInfo
-> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
Monad m =>
Nat -> ConHead -> ConPatternInfo -> m (Match a)
blockedOnConstructor (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x) ConHead
c ConPatternInfo
ci
    ConP ConHead
c' ConPatternInfo
i [NamedArg SplitPattern]
qs
      | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c'   -> [NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
matchPats [NamedArg (Pattern' a)]
ps [NamedArg SplitPattern]
qs
      | Bool
otherwise -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    DotP PatternInfo
o Term
t  -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    DefP{}   -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    LitP{}    -> m (Match (DList (Nat, SplitPattern)))
forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing and unLitP
    ProjP{}   -> m (Match (DList (Nat, SplitPattern)))
forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing
    IApplyP PatternInfo
_ Term
_ Term
_ SplitPatVar
x -> Nat
-> ConHead
-> ConPatternInfo
-> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
Monad m =>
Nat -> ConHead -> ConPatternInfo -> m (Match a)
blockedOnConstructor (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x) ConHead
c ConPatternInfo
ci

  DefP PatternInfo
o QName
c [NamedArg (Pattern' a)]
ps -> SplitPattern -> m SplitPattern
forall (m :: * -> *) a.
(MonadReduce m, DeBruijn a) =>
Pattern' a -> m (Pattern' a)
unDotP SplitPattern
q m SplitPattern
-> (SplitPattern -> m (Match (DList (Nat, SplitPattern))))
-> m (Match (DList (Nat, SplitPattern)))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    VarP PatternInfo
_ SplitPatVar
x -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    ConP ConHead
c' ConPatternInfo
i [NamedArg SplitPattern]
qs -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    DotP PatternInfo
o Term
t  -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    LitP{}    -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    DefP PatternInfo
o QName
c' [NamedArg SplitPattern]
qs
      | QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
c'   -> [NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)]
-> [NamedArg SplitPattern] -> m (Match (DList (Nat, SplitPattern)))
matchPats [NamedArg (Pattern' a)]
ps [NamedArg SplitPattern]
qs
      | Bool
otherwise -> m (Match (DList (Nat, SplitPattern)))
forall (m :: * -> *) a. Monad m => m (Match a)
no
    ProjP{}   -> m (Match (DList (Nat, SplitPattern)))
forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing
    IApplyP PatternInfo
_ Term
_ Term
_ SplitPatVar
x -> m (Match (DList (Nat, SplitPattern)))
forall a. HasCallStack => a
__IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c

{-# SPECIALIZE unDotP :: DeBruijn a => Pattern' a -> TCM (Pattern' a) #-}
-- | Unfold one level of a dot pattern to a proper pattern if possible.
unDotP :: (MonadReduce m, DeBruijn a) => Pattern' a -> m (Pattern' a)
unDotP :: forall (m :: * -> *) a.
(MonadReduce m, DeBruijn a) =>
Pattern' a -> m (Pattern' a)
unDotP (DotP PatternInfo
o Term
v) = Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v m Term -> (Term -> m (Pattern' a)) -> m (Pattern' a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Var Nat
i [] -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Nat -> Pattern' a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i
  Con ConHead
c ConInfo
_ [Elim]
vs -> do
    let ps :: [Arg (Named NamedName (Pattern' a))]
ps = (Arg Term -> Arg (Named NamedName (Pattern' a)))
-> [Arg Term] -> [Arg (Named NamedName (Pattern' a))]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Named NamedName (Pattern' a))
-> Arg Term -> Arg (Named NamedName (Pattern' a))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> Named NamedName (Pattern' a))
 -> Arg Term -> Arg (Named NamedName (Pattern' a)))
-> (Term -> Named NamedName (Pattern' a))
-> Arg Term
-> Arg (Named NamedName (Pattern' a))
forall a b. (a -> b) -> a -> b
$ Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed (Pattern' a -> Named NamedName (Pattern' a))
-> (Term -> Pattern' a) -> Term -> Named NamedName (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o) ([Arg Term] -> [Arg (Named NamedName (Pattern' a))])
-> [Arg Term] -> [Arg (Named NamedName (Pattern' a))]
forall a b. (a -> b) -> a -> b
$ [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
$ [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
vs
    Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ ConHead
-> ConPatternInfo
-> [Arg (Named NamedName (Pattern' a))]
-> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo [Arg (Named NamedName (Pattern' a))]
ps
  Lit Literal
l -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatODot []) Literal
l
  Term
v     -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
unDotP Pattern' a
p = Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p

{-# SPECIALIZE isLitP :: Pattern' a -> TCM (Maybe Literal) #-}
isLitP :: PureTCM m => Pattern' a -> m (Maybe Literal)
isLitP :: forall (m :: * -> *) a.
PureTCM m =>
Pattern' a -> m (Maybe Literal)
isLitP (LitP PatternInfo
_ Literal
l) = Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Literal -> m (Maybe Literal))
-> Maybe Literal -> m (Maybe Literal)
forall a b. (a -> b) -> a -> b
$ Literal -> Maybe Literal
forall a. a -> Maybe a
Just Literal
l
isLitP (DotP PatternInfo
_ Term
u) = Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u m Term -> (Term -> m (Maybe Literal)) -> m (Maybe Literal)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Lit Literal
l -> Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Literal -> m (Maybe Literal))
-> Maybe Literal -> m (Maybe Literal)
forall a b. (a -> b) -> a -> b
$ Literal -> Maybe Literal
forall a. a -> Maybe a
Just Literal
l
  Term
_ -> Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Literal -> m (Maybe Literal))
-> Maybe Literal -> m (Maybe Literal)
forall a b. (a -> b) -> a -> b
$ Maybe Literal
forall a. Maybe a
Nothing
isLitP (ConP ConHead
c ConPatternInfo
ci []) = do
  Con ConHead
zero ConInfo
_ [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
  if ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
zero
    then Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Literal -> m (Maybe Literal))
-> Maybe Literal -> m (Maybe Literal)
forall a b. (a -> b) -> a -> b
$ Literal -> Maybe Literal
forall a. a -> Maybe a
Just (Literal -> Maybe Literal) -> Literal -> Maybe Literal
forall a b. (a -> b) -> a -> b
$ Integer -> Literal
LitNat Integer
0
    else Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Literal
forall a. Maybe a
Nothing
isLitP (ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)
a]) | NamedArg (Pattern' a) -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg (Pattern' a)
a Bool -> Bool -> Bool
&& NamedArg (Pattern' a) -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant NamedArg (Pattern' a)
a = do
  Con ConHead
suc ConInfo
_ [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc
  if ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
suc
    then (Literal -> Literal) -> Maybe Literal -> Maybe Literal
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Literal -> Literal
inc (Maybe Literal -> Maybe Literal)
-> m (Maybe Literal) -> m (Maybe Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' a -> m (Maybe Literal)
forall (m :: * -> *) a.
PureTCM m =>
Pattern' a -> m (Maybe Literal)
isLitP (NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
a)
    else Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Literal
forall a. Maybe a
Nothing
  where
    inc :: Literal -> Literal
    inc :: Literal -> Literal
inc (LitNat Integer
n) = Integer -> Literal
LitNat (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    inc Literal
_ = Literal
forall a. HasCallStack => a
__IMPOSSIBLE__
isLitP Pattern' a
_ = Maybe Literal -> m (Maybe Literal)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Literal
forall a. Maybe a
Nothing

{-# SPECIALIZE unLitP :: Pattern' a -> TCM (Pattern' a) #-}
unLitP :: HasBuiltins m => Pattern' a -> m (Pattern' a)
unLitP :: forall (m :: * -> *) a.
HasBuiltins m =>
Pattern' a -> m (Pattern' a)
unLitP (LitP PatternInfo
info l :: Literal
l@(LitNat Integer
n)) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = do
  Con ConHead
c ConInfo
ci [Elim]
es <- m Term -> m Term -> Term -> m Term
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero)
                                  (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc)
                                  (Literal -> Term
Lit Literal
l)
  let toP :: Elim -> Arg (Pattern' a)
toP (Apply (Arg ArgInfo
i (Lit Literal
l))) = ArgInfo -> Pattern' a -> Arg (Pattern' a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
info Literal
l)
      toP Elim
_ = Arg (Pattern' a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      cpi :: ConPatternInfo
cpi   = ConPatternInfo
noConPatternInfo { conPInfo = info }
  Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (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
cpi ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (Elim -> NamedArg (Pattern' a))
-> [Elim] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' a -> Named_ (Pattern' a))
-> Arg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' a -> Named_ (Pattern' a)
forall a name. a -> Named name a
unnamed (Arg (Pattern' a) -> NamedArg (Pattern' a))
-> (Elim -> Arg (Pattern' a)) -> Elim -> NamedArg (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim -> Arg (Pattern' a)
toP) [Elim]
es
unLitP Pattern' a
p = Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p