Safe Haskell	Safe-Inferred
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
- constr :: ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
- kase :: ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
- termLet :: ann -> TermDef term tyname name uni ann -> term ann -> term ann
- typeLet :: ann -> TypeDef tyname uni ann -> term ann -> term ann
type family UniOf a :: Type -> Type
type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x)
type HasTermLevel uni = Includes uni
type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x)
mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltin :: forall a (x :: a) uni ann tyname. uni `HasTypeLevel` x => 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 `HasTermLevel` a) => ann -> a -> term ann
data VarDecl tyname name uni 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 => VarDecl tyname name uni 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
}
embedTerm :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
type TermDef term tyname name uni ann = Def (VarDecl tyname name uni 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 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 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 => term ann -> [(ann, term ann)] -> term ann
mkIterAppNoAnn :: TermLike term tyname name uni fun => term () -> [term ()] -> term ()
(@@) :: TermLike term tyname name uni fun => term () -> [term ()] -> term ()
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 ann] -> term ann -> term ann
mkIterInst :: TermLike term tyname name uni fun => term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInstNoAnn :: TermLike term tyname name uni fun => term () -> [Type tyname uni ()] -> term ()
mkIterTyAbs :: TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyApp :: Type tyname uni ann -> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyAppNoAnn :: Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann
mkFreshTermLet :: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a) => Type tyname uni a -> t a -> m (t a, t a -> t a)
headSpineToTerm :: TermLike term tyname name uni fun => ann -> MonoHeadSpine err (term ann) -> Either err (term ann)
headSpineToTermNoAnn :: TermLike term tyname name uni fun => MonoHeadSpine err (term ()) -> Either err (term ())

Documentation

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

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, constr, kase

Methods

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 #

constr :: ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann #

kase :: ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann #

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

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

Instances

Instances details

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

type family UniOf a :: Type -> Type #

Extract the universe from a type.

Instances

Instances details

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

type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x) #

Specifies that the given type is a built-in one and can be embedded into a Kind.

type HasTermLevel uni = Includes uni #

Specifies that the given type is a built-in one and its values can be embedded into a Term.

type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x) #

The product of HasTypeLevel and HasTermLevel.

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

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

mkTyBuiltin :: forall a (x :: a) uni ann tyname. uni `HasTypeLevel` x => ann -> Type tyname uni ann #

Convert a Haskell representation of a possibly 0-ary application of a built-in type to arbitrary types implementing KnownTypeAst.

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

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 `HasTermLevel` a) => ann -> a -> term ann #

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

data VarDecl tyname name uni ann #

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

(PrettyReadableBy configName tyname, PrettyReadableBy configName name, PrettyUni uni) => PrettyBy (PrettyConfigReadable configName) (VarDecl tyname name uni ann) #
Instance details Defined in PlutusCore.Core.Instance.Pretty.Readable Methods prettyBy :: PrettyConfigReadable configName -> VarDecl tyname name uni ann -> Doc ann0 # prettyListBy :: PrettyConfigReadable configName -> [VarDecl tyname name uni ann] -> Doc ann0 #
NumBits #
HasUnique tyname TypeUnique => HasUnique (TyVarDecl tyname ann) TypeUnique #
Instance details Defined in PlutusCore.Core.Type Methods unique :: Lens' (TyVarDecl tyname ann) TypeUnique #
type Rep (TyVarDecl tyname ann) #
Instance details Defined in PlutusCore.Core.Type type Rep (TyVarDecl tyname ann) = D1 ('MetaData "TyVarDecl" "PlutusCore.Core.Type" "plutus-core-1.60.0.0-inplace" '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 #

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) #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b # (<$) :: a -> TyDecl tyname uni b -> TyDecl tyname uni a #
Generic (TyDecl tyname uni ann) #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (TyDecl tyname uni ann) :: Type -> Type # Methods from :: TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x # to :: Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann #
(GShow uni, Show ann, Show tyname) => Show (TyDecl tyname uni ann) #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> TyDecl tyname uni ann -> ShowS # show :: TyDecl tyname uni ann -> String # showList :: [TyDecl tyname uni ann] -> ShowS #
type Rep (TyDecl tyname uni ann) #
Instance details Defined in PlutusCore.Core.Type type Rep (TyDecl tyname uni ann) = D1 ('MetaData "TyDecl" "PlutusCore.Core.Type" "plutus-core-1.60.0.0-inplace" '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 => VarDecl tyname name uni ann -> term ann #

Make a Var referencing the given VarDecl. The ann is propagated from the VarDecl to the Var.

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

Make a TyVar referencing the given TyVarDecl.

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

data Def var val #

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

Constructors

Def
Fields defVar :: var defVal :: val

Instances

Instances details

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

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

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

A term definition as a variable.

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

A type definition as a type variable.

data FunctionType tyname uni ann #

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 #

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 #

Convert a FunctionType to the corresponding Kind.

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

Get the type of a FunctionDef.

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

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) #

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

mkImmediateLamAbs #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> TermDef term tyname name uni 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 #

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 #

Universally quantify a list of names.

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

Lambda abstract a list of names.

mkIterApp :: TermLike term tyname name uni fun => term ann -> [(ann, term ann)] -> term ann #

Make an iterated application. Each apply node uses the annotation associated with the corresponding argument.

mkIterAppNoAnn #

Arguments

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

Make an iterated application with no annotation.

(@@) #

Arguments

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

An infix synonym for mkIterAppNoAnn

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

Make an iterated function type.

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

Lambda abstract a list of names.

mkIterInst #

Arguments

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

Make an iterated instantiation. Each tyInst node uses the annotation associated with the corresponding argument.

mkIterInstNoAnn #

Arguments

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

Make an iterated instantiation with no annotation.

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

Type abstract a list of names.

mkIterTyApp #

Arguments

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

Make an iterated type application. Each TyApp node uses the annotation associated with the corresponding argument.

mkIterTyAppNoAnn #

Arguments

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

Make an iterated type application with no annotation.

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

Make an iterated function kind.

mkFreshTermLet #

Arguments

:: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a)
=> Type tyname uni a	the type of binding
-> t a	the term bound to the fresh variable
-> m (t a, t a -> t a)	the fresh Var and a function that takes an "in" term to construct the Let

A helper to create a single, fresh strict binding; It returns the fresh bound Variable and a function `Term -> Term`, expecting an "in-Term" to form a let-expression.

headSpineToTerm :: TermLike term tyname name uni fun => ann -> MonoHeadSpine err (term ann) -> Either err (term ann) #

apply the head of the application to the arguments iteratively.

headSpineToTermNoAnn :: TermLike term tyname name uni fun => MonoHeadSpine err (term ()) -> Either err (term ()) #

headSpineToTerm but without annotation.