    {-# 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
        ) 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
    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 (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' ())
    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' :: forall a. Free a => IgnoreSorts -> Int -> a -> Maybe (FlexRig' ())
    flexRigOccurrenceIn' IgnoreSorts
    ig Int
    x 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 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' ())
    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

    -- | Hereditary Semigroup instance for 'Maybe'.
    --   (The default instance for 'Maybe' may not be the hereditary one.)
    instance Semigroup SingleFlexRig where
      SingleFlexRig Maybe (FlexRig' ())
    Nothing <> :: SingleFlexRig -> SingleFlexRig -> SingleFlexRig
    <> SingleFlexRig
    s = SingleFlexRig
    s
      SingleFlexRig
    s <> SingleFlexRig Maybe (FlexRig' ())
    Nothing = SingleFlexRig
    s
      SingleFlexRig (Just FlexRig' ()
    o) <> SingleFlexRig (Just 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 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

    -- ** 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
    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, 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
    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 (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