Safe Haskell	None
Language	Haskell2010

PlutusCore.MkPlc

Synopsis

class TermLike term tyname name uni fun | term -> tyname name uni fun where
- var :: ann -> name -> term ann
- tyAbs :: ann -> tyname -> Kind ann -> term ann -> term ann
- lamAbs :: ann -> name -> Type tyname uni ann -> term ann -> term ann
- apply :: ann -> term ann -> term ann -> term ann
- constant :: ann -> Some (ValueOf uni) -> term ann
- builtin :: ann -> fun -> term ann
- tyInst :: ann -> term ann -> Type tyname uni ann -> term ann
- unwrap :: ann -> term ann -> term ann
- iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> term ann -> term ann
- error :: ann -> Type tyname uni ann -> term ann
- termLet :: ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
- typeLet :: ann -> TypeDef tyname uni ann -> term ann -> term ann
type family UniOf a :: Type -> Type
mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltin :: forall k (a :: k) uni tyname ann. uni `Contains` a => ann -> Type tyname uni ann
mkConstantOf :: forall a uni fun term tyname name ann. TermLike term tyname name uni fun => ann -> uni (Esc a) -> a -> term ann
mkConstant :: forall a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `Includes` a) => ann -> a -> term ann
data VarDecl tyname name uni fun ann = VarDecl {
- _varDeclAnn :: ann
- _varDeclName :: name
- _varDeclType :: Type tyname uni ann
}
data TyVarDecl tyname ann = TyVarDecl {
- _tyVarDeclAnn :: ann
- _tyVarDeclName :: tyname
- _tyVarDeclKind :: Kind ann
}
data TyDecl tyname uni ann = TyDecl {
- _tyDeclAnn :: ann
- _tyDeclType :: Type tyname uni ann
- _tyDeclKind :: Kind ann
}
mkVar :: TermLike term tyname name uni fun => ann -> VarDecl tyname name uni fun ann -> term ann
mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann
tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann
data Def var val = Def {
- defVar :: var
- defVal :: val
}
embed :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
type TermDef term tyname name uni fun ann = Def (VarDecl tyname name uni fun ann) (term ann)
type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann)
data FunctionType tyname uni ann = FunctionType {
- _functionTypeAnn :: ann
- _functionTypeDom :: Type tyname uni ann
- _functionTypeCod :: Type tyname uni ann
}
data FunctionDef term tyname name uni fun ann = FunctionDef {
- _functionDefAnn :: ann
- _functionDefName :: name
- _functionDefType :: FunctionType tyname uni ann
- _functionDefTerm :: term ann
}
functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann
functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefVarDecl :: FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni fun ann
mkFunctionDef :: ann -> name -> Type tyname uni ann -> term ann -> Maybe (FunctionDef term tyname name uni fun ann)
mkImmediateLamAbs :: TermLike term tyname name uni fun => ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
mkImmediateTyAbs :: TermLike term tyname name uni fun => ann -> TypeDef tyname uni ann -> term ann -> term ann
mkIterTyForall :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterApp :: TermLike term tyname name uni fun => ann -> term ann -> [term ann] -> term ann
mkIterTyFun :: ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterLamAbs :: TermLike term tyname name uni fun => [VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterInst :: TermLike term tyname name uni fun => ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterTyAbs :: TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyApp :: ann -> Type tyname uni ann -> [Type tyname uni ann] -> Type tyname uni ann
mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann

Documentation

class TermLike term tyname name uni fun | term -> tyname name uni fun where Source #

A final encoding for Term, to allow PLC terms to be used transparently as PIR terms.

Minimal complete definition

var, tyAbs, lamAbs, apply, constant, builtin, tyInst, unwrap, iWrap, error

Methods

var :: ann -> name -> term ann Source #

tyAbs :: ann -> tyname -> Kind ann -> term ann -> term ann Source #

lamAbs :: ann -> name -> Type tyname uni ann -> term ann -> term ann Source #

apply :: ann -> term ann -> term ann -> term ann Source #

constant :: ann -> Some (ValueOf uni) -> term ann Source #

builtin :: ann -> fun -> term ann Source #

tyInst :: ann -> term ann -> Type tyname uni ann -> term ann Source #

unwrap :: ann -> term ann -> term ann Source #

iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> term ann -> term ann Source #

error :: ann -> Type tyname uni ann -> term ann Source #

termLet :: ann -> TermDef term tyname name uni fun ann -> term ann -> term ann Source #

typeLet :: ann -> TypeDef tyname uni ann -> term ann -> term ann Source #

Instances

Instances details

TermLike (Term name uni fun) TyName name uni fun Source #
Instance details Defined in UntypedPlutusCore.Core.Type Methods var :: ann -> name -> Term name uni fun ann Source # tyAbs :: ann -> TyName -> Kind ann -> Term name uni fun ann -> Term name uni fun ann Source # lamAbs :: ann -> name -> Type TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source # apply :: ann -> Term name uni fun ann -> Term name uni fun ann -> Term name uni fun ann Source # constant :: ann -> Some (ValueOf uni) -> Term name uni fun ann Source # builtin :: ann -> fun -> Term name uni fun ann Source # tyInst :: ann -> Term name uni fun ann -> Type TyName uni ann -> Term name uni fun ann Source # unwrap :: ann -> Term name uni fun ann -> Term name uni fun ann Source # iWrap :: ann -> Type TyName uni ann -> Type TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source # error :: ann -> Type TyName uni ann -> Term name uni fun ann Source # termLet :: ann -> TermDef (Term name uni fun) TyName name uni fun ann -> Term name uni fun ann -> Term name uni fun ann Source # typeLet :: ann -> TypeDef TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source #
TermLike (Term tyname name uni fun) tyname name uni fun Source #
Instance details Defined in PlutusCore.MkPlc Methods var :: ann -> name -> Term tyname name uni fun ann Source # tyAbs :: ann -> tyname -> Kind ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # lamAbs :: ann -> name -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # apply :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # constant :: ann -> Some (ValueOf uni) -> Term tyname name uni fun ann Source # builtin :: ann -> fun -> Term tyname name uni fun ann Source # tyInst :: ann -> Term tyname name uni fun ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # unwrap :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # error :: ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # termLet :: ann -> TermDef (Term tyname name uni fun) tyname name uni fun ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # typeLet :: ann -> TypeDef tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source #
TermLike (Term tyname name uni fun) tyname name uni fun Source #
Instance details Defined in PlutusIR.Core.Type Methods var :: ann -> name -> Term tyname name uni fun ann Source # tyAbs :: ann -> tyname -> Kind ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # lamAbs :: ann -> name -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # apply :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # constant :: ann -> Some (ValueOf uni) -> Term tyname name uni fun ann Source # builtin :: ann -> fun -> Term tyname name uni fun ann Source # tyInst :: ann -> Term tyname name uni fun ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # unwrap :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # error :: ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # termLet :: ann -> TermDef (Term tyname name uni fun) tyname name uni fun ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # typeLet :: ann -> TypeDef tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source #

type family UniOf a :: Type -> Type Source #

Extract the universe from a type.

Instances

Instances details

type UniOf (Opaque val rep) Source #
Instance details Defined in PlutusCore.Builtin.Polymorphism type UniOf (Opaque val rep) = UniOf val
type UniOf (CkValue uni fun) Source #
Instance details Defined in PlutusCore.Evaluation.Machine.Ck type UniOf (CkValue uni fun) = uni
type UniOf (CekValue uni fun) Source #
Instance details Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type UniOf (CekValue uni fun) = uni
type UniOf (Term name uni fun ann) Source #
Instance details Defined in UntypedPlutusCore.Core.Type type UniOf (Term name uni fun ann) = uni
type UniOf (Term tyname name uni fun ann) Source #
Instance details Defined in PlutusCore.Core.Type type UniOf (Term tyname name uni fun ann) = uni
type UniOf (Term tyname name uni fun ann) Source #
Instance details Defined in PlutusIR.Core.Type type UniOf (Term tyname name uni fun ann) = uni

mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann Source #

Embed a type (given its explicit type tag) into a PLC type.

mkTyBuiltin :: forall k (a :: k) uni tyname ann. uni `Contains` a => ann -> Type tyname uni ann Source #

Embed a type (provided it's in the universe) into a PLC type.

mkConstantOf :: forall a uni fun term tyname name ann. TermLike term tyname name uni fun => ann -> uni (Esc a) -> a -> term ann Source #

Embed a Haskell value (given its explicit type tag) into a PLC term.

mkConstant :: forall a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `Includes` a) => ann -> a -> term ann Source #

Embed a Haskell value (provided its type is in the universe) into a PLC term.

data VarDecl tyname name uni fun ann Source #

A "variable declaration", i.e. a name and a type for a variable.

Constructors

VarDecl
Fields _varDeclAnn :: ann _varDeclName :: name _varDeclType :: Type tyname uni ann

Instances

Instances details

tyname ~ TyName => Reference TyName (VarDecl tyname name uni fun) Source #
Instance details Defined in PlutusIR.Core.Instance.Scoping Methods referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> VarDecl tyname name uni fun NameAnn -> VarDecl tyname name uni fun NameAnn Source #
(PrettyClassicBy configName tyname, PrettyClassicBy configName name, GShow uni, Everywhere uni PrettyConst, Pretty ann) => PrettyBy (PrettyConfigClassic configName) (VarDecl tyname name uni fun ann) Source #
Instance details Defined in PlutusIR.Core.Instance.Pretty Methods prettyBy :: PrettyConfigClassic configName -> VarDecl tyname name uni fun ann -> Doc ann0 # prettyListBy :: PrettyConfigClassic configName -> [VarDecl tyname name uni fun ann] -> Doc ann0 #
Functor (VarDecl tyname name uni fun) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> VarDecl tyname name uni fun a -> VarDecl tyname name uni fun b Source # (<$) :: a -> VarDecl tyname name uni fun b -> VarDecl tyname name uni fun a Source #
(tyname ~ TyName, name ~ Name) => CollectScopeInfo (VarDecl tyname name uni fun) Source #
Instance details Defined in PlutusIR.Core.Instance.Scoping Methods collectScopeInfo :: VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #
(Show ann, Show name, Show tyname, GShow uni) => Show (VarDecl tyname name uni fun ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> VarDecl tyname name uni fun ann -> ShowS Source # show :: VarDecl tyname name uni fun ann -> String Source # showList :: [VarDecl tyname name uni fun ann] -> ShowS Source #
Generic (VarDecl tyname name uni fun ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (VarDecl tyname name uni fun ann) :: Type -> Type Source # Methods from :: VarDecl tyname name uni fun ann -> Rep (VarDecl tyname name uni fun ann) x Source # to :: Rep (VarDecl tyname name uni fun ann) x -> VarDecl tyname name uni fun ann Source #
(PrettyClassic tyname, PrettyClassic name, GShow uni, Everywhere uni PrettyConst, Pretty ann) => Pretty (VarDecl tyname name uni fun ann) Source #
Instance details Defined in PlutusIR.Core.Instance.Pretty Methods pretty :: VarDecl tyname name uni fun ann -> Doc ann0 # prettyList :: [VarDecl tyname name uni fun ann] -> Doc ann0 #
(Closed uni, Flat fun, Flat ann, Flat tyname, Flat name) => Flat (VarDecl tyname name uni fun ann)
Instance details Defined in PlutusCore.Flat Methods encode :: VarDecl tyname name uni fun ann -> Encoding decode :: Get (VarDecl tyname name uni fun ann) size :: VarDecl tyname name uni fun ann -> NumBits -> NumBits
HasUnique name TermUnique => HasUnique (VarDecl tyname name uni fun ann) TermUnique Source #
Instance details Defined in PlutusCore.Core.Type Methods unique :: Lens' (VarDecl tyname name uni fun ann) TermUnique Source #
Reference name t => Reference (VarDecl tyname name uni fun ann) t Source #
Instance details Defined in PlutusIR.Core.Instance.Scoping Methods referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> VarDecl tyname name uni fun ann -> t NameAnn -> t NameAnn Source #
type Rep (VarDecl tyname name uni fun ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (VarDecl tyname name uni fun ann) = D1 ('MetaData "VarDecl" "PlutusCore.Core.Type" "plutus-core-1.0.0.1-6wMiyL0yerXJu56t8zBoKx" 'False) (C1 ('MetaCons "VarDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_varDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_varDeclName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name) :: S1 ('MetaSel ('Just "_varDeclType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type tyname uni ann)))))

data TyVarDecl tyname ann Source #

A "type variable declaration", i.e. a name and a kind for a type variable.

Constructors

TyVarDecl
Fields _tyVarDeclAnn :: ann _tyVarDeclName :: tyname _tyVarDeclKind :: Kind ann

Instances

Instances details

Functor (TyVarDecl tyname) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b Source # (<$) :: a -> TyVarDecl tyname b -> TyVarDecl tyname a Source #
tyname ~ TyName => CollectScopeInfo (TyVarDecl tyname) Source #
Instance details Defined in PlutusIR.Core.Instance.Scoping Methods collectScopeInfo :: TyVarDecl tyname NameAnn -> ScopeErrorOrInfo Source #
(PrettyClassicBy configName tyname, Pretty ann) => PrettyBy (PrettyConfigClassic configName) (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusIR.Core.Instance.Pretty Methods prettyBy :: PrettyConfigClassic configName -> TyVarDecl tyname ann -> Doc ann0 # prettyListBy :: PrettyConfigClassic configName -> [TyVarDecl tyname ann] -> Doc ann0 #
(Show ann, Show tyname) => Show (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> TyVarDecl tyname ann -> ShowS Source # show :: TyVarDecl tyname ann -> String Source # showList :: [TyVarDecl tyname ann] -> ShowS Source #
Generic (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (TyVarDecl tyname ann) :: Type -> Type Source # Methods from :: TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x Source # to :: Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann Source #
(PrettyClassic tyname, Pretty ann) => Pretty (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusIR.Core.Instance.Pretty Methods pretty :: TyVarDecl tyname ann -> Doc ann0 # prettyList :: [TyVarDecl tyname ann] -> Doc ann0 #
(Flat ann, Flat tyname) => Flat (TyVarDecl tyname ann)
Instance details Defined in PlutusCore.Flat Methods encode :: TyVarDecl tyname ann -> Encoding decode :: Get (TyVarDecl tyname ann) size :: TyVarDecl tyname ann -> NumBits -> NumBits
HasUnique tyname TypeUnique => HasUnique (TyVarDecl tyname ann) TypeUnique Source #
Instance details Defined in PlutusCore.Core.Type Methods unique :: Lens' (TyVarDecl tyname ann) TypeUnique Source #
Reference tyname t => Reference (TyVarDecl tyname ann) t Source #
Instance details Defined in PlutusIR.Core.Instance.Scoping Methods referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> TyVarDecl tyname ann -> t NameAnn -> t NameAnn Source #
type Rep (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (TyVarDecl tyname ann) = D1 ('MetaData "TyVarDecl" "PlutusCore.Core.Type" "plutus-core-1.0.0.1-6wMiyL0yerXJu56t8zBoKx" 'False) (C1 ('MetaCons "TyVarDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tyVarDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_tyVarDeclName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 tyname) :: S1 ('MetaSel ('Just "_tyVarDeclKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Kind ann)))))

data TyDecl tyname uni ann Source #

A "type declaration", i.e. a kind for a type.

Constructors

TyDecl
Fields _tyDeclAnn :: ann _tyDeclType :: Type tyname uni ann _tyDeclKind :: Kind ann

Instances

Instances details

Functor (TyDecl tyname uni) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b Source # (<$) :: a -> TyDecl tyname uni b -> TyDecl tyname uni a Source #
(Show ann, Show tyname, GShow uni) => Show (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> TyDecl tyname uni ann -> ShowS Source # show :: TyDecl tyname uni ann -> String Source # showList :: [TyDecl tyname uni ann] -> ShowS Source #
Generic (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (TyDecl tyname uni ann) :: Type -> Type Source # Methods from :: TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x Source # to :: Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann Source #
type Rep (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (TyDecl tyname uni ann) = D1 ('MetaData "TyDecl" "PlutusCore.Core.Type" "plutus-core-1.0.0.1-6wMiyL0yerXJu56t8zBoKx" 'False) (C1 ('MetaCons "TyDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tyDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_tyDeclType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type tyname uni ann)) :: S1 ('MetaSel ('Just "_tyDeclKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Kind ann)))))

mkVar :: TermLike term tyname name uni fun => ann -> VarDecl tyname name uni fun ann -> term ann Source #

Make a Var referencing the given VarDecl.

mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann Source #

Make a TyVar referencing the given TyVarDecl.

tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann Source #

data Def var val Source #

A definition. Pretty much just a pair with more descriptive names.

Constructors

Def
Fields defVar :: var defVal :: val

Instances

Instances details

(Eq var, Eq val) => Eq (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods (==) :: Def var val -> Def var val -> Bool Source # (/=) :: Def var val -> Def var val -> Bool Source #
(Ord var, Ord val) => Ord (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods compare :: Def var val -> Def var val -> Ordering Source # (<) :: Def var val -> Def var val -> Bool Source # (<=) :: Def var val -> Def var val -> Bool Source # (>) :: Def var val -> Def var val -> Bool Source # (>=) :: Def var val -> Def var val -> Bool Source # max :: Def var val -> Def var val -> Def var val Source # min :: Def var val -> Def var val -> Def var val Source #
(Show var, Show val) => Show (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods showsPrec :: Int -> Def var val -> ShowS Source # show :: Def var val -> String Source # showList :: [Def var val] -> ShowS Source #
Generic (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Associated Types type Rep (Def var val) :: Type -> Type Source # Methods from :: Def var val -> Rep (Def var val) x Source # to :: Rep (Def var val) x -> Def var val Source #
type Rep (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc type Rep (Def var val) = D1 ('MetaData "Def" "PlutusCore.MkPlc" "plutus-core-1.0.0.1-6wMiyL0yerXJu56t8zBoKx" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) (S1 ('MetaSel ('Just "defVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 var) :*: S1 ('MetaSel ('Just "defVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 val)))

embed :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann Source #

type TermDef term tyname name uni fun ann = Def (VarDecl tyname name uni fun ann) (term ann) Source #

A term definition as a variable.

type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann) Source #

A type definition as a type variable.

data FunctionType tyname uni ann Source #

The type of a PLC function.

Constructors

FunctionType
Fields _functionTypeAnn :: ann An annotation. _functionTypeDom :: Type tyname uni ann The domain of a function. _functionTypeCod :: Type tyname uni ann The codomain of the function.

data FunctionDef term tyname name uni fun ann Source #

A PLC function.

Constructors

FunctionDef
Fields _functionDefAnn :: ann An annotation. _functionDefName :: name The name of a function. _functionDefType :: FunctionType tyname uni ann The type of the function. _functionDefTerm :: term ann The definition of the function.

functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann Source #

Convert a FunctionType to the corresponding Type.

functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann Source #

Get the type of a FunctionDef.

functionDefVarDecl :: FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni fun ann Source #

Convert a FunctionDef to a VarDecl. I.e. ignore the actual term.

mkFunctionDef :: ann -> name -> Type tyname uni ann -> term ann -> Maybe (FunctionDef term tyname name uni fun ann) Source #

Make a FunctionDef. Return Nothing if the provided type is not functional.

mkImmediateLamAbs Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> TermDef term tyname name uni fun ann
-> term ann	The body of the let, possibly referencing the name.
-> term ann

Make a "let-binding" for a term as an immediately applied lambda abstraction.

mkImmediateTyAbs Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> TypeDef tyname uni ann
-> term ann	The body of the let, possibly referencing the name.
-> term ann

Make a "let-binding" for a type as an immediately instantiated type abstraction. Note: the body must be a value.

mkIterTyForall :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Universally quantify a list of names.

mkIterTyLam :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Lambda abstract a list of names.

mkIterApp Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> term ann	f
-> [term ann]	[ x0 ... xn ]
-> term ann	[f x0 ... xn ]

Make an iterated application.

mkIterTyFun :: ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Make an iterated function type.

mkIterLamAbs :: TermLike term tyname name uni fun => [VarDecl tyname name uni fun ann] -> term ann -> term ann Source #

Lambda abstract a list of names.

mkIterInst Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> term ann	a
-> [Type tyname uni ann]	[ x0 ... xn ]
-> term ann	{ a x0 ... xn }

Make an iterated instantiation.

mkIterTyAbs :: TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann Source #

Type abstract a list of names.

mkIterTyApp Source #

Arguments

:: ann
-> Type tyname uni ann	f
-> [Type tyname uni ann]	[ x0 ... xn ]
-> Type tyname uni ann	[ f x0 ... xn ]

Make an iterated type application.

mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann Source #

Make an iterated function kind.