{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PlutusIR.TypeCheck (
BuiltinTypes (..),
PirTCConfig (..),
tccBuiltinTypes,
getDefTypeCheckConfig,
inferType,
checkType,
inferTypeOfProgram,
checkTypeOfProgram,
MonadTypeCheckPir,
) where
import PlutusCore.Rename
import PlutusCore.TypeCheck qualified as PLC
import PlutusIR
import PlutusIR.Error
import PlutusIR.Transform.Rename ()
import PlutusIR.TypeCheck.Internal
import Control.Monad ((>=>))
getDefTypeCheckConfig ::
(MonadKindCheck err term uni fun ann m, PLC.Typecheckable uni fun) =>
ann ->
m (PirTCConfig uni fun)
getDefTypeCheckConfig :: forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (PirTCConfig uni fun)
getDefTypeCheckConfig ann
ann = do
TypeCheckConfig uni fun
configPlc <- ann -> m (TypeCheckConfig uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
PLC.getDefTypeCheckConfig ann
ann
PirTCConfig uni fun -> m (PirTCConfig uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PirTCConfig uni fun -> m (PirTCConfig uni fun))
-> PirTCConfig uni fun -> m (PirTCConfig uni fun)
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig uni fun -> AllowEscape -> PirTCConfig uni fun
forall (uni :: * -> *) fun.
TypeCheckConfig uni fun -> AllowEscape -> PirTCConfig uni fun
PirTCConfig TypeCheckConfig uni fun
configPlc AllowEscape
YesEscape
inferType ::
(MonadTypeCheckPir err uni fun ann m) =>
PirTCConfig uni fun ->
Term TyName Name uni fun ann ->
m (Normalized (Type TyName uni ()))
inferType :: forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferType PirTCConfig uni fun
config = 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)
rename (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> (Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ())))
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> PirTCConfig uni fun
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
-> m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun (m :: * -> *) a.
PirTCConfig uni fun -> PirTCEnv uni fun m a -> m a
runTypeCheckM PirTCConfig uni fun
config (PirTCEnv uni fun m (Normalized (Type TyName uni ()))
-> m (Normalized (Type TyName uni ())))
-> (Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM
checkType ::
(MonadTypeCheckPir err uni fun ann m) =>
PirTCConfig uni fun ->
ann ->
Term TyName Name uni fun ann ->
Normalized (Type TyName uni ()) ->
m ()
checkType :: forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType PirTCConfig uni fun
config ann
ann Term TyName Name uni fun ann
term Normalized (Type TyName uni ())
ty = do
Term TyName Name uni fun ann
termRen <- 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)
rename Term TyName Name uni fun ann
term
PirTCConfig uni fun -> PirTCEnv uni fun m () -> m ()
forall (uni :: * -> *) fun (m :: * -> *) a.
PirTCConfig uni fun -> PirTCEnv uni fun m a -> m a
runTypeCheckM PirTCConfig uni fun
config (PirTCEnv uni fun m () -> m ()) -> PirTCEnv uni fun m () -> m ()
forall a b. (a -> b) -> a -> b
$ ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
termRen Normalized (Type TyName uni ())
ty
inferTypeOfProgram ::
(MonadTypeCheckPir err uni fun ann m) =>
PirTCConfig uni fun ->
Program TyName Name uni fun ann ->
m (Normalized (Type TyName uni ()))
inferTypeOfProgram :: forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> Program TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferTypeOfProgram PirTCConfig uni fun
config (Program ann
_ Version
_ Term TyName Name uni fun ann
term) = PirTCConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferType PirTCConfig uni fun
config Term TyName Name uni fun ann
term
checkTypeOfProgram ::
(MonadTypeCheckPir err uni fun ann m) =>
PirTCConfig uni fun ->
ann ->
Program TyName Name uni fun ann ->
Normalized (Type TyName uni ()) ->
m ()
checkTypeOfProgram :: forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> ann
-> Program TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkTypeOfProgram PirTCConfig uni fun
config ann
ann (Program ann
_ Version
_ Term TyName Name uni fun ann
term) = PirTCConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType PirTCConfig uni fun
config ann
ann Term TyName Name uni fun ann
term