-- 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)