{-| 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 Control.Monad.State

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.Syntax.Position

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.Utils.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 -> 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
<$ :: forall a b. a -> Match b -> Match a
$c<$ :: forall a b. a -> Match b -> Match a
fmap :: forall a b. (a -> b) -> Match a -> Match b
$cfmap :: forall a b. (a -> b) -> Match a -> Match b
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
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: BlockingVars -> ShowS
$cshowList :: BlockingVars -> ShowS
show :: BlockingVar -> String
$cshow :: BlockingVar -> String
showsPrec :: Nat -> BlockingVar -> ShowS
$cshowsPrec :: Nat -> BlockingVar -> ShowS
Show)

type BlockingVars = [BlockingVar]

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

-- | 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall (m :: * -> *) a.
Monad m =>
m (Match a) -> m (Match a) -> m (Match a)
choice (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Match a
No) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\DList (Nat, SplitPattern)
s -> (Nat
i, forall (t :: * -> *) a. Foldable t => t a -> [a]
toList DList (Nat, SplitPattern)
s)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
[NamedArg SplitPattern] -> Clause -> m MatchResult
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
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SplitPatVar] -> ShowS
$cshowList :: [SplitPatVar] -> ShowS
show :: SplitPatVar -> String
$cshow :: SplitPatVar -> String
showsPrec :: Nat -> SplitPatVar -> ShowS
$cshowsPrec :: Nat -> SplitPatVar -> ShowS
Show)

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

instance PrettyTCM SplitPatVar where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitPatVar -> m Doc
prettyTCM = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Term
var 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 = 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 (forall a. DeBruijn a => String -> Nat -> a
debruijnNamedVar String
n Nat
i)

toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DBPatVar -> SplitPatVar
toSplitVar

fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst 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 = forall a. a -> a
id
  applySubst Substitution' (SubstArg SplitPattern)
rho = \case
    VarP PatternInfo
i SplitPatVar
x        ->
      forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i forall a b. (a -> b) -> a -> b
$
      String -> SplitPattern -> SplitPattern
useName (SplitPatVar -> String
splitPatVarName SplitPatVar
x) forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) forall a b. (a -> b) -> a -> b
$
      forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' (SubstArg SplitPattern)
rho forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x
    DotP PatternInfo
i Term
u        -> forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst Substitution' (SubstArg SplitPattern)
rho Term
u
    ConP ConHead
c ConPatternInfo
ci [NamedArg SplitPattern]
ps    -> forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg SplitPattern)
rho [NamedArg SplitPattern]
ps
    DefP PatternInfo
i QName
q [NamedArg SplitPattern]
ps     -> forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst 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 (forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst Substitution' (SubstArg SplitPattern)
rho Term
l) (forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst Substitution' (SubstArg SplitPattern)
rho Term
r) forall a b. (a -> b) -> a -> b
$
      forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i forall a b. (a -> b) -> a -> b
$
      String -> SplitPattern -> SplitPattern
useName (SplitPatVar -> String
splitPatVarName SplitPatVar
x) forall a b. (a -> b) -> a -> b
$
      [Literal] -> SplitPattern -> SplitPattern
useExcludedLits (SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x) forall a b. (a -> b) -> a -> b
$
      forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' (SubstArg SplitPattern)
rho 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)        = 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) = forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
l Term
r SplitPatVar
x
      useEndPoints Term
l Term
r SplitPattern
x                 = forall a. HasCallStack => a
__IMPOSSIBLE__

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

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


-- | 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{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  DotP{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall a b. (a -> b) -> a -> b
$ ((ConPatternInfo -> Bool
conPLazy ConPatternInfo
i Bool -> Bool -> Bool
||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaCon (ConHead -> QName
conName ConHead
c))
                      forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps)
  DefP{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  LitP{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  ProjP{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  IApplyP{}   -> 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
cat
    [ String -> Doc
text (String
"variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Nat
i)
    , if forall a. Null a => a -> Bool
null [ConHead]
cs then forall a. Null a => a
empty else Doc
" blocked on constructors" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty [ConHead]
cs
    , if forall a. Null a => a -> Bool
null [Literal]
ls then forall a. Null a => a
empty else Doc
" blocked on literals" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty [Literal]
ls
    , if Bool
o then Doc
" (overlapping)" else forall a. Null a => a
empty
    , if Bool
l then Doc
" (lazy)" else forall a. Null a => a
empty
    ]

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

no :: Monad m => m (Match a)
no :: forall (m :: * -> *) a. Monad m => m (Match a)
no = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlockedOnResult -> BlockingVars -> Match a
Block BlockedOnResult
NotBlockedOnResult [Nat -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Nat
i [ConHead
c] [] Bool
False 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 :: Bool
blockingVarOverlap = Bool
True }

overlapping :: BlockingVars -> BlockingVars
overlapping :: BlockingVars -> BlockingVars
overlapping = 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 = 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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Nat
x forall a. Eq a => a -> a -> 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 forall a. [a] -> [a] -> [a]
++ [ConHead]
cons') ([Literal]
lits 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 :: Bool
blockedOnResultOverlap = Bool
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
_                 ) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Yes a
a -> forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes a
a
  Block BlockedOnResult
r BlockingVars
xs -> m (Match a)
m' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Block BlockedOnResult
s BlockingVars
ys -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
choiceBlockedOnResult BlockedOnResult
r BlockedOnResult
s) forall a b. (a -> b) -> a -> b
$ BlockingVars -> BlockingVars -> BlockingVars
zipBlockingVars BlockingVars
xs BlockingVars
ys
    Yes a
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult
setBlockedOnResultOverlap BlockedOnResult
r) forall a b. (a -> b) -> a -> b
$ BlockingVars -> BlockingVars
overlapping BlockingVars
xs
    Match a
No         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlockedOnResult -> BlockingVars -> Match a
Block BlockedOnResult
r BlockingVars
xs
  Match a
No    -> m (Match a)
m'

-- | @matchClause qs i c@ checks whether clause @c@
--   covers a split clause with patterns @qs@.
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 MatchResult
matchClause [NamedArg SplitPattern]
qs Clause
c = forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> m MatchResult
matchPats (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
c) [NamedArg SplitPattern]
qs


-- | @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 MatchResult
matchPats [] [] = forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes forall a. Monoid a => a
mempty
matchPats (NamedArg (Pattern' a)
p:[NamedArg (Pattern' a)]
ps) (NamedArg SplitPattern
q:[NamedArg SplitPattern]
qs) =
  forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
Pattern' a -> SplitPattern -> m MatchResult
matchPat (forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
p) (forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
q) forall (m :: * -> *) a.
(Monad m, Semigroup a) =>
m (Match a) -> m (Match a) -> m (Match a)
`combine` forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> m MatchResult
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 forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP [NamedArg SplitPattern]
qs of
  [] -> forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes forall a. Monoid a => a
mempty -- no proj. patterns left
  [(ProjOrigin, AmbiguousQName)]
_  -> 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 forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg (Pattern' a)
p of
  Just{}  -> forall (m :: * -> *) a. Monad m => m (Match a)
blockedOnProjection
  Maybe (ProjOrigin, AmbiguousQName)
Nothing -> forall (m :: * -> *) a. Monad m => ApplyOrIApply -> m (Match a)
blockedOnApplication (case 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Yes a
a -> m (Match a)
m' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Yes a
b -> forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes (a
a forall a. Semigroup a => a -> a -> a
<> a
b)
      Match a
y     -> forall (m :: * -> *) a. Monad m => a -> m a
return Match a
y
    Match a
No    -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    x :: Match a
x@(Block BlockedOnResult
r BlockingVars
xs) -> m (Match a)
m' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Match a
No    -> forall (m :: * -> *) a. Monad m => m (Match a)
no
      Block BlockedOnResult
s BlockingVars
ys -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlockedOnResult -> BlockingVars -> Match a
Block (BlockedOnResult -> BlockedOnResult -> BlockedOnResult
anyBlockedOnResult BlockedOnResult
r BlockedOnResult
s) (BlockingVars
xs forall a. [a] -> [a] -> [a]
++ BlockingVars
ys)
      Yes{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Match a
x

-- | @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 MatchResult
matchPat Pattern' a
p SplitPattern
q = case Pattern' a
p of

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

  DotP{} -> forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SplitPatVar -> [Literal]
splitExcludedLits SplitPatVar
x
                then forall (m :: * -> *) a. Monad m => m (Match a)
no
                else forall (m :: * -> *) a. Monad m => Nat -> Literal -> m (Match a)
blockedOnLiteral (SplitPatVar -> Nat
splitPatVarIndex SplitPatVar
x) Literal
l
    SplitPattern
_ -> forall (m :: * -> *) a.
PureTCM m =>
Pattern' a -> m (Maybe Literal)
isLitP SplitPattern
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Literal
l' -> if Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l' then forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes forall a. Monoid a => a
mempty else forall (m :: * -> *) a. Monad m => m (Match a)
no
      Maybe Literal
Nothing -> forall (m :: * -> *) a. Monad m => m (Match a)
no

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

  IApplyP PatternInfo
_ Term
_ Term
_ a
x ->
    forall (m :: * -> *) a. Monad m => a -> m (Match a)
yes forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ (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 -> forall (m :: * -> *) a.
(MonadReduce m, DeBruijn a) =>
Pattern' a -> m (Pattern' a)
unDotP SplitPattern
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a.
HasBuiltins m =>
Pattern' a -> m (Pattern' a)
unLitP forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    VarP PatternInfo
_ SplitPatVar
x -> 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 forall a. Eq a => a -> a -> Bool
== ConHead
c'   -> forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> m MatchResult
matchPats [NamedArg (Pattern' a)]
ps [NamedArg SplitPattern]
qs
      | Bool
otherwise -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    DotP PatternInfo
o Term
t  -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    DefP{}   -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    LitP{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing and unLitP
    ProjP{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing
    IApplyP PatternInfo
_ Term
_ Term
_ SplitPatVar
x -> 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 -> forall (m :: * -> *) a.
(MonadReduce m, DeBruijn a) =>
Pattern' a -> m (Pattern' a)
unDotP SplitPattern
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    VarP PatternInfo
_ SplitPatVar
x -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    ConP ConHead
c' ConPatternInfo
i [NamedArg SplitPattern]
qs -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    DotP PatternInfo
o Term
t  -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    LitP{}    -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    DefP PatternInfo
o QName
c' [NamedArg SplitPattern]
qs
      | QName
c forall a. Eq a => a -> a -> Bool
== QName
c'   -> forall (m :: * -> *) a.
(PureTCM m, DeBruijn a) =>
[NamedArg (Pattern' a)] -> [NamedArg SplitPattern] -> m MatchResult
matchPats [NamedArg (Pattern' a)]
ps [NamedArg SplitPattern]
qs
      | Bool
otherwise -> forall (m :: * -> *) a. Monad m => m (Match a)
no
    ProjP{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- excluded by typing
    IApplyP PatternInfo
_ Term
_ Term
_ SplitPatVar
x -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c

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

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

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