{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Rewriting.NonLinPattern where
import Control.Monad.Reader
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.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Irrelevance (workOnTypes, isPropM)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
class PatternFrom t a b where
patternFrom :: Relevance -> Int -> t -> a -> TCM b
instance (PatternFrom t a b) => PatternFrom (Dom t) (Arg a) (Arg b) where
patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b)
patternFrom r :: Relevance
r k :: Int
k t :: Dom t
t u :: 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)
traverse (Relevance -> Int -> t -> a -> TCMT IO b
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r' Int
k (t -> a -> TCMT IO b) -> t -> a -> TCMT IO b
forall a b. (a -> b) -> a -> b
$ Dom t -> t
forall t e. Dom' t e -> e
unDom Dom t
t) Arg a
u
instance PatternFrom (Type, Term) Elims [Elim' NLPat] where
patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
patternFrom r :: Relevance
r k :: Int
k (t :: Type
t,hd :: Term
hd) = \case
[] -> [Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Apply u :: Arg Term
u : es :: Elims
es) -> do
~(Pi a :: Dom Type
a b :: Abs Type
b) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> TCMT IO Type -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
Arg NLPat
p <- Relevance -> Int -> Dom Type -> Arg Term -> TCM (Arg NLPat)
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k Dom Type
a Arg Term
u
Type
t' <- Type
t Type -> Arg Term -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Arg Term
u
let hd' :: Term
hd' = Term
hd Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Arg Term
u ]
[Elim' NLPat]
ps <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Term
hd') Elims
es
[Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Elim' NLPat] -> TCM [Elim' NLPat])
-> [Elim' NLPat] -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply Arg NLPat
p Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
(IApply x :: Term
x y :: Term
y u :: Term
u : es :: Elims
es) -> TypeError -> TCM [Elim' NLPat]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM [Elim' NLPat]) -> TypeError -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
"Rewrite rules with cubical are not yet supported"
(Proj o :: ProjOrigin
o f :: QName
f : es :: Elims
es) -> do
~(Just (El _ (Pi a :: Dom Type
a b :: Abs Type
b))) <- QName -> Type -> TCMT IO (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> TCMT IO (Maybe Type))
-> TCMT IO Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
let t' :: Type
t' = Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
hd
Term
hd' <- ProjOrigin -> QName -> Arg Term -> TCMT IO Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
hd)
[Elim' NLPat]
ps <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Term
hd') Elims
es
[Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Elim' NLPat] -> TCM [Elim' NLPat])
-> [Elim' NLPat] -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
instance (PatternFrom t a b) => PatternFrom t (Dom a) (Dom b) where
patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b)
patternFrom r :: Relevance
r k :: Int
k t :: t
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)
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 -> t -> a -> TCMT IO b
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k t
t
instance PatternFrom () Type NLPType where
patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType
patternFrom r :: Relevance
r k :: Int
k _ a :: 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 -> () -> Sort -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a)
TCMT IO (NLPat -> NLPType) -> TCMT IO NLPat -> TCM NLPType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> 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 -> () -> Sort -> TCMT IO NLPSort
patternFrom r :: Relevance
r k :: Int
k _ s :: Sort
s = do
Sort
s <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
case Sort
s of
Type l :: Level' Term
l -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> TCMT IO NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Level' Term
l
Prop l :: Level' Term
l -> NLPat -> NLPSort
PProp (NLPat -> NLPSort) -> TCMT IO NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Level' Term
l
Inf -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PInf
SizeUniv -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
PiSort _ _ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
FunSort _ _ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
UnivSort _ -> 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 s :: String
s -> do
String -> Int -> [String] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS "impossible" 10
[ "patternFrom: hit dummy sort with content:"
, String
s
]
TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
instance PatternFrom () Level NLPat where
patternFrom :: Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
patternFrom r :: Relevance
r k :: Int
k _ l :: Level' Term
l = do
Type
t <- TCMT IO Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
Term
v <- Level' Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k Type
t Term
v
instance PatternFrom Type Term NLPat where
patternFrom :: Relevance -> Int -> Type -> Term -> TCMT IO NLPat
patternFrom r0 :: Relevance
r0 k :: Int
k t :: Type
t v :: Term
v = do
Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
Maybe (QName, Args)
etaRecord <- Type -> TCMT IO (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t
Bool
prop <- Type -> TCMT IO Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, MonadReduce m, MonadDebug m) =>
a -> m Bool
isPropM Type
t
let r :: Relevance
r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
Term
v <- Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "rewriting.build" 60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "building a pattern from term v = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
, " of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
]
let done :: TCMT IO NLPat
done = NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm Term
v
case (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t , Term -> Term
stripDontCare Term
v) of
(Pi a :: Dom Type
a b :: Abs Type
b , _) -> do
let body :: Term
body = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise 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 0 ]
NLPat
p <- Dom Type -> TCMT IO NLPat -> TCMT IO NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) Term
body)
NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs NLPat -> NLPat
PLam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
forall a b. (a -> b) -> a -> b
$ String -> NLPat -> Abs NLPat
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) NLPat
p
(_ , Var i :: Int
i es :: Elims
es)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> do
Type
t <- Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t , Int -> Term
var Int
i) Elims
es
| Just vs :: Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
TelV tel :: Tele (Dom Type)
tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (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
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Args -> Int
forall a. Sized a => a -> Int
size Args
vs) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let ts :: [Type]
ts = Substitution' Term -> [Type] -> [Type]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
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. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
[Maybe (Arg Int)]
mbvs <- [(Type, Arg Term)]
-> ((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO [Maybe (Arg Int)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Type] -> Args -> [(Type, Arg Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts Args
vs) (((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO [Maybe (Arg Int)])
-> ((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO [Maybe (Arg Int)]
forall a b. (a -> b) -> a -> b
$ \(t :: Type
t , v :: Arg Term
v) -> do
Term -> Type -> TCM (Maybe Int)
isEtaVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) Type
t TCM (Maybe Int)
-> (Maybe Int -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO (Maybe (Arg Int))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just j :: 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 (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 (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Arg Int)
forall a. Maybe a
Nothing
case [Maybe (Arg Int)] -> Maybe [Arg Int]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe (Arg Int)]
mbvs of
Just bvs :: [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 -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Arg Int] -> NLPat
PVar Int
i [Arg Int]
bvs) else TCMT IO NLPat
done
_ -> TCMT IO NLPat
done
| Bool
otherwise -> TCMT IO NLPat
done
(_ , _ ) | Just (d :: QName
d, pars :: Args
pars) <- Maybe (QName, Args)
etaRecord -> do
Defn
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 :: Tele (Dom Type)
tel, c :: ConHead
c, ci :: ConInfo
ci, vs :: Args
vs) <- QName
-> Args
-> Defn
-> Term
-> TCMT IO (Tele (Dom Type), ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args
-> Defn
-> Term
-> m (Tele (Dom Type), ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
TCMT IO (Maybe ((QName, Type, Args), Type))
-> TCMT IO NLPat
-> (((QName, Type, Args), Type) -> TCMT IO NLPat)
-> TCMT IO NLPat
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat)
-> (((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ \ (_ , ct :: Type
ct) -> do
QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) ((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
vs)
(_ , Lam i :: ArgInfo
i t :: Abs Term
t) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , Lit{}) -> TCMT IO NLPat
done
(_ , Def f :: QName
f es :: Elims
es) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
(_ , Def f :: QName
f es :: Elims
es) -> do
Def lsuc :: QName
lsuc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
Def lmax :: QName
lmax [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax
case Elims
es of
[x :: Elim' Term
x] | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lsuc -> TCMT IO NLPat
done
[x :: Elim' Term
x , y :: Elim' Term
y] | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lmax -> TCMT IO NLPat
done
_ -> do
Type
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
QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ft , QName -> Elims -> Term
Def QName
f []) Elims
es
(_ , Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
(_ , Con c :: ConHead
c ci :: ConInfo
ci vs :: Elims
vs) ->
TCMT IO (Maybe ((QName, Type, Args), Type))
-> TCMT IO NLPat
-> (((QName, Type, Args), Type) -> TCMT IO NLPat)
-> TCMT IO NLPat
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat)
-> (((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ \ (_ , ct :: Type
ct) -> do
QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) Elims
vs
(_ , Pi a :: Dom Type
a b :: Abs Type
b) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
(_ , Pi a :: Dom Type
a b :: Abs Type
b) -> do
Dom NLPType
pa <- Relevance -> Int -> () -> Dom Type -> TCM (Dom NLPType)
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Dom Type
a
NLPType
pb <- Dom Type -> TCM NLPType -> TCM NLPType
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> () -> Type -> TCM NLPType
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) () (Type -> TCM NLPType) -> Type -> TCM NLPType
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
pa (String -> NLPType -> Abs NLPType
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) NLPType
pb)
(_ , Sort s :: Sort
s) -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> TCMT IO NLPSort -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Sort -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Sort
s
(_ , Level l :: Level' Term
l) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , DontCare{}) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , MetaV{}) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , Dummy s :: String
s _) -> String -> TCMT IO NLPat
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s
class NLPatToTerm p a where
nlPatToTerm
:: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m)
=> p -> m a
default nlPatToTerm ::
( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
, MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug 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)
traverse p' -> m a'
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug 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 :: Int -> m Term
nlPatToTerm = Term -> m Term
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 :: NLPat -> m Term
nlPatToTerm = \case
PVar i :: Int
i xs :: [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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm [Arg Int]
xs
PTerm u :: Term
u -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
PDef f :: QName
f es :: [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 (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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es
_ -> 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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es
PLam i :: ArgInfo
i u :: 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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm Abs NLPat
u
PPi a :: Dom NLPType
a b :: 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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm Dom NLPType
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm Abs NLPType
b
PSort s :: 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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm NLPSort
s
PBoundVar i :: Int
i es :: [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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es
instance NLPatToTerm NLPat Level where
nlPatToTerm :: NLPat -> m (Level' Term)
nlPatToTerm = NLPat -> m Term
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
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 :: * -> *).
(HasBuiltins m, MonadReduce m, MonadDebug m) =>
Term -> m (Level' Term)
levelView
instance NLPatToTerm NLPType Type where
nlPatToTerm :: NLPType -> m Type
nlPatToTerm (NLPType s :: NLPSort
s a :: 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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm NLPSort
s m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NLPat -> m Term
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
a
instance NLPatToTerm NLPSort Sort where
nlPatToTerm :: NLPSort -> m Sort
nlPatToTerm (PType l :: NLPat
l) = Level' Term -> Sort
forall t. Level' t -> Sort' t
Type (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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
l
nlPatToTerm (PProp l :: NLPat
l) = Level' Term -> Sort
forall t. Level' t -> Sort' t
Prop (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, MonadReduce m, HasBuiltins m, HasConstInfo m,
MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
l
nlPatToTerm PInf = Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
Inf
nlPatToTerm PSizeUniv = Sort -> m Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
SizeUniv
class NLPatVars a where
nlPatVarsUnder :: Int -> a -> IntSet
nlPatVars :: a -> IntSet
nlPatVars = Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder 0
instance {-# OVERLAPPABLE #-} (Foldable f, NLPatVars a) => NLPatVars (f a) where
nlPatVarsUnder :: Int -> f a -> IntSet
nlPatVarsUnder k :: Int
k = (a -> IntSet) -> f a -> IntSet
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 k :: Int
k (NLPType l :: NLPSort
l a :: 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 k :: Int
k = \case
PType l :: NLPat
l -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
PProp l :: NLPat
l -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
PInf -> IntSet
forall a. Null a => a
empty
PSizeUniv -> IntSet
forall a. Null a => a
empty
instance NLPatVars NLPat where
nlPatVarsUnder :: Int -> NLPat -> IntSet
nlPatVarsUnder k :: Int
k = \case
PVar i :: Int
i _ -> 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 _ es :: [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k [Elim' NLPat]
es
PLam _ p :: Abs NLPat
p -> Int -> Abs NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k Abs NLPat
p
PPi a :: Dom NLPType
a b :: 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 s :: NLPSort
s -> Int -> NLPSort -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPSort
s
PBoundVar _ es :: [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 k :: Int
k (a :: a
a,b :: 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 k :: Int
k = \case
Abs _ v :: a
v -> Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) a
v
NoAbs _ v :: 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 (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 (x :: a
x,y :: 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 p :: NLPat
p =
case NLPat
p of
PVar _ _ -> [QName]
forall a. Null a => a
empty
PDef f :: QName
f _ -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f
PLam _ x :: Abs NLPat
x -> Abs NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Abs NLPat
x
PPi a :: Dom NLPType
a b :: Abs NLPType
b -> (Dom NLPType, Abs NLPType) -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (Dom NLPType
a,Abs NLPType
b)
PSort s :: NLPSort
s -> NLPSort -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPSort
s
PBoundVar i :: Int
i es :: [Elim' NLPat]
es -> [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [Elim' NLPat]
es
PTerm u :: 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
PType l :: NLPat
l -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
PProp l :: NLPat
l -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
PInf -> [QName]
forall a. Null a => a
empty
PSizeUniv -> [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' :: NLPat -> FreeM a c
freeVars' = \case
PVar _ _ -> FreeM a c
forall a. Monoid a => a
mempty
PDef _ es :: [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
PLam _ u :: Abs NLPat
u -> Abs NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Abs NLPat
u
PPi a :: Dom NLPType
a b :: Abs NLPType
b -> (Dom NLPType, Abs NLPType) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Dom NLPType
a,Abs NLPType
b)
PSort s :: NLPSort
s -> NLPSort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPSort
s
PBoundVar _ es :: [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
PTerm t :: Term
t -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
t
instance Free NLPType where
freeVars' :: NLPType -> FreeM a c
freeVars' (NLPType s :: NLPSort
s a :: NLPat
a) =
ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> FreeM a c -> FreeM a c -> FreeM a c
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((IgnoreSorts
IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity IgnoreSorts
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity IgnoreSorts
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts)
((NLPSort, NLPat) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (NLPSort
s, NLPat
a))
(NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
a)
instance Free NLPSort where
freeVars' :: NLPSort -> FreeM a c
freeVars' = \case
PType l :: NLPat
l -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
l
PProp l :: NLPat
l -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
l
PInf -> FreeM a c
forall a. Monoid a => a
mempty
PSizeUniv -> FreeM a c
forall a. Monoid a => a
mempty