{-|
  Copyright   :  (C) 2012-2016, University of Twente
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  Christiaan Baaij <christiaan.baaij@gmail.com>

  Free variable calculations
-}

{-# LANGUAGE LambdaCase   #-}
{-# LANGUAGE RankNTypes   #-}
{-# LANGUAGE ViewPatterns #-}

module Clash.Core.FreeVars
  (-- * Free variable calculation
    typeFreeVars
  , termFreeVarsX
  , freeIds
  , freeLocalVars
  , freeLocalIds
  , globalIds
  , termFreeTyVars
  , tyFVsOfTypes
  , localFVsOfTerms
  , hasLocalFreeVars
  -- * Fast
  , noFreeVarsOfType
  -- * occurrence check
  , localIdOccursIn
  , globalIdOccursIn
  , localIdDoesNotOccurIn
  , localIdsDoNotOccurIn
  , localVarsDoNotOccurIn
  -- * Internal
  , typeFreeVars'
  , termFreeVars'
  )
where

import qualified Control.Lens           as Lens
import Control.Lens.Fold                (Fold)
import Control.Lens.Getter              (Contravariant)
import Data.Coerce
import qualified Data.IntSet            as IntSet
import Data.Monoid                      (All (..), Any (..))

import Clash.Core.Term                  (Pat (..), Term (..), TickInfo (..))
import Clash.Core.Type                  (Type (..))
import Clash.Core.Var                   (Id, IdScope (..), TyVar, Var (..))
import Clash.Core.VarEnv                (VarSet, unitVarSet)

-- | Gives the free type-variables in a Type, implemented as a 'Fold'
--
-- The 'Fold' is closed over the types of its variables, so:
--
-- @
-- foldMapOf typeFreeVars unitVarSet ((a:* -> k) Int) = {a, k}
-- @
typeFreeVars :: Fold Type TyVar
typeFreeVars :: (TyVar -> f TyVar) -> Type -> f Type
typeFreeVars = (forall b. Var b -> Bool)
-> IntSet -> (TyVar -> f TyVar) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' (Bool -> Var b -> Bool
forall a b. a -> b -> a
const Bool
True) IntSet
IntSet.empty

-- | Gives the "interesting" free variables in a Type, implemented as a 'Fold'
--
-- The 'Fold' is closed over the types of variables, so:
--
-- @
-- foldMapOf (typeFreeVars' (const True) IntSet.empty) unitVarSet ((a:* -> k) Int) = {a, k}
-- @
--
-- Note [Closing over kind variables]
--
-- Consider the type
--
-- > forall k . b -> k
--
-- where
--
-- > b :: k -> Type
--
-- When we close over the free variables of @forall k . b -> k@, i.e. @b@, then
-- the @k@ in @b :: k -> Type@ is most definitely /not/ the @k@ in
-- @forall k . b -> k@. So when a type variable is free, i.e. not in the inScope
-- set, its kind variables also aren´t; so in order to prevent collisions due to
-- shadowing we close using an empty inScope set.
--
-- See also: https://git.haskell.org/ghc.git/commitdiff/503514b94f8dc7bd9eab5392206649aee45f140b
typeFreeVars'
  :: (Contravariant f, Applicative f)
  => (forall b . Var b -> Bool)
  -- ^ Predicate telling whether a variable is interesting
  -> IntSet.IntSet
  -- ^ Uniques of the variables in scope, used by 'termFreeVars''
  -> (Var a -> f (Var a))
  -> Type
  -> f Type
typeFreeVars' :: (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' interesting :: forall b. Var b -> Bool
interesting is :: IntSet
is f :: Var a -> f (Var a)
f = IntSet -> Type -> f Type
go IntSet
is where
  go :: IntSet -> Type -> f Type
go inScope :: IntSet
inScope = \case
    VarTy tv :: TyVar
tv -> f Type
tv1 f Type -> f Type -> f Type
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* IntSet -> Type -> f Type
go IntSet
inScope1 (TyVar -> Type
forall a. Var a -> Type
varType TyVar
tv)
      where
        isInteresting :: Bool
isInteresting = TyVar -> Bool
forall b. Var b -> Bool
interesting TyVar
tv
        tvInScope :: Bool
tvInScope     = TyVar -> Unique
forall a. Var a -> Unique
varUniq TyVar
tv Unique -> IntSet -> Bool
`IntSet.member` IntSet
inScope
        inScope1 :: IntSet
inScope1
          | Bool
tvInScope = IntSet
inScope
          | Bool
otherwise = IntSet
IntSet.empty -- See Note [Closing over type variables]

        tv1 :: f Type
tv1 | Bool
isInteresting
            , Bool -> Bool
not Bool
tvInScope
            = TyVar -> Type
VarTy (TyVar -> Type) -> (Var a -> TyVar) -> Var a -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> TyVar
forall a b. Coercible a b => a -> b
coerce (Var a -> Type) -> f (Var a) -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var a -> f (Var a)
f (TyVar -> Var a
forall a b. Coercible a b => a -> b
coerce TyVar
tv)
            | Bool
otherwise
            = Type -> f Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> Type
VarTy TyVar
tv)

    ForAllTy tv :: TyVar
tv ty :: Type
ty -> TyVar -> Type -> Type
ForAllTy (TyVar -> Type -> Type) -> f TyVar -> f (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> TyVar -> f TyVar
goBndr IntSet
inScope TyVar
tv
                               f (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Type -> f Type
go (Unique -> IntSet -> IntSet
IntSet.insert (TyVar -> Unique
forall a. Var a -> Unique
varUniq TyVar
tv) IntSet
inScope) Type
ty
    AppTy l :: Type
l r :: Type
r -> Type -> Type -> Type
AppTy (Type -> Type -> Type) -> f Type -> f (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Type -> f Type
go IntSet
inScope Type
l f (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Type -> f Type
go IntSet
inScope Type
r
    ty :: Type
ty -> Type -> f Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty

  goBndr :: IntSet -> TyVar -> f TyVar
goBndr inScope :: IntSet
inScope tv :: TyVar
tv = (\t :: Type
t -> TyVar
tv {varType :: Type
varType = Type
t}) (Type -> TyVar) -> f Type -> f TyVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Type -> f Type
go IntSet
inScope (TyVar -> Type
forall a. Var a -> Type
varType TyVar
tv)

-- | Check whether an identifier does not occur free in a term
localIdDoesNotOccurIn
  :: Id
  -> Term
  -> Bool
localIdDoesNotOccurIn :: Id -> Term -> Bool
localIdDoesNotOccurIn v :: Id
v e :: Term
e = All -> Bool
getAll (Getting All Term Id -> (Id -> All) -> Term -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting All Term Id
Fold Term Id
freeLocalIds (Bool -> All
All (Bool -> All) -> (Id -> Bool) -> Id -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
v)) Term
e)

-- | Check whether a set of identifiers does not occur free in a term
localIdsDoNotOccurIn
  :: [Id]
  -> Term
  -> Bool
localIdsDoNotOccurIn :: [Id] -> Term -> Bool
localIdsDoNotOccurIn vs :: [Id]
vs e :: Term
e =
  All -> Bool
getAll (Getting All Term Id -> (Id -> All) -> Term -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting All Term Id
Fold Term Id
freeLocalIds (Bool -> All
All (Bool -> All) -> (Id -> Bool) -> Id -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Id]
vs)) Term
e)

-- | Check whether a set of variables does not occur free in a term
localVarsDoNotOccurIn
  :: [Var a]
  -> Term
  -> Bool
localVarsDoNotOccurIn :: [Var a] -> Term -> Bool
localVarsDoNotOccurIn vs :: [Var a]
vs e :: Term
e =
  All -> Bool
getAll (Getting All Term (Var a) -> (Var a -> All) -> Term -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting All Term (Var a)
forall a. Fold Term (Var a)
freeLocalVars (Bool -> All
All (Bool -> All) -> (Var a -> Bool) -> Var a -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var a -> [Var a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Var a]
vs)) Term
e)

-- | Check whether a local identifier occurs free in a term
localIdOccursIn
  :: Id
  -> Term
  -> Bool
localIdOccursIn :: Id -> Term -> Bool
localIdOccursIn v :: Id
v e :: Term
e = Any -> Bool
getAny (Getting Any Term Id -> (Id -> Any) -> Term -> Any
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting Any Term Id
Fold Term Id
freeLocalIds (Bool -> Any
Any (Bool -> Any) -> (Id -> Bool) -> Id -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
v)) Term
e)

-- | Check whether a local identifier occurs free in a term
globalIdOccursIn
  :: Id
  -> Term
  -> Bool
globalIdOccursIn :: Id -> Term -> Bool
globalIdOccursIn v :: Id
v e :: Term
e = Any -> Bool
getAny (Getting Any Term Id -> (Id -> Any) -> Term -> Any
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting Any Term Id
Fold Term Id
globalIds (Bool -> Any
Any (Bool -> Any) -> (Id -> Bool) -> Id -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
v)) Term
e)

-- | Calculate the /local/ free variable of an expression: the free type
-- variables and the free identifiers that are not bound in the global
-- environment.
freeLocalVars :: Fold Term (Var a)
freeLocalVars :: (Var a -> f (Var a)) -> Term -> f Term
freeLocalVars = (forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isLocalVar where
  isLocalVar :: Var a -> Bool
isLocalVar (Id {idScope :: forall a. Var a -> IdScope
idScope = IdScope
GlobalId}) = Bool
False
  isLocalVar _ = Bool
True

-- | Gives the free identifiers of a Term, implemented as a 'Fold'
freeIds :: Fold Term Id
freeIds :: (Id -> f Id) -> Term -> f Term
freeIds = (forall b. Var b -> Bool) -> (Id -> f Id) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isId where
  isId :: Var a -> Bool
isId (Id {}) = Bool
True
  isId _       = Bool
False

-- | Calculate the /local/ free identifiers of an expression: the free
-- identifiers that are not bound in the global environment.
freeLocalIds :: Fold Term Id
freeLocalIds :: (Id -> f Id) -> Term -> f Term
freeLocalIds = (forall b. Var b -> Bool) -> (Id -> f Id) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isLocalId where
  isLocalId :: Var a -> Bool
isLocalId (Id {idScope :: forall a. Var a -> IdScope
idScope = IdScope
LocalId}) = Bool
True
  isLocalId _ = Bool
False

-- | Calculate the /global/ free identifiers of an expression: the free
-- identifiers that are bound in the global environment.
globalIds :: Fold Term Id
globalIds :: (Id -> f Id) -> Term -> f Term
globalIds = (forall b. Var b -> Bool) -> (Id -> f Id) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isGlobalId where
  isGlobalId :: Var a -> Bool
isGlobalId (Id {idScope :: forall a. Var a -> IdScope
idScope = IdScope
GlobalId}) = Bool
True
  isGlobalId _ = Bool
False

-- | Determines if term has any locally free variables. That is, the free type
-- variables and the free identifiers that are not bound in the global
-- scope.
hasLocalFreeVars :: Term -> Bool
hasLocalFreeVars :: Term -> Bool
hasLocalFreeVars = Getting Any Term (Var Any) -> Term -> Bool
forall s a. Getting Any s a -> s -> Bool
Lens.notNullOf Getting Any Term (Var Any)
forall a. Fold Term (Var a)
freeLocalVars

-- | Gives the free type-variables of a Term, implemented as a 'Fold'
--
-- The 'Fold' is closed over the types of variables, so:
--
-- @
-- foldMapOf termFreeTyVars unitVarSet (case (x : (a:* -> k) Int)) of {}) = {a, k}
-- @
termFreeTyVars :: Fold Term TyVar
termFreeTyVars :: (TyVar -> f TyVar) -> Term -> f Term
termFreeTyVars = (forall b. Var b -> Bool) -> (TyVar -> f TyVar) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isTV where
  isTV :: Var a -> Bool
isTV (TyVar {}) = Bool
True
  isTV _          = Bool
False

-- | Gives the free variables of a Term, implemented as a 'Fold'
--
-- The 'Fold' is closed over the types of variables, so:
--
-- @
-- foldMapOf termFreeVars unitVarSet (case (x : (a:* -> k) Int)) of {}) = {x, a, k}
-- @
--
-- __NB__ this collects both global and local IDs, and you almost __NEVER__ want
-- to use this. Use one of the other FV calculations instead
termFreeVarsX :: Fold Term (Var a)
termFreeVarsX :: (Var a -> f (Var a)) -> Term -> f Term
termFreeVarsX = (forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' (Bool -> Var b -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | Gives the "interesting" free variables in a Term, implemented as a 'Fold'
--
-- The 'Fold' is closed over the types of variables, so:
--
-- @
-- foldMapOf (termFreeVars' (const True)) unitVarSet (case (x : (a:* -> k) Int)) of {}) = {x, a, k}
-- @
--
-- Note [Closing over type variables]
--
-- Consider the term
--
-- > /\(k :: Type) -> \(b :: k) -> a
--
-- where
--
-- > a :: k
--
-- When we close over the free variables of @/\k -> \(b :: k) -> (a :: k)@, i.e.
-- @a@, then the @k@ in @a :: k@ is most definitely /not/ the @k@ in introduced
-- by the @/\k ->@. So when a term variable is free, i.e. not in the inScope
-- set, its type variables also aren´t; so in order to prevent collisions due to
-- shadowing we close using an empty inScope set.
--
-- See also: https://git.haskell.org/ghc.git/commitdiff/503514b94f8dc7bd9eab5392206649aee45f140b
termFreeVars'
  :: (Contravariant f, Applicative f)
  => (forall b . Var b -> Bool)
  -- ^ Predicate telling whether a variable is interesting
  -> (Var a -> f (Var a))
  -> Term
  -> f Term
termFreeVars' :: (forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' interesting :: forall b. Var b -> Bool
interesting f :: Var a -> f (Var a)
f = IntSet -> Term -> f Term
go IntSet
IntSet.empty where
  go :: IntSet -> Term -> f Term
go inScope :: IntSet
inScope = \case
    Var v :: Id
v -> f Term
v1 f Term -> f Type -> f Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope1 Var a -> f (Var a)
f (Id -> Type
forall a. Var a -> Type
varType Id
v)
      where
        isInteresting :: Bool
isInteresting = Id -> Bool
forall b. Var b -> Bool
interesting Id
v
        vInScope :: Bool
vInScope      = Id -> Unique
forall a. Var a -> Unique
varUniq Id
v Unique -> IntSet -> Bool
`IntSet.member` IntSet
inScope
        inScope1 :: IntSet
inScope1
          | Bool
vInScope  = IntSet
inScope
          | Bool
otherwise = IntSet
IntSet.empty -- See Note [Closing over type variables]

        v1 :: f Term
v1 | Bool
isInteresting
           , Bool -> Bool
not Bool
vInScope
           = Id -> Term
Var (Id -> Term) -> (Var a -> Id) -> Var a -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> Id
forall a b. Coercible a b => a -> b
coerce (Var a -> Term) -> f (Var a) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var a -> f (Var a)
f (Id -> Var a
forall a b. Coercible a b => a -> b
coerce Id
v)
           | Bool
otherwise
           = Term -> f Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> Term
Var Id
v)

    Lam id_ :: Id
id_ tm :: Term
tm -> Id -> Term -> Term
Lam (Id -> Term -> Term) -> f Id -> f (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Id -> f Id
forall a. IntSet -> Var a -> f (Var a)
goBndr IntSet
inScope Id
id_
                      f (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go (Unique -> IntSet -> IntSet
IntSet.insert (Id -> Unique
forall a. Var a -> Unique
varUniq Id
id_) IntSet
inScope) Term
tm
    TyLam tv :: TyVar
tv tm :: Term
tm -> TyVar -> Term -> Term
TyLam (TyVar -> Term -> Term) -> f TyVar -> f (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> TyVar -> f TyVar
forall a. IntSet -> Var a -> f (Var a)
goBndr IntSet
inScope TyVar
tv
                         f (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go (Unique -> IntSet -> IntSet
IntSet.insert (TyVar -> Unique
forall a. Var a -> Unique
varUniq TyVar
tv) IntSet
inScope) Term
tm
    App l :: Term
l r :: Term
r -> Term -> Term -> Term
App (Term -> Term -> Term) -> f Term -> f (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Term -> f Term
go IntSet
inScope Term
l f (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope Term
r
    TyApp l :: Term
l r :: Type
r -> Term -> Type -> Term
TyApp (Term -> Type -> Term) -> f Term -> f (Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Term -> f Term
go IntSet
inScope Term
l
                       f (Type -> Term) -> f Type -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f Type
r
    Letrec bs :: [LetBinding]
bs e :: Term
e -> [LetBinding] -> Term -> Term
Letrec ([LetBinding] -> Term -> Term)
-> f [LetBinding] -> f (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LetBinding -> f LetBinding) -> [LetBinding] -> f [LetBinding]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (IntSet -> LetBinding -> f LetBinding
goBind IntSet
inScope') [LetBinding]
bs f (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope' Term
e
      where inScope' :: IntSet
inScope' = (Unique -> IntSet -> IntSet) -> IntSet -> [Unique] -> IntSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Unique -> IntSet -> IntSet
IntSet.insert IntSet
inScope ((LetBinding -> Unique) -> [LetBinding] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Unique
forall a. Var a -> Unique
varUniq(Id -> Unique) -> (LetBinding -> Id) -> LetBinding -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
.LetBinding -> Id
forall a b. (a, b) -> a
fst) [LetBinding]
bs)
    Case subj :: Term
subj ty :: Type
ty alts :: [Alt]
alts -> Term -> Type -> [Alt] -> Term
Case (Term -> Type -> [Alt] -> Term)
-> f Term -> f (Type -> [Alt] -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Term -> f Term
go IntSet
inScope Term
subj
                              f (Type -> [Alt] -> Term) -> f Type -> f ([Alt] -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f Type
ty
                              f ([Alt] -> Term) -> f [Alt] -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Alt -> f Alt) -> [Alt] -> f [Alt]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (IntSet -> Alt -> f Alt
goAlt IntSet
inScope) [Alt]
alts
    Cast tm :: Term
tm t1 :: Type
t1 t2 :: Type
t2 -> Term -> Type -> Type -> Term
Cast (Term -> Type -> Type -> Term)
-> f Term -> f (Type -> Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Term -> f Term
go IntSet
inScope Term
tm
                          f (Type -> Type -> Term) -> f Type -> f (Type -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f Type
t1
                          f (Type -> Term) -> f Type -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f Type
t2
    Tick tick :: TickInfo
tick tm :: Term
tm -> TickInfo -> Term -> Term
Tick (TickInfo -> Term -> Term) -> f TickInfo -> f (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> TickInfo -> f TickInfo
goTick IntSet
inScope TickInfo
tick f (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope Term
tm
    tm :: Term
tm -> Term -> f Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tm

  goBndr :: IntSet -> Var a -> f (Var a)
goBndr inScope :: IntSet
inScope v :: Var a
v =
    (\t :: Type
t -> Var a
v  {varType :: Type
varType = Type
t}) (Type -> Var a) -> f Type -> f (Var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f (Var a -> Type
forall a. Var a -> Type
varType Var a
v)

  goBind :: IntSet -> LetBinding -> f LetBinding
goBind inScope :: IntSet
inScope (l :: Id
l,r :: Term
r) = (,) (Id -> Term -> LetBinding) -> f Id -> f (Term -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> Id -> f Id
forall a. IntSet -> Var a -> f (Var a)
goBndr IntSet
inScope Id
l f (Term -> LetBinding) -> f Term -> f LetBinding
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope Term
r

  goAlt :: IntSet -> Alt -> f Alt
goAlt inScope :: IntSet
inScope (pat :: Pat
pat,alt :: Term
alt) = case Pat
pat of
    DataPat dc :: DataCon
dc tvs :: [TyVar]
tvs ids :: [Id]
ids -> (,) (Pat -> Term -> Alt) -> f Pat -> f (Term -> Alt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCon -> [TyVar] -> [Id] -> Pat
DataPat (DataCon -> [TyVar] -> [Id] -> Pat)
-> f DataCon -> f ([TyVar] -> [Id] -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> f DataCon
forall (f :: * -> *) a. Applicative f => a -> f a
pure DataCon
dc
                                           f ([TyVar] -> [Id] -> Pat) -> f [TyVar] -> f ([Id] -> Pat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TyVar -> f TyVar) -> [TyVar] -> f [TyVar]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (IntSet -> TyVar -> f TyVar
forall a. IntSet -> Var a -> f (Var a)
goBndr IntSet
inScope') [TyVar]
tvs
                                           f ([Id] -> Pat) -> f [Id] -> f Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Id -> f Id) -> [Id] -> f [Id]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (IntSet -> Id -> f Id
forall a. IntSet -> Var a -> f (Var a)
goBndr IntSet
inScope') [Id]
ids)
                              f (Term -> Alt) -> f Term -> f Alt
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope' Term
alt
      where
        inScope' :: IntSet
inScope' = (Unique -> IntSet -> IntSet) -> IntSet -> [Unique] -> IntSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Unique -> IntSet -> IntSet
IntSet.insert
                         ((Unique -> IntSet -> IntSet) -> IntSet -> [Unique] -> IntSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Unique -> IntSet -> IntSet
IntSet.insert IntSet
inScope ((TyVar -> Unique) -> [TyVar] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Unique
forall a. Var a -> Unique
varUniq [TyVar]
tvs))
                         ((Id -> Unique) -> [Id] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Unique
forall a. Var a -> Unique
varUniq [Id]
ids)
    _ -> (,) (Pat -> Term -> Alt) -> f Pat -> f (Term -> Alt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pat -> f Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pat
pat f (Term -> Alt) -> f Term -> f Alt
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntSet -> Term -> f Term
go IntSet
inScope Term
alt

  goTick :: IntSet -> TickInfo -> f TickInfo
goTick inScope :: IntSet
inScope = \case
    NameMod m :: NameMod
m ty :: Type
ty -> NameMod -> Type -> TickInfo
NameMod NameMod
m (Type -> TickInfo) -> f Type -> f TickInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
forall (f :: * -> *) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
interesting IntSet
inScope Var a -> f (Var a)
f Type
ty
    tick :: TickInfo
tick         -> TickInfo -> f TickInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure TickInfo
tick

-- | Determine whether a type has no free type variables.
noFreeVarsOfType
  :: Type
  -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType ty :: Type
ty = case Type
ty of
  VarTy {}    -> Bool
False
  ForAllTy {} -> All -> Bool
getAll (Getting All Type TyVar -> (TyVar -> All) -> Type -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting All Type TyVar
Fold Type TyVar
typeFreeVars (All -> TyVar -> All
forall a b. a -> b -> a
const (Bool -> All
All Bool
False)) Type
ty)
  AppTy l :: Type
l r :: Type
r   -> Type -> Bool
noFreeVarsOfType Type
l Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
r
  _           -> Bool
True

-- | Collect the free variables of a collection of type into a set
tyFVsOfTypes
  :: Foldable f
  => f Type
  -> VarSet
tyFVsOfTypes :: f Type -> VarSet
tyFVsOfTypes = (Type -> VarSet) -> f Type -> VarSet
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> VarSet
go
 where
  go :: Type -> VarSet
go = Getting VarSet Type TyVar -> (TyVar -> VarSet) -> Type -> VarSet
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting VarSet Type TyVar
Fold Type TyVar
typeFreeVars TyVar -> VarSet
forall a. Var a -> VarSet
unitVarSet

-- | Collect the free variables of a collection of terms into a set
localFVsOfTerms
  :: Foldable f
  => f Term
  -> VarSet
localFVsOfTerms :: f Term -> VarSet
localFVsOfTerms = (Term -> VarSet) -> f Term -> VarSet
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> VarSet
go
 where
  go :: Term -> VarSet
go = Getting VarSet Term (Var Any)
-> (Var Any -> VarSet) -> Term -> VarSet
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting VarSet Term (Var Any)
forall a. Fold Term (Var a)
freeLocalVars Var Any -> VarSet
forall a. Var a -> VarSet
unitVarSet