-- editorconfig-checker-disable-file
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE LambdaCase    #-}
{-# LANGUAGE RankNTypes    #-}
module PlutusIR.Core.Plated
    ( termSubterms
    , termSubtermsDeep
    , termSubtypes
    , termSubtypesDeep
    , termSubkinds
    , termBindings
    , termVars
    , termConstants
    , termConstantsDeep
    , typeSubtypes
    , typeSubtypesDeep
    , typeSubkinds
    , typeUniques
    , typeUniquesDeep
    , datatypeSubtypes
    , datatypeSubkinds
    , datatypeTyNames
    , bindingSubterms
    , bindingSubtypes
    , bindingSubkinds
    , bindingNames
    , bindingTyNames
    , bindingIds
    , termUniques
    , termUniquesDeep
    , varDeclSubtypes
    , underBinders
    , _Constant
    ) where

import PlutusCore qualified as PLC
import PlutusCore.Arity
import PlutusCore.Core (tyVarDeclSubkinds, typeSubkinds, typeSubtypes, typeSubtypesDeep,
                        typeUniques, typeUniquesDeep, varDeclSubtypes)
import PlutusCore.Flat ()
import PlutusCore.Name.Unique qualified as PLC

import PlutusIR.Core.Type

import Control.Lens hiding (Strict, (<.>))
import Data.Functor.Apply
import Data.Functor.Bind.Class
import Universe

infixr 6 <^>

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

-- | View a term as a constant.
_Constant :: Prism' (Term tyname name uni fun a) (a, PLC.Some (PLC.ValueOf uni))
_Constant :: forall tyname name (uni :: * -> *) fun a (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (a, Some (ValueOf uni)) (f (a, Some (ValueOf uni)))
-> p (Term tyname name uni fun a) (f (Term tyname name uni fun a))
_Constant = ((a, Some (ValueOf uni)) -> Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Maybe (a, Some (ValueOf uni)))
-> Prism
     (Term tyname name uni fun a)
     (Term tyname name uni fun a)
     (a, Some (ValueOf uni))
     (a, Some (ValueOf uni))
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' ((a -> Some (ValueOf uni) -> Term tyname name uni fun a)
-> (a, Some (ValueOf uni)) -> Term tyname name uni fun a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Some (ValueOf uni) -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant) (\case { Constant a
a Some (ValueOf uni)
v -> (a, Some (ValueOf uni)) -> Maybe (a, Some (ValueOf uni))
forall a. a -> Maybe a
Just (a
a, Some (ValueOf uni)
v); Term tyname name uni fun a
_ -> Maybe (a, Some (ValueOf uni))
forall a. Maybe a
Nothing })

{-# INLINE bindingSubterms #-}
-- | Get all the direct child 'Term's of the given 'Binding'.
bindingSubterms :: Traversal' (Binding tyname name uni fun a) (Term tyname name uni fun a)
bindingSubterms :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms Term tyname name uni fun a -> f (Term tyname name uni fun a)
f = \case
    TermBind a
x Strictness
s VarDecl tyname name uni a
d Term tyname name uni fun a
t  -> a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s VarDecl tyname name uni a
d (Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    b :: Binding tyname name uni fun a
b@TypeBind {}     -> Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
b
    d :: Binding tyname name uni fun a
d@DatatypeBind {} -> Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
d

{-# INLINE datatypeSubtypes #-}
-- | Get all the direct child 'Type's of the given 'Datatype'.
datatypeSubtypes :: Traversal' (Datatype tyname name uni a) (Type tyname uni a)
datatypeSubtypes :: forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeSubtypes Type tyname uni a -> f (Type tyname uni a)
f (Datatype a
a TyVarDecl tyname a
n [TyVarDecl tyname a]
vs name
m [VarDecl tyname name uni a]
cs) = a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype a
a TyVarDecl tyname a
n [TyVarDecl tyname a]
vs name
m ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f [VarDecl tyname name uni a] -> f (Datatype tyname name uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> [VarDecl tyname name uni a] -> f [VarDecl tyname name uni a]
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 ((VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
 -> [VarDecl tyname name uni a] -> f [VarDecl tyname name uni a])
-> ((Type tyname uni a -> f (Type tyname uni a))
    -> VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> (Type tyname uni a -> f (Type tyname uni a))
-> [VarDecl tyname name uni a]
-> f [VarDecl tyname name uni a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni a -> f (Type tyname uni a))
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
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 tyname name uni a]
cs

{-# INLINE bindingSubtypes #-}
-- | Get all the direct child 'Type's of the given 'Binding'.
bindingSubtypes :: Traversal' (Binding tyname name uni fun a) (Type tyname uni a)
bindingSubtypes :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubtypes Type tyname uni a -> f (Type tyname uni a)
f = \case
    TermBind a
x Strictness
s VarDecl tyname name uni a
d Term tyname name uni fun a
t -> a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s (VarDecl tyname name uni a
 -> Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (VarDecl tyname name uni a)
-> f (Term tyname name uni fun a -> Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type tyname uni a -> f (Type tyname uni a))
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
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 tyname name uni a
d f (Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (Binding tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    DatatypeBind a
x Datatype tyname name uni a
d -> a -> Datatype tyname name uni a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind a
x (Datatype tyname name uni a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type tyname uni a -> f (Type tyname uni a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeSubtypes Type tyname uni a -> f (Type tyname uni a)
f Datatype tyname name uni a
d
    TypeBind a
a TyVarDecl tyname a
d Type tyname uni a
ty  -> a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a TyVarDecl tyname a
d (Type tyname uni a -> Binding tyname name uni fun a)
-> f (Type tyname uni a) -> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty

{-# INLINE datatypeSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Datatype'.
datatypeSubkinds :: Traversal' (Datatype tyname name uni a) (Kind a)
datatypeSubkinds :: forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Kind a -> f (Kind a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeSubkinds Kind a -> f (Kind a)
f (Datatype a
a TyVarDecl tyname a
n [TyVarDecl tyname a]
vs name
m [VarDecl tyname name uni a]
cs) = do
    TyVarDecl tyname a
n' <- (Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
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 tyname a
n
    [TyVarDecl tyname a]
vs' <- (TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> [TyVarDecl tyname a] -> f [TyVarDecl tyname a]
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 ((Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
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 tyname a]
vs
    pure $ a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype a
a TyVarDecl tyname a
n' [TyVarDecl tyname a]
vs' name
m [VarDecl tyname name uni a]
cs

{-# INLINE datatypeTyNames #-}
-- | Get all the type-names introduces by a datatype
datatypeTyNames :: Traversal' (Datatype tyname name uni a) tyname
datatypeTyNames :: forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeTyNames tyname -> f tyname
f (Datatype a
a2 TyVarDecl tyname a
tvdecl [TyVarDecl tyname a]
tvdecls name
n [VarDecl tyname name uni a]
vdecls) =
    a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype a
a2
        (TyVarDecl tyname a
 -> [TyVarDecl tyname a]
 -> name
 -> [VarDecl tyname name uni a]
 -> Datatype tyname name uni a)
-> f (TyVarDecl tyname a)
-> f ([TyVarDecl tyname a]
      -> name
      -> [VarDecl tyname name uni a]
      -> Datatype tyname name uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName tyname -> f tyname
f TyVarDecl tyname a
tvdecl
        f ([TyVarDecl tyname a]
   -> name
   -> [VarDecl tyname name uni a]
   -> Datatype tyname name uni a)
-> f [TyVarDecl tyname a]
-> f (name
      -> [VarDecl tyname name uni a] -> Datatype tyname name uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> [TyVarDecl tyname a] -> f [TyVarDecl tyname a]
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 ((tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName tyname -> f tyname
f) [TyVarDecl tyname a]
tvdecls
        f (name
   -> [VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f name
-> f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> name -> f name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure name
n
        f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f [VarDecl tyname name uni a] -> f (Datatype tyname name uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [VarDecl tyname name uni a] -> f [VarDecl tyname name uni a]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [VarDecl tyname name uni a]
vdecls

{-# INLINE bindingSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Binding'.
bindingSubkinds :: Traversal' (Binding tyname name uni fun a) (Kind a)
bindingSubkinds :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Kind a -> f (Kind a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubkinds Kind a -> f (Kind a)
f = \case
    t :: Binding tyname name uni fun a
t@TermBind {}    -> Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
t
    DatatypeBind a
x Datatype tyname name uni a
d -> a -> Datatype tyname name uni a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind a
x (Datatype tyname name uni a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind a -> f (Kind a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Kind a -> f (Kind a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeSubkinds Kind a -> f (Kind a)
f Datatype tyname name uni a
d
    TypeBind a
a TyVarDecl tyname a
d Type tyname uni a
ty  -> a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a (TyVarDecl tyname a
 -> Type tyname uni a -> Binding tyname name uni fun a)
-> f (TyVarDecl tyname a)
-> f (Type tyname uni a -> Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
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 tyname a
d f (Type tyname uni a -> Binding tyname name uni fun a)
-> f (Type tyname uni a) -> f (Binding tyname name uni fun a)
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 a -> f (Type tyname uni a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
ty

-- | All the identifiers/names introduced by this binding
-- In case of a datatype-binding it has multiple identifiers: the type, constructors, match function
bindingIds :: (PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)
            => Traversal1' (Binding tyname name uni fun a) PLC.Unique
bindingIds :: forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
Traversal1' (Binding tyname name uni fun a) Unique
bindingIds Unique -> f Unique
f = \case
   TermBind a
x Strictness
s VarDecl tyname name uni a
d Term tyname name uni fun a
t -> (VarDecl tyname name uni a
 -> Term tyname name uni fun a -> Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> VarDecl tyname name uni a
-> Binding tyname name uni fun a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s) Term tyname name uni fun a
t (VarDecl tyname name uni a -> Binding tyname name uni fun a)
-> f (VarDecl tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((name -> f name)
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
forall tyname name1 (uni :: * -> *) ann name2 (f :: * -> *).
Functor f =>
(name1 -> f name2)
-> VarDecl tyname name1 uni ann -> f (VarDecl tyname name2 uni ann)
PLC.varDeclName ((name -> f name)
 -> VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> ((Unique -> f Unique) -> name -> f name)
-> (Unique -> f Unique)
-> VarDecl tyname name uni a
-> f (VarDecl tyname name uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique) Unique -> f Unique
f VarDecl tyname name uni a
d
   TypeBind a
a TyVarDecl tyname a
d Type tyname uni a
ty -> (TyVarDecl tyname a
 -> Type tyname uni a -> Binding tyname name uni fun a)
-> Type tyname uni a
-> TyVarDecl tyname a
-> Binding tyname name uni fun a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a) Type tyname uni a
ty (TyVarDecl tyname a -> Binding tyname name uni fun a)
-> f (TyVarDecl tyname a) -> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName ((tyname -> f tyname)
 -> TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> ((Unique -> f Unique) -> tyname -> f tyname)
-> (Unique -> f Unique)
-> TyVarDecl tyname a
-> f (TyVarDecl tyname a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique) Unique -> f Unique
f TyVarDecl tyname a
d
   DatatypeBind a
a1 (Datatype a
a2 TyVarDecl tyname a
tvdecl [TyVarDecl tyname a]
tvdecls name
n [VarDecl tyname name uni a]
vdecls) ->
     a -> Datatype tyname name uni a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind a
a1 (Datatype tyname name uni a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       (a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype a
a2 (TyVarDecl tyname a
 -> [TyVarDecl tyname a]
 -> name
 -> [VarDecl tyname name uni a]
 -> Datatype tyname name uni a)
-> f (TyVarDecl tyname a)
-> f ([TyVarDecl tyname a]
      -> name
      -> [VarDecl tyname name uni a]
      -> Datatype tyname name uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName ((tyname -> f tyname)
 -> TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> ((Unique -> f Unique) -> tyname -> f tyname)
-> (Unique -> f Unique)
-> TyVarDecl tyname a
-> f (TyVarDecl tyname a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique) Unique -> f Unique
f TyVarDecl tyname a
tvdecl
                    f ([TyVarDecl tyname a]
   -> name
   -> [VarDecl tyname name uni a]
   -> Datatype tyname name uni a)
-> MaybeApply f [TyVarDecl tyname a]
-> f (name
      -> [VarDecl tyname name uni a] -> Datatype tyname name uni a)
forall (f :: * -> *) a b.
Apply f =>
f (a -> b) -> MaybeApply f a -> f b
<.*> (TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> [TyVarDecl tyname a] -> MaybeApply f [TyVarDecl tyname a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Apply f) =>
(a -> f b) -> t a -> MaybeApply f (t b)
traverse1Maybe (((tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName ((tyname -> f tyname)
 -> TyVarDecl tyname a -> f (TyVarDecl tyname a))
-> ((Unique -> f Unique) -> tyname -> f tyname)
-> (Unique -> f Unique)
-> TyVarDecl tyname a
-> f (TyVarDecl tyname a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique) -> tyname -> f tyname
forall name unique. HasUnique name unique => Lens' name Unique
Lens' tyname Unique
PLC.theUnique) Unique -> f Unique
f) [TyVarDecl tyname a]
tvdecls
                    f (name
   -> [VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f name
-> f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique Unique -> f Unique
f name
n
                    f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> MaybeApply f [VarDecl tyname name uni a]
-> f (Datatype tyname name uni a)
forall (f :: * -> *) a b.
Apply f =>
f (a -> b) -> MaybeApply f a -> f b
<.*> (VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> [VarDecl tyname name uni a]
-> MaybeApply f [VarDecl tyname name uni a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Apply f) =>
(a -> f b) -> t a -> MaybeApply f (t b)
traverse1Maybe (((name -> f name)
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
forall tyname name1 (uni :: * -> *) ann name2 (f :: * -> *).
Functor f =>
(name1 -> f name2)
-> VarDecl tyname name1 uni ann -> f (VarDecl tyname name2 uni ann)
PLC.varDeclName ((name -> f name)
 -> VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> ((Unique -> f Unique) -> name -> f name)
-> (Unique -> f Unique)
-> VarDecl tyname name uni a
-> f (VarDecl tyname name uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.theUnique) Unique -> f Unique
f) [VarDecl tyname name uni a]
vdecls)

-- | 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 a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
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
    Let{}            -> 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
    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

{-# INLINE termSubkinds #-}
-- | 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
    Let ann
x Recursivity
r NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
t    -> ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding 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
<$> ((Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> f (NonEmpty (Binding 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) -> NonEmpty a -> f (NonEmpty b)
traverse ((Binding tyname name uni fun ann
  -> f (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> f (NonEmpty (Binding tyname name uni fun ann)))
-> ((Kind ann -> f (Kind ann))
    -> Binding tyname name uni fun ann
    -> f (Binding tyname name uni fun ann))
-> (Kind ann -> f (Kind ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind ann -> f (Kind ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Kind a -> f (Kind a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubkinds) Kind ann -> f (Kind ann)
f NonEmpty (Binding tyname name uni fun ann)
bs 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
    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 a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 termSubterms #-}
-- | Get all the direct child 'Term's of the given 'Term', including those within 'Binding's.
termSubterms :: Traversal' (Term tyname name uni fun a) (Term tyname name uni fun a)
termSubterms :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> f (Term tyname name uni fun a)
f = \case
    Let a
x Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t      -> a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let a
x Recursivity
r (NonEmpty (Binding tyname name uni fun a)
 -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Binding tyname name uni fun a
 -> f (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
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) -> NonEmpty a -> f (NonEmpty b)
traverse ((Binding tyname name uni fun a
  -> f (Binding tyname name uni fun a))
 -> NonEmpty (Binding tyname name uni fun a)
 -> f (NonEmpty (Binding tyname name uni fun a)))
-> ((Term tyname name uni fun a -> f (Term tyname name uni fun a))
    -> Binding tyname name uni fun a
    -> f (Binding tyname name uni fun a))
-> (Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms) Term tyname name uni fun a -> f (Term tyname name uni fun a)
f NonEmpty (Binding tyname name uni fun a)
bs f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    TyAbs a
x tyname
tn Kind a
k Term tyname name uni fun a
t    -> a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs a
x tyname
tn Kind a
k (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    LamAbs a
x name
n Type tyname uni a
ty Term tyname name uni fun a
t   -> a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs a
x name
n Type tyname uni a
ty (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    Apply a
x Term tyname name uni fun a
t1 Term tyname name uni fun a
t2     -> a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply a
x (Term tyname name uni fun a
 -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t1 f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t2
    TyInst a
x Term tyname name uni fun a
t Type tyname uni a
ty     -> a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst a
x (Term tyname name uni fun a
 -> Type tyname uni a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (Type tyname uni a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t f (Type tyname uni a -> Term tyname name uni fun a)
-> f (Type tyname uni a) -> f (Term tyname name uni fun a)
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 a -> f (Type tyname uni a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
ty
    IWrap a
x Type tyname uni a
ty1 Type tyname uni a
ty2 Term tyname name uni fun a
t -> a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap a
x Type tyname uni a
ty1 Type tyname uni a
ty2 (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    Unwrap a
x Term tyname name uni fun a
t        -> a -> Term tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap a
x (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
    Constr a
x Type tyname uni a
ty Word64
i [Term tyname name uni fun a]
es  -> a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr a
x Type tyname uni a
ty Word64
i ([Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f [Term tyname name uni fun a] -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> [Term tyname name uni fun a] -> f [Term tyname name uni fun a]
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 a -> f (Term tyname name uni fun a)
f [Term tyname name uni fun a]
es
    Case a
x Type tyname uni a
ty Term tyname name uni fun a
arg [Term tyname name uni fun a]
cs  -> a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case a
x Type tyname uni a
ty (Term tyname name uni fun a
 -> [Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f ([Term tyname name uni fun a] -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
arg f ([Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f [Term tyname name uni fun a] -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a))
-> [Term tyname name uni fun a] -> f [Term tyname name uni fun a]
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 a -> f (Term tyname name uni fun a)
f [Term tyname name uni fun a]
cs
    e :: Term tyname name uni fun a
e@Error {}        -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
e
    v :: Term tyname name uni fun a
v@Var {}          -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
v
    c :: Term tyname name uni fun a
c@Constant {}     -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
c
    b :: Term tyname name uni fun a
b@Builtin {}      -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
b

-- | 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 a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms

{-# INLINE termSubtypes #-}
-- | Get all the direct child 'Type's of the given 'Term', including those within 'Binding's.
termSubtypes :: Traversal' (Term tyname name uni fun a) (Type tyname uni a)
termSubtypes :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubtypes Type tyname uni a -> f (Type tyname uni a)
f = \case
    Let a
x Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t      -> a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let a
x Recursivity
r (NonEmpty (Binding tyname name uni fun a)
 -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Binding tyname name uni fun a
 -> f (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
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) -> NonEmpty a -> f (NonEmpty b)
traverse ((Binding tyname name uni fun a
  -> f (Binding tyname name uni fun a))
 -> NonEmpty (Binding tyname name uni fun a)
 -> f (NonEmpty (Binding tyname name uni fun a)))
-> ((Type tyname uni a -> f (Type tyname uni a))
    -> Binding tyname name uni fun a
    -> f (Binding tyname name uni fun a))
-> (Type tyname uni a -> f (Type tyname uni a))
-> NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni a -> f (Type tyname uni a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubtypes) Type tyname uni a -> f (Type tyname uni a)
f NonEmpty (Binding tyname name uni fun a)
bs f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    LamAbs a
x name
n Type tyname uni a
ty Term tyname name uni fun a
t   -> a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs a
x name
n (Type tyname uni a
 -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Type tyname uni a)
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    TyInst a
x Term tyname name uni fun a
t Type tyname uni a
ty     -> a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst a
x Term tyname name uni fun a
t (Type tyname uni a -> Term tyname name uni fun a)
-> f (Type tyname uni a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty
    IWrap a
x Type tyname uni a
ty1 Type tyname uni a
ty2 Term tyname name uni fun a
t -> a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap a
x (Type tyname uni a
 -> Type tyname uni a
 -> Term tyname name uni fun a
 -> Term tyname name uni fun a)
-> f (Type tyname uni a)
-> f (Type tyname uni a
      -> Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty1 f (Type tyname uni a
   -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Type tyname uni a)
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
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 a -> f (Type tyname uni a)
f Type tyname uni a
ty2 f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    Error a
x Type tyname uni a
ty        -> a -> Type tyname uni a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error a
x (Type tyname uni a -> Term tyname name uni fun a)
-> f (Type tyname uni a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty
    Constr a
x Type tyname uni a
ty Word64
i [Term tyname name uni fun a]
es  -> a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr a
x (Type tyname uni a
 -> Word64
 -> [Term tyname name uni fun a]
 -> Term tyname name uni fun a)
-> f (Type tyname uni a)
-> f (Word64
      -> [Term tyname name uni fun a] -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty f (Word64
   -> [Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f Word64
-> f ([Term tyname name uni fun a] -> Term tyname name uni fun a)
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 a] -> Term tyname name uni fun a)
-> f [Term tyname name uni fun a] -> f (Term tyname name uni fun a)
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 a] -> f [Term tyname name uni fun a]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term tyname name uni fun a]
es
    Case a
x Type tyname uni a
ty Term tyname name uni fun a
arg [Term tyname name uni fun a]
cs  -> a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case a
x (Type tyname uni a
 -> Term tyname name uni fun a
 -> [Term tyname name uni fun a]
 -> Term tyname name uni fun a)
-> f (Type tyname uni a)
-> f (Term tyname name uni fun a
      -> [Term tyname name uni fun a] -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
ty f (Term tyname name uni fun a
   -> [Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f ([Term tyname name uni fun a] -> Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
arg f ([Term tyname name uni fun a] -> Term tyname name uni fun a)
-> f [Term tyname name uni fun a] -> f (Term tyname name uni fun a)
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 a] -> f [Term tyname name uni fun a]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term tyname name uni fun a]
cs
    t :: Term tyname name uni fun a
t@TyAbs {}        -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    a :: Term tyname name uni fun a
a@Apply {}        -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
a
    u :: Term tyname name uni fun a
u@Unwrap {}       -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
u
    v :: Term tyname name uni fun a
v@Var {}          -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
v
    c :: Term tyname name uni fun a
c@Constant {}     -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
c
    b :: Term tyname name uni fun a
b@Builtin {}      -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
b

-- | 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 a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
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

{-# INLINE termBindings #-}
-- | Get all the direct child 'Binding's of the given 'Term'.
termBindings :: Traversal' (Term tyname name uni fun a) (Binding tyname name uni fun a)
termBindings :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Binding tyname name uni fun a
 -> f (Binding tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termBindings Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
f = \case
    Let a
x Recursivity
r NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t -> a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let a
x Recursivity
r (NonEmpty (Binding tyname name uni fun a)
 -> Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
-> f (Term tyname name uni fun a -> Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding tyname name uni fun a
 -> f (Binding tyname name uni fun a))
-> NonEmpty (Binding tyname name uni fun a)
-> f (NonEmpty (Binding tyname name uni fun a))
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) -> NonEmpty a -> f (NonEmpty b)
traverse Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
f NonEmpty (Binding tyname name uni fun a)
bs f (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    Term tyname name uni fun a
t            -> Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t

-- | Get all the direct child 'Unique's of the given 'Term' (including the type-level ones).
termUniques
    :: PLC.HasUniques (Term tyname name uni fun ann)
    => Traversal' (Term tyname name uni fun ann) PLC.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 = \case
    Let ann
ann Recursivity
r NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
t    -> ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
ann Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding 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
<$> ATraversal
  (NonEmpty (Binding tyname name uni fun ann))
  (NonEmpty (Binding tyname name uni fun ann))
  Unique
  Unique
-> Traversal
     (NonEmpty (Binding tyname name uni fun ann))
     (NonEmpty (Binding tyname name uni fun ann))
     Unique
     Unique
forall s t a b. ATraversal s t a b -> Traversal s t a b
cloneTraversal ((Binding tyname name uni fun ann
 -> Bazaar (->) Unique Unique (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Bazaar
     (->) Unique Unique (NonEmpty (Binding tyname name uni fun ann))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
  Int
  (NonEmpty (Binding tyname name uni fun ann))
  (NonEmpty (Binding tyname name uni fun ann))
  (Binding tyname name uni fun ann)
  (Binding tyname name uni fun ann)
traversed((Binding tyname name uni fun ann
  -> Bazaar (->) Unique Unique (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> Bazaar
      (->) Unique Unique (NonEmpty (Binding tyname name uni fun ann)))
-> ((Unique -> Bazaar (->) Unique Unique Unique)
    -> Binding tyname name uni fun ann
    -> Bazaar (->) Unique Unique (Binding tyname name uni fun ann))
-> ATraversal
     (NonEmpty (Binding tyname name uni fun ann))
     (NonEmpty (Binding tyname name uni fun ann))
     Unique
     Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Unique -> Bazaar (->) Unique Unique Unique)
-> Binding tyname name uni fun ann
-> Bazaar (->) Unique Unique (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
(HasUnique tyname TypeUnique, HasUnique name TermUnique) =>
Traversal1' (Binding tyname name uni fun a) Unique
Traversal1' (Binding tyname name uni fun ann) Unique
bindingIds) Unique -> f Unique
f NonEmpty (Binding tyname name uni fun ann)
bs 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
    Var ann
ann name
n         -> (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique name unique => Lens' name Unique
Lens' name Unique
PLC.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 a.
a -> name -> Term tyname name uni fun a
Var ann
ann
    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
PLC.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 a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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
PLC.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 a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ann
ann name
n' Type tyname uni ann
ty Term tyname name uni fun ann
t
    a :: Term tyname name uni fun ann
a@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
a
    c :: Term tyname name uni fun ann
c@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
c
    b :: Term tyname name uni fun ann
b@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
b
    t :: Term tyname name uni fun ann
t@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
t
    e :: Term tyname name uni fun ann
e@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
e
    i :: Term tyname name uni fun ann
i@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
i
    u :: Term tyname name uni fun ann
u@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
u
    p :: Term tyname name uni fun ann
p@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
p
    p :: Term tyname name uni fun ann
p@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
p

-- | 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 a.
a -> name -> Term tyname name uni fun a
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
    Term tyname name uni fun ann
t         -> 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

-- | 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 'Unique's of the given 'Term' (including the type-level ones).
termUniquesDeep
    :: PLC.HasUniques (Term tyname name uni fun ann)
    => Fold (Term tyname name uni fun ann) PLC.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 a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
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)

-- | Get all the names introduces by a binding
bindingNames :: Traversal' (Binding tyname name uni fun a) name
bindingNames :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(name -> f name)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingNames name -> f name
f = \case
   TermBind a
x Strictness
s VarDecl tyname name uni a
d Term tyname name uni fun a
t -> a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s (VarDecl tyname name uni a
 -> Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (VarDecl tyname name uni a)
-> f (Term tyname name uni fun a -> Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (name -> f name)
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
forall tyname name1 (uni :: * -> *) ann name2 (f :: * -> *).
Functor f =>
(name1 -> f name2)
-> VarDecl tyname name1 uni ann -> f (VarDecl tyname name2 uni ann)
PLC.varDeclName name -> f name
f VarDecl tyname name uni a
d f (Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Term tyname name uni fun a)
-> f (Binding tyname name uni fun a)
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 a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
   DatatypeBind a
a1 (Datatype a
a2 TyVarDecl tyname a
tvdecl [TyVarDecl tyname a]
tvdecls name
n [VarDecl tyname name uni a]
vdecls) ->
     a -> Datatype tyname name uni a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind a
a1 (Datatype tyname name uni a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       (a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype a
a2 TyVarDecl tyname a
tvdecl [TyVarDecl tyname a]
tvdecls
                    (name -> [VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f name
-> f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> f name
f name
n
                    f ([VarDecl tyname name uni a] -> Datatype tyname name uni a)
-> f [VarDecl tyname name uni a] -> f (Datatype tyname name uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (VarDecl tyname name uni a -> f (VarDecl tyname name uni a))
-> [VarDecl tyname name uni a] -> f [VarDecl tyname name uni a]
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 ((name -> f name)
-> VarDecl tyname name uni a -> f (VarDecl tyname name uni a)
forall tyname name1 (uni :: * -> *) ann name2 (f :: * -> *).
Functor f =>
(name1 -> f name2)
-> VarDecl tyname name1 uni ann -> f (VarDecl tyname name2 uni ann)
PLC.varDeclName name -> f name
f) [VarDecl tyname name uni a]
vdecls)
   b :: Binding tyname name uni fun a
b@TypeBind{} -> Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
b

-- | Get all the type-names introduces by a binding
bindingTyNames :: Traversal' (Binding tyname name uni fun a) tyname
bindingTyNames :: forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingTyNames tyname -> f tyname
f = \case
   TypeBind a
a TyVarDecl tyname a
d Type tyname uni a
ty   -> a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
a (TyVarDecl tyname a
 -> Type tyname uni a -> Binding tyname name uni fun a)
-> f (TyVarDecl tyname a)
-> f (Type tyname uni a -> Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName tyname -> f tyname
f TyVarDecl tyname a
d f (Type tyname uni a -> Binding tyname name uni fun a)
-> f (Type tyname uni a) -> f (Binding tyname name uni fun a)
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 a -> f (Type tyname uni a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
ty
   DatatypeBind a
a1 Datatype tyname name uni a
d -> a -> Datatype tyname name uni a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind a
a1 (Datatype tyname name uni a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni a)
-> f (Binding tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (tyname -> f tyname)
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeTyNames tyname -> f tyname
f Datatype tyname name uni a
d
   b :: Binding tyname name uni fun a
b@TermBind{}      -> Binding tyname name uni fun a -> f (Binding tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
b

-- | Focus on the term under the binders corresponding to the given arity.
-- e.g. for arity @[TermParam, TermParam]@ and term @\x y -> t@ it focusses on @t@.
underBinders :: Arity -> Traversal' (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders :: forall tyname name (uni :: * -> *) fun a.
Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders [] Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t                                = Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
underBinders (Param
TermParam:Arity
arity) Term tyname name uni fun a -> f (Term tyname name uni fun a)
f (LamAbs a
a name
n Type tyname uni a
ty Term tyname name uni fun a
t) = a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs a
a name
n Type tyname uni a
ty (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders Arity
arity Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
underBinders (Param
TypeParam:Arity
arity) Term tyname name uni fun a -> f (Term tyname name uni fun a)
f (TyAbs a
a tyname
ty Kind a
k Term tyname name uni fun a
t)  = a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs a
a tyname
ty Kind a
k (Term tyname name uni fun a -> Term tyname name uni fun a)
-> f (Term tyname name uni fun a) -> f (Term tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Arity
-> Traversal'
     (Term tyname name uni fun a) (Term tyname name uni fun a)
underBinders Arity
arity Term tyname name uni fun a -> f (Term tyname name uni fun a)
f Term tyname name uni fun a
t
underBinders Arity
_ Term tyname name uni fun a -> f (Term tyname name uni fun a)
_ Term tyname name uni fun a
t                                 = Term tyname name uni fun a -> f (Term tyname name uni fun a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t