{-# 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

-- | Applicatively replace a type variable using the given function.
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
{-# INLINE substTyVarA #-}

-- | Applicatively replace a variable using the given function.
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

-- | Replace a type variable using the given function.
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

-- | Replace a variable using the given function.
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

-- | Naively monadically substitute type names (i.e. do not substitute binders).
-- INLINE is important here because the function is too polymorphic (determined from profiling)
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
{-# INLINE typeSubstTyNamesM #-}

-- | Naively monadically substitute names using the given function (i.e. do not substitute binders).
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

-- | Naively monadically substitute type names using the given function
-- (i.e. do not substitute binders).
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

-- | Naively substitute type names (i.e. do not substitute binders).
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

-- | Naively substitute names using the given function (i.e. do not substitute binders).
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

-- | Naively substitute type names using the given function (i.e. do not substitute binders).
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

-- | Substitute the given closed 'Type' for the given type variable in the given 'Type'. Does not
-- descend under binders that bind the same variable as the one we're substituting for (since from
-- there that variable is no longer free). The resulting 'Term' may and likely will not satisfy
-- global uniqueness.
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

-- | Substitute the given closed 'Type' for the given type variable in the given 'Term'. Does not
-- descend under binders that bind the same variable as the one we're substituting for (since from
-- there that variable is no longer free). The resulting 'Term' may and likely will not satisfy
-- global uniqueness.
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

-- | Substitute the given closed 'Term' for the given term variable in the given 'Term'. Does not
-- descend under binders that bind the same variable as the one we're substituting for (since from
-- there that variable is no longer free). The resulting 'Term' may and likely will not satisfy
-- global uniqueness.
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

-- Mapping name-modification functions over types and terms.

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 requires two function arguments: one (called f) to modify type names
-- and another (called g) to modify variable names.
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)

-- Free variables

-- | Get all the free term variables in a 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

-- | Get all the free type variables in a term.
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
    -- sound because the subterms and subtypes are disjoint
    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

-- | Get all the free type variables in a type.
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


-- TODO: these could be Traversals
-- | Get all the term variables in a term.
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

-- | Get all the type variables in a term.
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

-- | Get all the type variables in a type.
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