module Agda.TypeChecking.Free.Lazy where
import Control.Applicative hiding (empty)
import Control.Monad ( guard )
import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader )
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.Semigroup ( Semigroup, (<>) )
import qualified Data.Set as Set
import Data.Set (Set)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Semigroup
import Agda.Utils.Singleton
import Agda.Utils.Size
newtype MetaSet = MetaSet { MetaSet -> HashSet MetaId
theMetaSet :: HashSet MetaId }
deriving (MetaSet -> MetaSet -> Bool
(MetaSet -> MetaSet -> Bool)
-> (MetaSet -> MetaSet -> Bool) -> Eq MetaSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaSet -> MetaSet -> Bool
== :: MetaSet -> MetaSet -> Bool
$c/= :: MetaSet -> MetaSet -> Bool
/= :: MetaSet -> MetaSet -> Bool
Eq, Variable -> MetaSet -> ShowS
[MetaSet] -> ShowS
MetaSet -> String
(Variable -> MetaSet -> ShowS)
-> (MetaSet -> String) -> ([MetaSet] -> ShowS) -> Show MetaSet
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Variable -> MetaSet -> ShowS
showsPrec :: Variable -> MetaSet -> ShowS
$cshow :: MetaSet -> String
show :: MetaSet -> String
$cshowList :: [MetaSet] -> ShowS
showList :: [MetaSet] -> ShowS
Show, MetaSet
MetaSet -> Bool
MetaSet -> (MetaSet -> Bool) -> Null MetaSet
forall a. a -> (a -> Bool) -> Null a
$cempty :: MetaSet
empty :: MetaSet
$cnull :: MetaSet -> Bool
null :: MetaSet -> Bool
Null, NonEmpty MetaSet -> MetaSet
MetaSet -> MetaSet -> MetaSet
(MetaSet -> MetaSet -> MetaSet)
-> (NonEmpty MetaSet -> MetaSet)
-> (forall b. Integral b => b -> MetaSet -> MetaSet)
-> Semigroup MetaSet
forall b. Integral b => b -> MetaSet -> MetaSet
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: MetaSet -> MetaSet -> MetaSet
<> :: MetaSet -> MetaSet -> MetaSet
$csconcat :: NonEmpty MetaSet -> MetaSet
sconcat :: NonEmpty MetaSet -> MetaSet
$cstimes :: forall b. Integral b => b -> MetaSet -> MetaSet
stimes :: forall b. Integral b => b -> MetaSet -> MetaSet
Semigroup, Semigroup MetaSet
MetaSet
Semigroup MetaSet =>
MetaSet
-> (MetaSet -> MetaSet -> MetaSet)
-> ([MetaSet] -> MetaSet)
-> Monoid MetaSet
[MetaSet] -> MetaSet
MetaSet -> MetaSet -> MetaSet
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: MetaSet
mempty :: MetaSet
$cmappend :: MetaSet -> MetaSet -> MetaSet
mappend :: MetaSet -> MetaSet -> MetaSet
$cmconcat :: [MetaSet] -> MetaSet
mconcat :: [MetaSet] -> MetaSet
Monoid)
instance Singleton MetaId MetaSet where
singleton :: MetaId -> MetaSet
singleton = HashSet MetaId -> MetaSet
MetaSet (HashSet MetaId -> MetaSet)
-> (MetaId -> HashSet MetaId) -> MetaId -> MetaSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> HashSet MetaId
forall el coll. Singleton el coll => el -> coll
singleton
insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
m (MetaSet HashSet MetaId
ms) = HashSet MetaId -> MetaSet
MetaSet (HashSet MetaId -> MetaSet) -> HashSet MetaId -> MetaSet
forall a b. (a -> b) -> a -> b
$ MetaId -> HashSet MetaId -> HashSet MetaId
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert MetaId
m HashSet MetaId
ms
foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet :: forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet MetaId -> a -> a
f a
e MetaSet
ms = (MetaId -> a -> a) -> a -> HashSet MetaId -> a
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr MetaId -> a -> a
f a
e (HashSet MetaId -> a) -> HashSet MetaId -> a
forall a b. (a -> b) -> a -> b
$ MetaSet -> HashSet MetaId
theMetaSet MetaSet
ms
metaSetToBlocker :: MetaSet -> Blocker
metaSetToBlocker :: MetaSet -> Blocker
metaSetToBlocker MetaSet
ms = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set Blocker -> Set Blocker)
-> Set Blocker -> MetaSet -> Set Blocker
forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet (Blocker -> Set Blocker -> Set Blocker
forall a. Ord a => a -> Set a -> Set a
Set.insert (Blocker -> Set Blocker -> Set Blocker)
-> (MetaId -> Blocker) -> MetaId -> Set Blocker -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Blocker
unblockOnMeta) Set Blocker
forall a. Set a
Set.empty MetaSet
ms
data FlexRig' a
= Flexible a
| WeaklyRigid
| Unguarded
| StronglyRigid
deriving (FlexRig' a -> FlexRig' a -> Bool
(FlexRig' a -> FlexRig' a -> Bool)
-> (FlexRig' a -> FlexRig' a -> Bool) -> Eq (FlexRig' a)
forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
== :: FlexRig' a -> FlexRig' a -> Bool
$c/= :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
/= :: FlexRig' a -> FlexRig' a -> Bool
Eq, Variable -> FlexRig' a -> ShowS
[FlexRig' a] -> ShowS
FlexRig' a -> String
(Variable -> FlexRig' a -> ShowS)
-> (FlexRig' a -> String)
-> ([FlexRig' a] -> ShowS)
-> Show (FlexRig' a)
forall a. Show a => Variable -> FlexRig' a -> ShowS
forall a. Show a => [FlexRig' a] -> ShowS
forall a. Show a => FlexRig' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Variable -> FlexRig' a -> ShowS
showsPrec :: Variable -> FlexRig' a -> ShowS
$cshow :: forall a. Show a => FlexRig' a -> String
show :: FlexRig' a -> String
$cshowList :: forall a. Show a => [FlexRig' a] -> ShowS
showList :: [FlexRig' a] -> ShowS
Show, (forall a b. (a -> b) -> FlexRig' a -> FlexRig' b)
-> (forall a b. a -> FlexRig' b -> FlexRig' a) -> Functor FlexRig'
forall a b. a -> FlexRig' b -> FlexRig' a
forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
fmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
$c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
Functor, (forall m. Monoid m => FlexRig' m -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
-> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
-> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
-> (forall a. (a -> a -> a) -> FlexRig' a -> a)
-> (forall a. (a -> a -> a) -> FlexRig' a -> a)
-> (forall a. FlexRig' a -> [a])
-> (forall a. FlexRig' a -> Bool)
-> (forall a. FlexRig' a -> Variable)
-> (forall a. Eq a => a -> FlexRig' a -> Bool)
-> (forall a. Ord a => FlexRig' a -> a)
-> (forall a. Ord a => FlexRig' a -> a)
-> (forall a. Num a => FlexRig' a -> a)
-> (forall a. Num a => FlexRig' a -> a)
-> Foldable FlexRig'
forall a. Eq a => a -> FlexRig' a -> Bool
forall a. Num a => FlexRig' a -> a
forall a. Ord a => FlexRig' a -> a
forall m. Monoid m => FlexRig' m -> m
forall a. FlexRig' a -> Bool
forall a. FlexRig' a -> Variable
forall a. FlexRig' a -> [a]
forall a. (a -> a -> a) -> FlexRig' a -> a
forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Variable)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => FlexRig' m -> m
fold :: forall m. Monoid m => FlexRig' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$ctoList :: forall a. FlexRig' a -> [a]
toList :: forall a. FlexRig' a -> [a]
$cnull :: forall a. FlexRig' a -> Bool
null :: forall a. FlexRig' a -> Bool
$clength :: forall a. FlexRig' a -> Variable
length :: forall a. FlexRig' a -> Variable
$celem :: forall a. Eq a => a -> FlexRig' a -> Bool
elem :: forall a. Eq a => a -> FlexRig' a -> Bool
$cmaximum :: forall a. Ord a => FlexRig' a -> a
maximum :: forall a. Ord a => FlexRig' a -> a
$cminimum :: forall a. Ord a => FlexRig' a -> a
minimum :: forall a. Ord a => FlexRig' a -> a
$csum :: forall a. Num a => FlexRig' a -> a
sum :: forall a. Num a => FlexRig' a -> a
$cproduct :: forall a. Num a => FlexRig' a -> a
product :: forall a. Num a => FlexRig' a -> a
Foldable)
type FlexRig = FlexRig' MetaSet
class LensFlexRig o a | o -> a where
lensFlexRig :: Lens' o (FlexRig' a)
instance LensFlexRig (FlexRig' a) a where
lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)
lensFlexRig = (FlexRig' a -> f (FlexRig' a)) -> FlexRig' a -> f (FlexRig' a)
forall a. a -> a
id
isFlexible :: LensFlexRig o a => o -> Bool
isFlexible :: forall o a. LensFlexRig o a => o -> Bool
isFlexible o
o = case o
o o -> Lens' o (FlexRig' a) -> FlexRig' a
forall o i. o -> Lens' o i -> i
^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
Flexible {} -> Bool
True
FlexRig' a
_ -> Bool
False
isUnguarded :: LensFlexRig o a => o -> Bool
isUnguarded :: forall o a. LensFlexRig o a => o -> Bool
isUnguarded o
o = case o
o o -> Lens' o (FlexRig' a) -> FlexRig' a
forall o i. o -> Lens' o i -> i
^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
FlexRig' a
Unguarded -> Bool
True
FlexRig' a
_ -> Bool
False
isWeaklyRigid :: LensFlexRig o a => o -> Bool
isWeaklyRigid :: forall o a. LensFlexRig o a => o -> Bool
isWeaklyRigid o
o = case o
o o -> Lens' o (FlexRig' a) -> FlexRig' a
forall o i. o -> Lens' o i -> i
^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
FlexRig' a
WeaklyRigid -> Bool
True
FlexRig' a
_ -> Bool
False
isStronglyRigid :: LensFlexRig o a => o -> Bool
isStronglyRigid :: forall o a. LensFlexRig o a => o -> Bool
isStronglyRigid o
o = case o
o o -> Lens' o (FlexRig' a) -> FlexRig' a
forall o i. o -> Lens' o i -> i
^. (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
FlexRig' a
StronglyRigid -> Bool
True
FlexRig' a
_ -> Bool
False
addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a)
-> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a
-> FlexRig' a
-> FlexRig' a
forall a b. (a -> b) -> a -> b
$ \case
(FlexRig' a
StronglyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
(FlexRig' a
_, FlexRig' a
StronglyRigid) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
(FlexRig' a
Unguarded, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
Unguarded
(FlexRig' a
_, FlexRig' a
Unguarded) -> FlexRig' a
forall a. FlexRig' a
Unguarded
(FlexRig' a
WeaklyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
(FlexRig' a
_, FlexRig' a
WeaklyRigid) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
(Flexible a
ms1, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ a
ms1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ms2
zeroFlexRig :: Monoid a => FlexRig' a
zeroFlexRig :: forall a. Monoid a => FlexRig' a
zeroFlexRig = a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty
omegaFlexRig :: FlexRig' a
omegaFlexRig :: forall a. FlexRig' a
omegaFlexRig = FlexRig' a
forall a. FlexRig' a
StronglyRigid
composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a)
-> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a
-> FlexRig' a
-> FlexRig' a
forall a b. (a -> b) -> a -> b
$ \case
(Flexible a
ms1, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ a
ms1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ms2
(Flexible a
ms1, FlexRig' a
_) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
ms1
(FlexRig' a
_, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
ms2
(FlexRig' a
WeaklyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
(FlexRig' a
_, FlexRig' a
WeaklyRigid) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
(FlexRig' a
StronglyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
(FlexRig' a
_, FlexRig' a
StronglyRigid) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
(FlexRig' a
Unguarded, FlexRig' a
Unguarded) -> FlexRig' a
forall a. FlexRig' a
Unguarded
oneFlexRig :: FlexRig' a
oneFlexRig :: forall a. FlexRig' a
oneFlexRig = FlexRig' a
forall a. FlexRig' a
Unguarded
data VarOcc' a = VarOcc
{ forall a. VarOcc' a -> FlexRig' a
varFlexRig :: FlexRig' a
, forall a. VarOcc' a -> Modality
varModality :: Modality
}
deriving (Variable -> VarOcc' a -> ShowS
[VarOcc' a] -> ShowS
VarOcc' a -> String
(Variable -> VarOcc' a -> ShowS)
-> (VarOcc' a -> String)
-> ([VarOcc' a] -> ShowS)
-> Show (VarOcc' a)
forall a. Show a => Variable -> VarOcc' a -> ShowS
forall a. Show a => [VarOcc' a] -> ShowS
forall a. Show a => VarOcc' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Variable -> VarOcc' a -> ShowS
showsPrec :: Variable -> VarOcc' a -> ShowS
$cshow :: forall a. Show a => VarOcc' a -> String
show :: VarOcc' a -> String
$cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
showList :: [VarOcc' a] -> ShowS
Show)
type VarOcc = VarOcc' MetaSet
instance Eq a => Eq (VarOcc' a) where
VarOcc FlexRig' a
fr Modality
m == :: VarOcc' a -> VarOcc' a -> Bool
== VarOcc FlexRig' a
fr' Modality
m' = FlexRig' a
fr FlexRig' a -> FlexRig' a -> Bool
forall a. Eq a => a -> a -> Bool
== FlexRig' a
fr' Bool -> Bool -> Bool
&& Modality -> Modality -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
m Modality
m'
instance LensModality (VarOcc' a) where
getModality :: VarOcc' a -> Modality
getModality = VarOcc' a -> Modality
forall a. VarOcc' a -> Modality
varModality
mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a
mapModality Modality -> Modality
f (VarOcc FlexRig' a
x Modality
r) = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
x (Modality -> VarOcc' a) -> Modality -> VarOcc' a
forall a b. (a -> b) -> a -> b
$ Modality -> Modality
f Modality
r
instance LensRelevance (VarOcc' a) where
instance LensQuantity (VarOcc' a) where
instance LensFlexRig (VarOcc' a) a where
lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f (VarOcc FlexRig' a
fr Modality
m) = FlexRig' a -> f (FlexRig' a)
f FlexRig' a
fr f (FlexRig' a) -> (FlexRig' a -> VarOcc' a) -> f (VarOcc' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FlexRig' a
fr' -> FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
fr' Modality
m
instance Semigroup a => Semigroup (VarOcc' a) where
VarOcc FlexRig' a
o Modality
m <> :: VarOcc' a -> VarOcc' a -> VarOcc' a
<> VarOcc FlexRig' a
o' Modality
m' = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig FlexRig' a
o FlexRig' a
o') (Modality -> Modality -> Modality
addModality Modality
m Modality
m')
instance (Semigroup a, Monoid a) => Monoid (VarOcc' a) where
mempty :: VarOcc' a
mempty = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty) Modality
zeroModality
mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a
mappend = VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>)
topVarOcc :: VarOcc' a
topVarOcc :: forall a. VarOcc' a
topVarOcc = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
forall a. FlexRig' a
StronglyRigid Modality
topModality
composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc :: forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc (VarOcc FlexRig' a
o Modality
m) (VarOcc FlexRig' a
o' Modality
m') = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig FlexRig' a
o FlexRig' a
o') (Modality -> Modality -> Modality
composeModality Modality
m Modality
m')
oneVarOcc :: VarOcc' a
oneVarOcc :: forall a. VarOcc' a
oneVarOcc = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
forall a. FlexRig' a
Unguarded Modality
unitModality
class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where
withVarOcc :: VarOcc' a -> c -> c
type TheVarMap' a = IntMap (VarOcc' a)
newtype VarMap' a = VarMap { forall a. VarMap' a -> TheVarMap' a
theVarMap :: TheVarMap' a }
deriving (VarMap' a -> VarMap' a -> Bool
(VarMap' a -> VarMap' a -> Bool)
-> (VarMap' a -> VarMap' a -> Bool) -> Eq (VarMap' a)
forall a. Eq a => VarMap' a -> VarMap' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
== :: VarMap' a -> VarMap' a -> Bool
$c/= :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
/= :: VarMap' a -> VarMap' a -> Bool
Eq, Variable -> VarMap' a -> ShowS
[VarMap' a] -> ShowS
VarMap' a -> String
(Variable -> VarMap' a -> ShowS)
-> (VarMap' a -> String)
-> ([VarMap' a] -> ShowS)
-> Show (VarMap' a)
forall a. Show a => Variable -> VarMap' a -> ShowS
forall a. Show a => [VarMap' a] -> ShowS
forall a. Show a => VarMap' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Variable -> VarMap' a -> ShowS
showsPrec :: Variable -> VarMap' a -> ShowS
$cshow :: forall a. Show a => VarMap' a -> String
show :: VarMap' a -> String
$cshowList :: forall a. Show a => [VarMap' a] -> ShowS
showList :: [VarMap' a] -> ShowS
Show)
type TheVarMap = TheVarMap' MetaSet
type VarMap = VarMap' MetaSet
instance Singleton Variable (VarMap' a) where
singleton :: Variable -> VarMap' a
singleton Variable
i = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ Variable -> VarOcc' a -> TheVarMap' a
forall a. Variable -> a -> IntMap a
IntMap.singleton Variable
i VarOcc' a
forall a. VarOcc' a
oneVarOcc
mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap :: forall a b.
(TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap TheVarMap' a -> TheVarMap' b
f = TheVarMap' b -> VarMap' b
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' b -> VarMap' b)
-> (VarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheVarMap' a -> TheVarMap' b
f (TheVarMap' a -> TheVarMap' b)
-> (VarMap' a -> TheVarMap' a) -> VarMap' a -> TheVarMap' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap' a -> TheVarMap' a
forall a. VarMap' a -> TheVarMap' a
theVarMap
lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap :: forall a. Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Variable
i = Variable -> IntMap (VarOcc' a) -> Maybe (VarOcc' a)
forall a. Variable -> IntMap a -> Maybe a
IntMap.lookup Variable
i (IntMap (VarOcc' a) -> Maybe (VarOcc' a))
-> (VarMap' a -> IntMap (VarOcc' a))
-> VarMap' a
-> Maybe (VarOcc' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap' a -> IntMap (VarOcc' a)
forall a. VarMap' a -> TheVarMap' a
theVarMap
instance Semigroup a => Semigroup (VarMap' a) where
VarMap TheVarMap' a
m <> :: VarMap' a -> VarMap' a -> VarMap' a
<> VarMap TheVarMap' a
m' = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ (VarOcc' a -> VarOcc' a -> VarOcc' a)
-> TheVarMap' a -> TheVarMap' a -> TheVarMap' a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>) TheVarMap' a
m TheVarMap' a
m'
instance Semigroup a => Monoid (VarMap' a) where
mempty :: VarMap' a
mempty = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap TheVarMap' a
forall a. IntMap a
IntMap.empty
mappend :: VarMap' a -> VarMap' a -> VarMap' a
mappend = VarMap' a -> VarMap' a -> VarMap' a
forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [VarMap' a] -> VarMap' a
mconcat = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a)
-> ([VarMap' a] -> TheVarMap' a) -> [VarMap' a] -> VarMap' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarOcc' a -> VarOcc' a -> VarOcc' a)
-> [TheVarMap' a] -> TheVarMap' a
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>) ([TheVarMap' a] -> TheVarMap' a)
-> ([VarMap' a] -> [TheVarMap' a]) -> [VarMap' a] -> TheVarMap' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarMap' a -> TheVarMap' a) -> [VarMap' a] -> [TheVarMap' a]
forall a b. (a -> b) -> [a] -> [b]
map VarMap' a -> TheVarMap' a
forall a. VarMap' a -> TheVarMap' a
theVarMap
instance (Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) where
withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a
withVarOcc VarOcc' a
o = (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
forall a b.
(TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap ((TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a)
-> (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a)
-> (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
forall a b. (a -> b) -> a -> b
$ VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc VarOcc' a
o
type TheFlexRigMap = IntMap (FlexRig' ())
newtype FlexRigMap = FlexRigMap { FlexRigMap -> TheFlexRigMap
theFlexRigMap :: TheFlexRigMap }
deriving (Variable -> FlexRigMap -> ShowS
[FlexRigMap] -> ShowS
FlexRigMap -> String
(Variable -> FlexRigMap -> ShowS)
-> (FlexRigMap -> String)
-> ([FlexRigMap] -> ShowS)
-> Show FlexRigMap
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Variable -> FlexRigMap -> ShowS
showsPrec :: Variable -> FlexRigMap -> ShowS
$cshow :: FlexRigMap -> String
show :: FlexRigMap -> String
$cshowList :: [FlexRigMap] -> ShowS
showList :: [FlexRigMap] -> ShowS
Show, Singleton (Variable, FlexRig' ()))
mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap TheFlexRigMap -> TheFlexRigMap
f = TheFlexRigMap -> FlexRigMap
FlexRigMap (TheFlexRigMap -> FlexRigMap)
-> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheFlexRigMap -> TheFlexRigMap
f (TheFlexRigMap -> TheFlexRigMap)
-> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> TheFlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexRigMap -> TheFlexRigMap
theFlexRigMap
instance Semigroup FlexRigMap where
FlexRigMap TheFlexRigMap
m <> :: FlexRigMap -> FlexRigMap -> FlexRigMap
<> FlexRigMap TheFlexRigMap
m' = TheFlexRigMap -> FlexRigMap
FlexRigMap (TheFlexRigMap -> FlexRigMap) -> TheFlexRigMap -> FlexRigMap
forall a b. (a -> b) -> a -> b
$ (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> TheFlexRigMap -> TheFlexRigMap -> TheFlexRigMap
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig TheFlexRigMap
m TheFlexRigMap
m'
instance Monoid FlexRigMap where
mempty :: FlexRigMap
mempty = TheFlexRigMap -> FlexRigMap
FlexRigMap TheFlexRigMap
forall a. IntMap a
IntMap.empty
mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap
mappend = FlexRigMap -> FlexRigMap -> FlexRigMap
forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [FlexRigMap] -> FlexRigMap
mconcat = TheFlexRigMap -> FlexRigMap
FlexRigMap (TheFlexRigMap -> FlexRigMap)
-> ([FlexRigMap] -> TheFlexRigMap) -> [FlexRigMap] -> FlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> [TheFlexRigMap] -> TheFlexRigMap
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig ([TheFlexRigMap] -> TheFlexRigMap)
-> ([FlexRigMap] -> [TheFlexRigMap])
-> [FlexRigMap]
-> TheFlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRigMap -> TheFlexRigMap) -> [FlexRigMap] -> [TheFlexRigMap]
forall a b. (a -> b) -> [a] -> [b]
map FlexRigMap -> TheFlexRigMap
theFlexRigMap
instance IsVarSet () FlexRigMap where
withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap
withVarOcc VarOcc' ()
o = (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap ((TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap)
-> (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
forall a b. (a -> b) -> a -> b
$ (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap)
-> (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a b. (a -> b) -> a -> b
$ () () -> FlexRig' () -> FlexRig' ()
forall a b. a -> FlexRig' b -> FlexRig' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VarOcc' () -> FlexRig' ()
forall a. VarOcc' a -> FlexRig' a
varFlexRig VarOcc' ()
o
instance Singleton MetaId () where
singleton :: MetaId -> ()
singleton MetaId
_ = ()
data IgnoreSorts
= IgnoreNot
| IgnoreInAnnotations
| IgnoreAll
deriving (IgnoreSorts -> IgnoreSorts -> Bool
(IgnoreSorts -> IgnoreSorts -> Bool)
-> (IgnoreSorts -> IgnoreSorts -> Bool) -> Eq IgnoreSorts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IgnoreSorts -> IgnoreSorts -> Bool
== :: IgnoreSorts -> IgnoreSorts -> Bool
$c/= :: IgnoreSorts -> IgnoreSorts -> Bool
/= :: IgnoreSorts -> IgnoreSorts -> Bool
Eq, Variable -> IgnoreSorts -> ShowS
[IgnoreSorts] -> ShowS
IgnoreSorts -> String
(Variable -> IgnoreSorts -> ShowS)
-> (IgnoreSorts -> String)
-> ([IgnoreSorts] -> ShowS)
-> Show IgnoreSorts
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Variable -> IgnoreSorts -> ShowS
showsPrec :: Variable -> IgnoreSorts -> ShowS
$cshow :: IgnoreSorts -> String
show :: IgnoreSorts -> String
$cshowList :: [IgnoreSorts] -> ShowS
showList :: [IgnoreSorts] -> ShowS
Show)
data FreeEnv' a b c = FreeEnv
{ :: !b
, forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig :: !(FlexRig' a)
, forall a b c. FreeEnv' a b c -> Modality
feModality :: !Modality
, forall a b c. FreeEnv' a b c -> Maybe Variable -> c
feSingleton :: Maybe Variable -> c
}
type Variable = Int
type SingleVar c = Variable -> c
type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c
feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts :: forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts = FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a b c. FreeEnv' a b c -> b
feExtra
instance LensFlexRig (FreeEnv' a b c) a where
lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f FreeEnv' a b c
e = FlexRig' a -> f (FlexRig' a)
f (FreeEnv' a b c -> FlexRig' a
forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig FreeEnv' a b c
e) f (FlexRig' a)
-> (FlexRig' a -> FreeEnv' a b c) -> f (FreeEnv' a b c)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FlexRig' a
fr -> FreeEnv' a b c
e { feFlexRig = fr }
instance LensModality (FreeEnv' a b c) where
getModality :: FreeEnv' a b c -> Modality
getModality = FreeEnv' a b c -> Modality
forall a b c. FreeEnv' a b c -> Modality
feModality
mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c
mapModality Modality -> Modality
f FreeEnv' a b c
e = FreeEnv' a b c
e { feModality = f (feModality e) }
instance LensRelevance (FreeEnv' a b c) where
instance LensQuantity (FreeEnv' a b c) where
initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv :: forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv b
e SingleVar c
sing = FreeEnv
{ feExtra :: b
feExtra = b
e
, feFlexRig :: FlexRig' a
feFlexRig = FlexRig' a
forall a. FlexRig' a
Unguarded
, feModality :: Modality
feModality = Modality
unitModality
, feSingleton :: Maybe Variable -> c
feSingleton = c -> SingleVar c -> Maybe Variable -> c
forall b a. b -> (a -> b) -> Maybe a -> b
maybe c
forall a. Monoid a => a
mempty SingleVar c
sing
}
type FreeT a b m c = ReaderT (FreeEnv' a b c) m c
type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c
runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM :: forall a c.
IsVarSet a c =>
SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM SingleVar c
single IgnoreSorts
i FreeM a c
m = FreeM a c -> FreeEnv' a IgnoreSorts c -> c
forall r a. Reader r a -> r -> a
runReader FreeM a c
m (FreeEnv' a IgnoreSorts c -> c) -> FreeEnv' a IgnoreSorts c -> c
forall a b. (a -> b) -> a -> b
$ IgnoreSorts -> SingleVar c -> FreeEnv' a IgnoreSorts c
forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv IgnoreSorts
i SingleVar c
single
instance (Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) where
mempty :: FreeT a b m c
mempty = c -> FreeT a b m c
forall a. a -> ReaderT (FreeEnv' a b c) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
forall a. Monoid a => a
mempty
mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c
mappend = FreeT a b m c -> FreeT a b m c -> FreeT a b m c
forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [FreeT a b m c] -> FreeT a b m c
mconcat = [c] -> c
forall a. Monoid a => [a] -> a
mconcat ([c] -> c)
-> ([FreeT a b m c] -> ReaderT (FreeEnv' a b c) m [c])
-> [FreeT a b m c]
-> FreeT a b m c
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> [FreeT a b m c] -> ReaderT (FreeEnv' a b c) m [c]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
variable :: (Monad m, IsVarSet a c) => Int -> FreeT a b m c
variable :: forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Variable -> FreeT a b m c
variable Variable
n = do
o <- (FreeEnv' a b c -> FlexRig' a)
-> ReaderT (FreeEnv' a b c) m (FlexRig' a)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a b c -> FlexRig' a
forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig
r <- asks feModality
s <- asks feSingleton
return $ withVarOcc (VarOcc o r) (s $ Just n)
subVar :: Int -> Maybe Variable -> Maybe Variable
subVar :: Variable -> Maybe Variable -> Maybe Variable
subVar Variable
n Maybe Variable
x = do
i <- Maybe Variable
x
guard $ i >= n
return $ i - n
underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z
underBinder :: forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder = Variable -> m z -> m z
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' Variable
1
underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z
underBinder' :: forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' Variable
n = (FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z
forall a. (FreeEnv' a b c -> FreeEnv' a b c) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z)
-> (FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z
forall a b. (a -> b) -> a -> b
$ \ FreeEnv' a b c
e -> FreeEnv' a b c
e { feSingleton = feSingleton e . subVar n }
underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z
underModality :: forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Modality -> Modality) -> r -> r
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Modality -> Modality) -> r -> r)
-> (o -> Modality -> Modality) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> Modality -> Modality
composeModality (Modality -> Modality -> Modality)
-> (o -> Modality) -> o -> Modality -> Modality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Modality
forall a. LensModality a => a -> Modality
getModality
underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z
underRelevance :: forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Relevance -> Relevance) -> r -> r
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance ((Relevance -> Relevance) -> r -> r)
-> (o -> Relevance -> Relevance) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance (Relevance -> Relevance -> Relevance)
-> (o -> Relevance) -> o -> Relevance -> Relevance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
underQuantity ::
(MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a
underQuantity :: forall r (m :: * -> *) o a.
(MonadReader r m, LensQuantity r, LensQuantity o) =>
o -> m a -> m a
underQuantity = (r -> r) -> m a -> m a
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m a -> m a) -> (o -> r -> r) -> o -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantity -> Quantity) -> r -> r
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity ((Quantity -> Quantity) -> r -> r)
-> (o -> Quantity -> Quantity) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity (Quantity -> Quantity -> Quantity)
-> (o -> Quantity) -> o -> Quantity -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity
underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z
underFlexRig :: forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' r (FlexRig' a) -> LensMap r (FlexRig' a)
forall o i. Lens' o i -> LensMap o i
over (FlexRig' a -> f (FlexRig' a)) -> r -> f r
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' r (FlexRig' a)
lensFlexRig LensMap r (FlexRig' a)
-> (o -> FlexRig' a -> FlexRig' a) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (FlexRig' a -> FlexRig' a -> FlexRig' a)
-> (o -> FlexRig' a) -> o -> FlexRig' a -> FlexRig' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' o (FlexRig' a) -> o -> FlexRig' a
forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig
underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z
underConstructor :: forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig r a, Semigroup a) =>
ConHead -> Elims -> m z -> m z
underConstructor (ConHead QName
_c DataOrRecord
_d Induction
i [Arg QName]
fs) Elims
es =
case Induction
i of
Induction
CoInductive -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid
Induction
Inductive | Elims -> Peano
forall a. Sized a => a -> Peano
natSize Elims
es Peano -> Peano -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg QName] -> Peano
forall a. Sized a => a -> Peano
natSize [Arg QName]
fs -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
StronglyRigid
| Bool
otherwise -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid
class Free t where
freeVars' :: IsVarSet a c => t -> FreeM a c
default freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t -> FreeM a c
freeVars' = (b -> FreeM a c) -> f b -> FreeM a c
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => b -> FreeM a c
freeVars'
instance Free Term where
freeVars' :: forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
t = case Term -> Term
unSpine Term
t of
Var Variable
n Elims
ts -> Variable -> FreeM a c
forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Variable -> FreeT a b m c
variable Variable
n FreeM a c -> FreeM a c -> FreeM a c
forall a. Monoid a => a -> a -> a
`mappend` do FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
ts
Lam ArgInfo
_ Abs Term
t -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Abs Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Abs Term -> FreeM a c
freeVars' Abs Term
t
Lit Literal
_ -> FreeM a c
forall a. Monoid a => a
mempty
Def QName
_ Elims
ts -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
ts
Con ConHead
c ConInfo
_ Elims
ts -> ConHead -> Elims -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig r a, Semigroup a) =>
ConHead -> Elims -> m z -> m z
underConstructor ConHead
c Elims
ts (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
ts
Pi Dom Type
a Abs Type
b -> (Dom Type, Abs Type) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Dom Type, Abs Type) -> FreeM a c
freeVars' (Dom Type
a,Abs Type
b)
Sort Sort
s -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
Level Level
l -> Level -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Level -> FreeM a c
freeVars' Level
l
MetaV MetaId
m Elims
ts -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ MetaId -> a
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
ts
DontCare Term
mt -> Modality -> FreeM a c -> FreeM a c
forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality (Relevance -> Quantity -> Cohesion -> Modality
Modality Relevance
Irrelevant Quantity
unitQuantity Cohesion
unitCohesion) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ 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
mt
Dummy{} -> FreeM a c
forall a. Monoid a => a
mempty
instance Free t => Free (Type' t) where
freeVars' :: forall a c. IsVarSet a c => Type' t -> FreeM a c
freeVars' (El Sort
s t
t) =
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))
((Sort, t) -> 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 => (Sort, t) -> FreeM a c
freeVars' (Sort
s, t
t))
(t -> 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 => t -> FreeM a c
freeVars' t
t)
instance Free Sort where
freeVars' :: forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s =
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
IgnoreAll 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)) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$
case Sort
s of
Univ Univ
_ Level
a -> Level -> 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 => Level -> FreeM a c
freeVars' Level
a
Inf Univ
_ Integer
_ -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
Sort
SizeUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
Sort
LockUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
Sort
LevelUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
Sort
IntervalUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty) (Term -> 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 => Term -> FreeM a c
freeVars' (Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
a) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a -> a -> a
`mappend`
FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid ((Sort, Abs Sort) -> 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 => (Sort, Abs Sort) -> FreeM a c
freeVars' (Sort
s1, Abs Sort
s2))
FunSort Sort
s1 Sort
s2 -> Sort -> 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 => Sort -> FreeM a c
freeVars' Sort
s1 ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a -> a -> a
`mappend` Sort -> 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 => Sort -> FreeM a c
freeVars' Sort
s2
UnivSort Sort
s -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Sort -> 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 => Sort -> FreeM a c
freeVars' Sort
s
MetaS MetaId
x Elims
es -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ MetaId -> a
forall el coll. Singleton el coll => el -> coll
singleton MetaId
x) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Elims -> 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 => Elims -> FreeM a c
freeVars' Elims
es
DefS QName
_ Elims
es -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Elims -> 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 => Elims -> FreeM a c
freeVars' Elims
es
DummyS{} -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
instance Free Level where
freeVars' :: forall a c. IsVarSet a c => Level -> FreeM a c
freeVars' (Max Integer
_ [PlusLevel' Term]
as) = [PlusLevel' Term] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => [PlusLevel' Term] -> FreeM a c
freeVars' [PlusLevel' Term]
as
instance Free t => Free (PlusLevel' t) where
freeVars' :: forall a c. IsVarSet a c => PlusLevel' t -> FreeM a c
freeVars' (Plus Integer
_ t
l) = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' t
l
instance Free t => Free [t] where
instance Free t => Free (Maybe t) where
instance Free t => Free (WithHiding t) where
instance Free t => Free (Named nm t)
instance (Free t, Free u) => Free (t, u) where
freeVars' :: forall a c. IsVarSet a c => (t, u) -> FreeM a c
freeVars' (t
t, u
u) = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' t
t FreeM a c -> FreeM a c -> FreeM a c
forall a. Monoid a => a -> a -> a
`mappend` u -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => u -> FreeM a c
freeVars' u
u
instance (Free t, Free u, Free v) => Free (t, u, v) where
freeVars' :: forall a c. IsVarSet a c => (t, u, v) -> FreeM a c
freeVars' (t
t, u
u, v
v) = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' t
t FreeM a c -> FreeM a c -> FreeM a c
forall a. Monoid a => a -> a -> a
`mappend` u -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => u -> FreeM a c
freeVars' u
u FreeM a c -> FreeM a c -> FreeM a c
forall a. Monoid a => a -> a -> a
`mappend` v -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => v -> FreeM a c
freeVars' v
v
instance Free t => Free (Elim' t) where
freeVars' :: forall a c. IsVarSet a c => Elim' t -> FreeM a c
freeVars' (Apply Arg t
t) = Arg t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Arg t -> FreeM a c
freeVars' Arg t
t
freeVars' (Proj{} ) = FreeM a c
forall a. Monoid a => a
mempty
freeVars' (IApply t
x t
y t
r) = (t, t, t) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (t, t, t) -> FreeM a c
freeVars' (t
x,t
y,t
r)
instance Free t => Free (Arg t) where
freeVars' :: forall a c. IsVarSet a c => Arg t -> FreeM a c
freeVars' Arg t
t = Modality
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality (Arg t -> Modality
forall a. LensModality a => a -> Modality
getModality Arg t
t) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ t -> 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 => t -> FreeM a c
freeVars' (t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Arg t -> t
forall e. Arg e -> e
unArg Arg t
t
instance Free t => Free (Dom t) where
freeVars' :: forall a c. IsVarSet a c => Dom t -> FreeM a c
freeVars' Dom t
d = (Maybe Term, t) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Maybe Term, t) -> FreeM a c
freeVars' (Dom t -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom t
d, Dom t -> t
forall t e. Dom' t e -> e
unDom Dom t
d)
instance Free t => Free (Abs t) where
freeVars' :: forall a c. IsVarSet a c => Abs t -> FreeM a c
freeVars' (Abs String
_ t
b) = ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ t -> 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 => t -> FreeM a c
freeVars' t
b
freeVars' (NoAbs String
_ t
b) = t -> 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 => t -> FreeM a c
freeVars' t
b
instance Free t => Free (Tele t) where
freeVars' :: forall a c. IsVarSet a c => Tele t -> FreeM a c
freeVars' Tele t
EmptyTel = FreeM a c
forall a. Monoid a => a
mempty
freeVars' (ExtendTel t
t Abs (Tele t)
tel) = (t, Abs (Tele t)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (t, Abs (Tele t)) -> FreeM a c
freeVars' (t
t, Abs (Tele t)
tel)
instance Free Clause where
freeVars' :: forall a c. IsVarSet a c => Clause -> FreeM a c
freeVars' Clause
cl = Variable
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' (Telescope -> Variable
forall a. Sized a => a -> Variable
size (Telescope -> Variable) -> Telescope -> Variable
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Maybe Term -> 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 => Maybe Term -> FreeM a c
freeVars' (Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl
instance Free EqualityView where
freeVars' :: forall a c. IsVarSet a c => EqualityView -> FreeM a c
freeVars' = \case
OtherType Type
t -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
IdiomType Type
t -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
EqualityType Sort
s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> (Sort, Args, Args) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, Args, Args) -> FreeM a c
freeVars' (Sort
s, Args
l, [Arg Term
t, Arg Term
a, Arg Term
b])