-- editorconfig-checker-disable-file
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE DerivingVia              #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PatternSynonyms          #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell          #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE UndecidableInstances     #-}

-- We rely on things from this module being lazy (e.g. the PIR generators rely on types being lazy),
-- so don't use @StrictData@ in this module.

module PlutusCore.Core.Type
    ( Kind (..)
    , toPatFuncKind
    , fromPatFuncKind
    , argsFunKind
    , Type (..)
    , splitFunTyParts
    , funTyArgs
    , funTyResultType
    , Term (..)
    , Program (..)
    , HasTermLevel
    , UniOf
    , Normalized (..)
    , TyVarDecl (..)
    , VarDecl (..)
    , TyDecl (..)
    , tyDeclVar
    , HasUniques
    , Binder (..)
    , module Export
    -- * Helper functions
    , termAnn
    , typeAnn
    , mapFun
    , tyVarDeclAnn
    , tyVarDeclName
    , tyVarDeclKind
    , varDeclAnn
    , varDeclName
    , varDeclType
    , tyDeclAnn
    , tyDeclType
    , tyDeclKind
    , progAnn
    , progVer
    , progTerm
    )
where

import PlutusPrelude

import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Name.Unique
import PlutusCore.Version as Export

import Control.Lens
import Data.Hashable
import Data.Kind qualified as GHC
import Data.List.NonEmpty qualified as NE
import Data.Word
import Instances.TH.Lift ()
import Language.Haskell.TH.Lift
import Universe

data Kind ann
    = Type ann
    | KindArrow ann (Kind ann) (Kind ann)
    deriving stock (Kind ann -> Kind ann -> Bool
(Kind ann -> Kind ann -> Bool)
-> (Kind ann -> Kind ann -> Bool) -> Eq (Kind ann)
forall ann. Eq ann => Kind ann -> Kind ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall ann. Eq ann => Kind ann -> Kind ann -> Bool
== :: Kind ann -> Kind ann -> Bool
$c/= :: forall ann. Eq ann => Kind ann -> Kind ann -> Bool
/= :: Kind ann -> Kind ann -> Bool
Eq, Int -> Kind ann -> ShowS
[Kind ann] -> ShowS
Kind ann -> String
(Int -> Kind ann -> ShowS)
-> (Kind ann -> String) -> ([Kind ann] -> ShowS) -> Show (Kind ann)
forall ann. Show ann => Int -> Kind ann -> ShowS
forall ann. Show ann => [Kind ann] -> ShowS
forall ann. Show ann => Kind ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ann. Show ann => Int -> Kind ann -> ShowS
showsPrec :: Int -> Kind ann -> ShowS
$cshow :: forall ann. Show ann => Kind ann -> String
show :: Kind ann -> String
$cshowList :: forall ann. Show ann => [Kind ann] -> ShowS
showList :: [Kind ann] -> ShowS
Show, (forall a b. (a -> b) -> Kind a -> Kind b)
-> (forall a b. a -> Kind b -> Kind a) -> Functor Kind
forall a b. a -> Kind b -> Kind a
forall a b. (a -> b) -> Kind a -> Kind b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Kind a -> Kind b
fmap :: forall a b. (a -> b) -> Kind a -> Kind b
$c<$ :: forall a b. a -> Kind b -> Kind a
<$ :: forall a b. a -> Kind b -> Kind a
Functor, (forall x. Kind ann -> Rep (Kind ann) x)
-> (forall x. Rep (Kind ann) x -> Kind ann) -> Generic (Kind ann)
forall x. Rep (Kind ann) x -> Kind ann
forall x. Kind ann -> Rep (Kind ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ann x. Rep (Kind ann) x -> Kind ann
forall ann x. Kind ann -> Rep (Kind ann) x
$cfrom :: forall ann x. Kind ann -> Rep (Kind ann) x
from :: forall x. Kind ann -> Rep (Kind ann) x
$cto :: forall ann x. Rep (Kind ann) x -> Kind ann
to :: forall x. Rep (Kind ann) x -> Kind ann
Generic, (forall (m :: * -> *). Quote m => Kind ann -> m Exp)
-> (forall (m :: * -> *). Quote m => Kind ann -> Code m (Kind ann))
-> Lift (Kind ann)
forall ann (m :: * -> *). (Lift ann, Quote m) => Kind ann -> m Exp
forall ann (m :: * -> *).
(Lift ann, Quote m) =>
Kind ann -> Code m (Kind ann)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Kind ann -> m Exp
forall (m :: * -> *). Quote m => Kind ann -> Code m (Kind ann)
$clift :: forall ann (m :: * -> *). (Lift ann, Quote m) => Kind ann -> m Exp
lift :: forall (m :: * -> *). Quote m => Kind ann -> m Exp
$cliftTyped :: forall ann (m :: * -> *).
(Lift ann, Quote m) =>
Kind ann -> Code m (Kind ann)
liftTyped :: forall (m :: * -> *). Quote m => Kind ann -> Code m (Kind ann)
Lift)
    deriving anyclass (Kind ann -> ()
(Kind ann -> ()) -> NFData (Kind ann)
forall ann. NFData ann => Kind ann -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall ann. NFData ann => Kind ann -> ()
rnf :: Kind ann -> ()
NFData, Eq (Kind ann)
Eq (Kind ann) =>
(Int -> Kind ann -> Int)
-> (Kind ann -> Int) -> Hashable (Kind ann)
Int -> Kind ann -> Int
Kind ann -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall ann. Hashable ann => Eq (Kind ann)
forall ann. Hashable ann => Int -> Kind ann -> Int
forall ann. Hashable ann => Kind ann -> Int
$chashWithSalt :: forall ann. Hashable ann => Int -> Kind ann -> Int
hashWithSalt :: Int -> Kind ann -> Int
$chash :: forall ann. Hashable ann => Kind ann -> Int
hash :: Kind ann -> Int
Hashable)

-- | The kind of a pattern functor (the first 'Type' argument of 'TyIFix') at a given kind (of the
-- second 'Type' argument of 'TyIFix'):
--
-- > toPatFuncKind k = (k -> *) -> k -> *
toPatFuncKind :: Kind () -> Kind ()
toPatFuncKind :: Kind () -> Kind ()
toPatFuncKind Kind ()
k = () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))

fromPatFuncKind :: Kind () -> Maybe (Kind ())
fromPatFuncKind :: Kind () -> Maybe (Kind ())
fromPatFuncKind (KindArrow () (KindArrow () Kind ()
k1 (Type ())) (KindArrow () Kind ()
k2 (Type ())))
    | Kind ()
k1 Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k2 = Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
Just Kind ()
k1
fromPatFuncKind Kind ()
_ = Maybe (Kind ())
forall a. Maybe a
Nothing

-- | Extract all @a_i@ from @a_0 -> a_1 -> ... -> r@.
argsFunKind :: Kind ann -> [Kind ann]
argsFunKind :: forall ann. Kind ann -> [Kind ann]
argsFunKind Type{}            = []
argsFunKind (KindArrow ann
_ Kind ann
k Kind ann
l) = Kind ann
k Kind ann -> [Kind ann] -> [Kind ann]
forall a. a -> [a] -> [a]
: Kind ann -> [Kind ann]
forall ann. Kind ann -> [Kind ann]
argsFunKind Kind ann
l

-- | A 'Type' assigned to expressions.
type Type :: GHC.Type -> (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Type
data Type tyname uni ann
    = TyVar ann tyname -- ^ Type variable
    | TyFun ann (Type tyname uni ann) (Type tyname uni ann) -- ^ Function type
    | TyIFix ann (Type tyname uni ann) (Type tyname uni ann)
      -- ^ Fix-point type, for constructing self-recursive types
    | TyForall ann tyname (Kind ann) (Type tyname uni ann) -- ^ Polymorphic type
    | TyBuiltin ann (SomeTypeIn uni) -- ^ Builtin type
    | TyLam ann tyname (Kind ann) (Type tyname uni ann) -- ^ Type lambda
    | TyApp ann (Type tyname uni ann) (Type tyname uni ann) -- ^ Type application
    | TySOP ann [[Type tyname uni ann]] -- ^ Sum-of-products type
    deriving stock (Int -> Type tyname uni ann -> ShowS
[Type tyname uni ann] -> ShowS
Type tyname uni ann -> String
(Int -> Type tyname uni ann -> ShowS)
-> (Type tyname uni ann -> String)
-> ([Type tyname uni ann] -> ShowS)
-> Show (Type tyname uni ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
Int -> Type tyname uni ann -> ShowS
forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
[Type tyname uni ann] -> ShowS
forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
Type tyname uni ann -> String
$cshowsPrec :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
Int -> Type tyname uni ann -> ShowS
showsPrec :: Int -> Type tyname uni ann -> ShowS
$cshow :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
Type tyname uni ann -> String
show :: Type tyname uni ann -> String
$cshowList :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show tyname, Show ann) =>
[Type tyname uni ann] -> ShowS
showList :: [Type tyname uni ann] -> ShowS
Show, (forall a b. (a -> b) -> Type tyname uni a -> Type tyname uni b)
-> (forall a b. a -> Type tyname uni b -> Type tyname uni a)
-> Functor (Type tyname uni)
forall a b. a -> Type tyname uni b -> Type tyname uni a
forall a b. (a -> b) -> Type tyname uni a -> Type tyname uni b
forall tyname (uni :: * -> *) a b.
a -> Type tyname uni b -> Type tyname uni a
forall tyname (uni :: * -> *) a b.
(a -> b) -> Type tyname uni a -> Type tyname uni b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname (uni :: * -> *) a b.
(a -> b) -> Type tyname uni a -> Type tyname uni b
fmap :: forall a b. (a -> b) -> Type tyname uni a -> Type tyname uni b
$c<$ :: forall tyname (uni :: * -> *) a b.
a -> Type tyname uni b -> Type tyname uni a
<$ :: forall a b. a -> Type tyname uni b -> Type tyname uni a
Functor, (forall x. Type tyname uni ann -> Rep (Type tyname uni ann) x)
-> (forall x. Rep (Type tyname uni ann) x -> Type tyname uni ann)
-> Generic (Type tyname uni ann)
forall x. Rep (Type tyname uni ann) x -> Type tyname uni ann
forall x. Type tyname uni ann -> Rep (Type tyname uni ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname (uni :: * -> *) ann x.
Rep (Type tyname uni ann) x -> Type tyname uni ann
forall tyname (uni :: * -> *) ann x.
Type tyname uni ann -> Rep (Type tyname uni ann) x
$cfrom :: forall tyname (uni :: * -> *) ann x.
Type tyname uni ann -> Rep (Type tyname uni ann) x
from :: forall x. Type tyname uni ann -> Rep (Type tyname uni ann) x
$cto :: forall tyname (uni :: * -> *) ann x.
Rep (Type tyname uni ann) x -> Type tyname uni ann
to :: forall x. Rep (Type tyname uni ann) x -> Type tyname uni ann
Generic)
    deriving anyclass (Type tyname uni ann -> ()
(Type tyname uni ann -> ()) -> NFData (Type tyname uni ann)
forall a. (a -> ()) -> NFData a
forall tyname (uni :: * -> *) ann.
(NFData ann, NFData tyname, Closed uni) =>
Type tyname uni ann -> ()
$crnf :: forall tyname (uni :: * -> *) ann.
(NFData ann, NFData tyname, Closed uni) =>
Type tyname uni ann -> ()
rnf :: Type tyname uni ann -> ()
NFData)

-- | Get recursively all the domains and codomains of a type.
-- @splitFunTyParts (A->B->C) = [A, B, C]@
-- @splitFunTyParts (X) = [X]@
splitFunTyParts :: Type tyname uni a -> NE.NonEmpty (Type tyname uni a)
splitFunTyParts :: forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
splitFunTyParts = \case
    TyFun a
_ Type tyname uni a
t1 Type tyname uni a
t2 -> Type tyname uni a
t1 Type tyname uni a
-> NonEmpty (Type tyname uni a) -> NonEmpty (Type tyname uni a)
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
splitFunTyParts Type tyname uni a
t2
    Type tyname uni a
t             -> Type tyname uni a -> NonEmpty (Type tyname uni a)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
t

-- | Get the argument types of a function type.
-- @funTyArgs (A->B->C) = [A, B]@
funTyArgs :: Type tyname uni a ->  [Type tyname uni a]
funTyArgs :: forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
funTyArgs = NonEmpty (Type tyname uni a) -> [Type tyname uni a]
forall a. NonEmpty a -> [a]
NE.init (NonEmpty (Type tyname uni a) -> [Type tyname uni a])
-> (Type tyname uni a -> NonEmpty (Type tyname uni a))
-> Type tyname uni a
-> [Type tyname uni a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
splitFunTyParts

-- | Get the result type of a function.
-- If not a function, then is the same as `id`
-- @funResultType (A->B->C) = C@
-- @funResultType (X) = X@
funTyResultType :: Type tyname uni a ->  Type tyname uni a
funTyResultType :: forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a
funTyResultType = NonEmpty (Type tyname uni a) -> Type tyname uni a
forall a. NonEmpty a -> a
NE.last (NonEmpty (Type tyname uni a) -> Type tyname uni a)
-> (Type tyname uni a -> NonEmpty (Type tyname uni a))
-> Type tyname uni a
-> Type tyname uni a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
splitFunTyParts

data Term tyname name uni fun ann
    = Var ann name -- ^ a named variable
    | LamAbs ann name (Type tyname uni ann) (Term tyname name uni fun ann) -- ^ lambda abstraction
    | Apply ann (Term tyname name uni fun ann) (Term tyname name uni fun ann) -- ^ application
    | TyAbs ann tyname (Kind ann) (Term tyname name uni fun ann) -- ^ type abstraction
    | TyInst ann (Term tyname name uni fun ann) (Type tyname uni ann) -- ^ instantiation
    | IWrap ann (Type tyname uni ann) (Type tyname uni ann) (Term tyname name uni fun ann) -- ^ wrapping
    | Unwrap ann (Term tyname name uni fun ann) -- ^ unwrapping
    -- See Note [Constr tag type]
    | Constr ann (Type tyname uni ann) Word64 [Term tyname name uni fun ann] -- ^ constructor
    | Case ann (Type tyname uni ann) (Term tyname name uni fun ann) [Term tyname name uni fun ann] -- ^ case
    | Constant ann (Some (ValueOf uni)) -- ^ constants
    | Builtin ann fun -- ^ builtin functions
    | Error ann (Type tyname uni ann) -- ^ fail with error
    deriving stock ((forall a b.
 (a -> b)
 -> Term tyname name uni fun a -> Term tyname name uni fun b)
-> (forall a b.
    a -> Term tyname name uni fun b -> Term tyname name uni fun a)
-> Functor (Term tyname name uni fun)
forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
<$ :: forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
Functor, (forall x.
 Term tyname name uni fun ann
 -> Rep (Term tyname name uni fun ann) x)
-> (forall x.
    Rep (Term tyname name uni fun ann) x
    -> Term tyname name uni fun ann)
-> Generic (Term tyname name uni fun ann)
forall x.
Rep (Term tyname name uni fun ann) x
-> Term tyname name uni fun ann
forall x.
Term tyname name uni fun ann
-> Rep (Term tyname name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun ann x.
Rep (Term tyname name uni fun ann) x
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann x.
Term tyname name uni fun ann
-> Rep (Term tyname name uni fun ann) x
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Term tyname name uni fun ann
-> Rep (Term tyname name uni fun ann) x
from :: forall x.
Term tyname name uni fun ann
-> Rep (Term tyname name uni fun ann) x
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Term tyname name uni fun ann) x
-> Term tyname name uni fun ann
to :: forall x.
Rep (Term tyname name uni fun ann) x
-> Term tyname name uni fun ann
Generic)

deriving stock instance (Show tyname, Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (Term tyname name uni fun ann)

deriving anyclass instance (NFData tyname, NFData name, NFData fun, NFData ann, Everywhere uni NFData, Closed uni)
    => NFData (Term tyname name uni fun ann)

-- See Note [ExMemoryUsage instances for non-constants].
instance ExMemoryUsage (Term tyname name uni fun ann) where
    memoryUsage :: Term tyname name uni fun ann -> CostRose
memoryUsage = String -> Term tyname name uni fun ann -> CostRose
forall a. HasCallStack => String -> a
error String
"Internal error: 'memoryUsage' for Core 'Term' is not supposed to be forced"

-- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language.
data Program tyname name uni fun ann = Program
    { forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> ann
_progAnn  :: ann
    , forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> Version
_progVer  :: Version
    , forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> Term tyname name uni fun ann
_progTerm :: Term tyname name uni fun ann
    }
    deriving stock ((forall a b.
 (a -> b)
 -> Program tyname name uni fun a -> Program tyname name uni fun b)
-> (forall a b.
    a
    -> Program tyname name uni fun b -> Program tyname name uni fun a)
-> Functor (Program tyname name uni fun)
forall a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
forall a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
<$ :: forall a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
Functor, (forall x.
 Program tyname name uni fun ann
 -> Rep (Program tyname name uni fun ann) x)
-> (forall x.
    Rep (Program tyname name uni fun ann) x
    -> Program tyname name uni fun ann)
-> Generic (Program tyname name uni fun ann)
forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
from :: forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
to :: forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
Generic)

makeLenses ''Program

deriving stock instance (Show tyname, Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (Program tyname name uni fun ann)

deriving anyclass instance (NFData tyname, NFData name, Everywhere uni NFData, NFData fun, NFData ann, Closed uni)
    => NFData (Program tyname name uni fun ann)

-- | Specifies that the given type is a built-in one and its values can be embedded into a 'Term'.
type HasTermLevel :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint
type HasTermLevel uni = Includes uni

-- | Extract the universe from a type.
type family UniOf a :: GHC.Type -> GHC.Type

type instance UniOf (Term tyname name uni fun ann) = uni

-- | A "type variable declaration", i.e. a name and a kind for a type variable.
data TyVarDecl tyname ann = TyVarDecl
    { forall tyname ann. TyVarDecl tyname ann -> ann
_tyVarDeclAnn  :: ann
    , forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName :: tyname
    , forall tyname ann. TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind :: Kind ann
    } deriving stock ((forall a b. (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b)
-> (forall a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a)
-> Functor (TyVarDecl tyname)
forall a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a
forall a b. (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
forall tyname a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a
forall tyname a b.
(a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname a b.
(a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
fmap :: forall a b. (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
$c<$ :: forall tyname a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a
<$ :: forall a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a
Functor, Int -> TyVarDecl tyname ann -> ShowS
[TyVarDecl tyname ann] -> ShowS
TyVarDecl tyname ann -> String
(Int -> TyVarDecl tyname ann -> ShowS)
-> (TyVarDecl tyname ann -> String)
-> ([TyVarDecl tyname ann] -> ShowS)
-> Show (TyVarDecl tyname ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname ann.
(Show ann, Show tyname) =>
Int -> TyVarDecl tyname ann -> ShowS
forall tyname ann.
(Show ann, Show tyname) =>
[TyVarDecl tyname ann] -> ShowS
forall tyname ann.
(Show ann, Show tyname) =>
TyVarDecl tyname ann -> String
$cshowsPrec :: forall tyname ann.
(Show ann, Show tyname) =>
Int -> TyVarDecl tyname ann -> ShowS
showsPrec :: Int -> TyVarDecl tyname ann -> ShowS
$cshow :: forall tyname ann.
(Show ann, Show tyname) =>
TyVarDecl tyname ann -> String
show :: TyVarDecl tyname ann -> String
$cshowList :: forall tyname ann.
(Show ann, Show tyname) =>
[TyVarDecl tyname ann] -> ShowS
showList :: [TyVarDecl tyname ann] -> ShowS
Show, (forall x. TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x)
-> (forall x. Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann)
-> Generic (TyVarDecl tyname ann)
forall x. Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann
forall x. TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname ann x.
Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann
forall tyname ann x.
TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x
$cfrom :: forall tyname ann x.
TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x
from :: forall x. TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x
$cto :: forall tyname ann x.
Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann
to :: forall x. Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann
Generic)
makeLenses ''TyVarDecl

-- | A "variable declaration", i.e. a name and a type for a variable.
data VarDecl tyname name uni ann = VarDecl
    { forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> ann
_varDeclAnn  :: ann
    , forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName :: name
    , forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType :: Type tyname uni ann
    } deriving stock ((forall a b.
 (a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b)
-> (forall a b.
    a -> VarDecl tyname name uni b -> VarDecl tyname name uni a)
-> Functor (VarDecl tyname name uni)
forall a b.
a -> VarDecl tyname name uni b -> VarDecl tyname name uni a
forall a b.
(a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b
forall tyname name (uni :: * -> *) a b.
a -> VarDecl tyname name uni b -> VarDecl tyname name uni a
forall tyname name (uni :: * -> *) a b.
(a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) a b.
(a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b
fmap :: forall a b.
(a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b
$c<$ :: forall tyname name (uni :: * -> *) a b.
a -> VarDecl tyname name uni b -> VarDecl tyname name uni a
<$ :: forall a b.
a -> VarDecl tyname name uni b -> VarDecl tyname name uni a
Functor, Int -> VarDecl tyname name uni ann -> ShowS
[VarDecl tyname name uni ann] -> ShowS
VarDecl tyname name uni ann -> String
(Int -> VarDecl tyname name uni ann -> ShowS)
-> (VarDecl tyname name uni ann -> String)
-> ([VarDecl tyname name uni ann] -> ShowS)
-> Show (VarDecl tyname name uni ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
Int -> VarDecl tyname name uni ann -> ShowS
forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
[VarDecl tyname name uni ann] -> ShowS
forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
VarDecl tyname name uni ann -> String
$cshowsPrec :: forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
Int -> VarDecl tyname name uni ann -> ShowS
showsPrec :: Int -> VarDecl tyname name uni ann -> ShowS
$cshow :: forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
VarDecl tyname name uni ann -> String
show :: VarDecl tyname name uni ann -> String
$cshowList :: forall tyname name (uni :: * -> *) ann.
(GShow uni, Show ann, Show name, Show tyname) =>
[VarDecl tyname name uni ann] -> ShowS
showList :: [VarDecl tyname name uni ann] -> ShowS
Show, (forall x.
 VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x)
-> (forall x.
    Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann)
-> Generic (VarDecl tyname name uni ann)
forall x.
Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann
forall x.
VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) ann x.
Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann x.
VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x
$cfrom :: forall tyname name (uni :: * -> *) ann x.
VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x
from :: forall x.
VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x
$cto :: forall tyname name (uni :: * -> *) ann x.
Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann
to :: forall x.
Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann
Generic)
makeLenses ''VarDecl

-- | A "type declaration", i.e. a kind for a type.
data TyDecl tyname uni ann = TyDecl
    { forall tyname (uni :: * -> *) ann. TyDecl tyname uni ann -> ann
_tyDeclAnn  :: ann
    , forall tyname (uni :: * -> *) ann.
TyDecl tyname uni ann -> Type tyname uni ann
_tyDeclType :: Type tyname uni ann
    , forall tyname (uni :: * -> *) ann.
TyDecl tyname uni ann -> Kind ann
_tyDeclKind :: Kind ann
    } deriving stock ((forall a b.
 (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b)
-> (forall a b. a -> TyDecl tyname uni b -> TyDecl tyname uni a)
-> Functor (TyDecl tyname uni)
forall a b. a -> TyDecl tyname uni b -> TyDecl tyname uni a
forall a b. (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b
forall tyname (uni :: * -> *) a b.
a -> TyDecl tyname uni b -> TyDecl tyname uni a
forall tyname (uni :: * -> *) a b.
(a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname (uni :: * -> *) a b.
(a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b
fmap :: forall a b. (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b
$c<$ :: forall tyname (uni :: * -> *) a b.
a -> TyDecl tyname uni b -> TyDecl tyname uni a
<$ :: forall a b. a -> TyDecl tyname uni b -> TyDecl tyname uni a
Functor, Int -> TyDecl tyname uni ann -> ShowS
[TyDecl tyname uni ann] -> ShowS
TyDecl tyname uni ann -> String
(Int -> TyDecl tyname uni ann -> ShowS)
-> (TyDecl tyname uni ann -> String)
-> ([TyDecl tyname uni ann] -> ShowS)
-> Show (TyDecl tyname uni ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
Int -> TyDecl tyname uni ann -> ShowS
forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
[TyDecl tyname uni ann] -> ShowS
forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
TyDecl tyname uni ann -> String
$cshowsPrec :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
Int -> TyDecl tyname uni ann -> ShowS
showsPrec :: Int -> TyDecl tyname uni ann -> ShowS
$cshow :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
TyDecl tyname uni ann -> String
show :: TyDecl tyname uni ann -> String
$cshowList :: forall tyname (uni :: * -> *) ann.
(GShow uni, Show ann, Show tyname) =>
[TyDecl tyname uni ann] -> ShowS
showList :: [TyDecl tyname uni ann] -> ShowS
Show, (forall x. TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x)
-> (forall x.
    Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann)
-> Generic (TyDecl tyname uni ann)
forall x. Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann
forall x. TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname (uni :: * -> *) ann x.
Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann
forall tyname (uni :: * -> *) ann x.
TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x
$cfrom :: forall tyname (uni :: * -> *) ann x.
TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x
from :: forall x. TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x
$cto :: forall tyname (uni :: * -> *) ann x.
Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann
to :: forall x. Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann
Generic)
makeLenses ''TyDecl

tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann
tyDeclVar :: forall tyname ann (uni :: * -> *).
TyVarDecl tyname ann -> TyDecl tyname uni ann
tyDeclVar (TyVarDecl ann
ann tyname
name Kind ann
kind) = ann -> Type tyname uni ann -> Kind ann -> TyDecl tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> Type tyname uni ann -> Kind ann -> TyDecl tyname uni ann
TyDecl ann
ann (ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann tyname
name) Kind ann
kind

instance HasUnique tyname TypeUnique => HasUnique (TyVarDecl tyname ann) TypeUnique where
    unique :: Lens' (TyVarDecl tyname ann) TypeUnique
unique TypeUnique -> f TypeUnique
f (TyVarDecl ann
ann tyname
tyname Kind ann
kind) =
        (TypeUnique -> f TypeUnique) -> tyname -> f tyname
forall a unique. HasUnique a unique => Lens' a unique
Lens' tyname TypeUnique
unique TypeUnique -> f TypeUnique
f tyname
tyname f tyname
-> (tyname -> TyVarDecl tyname ann) -> f (TyVarDecl tyname ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \tyname
tyname' -> ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann tyname
tyname' Kind ann
kind

instance HasUnique name TermUnique => HasUnique (VarDecl tyname name uni ann) TermUnique where
    unique :: Lens' (VarDecl tyname name uni ann) TermUnique
unique TermUnique -> f TermUnique
f (VarDecl ann
ann name
name Type tyname uni ann
ty) =
        (TermUnique -> f TermUnique) -> name -> f name
forall a unique. HasUnique a unique => Lens' a unique
Lens' name TermUnique
unique TermUnique -> f TermUnique
f name
name f name
-> (name -> VarDecl tyname name uni ann)
-> f (VarDecl tyname name uni ann)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \name
name' -> 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
name' Type tyname uni ann
ty

newtype Normalized a = Normalized
    { forall a. Normalized a -> a
unNormalized :: a
    } deriving stock (Int -> Normalized a -> ShowS
[Normalized a] -> ShowS
Normalized a -> String
(Int -> Normalized a -> ShowS)
-> (Normalized a -> String)
-> ([Normalized a] -> ShowS)
-> Show (Normalized a)
forall a. Show a => Int -> Normalized a -> ShowS
forall a. Show a => [Normalized a] -> ShowS
forall a. Show a => Normalized a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Normalized a -> ShowS
showsPrec :: Int -> Normalized a -> ShowS
$cshow :: forall a. Show a => Normalized a -> String
show :: Normalized a -> String
$cshowList :: forall a. Show a => [Normalized a] -> ShowS
showList :: [Normalized a] -> ShowS
Show, Normalized a -> Normalized a -> Bool
(Normalized a -> Normalized a -> Bool)
-> (Normalized a -> Normalized a -> Bool) -> Eq (Normalized a)
forall a. Eq a => Normalized a -> Normalized a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Normalized a -> Normalized a -> Bool
== :: Normalized a -> Normalized a -> Bool
$c/= :: forall a. Eq a => Normalized a -> Normalized a -> Bool
/= :: Normalized a -> Normalized a -> Bool
Eq, (forall a b. (a -> b) -> Normalized a -> Normalized b)
-> (forall a b. a -> Normalized b -> Normalized a)
-> Functor Normalized
forall a b. a -> Normalized b -> Normalized a
forall a b. (a -> b) -> Normalized a -> Normalized b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Normalized a -> Normalized b
fmap :: forall a b. (a -> b) -> Normalized a -> Normalized b
$c<$ :: forall a b. a -> Normalized b -> Normalized a
<$ :: forall a b. a -> Normalized b -> Normalized a
Functor, (forall m. Monoid m => Normalized m -> m)
-> (forall m a. Monoid m => (a -> m) -> Normalized a -> m)
-> (forall m a. Monoid m => (a -> m) -> Normalized a -> m)
-> (forall a b. (a -> b -> b) -> b -> Normalized a -> b)
-> (forall a b. (a -> b -> b) -> b -> Normalized a -> b)
-> (forall b a. (b -> a -> b) -> b -> Normalized a -> b)
-> (forall b a. (b -> a -> b) -> b -> Normalized a -> b)
-> (forall a. (a -> a -> a) -> Normalized a -> a)
-> (forall a. (a -> a -> a) -> Normalized a -> a)
-> (forall a. Normalized a -> [a])
-> (forall a. Normalized a -> Bool)
-> (forall a. Normalized a -> Int)
-> (forall a. Eq a => a -> Normalized a -> Bool)
-> (forall a. Ord a => Normalized a -> a)
-> (forall a. Ord a => Normalized a -> a)
-> (forall a. Num a => Normalized a -> a)
-> (forall a. Num a => Normalized a -> a)
-> Foldable Normalized
forall a. Eq a => a -> Normalized a -> Bool
forall a. Num a => Normalized a -> a
forall a. Ord a => Normalized a -> a
forall m. Monoid m => Normalized m -> m
forall a. Normalized a -> Bool
forall a. Normalized a -> Int
forall a. Normalized a -> [a]
forall a. (a -> a -> a) -> Normalized a -> a
forall m a. Monoid m => (a -> m) -> Normalized a -> m
forall b a. (b -> a -> b) -> b -> Normalized a -> b
forall a b. (a -> b -> b) -> b -> Normalized a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Normalized m -> m
fold :: forall m. Monoid m => Normalized m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Normalized a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Normalized a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Normalized a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Normalized a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Normalized a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Normalized a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Normalized a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Normalized a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Normalized a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Normalized a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Normalized a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Normalized a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Normalized a -> a
foldr1 :: forall a. (a -> a -> a) -> Normalized a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Normalized a -> a
foldl1 :: forall a. (a -> a -> a) -> Normalized a -> a
$ctoList :: forall a. Normalized a -> [a]
toList :: forall a. Normalized a -> [a]
$cnull :: forall a. Normalized a -> Bool
null :: forall a. Normalized a -> Bool
$clength :: forall a. Normalized a -> Int
length :: forall a. Normalized a -> Int
$celem :: forall a. Eq a => a -> Normalized a -> Bool
elem :: forall a. Eq a => a -> Normalized a -> Bool
$cmaximum :: forall a. Ord a => Normalized a -> a
maximum :: forall a. Ord a => Normalized a -> a
$cminimum :: forall a. Ord a => Normalized a -> a
minimum :: forall a. Ord a => Normalized a -> a
$csum :: forall a. Num a => Normalized a -> a
sum :: forall a. Num a => Normalized a -> a
$cproduct :: forall a. Num a => Normalized a -> a
product :: forall a. Num a => Normalized a -> a
Foldable, Functor Normalized
Foldable Normalized
(Functor Normalized, Foldable Normalized) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Normalized a -> f (Normalized b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Normalized (f a) -> f (Normalized a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Normalized a -> m (Normalized b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Normalized (m a) -> m (Normalized a))
-> Traversable Normalized
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Normalized (m a) -> m (Normalized a)
forall (f :: * -> *) a.
Applicative f =>
Normalized (f a) -> f (Normalized a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Normalized a -> m (Normalized b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Normalized a -> f (Normalized b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Normalized a -> f (Normalized b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Normalized a -> f (Normalized b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Normalized (f a) -> f (Normalized a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Normalized (f a) -> f (Normalized a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Normalized a -> m (Normalized b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Normalized a -> m (Normalized b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Normalized (m a) -> m (Normalized a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Normalized (m a) -> m (Normalized a)
Traversable, (forall x. Normalized a -> Rep (Normalized a) x)
-> (forall x. Rep (Normalized a) x -> Normalized a)
-> Generic (Normalized a)
forall x. Rep (Normalized a) x -> Normalized a
forall x. Normalized a -> Rep (Normalized a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Normalized a) x -> Normalized a
forall a x. Normalized a -> Rep (Normalized a) x
$cfrom :: forall a x. Normalized a -> Rep (Normalized a) x
from :: forall x. Normalized a -> Rep (Normalized a) x
$cto :: forall a x. Rep (Normalized a) x -> Normalized a
to :: forall x. Rep (Normalized a) x -> Normalized a
Generic)
      deriving newtype (Normalized a -> ()
(Normalized a -> ()) -> NFData (Normalized a)
forall a. NFData a => Normalized a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => Normalized a -> ()
rnf :: Normalized a -> ()
NFData, (forall ann. Normalized a -> Doc ann)
-> (forall ann. [Normalized a] -> Doc ann) -> Pretty (Normalized a)
forall ann. [Normalized a] -> Doc ann
forall a ann. Pretty a => [Normalized a] -> Doc ann
forall a ann. Pretty a => Normalized a -> Doc ann
forall ann. Normalized a -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall a ann. Pretty a => Normalized a -> Doc ann
pretty :: forall ann. Normalized a -> Doc ann
$cprettyList :: forall a ann. Pretty a => [Normalized a] -> Doc ann
prettyList :: forall ann. [Normalized a] -> Doc ann
Pretty, PrettyBy config)
      deriving Functor Normalized
Functor Normalized =>
(forall a. a -> Normalized a)
-> (forall a b.
    Normalized (a -> b) -> Normalized a -> Normalized b)
-> (forall a b c.
    (a -> b -> c) -> Normalized a -> Normalized b -> Normalized c)
-> (forall a b. Normalized a -> Normalized b -> Normalized b)
-> (forall a b. Normalized a -> Normalized b -> Normalized a)
-> Applicative Normalized
forall a. a -> Normalized a
forall a b. Normalized a -> Normalized b -> Normalized a
forall a b. Normalized a -> Normalized b -> Normalized b
forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
forall a b c.
(a -> b -> c) -> Normalized a -> Normalized b -> Normalized c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> Normalized a
pure :: forall a. a -> Normalized a
$c<*> :: forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
<*> :: forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
$cliftA2 :: forall a b c.
(a -> b -> c) -> Normalized a -> Normalized b -> Normalized c
liftA2 :: forall a b c.
(a -> b -> c) -> Normalized a -> Normalized b -> Normalized c
$c*> :: forall a b. Normalized a -> Normalized b -> Normalized b
*> :: forall a b. Normalized a -> Normalized b -> Normalized b
$c<* :: forall a b. Normalized a -> Normalized b -> Normalized a
<* :: forall a b. Normalized a -> Normalized b -> Normalized a
Applicative via Identity

-- | All kinds of uniques an entity contains.
type family HasUniques a :: GHC.Constraint
type instance HasUniques (Kind ann) = ()
type instance HasUniques (Type tyname uni ann) = HasUnique tyname TypeUnique
type instance HasUniques (Term tyname name uni fun ann) =
    (HasUnique tyname TypeUnique, HasUnique name TermUnique)
type instance HasUniques (Program tyname name uni fun ann) =
    HasUniques (Term tyname name uni fun ann)

typeAnn :: Type tyname uni ann -> ann
typeAnn :: forall tyname (uni :: * -> *) ann. Type tyname uni ann -> ann
typeAnn (TyVar ann
ann tyname
_       ) = ann
ann
typeAnn (TyFun ann
ann Type tyname uni ann
_ Type tyname uni ann
_     ) = ann
ann
typeAnn (TyIFix ann
ann Type tyname uni ann
_ Type tyname uni ann
_    ) = ann
ann
typeAnn (TyForall ann
ann tyname
_ Kind ann
_ Type tyname uni ann
_) = ann
ann
typeAnn (TyBuiltin ann
ann SomeTypeIn uni
_   ) = ann
ann
typeAnn (TyLam ann
ann tyname
_ Kind ann
_ Type tyname uni ann
_   ) = ann
ann
typeAnn (TyApp ann
ann Type tyname uni ann
_ Type tyname uni ann
_     ) = ann
ann
typeAnn (TySOP ann
ann [[Type tyname uni ann]]
_       ) = ann
ann

termAnn :: Term tyname name uni fun ann -> ann
termAnn :: forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> ann
termAnn (Var ann
ann name
_       ) = ann
ann
termAnn (TyAbs ann
ann tyname
_ Kind ann
_ Term tyname name uni fun ann
_ ) = ann
ann
termAnn (Apply ann
ann Term tyname name uni fun ann
_ Term tyname name uni fun ann
_   ) = ann
ann
termAnn (Constant ann
ann Some (ValueOf uni)
_  ) = ann
ann
termAnn (Builtin  ann
ann fun
_  ) = ann
ann
termAnn (TyInst ann
ann Term tyname name uni fun ann
_ Type tyname uni ann
_  ) = ann
ann
termAnn (Unwrap ann
ann Term tyname name uni fun ann
_    ) = ann
ann
termAnn (IWrap ann
ann Type tyname uni ann
_ Type tyname uni ann
_ Term tyname name uni fun ann
_ ) = ann
ann
termAnn (Error ann
ann Type tyname uni ann
_     ) = ann
ann
termAnn (LamAbs ann
ann name
_ Type tyname uni ann
_ Term tyname name uni fun ann
_) = ann
ann
termAnn (Constr ann
ann Type tyname uni ann
_ Word64
_ [Term tyname name uni fun ann]
_) = ann
ann
termAnn (Case ann
ann Type tyname uni ann
_ Term tyname name uni fun ann
_ [Term tyname name uni fun ann]
_  ) = ann
ann

-- | Map a function over the set of built-in functions.
mapFun :: (fun -> fun') -> Term tyname name uni fun ann -> Term tyname name uni fun' ann
mapFun :: forall fun fun' tyname name (uni :: * -> *) ann.
(fun -> fun')
-> Term tyname name uni fun ann -> Term tyname name uni fun' ann
mapFun fun -> fun'
f = Term tyname name uni fun ann -> Term tyname name uni fun' ann
go where
    go :: Term tyname name uni fun ann -> Term tyname name uni fun' ann
go (LamAbs ann
ann name
name Type tyname uni ann
ty Term tyname name uni fun ann
body)  = ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun' ann
-> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann name
name Type tyname uni ann
ty (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
body)
    go (TyAbs ann
ann tyname
name Kind ann
kind Term tyname name uni fun ann
body) = ann
-> tyname
-> Kind ann
-> Term tyname name uni fun' ann
-> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann tyname
name Kind ann
kind (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
body)
    go (IWrap ann
ann 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 ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann Type tyname uni ann
pat Type tyname uni ann
arg (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
term)
    go (Apply ann
ann 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 ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
fun) (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
arg)
    go (Unwrap ann
ann 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 ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
ann (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
term)
    go (Error ann
ann Type tyname uni ann
ty)             = ann -> Type tyname uni ann -> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann Type tyname uni ann
ty
    go (TyInst ann
ann 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 ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
term) Type tyname uni ann
ty
    go (Var ann
ann name
name)             = ann -> name -> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann name
name
    go (Constant ann
ann Some (ValueOf uni)
con)         = ann -> Some (ValueOf uni) -> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
    go (Builtin ann
ann fun
fun)          = ann -> fun' -> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin ann
ann (fun -> fun'
f fun
fun)
    go (Constr ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
args)     = ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun' ann]
-> Term tyname name uni fun' ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann Type tyname uni ann
ty Word64
i ((Term tyname name uni fun ann -> Term tyname name uni fun' ann)
-> [Term tyname name uni fun ann]
-> [Term tyname name uni fun' ann]
forall a b. (a -> b) -> [a] -> [b]
map Term tyname name uni fun ann -> Term tyname name uni fun' ann
go [Term tyname name uni fun ann]
args)
    go (Case ann
ann 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 ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann Type tyname uni ann
ty (Term tyname name uni fun ann -> Term tyname name uni fun' ann
go Term tyname name uni fun ann
arg) ((Term tyname name uni fun ann -> Term tyname name uni fun' ann)
-> [Term tyname name uni fun ann]
-> [Term tyname name uni fun' ann]
forall a b. (a -> b) -> [a] -> [b]
map Term tyname name uni fun ann -> Term tyname name uni fun' ann
go [Term tyname name uni fun ann]
cs)

-- | This is a wrapper to mark the place where the binder is introduced (i.e. LamAbs/TyAbs)
-- and not where it is actually used (TyVar/Var..).
-- This marking allows us to skip the (de)serialization of binders at LamAbs/TyAbs positions
-- iff 'name' is DeBruijn-encoded (level or index). See for example the instance of  'UntypedPlutusCore.Core.Instance.Flat'
newtype Binder name = Binder { forall name. Binder name -> name
unBinder :: name }
    deriving stock (Binder name -> Binder name -> Bool
(Binder name -> Binder name -> Bool)
-> (Binder name -> Binder name -> Bool) -> Eq (Binder name)
forall name. Eq name => Binder name -> Binder name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall name. Eq name => Binder name -> Binder name -> Bool
== :: Binder name -> Binder name -> Bool
$c/= :: forall name. Eq name => Binder name -> Binder name -> Bool
/= :: Binder name -> Binder name -> Bool
Eq, Int -> Binder name -> ShowS
[Binder name] -> ShowS
Binder name -> String
(Int -> Binder name -> ShowS)
-> (Binder name -> String)
-> ([Binder name] -> ShowS)
-> Show (Binder name)
forall name. Show name => Int -> Binder name -> ShowS
forall name. Show name => [Binder name] -> ShowS
forall name. Show name => Binder name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall name. Show name => Int -> Binder name -> ShowS
showsPrec :: Int -> Binder name -> ShowS
$cshow :: forall name. Show name => Binder name -> String
show :: Binder name -> String
$cshowList :: forall name. Show name => [Binder name] -> ShowS
showList :: [Binder name] -> ShowS
Show)
    -- using this generates faster code, see discussion at <https://input-output-rnd.slack.com/archives/C48HA39RS/p1687917638566799>
    deriving (forall a b. (a -> b) -> Binder a -> Binder b)
-> (forall a b. a -> Binder b -> Binder a) -> Functor Binder
forall a b. a -> Binder b -> Binder a
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Binder a -> Binder b
fmap :: forall a b. (a -> b) -> Binder a -> Binder b
$c<$ :: forall a b. a -> Binder b -> Binder a
<$ :: forall a b. a -> Binder b -> Binder a
Functor via Identity

{- Note [Constr tag type]
Constructor tags are not dynamically created, they can only come from the program itself.

So we do not have to worry about e.g. overflow.

The main constraints that we have are:
1. The use of the tags in the evaluator must be fast.
2. We don't want to allow nonsensical things (e.g. negative tags)
3. We don't want the format to change unexpectedly

These are in tension. The structure we use for storing case branches is a list, which is
traditionally indexed with an 'Int' (and most of the other alternatives are the same). That
suggests using 'Int' as the tag, but 'Int' allows negative tags. A 'Word' would be more
appropriate (of fixed size to satisfy 3), but then we need to be able to index lists by
'Word's.

Well, except there's nothing that _stops_ us indexing lists by 'Word's, we just need to
write our own indexing functions. So that's what we have done.

We use 'Word64' since it's the actual machine word, so no benefit from using a smaller
one (smaller values will be serialized by flat in fewer bytes anyway).
-}