{-# 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' ()
_ = VarSet -> VarSet
forall a. a -> a
id
instance IsVarSet () [Int]  where withVarOcc :: VarOcc' () -> [Int] -> [Int]
withVarOcc VarOcc' ()
_ = [Int] -> [Int]
forall a. a -> a
id
instance IsVarSet () Any    where withVarOcc :: VarOcc' () -> Any -> Any
withVarOcc VarOcc' ()
_ = Any -> Any
forall a. a -> a
id
instance IsVarSet () All    where withVarOcc :: VarOcc' () -> All -> All
withVarOcc VarOcc' ()
_ = All -> All
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 ((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 VarOcc' ()
_ = VarCounts -> VarCounts
forall a. a -> a
id

instance Singleton Variable VarCounts where
  singleton :: Int -> VarCounts
singleton 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 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 = 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 :: forall a c t.
(IsVarSet a c, Singleton Int c, Free t) =>
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

-- 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)
  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
forall a c. 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 ]

---------------------------------------------------------------------------
-- * 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 = 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' :: forall a. Free a => IgnoreSorts -> Int -> a -> Maybe VarOcc
varOccurrenceIn' IgnoreSorts
ig Int
x 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 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

-- | "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 (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

-- | 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 (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 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 a b. (a -> b) -> Maybe a -> Maybe b
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

-- ** 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 = IgnoreSorts -> Int -> a -> Maybe (FlexRig' MetaSet)
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 (SingleFlexRig -> Maybe (FlexRig' MetaSet))
-> SingleFlexRig -> Maybe (FlexRig' MetaSet)
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 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

-- | "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 (Maybe (FlexRig' MetaSet) -> SingleFlexRig)
-> Maybe (FlexRig' MetaSet) -> SingleFlexRig
forall a b. (a -> b) -> a -> b
$ FlexRig' MetaSet -> Maybe (FlexRig' MetaSet)
forall a. a -> Maybe a
Just (FlexRig' MetaSet -> Maybe (FlexRig' MetaSet))
-> FlexRig' MetaSet -> Maybe (FlexRig' MetaSet)
forall a b. (a -> b) -> a -> b
$ FlexRig' MetaSet
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 (Maybe (FlexRig' MetaSet) -> SingleFlexRig)
-> Maybe (FlexRig' MetaSet) -> SingleFlexRig
forall a b. (a -> b) -> a -> b
$ FlexRig' MetaSet -> Maybe (FlexRig' MetaSet)
forall a. a -> Maybe a
Just (FlexRig' MetaSet -> Maybe (FlexRig' MetaSet))
-> FlexRig' MetaSet -> Maybe (FlexRig' MetaSet)
forall a b. (a -> b) -> a -> b
$ FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet
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 Maybe (FlexRig' MetaSet)
forall a. Maybe a
Nothing
  mappend :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
mappend = SingleFlexRig -> SingleFlexRig -> SingleFlexRig
forall a. Semigroup a => a -> a -> a
(<>)

instance IsVarSet MetaSet SingleFlexRig where
  withVarOcc :: VarOcc -> SingleFlexRig -> SingleFlexRig
withVarOcc VarOcc
o = Maybe (FlexRig' MetaSet) -> SingleFlexRig
SingleFlexRig (Maybe (FlexRig' MetaSet) -> SingleFlexRig)
-> (SingleFlexRig -> Maybe (FlexRig' MetaSet))
-> SingleFlexRig
-> SingleFlexRig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRig' MetaSet -> FlexRig' MetaSet)
-> Maybe (FlexRig' MetaSet) -> Maybe (FlexRig' MetaSet)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet)
-> FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet
forall a b. (a -> b) -> a -> b
$ VarOcc -> FlexRig' MetaSet
forall a. VarOcc' a -> FlexRig' a
varFlexRig VarOcc
o) (Maybe (FlexRig' MetaSet) -> Maybe (FlexRig' MetaSet))
-> (SingleFlexRig -> Maybe (FlexRig' MetaSet))
-> SingleFlexRig
-> Maybe (FlexRig' MetaSet)
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 (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 :: forall a. Free a => 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 :: forall a. Free a => Int -> a -> Bool
freeInIgnoringSorts = IgnoreSorts -> Int -> a -> Bool
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 Int -> a -> Bool
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
(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
$c<> :: forall c.
Semigroup c =>
RelevantIn c -> RelevantIn c -> RelevantIn c
<> :: RelevantIn c -> RelevantIn c -> RelevantIn c
$csconcat :: forall c. Semigroup c => NonEmpty (RelevantIn c) -> RelevantIn c
sconcat :: NonEmpty (RelevantIn c) -> RelevantIn c
$cstimes :: forall c b.
(Semigroup c, Integral b) =>
b -> RelevantIn c -> RelevantIn c
stimes :: forall b. Integral b => b -> 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
$cmempty :: forall c. Monoid c => RelevantIn c
mempty :: RelevantIn c
$cmappend :: forall c. Monoid c => RelevantIn c -> RelevantIn c -> RelevantIn c
mappend :: RelevantIn c -> RelevantIn c -> RelevantIn c
$cmconcat :: forall c. Monoid c => [RelevantIn c] -> RelevantIn c
mconcat :: [RelevantIn 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
    | 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' :: forall a. Free a => IgnoreSorts -> Int -> a -> Bool
relevantIn' IgnoreSorts
ig Int
x 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 :: forall a. Free a => Int -> a -> Bool
relevantInIgnoringSortAnn = IgnoreSorts -> Int -> t -> Bool
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 = IgnoreSorts -> Int -> t -> Bool
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 (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

-- | Collect all free variables.
allFreeVars :: Free t => t -> VarSet
allFreeVars :: forall t. Free t => 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

-- | 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 = 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

-- | Collect all relevant free variables, excluding the "unused" ones.
allRelevantVars :: Free t => t -> VarSet
allRelevantVars :: forall t. Free t => t -> VarSet
allRelevantVars = IgnoreSorts -> t -> VarSet
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 = 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 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

-- | Variables under only and at least one inductive constructor(s).
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 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 ((VarOcc -> Bool) -> VarMap -> VarSet)
-> (VarOcc -> Bool) -> VarMap -> VarSet
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 ((VarOcc -> Bool) -> VarMap -> VarSet)
-> (VarOcc -> Bool) -> VarMap -> VarSet
forall a b. (a -> b) -> a -> b
$ \case
  VarOcc FlexRig' MetaSet
o Modality
_ -> FlexRig' MetaSet
o FlexRig' MetaSet -> [FlexRig' MetaSet] -> Bool
forall a. Eq a => a -> [a] -> 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 ]

-- | 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) = ((VarOcc -> Maybe MetaSet) -> IntMap VarOcc -> IntMap MetaSet
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
`IntMap.mapMaybe` IntMap VarOcc
m) ((VarOcc -> Maybe MetaSet) -> IntMap MetaSet)
-> (VarOcc -> Maybe MetaSet) -> IntMap MetaSet
forall a b. (a -> b) -> a -> b
$ \case
 VarOcc (Flexible MetaSet
ms) Modality
_ -> MetaSet -> Maybe MetaSet
forall a. a -> Maybe a
Just MetaSet
ms
 VarOcc
_ -> Maybe MetaSet
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 = 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