{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module PlutusCore.Normalize.Internal (
NormalizeTypeT,
MonadNormalizeType,
runNormalizeTypeT,
withExtendedTypeVarEnv,
normalizeTypeM,
substNormalizeTypeM,
normalizeTypesInM,
) where
import PlutusCore.Core.Plated (termSubterms, termSubtypes)
import PlutusCore.Core.Type (Normalized (..), Term, Type (..))
import PlutusCore.MkPlc (mkTyBuiltinOf)
import PlutusCore.Name.Unique (HasUnique, TypeUnique (TypeUnique), Unique (Unique))
import PlutusCore.Name.UniqueMap (UniqueMap, insertByName, lookupName)
import PlutusCore.Quote (MonadQuote)
import PlutusCore.Rename (Dupable, dupable, liftDupable)
import PlutusPrelude (Alternative, over, (<<$>>), (<<*>>))
import Control.Lens (makeLenses, transformMOf)
import Control.Monad (MonadPlus)
import Control.Monad.Reader (MonadReader (local), ReaderT (..), asks)
import Control.Monad.State (MonadState)
import Universe.Core (Esc, HasUniApply (matchUniApply), SomeTypeIn (SomeTypeIn))
type TypeVarEnv tyname uni ann = UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
newtype NormalizeTypeEnv tyname uni ann = NormalizeTypeEnv
{ forall tyname (uni :: * -> *) ann.
NormalizeTypeEnv tyname uni ann -> TypeVarEnv tyname uni ann
_normalizeTypeEnvTypeVarEnv :: TypeVarEnv tyname uni ann
}
makeLenses ''NormalizeTypeEnv
newtype NormalizeTypeT m tyname uni ann a = NormalizeTypeT
{ forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
unNormalizeTypeT :: ReaderT (NormalizeTypeEnv tyname uni ann) m a
}
deriving newtype
( (forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a)
-> Functor (NormalizeTypeT m tyname uni ann)
forall a b.
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$cfmap :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
fmap :: forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$c<$ :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
<$ :: forall a b.
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
Functor
, Functor (NormalizeTypeT m tyname uni ann)
Functor (NormalizeTypeT m tyname uni ann) =>
(forall a. a -> NormalizeTypeT m tyname uni ann a)
-> (forall a b.
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b)
-> (forall a b c.
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c)
-> (forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a)
-> Applicative (NormalizeTypeT m tyname uni ann)
forall a. a -> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall a b.
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall a b c.
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Applicative m =>
Functor (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Applicative m =>
a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b c.
Applicative m =>
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
$cpure :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Applicative m =>
a -> NormalizeTypeT m tyname uni ann a
pure :: forall a. a -> NormalizeTypeT m tyname uni ann a
$c<*> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
<*> :: forall a b.
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$cliftA2 :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b c.
Applicative m =>
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
liftA2 :: forall a b c.
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
$c*> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
*> :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
$c<* :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
<* :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
Applicative
, Applicative (NormalizeTypeT m tyname uni ann)
Applicative (NormalizeTypeT m tyname uni ann) =>
(forall a. NormalizeTypeT m tyname uni ann a)
-> (forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a)
-> (forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a])
-> (forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a])
-> Alternative (NormalizeTypeT m tyname uni ann)
forall a. NormalizeTypeT m tyname uni ann a
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Alternative m =>
Applicative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$cempty :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
empty :: forall a. NormalizeTypeT m tyname uni ann a
$c<|> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
<|> :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$csome :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
some :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
$cmany :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
many :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
Alternative
, Applicative (NormalizeTypeT m tyname uni ann)
Applicative (NormalizeTypeT m tyname uni ann) =>
(forall a b.
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b)
-> (forall a. a -> NormalizeTypeT m tyname uni ann a)
-> Monad (NormalizeTypeT m tyname uni ann)
forall a. a -> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall a b.
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
Applicative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Monad m =>
a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
$c>>= :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
>>= :: forall a b.
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
$c>> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
>> :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
$creturn :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Monad m =>
a -> NormalizeTypeT m tyname uni ann a
return :: forall a. a -> NormalizeTypeT m tyname uni ann a
Monad
, Monad (NormalizeTypeT m tyname uni ann)
Alternative (NormalizeTypeT m tyname uni ann)
(Alternative (NormalizeTypeT m tyname uni ann),
Monad (NormalizeTypeT m tyname uni ann)) =>
(forall a. NormalizeTypeT m tyname uni ann a)
-> (forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a)
-> MonadPlus (NormalizeTypeT m tyname uni ann)
forall a. NormalizeTypeT m tyname uni ann a
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadPlus m =>
Monad (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadPlus m =>
Alternative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$cmzero :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
mzero :: forall a. NormalizeTypeT m tyname uni ann a
$cmplus :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
mplus :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
MonadPlus
, MonadReader (NormalizeTypeEnv tyname uni ann)
, MonadState s
, Monad (NormalizeTypeT m tyname uni ann)
Monad (NormalizeTypeT m tyname uni ann) =>
(forall a. Quote a -> NormalizeTypeT m tyname uni ann a)
-> MonadQuote (NormalizeTypeT m tyname uni ann)
forall a. Quote a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *).
Monad m =>
(forall a. Quote a -> m a) -> MonadQuote m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadQuote m =>
Monad (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadQuote m =>
Quote a -> NormalizeTypeT m tyname uni ann a
$cliftQuote :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadQuote m =>
Quote a -> NormalizeTypeT m tyname uni ann a
liftQuote :: forall a. Quote a -> NormalizeTypeT m tyname uni ann a
MonadQuote
)
type MonadNormalizeType uni m =
( MonadQuote m
, HasUniApply uni
)
runNormalizeTypeT :: NormalizeTypeT m tyname uni ann a -> m a
runNormalizeTypeT :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
runNormalizeTypeT = (ReaderT (NormalizeTypeEnv tyname uni ann) m a
-> NormalizeTypeEnv tyname uni ann -> m a)
-> NormalizeTypeEnv tyname uni ann
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (NormalizeTypeEnv tyname uni ann) m a
-> NormalizeTypeEnv tyname uni ann -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeVarEnv tyname uni ann -> NormalizeTypeEnv tyname uni ann
forall tyname (uni :: * -> *) ann.
TypeVarEnv tyname uni ann -> NormalizeTypeEnv tyname uni ann
NormalizeTypeEnv TypeVarEnv tyname uni ann
forall a. Monoid a => a
mempty) (ReaderT (NormalizeTypeEnv tyname uni ann) m a -> m a)
-> (NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a)
-> NormalizeTypeT m tyname uni ann a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
unNormalizeTypeT
withExtendedTypeVarEnv ::
(HasUnique tyname TypeUnique, Monad m) =>
tyname ->
Normalized (Type tyname uni ann) ->
NormalizeTypeT m tyname uni ann a ->
NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv :: forall tyname (m :: * -> *) (uni :: * -> *) ann a.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv tyname
name =
(NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall a.
(NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a)
-> (Normalized (Type tyname uni ann)
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann)
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
(NormalizeTypeEnv tyname uni ann)
(NormalizeTypeEnv tyname uni ann)
(UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
(UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> (UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(NormalizeTypeEnv tyname uni ann)
(NormalizeTypeEnv tyname uni ann)
(UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
(UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
forall tyname (uni :: * -> *) ann tyname (uni :: * -> *) ann
(p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (TypeVarEnv tyname uni ann) (f (TypeVarEnv tyname uni ann))
-> p (NormalizeTypeEnv tyname uni ann)
(f (NormalizeTypeEnv tyname uni ann))
normalizeTypeEnvTypeVarEnv ((UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann)
-> (Normalized (Type tyname uni ann)
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tyname
-> Dupable (Normalized (Type tyname uni ann))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName tyname
name (Dupable (Normalized (Type tyname uni ann))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> (Normalized (Type tyname uni ann)
-> Dupable (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Normalized (Type tyname uni ann)
-> Dupable (Normalized (Type tyname uni ann))
forall a. a -> Dupable a
dupable
lookupTyNameM ::
(HasUnique tyname TypeUnique, Monad m) =>
tyname ->
NormalizeTypeT m tyname uni ann (Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM :: forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM tyname
name = (NormalizeTypeEnv tyname uni ann
-> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann))))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((NormalizeTypeEnv tyname uni ann
-> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann)))))
-> (NormalizeTypeEnv tyname uni ann
-> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann))))
forall a b. (a -> b) -> a -> b
$ tyname
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> Maybe (Dupable (Normalized (Type tyname uni ann)))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName tyname
name (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> (NormalizeTypeEnv tyname uni ann
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeEnv tyname uni ann
-> Maybe (Dupable (Normalized (Type tyname uni ann)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NormalizeTypeEnv tyname uni ann
-> UniqueMap
TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall tyname (uni :: * -> *) ann.
NormalizeTypeEnv tyname uni ann -> TypeVarEnv tyname uni ann
_normalizeTypeEnvTypeVarEnv
normalizeUni :: forall k (a :: k) uni tyname. HasUniApply uni => uni (Esc a) -> Type tyname uni ()
normalizeUni :: forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uni =
uni (Esc a)
-> Type tyname uni ()
-> (forall k l (f :: k -> l) (a :: k).
(Esc a ~ Esc (f a)) =>
uni (Esc f) -> uni (Esc a) -> Type tyname uni ())
-> Type tyname uni ()
forall tb r.
uni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
uni (Esc f) -> uni (Esc a) -> r)
-> r
forall (uni :: * -> *) tb r.
HasUniApply uni =>
uni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
uni (Esc f) -> uni (Esc a) -> r)
-> r
matchUniApply
uni (Esc a)
uni
(() -> uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () uni (Esc a)
uni)
(\uni (Esc f)
uniF uni (Esc a)
uniA -> ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (uni (Esc f) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc f)
uniF) (Type tyname uni () -> Type tyname uni ())
-> Type tyname uni () -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uniA)
normalizeTypeM ::
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann ->
NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM :: forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM (TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) =
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
name Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
body
normalizeTypeM (TyIFix ann
ann Type tyname uni ann
pat Type tyname uni ann
arg) =
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 -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m
tyname
uni
ann
(Normalized (Type tyname uni ann -> Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
pat NormalizeTypeT
m
tyname
uni
ann
(Normalized (Type tyname uni ann -> Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
arg
normalizeTypeM (TyFun ann
ann Type tyname uni ann
dom Type tyname uni ann
cod) =
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 -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m
tyname
uni
ann
(Normalized (Type tyname uni ann -> Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
dom NormalizeTypeT
m
tyname
uni
ann
(Normalized (Type tyname uni ann -> Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
cod
normalizeTypeM (TyLam ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) =
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
name Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
body
normalizeTypeM (TyApp ann
ann Type tyname uni ann
fun Type tyname uni ann
arg) = do
Normalized (Type tyname uni ann)
vFun <- Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
fun
Normalized (Type tyname uni ann)
vArg <- Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
arg
case Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized Normalized (Type tyname uni ann)
vFun of
TyLam ann
_ tyname
nArg Kind ann
_ Type tyname uni ann
body -> Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM Normalized (Type tyname uni ann)
vArg tyname
nArg Type tyname uni ann
body
Type tyname uni ann
_ -> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ 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 -> Type tyname uni ann)
-> Normalized (Type tyname uni ann)
-> Normalized (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type tyname uni ann)
vFun Normalized (Type tyname uni ann -> Type tyname uni ann)
-> Normalized (Type tyname uni ann)
-> Normalized (Type tyname uni ann)
forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Normalized (Type tyname uni ann)
vArg
normalizeTypeM var :: Type tyname uni ann
var@(TyVar ann
_ tyname
name) = do
Maybe (Dupable (Normalized (Type tyname uni ann)))
mayTy <- tyname
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann))))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> NormalizeTypeT
m
tyname
uni
ann
(Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM tyname
name
case Maybe (Dupable (Normalized (Type tyname uni ann)))
mayTy of
Maybe (Dupable (Normalized (Type tyname uni ann)))
Nothing -> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized Type tyname uni ann
var
Just Dupable (Normalized (Type tyname uni ann))
ty -> Dupable (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type tyname uni ann))
ty
normalizeTypeM (TyBuiltin ann
ann (SomeTypeIn uni (Esc a)
uni)) =
Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> (Type tyname uni ann -> Normalized (Type tyname uni ann))
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized (Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type tyname uni () -> Type tyname uni ann
forall a b. a -> Type tyname uni b -> Type tyname uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uni
normalizeTypeM (TySOP ann
ann [[Type tyname uni ann]]
tyls) = do
[[Type tyname uni ann]]
tyls' <- (([Type tyname uni ann]
-> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
-> [[Type tyname uni ann]]
-> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (([Type tyname uni ann]
-> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
-> [[Type tyname uni ann]]
-> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]])
-> ((Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> [Type tyname uni ann]
-> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
-> (Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> [[Type tyname uni ann]]
-> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> [Type tyname uni ann]
-> NormalizeTypeT m tyname uni ann [Type tyname uni ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) ((Normalized (Type tyname uni ann) -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> (Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM) [[Type tyname uni ann]]
tyls
Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized (Type tyname uni ann -> Normalized (Type tyname uni ann))
-> Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ 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]]
tyls'
substNormalizeTypeM ::
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Normalized (Type tyname uni ann) ->
tyname ->
Type tyname uni ann ->
NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM :: forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM Normalized (Type tyname uni ann)
ty tyname
name = tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (m :: * -> *) (uni :: * -> *) ann a.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv tyname
name Normalized (Type tyname uni ann)
ty (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> (Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM
normalizeTypesInM ::
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Term tyname name uni fun ann ->
NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeTypesInM :: forall tyname (uni :: * -> *) (m :: * -> *) name fun ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeTypesInM = LensLike
(WrappedMonad (NormalizeTypeT m tyname uni 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)
-> (Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (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 (NormalizeTypeT m tyname uni 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)
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
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
forall {name} {fun} {ann}.
Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeChildTypes
where
normalizeChildTypes :: Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeChildTypes = (Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (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 ((Normalized (Type tyname uni ann) -> Type tyname uni ann)
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> (Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM)