Safe Haskell	None
Language	Haskell2010

PlutusCore.MkPlc

Synopsis

class TermLike (term :: Type -> Type) tyname name (uni :: Type -> Type) 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 :: Type -> Type) (x :: a) = KnownTypeAst Void uni (ElaborateBuiltin uni x)
type HasTermLevel (uni :: Type -> Type) = Includes uni :: a -> Constraint
type HasTypeAndTermLevel (uni :: Type -> Type) (x :: a) = (HasTypeLevel uni x, HasTermLevel uni x)
mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltin :: forall a (x :: a) (uni :: Type -> Type) ann tyname. HasTypeLevel uni 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 :: Type -> Type) fun term tyname name ann. (TermLike term tyname name uni fun, HasTermLevel uni a) => ann -> a -> term ann
data VarDecl tyname name (uni :: Type -> Type) 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 :: Type -> Type) ann = TyDecl {
- _tyDeclAnn :: ann
- _tyDeclType :: Type tyname uni ann
- _tyDeclKind :: Kind ann
}
mkVar :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => VarDecl tyname name uni ann -> term ann
mkTyVar :: forall ann tyname (uni :: Type -> Type). ann -> TyVarDecl tyname ann -> Type tyname uni ann
tyDeclVar :: forall tyname ann (uni :: Type -> Type). TyVarDecl tyname ann -> TyDecl tyname uni ann
data Def var val = Def {
- defVar :: var
- defVal :: val
}
embedTerm :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
type TermDef (term :: Type -> Type) tyname name (uni :: Type -> Type) ann = Def (VarDecl tyname name uni ann) (term ann)
type TypeDef tyname (uni :: Type -> Type) ann = Def (TyVarDecl tyname ann) (Type tyname uni ann)
data FunctionType tyname (uni :: Type -> Type) ann = FunctionType {
- _functionTypeAnn :: ann
- _functionTypeDom :: Type tyname uni ann
- _functionTypeCod :: Type tyname uni ann
}
data FunctionDef (term :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) ann = FunctionDef {
- _functionDefAnn :: ann
- _functionDefName :: name
- _functionDefType :: FunctionType tyname uni ann
- _functionDefTerm :: term ann
}
functionTypeToType :: forall tyname (uni :: Type -> Type) ann. FunctionType tyname uni ann -> Type tyname uni ann
functionDefToType :: forall {k} (term :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) ann. FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefVarDecl :: forall {k} (term :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) ann. FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni ann
mkFunctionDef :: forall {k} ann name tyname (uni :: Type -> Type) term (fun :: k). ann -> name -> Type tyname uni ann -> term ann -> Maybe (FunctionDef term tyname name uni fun ann)
mkImmediateLamAbs :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => ann -> TermDef term tyname name uni ann -> term ann -> term ann
mkImmediateTyAbs :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => ann -> TypeDef tyname uni ann -> term ann -> term ann
mkIterTyForall :: forall tyname ann (uni :: Type -> Type). [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam :: forall tyname ann (uni :: Type -> Type). [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterApp :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => term ann -> [(ann, term ann)] -> term ann
mkIterAppNoAnn :: forall term tyname name (uni :: Type -> Type) fun. TermLike term tyname name uni fun => term () -> [term ()] -> term ()
(@@) :: forall term tyname name (uni :: Type -> Type) fun. TermLike term tyname name uni fun => term () -> [term ()] -> term ()
mkIterTyFun :: forall ann tyname (uni :: Type -> Type). ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterLamAbs :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => [VarDecl tyname name uni ann] -> term ann -> term ann
mkIterInst :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInstNoAnn :: forall term tyname name (uni :: Type -> Type) fun. TermLike term tyname name uni fun => term () -> [Type tyname uni ()] -> term ()
mkIterTyAbs :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyApp :: forall tyname (uni :: Type -> Type) ann. Type tyname uni ann -> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyAppNoAnn :: forall tyname (uni :: Type -> Type). Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann
mkFreshTermLet :: forall m t tyname (uni :: Type -> Type) fun a. (MonadQuote m, TermLike t tyname Name uni fun, Monoid a) => Type tyname uni a -> t a -> m (t a, t a -> t a)
headSpineToTerm :: forall term tyname name (uni :: Type -> Type) fun ann err. TermLike term tyname name uni fun => ann -> MonoHeadSpine err (term ann) -> Either err (term ann)
headSpineToTermNoAnn :: forall term tyname name (uni :: Type -> Type) fun err. TermLike term tyname name uni fun => MonoHeadSpine err (term ()) -> Either err (term ())

Documentation

class TermLike (term :: Type -> Type) tyname name (uni :: Type -> Type) 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, constr, kase

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 #

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

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

termLet :: ann -> TermDef term tyname name uni 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 # constr :: ann -> Type TyName uni ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann Source # kase :: ann -> Type TyName uni ann -> Term name uni fun ann -> [Term name uni fun ann] -> Term name uni fun ann Source # termLet :: ann -> TermDef (Term name uni fun) TyName name uni 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 # constr :: ann -> Type tyname uni ann -> Word64 -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann Source # kase :: ann -> Type tyname uni ann -> Term tyname name uni fun ann -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann Source # termLet :: ann -> TermDef (Term tyname name uni fun) tyname name uni 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 (SomeConstant uni rep) Source #
Instance details Defined in PlutusCore.Builtin.Polymorphism type UniOf (SomeConstant uni rep) = uni
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 ann) Source #
Instance details Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type UniOf (CekValue uni fun ann) = 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 HasTypeLevel (uni :: Type -> Type) (x :: a) = KnownTypeAst Void uni (ElaborateBuiltin uni x) Source #

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

type HasTermLevel (uni :: Type -> Type) = Includes uni :: a -> Constraint Source #

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

type HasTypeAndTermLevel (uni :: Type -> Type) (x :: a) = (HasTypeLevel uni x, HasTermLevel uni x) Source #

The product of HasTypeLevel and HasTermLevel.

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 a (x :: a) (uni :: Type -> Type) ann tyname. HasTypeLevel uni x => ann -> Type tyname uni ann Source #

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

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

mkConstant :: forall a (uni :: Type -> Type) fun term tyname name ann. (TermLike term tyname name uni fun, HasTermLevel uni 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 :: Type -> Type) 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

(PrettyReadableBy configName tyname, PrettyReadableBy configName name, PrettyUni uni) => PrettyBy (PrettyConfigReadable configName) (VarDecl tyname name uni ann) Source #

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 #

Functor (VarDecl tyname name uni) Source #

Instance details

Defined in PlutusCore.Core.Type

Methods

fmap :: (a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b Source #

(<$) :: a -> VarDecl tyname name uni b -> VarDecl tyname name uni a Source #

Generic (VarDecl tyname name uni ann) Source #

Instance details

Defined in PlutusCore.Core.Type

Associated Types

type Rep (VarDecl tyname name uni ann)

Instance details

Defined in PlutusCore.Core.Type

type Rep (VarDecl tyname name uni ann) = D1 ('MetaData "VarDecl" "PlutusCore.Core.Type" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" '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)))))

Methods

from :: VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x Source #

to :: Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann Source #

(GShow uni, Show ann, Show name, Show tyname) => Show (VarDecl tyname name uni ann) Source #

Instance details

Defined in PlutusCore.Core.Type

Methods

showsPrec :: Int -> VarDecl tyname name uni ann -> ShowS Source #

show :: VarDecl tyname name uni ann -> String Source #

showList :: [VarDecl tyname name uni ann] -> ShowS Source #

(Closed uni, Flat ann, Flat tyname, Flat name) => Flat (VarDecl tyname name uni ann)

Instance details

Defined in PlutusCore.FlatInstances

Methods

encode :: VarDecl tyname name uni ann -> Encoding

decode :: Get (VarDecl tyname name uni ann)

size :: VarDecl tyname name uni ann -> NumBits -> NumBits

HasUnique name TermUnique => HasUnique (VarDecl tyname name uni ann) TermUnique Source #

Instance details

Defined in PlutusCore.Core.Type

Methods

unique :: Lens' (VarDecl tyname name uni ann) TermUnique Source #

type Rep (VarDecl tyname name uni ann) Source #

Instance details

Defined in PlutusCore.Core.Type

type Rep (VarDecl tyname name uni ann) = D1 ('MetaData "VarDecl" "PlutusCore.Core.Type" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" '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 #

PrettyReadableBy configName tyname => PrettyBy (PrettyConfigReadable configName) (TyVarDecl tyname ann) Source #

Instance details

Defined in PlutusCore.Core.Instance.Pretty.Readable

Methods

prettyBy :: PrettyConfigReadable configName -> TyVarDecl tyname ann -> Doc ann0 #

prettyListBy :: PrettyConfigReadable configName -> [TyVarDecl tyname ann] -> Doc ann0 #

Generic (TyVarDecl tyname ann) Source #

Instance details

Defined in PlutusCore.Core.Type

Associated Types

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-LXFqBsoUlXsJIEqLytHte7" '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)))))

Methods

from :: TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x Source #

to :: Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann Source #

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

(Flat ann, Flat tyname) => Flat (TyVarDecl tyname ann)

Instance details

Defined in PlutusCore.FlatInstances

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 #

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.60.0.0-LXFqBsoUlXsJIEqLytHte7" '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 :: Type -> Type) 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 #

Generic (TyDecl tyname uni ann) Source #

Instance details

Defined in PlutusCore.Core.Type

Associated Types

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-LXFqBsoUlXsJIEqLytHte7" '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)))))

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 #

(GShow uni, Show ann, Show tyname) => 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 #

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.60.0.0-LXFqBsoUlXsJIEqLytHte7" '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 :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => VarDecl tyname name uni ann -> term ann Source #

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

mkTyVar :: forall ann tyname (uni :: Type -> Type). ann -> TyVarDecl tyname ann -> Type tyname uni ann Source #

Make a TyVar referencing the given TyVarDecl.

tyDeclVar :: forall tyname ann (uni :: Type -> Type). 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

Generic (Def var val) Source #

Instance details

Defined in PlutusCore.MkPlc

Associated Types

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-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) (S1 ('MetaSel ('Just "defVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 var) :*: S1 ('MetaSel ('Just "defVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 val)))

Methods

from :: Def var val -> Rep (Def var val) x Source #

to :: Rep (Def var val) x -> 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 #

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

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.60.0.0-LXFqBsoUlXsJIEqLytHte7" '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 :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann Source #

type TermDef (term :: Type -> Type) tyname name (uni :: Type -> Type) ann = Def (VarDecl tyname name uni ann) (term ann) Source #

A term definition as a variable.

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

A type definition as a type variable.

data FunctionType tyname (uni :: Type -> Type) 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 :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) 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 :: forall tyname (uni :: Type -> Type) ann. FunctionType tyname uni ann -> Type tyname uni ann Source #

Convert a FunctionType to the corresponding Type.

functionDefToType :: forall {k} (term :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) ann. FunctionDef term tyname name uni fun ann -> Type tyname uni ann Source #

Get the type of a FunctionDef.

functionDefVarDecl :: forall {k} (term :: Type -> Type) tyname name (uni :: Type -> Type) (fun :: k) ann. FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni ann Source #

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

mkFunctionDef :: forall {k} ann name tyname (uni :: Type -> Type) term (fun :: k). 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

:: forall term tyname name (uni :: Type -> Type) fun ann. 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 Source #

Arguments

:: forall term tyname name (uni :: Type -> Type) fun ann. 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 :: forall tyname ann (uni :: Type -> Type). [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Universally quantify a list of names.

mkIterTyLam :: forall tyname ann (uni :: Type -> Type). [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Lambda abstract a list of names.

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

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

mkIterAppNoAnn Source #

Arguments

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

Make an iterated application with no annotation.

(@@) Source #

Arguments

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

An infix synonym for mkIterAppNoAnn

mkIterTyFun :: forall ann tyname (uni :: Type -> Type). ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Make an iterated function type.

mkIterLamAbs :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => [VarDecl tyname name uni ann] -> term ann -> term ann Source #

Lambda abstract a list of names.

mkIterInst Source #

Arguments

:: forall term tyname name (uni :: Type -> Type) fun ann. 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 Source #

Arguments

:: forall term tyname name (uni :: Type -> Type) fun. 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 :: forall term tyname name (uni :: Type -> Type) fun ann. TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann Source #

Type abstract a list of names.

mkIterTyApp Source #

Arguments

:: forall tyname (uni :: Type -> Type) ann. 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 Source #

Arguments

:: forall tyname (uni :: Type -> Type). 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 Source #

Make an iterated function kind.

mkFreshTermLet Source #

Arguments

:: forall m t tyname (uni :: Type -> Type) fun a. (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 :: forall term tyname name (uni :: Type -> Type) fun ann err. TermLike term tyname name uni fun => ann -> MonoHeadSpine err (term ann) -> Either err (term ann) Source #

apply the head of the application to the arguments iteratively.

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

headSpineToTerm but without annotation.