{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module PlutusIR.Subst (
fvTerm,
ftvTerm,
fvBinding,
ftvBinding,
ftvTy,
vTerm,
tvTerm,
tvTy,
) where
import PlutusCore.Core (typeTyVars)
import PlutusCore.Core qualified as PLC
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Name.UniqueSet qualified as USet
import PlutusCore.Subst (ftvTy, ftvTyCtx, tvTy)
import PlutusIR.Core
import Control.Lens
import Control.Lens.Unsound qualified as Unsound
import Data.Traversable (mapAccumL)
import PlutusCore.Name.Unique (HasUnique, TermUnique, TypeUnique)
import PlutusCore.Name.UniqueSet (UniqueSet)
fvTerm :: (HasUnique name TermUnique) => Traversal' (Term tyname name uni fun ann) name
fvTerm :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Traversal' (Term tyname name uni fun ann) name
fvTerm = UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
forall a. Monoid a => a
mempty
fvTermCtx
:: forall tyname name uni fun ann .
(HasUnique name TermUnique) =>
UniqueSet TermUnique ->
Traversal' (Term tyname name uni fun ann) name
fvTermCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound name -> f name
f = \case
Let ann
a r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
let fvLinearScope :: UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
fvLinearScope UniqueSet TermUnique
boundSoFar Binding tyname name uni fun ann
b =
(UniqueSet TermUnique
boundSoFar UniqueSet TermUnique
-> UniqueSet TermUnique -> UniqueSet TermUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
(UniqueSet TermUnique) (Binding tyname name uni fun ann) name
-> Binding tyname name uni fun ann -> UniqueSet TermUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting
(UniqueSet TermUnique) (Binding tyname name uni fun ann) name
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 Binding tyname name uni fun ann
b, UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
boundSoFar name -> f name
f Binding tyname name uni fun ann
b)
(UniqueSet TermUnique
boundAtTheEnd, NonEmpty (f (Binding tyname name uni fun ann))
bs') = (UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann)))
-> UniqueSet TermUnique
-> NonEmpty (Binding tyname name uni fun ann)
-> (UniqueSet TermUnique,
NonEmpty (f (Binding tyname name uni fun ann)))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
forall {tyname} {uni :: * -> *} {fun} {ann}.
UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
fvLinearScope UniqueSet TermUnique
bound NonEmpty (Binding tyname name uni fun ann)
bs
in 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
a 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
<$> NonEmpty (f (Binding tyname name uni fun ann))
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
NonEmpty (f a) -> f (NonEmpty a)
sequenceA NonEmpty (f (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
<*> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
boundAtTheEnd name -> f name
f Term tyname name uni fun ann
tIn
Let ann
a r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
let bound' :: UniqueSet TermUnique
bound' = UniqueSet TermUnique
bound UniqueSet TermUnique
-> UniqueSet TermUnique -> UniqueSet TermUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
(UniqueSet TermUnique)
(NonEmpty (Binding tyname name uni fun ann))
name
-> NonEmpty (Binding tyname name uni fun ann)
-> UniqueSet TermUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((Binding tyname name uni fun ann
-> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
(UniqueSet TermUnique) (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
-> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
(UniqueSet TermUnique)
(NonEmpty (Binding tyname name uni fun ann)))
-> ((name -> Const (UniqueSet TermUnique) name)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
-> Getting
(UniqueSet TermUnique)
(NonEmpty (Binding tyname name uni fun ann))
name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> Const (UniqueSet TermUnique) name)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann)
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) NonEmpty (Binding tyname name uni fun ann)
bs
in 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
a 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 (UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
bound name -> f name
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
<*> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound' name -> f name
f Term tyname name uni fun ann
tIn
Var ann
a 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
a (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
<$> (if name -> UniqueSet TermUnique -> Bool
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> Bool
USet.memberByName name
n UniqueSet TermUnique
bound then name -> f name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure name
n else name -> f name
f name
n)
LamAbs ann
a name
n Type tyname uni ann
ty Term tyname name uni fun ann
t -> ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ann
a name
n Type tyname uni ann
ty (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx (name -> UniqueSet TermUnique -> UniqueSet TermUnique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName name
n UniqueSet TermUnique
bound) name -> f name
f Term tyname name uni fun ann
t
Term tyname name uni fun ann
t -> ((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 (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 ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> ((name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound) name -> f name
f Term tyname name uni fun ann
t
ftvTerm :: (HasUnique tyname TypeUnique) => Traversal' (Term tyname name uni fun ann) tyname
ftvTerm :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Traversal' (Term tyname name uni fun ann) tyname
ftvTerm = UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
forall a. Monoid a => a
mempty
ftvTermCtx ::
(HasUnique tyname TypeUnique) =>
UniqueSet TypeUnique ->
Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound tyname -> f tyname
f = \case
Let ann
a r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
let ftvLinearScope :: UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
ftvLinearScope UniqueSet TypeUnique
bound' Binding tyname name uni fun ann
b =
(UniqueSet TypeUnique
bound' UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
(UniqueSet TypeUnique) (Binding tyname name uni fun ann) tyname
-> Binding tyname name uni fun ann -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting
(UniqueSet TypeUnique) (Binding tyname name uni fun ann) tyname
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 Binding tyname name uni fun ann
b, Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound' tyname -> f tyname
f Binding tyname name uni fun ann
b)
(UniqueSet TypeUnique
bound'', NonEmpty (f (Binding tyname name uni fun ann))
bs') = (UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann)))
-> UniqueSet TypeUnique
-> NonEmpty (Binding tyname name uni fun ann)
-> (UniqueSet TypeUnique,
NonEmpty (f (Binding tyname name uni fun ann)))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
forall {name} {uni :: * -> *} {fun} {ann}.
UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
ftvLinearScope UniqueSet TypeUnique
bound NonEmpty (Binding tyname name uni fun ann)
bs
in 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
a 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
<$> NonEmpty (f (Binding tyname name uni fun ann))
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
NonEmpty (f a) -> f (NonEmpty a)
sequenceA NonEmpty (f (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
<*> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound'' tyname -> f tyname
f Term tyname name uni fun ann
tIn
Let ann
a r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
let bound' :: UniqueSet TypeUnique
bound' = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
(UniqueSet TypeUnique)
(NonEmpty (Binding tyname name uni fun ann))
tyname
-> NonEmpty (Binding tyname name uni fun ann)
-> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((Binding tyname name uni fun ann
-> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
(UniqueSet TypeUnique) (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
-> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
(UniqueSet TypeUnique)
(NonEmpty (Binding tyname name uni fun ann)))
-> ((tyname -> Const (UniqueSet TypeUnique) tyname)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
-> Getting
(UniqueSet TypeUnique)
(NonEmpty (Binding tyname name uni fun ann))
tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> Const (UniqueSet TypeUnique) tyname)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann)
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) NonEmpty (Binding tyname name uni fun ann)
bs
in 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
a 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 (Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
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
<*> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound' tyname -> f tyname
f Term tyname name uni fun ann
tIn
TyAbs ann
a tyname
tn Kind ann
k Term tyname name uni fun ann
t -> ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs ann
a tyname
tn Kind ann
k (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx (tyname -> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName tyname
tn UniqueSet TypeUnique
bound) tyname -> f tyname
f Term tyname name uni fun ann
t
Term tyname name uni fun ann
t -> (((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 (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 ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> ((tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound) Traversal' (Term tyname name uni fun ann) tyname
-> Traversal' (Term tyname name uni fun ann) tyname
-> Traversal' (Term tyname name uni fun ann) tyname
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin` ((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))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
bound)) tyname -> f tyname
f Term tyname name uni fun ann
t
fvBinding :: (HasUnique name TermUnique) => Traversal' (Binding tyname name uni fun ann) name
fvBinding :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Traversal' (Binding tyname name uni fun ann) name
fvBinding = UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
forall a. Monoid a => a
mempty
fvBindingCtx ::
(HasUnique name TermUnique) =>
UniqueSet TermUnique ->
Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
bound = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding 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))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann))
-> ((name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound
ftvBinding ::
(HasUnique tyname TypeUnique) =>
Recursivity ->
Traversal' (Binding tyname name uni fun ann) tyname
ftvBinding :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity -> Traversal' (Binding tyname name uni fun ann) tyname
ftvBinding Recursivity
r = Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
forall a. Monoid a => a
mempty
ftvBindingCtx ::
(HasUnique tyname TypeUnique) =>
Recursivity ->
UniqueSet TypeUnique ->
Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f = \case
DatatypeBind ann
a Datatype tyname name uni ann
d -> ann
-> Datatype tyname name uni ann -> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind ann
a (Datatype tyname name uni ann -> Binding tyname name uni fun ann)
-> f (Datatype tyname name uni ann)
-> f (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
forall tyname name (uni :: * -> *) ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f Datatype tyname name uni ann
d
Binding tyname name uni fun ann
b ->
( ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding 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))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann))
-> ((tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> (tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound)
(forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann))
-> (forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann))
-> forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin` ((Type tyname uni ann -> f (Type tyname uni ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
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 ann -> f (Type tyname uni ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
bound)
)
tyname -> f tyname
f
Binding tyname name uni fun ann
b
ftvDatatypeCtx ::
(HasUnique tyname TypeUnique) =>
Recursivity ->
UniqueSet TypeUnique ->
Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx :: forall tyname name (uni :: * -> *) ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f d :: Datatype tyname name uni ann
d@(Datatype ann
a TyVarDecl tyname ann
tyconstr [TyVarDecl tyname ann]
tyvars name
destr [VarDecl tyname name uni ann]
constrs) =
let
tyConstr :: UniqueSet TypeUnique
tyConstr = Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
-> TyVarDecl tyname ann -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName TyVarDecl tyname ann
tyconstr
tyVars :: UniqueSet TypeUnique
tyVars = Getting (UniqueSet TypeUnique) [TyVarDecl tyname ann] tyname
-> [TyVarDecl tyname ann] -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((TyVarDecl tyname ann
-> Const (UniqueSet TypeUnique) (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> Const (UniqueSet TypeUnique) [TyVarDecl tyname ann]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
[TyVarDecl tyname ann]
[TyVarDecl tyname ann]
(TyVarDecl tyname ann)
(TyVarDecl tyname ann)
traversed ((TyVarDecl tyname ann
-> Const (UniqueSet TypeUnique) (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> Const (UniqueSet TypeUnique) [TyVarDecl tyname ann])
-> Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
-> Getting (UniqueSet TypeUnique) [TyVarDecl tyname ann] tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName) [TyVarDecl tyname ann]
tyvars
allBound :: UniqueSet TypeUnique
allBound = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyConstr UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyVars
varsBound :: UniqueSet TypeUnique
varsBound = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyVars
in
case Recursivity
r of
Recursivity
Rec -> ((Type tyname uni ann -> f (Type tyname uni ann))
-> Datatype tyname name uni ann -> f (Datatype tyname name uni ann)
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 ann -> f (Type tyname uni ann))
-> Datatype tyname name uni ann
-> f (Datatype tyname name uni ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Datatype tyname name uni ann
-> f (Datatype tyname name uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
allBound) tyname -> f tyname
f Datatype tyname name uni ann
d
Recursivity
NonRec ->
let
combinedTraversal :: (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
combinedTraversal =
((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs ((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a))
-> ((tyname -> f tyname)
-> Type tyname uni a -> f (Type tyname uni a))
-> (tyname -> f tyname)
-> Type tyname uni a
-> f (Type tyname uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
varsBound)
(forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a))
-> (forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a))
-> forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin`
((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes ((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a))
-> ((tyname -> f tyname)
-> Type tyname uni a -> f (Type tyname uni a))
-> (tyname -> f tyname)
-> Type tyname uni a
-> f (Type tyname uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> forall {f :: * -> *}.
Applicative f =>
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
allBound)
constrs' :: f [VarDecl tyname name uni ann]
constrs' = LensLike
f
[VarDecl tyname name uni ann]
[VarDecl tyname name uni ann]
tyname
tyname
-> LensLike
f
[VarDecl tyname name uni ann]
[VarDecl tyname name uni ann]
tyname
tyname
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf ((VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> [VarDecl tyname name uni ann] -> f [VarDecl tyname name uni ann]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
Int
[VarDecl tyname name uni ann]
[VarDecl tyname name uni ann]
(VarDecl tyname name uni ann)
(VarDecl tyname name uni ann)
traversed ((VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> [VarDecl tyname name uni ann]
-> f [VarDecl tyname name uni ann])
-> ((tyname -> f tyname)
-> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> LensLike
f
[VarDecl tyname name uni ann]
[VarDecl tyname name uni ann]
tyname
tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> f (Type tyname uni ann))
-> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann)
forall tyname1 name (uni1 :: * -> *) ann tyname2 (uni2 :: * -> *)
(f :: * -> *).
Functor f =>
(Type tyname1 uni1 ann -> f (Type tyname2 uni2 ann))
-> VarDecl tyname1 name uni1 ann
-> f (VarDecl tyname2 name uni2 ann)
PLC.varDeclType ((Type tyname uni ann -> f (Type tyname uni ann))
-> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> VarDecl tyname name uni ann
-> f (VarDecl tyname name uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall {uni :: * -> *} {a}.
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
combinedTraversal) tyname -> f tyname
f [VarDecl tyname name uni ann]
constrs
in
ann
-> TyVarDecl tyname ann
-> [TyVarDecl tyname ann]
-> name
-> [VarDecl tyname name uni ann]
-> Datatype tyname name uni ann
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype ann
a TyVarDecl tyname ann
tyconstr [TyVarDecl tyname ann]
tyvars name
destr ([VarDecl tyname name uni ann] -> Datatype tyname name uni ann)
-> f [VarDecl tyname name uni ann]
-> f (Datatype tyname name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [VarDecl tyname name uni ann]
constrs'
funArgs :: Traversal' (Type tyname uni a) (Type tyname uni a)
funArgs :: forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs Type tyname uni a -> f (Type tyname uni a)
f = \case
TyFun a
a Type tyname uni a
dom cod :: Type tyname uni a
cod@TyFun{} -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a (Type tyname uni a -> Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a)
-> f (Type tyname uni a -> Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
dom f (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname 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
<*> (Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
cod
TyFun a
a Type tyname uni a
dom Type tyname uni a
res -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a (Type tyname uni a -> Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a)
-> f (Type tyname uni a -> Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
dom f (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname 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
<*> 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
res
Type tyname uni a
t -> 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
t
funRes :: Lens' (Type tyname uni a) (Type tyname uni a)
funRes :: forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes Type tyname uni a -> f (Type tyname uni a)
f = \case
TyFun a
a Type tyname uni a
dom Type tyname uni a
cod -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a Type tyname uni a
dom (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
cod
Type tyname uni a
t -> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
t
vTerm :: Fold (Term tyname name uni fun ann) name
vTerm :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
vTerm = (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))
-> ((name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
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
tvTerm :: Fold (Term tyname name uni fun ann) tyname
tvTerm :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(tyname -> f tyname)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
tvTerm = (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(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 ((Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
typeTyVars