{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module PlutusCore.Subst
( substTyVarA
, substVarA
, substTyVar
, substVar
, termSubstNamesM
, termSubstTyNamesM
, typeSubstTyNamesM
, termSubstNames
, termSubstTyNames
, typeSubstTyNames
, typeSubstClosedType
, termSubstClosedType
, termSubstClosedTerm
, typeMapNames
, termMapNames
, programMapNames
, fvTerm
, ftvTerm
, ftvTy
, ftvTyCtx
, vTerm
, tvTerm
, tvTy
, purely
) where
import PlutusPrelude
import PlutusCore.Core
import Control.Lens
import Control.Lens.Unsound qualified as Unsound
import PlutusCore.Name.Unique (HasUnique)
import PlutusCore.Name.UniqueSet (UniqueSet)
import PlutusCore.Name.UniqueSet qualified as USet
purely :: ((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely :: forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely = ((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
forall a b. Coercible a b => a -> b
coerce
{-# INLINE substTyVarA #-}
substTyVarA
:: Applicative f
=> (tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> f (Type tyname uni ann)
substTyVarA :: forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA tyname -> f (Maybe (Type tyname uni ann))
tynameF ty :: Type tyname uni ann
ty@(TyVar ann
_ tyname
tyname) = Type tyname uni ann
-> Maybe (Type tyname uni ann) -> Type tyname uni ann
forall a. a -> Maybe a -> a
fromMaybe Type tyname uni ann
ty (Maybe (Type tyname uni ann) -> Type tyname uni ann)
-> f (Maybe (Type tyname uni ann)) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tyname -> f (Maybe (Type tyname uni ann))
tynameF tyname
tyname
substTyVarA tyname -> f (Maybe (Type tyname uni ann))
_ Type tyname uni ann
ty = Type tyname uni ann -> f (Type tyname uni ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty
substVarA
:: Applicative f
=> (name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
substVarA :: forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
Applicative f =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA name -> f (Maybe (Term tyname name uni fun ann))
nameF t :: Term tyname name uni fun ann
t@(Var ann
_ name
name) = Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
forall a. a -> Maybe a -> a
fromMaybe Term tyname name uni fun ann
t (Maybe (Term tyname name uni fun ann)
-> Term tyname name uni fun ann)
-> f (Maybe (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
<$> name -> f (Maybe (Term tyname name uni fun ann))
nameF name
name
substVarA name -> f (Maybe (Term tyname name uni fun ann))
_ 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
substTyVar
:: (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
substTyVar :: forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
substTyVar = ((tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA
substVar
:: (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
substVar :: forall name tyname (uni :: * -> *) fun ann.
(name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
substVar = ((name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann))
-> (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
Applicative f =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA
{-# INLINE typeSubstTyNamesM #-}
typeSubstTyNamesM
:: Monad m
=> (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> m (Type tyname uni ann)
typeSubstTyNamesM :: forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
typeSubstTyNamesM = LensLike
(WrappedMonad m)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
-> (Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
(WrappedMonad m)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypes ((Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann -> m (Type tyname uni ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA
termSubstNamesM
:: Monad m
=> (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
termSubstNamesM :: forall (m :: * -> *) name tyname (uni :: * -> *) fun ann.
Monad m =>
(name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM = LensLike
(WrappedMonad m)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
-> (Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
(WrappedMonad m)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> ((name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) name tyname (uni :: * -> *) fun ann.
Applicative f =>
(name -> f (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
substVarA
termSubstTyNamesM
:: Monad m
=> (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
termSubstTyNamesM :: forall (m :: * -> *) tyname (uni :: * -> *) ann name fun.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM =
LensLike
(WrappedMonad m)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
-> (Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
(WrappedMonad m)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLike
m
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Type tyname uni ann)
(Type tyname uni ann)
-> LensLike
m
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Type tyname uni ann)
(Type tyname uni ann)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike
m
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Type tyname uni ann)
(Type tyname uni ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypes LensLike
m
(Term tyname name uni fun ann)
(Term tyname name uni fun ann)
(Type tyname uni ann)
(Type tyname uni ann)
-> ((tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLike
(WrappedMonad m)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
-> (Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
(WrappedMonad m)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
(Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypes ((Type tyname uni ann -> m (Type tyname uni ann))
-> Type tyname uni ann -> m (Type tyname uni ann))
-> ((tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann))
-> (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann
-> m (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) tyname (uni :: * -> *) ann.
Applicative f =>
(tyname -> f (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> f (Type tyname uni ann)
substTyVarA
typeSubstTyNames
:: (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
typeSubstTyNames :: forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames = ((tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann
-> Type tyname uni ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> Identity (Type tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Type tyname uni ann -> m (Type tyname uni ann)
typeSubstTyNamesM
termSubstNames
:: (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
termSubstNames :: forall name tyname (uni :: * -> *) fun ann.
(name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
termSubstNames = ((name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann))
-> (name -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (name -> Identity (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (m :: * -> *) name tyname (uni :: * -> *) fun ann.
Monad m =>
(name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM
termSubstTyNames
:: (tyname -> Maybe (Type tyname uni ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
termSubstTyNames :: forall tyname (uni :: * -> *) ann name fun.
(tyname -> Maybe (Type tyname uni ann))
-> Term tyname name uni fun ann -> Term tyname name uni fun ann
termSubstTyNames = ((tyname -> Identity (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann))
-> (tyname -> Maybe (Type tyname uni ann))
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a b c d.
((a -> Identity b) -> c -> Identity d) -> (a -> b) -> c -> d
purely (tyname -> Identity (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> Identity (Term tyname name uni fun ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann name fun.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM
typeSubstClosedType
:: Eq tyname => tyname -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType :: forall tyname (uni :: * -> *) a.
Eq tyname =>
tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType tyname
tn0 Type tyname uni a
ty0 = Type tyname uni a -> Type tyname uni a
go where
go :: Type tyname uni a -> Type tyname uni a
go = \case
TyVar a
a tyname
tn -> if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Type tyname uni a
ty0 else a -> tyname -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar a
a tyname
tn
TyForall a
a tyname
tn Kind a
k Type tyname uni a
ty -> a -> tyname -> Kind a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall a
a tyname
tn Kind a
k (tyname -> Type tyname uni a -> Type tyname uni a
goUnder tyname
tn Type tyname uni a
ty)
TyLam a
a tyname
tn Kind a
k Type tyname uni a
ty -> a -> tyname -> Kind a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam a
a tyname
tn Kind a
k (tyname -> Type tyname uni a -> Type tyname uni a
goUnder tyname
tn Type tyname uni a
ty)
Type tyname uni a
ty -> Type tyname uni a
ty Type tyname uni a
-> (Type tyname uni a -> Type tyname uni a) -> Type tyname uni a
forall a b. a -> (a -> b) -> b
& ASetter
(Type tyname uni a)
(Type tyname uni a)
(Type tyname uni a)
(Type tyname uni a)
-> (Type tyname uni a -> Type tyname uni a)
-> Type tyname uni a
-> Type tyname uni a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(Type tyname uni a)
(Type tyname uni a)
(Type tyname uni a)
(Type tyname uni a)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypes Type tyname uni a -> Type tyname uni a
go
goUnder :: tyname -> Type tyname uni a -> Type tyname uni a
goUnder tyname
tn Type tyname uni a
ty = if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Type tyname uni a
ty else Type tyname uni a -> Type tyname uni a
go Type tyname uni a
ty
termSubstClosedType
:: Eq tyname
=> tyname -> Type tyname uni a -> Term tyname name uni fun a -> Term tyname name uni fun a
termSubstClosedType :: forall tyname (uni :: * -> *) a name fun.
Eq tyname =>
tyname
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
termSubstClosedType tyname
tn0 Type tyname uni a
ty0 = Term tyname name uni fun a -> Term tyname name uni fun a
forall {name} {fun}.
Term tyname name uni fun a -> Term tyname name uni fun a
go where
go :: Term tyname name uni fun a -> Term tyname name uni fun a
go = \case
TyAbs a
a tyname
tn Kind a
k Term tyname name uni fun a
body -> a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs a
a tyname
tn Kind a
k (tyname -> Term tyname name uni fun a -> Term tyname name uni fun a
goUnder tyname
tn Term tyname name uni fun a
body)
Term tyname name uni fun a
t -> Term tyname name uni fun a
t Term tyname name uni fun a
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
forall a b. a -> (a -> b) -> b
& ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Type tyname uni a)
(Type tyname uni a)
-> (Type tyname uni a -> Type tyname uni a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Type tyname uni a)
(Type tyname uni a)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypes Type tyname uni a -> Type tyname uni a
goTy Term tyname name uni fun a
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
forall a b. a -> (a -> b) -> b
& ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms Term tyname name uni fun a -> Term tyname name uni fun a
go
goUnder :: tyname -> Term tyname name uni fun a -> Term tyname name uni fun a
goUnder tyname
tn Term tyname name uni fun a
term = if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Term tyname name uni fun a
term else Term tyname name uni fun a -> Term tyname name uni fun a
go Term tyname name uni fun a
term
goTy :: Type tyname uni a -> Type tyname uni a
goTy = tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) a.
Eq tyname =>
tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType tyname
tn0 Type tyname uni a
ty0
termSubstClosedTerm
:: Eq name
=> name
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
termSubstClosedTerm :: forall name tyname (uni :: * -> *) fun a.
Eq name =>
name
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
termSubstClosedTerm name
varFor Term tyname name uni fun a
new = Term tyname name uni fun a -> Term tyname name uni fun a
go where
go :: Term tyname name uni fun a -> Term tyname name uni fun a
go = \case
Var a
a name
var -> if name
var name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
varFor then Term tyname name uni fun a
new else a -> name -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var a
a name
var
LamAbs a
a name
var Type tyname uni a
ty Term tyname name uni fun a
body -> a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs a
a name
var Type tyname uni a
ty (name -> Term tyname name uni fun a -> Term tyname name uni fun a
goUnder name
var Term tyname name uni fun a
body)
Term tyname name uni fun a
t -> Term tyname name uni fun a
t Term tyname name uni fun a
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
forall a b. a -> (a -> b) -> b
& ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
(Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms Term tyname name uni fun a -> Term tyname name uni fun a
go
goUnder :: name -> Term tyname name uni fun a -> Term tyname name uni fun a
goUnder name
var Term tyname name uni fun a
term = if name
var name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
varFor then Term tyname name uni fun a
term else Term tyname name uni fun a -> Term tyname name uni fun a
go Term tyname name uni fun a
term
typeMapNames
:: forall tyname tyname' uni ann
. (tyname -> tyname')
-> Type tyname uni ann
-> Type tyname' uni ann
typeMapNames :: forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f = Type tyname uni ann -> Type tyname' uni ann
go
where
go :: Type tyname uni ann -> Type tyname' uni ann
go :: Type tyname uni ann -> Type tyname' uni ann
go = \case
TyVar ann
ann tyname
tn -> ann -> tyname' -> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (tyname -> tyname'
f tyname
tn)
TyFun ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 -> ann
-> Type tyname' uni ann
-> Type tyname' uni ann
-> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty1) (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty2)
TyIFix ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 -> ann
-> Type tyname' uni ann
-> Type tyname' uni ann
-> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty1) (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty2)
TyForall ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> ann
-> tyname'
-> Kind ann
-> Type tyname' uni ann
-> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann (tyname -> tyname'
f tyname
tn) Kind ann
k (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty)
TyBuiltin ann
ann SomeTypeIn uni
s -> ann -> SomeTypeIn uni -> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin ann
ann SomeTypeIn uni
s
TyLam ann
ann tyname
tn Kind ann
k Type tyname uni ann
ty -> ann
-> tyname'
-> Kind ann
-> Type tyname' uni ann
-> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann (tyname -> tyname'
f tyname
tn) Kind ann
k (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty)
TyApp ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 -> ann
-> Type tyname' uni ann
-> Type tyname' uni ann
-> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty1) (Type tyname uni ann -> Type tyname' uni ann
go Type tyname uni ann
ty2)
TySOP ann
ann [[Type tyname uni ann]]
tyls -> ann -> [[Type tyname' uni ann]] -> Type tyname' uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ((([Type tyname uni ann] -> [Type tyname' uni ann])
-> [[Type tyname uni ann]] -> [[Type tyname' uni ann]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Type tyname uni ann] -> [Type tyname' uni ann])
-> [[Type tyname uni ann]] -> [[Type tyname' uni ann]])
-> ((Type tyname uni ann -> Type tyname' uni ann)
-> [Type tyname uni ann] -> [Type tyname' uni ann])
-> (Type tyname uni ann -> Type tyname' uni ann)
-> [[Type tyname uni ann]]
-> [[Type tyname' uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> Type tyname' uni ann)
-> [Type tyname uni ann] -> [Type tyname' uni ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Type tyname uni ann -> Type tyname' uni ann
go [[Type tyname uni ann]]
tyls)
termMapNames
:: forall tyname tyname' name name' uni fun ann
. (tyname -> tyname')
-> (name -> name')
-> Term tyname name uni fun ann
-> Term tyname' name' uni fun ann
termMapNames :: forall tyname tyname' name name' (uni :: * -> *) fun ann.
(tyname -> tyname')
-> (name -> name')
-> Term tyname name uni fun ann
-> Term tyname' name' uni fun ann
termMapNames tyname -> tyname'
f name -> name'
g = Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go
where
go :: Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go :: Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go = \case
LamAbs ann
ann name
name Type tyname uni ann
ty Term tyname name uni fun ann
body -> ann
-> name'
-> Type tyname' uni ann
-> Term tyname' name' uni fun ann
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann (name -> name'
g name
name) ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty) (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
body)
TyAbs ann
ann tyname
tyname Kind ann
k Term tyname name uni fun ann
body -> ann
-> tyname'
-> Kind ann
-> Term tyname' name' uni fun ann
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann (tyname -> tyname'
f tyname
tyname) Kind ann
k (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
body)
Var ann
ann name
name -> ann -> name' -> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann (name -> name'
g name
name)
Apply ann
ann Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2 -> ann
-> Term tyname' name' uni fun ann
-> Term tyname' name' uni fun ann
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
t1) (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
t2)
Constant ann
ann Some (ValueOf uni)
c -> ann -> Some (ValueOf uni) -> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant ann
ann Some (ValueOf uni)
c
Builtin ann
ann fun
b -> ann -> fun -> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin ann
ann fun
b
TyInst ann
ann Term tyname name uni fun ann
body Type tyname uni ann
ty -> ann
-> Term tyname' name' uni fun ann
-> Type tyname' uni ann
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
body) ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty)
Unwrap ann
ann Term tyname name uni fun ann
body -> ann
-> Term tyname' name' uni fun ann -> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
ann (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
body)
IWrap ann
ann Type tyname uni ann
ty1 Type tyname uni ann
ty2 Term tyname name uni fun ann
body -> ann
-> Type tyname' uni ann
-> Type tyname' uni ann
-> Term tyname' name' uni fun ann
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty1) ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty2) (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
body)
Constr ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es -> ann
-> Type tyname' uni ann
-> Word64
-> [Term tyname' name' uni fun ann]
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty) Word64
i ((Term tyname name uni fun ann -> Term tyname' name' uni fun ann)
-> [Term tyname name uni fun ann]
-> [Term tyname' name' uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go [Term tyname name uni fun ann]
es)
Case ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs -> ann
-> Type tyname' uni ann
-> Term tyname' name' uni fun ann
-> [Term tyname' name' uni fun ann]
-> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty) (Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go Term tyname name uni fun ann
arg) ((Term tyname name uni fun ann -> Term tyname' name' uni fun ann)
-> [Term tyname name uni fun ann]
-> [Term tyname' name' uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun ann -> Term tyname' name' uni fun ann
go [Term tyname name uni fun ann]
cs)
Error ann
ann Type tyname uni ann
ty -> ann -> Type tyname' uni ann -> Term tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann ((tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
forall tyname tyname' (uni :: * -> *) ann.
(tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
typeMapNames tyname -> tyname'
f Type tyname uni ann
ty)
programMapNames
:: forall tyname tyname' name name' uni fun ann
. (tyname -> tyname')
-> (name -> name')
-> Program tyname name uni fun ann
-> Program tyname' name' uni fun ann
programMapNames :: forall tyname tyname' name name' (uni :: * -> *) fun ann.
(tyname -> tyname')
-> (name -> name')
-> Program tyname name uni fun ann
-> Program tyname' name' uni fun ann
programMapNames tyname -> tyname'
f name -> name'
g (Program ann
a Version
v Term tyname name uni fun ann
term) = ann
-> Version
-> Term tyname' name' uni fun ann
-> Program tyname' name' uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program ann
a Version
v ((tyname -> tyname')
-> (name -> name')
-> Term tyname name uni fun ann
-> Term tyname' name' uni fun ann
forall tyname tyname' name name' (uni :: * -> *) fun ann.
(tyname -> tyname')
-> (name -> name')
-> Term tyname name uni fun ann
-> Term tyname' name' uni fun ann
termMapNames tyname -> tyname'
f name -> name'
g Term tyname name uni fun ann
term)
fvTerm :: HasUnique name unique => Traversal' (Term tyname name uni fun ann) name
fvTerm :: forall name unique tyname (uni :: * -> *) fun ann.
HasUnique name unique =>
Traversal' (Term tyname name uni fun ann) name
fvTerm = UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
forall name unique tyname (uni :: * -> *) fun ann.
HasUnique name unique =>
UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet unique
forall a. Monoid a => a
mempty
fvTermCtx
:: HasUnique name unique
=> UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
fvTermCtx :: forall name unique tyname (uni :: * -> *) fun ann.
HasUnique name unique =>
UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet unique
bound name -> f name
f = \case
Var ann
a name
n -> ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
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 unique -> Bool
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> Bool
USet.memberByName name
n UniqueSet unique
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 ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
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 unique -> Traversal' (Term tyname name uni fun ann) name
forall name unique tyname (uni :: * -> *) fun ann.
HasUnique name unique =>
UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
fvTermCtx (name -> UniqueSet unique -> UniqueSet unique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName name
n UniqueSet unique
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 ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> 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 unique -> Traversal' (Term tyname name uni fun ann) name
forall name unique tyname (uni :: * -> *) fun ann.
HasUnique name unique =>
UniqueSet unique -> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet unique
bound) name -> f name
f Term tyname name uni fun ann
t
ftvTerm :: HasUnique tyname unique => Traversal' (Term tyname name uni fun ann) tyname
ftvTerm :: forall tyname unique name (uni :: * -> *) fun ann.
HasUnique tyname unique =>
Traversal' (Term tyname name uni fun ann) tyname
ftvTerm = UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname unique name (uni :: * -> *) fun ann.
HasUnique tyname unique =>
UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet unique
forall a. Monoid a => a
mempty
ftvTermCtx
:: HasUnique tyname unique
=> UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx :: forall tyname unique name (uni :: * -> *) fun ann.
HasUnique tyname unique =>
UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet unique
bound tyname -> f tyname
f = \case
TyAbs ann
a tyname
ty Kind ann
k Term tyname name uni fun ann
t -> ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
a tyname
ty 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 unique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname unique name (uni :: * -> *) fun ann.
HasUnique tyname unique =>
UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx (tyname -> UniqueSet unique -> UniqueSet unique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName tyname
ty UniqueSet unique
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 ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> 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 unique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname unique name (uni :: * -> *) fun ann.
HasUnique tyname unique =>
UniqueSet unique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet unique
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 ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann))
-> ((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 unique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet unique
bound)) tyname -> f tyname
f Term tyname name uni fun ann
t
ftvTy
:: HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
ftvTy :: forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
ftvTy = UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet unique
forall a. Monoid a => a
mempty
ftvTyCtx
:: HasUnique tyname unique
=> UniqueSet unique
-> Traversal' (Type tyname uni ann) tyname
ftvTyCtx :: forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet unique
bound tyname -> f tyname
f = \case
TyVar ann
a tyname
ty -> ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
a (tyname -> Type tyname uni ann)
-> f tyname -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (if tyname -> UniqueSet unique -> Bool
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> Bool
USet.memberByName tyname
ty UniqueSet unique
bound then tyname -> f tyname
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure tyname
ty else tyname -> f tyname
f tyname
ty)
TyForall ann
a tyname
bnd Kind ann
k Type tyname uni ann
ty -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
a tyname
bnd Kind ann
k (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx (tyname -> UniqueSet unique -> UniqueSet unique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName tyname
bnd UniqueSet unique
bound) tyname -> f tyname
f Type tyname uni ann
ty
TyLam ann
a tyname
bnd Kind ann
k Type tyname uni ann
ty -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
a tyname
bnd Kind ann
k (Type tyname uni ann -> Type tyname uni ann)
-> f (Type tyname uni ann) -> f (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx (tyname -> UniqueSet unique -> UniqueSet unique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName tyname
bnd UniqueSet unique
bound) tyname -> f tyname
f Type tyname uni ann
ty
Type tyname uni ann
t -> ((Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Type tyname uni ann
-> f (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet unique
bound) tyname -> f tyname
f Type tyname uni ann
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
tvTy :: Fold (Type tyname uni ann) tyname
tvTy :: forall tyname (uni :: * -> *) ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
tvTy = (Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann)
typeSubtypesDeep ((Type tyname uni ann -> f (Type tyname uni ann))
-> Type tyname uni ann -> f (Type tyname uni ann))
-> ((tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Type tyname uni ann
-> f (Type tyname 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 tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
typeTyVars