{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module PlutusCore.Check.Normal
( checkProgram
, checkTerm
, isNormalType
, NormCheckError (..)
) where
import PlutusPrelude
import PlutusCore.Core
import PlutusCore.Error
import PlutusCore.MkPlc (mkTyBuiltinOf)
import Control.Monad.Except
import Universe.Core (HasUniApply (matchUniApply), SomeTypeIn (..))
checkProgram
:: (AsNormCheckError e tyname name uni fun ann, HasUniApply uni, MonadError e m)
=> Program tyname name uni fun ann -> m ()
checkProgram :: forall e tyname name (uni :: * -> *) fun ann (m :: * -> *).
(AsNormCheckError e tyname name uni fun ann, HasUniApply uni,
MonadError e m) =>
Program tyname name uni fun ann -> m ()
checkProgram (Program ann
_ Version
_ Term tyname name uni fun ann
t) = Term tyname name uni fun ann -> m ()
forall e tyname name (uni :: * -> *) fun ann (m :: * -> *).
(AsNormCheckError e tyname name uni fun ann, HasUniApply uni,
MonadError e m) =>
Term tyname name uni fun ann -> m ()
checkTerm Term tyname name uni fun ann
t
checkTerm
:: (AsNormCheckError e tyname name uni fun ann, HasUniApply uni, MonadError e m)
=> Term tyname name uni fun ann -> m ()
checkTerm :: forall e tyname name (uni :: * -> *) fun ann (m :: * -> *).
(AsNormCheckError e tyname name uni fun ann, HasUniApply uni,
MonadError e m) =>
Term tyname name uni fun ann -> m ()
checkTerm Term tyname name uni fun ann
p = AReview e (NormCheckError tyname name uni fun ann)
-> Either (NormCheckError tyname name uni fun ann) () -> m ()
forall e (m :: * -> *) t a.
MonadError e m =>
AReview e t -> Either t a -> m a
throwingEither AReview e (NormCheckError tyname name uni fun ann)
forall r tyname name (uni :: * -> *) fun ann.
AsNormCheckError r tyname name uni fun ann =>
Prism' r (NormCheckError tyname name uni fun ann)
Prism' e (NormCheckError tyname name uni fun ann)
_NormCheckError (Either (NormCheckError tyname name uni fun ann) () -> m ())
-> Either (NormCheckError tyname name uni fun ann) () -> m ()
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
p
check
:: HasUniApply uni
=> Term tyname name uni fun ann -> Either (NormCheckError tyname name uni fun ann) ()
check :: forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check (Error ann
_ Type tyname uni ann
ty) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty
check (TyInst ann
_ Term tyname name uni fun ann
t Type tyname uni ann
ty) = Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty
check (IWrap ann
_ Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
pat Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
arg Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
term
check (Unwrap ann
_ Term tyname name uni fun ann
t) = Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t
check (LamAbs ann
_ name
_ Type tyname uni ann
ty Term tyname name uni fun ann
t) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t
check (Apply ann
_ Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2) = Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t1 Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t2
check (TyAbs ann
_ tyname
_ Kind ann
_ Term tyname name uni fun ann
t) = Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
t
check (Constr ann
_ Type tyname uni ann
ty Word64
_ [Term tyname name uni fun ann]
es) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ())
-> [Term tyname name uni fun ann]
-> Either (NormCheckError tyname name uni fun ann) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check [Term tyname name uni fun ann]
es
check (Case ann
_ Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check Term tyname name uni fun ann
arg Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ())
-> [Term tyname name uni fun ann]
-> Either (NormCheckError tyname name uni fun ann) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname name fun ann.
HasUniApply uni =>
Term tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
check [Term tyname name uni fun ann]
cs
check Var{} = () -> Either (NormCheckError tyname name uni fun ann) ()
forall a. a -> Either (NormCheckError tyname name uni fun ann) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
check Constant{} = () -> Either (NormCheckError tyname name uni fun ann) ()
forall a. a -> Either (NormCheckError tyname name uni fun ann) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
check Builtin{} = () -> Either (NormCheckError tyname name uni fun ann) ()
forall a. a -> Either (NormCheckError tyname name uni fun ann) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
isNormalType :: HasUniApply uni => Type tyname uni ann -> Bool
isNormalType :: forall (uni :: * -> *) tyname ann.
HasUniApply uni =>
Type tyname uni ann -> Bool
isNormalType = Either (NormCheckError tyname Any uni Any ann) () -> Bool
forall a b. Either a b -> Bool
isRight (Either (NormCheckError tyname Any uni Any ann) () -> Bool)
-> (Type tyname uni ann
-> Either (NormCheckError tyname Any uni Any ann) ())
-> Type tyname uni ann
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> Either (NormCheckError tyname Any uni Any ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType
normalType
:: HasUniApply uni
=> Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) ()
normalType :: forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType (TyFun ann
_ Type tyname uni ann
i Type tyname uni ann
o) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
i Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
o
normalType (TyForall ann
_ tyname
_ Kind ann
_ Type tyname uni ann
ty) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty
normalType (TyIFix ann
_ Type tyname uni ann
pat Type tyname uni ann
arg) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
pat Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
arg
normalType (TySOP ann
_ [[Type tyname uni ann]]
tyls) = ([Type tyname uni ann]
-> Either (NormCheckError tyname name uni fun ann) ())
-> [[Type tyname uni ann]]
-> Either (NormCheckError tyname name uni fun ann) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ())
-> [Type tyname uni ann]
-> Either (NormCheckError tyname name uni fun ann) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType) [[Type tyname uni ann]]
tyls
normalType (TyLam ann
_ tyname
_ Kind ann
_ Type tyname uni ann
ty) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty
normalType Type tyname uni ann
ty = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
neutralType Type tyname uni ann
ty
neutralType
:: HasUniApply uni
=> Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) ()
neutralType :: forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
neutralType TyVar{} = () -> Either (NormCheckError tyname name uni fun ann) ()
forall a. a -> Either (NormCheckError tyname name uni fun ann) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
neutralType (TyBuiltin ann
ann SomeTypeIn uni
someUni) = ann
-> SomeTypeIn uni
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) ann tyname name fun.
HasUniApply uni =>
ann
-> SomeTypeIn uni
-> Either (NormCheckError tyname name uni fun ann) ()
neutralUni ann
ann SomeTypeIn uni
someUni
neutralType (TyApp ann
_ Type tyname uni ann
ty1 Type tyname uni ann
ty2) = Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
neutralType Type tyname uni ann
ty1 Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b.
Either (NormCheckError tyname name uni fun ann) a
-> Either (NormCheckError tyname name uni fun ann) b
-> Either (NormCheckError tyname name uni fun ann) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall (uni :: * -> *) tyname ann name fun.
HasUniApply uni =>
Type tyname uni ann
-> Either (NormCheckError tyname name uni fun ann) ()
normalType Type tyname uni ann
ty2
neutralType Type tyname uni ann
ty = NormCheckError tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b. a -> Either a b
Left (ann
-> Type tyname uni ann
-> Text
-> NormCheckError tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Text
-> NormCheckError tyname name uni fun ann
BadType (Type tyname uni ann -> ann
forall tyname (uni :: * -> *) ann. Type tyname uni ann -> ann
typeAnn Type tyname uni ann
ty) Type tyname uni ann
ty Text
"neutral type")
neutralUni
:: HasUniApply uni
=> ann -> SomeTypeIn uni -> Either (NormCheckError tyname name uni fun ann) ()
neutralUni :: forall (uni :: * -> *) ann tyname name fun.
HasUniApply uni =>
ann
-> SomeTypeIn uni
-> Either (NormCheckError tyname name uni fun ann) ()
neutralUni ann
ann (SomeTypeIn uni (Esc a)
uni) =
uni (Esc a)
-> Either (NormCheckError tyname name uni fun ann) ()
-> (forall k l (f :: k -> l) (a :: k).
(Esc a ~ Esc (f a)) =>
uni (Esc f)
-> uni (Esc a)
-> Either (NormCheckError tyname name uni fun ann) ())
-> Either (NormCheckError tyname name uni fun ann) ()
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
(() -> Either (NormCheckError tyname name uni fun ann) ()
forall a b. b -> Either a b
Right ())
(\uni (Esc f)
_ uni (Esc a)
_ -> NormCheckError tyname name uni fun ann
-> Either (NormCheckError tyname name uni fun ann) ()
forall a b. a -> Either a b
Left (ann
-> Type tyname uni ann
-> Text
-> NormCheckError tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Text
-> NormCheckError tyname name uni fun ann
BadType ann
ann (ann -> uni (Esc a) -> Type tyname uni ann
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf ann
ann uni (Esc a)
uni) Text
"neutral type"))