{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}

-- | This module makes sure types are normalized inside programs.
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 (..))

-- | Ensure that all types in the 'Program' are normalized.
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

-- | Ensure that all types in the 'Term' are normalized.
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")

-- See Note [Normalization of built-in types].
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
    -- If @uni@ is not an intra-universe application, then it's neutral.
    (() -> Either (NormCheckError tyname name uni fun ann) ()
forall a b. b -> Either a b
Right ())
    -- If it is, then it's not neutral and we throw an error.
    (\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"))