{-# 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 Control.Monad        ( (>=>), forM )
import Control.Monad.Reader ( asks )

import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet

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.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Irrelevance (isPropM)
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

-- | Turn a term into a non-linear pattern, treating the
--   free variables as pattern variables.
--   The first argument indicates the relevance we are working under: if this
--   is Irrelevant, then we construct a pattern that never fails to match.
--   The second argument is the number of bound variables (from pattern lambdas).
--   The third argument is the type of the term.

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

instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
  patternFrom :: Relevance -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b)
patternFrom Relevance
r Int
k TypeOf (Arg a)
t Arg a
u = let r' :: Relevance
r' = Relevance
r Relevance -> Relevance -> Relevance
`composeRelevance` forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
u
                        in  forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r' Int
k forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom TypeOf (Arg a)
t) Arg a
u

instance PatternFrom Elims [Elim' NLPat] where
  patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat]
patternFrom Relevance
r Int
k (Type
t,Elims -> Term
hd) = \case
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Apply Arg Term
u : Elims
es) -> do
      (Dom Type
a, Abs Type
b) <- Type -> TCM (Dom Type, Abs Type)
assertPi Type
t
      Arg NLPat
p   <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k Dom Type
a Arg Term
u
      let t' :: Type
t'  = forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (forall e. Arg e -> e
unArg Arg Term
u)
      let hd' :: Elims -> Term
hd' = Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply Arg Term
uforall a. a -> [a] -> [a]
:)
      [Elim' NLPat]
ps  <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Elims -> Term
hd') Elims
es
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Arg a -> Elim' a
Apply Arg NLPat
p forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
    (IApply Term
x Term
y Term
i : Elims
es) -> do
      (Sort
s, QName
q, Arg Term
l, Arg Term
b, Arg Term
u, Arg Term
v) <- Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type
t
      let t' :: Type
t' = forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
b forall t. Apply t => t -> Args -> t
`apply` [ forall a. a -> Arg a
defaultArg Term
i ]
      let hd' :: Elims -> Term
hd' = Elims -> Term
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y Term
iforall a. a -> [a] -> [a]
:)
      Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
      NLPat
p   <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k Type
interval Term
i
      [Elim' NLPat]
ps  <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Elims -> Term
hd') Elims
es
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> a -> Elim' a
IApply (Term -> NLPat
PTerm Term
x) (Term -> NLPat
PTerm Term
y) NLPat
p forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
    (Proj ProjOrigin
o QName
f : Elims
es) -> do
      (Dom Type
a,Abs Type
b) <- QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf QName
f Type
t
      let u :: Term
u = Elims -> Term
hd []
          t' :: Type
t' = Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
u
      Term
hd' <- forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
u)
      [Elim' NLPat]
ps  <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',forall t. Apply t => t -> Elims -> t
applyE Term
hd') Elims
es
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps

instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
  patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b)
patternFrom Relevance
r Int
k TypeOf (Dom a)
t = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k TypeOf (Dom a)
t

instance PatternFrom Type NLPType where
  patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType
patternFrom Relevance
r Int
k TypeOf Type
_ Type
a = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$
    NLPSort -> NLPat -> NLPType
NLPType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () (forall a. LensSort a => a -> Sort
getSort Type
a)
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
a) (forall t a. Type'' t a -> a
unEl Type
a)

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

instance PatternFrom Level NLPat where
  patternFrom :: Relevance
-> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
patternFrom Relevance
r Int
k TypeOf (Level' Term)
_ Level' Term
l = do
    Type
t <- forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
    Term
v <- forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
    forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k Type
t Term
v

instance PatternFrom Term NLPat where
  patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
patternFrom Relevance
r0 Int
k TypeOf Term
t Term
v = do
    Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked TypeOf Term
t
    Maybe (QName, Args)
etaRecord <- forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t
    Bool
prop <- forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
t
    let r :: Relevance
r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
    Term
v <- forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Term
v
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"rewriting.build" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"building a pattern from term v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      , TCMT IO Doc
" of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      ]
    Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview <- forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
    let done :: TCM NLPat
done = forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn Term
v forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> NLPat
PTerm Term
v)
    case (forall t a. Type'' t a -> a
unEl Type
t , Term -> Term
stripDontCare Term
v) of
      (Pi Dom Type
a Abs Type
b , Term
_) -> do
        let body :: Term
body = forall a. Subst a => Int -> a -> a
raise Int
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [ forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        NLPat
p <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (Int
kforall a. Num a => a -> a -> a
+Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Type
b) Term
body)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs NLPat -> NLPat
PLam (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) NLPat
p
      (Term, Term)
_ | Left ((Dom Type
a,Abs Type
b),(Term
x,Term
y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview Type
t -> do
        let body :: Term
body = forall a. Subst a => Int -> a -> a
raise Int
1 Term
v forall t. Apply t => t -> Elims -> t
`applyE` [ forall a. a -> a -> a -> Elim' a
IApply (forall a. Subst a => Int -> a -> a
raise Int
1 forall a b. (a -> b) -> a -> b
$ Term
x) (forall a. Subst a => Int -> a -> a
raise Int
1 forall a b. (a -> b) -> a -> b
$ Term
y) forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        NLPat
p <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (Int
kforall a. Num a => a -> a -> a
+Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Type
b) Term
body)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs NLPat -> NLPat
PLam (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) NLPat
p
      (Term
_ , Var Int
i Elims
es)
       | Int
i forall a. Ord a => a -> a -> Bool
< Int
k     -> do
           Type
t <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
           Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t , Int -> Elims -> Term
Var Int
i) Elims
es
       -- The arguments of `var i` should be distinct bound variables
       -- in order to build a Miller pattern
       | Just Args
vs <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
           TelV Tele (Dom Type)
tel Type
rest <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
           forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Tele (Dom Type)
tel forall a. Ord a => a -> a -> Bool
>= forall a. Sized a => a -> Peano
natSize Args
vs) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn Type
rest forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (forall a. Type -> TCM a
errNotPi Type
rest)
           let ts :: [Type]
ts = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
           [Maybe (Arg Int)]
mbvs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts Args
vs) forall a b. (a -> b) -> a -> b
$ \(Type
t , Arg Term
v) -> do
             forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn (Arg Term
v,Type
t)
             forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar (forall e. Arg e -> e
unArg Arg Term
v) Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               Just Int
j | Int
j forall a. Ord a => a -> a -> Bool
< Int
k -> 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
$ Arg Term
v forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
j
               Maybe Int
_              -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
           case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe (Arg Int)]
mbvs of
             Just [Arg Int]
bvs | forall a. Ord a => [a] -> Bool
fastDistinct [Arg Int]
bvs -> do
               let allBoundVars :: IntSet
allBoundVars = [Int] -> IntSet
IntSet.fromList (forall a. Integral a => a -> [a]
downFrom Int
k)
                   ok :: Bool
ok = Bool -> Bool
not (forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r) Bool -> Bool -> Bool
||
                        [Int] -> IntSet
IntSet.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Int]
bvs) forall a. Eq a => a -> a -> Bool
== IntSet
allBoundVars
               if Bool
ok then forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Arg Int] -> NLPat
PVar Int
i [Arg Int]
bvs) else TCM NLPat
done
             Maybe [Arg Int]
_ -> TCM NLPat
done
       | Bool
otherwise -> TCM NLPat
done
      (Term
_ , Term
_ ) | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
        Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
        (Tele (Dom Type)
tel, ConHead
c, ConInfo
ci, Args
vs) <- forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args
-> Defn
-> Term
-> m (Tele (Dom Type), ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
        Type
ct <- ConHead -> Type -> TCM Type
assertConOf ConHead
c Type
t
        QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
vs)
      (Term
_ , Lam{})   -> forall a. Type -> TCM a
errNotPi Type
t
      (Term
_ , Lit{})   -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) | forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) -> do
        Def QName
lsuc [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
        Def QName
lmax [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax
        case Elims
es of
          [Elim' Term
x]     | QName
f forall a. Eq a => a -> a -> Bool
== QName
lsuc -> TCM NLPat
done
          [Elim' Term
x , Elim' Term
y] | QName
f forall a. Eq a => a -> a -> Bool
== QName
lmax -> TCM NLPat
done
          Elims
_                   -> do
            Type
ft <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
            QName -> [Elim' NLPat] -> NLPat
PDef QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ft , QName -> Elims -> Term
Def QName
f) Elims
es
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) | forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM NLPat
done
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) -> do
        Type
ct <- ConHead -> Type -> TCM Type
assertConOf ConHead
c Type
t
        QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
vs
      (Term
_ , Pi Dom Type
a Abs Type
b) | forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM NLPat
done
      (Term
_ , Pi Dom Type
a Abs Type
b) -> do
        Dom NLPType
pa <- forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () Dom Type
a
        NLPType
pb <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (Int
kforall a. Num a => a -> a -> a
+Int
1) () forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> a
absBody Abs Type
b)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
pa (forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Type
b) NLPType
pb)
      (Term
_ , Sort Sort
s)     -> NLPSort -> NLPat
PSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () Sort
s
      (Term
_ , Level Level' Term
l)    -> forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , DontCare{}) -> forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , MetaV MetaId
m Elims
_)  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Dummy String
s Elims
_)  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall p a (m :: * -> *). (NLPatToTerm p a, 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 Int
i [Arg Int]
xs      -> Int -> Elims -> Term
Var Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm [Arg Int]
xs
    PTerm Term
u        -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    PDef QName
f [Elim' NLPat]
es      -> (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f) 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm [Elim' NLPat]
es
      Defn
_                            -> QName -> Elims -> Term
Def QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm [Elim' NLPat]
es
    PLam ArgInfo
i Abs NLPat
u       -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm Abs NLPat
u
    PPi Dom NLPType
a Abs NLPType
b        -> Dom Type -> Abs Type -> Term
Pi    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm Dom NLPType
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm Abs NLPType
b
    PSort NLPSort
s        -> Sort -> Term
Sort  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm NLPSort
s
    PBoundVar Int
i [Elim' NLPat]
es -> Int -> Elims -> Term
Var Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
nlPatToTerm [Elim' NLPat]
es

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

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

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

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

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

instance {-# OVERLAPPABLE #-} (Foldable f, NLPatVars a) => NLPatVars (f a) where
  nlPatVarsUnder :: Int -> f a -> IntSet
nlPatVarsUnder Int
k = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a b. (a -> b) -> a -> b
$ forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k

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

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

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

instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
  nlPatVarsUnder :: Int -> (a, b) -> IntSet
nlPatVarsUnder Int
k (a
a,b
b) = forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
a forall a. Monoid a => a -> a -> a
`mappend` forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k b
b

instance NLPatVars a => NLPatVars (Abs a) where
  nlPatVarsUnder :: Int -> Abs a -> IntSet
nlPatVarsUnder Int
k = \case
    Abs   String
_ a
v -> forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder (Int
kforall a. Num a => a -> a -> a
+Int
1) a
v
    NoAbs String
_ a
v -> forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
v

-- | 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 = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap 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) = forall a. GetMatchables a => a -> [QName]
getMatchables a
x forall a. [a] -> [a] -> [a]
++ forall a. GetMatchables a => a -> [QName]
getMatchables b
y

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

instance GetMatchables NLPType where
  getMatchables :: NLPType -> [QName]
getMatchables = forall a. GetMatchables a => a -> [QName]
getMatchables 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 -> forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
    PInf Univ
f Integer
n  -> forall a. Null a => a
empty
    NLPSort
PSizeUniv -> forall a. Null a => a
empty
    NLPSort
PLockUniv -> forall a. Null a => a
empty
    NLPSort
PLevelUniv -> forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> forall a. Null a => a
empty

instance GetMatchables Term where
  getMatchables :: Term -> [QName]
getMatchables = forall a b.
(GetDefs a, Monoid b) =>
(MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' forall a. HasCallStack => a
__IMPOSSIBLE__ forall el coll. Singleton el coll => el -> coll
singleton

instance GetMatchables RewriteRule where
  getMatchables :: RewriteRule -> [QName]
getMatchables = forall a. GetMatchables a => a -> [QName]
getMatchables forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> [Elim' NLPat]
rewPats

-- | Only computes free variables that are not bound (see 'nlPatVars'),
--   i.e., those in a 'PTerm'.

instance Free NLPat where
  freeVars' :: forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' = \case
    PVar Int
_ [Arg Int]
_       -> forall a. Monoid a => a
mempty
    PDef QName
_ [Elim' NLPat]
es      -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
    PLam ArgInfo
_ Abs NLPat
u       -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Abs NLPat
u
    PPi Dom NLPType
a Abs NLPType
b        -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Dom NLPType
a,Abs NLPType
b)
    PSort NLPSort
s        -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPSort
s
    PBoundVar Int
_ [Elim' NLPat]
es -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
    PTerm Term
t        -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
t

instance Free NLPType where
  freeVars' :: forall a c. IsVarSet a c => NLPType -> FreeM a c
freeVars' (NLPType NLPSort
s NLPat
a) =
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreNot forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts))
      {- then -} (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (NLPSort
s, NLPat
a))
      {- else -} (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
a)

instance Free NLPSort where
  freeVars' :: forall a c. IsVarSet a c => NLPSort -> FreeM a c
freeVars' = \case
    PUniv Univ
_ NLPat
l -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
l
    PInf Univ
f Integer
n  -> forall a. Monoid a => a
mempty
    NLPSort
PSizeUniv -> forall a. Monoid a => a
mempty
    NLPSort
PLockUniv -> forall a. Monoid a => a
mempty
    NLPSort
PLevelUniv -> forall a. Monoid a => a
mempty
    NLPSort
PIntervalUniv -> forall a. Monoid a => a
mempty

-- 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 forall t. AllMetas t => t -> Blocker
unblockOnAllMetasIn t
t of
  UnblockOnAll Set Blocker
ms | forall a. Null a => a -> Bool
null Set Blocker
ms -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Blocker
b -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
b

-- Helper functions


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

errNotPi :: Type -> TCM a
errNotPi :: forall a. Type -> TCM a
errNotPi Type
t = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
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 -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type
t = forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView 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 -> 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
t -> forall a. Type -> TCM a
errNotPath Type
t

errNotPath :: Type -> TCM a
errNotPath :: forall a. Type -> TCM a
errNotPath Type
t = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
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 -> TCM (Dom Type, Abs Type)
assertProjOf QName
f Type
t = do
  Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
f Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a,Abs Type
b)
    Maybe Type
_ -> forall a. QName -> Type -> TCM a
errNotProjOf QName
f Type
t

errNotProjOf :: QName -> Type -> TCM a
errNotProjOf :: forall a. QName -> Type -> TCM a
errNotProjOf QName
f Type
t = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f , TCMT IO Doc
"should be a projection from type"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
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 -> TCM Type
assertConOf ConHead
c Type
t = forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just ((QName, Type, Args)
_ , Type
ct) -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
ct
    Maybe ((QName, Type, Args), Type)
Nothing -> forall a. ConHead -> Type -> TCM a
errNotConOf ConHead
c Type
t

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