-- editorconfig-checker-disable-file
{-# LANGUAGE RankNTypes #-}

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

import PlutusPrelude ((<^>))

import PlutusCore.Core.Type
import PlutusCore.Name.Unique

import Control.Lens
import Universe

kindSubkinds :: Traversal' (Kind ann) (Kind ann)
kindSubkinds :: forall ann (f :: * -> *).
Applicative f =>
(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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ann
kind0

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

-- | Get all the direct child 'Kind's of the given 'TyVarDecl'.
tyVarDeclSubkinds :: Traversal' (TyVarDecl tyname a) (Kind a)
tyVarDeclSubkinds :: forall tyname a (f :: * -> *).
Applicative f =>
(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
{-# INLINE tyVarDeclSubkinds #-}

-- | Get all the direct child 'tyname a's of the given 'Type' from binders.
typeTyBinds :: Traversal' (Type tyname uni ann) tyname
typeTyBinds :: forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TySOP{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
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 :: forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TySOP{}     -> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
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 :: forall tyname (uni :: * -> *) ann.
HasUniques (Type tyname uni ann) =>
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
Lens' tyname 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
Lens' tyname 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
Lens' tyname 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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TySOP{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0

-- | Get all the direct child 'Kind's of the given 'Type'.
typeSubkinds :: Traversal' (Type tyname uni ann) (Kind ann)
typeSubkinds :: forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
    TySOP{}              -> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
{-# INLINE typeSubkinds #-}

-- | Get all the direct child 'Type's of the given 'Type'.
typeSubtypes :: Traversal' (Type tyname uni ann) (Type tyname uni ann)
typeSubtypes :: forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(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 a b. f (a -> b) -> f a -> f b
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 a b. f (a -> b) -> f a -> f b
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 a b. f (a -> b) -> f a -> f b
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
    TySOP ann
ann [[Type tyname uni ann]]
tyls       -> ann -> [[Type tyname uni ann]] -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ([[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])
-> [[Type tyname uni ann]] -> f [[Type tyname uni ann]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (([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])
-> (Type tyname uni ann -> f (Type tyname uni ann))
-> [[Type tyname uni ann]]
-> f [[Type tyname uni 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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) Type tyname uni ann -> f (Type tyname uni ann)
f [[Type tyname uni ann]]
tyls
    TyBuiltin{}          -> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty0
{-# INLINE typeSubtypes #-}

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

-- | Get all the direct child 'Type's of the given 'VarDecl'.
varDeclSubtypes :: Traversal' (VarDecl tyname name uni a) (Type tyname uni a)
varDeclSubtypes :: forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni 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 a
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl a
a name
n (Type tyname uni a -> VarDecl tyname name uni a)
-> f (Type tyname uni a) -> f (VarDecl tyname name uni 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
{-# INLINE varDeclSubtypes #-}

-- | Get all the direct constants of the given 'Term' from 'Constant's.
termConstants :: Traversal' (Term tyname name uni fun ann) (Some (ValueOf uni))
termConstants :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Some (ValueOf uni) -> f (Some (ValueOf uni)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termConstants Some (ValueOf uni) -> f (Some (ValueOf uni))
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    Constant ann
ann Some (ValueOf uni)
val -> ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant ann
ann (Some (ValueOf uni) -> Term tyname name uni fun ann)
-> f (Some (ValueOf uni)) -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Some (ValueOf uni) -> f (Some (ValueOf uni))
f Some (ValueOf uni)
val
    Var{}            -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}         -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}           -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0

-- | 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 :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}         -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}           -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}          -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}            -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}   -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}     -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 :: forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
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
Lens' tyname 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
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
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}          -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}            -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0

-- | Get all the direct child 'Kind's of the given 'Term'.
termSubkinds :: Traversal' (Term tyname name uni fun ann) (Kind ann)
termSubkinds :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constr{}        -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Case{}          -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
{-# INLINE termSubkinds #-}

-- | Get all the direct child 'Type's of the given 'Term'.
termSubtypes :: Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
termSubtypes :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
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 a b. f (a -> b) -> f a -> f b
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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
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
    Constr ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es  -> ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann (Type tyname uni ann
 -> Word64
 -> [Term tyname name uni fun ann]
 -> Term tyname name uni fun ann)
-> f (Type tyname uni ann)
-> f (Word64
      -> [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 (Word64
   -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann)
-> f Word64
-> f ([Term tyname name uni fun ann]
      -> Term tyname name uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> f Word64
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i 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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term tyname name uni fun ann]
es
    Case ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs  -> ann
-> Type tyname uni 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
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann (Type tyname uni ann
 -> Term tyname name uni fun 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] -> 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] -> 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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
arg 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 a b. f (a -> b) -> f a -> f b
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term tyname name uni fun ann]
cs
    TyAbs{}             -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
{-# INLINE termSubtypes #-}

-- | Get all the transitive child 'Constant's of the given 'Term'.
termConstantsDeep :: Fold (Term tyname name uni fun ann) (Some (ValueOf uni))
termConstantsDeep :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Some (ValueOf uni) -> f (Some (ValueOf uni)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termConstantsDeep = (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 (f :: * -> *).
(Contravariant f, Applicative f) =>
(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))
-> ((Some (ValueOf uni) -> f (Some (ValueOf uni)))
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (Some (ValueOf uni) -> f (Some (ValueOf uni)))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some (ValueOf uni) -> f (Some (ValueOf uni)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Some (ValueOf uni) -> f (Some (ValueOf uni)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termConstants

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

-- | 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 :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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 a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
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 a b. f (a -> b) -> f a -> f b
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
    Constr ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es  -> ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann Type tyname uni ann
ty Word64
i ([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))
-> [Term tyname name uni fun ann]
-> f [Term tyname name uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f [Term tyname name uni fun ann]
es
    Case ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs  -> ann
-> Type tyname uni 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
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann Type tyname uni ann
ty (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
arg 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 a b. f (a -> b) -> f a -> f b
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))
-> [Term tyname name uni fun ann]
-> f [Term tyname name uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
f [Term tyname name uni fun ann]
cs
    Error{}             -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall a. a -> f a
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 a. a -> f a
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 a. a -> f a
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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
{-# INLINE termSubterms #-}

-- | 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 :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(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 = LensLike'
  f (Term tyname name uni fun ann) (Term tyname name uni fun ann)
-> LensLike'
     f (Term tyname name uni fun ann) (Term tyname name uni fun ann)
forall (f :: * -> *) a.
(Applicative f, Contravariant f) =>
LensLike' f a a -> LensLike' f a a
cosmosOf LensLike'
  f (Term tyname name uni fun ann) (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(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

-- | Get all the transitive child 'Unique's of the given 'Type'.
typeUniquesDeep :: HasUniques (Type tyname uni ann) => Fold (Type tyname uni ann) Unique
typeUniquesDeep :: forall tyname (uni :: * -> *) ann.
HasUniques (Type tyname uni ann) =>
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 (f :: * -> *).
(Contravariant f, Applicative f) =>
(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))
-> ((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
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 :: forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
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 (f :: * -> *).
(Contravariant f, Applicative f) =>
(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))
-> ((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 (f :: * -> *).
Applicative f =>
(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))
 -> 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
Fold (Type tyname uni ann) Unique
typeUniquesDeep (forall {f :: * -> *}.
 (Contravariant f, Applicative f) =>
 (Unique -> f Unique)
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> (forall {f :: * -> *}.
    (Contravariant f, Applicative f) =>
    (Unique -> f Unique)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> forall {f :: * -> *}.
   (Contravariant f, Applicative f) =>
   (Unique -> f Unique)
   -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall s a. Fold s a -> Fold s a -> Fold s a
<^> (Unique -> f Unique)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
Traversal' (Term tyname name uni fun ann) Unique
Traversal' (Term tyname name uni fun ann) Unique
forall {f :: * -> *}.
(Contravariant f, Applicative f) =>
(Unique -> f Unique)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termUniques)