{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE DerivingVia              #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell          #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE UndecidableInstances     #-}

module PlutusCore.Core.Type
    ( Kind (..)
    , Type (..)
    , Term (..)
    , Version (..)
    , Program (..)
    , UniOf
    , Normalized (..)
    , TyVarDecl (..)
    , VarDecl (..)
    , TyDecl (..)
    , tyDeclVar
    , HasUniques
    , Binder (..)
    , defaultVersion
    -- * Helper functions
    , termAnn
    , typeAnn
    , mapFun
    , tyVarDeclAnn
    , tyVarDeclName
    , tyVarDeclKind
    , varDeclAnn
    , varDeclName
    , varDeclType
    , tyDeclAnn
    , tyDeclType
    , tyDeclKind
    , progAnn
    , progVer
    , progTerm
    )
where

import PlutusPrelude

import PlutusCore.Name

import Control.Lens
import Data.Hashable
import Data.Kind qualified as GHC
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
/= :: Kind ann -> Kind ann -> Bool
$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
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
showList :: [Kind ann] -> ShowS
$cshowList :: forall ann. Show ann => [Kind ann] -> ShowS
show :: Kind ann -> String
$cshow :: forall ann. Show ann => Kind ann -> String
showsPrec :: Int -> Kind ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> Kind ann -> ShowS
Show, a -> Kind b -> Kind a
(a -> b) -> Kind a -> Kind b
(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
<$ :: a -> Kind b -> Kind a
$c<$ :: forall a b. a -> Kind b -> Kind a
fmap :: (a -> b) -> Kind a -> Kind b
$cfmap :: forall a b. (a -> b) -> Kind a -> Kind b
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
$cto :: forall ann x. Rep (Kind ann) x -> Kind ann
$cfrom :: forall ann x. Kind ann -> Rep (Kind ann) x
Generic, Kind ann -> Q Exp
Kind ann -> Q (TExp (Kind ann))
(Kind ann -> Q Exp)
-> (Kind ann -> Q (TExp (Kind ann))) -> Lift (Kind ann)
forall ann. Lift ann => Kind ann -> Q Exp
forall ann. Lift ann => Kind ann -> Q (TExp (Kind ann))
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: Kind ann -> Q (TExp (Kind ann))
$cliftTyped :: forall ann. Lift ann => Kind ann -> Q (TExp (Kind ann))
lift :: Kind ann -> Q Exp
$clift :: forall ann. Lift ann => Kind ann -> Q Exp
Lift)
    deriving anyclass (Kind ann -> ()
(Kind ann -> ()) -> NFData (Kind ann)
forall ann. NFData ann => Kind ann -> ()
forall a. (a -> ()) -> NFData a
rnf :: Kind ann -> ()
$crnf :: forall ann. NFData ann => Kind ann -> ()
NFData, Int -> Kind ann -> Int
Kind ann -> Int
(Int -> Kind ann -> Int)
-> (Kind ann -> Int) -> Hashable (Kind ann)
forall ann. Hashable ann => Int -> Kind ann -> Int
forall ann. Hashable ann => Kind ann -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Kind ann -> Int
$chash :: forall ann. Hashable ann => Kind ann -> Int
hashWithSalt :: Int -> Kind ann -> Int
$chashWithSalt :: forall ann. Hashable ann => Int -> Kind ann -> Int
Hashable)

-- | 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
    | TyFun ann (Type tyname uni ann) (Type tyname uni ann)
    | 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)
    | TyBuiltin ann (SomeTypeIn uni) -- ^ Builtin type
    | TyLam ann tyname (Kind ann) (Type tyname uni ann)
    | TyApp ann (Type tyname uni ann) (Type tyname uni ann)
    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.
(Show ann, Show tyname, GShow uni) =>
Int -> Type tyname uni ann -> ShowS
forall tyname (uni :: * -> *) ann.
(Show ann, Show tyname, GShow uni) =>
[Type tyname uni ann] -> ShowS
forall tyname (uni :: * -> *) ann.
(Show ann, Show tyname, GShow uni) =>
Type tyname uni ann -> String
showList :: [Type tyname uni ann] -> ShowS
$cshowList :: forall tyname (uni :: * -> *) ann.
(Show ann, Show tyname, GShow uni) =>
[Type tyname uni ann] -> ShowS
show :: Type tyname uni ann -> String
$cshow :: forall tyname (uni :: * -> *) ann.
(Show ann, Show tyname, GShow uni) =>
Type tyname uni ann -> String
showsPrec :: Int -> Type tyname uni ann -> ShowS
$cshowsPrec :: forall tyname (uni :: * -> *) ann.
(Show ann, Show tyname, GShow uni) =>
Int -> Type tyname uni ann -> ShowS
Show, a -> Type tyname uni b -> Type tyname uni a
(a -> b) -> Type tyname uni a -> Type tyname uni b
(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
<$ :: a -> Type tyname uni b -> Type tyname uni a
$c<$ :: forall tyname (uni :: * -> *) a b.
a -> Type tyname uni b -> Type tyname uni a
fmap :: (a -> b) -> Type tyname uni a -> Type tyname uni b
$cfmap :: forall tyname (uni :: * -> *) a b.
(a -> b) -> Type tyname uni a -> Type tyname uni b
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
$cto :: forall tyname (uni :: * -> *) ann x.
Rep (Type tyname uni ann) x -> Type tyname uni ann
$cfrom :: forall tyname (uni :: * -> *) ann x.
Type tyname uni ann -> Rep (Type tyname uni ann) x
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 -> ()
rnf :: Type tyname uni ann -> ()
$crnf :: forall tyname (uni :: * -> *) ann.
(NFData ann, NFData tyname, Closed uni) =>
Type tyname uni ann -> ()
NFData)

data Term tyname name uni fun ann
    = Var ann name -- ^ a named variable
    | TyAbs ann tyname (Kind ann) (Term tyname name uni fun ann)
    | LamAbs ann name (Type tyname uni ann) (Term tyname name uni fun ann)
    | Apply ann (Term tyname name uni fun ann) (Term tyname name uni fun ann)
    | Constant ann (Some (ValueOf uni)) -- ^ a constant term
    | Builtin ann fun
    | TyInst ann (Term tyname name uni fun ann) (Type tyname uni ann)
    | Unwrap ann (Term tyname name uni fun ann)
    | IWrap ann (Type tyname uni ann) (Type tyname uni ann) (Term tyname name uni fun ann)
    | Error ann (Type tyname uni ann)
    deriving stock (Int -> Term tyname name uni fun ann -> ShowS
[Term tyname name uni fun ann] -> ShowS
Term tyname name uni fun ann -> String
(Int -> Term tyname name uni fun ann -> ShowS)
-> (Term tyname name uni fun ann -> String)
-> ([Term tyname name uni fun ann] -> ShowS)
-> Show (Term tyname name uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Int -> Term tyname name uni fun ann -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
[Term tyname name uni fun ann] -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Term tyname name uni fun ann -> String
showList :: [Term tyname name uni fun ann] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
[Term tyname name uni fun ann] -> ShowS
show :: Term tyname name uni fun ann -> String
$cshow :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Term tyname name uni fun ann -> String
showsPrec :: Int -> Term tyname name uni fun ann -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Int -> Term tyname name uni fun ann -> ShowS
Show, a -> Term tyname name uni fun b -> Term tyname name uni fun a
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
(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
<$ :: a -> Term tyname name uni fun b -> Term tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
fmap :: (a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
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
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Term tyname name uni fun ann) x
-> Term tyname name uni fun ann
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Term tyname name uni fun ann
-> Rep (Term tyname name uni fun ann) x
Generic)
    deriving anyclass (Term tyname name uni fun ann -> ()
(Term tyname name uni fun ann -> ())
-> NFData (Term tyname name uni fun ann)
forall a. (a -> ()) -> NFData a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData tyname, NFData fun) =>
Term tyname name uni fun ann -> ()
rnf :: Term tyname name uni fun ann -> ()
$crnf :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData tyname, NFData fun) =>
Term tyname name uni fun ann -> ()
NFData)

-- | Version of Plutus Core to be used for the program.
data Version ann
    = Version ann Natural Natural Natural
    deriving stock (Version ann -> Version ann -> Bool
(Version ann -> Version ann -> Bool)
-> (Version ann -> Version ann -> Bool) -> Eq (Version ann)
forall ann. Eq ann => Version ann -> Version ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Version ann -> Version ann -> Bool
$c/= :: forall ann. Eq ann => Version ann -> Version ann -> Bool
== :: Version ann -> Version ann -> Bool
$c== :: forall ann. Eq ann => Version ann -> Version ann -> Bool
Eq, Int -> Version ann -> ShowS
[Version ann] -> ShowS
Version ann -> String
(Int -> Version ann -> ShowS)
-> (Version ann -> String)
-> ([Version ann] -> ShowS)
-> Show (Version ann)
forall ann. Show ann => Int -> Version ann -> ShowS
forall ann. Show ann => [Version ann] -> ShowS
forall ann. Show ann => Version ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Version ann] -> ShowS
$cshowList :: forall ann. Show ann => [Version ann] -> ShowS
show :: Version ann -> String
$cshow :: forall ann. Show ann => Version ann -> String
showsPrec :: Int -> Version ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> Version ann -> ShowS
Show, a -> Version b -> Version a
(a -> b) -> Version a -> Version b
(forall a b. (a -> b) -> Version a -> Version b)
-> (forall a b. a -> Version b -> Version a) -> Functor Version
forall a b. a -> Version b -> Version a
forall a b. (a -> b) -> Version a -> Version b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Version b -> Version a
$c<$ :: forall a b. a -> Version b -> Version a
fmap :: (a -> b) -> Version a -> Version b
$cfmap :: forall a b. (a -> b) -> Version a -> Version b
Functor, (forall x. Version ann -> Rep (Version ann) x)
-> (forall x. Rep (Version ann) x -> Version ann)
-> Generic (Version ann)
forall x. Rep (Version ann) x -> Version ann
forall x. Version ann -> Rep (Version ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ann x. Rep (Version ann) x -> Version ann
forall ann x. Version ann -> Rep (Version ann) x
$cto :: forall ann x. Rep (Version ann) x -> Version ann
$cfrom :: forall ann x. Version ann -> Rep (Version ann) x
Generic)
    deriving anyclass (Version ann -> ()
(Version ann -> ()) -> NFData (Version ann)
forall ann. NFData ann => Version ann -> ()
forall a. (a -> ()) -> NFData a
rnf :: Version ann -> ()
$crnf :: forall ann. NFData ann => Version ann -> ()
NFData, Int -> Version ann -> Int
Version ann -> Int
(Int -> Version ann -> Int)
-> (Version ann -> Int) -> Hashable (Version ann)
forall ann. Hashable ann => Int -> Version ann -> Int
forall ann. Hashable ann => Version ann -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Version ann -> Int
$chash :: forall ann. Hashable ann => Version ann -> Int
hashWithSalt :: Int -> Version ann -> Int
$chashWithSalt :: forall ann. Hashable ann => Int -> Version ann -> Int
Hashable)

-- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language.
data Program tyname name uni fun ann = Program
    { Program tyname name uni fun ann -> ann
_progAnn  :: ann
    , Program tyname name uni fun ann -> Version ann
_progVer  :: Version ann
    , Program tyname name uni fun ann -> Term tyname name uni fun ann
_progTerm :: Term tyname name uni fun ann
    }
    deriving stock (Int -> Program tyname name uni fun ann -> ShowS
[Program tyname name uni fun ann] -> ShowS
Program tyname name uni fun ann -> String
(Int -> Program tyname name uni fun ann -> ShowS)
-> (Program tyname name uni fun ann -> String)
-> ([Program tyname name uni fun ann] -> ShowS)
-> Show (Program tyname name uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Int -> Program tyname name uni fun ann -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
[Program tyname name uni fun ann] -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Program tyname name uni fun ann -> String
showList :: [Program tyname name uni fun ann] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
[Program tyname name uni fun ann] -> ShowS
show :: Program tyname name uni fun ann -> String
$cshow :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Program tyname name uni fun ann -> String
showsPrec :: Int -> Program tyname name uni fun ann -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show tyname, Show fun) =>
Int -> Program tyname name uni fun ann -> ShowS
Show, a -> Program tyname name uni fun b -> Program tyname name uni fun a
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
(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
<$ :: a -> Program tyname name uni fun b -> Program tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
fmap :: (a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
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
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
Generic)
    deriving anyclass (Program tyname name uni fun ann -> ()
(Program tyname name uni fun ann -> ())
-> NFData (Program tyname name uni fun ann)
forall a. (a -> ()) -> NFData a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData tyname, NFData fun) =>
Program tyname name uni fun ann -> ()
rnf :: Program tyname name uni fun ann -> ()
$crnf :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData tyname, NFData fun) =>
Program tyname name uni fun ann -> ()
NFData)
makeLenses ''Program

-- | 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
    { TyVarDecl tyname ann -> ann
_tyVarDeclAnn  :: ann
    , TyVarDecl tyname ann -> tyname
_tyVarDeclName :: tyname
    , TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind :: Kind ann
    } deriving stock (a -> TyVarDecl tyname b -> TyVarDecl tyname a
(a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
(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
<$ :: a -> TyVarDecl tyname b -> TyVarDecl tyname a
$c<$ :: forall tyname a b. a -> TyVarDecl tyname b -> TyVarDecl tyname a
fmap :: (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
$cfmap :: forall tyname a b.
(a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b
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
showList :: [TyVarDecl tyname ann] -> ShowS
$cshowList :: forall tyname ann.
(Show ann, Show tyname) =>
[TyVarDecl tyname ann] -> ShowS
show :: TyVarDecl tyname ann -> String
$cshow :: forall tyname ann.
(Show ann, Show tyname) =>
TyVarDecl tyname ann -> String
showsPrec :: Int -> TyVarDecl tyname ann -> ShowS
$cshowsPrec :: forall tyname ann.
(Show ann, Show tyname) =>
Int -> 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
$cto :: forall tyname ann x.
Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann
$cfrom :: forall tyname ann x.
TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x
Generic)
makeLenses ''TyVarDecl

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

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

tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann
tyDeclVar :: 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 :: (TypeUnique -> f TypeUnique)
-> TyVarDecl tyname ann -> f (TyVarDecl tyname ann)
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
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 fun ann) TermUnique where
    unique :: (TermUnique -> f TermUnique)
-> VarDecl tyname name uni fun ann
-> f (VarDecl tyname name uni fun ann)
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
unique TermUnique -> f TermUnique
f name
name f name
-> (name -> VarDecl tyname name uni fun ann)
-> f (VarDecl tyname name uni fun 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 fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
ann name
name' Type tyname uni ann
ty

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

-- | The default version of Plutus Core supported by this library.
defaultVersion :: ann -> Version ann
defaultVersion :: ann -> Version ann
defaultVersion ann
ann = ann -> Natural -> Natural -> Natural -> Version ann
forall ann. ann -> Natural -> Natural -> Natural -> Version ann
Version ann
ann Natural
1 Natural
0 Natural
0

typeAnn :: Type tyname uni ann -> ann
typeAnn :: 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

termAnn :: Term tyname name uni fun ann -> ann
termAnn :: 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

-- | 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 :: (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)

-- | 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 { Binder name -> name
unBinder :: name }