{-# LANGUAGE UndecidableInstances       #-} -- Due to underdetermined var in IsVarSet multi-param typeclass

-- | Computing the free variables of a term.
--
-- The distinction between rigid and strongly rigid occurrences comes from:
--   Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)
--
-- The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly
-- in t.  It might have a solution if the occurrence is not strongly rigid, e.g.
--
--   x = \f -> suc (f (x (\ y -> k)))  has  x = \f -> suc (f (suc k))
--
-- [Jason C. Reed, PhD thesis, page 106]
--
-- Under coinductive constructors, occurrences are never strongly rigid.
-- Also, function types and lambdas do not establish strong rigidity.
-- Only inductive constructors do so.
-- (See issue 1271).
--
-- If you need the occurrence information for all free variables, you can use
-- @freeVars@ which has amoungst others this instance
-- @
--    freeVars :: Term -> VarMap
-- @
-- From @VarMap@, specific information can be extracted, e.g.,
-- @
--    relevantVars :: VarMap -> VarSet
--    relevantVars = filterVarMap isRelevant
-- @
--
-- To just check the status of a single free variable, there are more
-- efficient methods, e.g.,
-- @
--    freeIn :: Nat -> Term -> Bool
-- @
--
-- Tailored optimized variable checks can be implemented as semimodules to 'VarOcc',
-- see, for example, 'VarCounts' or 'SingleFlexRig'.

module Agda.TypeChecking.Free
    ( VarCounts(..)
    , Free
    , IsVarSet(..)
    , IgnoreSorts(..)
    , freeVars, freeVars', filterVarMap, filterVarMapToList
    , runFree, rigidVars, stronglyRigidVars, unguardedVars, allVars
    , flexibleVars
    , allFreeVars
    , allRelevantVars, allRelevantVarsIgnoring
    , freeVarsIgnore
    , freeIn, freeInIgnoringSorts, isBinderUsed
    , relevantIn, relevantInIgnoringSortAnn
    , FlexRig'(..), FlexRig
    , LensFlexRig(..), isFlexible, isUnguarded, isStronglyRigid, isWeaklyRigid
    , VarOcc'(..), VarOcc
    , varOccurrenceIn
    , flexRigOccurrenceIn
    , closed
    , MetaSet
    , insertMetaSet, foldrMetaSet, metaSetToBlocker
    ) where

import Prelude hiding (null)

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
  -- ( Free(..) , FreeEnv(..), initFreeEnv
  -- , FlexRig, FlexRig'(..)
  -- , VarOcc(..), topVarOcc, TheVarMap, theVarMap, IgnoreSorts(..), Variable, SingleVar
  -- , MetaSet, insertMetaSet, foldrMetaSet
  -- , IsVarSet(..), runFreeM
  -- )

import Agda.Utils.Singleton

---------------------------------------------------------------------------
-- * Simple variable set implementations.

type VarSet = IntSet

-- In most cases we don't care about the VarOcc.

instance IsVarSet () VarSet where withVarOcc :: VarOcc' () -> VarSet -> VarSet
withVarOcc VarOcc' ()
_ = forall a. a -> a
id
instance IsVarSet () [Int]  where withVarOcc :: VarOcc' () -> [Int] -> [Int]
withVarOcc VarOcc' ()
_ = forall a. a -> a
id
instance IsVarSet () Any    where withVarOcc :: VarOcc' () -> Any -> Any
withVarOcc VarOcc' ()
_ = forall a. a -> a
id
instance IsVarSet () All    where withVarOcc :: VarOcc' () -> All -> All
withVarOcc VarOcc' ()
_ = forall a. a -> a
id

---------------------------------------------------------------------------
-- * Plain variable occurrence counting.

newtype VarCounts = VarCounts { VarCounts -> IntMap Int
varCounts :: IntMap Int }

instance Semigroup VarCounts where
  VarCounts IntMap Int
fv1 <> :: VarCounts -> VarCounts -> VarCounts
<> VarCounts IntMap Int
fv2 = IntMap Int -> VarCounts
VarCounts (forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Num a => a -> a -> a
(+) IntMap Int
fv1 IntMap Int
fv2)

instance Monoid VarCounts where
  mempty :: VarCounts
mempty = IntMap Int -> VarCounts
VarCounts forall a. IntMap a
IntMap.empty
  mappend :: VarCounts -> VarCounts -> VarCounts
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance IsVarSet () VarCounts where
  withVarOcc :: VarOcc' () -> VarCounts -> VarCounts
withVarOcc VarOcc' ()
_ = forall a. a -> a
id

instance Singleton Variable VarCounts where
  singleton :: Int -> VarCounts
singleton Int
i = IntMap Int -> VarCounts
VarCounts forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> IntMap a
IntMap.singleton Int
i Int
1

---------------------------------------------------------------------------
-- * Collecting free variables (generic).

-- | Collect all free variables together with information about their occurrence.
--
-- Doesn't go inside solved metas, but collects the variables from a
-- metavariable application @X ts@ as @flexibleVars@.
{-# SPECIALIZE freeVars :: Free a => a -> VarMap #-}
freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c
freeVars :: forall a c t. (IsVarSet a c, Singleton Int c, Free t) => t -> c
freeVars = 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 :: forall a c t.
(IsVarSet a c, Singleton Int c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore = forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree forall el coll. Singleton el coll => el -> coll
singleton

-- Specialization to typical monoids
{-# SPECIALIZE runFree :: Free a => SingleVar Any      -> IgnoreSorts -> a -> Any #-}
-- Specialization to Term
{-# SPECIALIZE runFree :: SingleVar Any      -> IgnoreSorts -> Term -> Any #-}

-- | Compute free variables.
runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c
runFree :: forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree SingleVar c
single IgnoreSorts
i t
t = -- bench $  -- Benchmarking is expensive (4% on std-lib)
  forall a c.
IsVarSet a c =>
SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM SingleVar c
single IgnoreSorts
i (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
t)
  where
  bench :: a -> a
bench = forall a. Account -> a -> a
Bench.billToPure [ Phase
Bench.Typing , Phase
Bench.Free ]

---------------------------------------------------------------------------
-- * Occurrence computation for a single variable.

-- ** Full free occurrence info for a single variable.

-- | Get the full occurrence information of a free variable.
varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc
varOccurrenceIn :: forall a. Free a => Int -> a -> Maybe VarOcc
varOccurrenceIn = forall a. Free a => IgnoreSorts -> Int -> a -> Maybe VarOcc
varOccurrenceIn' IgnoreSorts
IgnoreNot

varOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe VarOcc
varOccurrenceIn' :: forall a. Free a => IgnoreSorts -> Int -> a -> Maybe VarOcc
varOccurrenceIn' IgnoreSorts
ig Int
x a
t = SingleVarOcc -> Maybe VarOcc
theSingleVarOcc forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> SingleVarOcc
sg IgnoreSorts
ig a
t
  where
  sg :: Int -> SingleVarOcc
sg Int
y = if Int
x forall a. Eq a => a -> a -> Bool
== Int
y then SingleVarOcc
oneSingleVarOcc else forall a. Monoid a => a
mempty

-- | "Collection" just keeping track of the occurrence of a single variable.
--   'Nothing' means variable does not occur freely.
newtype SingleVarOcc = SingleVarOcc { SingleVarOcc -> Maybe VarOcc
theSingleVarOcc :: Maybe VarOcc }

oneSingleVarOcc :: SingleVarOcc
oneSingleVarOcc :: SingleVarOcc
oneSingleVarOcc = Maybe VarOcc -> SingleVarOcc
SingleVarOcc forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. VarOcc' a
oneVarOcc

-- | Hereditary Semigroup instance for 'Maybe'.
--   (The default instance for 'Maybe' may not be the hereditary one.)
instance Semigroup SingleVarOcc where
  SingleVarOcc Maybe VarOcc
Nothing <> :: SingleVarOcc -> SingleVarOcc -> SingleVarOcc
<> SingleVarOcc
s = SingleVarOcc
s
  SingleVarOcc
s <> SingleVarOcc Maybe VarOcc
Nothing = SingleVarOcc
s
  SingleVarOcc (Just VarOcc
o) <> SingleVarOcc (Just VarOcc
o') = Maybe VarOcc -> SingleVarOcc
SingleVarOcc forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ VarOcc
o forall a. Semigroup a => a -> a -> a
<> VarOcc
o'

instance Monoid SingleVarOcc where
  mempty :: SingleVarOcc
mempty = Maybe VarOcc -> SingleVarOcc
SingleVarOcc forall a. Maybe a
Nothing
  mappend :: SingleVarOcc -> SingleVarOcc -> SingleVarOcc
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance IsVarSet MetaSet SingleVarOcc where
  withVarOcc :: VarOcc -> SingleVarOcc -> SingleVarOcc
withVarOcc VarOcc
o = Maybe VarOcc -> SingleVarOcc
SingleVarOcc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc VarOcc
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleVarOcc -> Maybe VarOcc
theSingleVarOcc

-- ** Flexible /rigid occurrence info for a single variable.

-- | Get the full occurrence information of a free variable.
flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig
flexRigOccurrenceIn :: forall a. Free a => Int -> a -> Maybe (FlexRig' MetaSet)
flexRigOccurrenceIn = forall a.
Free a =>
IgnoreSorts -> Int -> a -> Maybe (FlexRig' MetaSet)
flexRigOccurrenceIn' IgnoreSorts
IgnoreNot

flexRigOccurrenceIn' :: Free a => IgnoreSorts -> Nat -> a -> Maybe FlexRig
flexRigOccurrenceIn' :: forall a.
Free a =>
IgnoreSorts -> Int -> a -> Maybe (FlexRig' MetaSet)
flexRigOccurrenceIn' IgnoreSorts
ig Int
x a
t = SingleFlexRig -> Maybe (FlexRig' MetaSet)
theSingleFlexRig forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> SingleFlexRig
sg IgnoreSorts
ig a
t
  where
  sg :: Int -> SingleFlexRig
sg Int
y = if Int
x forall a. Eq a => a -> a -> Bool
== Int
y then SingleFlexRig
oneSingleFlexRig else forall a. Monoid a => a
mempty

-- | "Collection" just keeping track of the occurrence of a single variable.
--   'Nothing' means variable does not occur freely.
newtype SingleFlexRig = SingleFlexRig { SingleFlexRig -> Maybe (FlexRig' MetaSet)
theSingleFlexRig :: Maybe FlexRig }

oneSingleFlexRig :: SingleFlexRig
oneSingleFlexRig :: SingleFlexRig
oneSingleFlexRig = Maybe (FlexRig' MetaSet) -> SingleFlexRig
SingleFlexRig forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. FlexRig' a
oneFlexRig

-- | Hereditary Semigroup instance for 'Maybe'.
--   (The default instance for 'Maybe' may not be the hereditary one.)
instance Semigroup SingleFlexRig where
  SingleFlexRig Maybe (FlexRig' MetaSet)
Nothing <> :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
<> SingleFlexRig
s = SingleFlexRig
s
  SingleFlexRig
s <> SingleFlexRig Maybe (FlexRig' MetaSet)
Nothing = SingleFlexRig
s
  SingleFlexRig (Just FlexRig' MetaSet
o) <> SingleFlexRig (Just FlexRig' MetaSet
o') = Maybe (FlexRig' MetaSet) -> SingleFlexRig
SingleFlexRig forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig FlexRig' MetaSet
o FlexRig' MetaSet
o'

instance Monoid SingleFlexRig where
  mempty :: SingleFlexRig
mempty = Maybe (FlexRig' MetaSet) -> SingleFlexRig
SingleFlexRig forall a. Maybe a
Nothing
  mappend :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance IsVarSet MetaSet SingleFlexRig where
  withVarOcc :: VarOcc -> SingleFlexRig -> SingleFlexRig
withVarOcc VarOcc
o = Maybe (FlexRig' MetaSet) -> SingleFlexRig
SingleFlexRig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig forall a b. (a -> b) -> a -> b
$ forall a. VarOcc' a -> FlexRig' a
varFlexRig VarOcc
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleFlexRig -> Maybe (FlexRig' MetaSet)
theSingleFlexRig

-- ** Plain free occurrence.

-- | Check if a variable is free, possibly ignoring sorts.
freeIn' :: Free a => IgnoreSorts -> Nat -> a -> Bool
freeIn' :: forall a. Free a => IgnoreSorts -> Int -> a -> Bool
freeIn' IgnoreSorts
ig Int
x a
t = Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
x forall a. Eq a => a -> a -> Bool
==)) IgnoreSorts
ig a
t

{-# SPECIALIZE freeIn :: Nat -> Term -> Bool #-}
freeIn :: Free a => Nat -> a -> Bool
freeIn :: forall a. Free a => Int -> a -> Bool
freeIn = forall a. Free a => IgnoreSorts -> Int -> a -> Bool
freeIn' IgnoreSorts
IgnoreNot

freeInIgnoringSorts :: Free a => Nat -> a -> Bool
freeInIgnoringSorts :: forall a. Free a => Int -> a -> Bool
freeInIgnoringSorts = forall a. Free a => IgnoreSorts -> Int -> a -> Bool
freeIn' IgnoreSorts
IgnoreAll

-- UNUSED Liang-Ting Chen 2019-07-16
--freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool
--freeInIgnoringSortAnn = freeIn' IgnoreInAnnotations

-- | Is the variable bound by the abstraction actually used?
isBinderUsed :: Free a => Abs a -> Bool
isBinderUsed :: forall a. Free a => Abs a -> Bool
isBinderUsed NoAbs{}   = Bool
False
isBinderUsed (Abs ArgName
_ a
x) = Int
0 forall a. Free a => Int -> a -> Bool
`freeIn` a
x

-- ** Relevant free occurrence.

newtype RelevantIn c = RelevantIn {forall c. RelevantIn c -> c
getRelevantIn :: c}
  deriving (NonEmpty (RelevantIn c) -> RelevantIn c
RelevantIn c -> RelevantIn c -> 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 :: forall b. Integral b => 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, 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
Monoid)

instance IsVarSet a c => IsVarSet a (RelevantIn c) where  -- UndecidableInstances
  withVarOcc :: VarOcc' a -> RelevantIn c -> RelevantIn c
withVarOcc VarOcc' a
o RelevantIn c
x
    | forall a. LensRelevance a => a -> Bool
isIrrelevant VarOcc' a
o = forall a. Monoid a => a
mempty
    | Bool
otherwise = forall c. c -> RelevantIn c
RelevantIn forall a b. (a -> b) -> a -> b
$ forall a c. IsVarSet a c => VarOcc' a -> c -> c
withVarOcc VarOcc' a
o forall a b. (a -> b) -> a -> b
$ forall c. RelevantIn c -> c
getRelevantIn RelevantIn c
x

relevantIn' :: Free t => IgnoreSorts -> Nat -> t -> Bool
relevantIn' :: forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
ig Int
x t
t = Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. RelevantIn c -> c
getRelevantIn forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (forall c. c -> RelevantIn c
RelevantIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
x forall a. Eq a => a -> a -> Bool
==)) IgnoreSorts
ig t
t

relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool
relevantInIgnoringSortAnn :: forall a. Free a => Int -> a -> Bool
relevantInIgnoringSortAnn = forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
IgnoreInAnnotations

relevantIn :: Free t => Nat -> t -> Bool
relevantIn :: forall a. Free a => Int -> a -> Bool
relevantIn = forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
IgnoreAll

---------------------------------------------------------------------------
-- * Occurrences of all free variables.

-- | Is the term entirely closed (no free variables)?
closed :: Free t => t -> Bool
closed :: forall t. Free t => t -> Bool
closed t
t = All -> Bool
getAll forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Bool -> All
All Bool
False) IgnoreSorts
IgnoreNot t
t

-- | Collect all free variables.
allFreeVars :: Free t => t -> VarSet
allFreeVars :: forall t. Free t => t -> VarSet
allFreeVars = forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> VarSet
IntSet.singleton IgnoreSorts
IgnoreNot

-- | Collect all relevant free variables, possibly ignoring sorts.
allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring :: forall t. Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring IgnoreSorts
ig = forall c. RelevantIn c -> c
getRelevantIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (forall c. c -> RelevantIn c
RelevantIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> VarSet
IntSet.singleton) IgnoreSorts
ig

-- | Collect all relevant free variables, excluding the "unused" ones.
allRelevantVars :: Free t => t -> VarSet
allRelevantVars :: forall t. Free t => t -> VarSet
allRelevantVars = forall t. Free t => IgnoreSorts -> t -> VarSet
allRelevantVarsIgnoring IgnoreSorts
IgnoreNot

---------------------------------------------------------------------------
-- * Backwards-compatible interface to 'freeVars'.

filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap VarOcc -> Bool
f = forall a. IntMap a -> VarSet
IntMap.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter VarOcc -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. VarMap' a -> TheVarMap' a
theVarMap

filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Variable]
filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Int]
filterVarMapToList VarOcc -> Bool
f = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (VarOcc -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> [(Int, a)]
IntMap.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. VarMap' a -> TheVarMap' a
theVarMap

-- | Variables under only and at least one inductive constructor(s).
stronglyRigidVars :: VarMap -> VarSet
stronglyRigidVars :: VarMap -> VarSet
stronglyRigidVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap forall a b. (a -> b) -> a -> b
$ \case
  VarOcc FlexRig' MetaSet
StronglyRigid Modality
_ -> Bool
True
  VarOcc
_ -> Bool
False

-- | Variables at top or only under inductive record constructors
--   λs and Πs.
--   The purpose of recording these separately is that they
--   can still become strongly rigid if put under a constructor
--   whereas weakly rigid ones stay weakly rigid.
unguardedVars :: VarMap -> VarSet
unguardedVars :: VarMap -> VarSet
unguardedVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap forall a b. (a -> b) -> a -> b
$ \case
  VarOcc FlexRig' MetaSet
Unguarded Modality
_ -> Bool
True
  VarOcc
_ -> Bool
False

-- UNUSED Liang-Ting Chen 2019-07-16
---- | Ordinary rigid variables, e.g., in arguments of variables or functions.
--weaklyRigidVars :: VarMap -> VarSet
--weaklyRigidVars = filterVarMap $ \case
--  VarOcc WeaklyRigid _ -> True
--  _ -> False

-- | Rigid variables: either strongly rigid, unguarded, or weakly rigid.
rigidVars :: VarMap -> VarSet
rigidVars :: VarMap -> VarSet
rigidVars = (VarOcc -> Bool) -> VarMap -> VarSet
filterVarMap forall a b. (a -> b) -> a -> b
$ \case
  VarOcc FlexRig' MetaSet
o Modality
_ -> FlexRig' MetaSet
o forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ forall a. FlexRig' a
WeaklyRigid, forall a. FlexRig' a
Unguarded, forall a. FlexRig' a
StronglyRigid ]

-- | Variables occuring in arguments of metas.
--  These are only potentially free, depending how the meta variable is instantiated.
--  The set contains the id's of the meta variables that this variable is an argument to.
flexibleVars :: VarMap -> IntMap MetaSet
flexibleVars :: VarMap -> IntMap MetaSet
flexibleVars (VarMap IntMap VarOcc
m) = (forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
`IntMap.mapMaybe` IntMap VarOcc
m) forall a b. (a -> b) -> a -> b
$ \case
 VarOcc (Flexible MetaSet
ms) Modality
_ -> forall a. a -> Maybe a
Just MetaSet
ms
 VarOcc
_ -> forall a. Maybe a
Nothing

---- | Variables in irrelevant arguments and under a @DontCare@, i.e.,
----   in irrelevant positions.
--irrelevantVars :: VarMap -> VarSet
--irrelevantVars = filterVarMap isIrrelevant

allVars :: VarMap -> VarSet
allVars :: VarMap -> VarSet
allVars = forall a. IntMap a -> VarSet
IntMap.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. VarMap' a -> TheVarMap' a
theVarMap