{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
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
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` 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 (Relevance -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r' Int
k (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 [Elim' NLPat] where
patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat]
patternFrom Relevance
r Int
k (Type
t,Elims -> Term
hd) = \case
[] -> [Elim' NLPat] -> TCM [Elim' NLPat]
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 -> TCM (Dom Type, Abs Type)
assertPi Type
t
p <- patternFrom r k a u
let t' = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
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 r k (t',hd') es
return $ Apply p : ps
(IApply Term
x Term
y Term
i : Elims
es) -> do
(s, q, l, b, u, v) <- Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type
t
let t' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
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 r k interval i
ps <- patternFrom r k (t',hd') es
return $ IApply (PTerm x) (PTerm y) p : ps
(Proj ProjOrigin
o QName
f : Elims
es) -> do
(a,b) <- QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf QName
f Type
t
let u = Elims -> Term
hd []
t' = Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
hd' <- applyDef o f (argFromDom a $> u)
ps <- patternFrom r k (t',applyE hd') es
return $ Proj o f : 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 = (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
$ Relevance -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k TypeOf a
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 = 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
<$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
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
<*> Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a) (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a)
instance PatternFrom Sort NLPSort where
patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
patternFrom Relevance
r Int
k 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
<$> Relevance
-> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
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 -> 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 String
s -> do
String -> Int -> [String] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> [String] -> m ()
reportS String
"impossible" Int
10
[ String
"patternFrom: hit dummy sort with content:"
, String
s
]
TCMT IO NLPSort
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
t <- TCMT IO Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
v <- reallyUnLevelView l
patternFrom r k t 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
t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked TypeOf Term
Type
t
etaRecord <- isEtaRecordType t
prop <- isPropM t
let r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
v <- unLevel =<< abortIfBlocked v
reportSDoc "rewriting.build" 60 $ sep
[ "building a pattern from term v = " <+> prettyTCM v
, " of type " <+> prettyTCM t
]
pview <- pathViewAsPi'whnf
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
a Abs Type
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 -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
p <- Dom Type -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) Term
body)
return $ PLam (domInfo a) $ Abs (absName b) 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 = 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 -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) Term
body)
return $ PLam (domInfo a) $ Abs (absName b) p
(Term
_ , Var Int
i Elims
es)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> do
t <- Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
PBoundVar i <$> patternFrom r k (t , Var i) es
| Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
TelV tel rest <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath (Type -> TCMT IO (TelV Type))
-> TCMT IO Type -> TCMT IO (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
unless (natSize tel >= natSize vs) $ blockOnMetasIn rest >> addContext tel (errNotPi rest)
let ts = Substitution' (SubstArg [Type]) -> [Type] -> [Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([SubstArg [Type]] -> Substitution' (SubstArg [Type])
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg [Type]] -> Substitution' (SubstArg [Type]))
-> [SubstArg [Type]] -> Substitution' (SubstArg [Type])
forall a b. (a -> b) -> a -> b
$ [SubstArg [Type]] -> [SubstArg [Type]]
forall a. [a] -> [a]
reverse ([SubstArg [Type]] -> [SubstArg [Type]])
-> [SubstArg [Type]] -> [SubstArg [Type]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
vs) ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
mbvs <- forM (zip ts vs) $ \(Type
t , Arg Term
v) -> do
(Arg Term, Type) -> TCMT IO ()
forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn (Arg Term
v,Type
t)
Term -> Type -> TCMT IO (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) Type
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
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> 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 :: IntSet
allBoundVars = [Int] -> IntSet
IntSet.fromList (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
k)
ok :: Bool
ok = Bool -> Bool
not (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r) Bool -> Bool -> Bool
||
[Int] -> IntSet
IntSet.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) IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntSet
allBoundVars
if Bool
ok then NLPat -> TCM NLPat
forall a. a -> TCMT IO a
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
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 => QName -> m Definition
getConstInfo QName
d
(tel, c, ci, vs) <- etaExpandRecord_ d pars def v
ct <- assertConOf c t
PDef (conName c) <$> patternFrom r k (ct , Con c ci) (map Apply vs)
(Term
_ , Lam{}) -> Type -> TCM NLPat
forall a. Type -> TCM a
errNotPi Type
t
(Term
_ , Lit{}) -> TCM NLPat
done
(Term
_ , Def QName
f Elims
es) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> 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
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
PDef f <$> patternFrom r k (ft , Def f) es
(Term
_ , Con ConHead
c ConInfo
ci Elims
vs) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM NLPat
done
(Term
_ , Con ConHead
c ConInfo
ci Elims
vs) -> do
ct <- ConHead -> Type -> TCMT IO Type
assertConOf ConHead
c Type
t
PDef (conName c) <$> patternFrom r k (ct , Con c ci) vs
(Term
_ , Pi Dom Type
a Abs Type
b) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM NLPat
done
(Term
_ , Pi Dom Type
a Abs Type
b) -> do
pa <- Relevance
-> Int -> TypeOf (Dom Type) -> Dom Type -> TCM (Dom NLPType)
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () Dom Type
a
pb <- addContext a (patternFrom r (k + 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
<$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
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) -> 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 String
s Elims
_) -> String -> TCM NLPat
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s
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 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 [Elim' NLPat]
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 => 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
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
nlPatToTerm [Elim' NLPat]
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
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
nlPatToTerm [Elim' NLPat]
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 NLPType
a Abs NLPType
b -> Dom Type -> Abs Type -> Term
Pi (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom NLPType -> m (Dom Type)
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => Dom NLPType -> m (Dom Type)
nlPatToTerm Dom NLPType
a m (Abs Type -> Term) -> m (Abs Type) -> 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)
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => Abs NLPType -> m (Abs Type)
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 [Elim' NLPat]
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
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
nlPatToTerm [Elim' NLPat]
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
nlPatToTerm (NLPType NLPSort
s NLPat
a) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
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) -> m Term -> m Type
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
class NLPatVars a where
nlPatVarsUnder :: Int -> a -> IntSet
nlPatVars :: a -> IntSet
nlPatVars = Int -> a -> IntSet
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 = (a -> IntSet) -> f a -> IntSet
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 -> IntSet) -> f a -> IntSet) -> (a -> IntSet) -> f a -> IntSet
forall a b. (a -> b) -> a -> b
$ Int -> a -> IntSet
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) = Int -> (NLPSort, NLPat) -> IntSet
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 -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
PInf Univ
f Integer
n -> IntSet
forall a. Null a => a
empty
NLPSort
PSizeUniv -> IntSet
forall a. Null a => a
empty
NLPSort
PLockUniv -> IntSet
forall a. Null a => a
empty
NLPSort
PLevelUniv -> IntSet
forall a. Null a => a
empty
NLPSort
PIntervalUniv -> IntSet
forall a. Null a => a
empty
instance NLPatVars NLPat where
nlPatVarsUnder :: Int -> NLPat -> IntSet
nlPatVarsUnder Int
k = \case
PVar Int
i [Arg Int]
_ -> Int -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton (Int -> IntSet) -> Int -> IntSet
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
PDef QName
_ [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k [Elim' NLPat]
es
PLam ArgInfo
_ Abs NLPat
p -> Int -> Abs NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k Abs NLPat
p
PPi Dom NLPType
a Abs NLPType
b -> Int -> (Dom NLPType, Abs NLPType) -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k (Dom NLPType
a, Abs NLPType
b)
PSort NLPSort
s -> Int -> NLPSort -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPSort
s
PBoundVar Int
_ [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k [Elim' NLPat]
es
PTerm{} -> IntSet
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) = Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
a IntSet -> IntSet -> IntSet
forall a. Monoid a => a -> a -> a
`mappend` Int -> b -> IntSet
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 -> Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
v
NoAbs String
_ a
v -> Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
v
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 Int
_ [Arg Int]
_ -> [QName]
forall a. Null a => a
empty
PDef QName
f [Elim' NLPat]
es -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [Elim' NLPat]
es
PLam ArgInfo
_ Abs NLPat
x -> Abs NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Abs NLPat
x
PPi Dom NLPType
a Abs NLPType
b -> (Dom NLPType, Abs NLPType) -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (Dom NLPType
a,Abs NLPType
b)
PSort NLPSort
s -> NLPSort -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPSort
s
PBoundVar Int
i [Elim' NLPat]
es -> [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [Elim' NLPat]
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 = (MetaId -> Maybe Term) -> (QName -> [QName]) -> Term -> [QName]
forall a b.
(GetDefs a, Monoid b) =>
(MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' MetaId -> Maybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton
instance GetMatchables RewriteRule where
getMatchables :: RewriteRule -> [QName]
getMatchables = [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables ([Elim' NLPat] -> [QName])
-> (RewriteRule -> [Elim' NLPat]) -> RewriteRule -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> [Elim' NLPat]
rewPats
instance Free NLPat where
freeVars' :: forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' = \case
PVar Int
_ [Arg Int]
_ -> FreeM a c
forall a. Monoid a => a
mempty
PDef QName
_ [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => [Elim' NLPat] -> FreeM a c
freeVars' [Elim' NLPat]
es
PLam ArgInfo
_ Abs NLPat
u -> Abs NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Abs NLPat -> FreeM a c
freeVars' Abs NLPat
u
PPi Dom NLPType
a Abs NLPType
b -> (Dom NLPType, Abs NLPType) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Dom NLPType, Abs NLPType) -> FreeM a c
freeVars' (Dom NLPType
a,Abs NLPType
b)
PSort NLPSort
s -> NLPSort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => NLPSort -> FreeM a c
freeVars' NLPSort
s
PBoundVar Int
_ [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => [Elim' NLPat] -> FreeM a c
freeVars' [Elim' NLPat]
es
PTerm Term
t -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Term -> 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) =
ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((FreeEnv' a IgnoreSorts c -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> FreeEnv' a IgnoreSorts c
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts))
((NLPSort, NLPat) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (NLPSort, NLPat) -> FreeM a c
freeVars' (NLPSort
s, NLPat
a))
(NLPat -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => NLPat -> 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 -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' NLPat
l
PInf Univ
f Integer
n -> FreeM a c
forall a. Monoid a => a
mempty
NLPSort
PSizeUniv -> FreeM a c
forall a. Monoid a => a
mempty
NLPSort
PLockUniv -> FreeM a c
forall a. Monoid a => a
mempty
NLPSort
PLevelUniv -> FreeM a c
forall a. Monoid a => a
mempty
NLPSort
PIntervalUniv -> FreeM a c
forall a. Monoid a => a
mempty
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
assertPi :: Type -> TCM (Dom Type, Abs Type)
assertPi :: Type -> TCM (Dom Type, Abs Type)
assertPi Type
t = Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t TCMT IO Type
-> (Type -> TCM (Dom Type, Abs Type)) -> TCM (Dom Type, Abs Type)
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
a Abs Type
b) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a,Abs Type
b)
Type
t -> Type -> TCM (Dom Type, Abs Type)
forall a. Type -> TCM a
errNotPi Type
t
errNotPi :: Type -> TCM a
errNotPi :: forall a. Type -> TCM a
errNotPi Type
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
GenericDocError (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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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 = Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t TCMT IO Type -> (Type -> 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 -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> 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
t -> Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. Type -> TCM a
errNotPath Type
t
errNotPath :: Type -> TCM a
errNotPath :: forall a. Type -> TCM a
errNotPath Type
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
GenericDocError (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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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
t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
getDefType f t >>= \case
Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a,Abs Type
b)
Maybe Type
_ -> QName -> Type -> TCM (Dom Type, Abs 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 = 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
GenericDocError (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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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 -> TCMT IO Type
assertConOf ConHead
c Type
t = ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t TCMT IO (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> TCMT IO Type)
-> TCMT IO Type
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, Args)
_ , Type
ct) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ct
Maybe ((QName, Type, Args), Type)
Nothing -> ConHead -> Type -> TCMT IO Type
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 = 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
GenericDocError (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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t , TCMT IO Doc
"but it isn't."
, TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
]