module PlutusCore.Subst
    ( substTyVarA
    , substVarA
    , substTyVar
    , substVar
    , termSubstNamesM
    , termSubstTyNamesM
    , typeSubstTyNamesM
    , termSubstNames
    , termSubstTyNames
    , typeSubstTyNames
    , termSubstFreeNamesA
    , termSubstFreeNames
    , fvTerm
    , ftvTerm
    , ftvTy
    , vTerm
    , tvTerm
    , tvTy
    , uniquesType
    , uniquesTerm
    ) where

import PlutusPrelude

import PlutusCore.Core
import PlutusCore.Name

import Control.Lens
import Data.Functor.Foldable (cata)
import Data.Set as Set
import Data.Set.Lens (setOf)

purely :: ((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely :: ((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely = ((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
coerce

{-# INLINE substTyVarA #-}
-- | Applicatively replace a type variable using the given function.
substTyVarA
    :: Applicative f
    => (tyname -> f (Maybe (Type tyname uni ann)))
    -> Type tyname uni ann
    -> f (Type tyname uni ann)
substTyVarA :: (tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA tyname -> f (Maybe (Type tyname uni ann))
tynameF ty :: Type tyname uni ann
ty@(TyVar ann
_ tyname
tyname) = Type tyname uni ann
-> Maybe (Type tyname uni ann) -> Type tyname uni ann
forall a. a -> Maybe a -> a
fromMaybe Type tyname uni ann
ty (Maybe (Type tyname uni ann) -> Type tyname uni ann)
-> f (Maybe (Type tyname uni ann)) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tyname -> f (Maybe (Type tyname uni ann))
tynameF tyname
tyname
substTyVarA tyname -> f (Maybe (Type tyname uni ann))
_       Type tyname uni ann
ty                  = Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty

-- | Applicatively replace a variable using the given function.
substVarA
    :: Applicative f
    => (name -> f (Maybe (Term tyname name uni fun ann)))
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann)
substVarA :: (name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA name -> f (Maybe (Term tyname name uni fun ann))
nameF t :: Term tyname name uni fun ann
t@(Var ann
_ name
name) = Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun ann
t (Maybe (Term tyname name uni fun ann)
 -> Term tyname name uni fun ann)
-> f (Maybe (Term tyname name uni fun ann))
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> f (Maybe (Term tyname name uni fun ann))
nameF name
name
substVarA name -> f (Maybe (Term tyname name uni fun ann))
_     Term tyname name uni fun ann
t              = Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
t

-- | Replace a type variable using the given function.
substTyVar
    :: (tyname -> Maybe (Type tyname uni ann))
    -> Type tyname uni ann
    -> Type tyname uni ann
substTyVar :: (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
substTyVar = ((tyname -> Identity (Maybe (Type tyname uni ann)))
 -> Type tyname uni ann -> Identity (Type tyname uni ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA

-- | Replace a variable using the given function.
substVar
    :: (name -> Maybe (Term tyname name uni fun ann))
    -> Term tyname name uni fun ann
    -> Term tyname name uni fun ann
substVar :: (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
substVar = ((name -> Identity (Maybe (Term tyname name uni fun ann)))
 -> Term tyname name uni fun ann
 -> Identity (Term tyname name uni fun ann))
-> (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
Applicative f =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA

{-# INLINE typeSubstTyNamesM #-}
-- | Naively monadically substitute type names (i.e. do not substitute binders).
-- INLINE is important here because the function is too polymorphic (determined from profiling)
typeSubstTyNamesM
    :: Monad m
    => (tyname -> m (Maybe (Type tyname uni ann)))
    -> Type tyname uni ann
    -> m (Type tyname uni ann)
typeSubstTyNamesM :: (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
typeSubstTyNamesM = LensLike
  (WrappedMonad m)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
-> (Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad m)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Traversal' (Type tyname uni ann) (Type tyname uni ann)
typeSubtypes ((Type tyname uni ann -> m (Type tyname uni ann))
 -> Type tyname uni ann -> m (Type tyname uni ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
    -> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA

-- | Naively monadically substitute names using the given function (i.e. do not substitute binders).
termSubstNamesM
    :: Monad m
    => (name -> m (Maybe (Term tyname name uni fun ann)))
    -> Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann)
termSubstNamesM :: (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM = LensLike
  (WrappedMonad m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> (Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Traversal'
  (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> m (Term tyname name uni fun ann))
-> ((name -> m (Maybe (Term tyname name uni fun ann)))
    -> Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann))
-> (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
Applicative f =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA

-- | Naively monadically substitute type names using the given function (i.e. do not substitute binders).
termSubstTyNamesM
    :: Monad m
    => (tyname -> m (Maybe (Type tyname uni ann)))
    -> Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann)
termSubstTyNamesM :: (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM =
    LensLike
  (WrappedMonad m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> (Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Traversal'
  (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> m (Term tyname name uni fun ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
    -> Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLike
  m
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
-> LensLike
     m
     (Term tyname name uni fun ann)
     (Term tyname name uni fun ann)
     (Type tyname uni ann)
     (Type tyname uni ann)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike
  m
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun ann.
Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypes LensLike
  m
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
-> ((tyname -> m (Maybe (Type tyname uni ann)))
    -> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLike
  (WrappedMonad m)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
-> (Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad m)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
  (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Traversal' (Type tyname uni ann) (Type tyname uni ann)
typeSubtypes ((Type tyname uni ann -> m (Type tyname uni ann))
 -> Type tyname uni ann -> m (Type tyname uni ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
    -> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA

-- | Naively substitute type names (i.e. do not substitute binders).
typeSubstTyNames
    :: (tyname -> Maybe (Type tyname uni ann))
    -> Type tyname uni ann
    -> Type tyname uni ann
typeSubstTyNames :: (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames = ((tyname -> Identity (Maybe (Type tyname uni ann)))
 -> Type tyname uni ann -> Identity (Type tyname uni ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
typeSubstTyNamesM

-- | Naively substitute names using the given function (i.e. do not substitute binders).
termSubstNames
    :: (name -> Maybe (Term tyname name uni fun ann))
    -> Term tyname name uni fun ann
    -> Term tyname name uni fun ann
termSubstNames :: (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
termSubstNames = ((name -> Identity (Maybe (Term tyname name uni fun ann)))
 -> Term tyname name uni fun ann
 -> Identity (Term tyname name uni fun ann))
-> (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (m :: * -> *) name tyname (uni :: * -> *) fun ann.
Monad m =>
(name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM

-- | Naively substitute type names using the given function (i.e. do not substitute binders).
termSubstTyNames
    :: (tyname -> Maybe (Type tyname uni ann))
    -> Term tyname name uni fun ann
    -> Term tyname name uni fun ann
termSubstTyNames :: (tyname -> Maybe (Type tyname uni ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
termSubstTyNames = ((tyname -> Identity (Maybe (Type tyname uni ann)))
 -> Term tyname name uni fun ann
 -> Identity (Term tyname name uni fun ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann name fun.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM

-- | Applicatively substitute *free* names using the given function.
termSubstFreeNamesA
    :: (Applicative f, HasUnique name TermUnique)
    => (name -> f (Maybe (Term tyname name uni fun ann)))
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann)
termSubstFreeNamesA :: (name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubstFreeNamesA name -> f (Maybe (Term tyname name uni fun ann))
f = Set TermUnique
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a.
(Ord a, HasUnique name a) =>
Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set TermUnique
forall a. Set a
Set.empty where
    go :: Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs var :: Term tyname name uni fun ann
var@(Var ann
_ name
name)           =
        if (name
name name -> Getting a name a -> a
forall s a. s -> Getting a s a -> a
^. Getting a name a
forall a unique. HasUnique a unique => Lens' a unique
unique) a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`member` Set a
bvs
            then Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
var
            else Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun ann
var (Maybe (Term tyname name uni fun ann)
 -> Term tyname name uni fun ann)
-> f (Maybe (Term tyname name uni fun ann))
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> f (Maybe (Term tyname name uni fun ann))
f name
name
    go Set a
bvs (TyAbs ann
ann tyname
name Kind ann
kind Term tyname name uni fun ann
body) = ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann tyname
name Kind ann
kind (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
body
    go Set a
bvs (LamAbs ann
ann name
name Type tyname uni ann
ty Term tyname name uni fun ann
body)  = ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann name
name Type tyname uni ann
ty (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
insert (name
name name -> Getting a name a -> a
forall s a. s -> Getting a s a -> a
^. Getting a name a
forall a unique. HasUnique a unique => Lens' a unique
unique) Set a
bvs) Term tyname name uni fun ann
body
    go Set a
bvs (Apply ann
ann Term tyname name uni fun ann
fun Term tyname name uni fun ann
arg)        = ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (Term tyname name uni fun ann
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
fun f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
arg
    go Set a
bvs (TyInst ann
ann Term tyname name uni fun ann
term Type tyname uni ann
ty)       = Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
term f (Term tyname name uni fun ann)
-> (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Term tyname name uni fun ann
term' -> ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann Term tyname name uni fun ann
term' Type tyname uni ann
ty
    go Set a
bvs (Unwrap ann
ann Term tyname name uni fun ann
term)          = ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
ann (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
term
    go Set a
bvs (IWrap ann
ann Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term)   = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann Type tyname uni ann
pat Type tyname uni ann
arg (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set a
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
go Set a
bvs Term tyname name uni fun ann
term
    go Set a
_   term :: Term tyname name uni fun ann
term@Constant{}            = Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term
    go Set a
_   term :: Term tyname name uni fun ann
term@Builtin{}             = Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term
    go Set a
_   term :: Term tyname name uni fun ann
term@Error{}               = Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term

-- | Substitute *free* names using the given function.
termSubstFreeNames
    :: HasUnique name TermUnique
    => (name -> Maybe (Term tyname name uni fun ann))
    -> Term tyname name uni fun ann
    -> Term tyname name uni fun ann
termSubstFreeNames :: (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
termSubstFreeNames = ((name -> Identity (Maybe (Term tyname name uni fun ann)))
 -> Term tyname name uni fun ann
 -> Identity (Term tyname name uni fun ann))
-> (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
(Applicative f, HasUnique name TermUnique) =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubstFreeNamesA

-- Free variables

-- | Get all the free term variables in a term.
fvTerm :: Ord name => Term tyname name uni fun ann -> Set name
fvTerm :: Term tyname name uni fun ann -> Set name
fvTerm = (Base (Term tyname name uni fun ann) (Set name) -> Set name)
-> Term tyname name uni fun ann -> Set name
forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base (Term tyname name uni fun ann) (Set name) -> Set name
forall a tyname (uni :: * -> *) fun ann.
Ord a =>
TermF tyname a uni fun ann (Set a) -> Set a
f
  where
    f :: TermF tyname a uni fun ann (Set a) -> Set a
f (VarF ann
_ a
n)        = a -> Set a
forall a. a -> Set a
singleton a
n
    f (TyAbsF ann
_ tyname
_ Kind ann
_ Set a
t)  = Set a
t
    f (LamAbsF ann
_ a
n Type tyname uni ann
_ Set a
t) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
delete a
n Set a
t
    f (ApplyF ann
_ Set a
t1 Set a
t2)  = Set a
t1 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`union` Set a
t2
    f (TyInstF ann
_ Set a
t Type tyname uni ann
_)   = Set a
t
    f (UnwrapF ann
_ Set a
t)     = Set a
t
    f (IWrapF ann
_ Type tyname uni ann
_ Type tyname uni ann
_ Set a
t)  = Set a
t
    f ConstantF{}       = Set a
forall a. Set a
Set.empty
    f BuiltinF{}        = Set a
forall a. Set a
Set.empty
    f ErrorF{}          = Set a
forall a. Set a
Set.empty

-- | Get all the free type variables in a term.
ftvTerm :: Ord tyname => Term tyname name uni fun ann -> Set tyname
ftvTerm :: Term tyname name uni fun ann -> Set tyname
ftvTerm = (Base (Term tyname name uni fun ann) (Set tyname) -> Set tyname)
-> Term tyname name uni fun ann -> Set tyname
forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base (Term tyname name uni fun ann) (Set tyname) -> Set tyname
forall tyname name (uni :: * -> *) fun ann.
Ord tyname =>
TermF tyname name uni fun ann (Set tyname) -> Set tyname
f
  where
    f :: TermF tyname name uni fun ann (Set tyname) -> Set tyname
f (TyAbsF ann
_ tyname
ty Kind ann
_ Set tyname
t)    = tyname -> Set tyname -> Set tyname
forall a. Ord a => a -> Set a -> Set a
delete tyname
ty Set tyname
t
    f (LamAbsF ann
_ name
_ Type tyname uni ann
ty Set tyname
t)   = Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
`union` Set tyname
t
    f (ApplyF ann
_ Set tyname
t1 Set tyname
t2)     = Set tyname
t1 Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
`union` Set tyname
t2
    f (TyInstF ann
_ Set tyname
t Type tyname uni ann
ty)     = Set tyname
t Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
`union` Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty
    f (UnwrapF ann
_ Set tyname
t)        = Set tyname
t
    f (IWrapF ann
_ Type tyname uni ann
pat Type tyname uni ann
arg Set tyname
t) = Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
pat Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
`union` Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
arg Set tyname -> Set tyname -> Set tyname
forall a. Ord a => Set a -> Set a -> Set a
`union` Set tyname
t
    f (ErrorF ann
_ Type tyname uni ann
ty)        = Type tyname uni ann -> Set tyname
forall tyname (uni :: * -> *) ann.
Ord tyname =>
Type tyname uni ann -> Set tyname
ftvTy Type tyname uni ann
ty
    f VarF{}               = Set tyname
forall a. Set a
Set.empty
    f ConstantF{}          = Set tyname
forall a. Set a
Set.empty
    f BuiltinF{}           = Set tyname
forall a. Set a
Set.empty

-- | Get all the free type variables in a type.
ftvTy :: Ord tyname => Type tyname uni ann -> Set tyname
ftvTy :: Type tyname uni ann -> Set tyname
ftvTy = (Base (Type tyname uni ann) (Set tyname) -> Set tyname)
-> Type tyname uni ann -> Set tyname
forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base (Type tyname uni ann) (Set tyname) -> Set tyname
forall a (uni :: * -> *) ann.
Ord a =>
TypeF a uni ann (Set a) -> Set a
f
  where
    f :: TypeF a uni ann (Set a) -> Set a
f (TyVarF ann
_ a
ty)          = a -> Set a
forall a. a -> Set a
singleton a
ty
    f (TyFunF ann
_ Set a
i Set a
o)         = Set a
i Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`union` Set a
o
    f (TyIFixF ann
_ Set a
pat Set a
arg)    = Set a
pat Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`union` Set a
arg
    f (TyForallF ann
_ a
bnd Kind ann
_ Set a
ty) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
delete a
bnd Set a
ty
    f (TyLamF ann
_ a
bnd Kind ann
_ Set a
ty)    = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
delete a
bnd Set a
ty
    f (TyAppF ann
_ Set a
ty1 Set a
ty2)     = Set a
ty1 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`union` Set a
ty2
    f TyBuiltinF{}           = Set a
forall a. Set a
Set.empty

-- | Get all the term variables in a term.
vTerm :: Ord name => Term tyname name uni fun ann -> Set name
vTerm :: Term tyname name uni fun ann -> Set name
vTerm = Getting (Set name) (Term tyname name uni fun ann) name
-> Term tyname name uni fun ann -> Set name
forall a s. Getting (Set a) s a -> s -> Set a
setOf (Getting (Set name) (Term tyname name uni fun ann) name
 -> Term tyname name uni fun ann -> Set name)
-> Getting (Set name) (Term tyname name uni fun ann) name
-> Term tyname name uni fun ann
-> Set name
forall a b. (a -> b) -> a -> b
$ (Term tyname name uni fun ann
 -> Const (Set name) (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Const (Set name) (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Fold (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubtermsDeep ((Term tyname name uni fun ann
  -> Const (Set name) (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> Const (Set name) (Term tyname name uni fun ann))
-> Getting (Set name) (Term tyname name uni fun ann) name
-> Getting (Set name) (Term tyname name uni fun ann) name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Set name) (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
Traversal' (Term tyname name uni fun ann) name
termVars

-- | Get all the type variables in a term.
tvTerm :: Ord tyname => Term tyname name uni fun ann -> Set tyname
tvTerm :: Term tyname name uni fun ann -> Set tyname
tvTerm = Getting (Set tyname) (Term tyname name uni fun ann) tyname
-> Term tyname name uni fun ann -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf (Getting (Set tyname) (Term tyname name uni fun ann) tyname
 -> Term tyname name uni fun ann -> Set tyname)
-> Getting (Set tyname) (Term tyname name uni fun ann) tyname
-> Term tyname name uni fun ann
-> Set tyname
forall a b. (a -> b) -> a -> b
$ (Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
-> Term tyname name uni fun ann
-> Const (Set tyname) (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Fold (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypesDeep ((Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
 -> Term tyname name uni fun ann
 -> Const (Set tyname) (Term tyname name uni fun ann))
-> ((tyname -> Const (Set tyname) tyname)
    -> Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
-> Getting (Set tyname) (Term tyname name uni fun ann) tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> Const (Set tyname) tyname)
-> Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Traversal' (Type tyname uni ann) tyname
typeTyVars

-- | Get all the type variables in a type.
tvTy :: Ord tyname => Type tyname uni ann -> Set tyname
tvTy :: Type tyname uni ann -> Set tyname
tvTy = Getting (Set tyname) (Type tyname uni ann) tyname
-> Type tyname uni ann -> Set tyname
forall a s. Getting (Set a) s a -> s -> Set a
setOf (Getting (Set tyname) (Type tyname uni ann) tyname
 -> Type tyname uni ann -> Set tyname)
-> Getting (Set tyname) (Type tyname uni ann) tyname
-> Type tyname uni ann
-> Set tyname
forall a b. (a -> b) -> a -> b
$ (Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
-> Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Fold (Type tyname uni ann) (Type tyname uni ann)
typeSubtypesDeep ((Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
 -> Type tyname uni ann -> Const (Set tyname) (Type tyname uni ann))
-> Getting (Set tyname) (Type tyname uni ann) tyname
-> Getting (Set tyname) (Type tyname uni ann) tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Set tyname) (Type tyname uni ann) tyname
forall tyname (uni :: * -> *) ann.
Traversal' (Type tyname uni ann) tyname
typeTyVars

-- All uniques

-- | Get all the uniques in a type.
uniquesType :: HasUniques (Type tyname uni ann) => Type tyname uni ann -> Set Unique
uniquesType :: Type tyname uni ann -> Set Unique
uniquesType = Getting (Set Unique) (Type tyname uni ann) Unique
-> Type tyname uni ann -> Set Unique
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set Unique) (Type tyname uni ann) Unique
forall tyname (uni :: * -> *) ann.
HasUniques (Type tyname uni ann) =>
Fold (Type tyname uni ann) Unique
typeUniquesDeep

-- | Get all the uniques in a term (including the type-level ones).
uniquesTerm :: HasUniques (Term tyname name uni fun ann) => Term tyname name uni fun ann -> Set Unique
uniquesTerm :: Term tyname name uni fun ann -> Set Unique
uniquesTerm = Getting (Set Unique) (Term tyname name uni fun ann) Unique
-> Term tyname name uni fun ann -> Set Unique
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set Unique) (Term tyname name uni fun ann) Unique
forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
Fold (Term tyname name uni fun ann) Unique
termUniquesDeep