{-# 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 <^>
(<^>) :: 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
_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 })
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 bindingSubterms #-}
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 datatypeSubtypes #-}
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 bindingSubtypes #-}
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 datatypeSubkinds #-}
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 datatypeTyNames #-}
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
{-# INLINE bindingSubkinds #-}
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)
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
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 termSubkinds #-}
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
{-# INLINE termSubterms #-}
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
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
{-# INLINE termSubtypes #-}
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
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
{-# INLINE termBindings #-}
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
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
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
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)
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
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
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