{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

{- | Various utility functions dealing with the non-linear, higher-order
     patterns used for rewrite rules.
-}

module Agda.TypeChecking.Rewriting.NonLinPattern where

import Prelude hiding ( null )

import Data.Foldable (Foldable(fold))

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Defs
import Agda.Syntax.Internal.MetaVars ( AllMetas, unblockOnAllMetasIn )

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance ( isDefSing, isPatternVar )
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive.Cubical.Base

import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.VarSet (VarSet)

-- | Turn a term into a non-linear pattern, treating the
--   free variables as pattern variables.
--   The first two arguments indicate whether the pattern we are under is
--   definitionally singular. Specifically, the first tracks the definitional
--   singularity of the last |PDef|/|PBoundVar| match, while the second tracks
--   the current definitional singularity.
--   The third argument and fourth arguments, k0 and k1, partition the context
--   into three chunks: the local context, the telescope of
--   of pattern variables associated with the rewrite and the pattern-lambda
--   bound variables.
--   The fifth argument is the type of the term.

class PatternFrom a b where
  patternFrom :: DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b

instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
  patternFrom :: DefSing
-> DefSing -> Int -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b)
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf (Arg a)
t Arg a
u
    = let r1' :: DefSing
r1' = DefSing
r1 DefSing -> DefSing -> DefSing
`maxDefSing` Relevance -> DefSing
relToDefSing (Arg a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
u)
      in  (a -> TCMT IO b) -> Arg a -> TCM (Arg b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1' Int
k0 Int
k1 (TypeOf a -> a -> TCMT IO b) -> TypeOf a -> a -> TCMT IO b
forall a b. (a -> b) -> a -> b
$ Dom' Term (TypeOf a) -> TypeOf a
forall t e. Dom' t e -> e
unDom TypeOf (Arg a)
Dom' Term (TypeOf a)
t) Arg a
u

instance PatternFrom Elims PElims where
  patternFrom :: DefSing
-> DefSing -> Int -> Int -> TypeOf Elims -> Elims -> TCM PElims
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 (Type'' Term Term
t,Elims -> Term
hd) = \case
    [] -> PElims -> TCM PElims
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Apply Arg Term
u : Elims
es) -> do
      (a, b) <- Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
assertPi Type'' Term Term
t
      p   <- patternFrom r0 r1 k0 k1 a u
      let t'  = Abs (Type'' Term Term)
-> SubstArg (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Type'' Term Term)
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)
      let hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
uElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
      ps  <- patternFrom r0 r1 k0 k1 (t',hd') es
      return $ Apply p : ps
    (IApply Term
x Term
y Term
i : Elims
es) -> do
      (s, q, l, b, u, v) <- Type'' Term Term
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type'' Term Term
t
      let t' = Sort -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
i ]
      let hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y Term
iElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
      interval <- primIntervalType
      p   <- patternFrom r0 r1 k0 k1 interval i
      ps  <- patternFrom r0 r1 k0 k1 (t',hd') es
      return $ IApply (PTerm x) (PTerm y) p : ps
    (Proj ProjOrigin
o QName
f : Elims
es) -> do
      (a,b) <- QName
-> Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
assertProjOf QName
f Type'' Term Term
t
      let u = Elims -> Term
hd []
          t' = Abs (Type'' Term Term)
b Abs (Type'' Term Term)
-> SubstArg (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg (Type'' Term Term)
u
      hd' <- applyDef o f (argFromDom a $> u)
      ps  <- patternFrom r0 r1 k0 k1 (t',applyE hd') es
      return $ Proj o f : ps

instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
  patternFrom :: DefSing
-> DefSing -> Int -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b)
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf (Dom a)
t = (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse ((a -> TCMT IO b) -> Dom a -> TCM (Dom b))
-> (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
forall a b. (a -> b) -> a -> b
$ DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf a
TypeOf (Dom a)
t

instance PatternFrom Type NLPType where
  patternFrom :: DefSing
-> DefSing
-> Int
-> Int
-> TypeOf (Type'' Term Term)
-> Type'' Term Term
-> TCM NLPType
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf (Type'' Term Term)
_ Type'' Term Term
a = TCM NLPType -> TCM NLPType
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM NLPType -> TCM NLPType) -> TCM NLPType -> TCM NLPType
forall a b. (a -> b) -> a -> b
$
    NLPSort -> NLPat -> NLPType
NLPType (NLPSort -> NLPat -> NLPType)
-> TCMT IO NLPSort -> TCMT IO (NLPat -> NLPType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefSing
-> DefSing -> Int -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 () (Type'' Term Term -> Sort
forall a. LensSort a => a -> Sort
getSort Type'' Term Term
a)
            TCMT IO (NLPat -> NLPType) -> TCM NLPat -> TCM NLPType
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DefSing
-> DefSing -> Int -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 (Sort -> Type'' Term Term
sort (Sort -> Type'' Term Term) -> Sort -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Sort
forall a. LensSort a => a -> Sort
getSort Type'' Term Term
a) (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
a)

instance PatternFrom Sort NLPSort where
  patternFrom :: DefSing
-> DefSing -> Int -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf Sort
_ Sort
s = do
    s <- Sort -> TCMT IO Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Sort
s
    case s of
      Univ Univ
u Level' Term
l -> Univ -> NLPat -> NLPSort
PUniv Univ
u (NLPat -> NLPSort) -> TCM NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefSing
-> DefSing
-> Int
-> Int
-> TypeOf (Level' Term)
-> Level' Term
-> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 () Level' Term
l
      Inf Univ
u Integer
n  -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPSort -> TCMT IO NLPSort) -> NLPSort -> TCMT IO NLPSort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> NLPSort
PInf Univ
u Integer
n
      Sort
SizeUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
      Sort
LockUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLockUniv
      Sort
LevelUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLevelUniv
      Sort
IntervalUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PIntervalUniv
      PiSort Dom' Term Term
_ Sort
_ Abs Sort
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      FunSort Sort
_ Sort
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      UnivSort Sort
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaS{}  -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      DefS{}   -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      DummyS [Char]
s -> do
        [Char] -> Int -> [[Char]] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"impossible" Int
10
          [ [Char]
"patternFrom: hit dummy sort with content:"
          , [Char]
s
          ]
        TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__

instance PatternFrom Level NLPat where
  patternFrom :: DefSing
-> DefSing
-> Int
-> Int
-> TypeOf (Level' Term)
-> Level' Term
-> TCM NLPat
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf (Level' Term)
_ Level' Term
l = do
    t <- TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Type'' Term Term)
levelType
    v <- reallyUnLevelView l
    patternFrom r0 r1 k0 k1 t v

instance PatternFrom Term NLPat where
  patternFrom :: DefSing
-> DefSing -> Int -> Int -> TypeOf Term -> Term -> TCM NLPat
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 TypeOf Term
t Term
v = do
    t <- Type'' Term Term -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked TypeOf Term
Type'' Term Term
t
    etaRecord <- isEtaRecordType t
    r1 <- maxDefSing r1 <$> isDefSing k0 k1 t
    -- We need to handle the primRewriteNoMatch primitive specially so need to
    -- stop it reducing away
    v <- modifyAllowedReductions (SmallSet.delete RewriteNoMatchReductions) $
      unLevel =<< abortIfBlocked v
    reportSDoc "rewriting.build" 60 $ sep
      [ "building a pattern from term v = " <+> prettyTCM v
      , " of type " <+> prettyTCM t
      ]
    pview <- pathViewAsPi'whnf
    noMatchPrim <- getPrimitive' builtinRewriteNoMatch
    let isRewriteNoMatch QName
f = Bool -> (PrimFun -> Bool) -> Maybe PrimFun -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) QName
f (QName -> Bool) -> (PrimFun -> QName) -> PrimFun -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimFun -> QName
primFunName) Maybe PrimFun
noMatchPrim
    let done = Term -> TCMT IO ()
forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn Term
v TCMT IO () -> TCM NLPat -> TCM NLPat
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> NLPat -> TCM NLPat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> NLPat
PTerm Term
v)
    case (unEl t , stripDontCare v) of
      (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b , Term
_) -> do
        let body :: Term
body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (Type'' Term Term)
a) (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        p <- Dom (Type'' Term Term) -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Dom (Type'' Term Term) -> m a -> m a
addContext Dom (Type'' Term Term)
a (DefSing
-> DefSing -> Int -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 (Int
k0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
k1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b) Term
body)
        return $ PLam (domInfo a) $ Abs (absName b) p
      (Term, Term)
_ | Left ((Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b),(Term
x,Term
y)) <- Type'' Term Term
-> Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term)
pview Type'' Term Term
t -> do
        let body :: Term
body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
x) (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
y) (Term -> Elim' Term) -> Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        p <- Dom (Type'' Term Term) -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Dom (Type'' Term Term) -> m a -> m a
addContext Dom (Type'' Term Term)
a (DefSing
-> DefSing -> Int -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 (Int
k0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
k1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b) Term
body)
        return $ PLam (domInfo a) $ Abs (absName b) p
      (Term
_ , Var Int
i Elims
es)
       -- Variables before k0 are locally bound outside the rewrite telescope
       -- Variables after k1 are bound in higher order patterns
       | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Bool
isPatternVar Int
k0 Int
k1 Int
i -> do
           t <- Int -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
i
           PBoundVar i <$> patternFrom r1 r1 k0 k1 (t , Var i) es
       -- The arguments of `var i` should be distinct bound variables
       -- in order to build a Miller pattern
       | Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
           TelV tel rest <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telViewPath (Type'' Term Term -> TCMT IO (TelV (Type'' Term Term)))
-> TCMT IO (Type'' Term Term) -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
i
           unless (natSize tel >= natSize vs) $ blockOnMetasIn rest >> addContext tel (errNotPi rest)
           let ts = Substitution' (SubstArg [Type'' Term Term])
-> [Type'' Term Term] -> [Type'' Term Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([SubstArg [Type'' Term Term]]
-> Substitution' (SubstArg [Type'' Term Term])
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg [Type'' Term Term]]
 -> Substitution' (SubstArg [Type'' Term Term]))
-> [SubstArg [Type'' Term Term]]
-> Substitution' (SubstArg [Type'' Term Term])
forall a b. (a -> b) -> a -> b
$ [SubstArg [Type'' Term Term]] -> [SubstArg [Type'' Term Term]]
forall a. [a] -> [a]
reverse ([SubstArg [Type'' Term Term]] -> [SubstArg [Type'' Term Term]])
-> [SubstArg [Type'' Term Term]] -> [SubstArg [Type'' Term Term]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> SubstArg [Type'' Term Term])
-> Args -> [SubstArg [Type'' Term Term]]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
Arg Term -> SubstArg [Type'' Term Term]
forall e. Arg e -> e
unArg Args
vs) ([Type'' Term Term] -> [Type'' Term Term])
-> [Type'' Term Term] -> [Type'' Term Term]
forall a b. (a -> b) -> a -> b
$ (Dom (Type'' Term Term) -> Type'' Term Term)
-> [Dom (Type'' Term Term)] -> [Type'' Term Term]
forall a b. (a -> b) -> [a] -> [b]
map Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom ([Dom (Type'' Term Term)] -> [Type'' Term Term])
-> [Dom (Type'' Term Term)] -> [Type'' Term Term]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel
           mbvs <- forM (zip ts vs) $ \(Type'' Term Term
t , Arg Term
v) -> do
             (Arg Term, Type'' Term Term) -> TCMT IO ()
forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn (Arg Term
v,Type'' Term Term
t)
             Term -> Type'' Term Term -> TCMT IO (Maybe Int)
forall (m :: * -> *).
PureTCM m =>
Term -> Type'' Term Term -> m (Maybe Int)
isEtaVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) Type'' Term Term
t TCMT IO (Maybe Int)
-> (Maybe Int -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO (Maybe (Arg Int))
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               Just Int
j | Int
k0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k1 -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int)))
-> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall a b. (a -> b) -> a -> b
$ Arg Int -> Maybe (Arg Int)
forall a. a -> Maybe a
Just (Arg Int -> Maybe (Arg Int)) -> Arg Int -> Maybe (Arg Int)
forall a b. (a -> b) -> a -> b
$ Arg Term
v Arg Term -> Int -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
j
               Maybe Int
_                         -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Arg Int)
forall a. Maybe a
Nothing
           case sequence mbvs of
             Just [Arg Int]
bvs | [Arg Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Arg Int]
bvs -> do
               let allBoundVars :: VarSet
allBoundVars = Int -> VarSet
VarSet.full Int
k1
                   ok :: Bool
ok = Bool -> Bool
not (DefSing -> Bool
isAlwaysSing DefSing
r1) Bool -> Bool -> Bool
||
                        [Int] -> VarSet
VarSet.fromList ((Arg Int -> Int) -> [Arg Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Arg Int -> Int
forall e. Arg e -> e
unArg [Arg Int]
bvs) VarSet -> VarSet -> Bool
forall a. Eq a => a -> a -> Bool
== VarSet
allBoundVars
               if Bool
ok then NLPat -> TCM NLPat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DefSing -> Int -> [Arg Int] -> NLPat
PVar DefSing
r0 Int
i [Arg Int]
bvs) else TCM NLPat
done
                 -- Important: Definitional singularity at |PVar|s should be
                 -- that of the surrounding pattern (|r| rather than |r'|).
                 -- If only the variable itself might be definitionally singular
                 -- that is not a problem.
             Maybe [Arg Int]
_ -> TCM NLPat
done
       | Bool
otherwise -> TCM NLPat
done
      (Term
_ , Term
_ ) | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
        RecordDefn def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
        (tel, c, ci, vs) <- etaExpandRecord_ d pars def v
        ct <- assertConOf c t
        PDef (conName c) <$> patternFrom r1 r1 k0 k1 (ct , Con c ci) (map Apply vs)
      (Term
_ , Lam{})   -> Type'' Term Term -> TCM NLPat
forall a. Type'' Term Term -> TCM a
errNotPi Type'' Term Term
t
      (Term
_ , Lit{})   -> TCM NLPat
done
      -- Terms wrapped in the primRewriteNoMatch primitive are converted to PTerms
      -- (i.e. rather than matching, we will just test conversion)
      (Term
_ , Def QName
f (Elim' Term
l : Elim' Term
a : Apply Arg Term
x : Elims
es)) | QName -> Bool
isRewriteNoMatch QName
f ->
        NLPat -> TCM NLPat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCM NLPat) -> NLPat -> TCM NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x) Elims
es
      (Term
_ , Def QName
f Elims
es) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) -> do
        Def lsuc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
        Def lmax [] <- primLevelMax
        case es of
          [Elim' Term
x]     | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lsuc -> TCM NLPat
done
          [Elim' Term
x , Elim' Term
y] | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lmax -> TCM NLPat
done
          Elims
_                   -> do
            ft <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCMT IO (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
            PDef f <$> patternFrom r1 r1 k0 k1 (ft , Def f) es
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) -> do
        ct <- ConHead -> Type'' Term Term -> TCMT IO (Type'' Term Term)
assertConOf ConHead
c Type'' Term Term
t
        PDef (conName c) <$> patternFrom r1 r1 k0 k1 (ct , Con c ci) vs
      (Term
_ , Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b) -> do
        pa <- DefSing
-> DefSing
-> Int
-> Int
-> TypeOf (Dom (Type'' Term Term))
-> Dom (Type'' Term Term)
-> TCM (Dom' Term NLPType)
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 () Dom (Type'' Term Term)
a
        pb <- addContext a (patternFrom r0 r1 (k0 + 1) (k1 + 1) () $ absBody b)
        return $ PPi pa (Abs (absName b) pb)
      (Term
_ , Sort Sort
s)     -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> TCMT IO NLPSort -> TCM NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefSing
-> DefSing -> Int -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k0 Int
k1 () Sort
s
      (Term
_ , Level Level' Term
l)    -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , DontCare{}) -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , MetaV MetaId
m Elims
_)  -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Dummy DummyTermKind
s Elims
_)  -> [Char] -> TCM NLPat
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)

-- | Convert from a non-linear pattern to a term.

class NLPatToTerm p a where
  nlPatToTerm :: PureTCM m => p -> m a

  default nlPatToTerm ::
    ( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
    , PureTCM m
    ) => p -> m a
  nlPatToTerm = (p' -> m a') -> f p' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse p' -> m a'
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => p' -> m a'
nlPatToTerm

instance NLPatToTerm p a => NLPatToTerm [p] [a] where
instance NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) where
instance NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) where
instance NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) where
instance NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) where

instance NLPatToTerm Nat Term where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => Int -> m Term
nlPatToTerm = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> (Int -> Term) -> Int -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var

instance NLPatToTerm NLPat Term where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm = \case
    PVar DefSing
s Int
i [Arg Int]
xs    -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> m Args -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Int] -> m Args
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Arg Int] -> m Args
nlPatToTerm [Arg Int]
xs
    PTerm Term
u        -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    PDef QName
f PElims
es      -> (Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f) m Defn -> (Defn -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c } -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
es
      Defn
_                            -> QName -> Elims -> Term
Def QName
f (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
es
    PLam ArgInfo
i Abs NLPat
u       -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs NLPat -> m (Abs Term)
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => Abs NLPat -> m (Abs Term)
nlPatToTerm Abs NLPat
u
    PPi Dom' Term NLPType
a Abs NLPType
b        -> Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
Pi    (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term)
-> m (Dom (Type'' Term Term)) -> m (Abs (Type'' Term Term) -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term NLPType -> m (Dom (Type'' Term Term))
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *).
PureTCM m =>
Dom' Term NLPType -> m (Dom (Type'' Term Term))
nlPatToTerm Dom' Term NLPType
a m (Abs (Type'' Term Term) -> Term)
-> m (Abs (Type'' Term Term)) -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs NLPType -> m (Abs (Type'' Term Term))
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *).
PureTCM m =>
Abs NLPType -> m (Abs (Type'' Term Term))
nlPatToTerm Abs NLPType
b
    PSort NLPSort
s        -> Sort -> Term
Sort  (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m Sort
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
nlPatToTerm NLPSort
s
    PBoundVar Int
i PElims
es -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
es

instance NLPatToTerm NLPat Level where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPat -> m (Level' Term)
nlPatToTerm = NLPat -> m Term
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm (NLPat -> m Term)
-> (Term -> m (Level' Term)) -> NLPat -> m (Level' Term)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term -> m (Level' Term)
forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView

instance NLPatToTerm NLPType Type where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPType -> m (Type'' Term Term)
nlPatToTerm (NLPType NLPSort
s NLPat
a) = Sort -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type'' Term Term)
-> m Sort -> m (Term -> Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m Sort
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
nlPatToTerm NLPSort
s m (Term -> Type'' Term Term) -> m Term -> m (Type'' Term Term)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NLPat -> m Term
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm NLPat
a

instance NLPatToTerm NLPSort Sort where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
nlPatToTerm (PUniv Univ
u NLPat
l) = Univ -> Level' Term -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' Term -> Sort) -> m (Level' Term) -> m Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPat -> m (Level' Term)
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => NLPat -> m (Level' Term)
nlPatToTerm NLPat
l
  nlPatToTerm (PInf Univ
u Integer
n) = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
  nlPatToTerm NLPSort
PSizeUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
SizeUniv
  nlPatToTerm NLPSort
PLockUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
LockUniv
  nlPatToTerm NLPSort
PLevelUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
LevelUniv
  nlPatToTerm NLPSort
PIntervalUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
IntervalUniv

data PatVars = PatVars
  { PatVars -> VarSet
neverSingPatVars :: VarSet
      -- ^ Variables bound in never definitionally singular contexts
  , PatVars -> VarSet
maybeSingPatVars :: VarSet
      -- ^ Variables bound in possibly definitionally singular contexts
  }
  deriving (PatVars -> PatVars -> Bool
(PatVars -> PatVars -> Bool)
-> (PatVars -> PatVars -> Bool) -> Eq PatVars
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PatVars -> PatVars -> Bool
== :: PatVars -> PatVars -> Bool
$c/= :: PatVars -> PatVars -> Bool
/= :: PatVars -> PatVars -> Bool
Eq)

instance Null PatVars where
  empty :: PatVars
empty = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Null a => a
empty VarSet
forall a. Null a => a
empty
  null :: PatVars -> Bool
null (PatVars VarSet
ps VarSet
ps') = VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
ps Bool -> Bool -> Bool
&& VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
ps'

instance Semigroup PatVars where
  PatVars VarSet
ps VarSet
ps' <> :: PatVars -> PatVars -> PatVars
<> PatVars VarSet
qs VarSet
qs' = VarSet -> VarSet -> PatVars
PatVars (VarSet
ps VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
qs) (VarSet
ps' VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
qs')

instance Monoid PatVars where
  mempty :: PatVars
mempty = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Monoid a => a
mempty VarSet
forall a. Monoid a => a
mempty

instance Singleton (DefSing, Int) PatVars where
  singleton :: (DefSing, Int) -> PatVars
singleton (DefSing
NeverSing,  Int
x) = VarSet -> VarSet -> PatVars
PatVars (Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
x) VarSet
forall a. Null a => a
empty
  singleton (DefSing
MaybeSing,  Int
x) = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Null a => a
empty (Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
x)
  singleton (DefSing
AlwaysSing, Int
x) = PatVars
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Gather the set of pattern variables of a non-linear pattern
class NLPatVars a where
  nlPatVarsUnder :: Int -> a -> PatVars

  default nlPatVarsUnder ::
    ( NLPatVars p, Foldable f, Functor f, a ~ f p
    ) => Int -> a -> PatVars
  nlPatVarsUnder Int
k a
x = f PatVars -> PatVars
forall m. Monoid m => f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (f PatVars -> PatVars) -> f PatVars -> PatVars
forall a b. (a -> b) -> a -> b
$ Int -> p -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k (p -> PatVars) -> f p -> f PatVars
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a
f p
x

  nlPatVars :: a -> PatVars
  nlPatVars = Int -> a -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
0

instance NLPatVars NLPType where
  nlPatVarsUnder :: Int -> NLPType -> PatVars
nlPatVarsUnder Int
k (NLPType NLPSort
l NLPat
a) = Int -> (NLPSort, NLPat) -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k (NLPSort
l, NLPat
a)

instance NLPatVars NLPSort where
  nlPatVarsUnder :: Int -> NLPSort -> PatVars
nlPatVarsUnder Int
k = \case
    PUniv Univ
_ NLPat
l   -> Int -> NLPat -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k NLPat
l
    PInf Univ
f Integer
n  -> PatVars
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PLockUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PLevelUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> PatVars
forall a. Null a => a
empty

instance NLPatVars NLPat where
  nlPatVarsUnder :: Int -> NLPat -> PatVars
nlPatVarsUnder Int
k = \case
      PVar DefSing
s Int
i [Arg Int]
_     -> (DefSing, Int) -> PatVars
forall el coll. Singleton el coll => el -> coll
singleton (DefSing
s, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
      PDef QName
_ PElims
es      -> Int -> PElims -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k PElims
es
      PLam ArgInfo
_ Abs NLPat
p       -> Int -> Abs NLPat -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k Abs NLPat
p
      PPi Dom' Term NLPType
a Abs NLPType
b        -> Int -> (Dom' Term NLPType, Abs NLPType) -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k (Dom' Term NLPType
a, Abs NLPType
b)
      PSort NLPSort
s        -> Int -> NLPSort -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k NLPSort
s
      PBoundVar Int
_ PElims
es -> Int -> PElims -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k PElims
es
      PTerm{}        -> PatVars
forall a. Null a => a
empty

instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
  nlPatVarsUnder :: Int -> (a, b) -> PatVars
nlPatVarsUnder Int
k (a
a,b
b) = Int -> a -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k a
a PatVars -> PatVars -> PatVars
forall a. Semigroup a => a -> a -> a
<> Int -> b -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k b
b

instance NLPatVars a => NLPatVars (Abs a) where
  nlPatVarsUnder :: Int -> Abs a -> PatVars
nlPatVarsUnder Int
k = \case
    Abs   [Char]
_ a
v -> Int -> a -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
v
    NoAbs [Char]
_ a
v -> Int -> a -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k a
v

instance NLPatVars a => NLPatVars (Arg a) where
instance NLPatVars a => NLPatVars (Dom a) where
instance NLPatVars a => NLPatVars (Elim' a) where
instance NLPatVars PElims where

-- | Get all symbols that a non-linear pattern matches against
class GetMatchables a where
  getMatchables :: a -> [QName]

  default getMatchables :: (Foldable f, GetMatchables a', a ~ f a') => a -> [QName]
  getMatchables = (a' -> [QName]) -> f a' -> [QName]
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a' -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables

instance GetMatchables a => GetMatchables [a] where
instance GetMatchables a => GetMatchables (Arg a) where
instance GetMatchables a => GetMatchables (Dom a) where
instance GetMatchables a => GetMatchables (Elim' a) where
instance GetMatchables a => GetMatchables (Abs a) where

instance (GetMatchables a, GetMatchables b) => GetMatchables (a,b) where
  getMatchables :: (a, b) -> [QName]
getMatchables (a
x,b
y) = a -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables a
x [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++! b -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables b
y

instance GetMatchables NLPat where
  getMatchables :: NLPat -> [QName]
getMatchables NLPat
p =
    case NLPat
p of
      PVar{}         -> [QName]
forall a. Null a => a
empty
      PDef QName
f PElims
es      -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++! PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables PElims
es
      PLam ArgInfo
_ Abs NLPat
x       -> Abs NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Abs NLPat
x
      PPi Dom' Term NLPType
a Abs NLPType
b        -> (Dom' Term NLPType, Abs NLPType) -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (Dom' Term NLPType
a,Abs NLPType
b)
      PSort NLPSort
s        -> NLPSort -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPSort
s
      PBoundVar Int
i PElims
es -> PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables PElims
es
      PTerm Term
u        -> Term -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Term
u

instance GetMatchables NLPType where
  getMatchables :: NLPType -> [QName]
getMatchables = NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (NLPat -> [QName]) -> (NLPType -> NLPat) -> NLPType -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NLPType -> NLPat
nlpTypeUnEl

instance GetMatchables NLPSort where
  getMatchables :: NLPSort -> [QName]
getMatchables = \case
    PUniv Univ
_ NLPat
l -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
    PInf Univ
f Integer
n  -> [QName]
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> [QName]
forall a. Null a => a
empty
    NLPSort
PLockUniv -> [QName]
forall a. Null a => a
empty
    NLPSort
PLevelUniv -> [QName]
forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> [QName]
forall a. Null a => a
empty

instance GetMatchables Term where
  getMatchables :: Term -> [QName]
getMatchables = Term -> [QName]
getDefListNoMetas

instance GetMatchables GlobalRewriteRule where
  getMatchables :: GlobalRewriteRule -> [QName]
getMatchables = PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (PElims -> [QName])
-> (GlobalRewriteRule -> PElims) -> GlobalRewriteRule -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRewriteRule -> PElims
grPats

-- Throws a pattern violation if the given term contains any
-- metavariables.
blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn :: forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn t
t = case t -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAllMetasIn t
t of
  UnblockOnAll Set Blocker
ms | Set Blocker -> Bool
forall a. Null a => a -> Bool
null Set Blocker
ms -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Blocker
b -> Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
b

-- Helper functions
assertPi :: Type -> TCM (Dom Type, Abs Type)
assertPi :: Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
assertPi Type'' Term Term
t = Type'' Term Term -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type'' Term Term
t TCMT IO (Type'' Term Term)
-> (Type'' Term Term
    -> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  El Sort
_ (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b) -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b)
  Type'' Term Term
t             -> Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. Type'' Term Term -> TCM a
errNotPi Type'' Term Term
t

errNotPi :: Type -> TCM a
errNotPi :: forall a. Type'' Term Term -> TCM a
errNotPi Type'' Term Term
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
    , TCMT IO Doc
"should be a function type, but it isn't."
    , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
    ]

assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath :: Type'' Term Term
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type'' Term Term
t = Type'' Term Term -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type'' Term Term
t TCMT IO (Type'' Term Term)
-> (Type'' Term Term -> TCMT IO PathView) -> TCMT IO PathView
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type'' Term Term -> TCMT IO PathView
forall (m :: * -> *).
HasBuiltins m =>
Type'' Term Term -> m PathView
pathView TCMT IO PathView
-> (PathView
    -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term))
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
u Arg Term
v -> (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort
s,QName
q,Arg Term
l,Arg Term
b,Arg Term
u,Arg Term
v)
  OType Type'' Term Term
t -> Type'' Term Term
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. Type'' Term Term -> TCM a
errNotPath Type'' Term Term
t

errNotPath :: Type -> TCM a
errNotPath :: forall a. Type'' Term Term -> TCM a
errNotPath Type'' Term Term
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
    , TCMT IO Doc
"should be a path type, but it isn't."
    , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
    ]

assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf :: QName
-> Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
assertProjOf QName
f Type'' Term Term
t = do
  t <- Type'' Term Term -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type'' Term Term
t
  getDefType f t >>= \case
    Just (El Sort
_ (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b)) -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b)
    Maybe (Type'' Term Term)
_ -> QName
-> Type'' Term Term
-> TCM (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. QName -> Type'' Term Term -> TCM a
errNotProjOf QName
f Type'' Term Term
t

errNotProjOf :: QName -> Type -> TCM a
errNotProjOf :: forall a. QName -> Type'' Term Term -> TCM a
errNotProjOf QName
f Type'' Term Term
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f , TCMT IO Doc
"should be a projection from type"
      , Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t , TCMT IO Doc
"but it isn't."
      , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
      ]

assertConOf :: ConHead -> Type -> TCM Type
assertConOf :: ConHead -> Type'' Term Term -> TCMT IO (Type'' Term Term)
assertConOf ConHead
c Type'' Term Term
t = ConHead
-> Type'' Term Term
-> TCMT
     IO (Maybe ((QName, Type'' Term Term, Args), Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
ConHead
-> Type'' Term Term
-> m (Maybe ((QName, Type'' Term Term, Args), Type'' Term Term))
getFullyAppliedConType ConHead
c Type'' Term Term
t TCMT IO (Maybe ((QName, Type'' Term Term, Args), Type'' Term Term))
-> (Maybe ((QName, Type'' Term Term, Args), Type'' Term Term)
    -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just ((QName, Type'' Term Term, Args)
_ , Type'' Term Term
ct) -> Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
ct
    Maybe ((QName, Type'' Term Term, Args), Type'' Term Term)
Nothing -> ConHead -> Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. ConHead -> Type'' Term Term -> TCM a
errNotConOf ConHead
c Type'' Term Term
t

errNotConOf :: ConHead -> Type -> TCM a
errNotConOf :: forall a. ConHead -> Type'' Term Term -> TCM a
errNotConOf ConHead
c Type'' Term Term
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c , TCMT IO Doc
"should be a constructor of type"
      , Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t , TCMT IO Doc
"but it isn't."
      , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
      ]