{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module PlutusIR.Transform.Rename
( renameTermM
, renameProgramM
) where
import PlutusPrelude
import PlutusIR
import PlutusIR.Mark
import PlutusCore qualified as PLC
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Rename.Internal qualified as PLC
import Control.Monad.Reader
import Control.Monad.Trans.Cont (ContT (..))
instance PLC.HasUniques (Term tyname name uni fun ann) => PLC.Rename (Term tyname name uni fun ann) where
rename :: forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
rename = (Term tyname name uni fun ann -> m ())
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term tyname name uni fun ann -> m ()
forall tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m) =>
Term tyname name uni fun ann -> m ()
markNonFreshTerm (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))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RenameT ScopedRenaming m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall ren (m :: * -> *) a. Monoid ren => RenameT ren m a -> m a
PLC.runRenameT (RenameT ScopedRenaming m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
-> RenameT ScopedRenaming m (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
. Term tyname name uni fun ann
-> RenameT ScopedRenaming m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM
instance PLC.HasUniques (Term tyname name uni fun ann) => PLC.Rename (Program tyname name uni fun ann) where
rename :: forall (m :: * -> *).
MonadQuote m =>
Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
rename (Program ann
ann 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
ann Version
v (Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Program tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
PLC.rename Term tyname name uni fun ann
term
newtype Restorer m = Restorer
{ forall (m :: * -> *). Restorer m -> forall a. m a -> m a
unRestorer :: forall a. m a -> m a
}
captureContext :: MonadReader ren m => ContT c m (Restorer m)
captureContext :: forall ren (m :: * -> *) c.
MonadReader ren m =>
ContT c m (Restorer m)
captureContext = ((Restorer m -> m c) -> m c) -> ContT c m (Restorer m)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((Restorer m -> m c) -> m c) -> ContT c m (Restorer m))
-> ((Restorer m -> m c) -> m c) -> ContT c m (Restorer m)
forall a b. (a -> b) -> a -> b
$ \Restorer m -> m c
k -> do
ren
env <- m ren
forall r (m :: * -> *). MonadReader r m => m r
ask
Restorer m -> m c
k (Restorer m -> m c) -> Restorer m -> m c
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> m a) -> Restorer m
forall (m :: * -> *). (forall a. m a -> m a) -> Restorer m
Restorer ((forall a. m a -> m a) -> Restorer m)
-> (forall a. m a -> m a) -> Restorer m
forall a b. (a -> b) -> a -> b
$ (ren -> ren) -> m a -> m a
forall a. (ren -> ren) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ren -> ren) -> m a -> m a) -> (ren -> ren) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ren -> ren -> ren
forall a b. a -> b -> a
const ren
env
type MonadRename m = (PLC.MonadQuote m, MonadReader PLC.ScopedRenaming m)
renameConstrTypeM
:: (MonadRename m, PLC.HasUniques (Type tyname uni ann))
=> Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM :: forall (m :: * -> *) tyname (uni :: * -> *) ann.
(MonadRename m, HasUniques (Type tyname uni ann)) =>
Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM (Restorer forall a. m a -> m a
restoreAfterData) = Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM where
renameSpineM :: Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM (TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
ty) =
tyname
-> (tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName tyname
name ((tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann))
-> (tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ \tyname
nameFr -> 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
nameFr Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM Type tyname uni ann
ty
renameSpineM (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)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
dom m (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM Type tyname uni ann
cod
renameSpineM Type tyname uni ann
ty = Type tyname uni ann -> m (Type tyname uni ann)
renameResultM Type tyname uni ann
ty
renameResultM :: Type tyname uni ann -> m (Type tyname uni ann)
renameResultM (TyApp ann
ann Type tyname uni ann
fun 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
TyApp ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
renameResultM Type tyname uni ann
fun m (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
arg
renameResultM (TyVar ann
ann tyname
name) = ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (tyname -> Type tyname uni ann)
-> m tyname -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m tyname -> m tyname
forall a. m a -> m a
restoreAfterData (tyname -> m tyname
forall ren unique name (m :: * -> *).
(HasRenaming ren unique, HasUnique name unique,
MonadReader ren m) =>
name -> m name
PLC.renameNameM tyname
name)
renameResultM Type tyname uni ann
_ =
[Char] -> m (Type tyname uni ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: a constructor returns something that is not an iterated application of a type variable"
renameConstrCM
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Restorer m
-> VarDecl tyname name uni ann
-> ContT c m (m (VarDecl tyname name uni ann))
renameConstrCM :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Restorer m
-> VarDecl tyname name uni ann
-> ContT c m (m (VarDecl tyname name uni ann))
renameConstrCM Restorer m
restorerAfterData (VarDecl ann
ann name
name Type tyname uni ann
ty) = do
name
nameFr <- ((name -> m c) -> m c) -> ContT c m name
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((name -> m c) -> m c) -> ContT c m name)
-> ((name -> m c) -> m c) -> ContT c m name
forall a b. (a -> b) -> a -> b
$ name -> (name -> m c) -> m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
name
m (VarDecl tyname name uni ann)
-> ContT c m (m (VarDecl tyname name uni ann))
forall a. a -> ContT c m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (VarDecl tyname name uni ann)
-> ContT c m (m (VarDecl tyname name uni ann)))
-> m (VarDecl tyname name uni ann)
-> ContT c m (m (VarDecl tyname name uni ann))
forall a b. (a -> b) -> a -> b
$ ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann name
nameFr (Type tyname uni ann -> VarDecl tyname name uni ann)
-> m (Type tyname uni ann) -> m (VarDecl tyname name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
(MonadRename m, HasUniques (Type tyname uni ann)) =>
Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM Restorer m
restorerAfterData Type tyname uni ann
ty
onNonRec :: Recursivity -> (a -> a) -> a -> a
onNonRec :: forall a. Recursivity -> (a -> a) -> a -> a
onNonRec Recursivity
NonRec a -> a
f a
x = a -> a
f a
x
onNonRec Recursivity
Rec a -> a
_ a
x = a
x
renameDatatypeCM
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
renameDatatypeCM :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
renameDatatypeCM Recursivity
recy (Datatype ann
x TyVarDecl tyname ann
dataDecl [TyVarDecl tyname ann]
params name
matchName [VarDecl tyname name uni ann]
constrs) = do
Restorer m
restorerBeforeData <- ContT c m (Restorer m)
forall ren (m :: * -> *) c.
MonadReader ren m =>
ContT c m (Restorer m)
captureContext
TyVarDecl tyname ann
dataDeclFr <- ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann))
-> ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall a b. (a -> b) -> a -> b
$ TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
dataDecl
Restorer m
restorerAfterData <- ContT c m (Restorer m)
forall ren (m :: * -> *) c.
MonadReader ren m =>
ContT c m (Restorer m)
captureContext
[m (VarDecl tyname name uni ann)]
constrsRen <- (VarDecl tyname name uni ann
-> ContT c m (m (VarDecl tyname name uni ann)))
-> [VarDecl tyname name uni ann]
-> ContT c m [m (VarDecl tyname name 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 (Restorer m
-> VarDecl tyname name uni ann
-> ContT c m (m (VarDecl tyname name uni ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Restorer m
-> VarDecl tyname name uni ann
-> ContT c m (m (VarDecl tyname name uni ann))
renameConstrCM Restorer m
restorerAfterData) [VarDecl tyname name uni ann]
constrs
name
matchNameFr <- ((name -> m c) -> m c) -> ContT c m name
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((name -> m c) -> m c) -> ContT c m name)
-> ((name -> m c) -> m c) -> ContT c m name
forall a b. (a -> b) -> a -> b
$ name -> (name -> m c) -> m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
matchName
m (Datatype tyname name uni ann)
-> ContT c m (m (Datatype tyname name uni ann))
forall a. a -> ContT c m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Datatype tyname name uni ann)
-> ContT c m (m (Datatype tyname name uni ann)))
-> (m (Datatype tyname name uni ann)
-> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann)
-> ContT c m (m (Datatype tyname name uni ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Recursivity
-> (m (Datatype tyname name uni ann)
-> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann)
-> m (Datatype tyname name uni ann)
forall a. Recursivity -> (a -> a) -> a -> a
onNonRec Recursivity
recy (Restorer m -> forall a. m a -> m a
forall (m :: * -> *). Restorer m -> forall a. m a -> m a
unRestorer Restorer m
restorerBeforeData) (m (Datatype tyname name uni ann)
-> ContT c m (m (Datatype tyname name uni ann)))
-> m (Datatype tyname name uni ann)
-> ContT c m (m (Datatype tyname name uni ann))
forall a b. (a -> b) -> a -> b
$
ContT (Datatype tyname name uni ann) m [TyVarDecl tyname ann]
-> ([TyVarDecl tyname ann] -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann)
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT ((TyVarDecl tyname ann
-> ContT (Datatype tyname name uni ann) m (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> ContT (Datatype tyname name uni ann) m [TyVarDecl tyname 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 (((TyVarDecl tyname ann -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann))
-> ContT (Datatype tyname name uni ann) m (TyVarDecl tyname ann)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann))
-> ContT (Datatype tyname name uni ann) m (TyVarDecl tyname ann))
-> (TyVarDecl tyname ann
-> (TyVarDecl tyname ann -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann))
-> TyVarDecl tyname ann
-> ContT (Datatype tyname name uni ann) m (TyVarDecl tyname ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl tyname ann
-> (TyVarDecl tyname ann -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl) [TyVarDecl tyname ann]
params) (([TyVarDecl tyname ann] -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann))
-> ([TyVarDecl tyname ann] -> m (Datatype tyname name uni ann))
-> m (Datatype tyname name uni ann)
forall a b. (a -> b) -> a -> b
$ \[TyVarDecl tyname ann]
paramsFr ->
ann
-> TyVarDecl tyname ann
-> [TyVarDecl tyname ann]
-> name
-> [VarDecl tyname name uni ann]
-> Datatype tyname name uni ann
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype ann
x TyVarDecl tyname ann
dataDeclFr [TyVarDecl tyname ann]
paramsFr name
matchNameFr ([VarDecl tyname name uni ann] -> Datatype tyname name uni ann)
-> m [VarDecl tyname name uni ann]
-> m (Datatype tyname name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m (VarDecl tyname name uni ann)]
-> m [VarDecl tyname name uni ann]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [m (VarDecl tyname name uni ann)]
constrsRen
renameBindingNonRecC
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
renameBindingNonRecC :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
renameBindingNonRecC Binding tyname name uni fun ann
binding = ((Binding tyname name uni fun ann -> m c) -> m c)
-> ContT c m (Binding tyname name uni fun ann)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((Binding tyname name uni fun ann -> m c) -> m c)
-> ContT c m (Binding tyname name uni fun ann))
-> ((Binding tyname name uni fun ann -> m c) -> m c)
-> ContT c m (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \Binding tyname name uni fun ann -> m c
cont -> case Binding tyname name uni fun ann
binding of
TermBind ann
x Strictness
s VarDecl tyname name uni ann
var Term tyname name uni fun ann
term -> do
Term tyname name uni fun ann
termFr <- Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
VarDecl tyname name uni ann
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
forall tyname name (uni :: * -> *) fun ann (m :: * -> *) c.
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
MonadReader ScopedRenaming m) =>
VarDecl tyname name uni ann
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
PLC.withFreshenedVarDecl VarDecl tyname name uni ann
var ((m (VarDecl tyname name uni ann) -> m c) -> m c)
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \m (VarDecl tyname name uni ann)
varRen -> do
VarDecl tyname name uni ann
varFr <- m (VarDecl tyname name uni ann)
varRen
Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> Binding tyname name uni fun ann -> m c
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
s VarDecl tyname name uni ann
varFr Term tyname name uni fun ann
termFr
TypeBind ann
x TyVarDecl tyname ann
var Type tyname uni ann
ty -> do
Type tyname uni ann
tyFr <- Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
var ((TyVarDecl tyname ann -> m c) -> m c)
-> (TyVarDecl tyname ann -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \TyVarDecl tyname ann
varFr ->
Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> Binding tyname name uni fun ann -> m c
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
varFr Type tyname uni ann
tyFr
DatatypeBind ann
x Datatype tyname name uni ann
datatype -> do
ContT c m (m (Datatype tyname name uni ann))
-> (m (Datatype tyname name uni ann) -> m c) -> m c
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT (Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
renameDatatypeCM Recursivity
NonRec Datatype tyname name uni ann
datatype) ((m (Datatype tyname name uni ann) -> m c) -> m c)
-> (m (Datatype tyname name uni ann) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \m (Datatype tyname name uni ann)
datatypeRen ->
m (Datatype tyname name uni ann)
datatypeRen m (Datatype tyname name uni ann)
-> (Datatype tyname name uni ann -> m c) -> m c
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> (Datatype tyname name uni ann
-> Binding tyname name uni fun ann)
-> Datatype tyname name uni ann
-> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Datatype tyname name uni ann -> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind ann
x
renameBindingRecCM
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM = \case
TermBind ann
x Strictness
s VarDecl tyname name uni ann
var Term tyname name uni fun ann
term -> do
m (VarDecl tyname name uni ann)
varRen <- ((m (VarDecl tyname name uni ann) -> m c) -> m c)
-> ContT c m (m (VarDecl tyname name uni ann))
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((m (VarDecl tyname name uni ann) -> m c) -> m c)
-> ContT c m (m (VarDecl tyname name uni ann)))
-> ((m (VarDecl tyname name uni ann) -> m c) -> m c)
-> ContT c m (m (VarDecl tyname name uni ann))
forall a b. (a -> b) -> a -> b
$ VarDecl tyname name uni ann
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
forall tyname name (uni :: * -> *) fun ann (m :: * -> *) c.
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
MonadReader ScopedRenaming m) =>
VarDecl tyname name uni ann
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
PLC.withFreshenedVarDecl VarDecl tyname name uni ann
var
m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a. a -> ContT c m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
s (VarDecl tyname name uni ann
-> Term tyname name uni fun ann -> Binding tyname name uni fun ann)
-> m (VarDecl tyname name uni ann)
-> m (Term tyname name uni fun ann
-> Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (VarDecl tyname name uni ann)
varRen m (Term tyname name uni fun ann -> Binding tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Binding tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
TypeBind ann
x TyVarDecl tyname ann
var Type tyname uni ann
ty -> do
TyVarDecl tyname ann
varFr <- ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann))
-> ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall a b. (a -> b) -> a -> b
$ TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
var
m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a. a -> ContT c m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
varFr (Type tyname uni ann -> Binding tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
DatatypeBind ann
x Datatype tyname name uni ann
datatype -> do
m (Datatype tyname name uni ann)
datatypeRen <- Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> Datatype tyname name uni ann
-> ContT c m (m (Datatype tyname name uni ann))
renameDatatypeCM Recursivity
Rec Datatype tyname name uni ann
datatype
m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a. a -> ContT c m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> Datatype tyname name uni ann -> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind ann
x (Datatype tyname name uni ann -> Binding tyname name uni fun ann)
-> m (Datatype tyname name uni ann)
-> m (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Datatype tyname name uni ann)
datatypeRen
withFreshenedBindings
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> m c
withFreshenedBindings :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> m c
withFreshenedBindings Recursivity
recy NonEmpty (Binding tyname name uni fun ann)
binds NonEmpty (Binding tyname name uni fun ann) -> m c
cont = case Recursivity
recy of
Recursivity
NonRec -> ContT c m (NonEmpty (Binding tyname name uni fun ann))
-> (NonEmpty (Binding tyname name uni fun ann) -> m c) -> m c
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT ((Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> ContT c m (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
renameBindingNonRecC NonEmpty (Binding tyname name uni fun ann)
binds) NonEmpty (Binding tyname name uni fun ann) -> m c
cont
Recursivity
Rec -> ContT c m (NonEmpty (m (Binding tyname name uni fun ann)))
-> (NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT ((Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann)))
-> NonEmpty (Binding tyname name uni fun ann)
-> ContT c m (NonEmpty (m (Binding tyname name uni fun ann)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM NonEmpty (Binding tyname name uni fun ann)
binds) ((NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c)
-> (NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ NonEmpty (m (Binding tyname name uni fun ann))
-> m (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => NonEmpty (m a) -> m (NonEmpty a)
sequence (NonEmpty (m (Binding tyname name uni fun ann))
-> m (NonEmpty (Binding tyname name uni fun ann)))
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> NonEmpty (m (Binding tyname name uni fun ann))
-> m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> NonEmpty (Binding tyname name uni fun ann) -> m c
cont
renameTermM
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM = \case
Let ann
x Recursivity
r NonEmpty (Binding tyname name uni fun ann)
binds Term tyname name uni fun ann
term ->
Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann)
-> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> m c
withFreshenedBindings Recursivity
r NonEmpty (Binding tyname name uni fun ann)
binds ((NonEmpty (Binding tyname name uni fun ann)
-> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann))
-> (NonEmpty (Binding tyname name uni fun ann)
-> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \NonEmpty (Binding tyname name uni fun ann)
bindsFr ->
ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
r NonEmpty (Binding tyname name uni fun ann)
bindsFr (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
Var ann
x name
name ->
ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var ann
x (name -> Term tyname name uni fun ann)
-> m name -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> m name
forall ren unique name (m :: * -> *).
(HasRenaming ren unique, HasUnique name unique,
MonadReader ren m) =>
name -> m name
PLC.renameNameM name
name
TyAbs ann
x tyname
name Kind ann
kind Term tyname name uni fun ann
body ->
tyname
-> (tyname -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName tyname
name ((tyname -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann))
-> (tyname -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \tyname
nameFr ->
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs ann
x tyname
nameFr Kind ann
kind (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
LamAbs ann
x name
name Type tyname uni ann
ty Term tyname name uni fun ann
body ->
name
-> (name -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
name ((name -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann))
-> (name -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \name
nameFr ->
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ann
x name
nameFr (Type tyname uni ann
-> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
Apply ann
x Term tyname name uni fun ann
fun Term tyname name uni fun ann
arg ->
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply ann
x (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)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
fun m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
arg
Constant ann
x Some (ValueOf uni)
con ->
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant ann
x Some (ValueOf uni)
con
Builtin ann
x fun
bi ->
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 a b. (a -> b) -> a -> b
$ ann -> fun -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin ann
x fun
bi
TyInst ann
x Term tyname name uni fun ann
term 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 a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst ann
x (Term tyname name uni fun ann
-> Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Type tyname uni ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term m (Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
Error ann
x Type tyname uni ann
ty ->
ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error ann
x (Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
IWrap ann
x Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term ->
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 a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap ann
x (Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann
-> Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
pat m (Type tyname uni ann
-> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
arg m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
Unwrap ann
x Term tyname name uni fun ann
term ->
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap ann
x (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
Constr ann
x 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 a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr ann
x (Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Word64
-> [Term tyname name uni fun ann] -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty m (Word64
-> [Term tyname name uni fun ann] -> Term tyname name uni fun ann)
-> m Word64
-> m ([Term tyname name uni fun ann]
-> Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> m Word64
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i m ([Term tyname name uni fun ann] -> Term tyname name uni fun ann)
-> m [Term tyname name uni fun ann]
-> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM [Term tyname name uni fun ann]
es
Case ann
x 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 a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case ann
x (Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Term tyname name uni fun ann
-> [Term tyname name uni fun ann] -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty m (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)
-> m ([Term tyname name uni fun ann]
-> Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
arg m ([Term tyname name uni fun ann] -> Term tyname name uni fun ann)
-> m [Term tyname name uni fun ann]
-> m (Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM [Term tyname name uni fun ann]
cs
renameProgramM
:: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
=> Program tyname name uni fun ann -> m (Program tyname name uni fun ann)
renameProgramM :: forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
renameProgramM (Program ann
ann 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
ann Version
v (Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Program tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term