{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE LambdaCase    #-}
{-# LANGUAGE RankNTypes    #-}
module PlutusIR.Core.Plated
    ( termSubterms
    , termSubtermsDeep
    , termSubtypes
    , termSubtypesDeep
    , termSubkinds
    , termBindings
    , typeSubtypes
    , typeSubtypesDeep
    , typeSubkinds
    , typeUniques
    , typeUniquesDeep
    , datatypeSubtypes
    , datatypeSubkinds
    , bindingSubterms
    , bindingSubtypes
    , bindingSubkinds
    , bindingNames
    , bindingTyNames
    , bindingIds
    , termUniques
    , termUniquesDeep
    ) where

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

import PlutusIR.Core.Type

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

infixr 6 <^>

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

{-# 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 :: (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 fun a
d Term tyname name uni fun a
t  -> a
-> Strictness
-> VarDecl tyname name uni fun 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 fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s VarDecl tyname name uni fun 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 (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 (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 fun a) (Type tyname uni a)
datatypeSubtypes :: (Type tyname uni a -> f (Type tyname uni a))
-> Datatype tyname name uni fun a
-> f (Datatype tyname name uni fun 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 fun a]
cs) = a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype a
a TyVarDecl tyname a
n [TyVarDecl tyname a]
vs name
m ([VarDecl tyname name uni fun a] -> Datatype tyname name uni fun a)
-> f [VarDecl tyname name uni fun a]
-> f (Datatype tyname name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((VarDecl tyname name uni fun a
 -> f (VarDecl tyname name uni fun a))
-> [VarDecl tyname name uni fun a]
-> f [VarDecl tyname name uni fun a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((VarDecl tyname name uni fun a
  -> f (VarDecl tyname name uni fun a))
 -> [VarDecl tyname name uni fun a]
 -> f [VarDecl tyname name uni fun a])
-> ((Type tyname uni a -> f (Type tyname uni a))
    -> VarDecl tyname name uni fun a
    -> f (VarDecl tyname name uni fun a))
-> (Type tyname uni a -> f (Type tyname uni a))
-> [VarDecl tyname name uni fun a]
-> f [VarDecl tyname name uni fun a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni a -> f (Type tyname uni a))
-> VarDecl tyname name uni fun a
-> f (VarDecl tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (VarDecl tyname name uni fun a) (Type tyname uni a)
varDeclSubtypes) Type tyname uni a -> f (Type tyname uni a)
f [VarDecl tyname name uni fun 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 :: (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 fun a
d Term tyname name uni fun a
t -> a
-> Strictness
-> VarDecl tyname name uni fun 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 fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind a
x Strictness
s (VarDecl tyname name uni fun a
 -> Term tyname name uni fun a -> Binding tyname name uni fun a)
-> f (VarDecl tyname name uni fun 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 fun a
-> f (VarDecl tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (VarDecl tyname name uni fun a) (Type tyname uni a)
varDeclSubtypes Type tyname uni a -> f (Type tyname uni a)
f VarDecl tyname name uni fun 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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t
    DatatypeBind a
x Datatype tyname name uni fun a
d -> a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind a
x (Datatype tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni fun 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 fun a
-> f (Datatype tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Datatype tyname name uni fun a) (Type tyname uni a)
datatypeSubtypes Type tyname uni a -> f (Type tyname uni a)
f Datatype tyname name uni fun 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 fun a) (Kind a)
datatypeSubkinds :: (Kind a -> f (Kind a))
-> Datatype tyname name uni fun a
-> f (Datatype tyname name uni fun 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 fun a]
cs) = do
    TyVarDecl tyname a
n' <- (Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname a. Traversal' (TyVarDecl tyname a) (Kind 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)
traverse ((Kind a -> f (Kind a))
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname a. Traversal' (TyVarDecl tyname a) (Kind 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 fun a]
-> Datatype tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype a
a TyVarDecl tyname a
n' [TyVarDecl tyname a]
vs' name
m [VarDecl tyname name uni fun a]
cs

{-# INLINE bindingSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Binding'.
bindingSubkinds :: Traversal' (Binding tyname name uni fun a) (Kind a)
bindingSubkinds :: (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 (f :: * -> *) a. Applicative f => a -> f a
pure Binding tyname name uni fun a
t
    DatatypeBind a
x Datatype tyname name uni fun a
d -> a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind a
x (Datatype tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni fun 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 fun a
-> f (Datatype tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Datatype tyname name uni fun a) (Kind a)
datatypeSubkinds Kind a -> f (Kind a)
f Datatype tyname name uni fun 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. Traversal' (TyVarDecl tyname a) (Kind 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni a -> f (Type tyname uni 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 :: Traversal1' (Binding tyname name uni fun a) Unique
bindingIds Unique -> f Unique
f = \case
   TermBind a
x Strictness
s VarDecl tyname name uni fun a
d Term tyname name uni fun a
t -> (VarDecl tyname name uni fun a
 -> Term tyname name uni fun a -> Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> VarDecl tyname name uni fun a
-> Binding tyname name uni fun a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a
-> Strictness
-> VarDecl tyname name uni fun 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 fun 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 fun a -> Binding tyname name uni fun a)
-> f (VarDecl tyname name uni fun 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 fun a
-> f (VarDecl tyname name uni fun a)
forall tyname name1 (uni :: * -> *) k1 (fun1 :: k1) ann name2 k2
       (fun2 :: k2).
Lens
  (VarDecl tyname name1 uni fun1 ann)
  (VarDecl tyname name2 uni fun2 ann)
  name1
  name2
PLC.varDeclName ((name -> f name)
 -> VarDecl tyname name uni fun a
 -> f (VarDecl tyname name uni fun a))
-> ((Unique -> f Unique) -> name -> f name)
-> (Unique -> f Unique)
-> VarDecl tyname name uni fun a
-> f (VarDecl tyname name uni fun 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
PLC.theUnique) Unique -> f Unique
f VarDecl tyname name uni fun 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.
Lens
  (TyVarDecl tyname1 ann) (TyVarDecl tyname2 ann) tyname1 tyname2
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
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 fun a]
vdecls) ->
     a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind a
a1 (Datatype tyname name uni fun a -> Binding tyname name uni fun a)
-> f (Datatype tyname name uni fun 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 fun a]
-> Datatype tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype a
a2 (TyVarDecl tyname a
 -> [TyVarDecl tyname a]
 -> name
 -> [VarDecl tyname name uni fun a]
 -> Datatype tyname name uni fun a)
-> f (TyVarDecl tyname a)
-> f ([TyVarDecl tyname a]
      -> name
      -> [VarDecl tyname name uni fun a]
      -> Datatype 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.
Lens
  (TyVarDecl tyname1 ann) (TyVarDecl tyname2 ann) tyname1 tyname2
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
PLC.theUnique) Unique -> f Unique
f TyVarDecl tyname a
tvdecl
                    f ([TyVarDecl tyname a]
   -> name
   -> [VarDecl tyname name uni fun a]
   -> Datatype tyname name uni fun a)
-> MaybeApply f [TyVarDecl tyname a]
-> f (name
      -> [VarDecl tyname name uni fun a]
      -> Datatype tyname name uni fun 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 (f :: * -> *) (t :: * -> *) a b.
(Apply f, Traversable t) =>
(a -> f b) -> t a -> MaybeApply f (t b)
traverse1Maybe (((tyname -> f tyname)
-> TyVarDecl tyname a -> f (TyVarDecl tyname a)
forall tyname1 ann tyname2.
Lens
  (TyVarDecl tyname1 ann) (TyVarDecl tyname2 ann) tyname1 tyname2
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
PLC.theUnique) Unique -> f Unique
f) [TyVarDecl tyname a]
tvdecls
                    f (name
   -> [VarDecl tyname name uni fun a]
   -> Datatype tyname name uni fun a)
-> f name
-> f ([VarDecl tyname name uni fun a]
      -> Datatype tyname name uni fun a)
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
PLC.theUnique Unique -> f Unique
f name
n
                    f ([VarDecl tyname name uni fun a]
   -> Datatype tyname name uni fun a)
-> MaybeApply f [VarDecl tyname name uni fun a]
-> f (Datatype tyname name uni fun a)
forall (f :: * -> *) a b.
Apply f =>
f (a -> b) -> MaybeApply f a -> f b
<.*> (VarDecl tyname name uni fun a
 -> f (VarDecl tyname name uni fun a))
-> [VarDecl tyname name uni fun a]
-> MaybeApply f [VarDecl tyname name uni fun a]
forall (f :: * -> *) (t :: * -> *) a b.
(Apply f, Traversable t) =>
(a -> f b) -> t a -> MaybeApply f (t b)
traverse1Maybe (((name -> f name)
-> VarDecl tyname name uni fun a
-> f (VarDecl tyname name uni fun a)
forall tyname name1 (uni :: * -> *) k1 (fun1 :: k1) ann name2 k2
       (fun2 :: k2).
Lens
  (VarDecl tyname name1 uni fun1 ann)
  (VarDecl tyname name2 uni fun2 ann)
  name1
  name2
PLC.varDeclName ((name -> f name)
 -> VarDecl tyname name uni fun a
 -> f (VarDecl tyname name uni fun a))
-> ((Unique -> f Unique) -> name -> f name)
-> (Unique -> f Unique)
-> VarDecl tyname name uni fun a
-> f (VarDecl tyname name uni fun 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
PLC.theUnique) Unique -> f Unique
f) [VarDecl tyname name uni fun a]
vdecls)
  where
    -- | Traverse using 'Apply', but getting back the result in 'MaybeApply f' instead of in 'f'.
    traverse1Maybe :: (Apply f, Traversable t) => (a -> f b) -> t a -> MaybeApply f (t b)
    traverse1Maybe :: (a -> f b) -> t a -> MaybeApply f (t b)
traverse1Maybe a -> f b
f' = (a -> MaybeApply f b) -> t a -> MaybeApply f (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Either (f b) b -> MaybeApply f b
forall (f :: * -> *) a. Either (f a) a -> MaybeApply f a
MaybeApply (Either (f b) b -> MaybeApply f b)
-> (a -> Either (f b) b) -> a -> MaybeApply f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f b -> Either (f b) b
forall a b. a -> Either a b
Left (f b -> Either (f b) b) -> (a -> f b) -> a -> Either (f b) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f')

    -- | Apply a non-empty container of functions to a possibly-empty-with-unit container of values.
    -- Taken from: <https://github.com/ekmett/semigroupoids/issues/66#issue-271899630>
    (<.*>) :: (Apply f) => f (a -> b) -> MaybeApply f a -> f b
    f (a -> b)
ff <.*> :: f (a -> b) -> MaybeApply f a -> f b
<.*> MaybeApply (Left f a
fa) = f (a -> b)
ff f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> f a
fa
    f (a -> b)
ff <.*> MaybeApply (Right a
a) = ((a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a
a) ((a -> b) -> b) -> f (a -> b) -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (a -> b)
ff
    infixl 4 <.*>


{-# INLINE termSubkinds #-}
-- | Get all the direct child 'Kind's of the given 'Term'.
termSubkinds :: Traversal' (Term tyname name uni fun ann) (Kind ann)
termSubkinds :: (Kind ann -> f (Kind ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubkinds Kind ann -> f (Kind ann)
f Term tyname name uni fun ann
term0 = case Term tyname name uni fun ann
term0 of
    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)
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.
Traversal' (Binding tyname name uni fun a) (Kind 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
t
    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 (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Var{}           -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    TyInst{}        -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    IWrap{}         -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Error{}         -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Apply{}         -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Unwrap{}        -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Constant{}      -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0
    Builtin{}       -> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
term0

{-# INLINE 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 :: (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)
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.
Traversal'
  (Binding tyname name uni fun a) (Term 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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni a -> f (Type tyname uni 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
    e :: Term tyname name uni fun a
e@Error {}        -> Term tyname name uni fun a -> f (Term tyname name uni fun 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 (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 (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 (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 :: (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtermsDeep = ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a.
(Applicative f, Contravariant f) =>
LensLike' f a a -> LensLike' f a a
cosmosOf (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Term tyname name uni fun a) (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 :: (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)
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.
Traversal' (Binding tyname name uni fun a) (Type tyname uni 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 (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 (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 (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 (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 (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 (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 (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
    t :: Term tyname name uni fun a
t@TyAbs {}        -> Term tyname name uni fun a -> f (Term tyname name uni fun 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 (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 (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 (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 (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 (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 :: (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypesDeep = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Fold (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubtermsDeep ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Type tyname uni ann -> f (Type tyname uni ann))
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Term tyname name uni fun a) (Type tyname uni 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.
Fold (Type tyname uni ann) (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 :: (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)
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 (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 (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 (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 :: 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
-> (Unique -> f Unique)
-> NonEmpty (Binding tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
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
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
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
t
    Var ann
ann name
n         -> (Unique -> f Unique) -> name -> f name
forall name unique. HasUnique 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
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
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 (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 (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 (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 (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 (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun ann
u

-- | 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 :: Fold (Term tyname name uni fun ann) Unique
termUniquesDeep = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann.
Fold (Term tyname name uni fun ann) (Term tyname name uni fun ann)
termSubtermsDeep ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((Unique -> f Unique)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (Unique -> f Unique)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a.
Traversal' (Term tyname name uni fun a) (Type tyname uni 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
typeUniquesDeep Fold (Term tyname name uni fun ann) Unique
-> Fold (Term tyname name uni fun ann) Unique
-> Fold (Term tyname name uni fun ann) Unique
forall s a. Fold s a -> Fold s a -> Fold s a
<^> forall tyname name (uni :: * -> *) fun ann.
HasUniques (Term tyname name uni fun ann) =>
Traversal' (Term tyname name uni fun ann) Unique
Fold (Term tyname name uni fun ann) Unique
termUniques)

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