{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Free
( VarCounts(..)
, Free
, IsVarSet(..)
, IgnoreSorts(..)
, freeVars, freeVars', filterVarMap, filterVarMapToList
, runFree, rigidVars, stronglyRigidVars, unguardedVars, allVars
, allFreeVars
, allRelevantVars, allRelevantVarsIgnoring
, freeIn, freeInIgnoringSorts, isBinderUsed
, relevantIn, relevantInIgnoringSortAnn
, FlexRig'(..), FlexRig
, LensFlexRig(..), isFlexible, isUnguarded, isStronglyRigid, isWeaklyRigid
, VarOcc'(..), VarOcc
, varOccurrenceIn
, flexRigOccurrenceIn
, closed
, MetaSet
, insertMetaSet, foldrMetaSet
) where
import Prelude hiding (null)
import Data.Monoid ( Monoid, mempty, mappend)
import Data.Semigroup ( Semigroup, (<>), Any(..), All(..) )
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common hiding (Arg, NamedArg)
import Agda.Syntax.Internal
import Agda.TypeChecking.Free.Lazy
import Agda.Utils.Singleton
type VarSet = IntSet
instance IsVarSet () VarSet where withVarOcc :: VarOcc' () -> VarSet -> VarSet
withVarOcc _ = VarSet -> VarSet
forall a. a -> a
id
instance IsVarSet () [Int] where withVarOcc :: VarOcc' () -> [Int] -> [Int]
withVarOcc _ = [Int] -> [Int]
forall a. a -> a
id
instance IsVarSet () Any where withVarOcc :: VarOcc' () -> Any -> Any
withVarOcc _ = Any -> Any
forall a. a -> a
id
instance IsVarSet () All where withVarOcc :: VarOcc' () -> All -> All
withVarOcc _ = All -> All
forall a. a -> a
id
newtype VarCounts = VarCounts { VarCounts -> IntMap Int
varCounts :: IntMap Int }
instance Semigroup VarCounts where
VarCounts fv1 :: IntMap Int
fv1 <> :: VarCounts -> VarCounts -> VarCounts
<> VarCounts fv2 :: IntMap Int
fv2 = IntMap Int -> VarCounts
VarCounts ((Int -> Int -> Int) -> IntMap Int -> IntMap Int -> IntMap Int
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) IntMap Int
fv1 IntMap Int
fv2)
instance Monoid VarCounts where
mempty :: VarCounts
mempty = IntMap Int -> VarCounts
VarCounts IntMap Int
forall a. IntMap a
IntMap.empty
mappend :: VarCounts -> VarCounts -> VarCounts
mappend = VarCounts -> VarCounts -> VarCounts
forall a. Semigroup a => a -> a -> a
(<>)
instance IsVarSet () VarCounts where
withVarOcc :: VarOcc' () -> VarCounts -> VarCounts
withVarOcc _ = VarCounts -> VarCounts
forall a. a -> a
id
instance Singleton Variable VarCounts where
singleton :: Int -> VarCounts
singleton i :: Int
i = IntMap Int -> VarCounts
VarCounts (IntMap Int -> VarCounts) -> IntMap Int -> VarCounts
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IntMap Int
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i 1
{-# SPECIALIZE freeVars :: Free a => a -> VarMap #-}
freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c
freeVars :: t -> c
freeVars = IgnoreSorts -> t -> c
forall a c t.
(IsVarSet a c, Singleton Int c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore IgnoreSorts
IgnoreNot
freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore :: IgnoreSorts -> t -> c
freeVarsIgnore = SingleVar c -> IgnoreSorts -> t -> c
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar c
forall el coll. Singleton el coll => el -> coll
singleton
{-# SPECIALIZE runFree :: Free a => SingleVar Any -> IgnoreSorts -> a -> Any #-}
{-# SPECIALIZE runFree :: SingleVar Any -> IgnoreSorts -> Term -> Any #-}
runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c
runFree :: SingleVar c -> IgnoreSorts -> t -> c
runFree single :: SingleVar c
single i :: IgnoreSorts
i t :: t
t =
SingleVar c -> IgnoreSorts -> FreeM a c -> c
forall a c.
IsVarSet a c =>
SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM SingleVar c
single IgnoreSorts
i (t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
t)
where
bench :: a -> a
bench = Account -> a -> a
forall a. Account -> a -> a
Bench.billToPure [ Phase
Bench.Typing , Phase
Bench.Free ]
varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc
varOccurrenceIn :: Int -> a -> Maybe VarOcc
varOccurrenceIn = IgnoreSorts -> Int -> a -> Maybe VarOcc
forall a. Free a => IgnoreSorts -> Int -> a -> Maybe VarOcc
varOccurrenceIn' IgnoreSorts
IgnoreNot
varOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe VarOcc
varOccurrenceIn' :: IgnoreSorts -> Int -> a -> Maybe VarOcc
varOccurrenceIn' ig :: IgnoreSorts
ig x :: Int
x t :: a
t = SingleVarOcc -> Maybe VarOcc
theSingleVarOcc (SingleVarOcc -> Maybe VarOcc) -> SingleVarOcc -> Maybe VarOcc
forall a b. (a -> b) -> a -> b
$ SingleVar SingleVarOcc -> IgnoreSorts -> a -> SingleVarOcc
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar SingleVarOcc
sg IgnoreSorts
ig a
t
where
sg :: SingleVar SingleVarOcc
sg y :: Int
y = if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y then SingleVarOcc
oneSingleVarOcc else SingleVarOcc
forall a. Monoid a => a
mempty
newtype SingleVarOcc = SingleVarOcc { SingleVarOcc -> Maybe VarOcc
theSingleVarOcc :: Maybe VarOcc }
oneSingleVarOcc :: SingleVarOcc
oneSingleVarOcc :: SingleVarOcc
oneSingleVarOcc = Maybe VarOcc -> SingleVarOcc
SingleVarOcc (Maybe VarOcc -> SingleVarOcc) -> Maybe VarOcc -> SingleVarOcc
forall a b. (a -> b) -> a -> b
$ VarOcc -> Maybe VarOcc
forall a. a -> Maybe a
Just (VarOcc -> Maybe VarOcc) -> VarOcc -> Maybe VarOcc
forall a b. (a -> b) -> a -> b
$ VarOcc
forall a. VarOcc' a
oneVarOcc
instance Semigroup SingleVarOcc where
SingleVarOcc Nothing <> :: SingleVarOcc -> SingleVarOcc -> SingleVarOcc
<> s :: SingleVarOcc
s = SingleVarOcc
s
s :: SingleVarOcc
s <> SingleVarOcc Nothing = SingleVarOcc
s
SingleVarOcc (Just o :: VarOcc
o) <> SingleVarOcc (Just o' :: VarOcc
o') = Maybe VarOcc -> SingleVarOcc
SingleVarOcc (Maybe VarOcc -> SingleVarOcc) -> Maybe VarOcc -> SingleVarOcc
forall a b. (a -> b) -> a -> b
$ VarOcc -> Maybe VarOcc
forall a. a -> Maybe a
Just (VarOcc -> Maybe VarOcc) -> VarOcc -> Maybe VarOcc
forall a b. (a -> b) -> a -> b
$ VarOcc
o VarOcc -> VarOcc -> VarOcc
forall a. Semigroup a => a -> a -> a
<> VarOcc
o'
instance Monoid SingleVarOcc where
mempty :: SingleVarOcc
mempty = Maybe VarOcc -> SingleVarOcc
SingleVarOcc Maybe VarOcc
forall a. Maybe a
Nothing
mappend :: SingleVarOcc -> SingleVarOcc -> SingleVarOcc
mappend = SingleVarOcc -> SingleVarOcc -> SingleVarOcc
forall a. Semigroup a => a -> a -> a
(<>)
instance IsVarSet MetaSet SingleVarOcc where
withVarOcc :: VarOcc -> SingleVarOcc -> SingleVarOcc
withVarOcc o :: VarOcc
o = Maybe VarOcc -> SingleVarOcc
SingleVarOcc (Maybe VarOcc -> SingleVarOcc)
-> (SingleVarOcc -> Maybe VarOcc) -> SingleVarOcc -> SingleVarOcc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarOcc -> VarOcc) -> Maybe VarOcc -> Maybe VarOcc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VarOcc -> VarOcc -> VarOcc
forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc VarOcc
o) (Maybe VarOcc -> Maybe VarOcc)
-> (SingleVarOcc -> Maybe VarOcc) -> SingleVarOcc -> Maybe VarOcc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleVarOcc -> Maybe VarOcc
theSingleVarOcc
flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn :: Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn = IgnoreSorts -> Int -> a -> Maybe (FlexRig' ())
forall a. Free a => IgnoreSorts -> Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn' IgnoreSorts
IgnoreNot
flexRigOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn' :: IgnoreSorts -> Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn' ig :: IgnoreSorts
ig x :: Int
x t :: a
t = SingleFlexRig -> Maybe (FlexRig' ())
theSingleFlexRig (SingleFlexRig -> Maybe (FlexRig' ()))
-> SingleFlexRig -> Maybe (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ SingleVar SingleFlexRig -> IgnoreSorts -> a -> SingleFlexRig
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar SingleFlexRig
sg IgnoreSorts
ig a
t
where
sg :: SingleVar SingleFlexRig
sg y :: Int
y = if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y then SingleFlexRig
oneSingleFlexRig else SingleFlexRig
forall a. Monoid a => a
mempty
newtype SingleFlexRig = SingleFlexRig { SingleFlexRig -> Maybe (FlexRig' ())
theSingleFlexRig :: Maybe (FlexRig' ()) }
oneSingleFlexRig :: SingleFlexRig
oneSingleFlexRig :: SingleFlexRig
oneSingleFlexRig = Maybe (FlexRig' ()) -> SingleFlexRig
SingleFlexRig (Maybe (FlexRig' ()) -> SingleFlexRig)
-> Maybe (FlexRig' ()) -> SingleFlexRig
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> Maybe (FlexRig' ())
forall a. a -> Maybe a
Just (FlexRig' () -> Maybe (FlexRig' ()))
-> FlexRig' () -> Maybe (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ FlexRig' ()
forall a. FlexRig' a
oneFlexRig
instance Semigroup SingleFlexRig where
SingleFlexRig Nothing <> :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
<> s :: SingleFlexRig
s = SingleFlexRig
s
s :: SingleFlexRig
s <> SingleFlexRig Nothing = SingleFlexRig
s
SingleFlexRig (Just o :: FlexRig' ()
o) <> SingleFlexRig (Just o' :: FlexRig' ()
o') = Maybe (FlexRig' ()) -> SingleFlexRig
SingleFlexRig (Maybe (FlexRig' ()) -> SingleFlexRig)
-> Maybe (FlexRig' ()) -> SingleFlexRig
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> Maybe (FlexRig' ())
forall a. a -> Maybe a
Just (FlexRig' () -> Maybe (FlexRig' ()))
-> FlexRig' () -> Maybe (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig FlexRig' ()
o FlexRig' ()
o'
instance Monoid SingleFlexRig where
mempty :: SingleFlexRig
mempty = Maybe (FlexRig' ()) -> SingleFlexRig
SingleFlexRig Maybe (FlexRig' ())
forall a. Maybe a
Nothing
mappend :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
mappend = SingleFlexRig -> SingleFlexRig -> SingleFlexRig
forall a. Semigroup a => a -> a -> a
(<>)
instance IsVarSet () SingleFlexRig where
withVarOcc :: VarOcc' () -> SingleFlexRig -> SingleFlexRig
withVarOcc o :: VarOcc' ()
o = Maybe (FlexRig' ()) -> SingleFlexRig
SingleFlexRig (Maybe (FlexRig' ()) -> SingleFlexRig)
-> (SingleFlexRig -> Maybe (FlexRig' ()))
-> SingleFlexRig
-> SingleFlexRig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRig' () -> FlexRig' ())
-> Maybe (FlexRig' ()) -> Maybe (FlexRig' ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VarOcc' () -> FlexRig' ()
forall a. VarOcc' a -> FlexRig' a
varFlexRig VarOcc' ()
o) (Maybe (FlexRig' ()) -> Maybe (FlexRig' ()))
-> (SingleFlexRig -> Maybe (FlexRig' ()))
-> SingleFlexRig
-> Maybe (FlexRig' ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleFlexRig -> Maybe (FlexRig' ())
theSingleFlexRig
freeIn' :: Free a => IgnoreSorts -> Nat -> a -> Bool
freeIn' :: IgnoreSorts -> Int -> a -> Bool
freeIn' ig :: IgnoreSorts
ig x :: Int
x t :: a
t = Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar Any -> IgnoreSorts -> a -> Any
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> Any
Any (Bool -> Any) -> (Int -> Bool) -> SingleVar Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==)) IgnoreSorts
ig a
t
{-# SPECIALIZE freeIn :: Nat -> Term -> Bool #-}
freeIn :: Free a => Nat -> a -> Bool
freeIn :: Int -> a -> Bool
freeIn = IgnoreSorts -> Int -> a -> Bool
forall a. Free a => IgnoreSorts -> Int -> a -> Bool
freeIn' IgnoreSorts
IgnoreNot
freeInIgnoringSorts :: Free a => Nat -> a -> Bool
freeInIgnoringSorts :: Int -> a -> Bool
freeInIgnoringSorts = IgnoreSorts -> Int -> a -> Bool
forall a. Free a => IgnoreSorts -> Int -> a -> Bool
freeIn' IgnoreSorts
IgnoreAll
isBinderUsed :: Free a => Abs a -> Bool
isBinderUsed :: Abs a -> Bool
isBinderUsed NoAbs{} = Bool
False
isBinderUsed (Abs _ x :: a
x) = 0 Int -> a -> Bool
forall a. Free a => Int -> a -> Bool
`freeIn` a
x
newtype RelevantIn c = RelevantIn {RelevantIn c -> c
getRelevantIn :: c}
deriving (b -> RelevantIn c -> RelevantIn c
NonEmpty (RelevantIn c) -> RelevantIn c
RelevantIn c -> RelevantIn c -> RelevantIn c
(RelevantIn c -> RelevantIn c -> RelevantIn c)
-> (NonEmpty (RelevantIn c) -> RelevantIn c)
-> (forall b. Integral b => b -> RelevantIn c -> RelevantIn c)
-> Semigroup (RelevantIn c)
forall b. Integral b => b -> RelevantIn c -> RelevantIn c
forall c. Semigroup c => NonEmpty (RelevantIn c) -> RelevantIn c
forall c.
Semigroup c =>
RelevantIn c -> RelevantIn c -> RelevantIn c
forall c b.
(Semigroup c, Integral b) =>
b -> RelevantIn c -> RelevantIn c
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> RelevantIn c -> RelevantIn c
$cstimes :: forall c b.
(Semigroup c, Integral b) =>
b -> RelevantIn c -> RelevantIn c
sconcat :: NonEmpty (RelevantIn c) -> RelevantIn c
$csconcat :: forall c. Semigroup c => NonEmpty (RelevantIn c) -> RelevantIn c
<> :: RelevantIn c -> RelevantIn c -> RelevantIn c
$c<> :: forall c.
Semigroup c =>
RelevantIn c -> RelevantIn c -> RelevantIn c
Semigroup, Semigroup (RelevantIn c)
RelevantIn c
Semigroup (RelevantIn c) =>
RelevantIn c
-> (RelevantIn c -> RelevantIn c -> RelevantIn c)
-> ([RelevantIn c] -> RelevantIn c)
-> Monoid (RelevantIn c)
[RelevantIn c] -> RelevantIn c
RelevantIn c -> RelevantIn c -> RelevantIn c
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall c. Monoid c => Semigroup (RelevantIn c)
forall c. Monoid c => RelevantIn c
forall c. Monoid c => [RelevantIn c] -> RelevantIn c
forall c. Monoid c => RelevantIn c -> RelevantIn c -> RelevantIn c
mconcat :: [RelevantIn c] -> RelevantIn c
$cmconcat :: forall c. Monoid c => [RelevantIn c] -> RelevantIn c
mappend :: RelevantIn c -> RelevantIn c -> RelevantIn c
$cmappend :: forall c. Monoid c => RelevantIn c -> RelevantIn c -> RelevantIn c
mempty :: RelevantIn c
$cmempty :: forall c. Monoid c => RelevantIn c
$cp1Monoid :: forall c. Monoid c => Semigroup (RelevantIn c)
Monoid)
instance IsVarSet a c => IsVarSet a (RelevantIn c) where
withVarOcc :: VarOcc' a -> RelevantIn c -> RelevantIn c
withVarOcc o :: VarOcc' a
o x :: RelevantIn c
x
| VarOcc' a -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant VarOcc' a
o = RelevantIn c
forall a. Monoid a => a
mempty
| Bool
otherwise = c -> RelevantIn c
forall c. c -> RelevantIn c
RelevantIn (c -> RelevantIn c) -> c -> RelevantIn c
forall a b. (a -> b) -> a -> b
$ VarOcc' a -> c -> c
forall a c. IsVarSet a c => VarOcc' a -> c -> c
withVarOcc VarOcc' a
o (c -> c) -> c -> c
forall a b. (a -> b) -> a -> b
$ RelevantIn c -> c
forall c. RelevantIn c -> c
getRelevantIn RelevantIn c
x
relevantIn' :: Free t => IgnoreSorts -> Nat -> t -> Bool
relevantIn' :: IgnoreSorts -> Int -> t -> Bool
relevantIn' ig :: IgnoreSorts
ig x :: Int
x t :: t
t = Any -> Bool
getAny (Any -> Bool) -> (RelevantIn Any -> Any) -> RelevantIn Any -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelevantIn Any -> Any
forall c. RelevantIn c -> c
getRelevantIn (RelevantIn Any -> Bool) -> RelevantIn Any -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar (RelevantIn Any) -> IgnoreSorts -> t -> RelevantIn Any
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Any -> RelevantIn Any
forall c. c -> RelevantIn c
RelevantIn (Any -> RelevantIn Any)
-> SingleVar Any -> SingleVar (RelevantIn Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Any
Any (Bool -> Any) -> (Int -> Bool) -> SingleVar Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==)) IgnoreSorts
ig t
t
relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool
relevantInIgnoringSortAnn :: Int -> t -> Bool
relevantInIgnoringSortAnn = IgnoreSorts -> Int -> t -> Bool
forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
IgnoreInAnnotations
relevantIn :: Free t => Nat -> t -> Bool
relevantIn :: Int -> t -> Bool
relevantIn = IgnoreSorts -> Int -> t -> Bool
forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
IgnoreAll
closed :: Free t => t -> Bool
closed :: t -> Bool
closed t :: t
t = All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar All -> IgnoreSorts -> t -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (All -> SingleVar All
forall a b. a -> b -> a
const (All -> SingleVar All) -> All -> SingleVar All
forall a b. (a -> b) -> a -> b
$ Bool -> All
All Bool
False) IgnoreSorts
IgnoreNot t
t
allFreeVars :: Free t => t -> VarSet
allFreeVars :: t -> VarSet
allFreeVars = SingleVar VarSet -> IgnoreSorts -> t -> VarSet
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar VarSet
IntSet.singleton IgnoreSorts
IgnoreNot
allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring :: IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring ig :: IgnoreSorts
ig = RelevantIn VarSet -> VarSet
forall c. RelevantIn c -> c
getRelevantIn (RelevantIn VarSet -> VarSet)
-> (t -> RelevantIn VarSet) -> t -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleVar (RelevantIn VarSet)
-> IgnoreSorts -> t -> RelevantIn VarSet
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (VarSet -> RelevantIn VarSet
forall c. c -> RelevantIn c
RelevantIn (VarSet -> RelevantIn VarSet)
-> SingleVar VarSet -> SingleVar (RelevantIn VarSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleVar VarSet
IntSet.singleton) IgnoreSorts
ig
allRelevantVars :: Free t => t -> VarSet
allRelevantVars :: t -> VarSet
allRelevantVars = IgnoreSorts -> t -> VarSet
forall t. Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring IgnoreSorts
IgnoreNot
filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap f :: VarOcc -> Bool
f = IntMap VarOcc -> VarSet
forall a. IntMap a -> VarSet
IntMap.keysSet (IntMap VarOcc -> VarSet)
-> (VarMap -> IntMap VarOcc) -> VarMap -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarOcc -> Bool) -> IntMap VarOcc -> IntMap VarOcc
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter VarOcc -> Bool
f (IntMap VarOcc -> IntMap VarOcc)
-> (VarMap -> IntMap VarOcc) -> VarMap -> IntMap VarOcc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap -> IntMap VarOcc
forall a. VarMap' a -> TheVarMap' a
theVarMap
filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Variable]
filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Int]
filterVarMapToList f :: VarOcc -> Bool
f = ((Int, VarOcc) -> Int) -> [(Int, VarOcc)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, VarOcc) -> Int
forall a b. (a, b) -> a
fst ([(Int, VarOcc)] -> [Int])
-> (VarMap -> [(Int, VarOcc)]) -> VarMap -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, VarOcc) -> Bool) -> [(Int, VarOcc)] -> [(Int, VarOcc)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VarOcc -> Bool
f (VarOcc -> Bool)
-> ((Int, VarOcc) -> VarOcc) -> (Int, VarOcc) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, VarOcc) -> VarOcc
forall a b. (a, b) -> b
snd) ([(Int, VarOcc)] -> [(Int, VarOcc)])
-> (VarMap -> [(Int, VarOcc)]) -> VarMap -> [(Int, VarOcc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap VarOcc -> [(Int, VarOcc)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList (IntMap VarOcc -> [(Int, VarOcc)])
-> (VarMap -> IntMap VarOcc) -> VarMap -> [(Int, VarOcc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap -> IntMap VarOcc
forall a. VarMap' a -> TheVarMap' a
theVarMap
stronglyRigidVars :: VarMap -> VarSet
stronglyRigidVars :: VarMap -> VarSet
stronglyRigidVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap ((VarOcc -> Bool) -> VarMap -> VarSet)
-> (VarOcc -> Bool) -> VarMap -> VarSet
forall a b. (a -> b) -> a -> b
$ \case
VarOcc StronglyRigid _ -> Bool
True
_ -> Bool
False
unguardedVars :: VarMap -> VarSet
unguardedVars :: VarMap -> VarSet
unguardedVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap ((VarOcc -> Bool) -> VarMap -> VarSet)
-> (VarOcc -> Bool) -> VarMap -> VarSet
forall a b. (a -> b) -> a -> b
$ \case
VarOcc Unguarded _ -> Bool
True
_ -> Bool
False
rigidVars :: VarMap -> VarSet
rigidVars :: VarMap -> VarSet
rigidVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap ((VarOcc -> Bool) -> VarMap -> VarSet)
-> (VarOcc -> Bool) -> VarMap -> VarSet
forall a b. (a -> b) -> a -> b
$ \case
VarOcc o :: FlexRig' MetaSet
o _ -> FlexRig' MetaSet
o FlexRig' MetaSet -> [FlexRig' MetaSet] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ FlexRig' MetaSet
forall a. FlexRig' a
WeaklyRigid, FlexRig' MetaSet
forall a. FlexRig' a
Unguarded, FlexRig' MetaSet
forall a. FlexRig' a
StronglyRigid ]
allVars :: VarMap -> VarSet
allVars :: VarMap -> VarSet
allVars = IntMap VarOcc -> VarSet
forall a. IntMap a -> VarSet
IntMap.keysSet (IntMap VarOcc -> VarSet)
-> (VarMap -> IntMap VarOcc) -> VarMap -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap -> IntMap VarOcc
forall a. VarMap' a -> TheVarMap' a
theVarMap