{-# LANGUAGE RankNTypes #-}

module PlutusCore.Core.Plated
    ( kindSubkinds
    , kindSubkindsDeep
    , tyVarDeclSubkinds
    , typeTyBinds
    , typeTyVars
    , typeUniques
    , typeSubkinds
    , typeSubtypes
    , typeSubtypesDeep
    , varDeclSubtypes
    , termTyBinds
    , termBinds
    , termVars
    , termUniques
    , termSubkinds
    , termSubtypes
    , termSubtypesDeep
    , termSubterms
    , termSubtermsDeep
    , typeUniquesDeep
    , termUniquesDeep
    ) where

import PlutusCore.Core.Type
import PlutusCore.Name

import Control.Lens

infixr 6 <^>

-- | Compose two folds to make them run in parallel. The results are concatenated.
(<^>) :: Fold s a -> Fold s a -> Fold s a
(Fold s a
f1 <^> :: Fold s a -> Fold s a -> Fold s a
<^> Fold s a
f2) a -> f a
g s
s = (a -> f a) -> s -> f s
Fold s a
f1 a -> f a
g s
s f s -> f s -> f s
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (a -> f a) -> s -> f s
Fold s a
f2 a -> f a
g s
s

kindSubkinds :: Traversal' (Kind ann) (Kind ann)
kindSubkinds :: (Kind ann -> f (Kind ann)) -> Kind ann -> f (Kind ann)
kindSubkinds Kind ann -> f (Kind ann)
f Kind ann
kind0 = case Kind ann
kind0 of
    KindArrow ann
ann Kind ann
dom Kind ann
cod -> ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann (Kind ann -> Kind ann -> Kind ann)
-> f (Kind ann) -> f (Kind ann -> Kind ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind ann -> f (Kind ann)
f Kind ann
dom f (Kind ann -> Kind ann) -> f (Kind ann) -> f (Kind ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind ann -> f (Kind ann)
f Kind ann
cod
    Type{}                -> Kind ann -> f (Kind ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ann
kind0

kindSubkindsDeep :: Fold (Kind ann) (Kind ann)
kindSubkindsDeep :: (Kind ann -> f (Kind ann)) -> Kind ann -> f (Kind ann)
kindSubkindsDeep = ((Kind ann -> f (Kind ann)) -> Kind ann -> f (Kind ann))
-> (Kind ann -> f (Kind ann)) -> Kind ann -> f (Kind ann)
forall (f :: * -> *) a.
(Applicative f, Contravariant f) =>
LensLike' f a a -> LensLike' f a a
cosmosOf (Kind ann -> f (Kind ann)) -> Kind ann -> f (Kind ann)
forall ann. Traversal' (Kind ann) (Kind ann)
kindSubkinds

{-# INLINE tyVarDeclSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'TyVarDecl'.
tyVarDeclSubkinds :: Traversal' (TyVarDecl tyname a) (Kind a)
tyVarDeclSubkinds :: (Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
tyVarDeclSubkinds Kind a -> f (Kind a)
f (TyVarDecl a
a tyname
ty Kind a
k) = a -> tyname -> Kind a -> TyVarDecl tyname a
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl a
a tyname
ty (Kind a -> TyVarDecl tyname a)
-> f (Kind a) -> f (TyVarDecl tyname a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind a -> f (Kind a)
f Kind a
k

-- | Get all the direct child 'tyname a's of the given 'Type' from binders.
typeTyBinds :: Traversal' (Type tyname uni ann) tyname
typeTyBinds :: (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
typeTyBinds tyname -> f tyname
f Type tyname uni ann
ty0 = case Type tyname uni ann
ty0 of
    TyForall ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> tyname -> f tyname
f tyname
tn f tyname
-> (tyname -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \tyname
tn' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
tn' Kind ann
k Type tyname uni ann
ty
    TyLam ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty    -> tyname -> f tyname
f tyname
tn f tyname
-> (tyname -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \tyname
tn' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
tn' Kind ann
k Type tyname uni ann
ty
    TyApp{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyIFix{}             -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyFun{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyBuiltin{}          -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyVar{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

-- | Get all the direct child 'tyname a's of the given 'Type' from 'TyVar's.
typeTyVars :: Traversal' (Type tyname uni ann) tyname
typeTyVars :: (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
typeTyVars tyname -> f tyname
f Type tyname uni ann
ty0 = case Type tyname uni ann
ty0 of
    TyVar ann
ann tyname
n -> ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (tyname -> Type tyname uni ann)
-> f tyname -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tyname -> f tyname
f tyname
n
    TyForall{}  -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyLam{}     -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyApp{}     -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyIFix{}    -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyFun{}     -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyBuiltin{} -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

-- | Get all the direct child 'Unique's of the given 'Type' from binders 'TyVar's.
typeUniques :: HasUniques (Type tyname uni ann) => Traversal' (Type tyname uni ann) Unique
typeUniques :: Traversal' (Type tyname uni ann) Unique
typeUniques Unique -> f Unique
f Type tyname uni ann
ty0 = case Type tyname uni ann
ty0 of
    TyForall ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f tyname
tn f tyname
-> (tyname -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \tyname
tn' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
tn' Kind ann
k Type tyname uni ann
ty
    TyLam ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty    -> (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f tyname
tn f tyname
-> (tyname -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \tyname
tn' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
tn' Kind ann
k Type tyname uni ann
ty
    TyVar ann
ann tyname
n          -> (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f tyname
n f tyname
-> (tyname -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann
    TyApp{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyIFix{}             -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyFun{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyBuiltin{}          -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

{-# INLINE typeSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Type'.
typeSubkinds :: Traversal' (Type tyname uni ann) (Kind ann)
typeSubkinds :: (Kind ann -> f (Kind ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubkinds Kind ann -> f (Kind ann)
f Type tyname uni ann
ty0 = case Type tyname uni ann
ty0 of
    TyForall ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> Kind ann -> f (Kind ann)
f Kind ann
k f (Kind ann)
-> (Kind ann -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Kind ann
k' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
tn Kind ann
k' Type tyname uni ann
ty
    TyLam ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty    -> Kind ann -> f (Kind ann)
f Kind ann
k f (Kind ann)
-> (Kind ann -> Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Kind ann
k' -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
tn Kind ann
k' Type tyname uni ann
ty
    TyApp{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyIFix{}             -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyFun{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyBuiltin{}          -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyVar{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

{-# INLINE typeSubtypes #-}
-- | Get all the direct child 'Type's of the given 'Type'.
typeSubtypes :: Traversal' (Type tyname uni ann) (Type tyname uni ann)
typeSubtypes :: (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypes Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty0 = case Type tyname uni ann
ty0 of
    TyFun ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2    -> ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann)
-> f (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty1 f (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty2
    TyIFix ann
ann Type tyname uni ann
pat Type tyname uni ann
arg   -> ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann)
-> f (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
pat f (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
arg
    TyForall ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
tn Kind ann
k (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty
    TyLam ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty    -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
tn Kind ann
k (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty
    TyApp ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2    -> ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann)
-> f (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty1 f (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty2
    TyBuiltin{}          -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TyVar{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

-- | Get all the transitive child 'Type's of the given 'Type'.
typeSubtypesDeep :: Fold (Type tyname uni ann) (Type tyname uni ann)
typeSubtypesDeep :: (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypesDeep = ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Type tyname uni ann -> f (Type tyname uni ann))
-> (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann
-> f (Type tyname uni ann)
forall (f :: * -> *) a.
(Applicative f, Contravariant f) =>
LensLike' f a a -> LensLike' f a a
cosmosOf (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Traversal' (Type tyname uni ann) (Type tyname uni ann)
typeSubtypes

{-# INLINE varDeclSubtypes #-}
-- | Get all the direct child 'Type's of the given 'VarDecl'.
varDeclSubtypes :: Traversal' (VarDecl tyname name uni fun a) (Type tyname uni a)
varDeclSubtypes :: (Type tyname uni a -> f (Type tyname uni a))
-> VarDecl tyname name uni fun a
-> f (VarDecl tyname name uni fun a)
varDeclSubtypes Type tyname uni a -> f (Type tyname uni a)
f (VarDecl a
a name
n Type tyname uni a
ty) = a -> name -> Type tyname uni a -> VarDecl tyname name uni fun a
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl a
a name
n (Type tyname uni a -> VarDecl tyname name uni fun a)
-> f (Type tyname uni a) -> f (VarDecl tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty

-- | Get all the direct child 'tyname a's of the given 'Term' from 'TyAbs'es.
termTyBinds :: Traversal' (Term tyname name uni fun ann) tyname
termTyBinds :: (tyname -> f tyname)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termTyBinds tyname -> f tyname
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    TyAbs ann
ann tyname
tn Kind ann
k Term tyname name uni fun ann
t -> tyname -> f tyname
f tyname
tn f tyname
-> (tyname -> 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
<&> \tyname
tn' -> 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
tn' Kind ann
k Term tyname name uni fun ann
t
    Var{}            -> 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
term0
    LamAbs{}         -> 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
term0
    TyInst{}         -> 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
term0
    IWrap{}          -> 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
term0
    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
term0
    Apply{}          -> 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
term0
    Unwrap{}         -> 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
term0
    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
term0
    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
term0

-- | Get all the direct child 'name a's of the given 'Term' from 'LamAbs'es.
termBinds :: Traversal' (Term tyname name uni fun ann) name
termBinds :: (name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termBinds name -> f name
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    LamAbs ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t -> name -> f name
f name
n f name
-> (name -> 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
<&> \name
n' -> 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
n' Type tyname uni ann
ty Term tyname name uni fun ann
t
    Var{}             -> 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
term0
    TyAbs{}           -> 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
term0
    TyInst{}          -> 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
term0
    IWrap{}           -> 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
term0
    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
term0
    Apply{}           -> 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
term0
    Unwrap{}          -> 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
term0
    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
term0
    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
term0

-- | Get all the direct child 'name a's of the given 'Term' from 'Var's.
termVars :: Traversal' (Term tyname name uni fun ann) name
termVars :: (name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termVars name -> f name
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    Var ann
ann name
n  -> ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann (name -> Term tyname name uni fun ann)
-> f name -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> f name
f name
n
    TyAbs{}    -> 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
term0
    LamAbs{}   -> 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
term0
    TyInst{}   -> 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
term0
    IWrap{}    -> 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
term0
    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
term0
    Apply{}    -> 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
term0
    Unwrap{}   -> 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
term0
    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
term0
    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
term0

-- | Get all the direct child 'Unique's of the given 'Term' (including the type-level ones).
termUniques :: HasUniques (Term tyname name uni fun ann) => Traversal' (Term tyname name uni fun ann) Unique
termUniques :: Traversal' (Term tyname name uni fun ann) Unique
termUniques Unique -> f Unique
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    TyAbs ann
ann tyname
tn Kind ann
k Term tyname name uni fun ann
t  -> (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f tyname
tn f tyname
-> (tyname -> 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
<&> \tyname
tn' -> 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
tn' Kind ann
k Term tyname name uni fun ann
t
    LamAbs ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t -> (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f name
n f name
-> (name -> 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
<&> \name
n' -> 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
n' Type tyname uni ann
ty Term tyname name uni fun ann
t
    Var ann
ann name
n         -> (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
theUnique Unique -> f Unique
f name
n f name
-> (name -> 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
<&> ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann
    TyInst{}          -> 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
term0
    IWrap{}           -> 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
term0
    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
term0
    Apply{}           -> 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
term0
    Unwrap{}          -> 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
term0
    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
term0
    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
term0

{-# INLINE termSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Term'.
termSubkinds :: Traversal' (Term tyname name uni fun ann) (Kind ann)
termSubkinds :: (Kind ann -> f (Kind ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubkinds Kind ann -> f (Kind ann)
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    TyAbs ann
ann tyname
n Kind ann
k Term tyname name uni fun ann
t -> Kind ann -> f (Kind ann)
f Kind ann
k f (Kind ann)
-> (Kind 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
<&> \Kind ann
k' -> 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
n Kind ann
k' Term tyname name uni fun ann
t
    LamAbs{}        -> 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
term0
    Var{}           -> 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
term0
    TyInst{}        -> 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
term0
    IWrap{}         -> 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
term0
    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
term0
    Apply{}         -> 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
term0
    Unwrap{}        -> 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
term0
    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
term0
    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
term0

{-# INLINE termSubtypes #-}
-- | Get all the direct child 'Type's of the given 'Term'.
termSubtypes :: Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypes :: (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypes Type tyname uni ann -> f (Type tyname uni ann)
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    LamAbs ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t   -> 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
n (Type tyname uni ann
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Type tyname uni 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
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty 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
<*> 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
    TyInst ann
ann Term tyname name uni fun ann
t Type tyname uni ann
ty     -> 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
t (Type tyname uni ann -> Term tyname name uni fun ann)
-> f (Type tyname uni ann) -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty
    IWrap ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 Term tyname name uni fun ann
t -> 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
 -> Type tyname uni ann
 -> Term tyname name uni fun ann
 -> Term tyname name uni fun ann)
-> f (Type tyname uni ann)
-> f (Type tyname uni ann
      -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty1 f (Type tyname uni ann
   -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Type tyname uni ann)
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty2 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
<*> 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
    Error ann
ann Type tyname uni ann
ty        -> ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann (Type tyname uni ann -> Term tyname name uni fun ann)
-> f (Type tyname uni ann) -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> f (Type tyname uni ann)
f Type tyname uni ann
ty
    TyAbs{}             -> 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
term0
    Apply{}             -> 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
term0
    Unwrap{}            -> 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
term0
    Var{}               -> 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
term0
    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
term0
    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
term0

-- | Get all the transitive child 'Type's of the given 'Term'.
termSubtypesDeep :: Fold (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypesDeep :: (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypesDeep = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (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 -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Type tyname uni ann -> f (Type tyname uni ann))
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Type tyname uni ann -> f (Type tyname uni ann))
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Fold (Type tyname uni ann) (Type tyname uni ann)
typeSubtypesDeep

{-# INLINE termSubterms #-}
-- | Get all the direct child 'Term's of the given 'Term'.
termSubterms :: Traversal' (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubterms :: (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    LamAbs ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t   -> 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
n 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
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t
    TyInst ann
ann Term tyname name uni fun ann
t Type tyname uni ann
ty     -> 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
 -> Type tyname uni ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Type tyname uni ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t f (Type tyname uni ann -> Term tyname name uni fun ann)
-> f (Type tyname uni ann) -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty
    IWrap ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 Term tyname name uni fun ann
t -> 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
ty1 Type tyname uni ann
ty2 (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
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t
    TyAbs ann
ann tyname
n Kind ann
k Term tyname name uni fun ann
t     -> 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
n Kind ann
k (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
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t
    Apply ann
ann Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2     -> 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
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t1 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
<*> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t2
    Unwrap ann
ann Term tyname name uni fun ann
t        -> 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
<$> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f Term tyname name uni fun ann
t
    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
term0
    Var{}               -> 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
term0
    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
term0
    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
term0

-- | Get all the transitive child 'Term's of the given 'Term'.
termSubtermsDeep :: Fold (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubtermsDeep :: (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtermsDeep = ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a.
(Applicative f, Contravariant f) =>
LensLike' f a a -> LensLike' f a a
cosmosOf (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (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

-- | Get all the transitive child 'Unique's of the given 'Type'.
typeUniquesDeep :: HasUniques (Type tyname uni ann) => Fold (Type tyname uni ann) Unique
typeUniquesDeep :: Fold (Type tyname uni ann) Unique
typeUniquesDeep = (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
Fold (Type tyname uni ann) (Type tyname uni ann)
typeSubtypesDeep ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Type tyname uni ann -> f (Type tyname uni ann))
-> ((Unique -> f Unique)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (Unique -> f Unique)
-> Type tyname uni ann
-> f (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
HasUniques (Type tyname uni ann) =>
Traversal' (Type tyname uni ann) Unique
typeUniques

-- | Get all the transitive child 'Unique's of the given 'Term' (including the type-level ones).
termUniquesDeep :: HasUniques (Term tyname name uni fun ann) => Fold (Term tyname name uni fun ann) Unique
termUniquesDeep :: Fold (Term tyname name uni fun ann) Unique
termUniquesDeep = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (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 -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Unique -> f Unique)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (Unique -> f Unique)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Unique -> f Unique)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (Unique -> f Unique)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann.
HasUniques (Type tyname uni ann) =>
Fold (Type tyname uni ann) Unique
typeUniquesDeep Fold (Term tyname name uni fun ann) Unique
-> Fold (Term tyname name uni fun ann) Unique
-> Fold (Term tyname name uni fun ann) Unique
forall s a. Fold s a -> Fold s a -> Fold s a
<^> forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
Traversal' (Term tyname name uni fun ann) Unique
Fold (Term tyname name uni fun ann) Unique
termUniques)