Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 ∷ ∀ k (a ∷ k) uni tyname ann. ann → uni (Esc a) → Type tyname uni ann
- mkTyBuiltin ∷ ∀ a (x ∷ a) uni ann tyname. uni `HasTypeLevel` x ⇒ ann → Type tyname uni ann
- mkConstantOf ∷ ∀ a uni fun term tyname name ann. TermLike term tyname name uni fun ⇒ ann → uni (Esc a) → a → term ann
- mkConstant ∷ ∀ 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 ⇒ ann → 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 {}
- 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 ⇒ HeadSpine (term ()) → term ()
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.
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
TermLike (Term name uni fun) TyName name uni fun Source # | |
Defined in UntypedPlutusCore.Core.Type 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 # | |
Defined in PlutusCore.MkPlc 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
type UniOf (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism | |
type UniOf (SomeConstant uni rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism | |
type UniOf (CkValue uni fun) Source # | |
Defined in PlutusCore.Evaluation.Machine.Ck | |
type UniOf (CekValue uni fun ann) Source # | |
type UniOf (Term name uni fun ann) Source # | |
Defined in UntypedPlutusCore.Core.Type | |
type UniOf (Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type |
type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x) Source #
Specifies that the given type is a built-in one and can be embedded into a Kind
.
type HasTermLevel uni = Includes uni Source #
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) Source #
The product of HasTypeLevel
and HasTermLevel
.
mkTyBuiltinOf ∷ ∀ 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 ∷ ∀ a (x ∷ a) uni ann tyname. uni `HasTypeLevel` 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 ∷ ∀ 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 ∷ ∀ a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `HasTermLevel` 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 ann Source #
A "variable declaration", i.e. a name and a type for a variable.
VarDecl | |
|
Instances
(PrettyReadableBy configName tyname, PrettyReadableBy configName name, PrettyUni uni) ⇒ PrettyBy (PrettyConfigReadable configName) (VarDecl tyname name uni ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Readable prettyBy ∷ PrettyConfigReadable configName → VarDecl tyname name uni ann → Doc ann0 Source # prettyListBy ∷ PrettyConfigReadable configName → [VarDecl tyname name uni ann] → Doc ann0 Source # | |
Functor (VarDecl tyname name uni) Source # | |
Generic (VarDecl tyname name uni ann) Source # | |
(GShow uni, Show ann, Show name, Show tyname) ⇒ Show (VarDecl tyname name uni ann) Source # | |
(Closed uni, Flat ann, Flat tyname, Flat name) ⇒ Flat (VarDecl tyname name uni ann) Source # | |
HasUnique name TermUnique ⇒ HasUnique (VarDecl tyname name uni ann) TermUnique Source # | |
Defined in PlutusCore.Core.Type | |
type Rep (VarDecl tyname name uni ann) Source # | |
Defined in PlutusCore.Core.Type type Rep (VarDecl tyname name uni ann) = D1 ('MetaData "VarDecl" "PlutusCore.Core.Type" "plutus-core-1.36.0.0-inplace" '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.
TyVarDecl | |
|
Instances
data TyDecl tyname uni ann Source #
A "type declaration", i.e. a kind for a type.
TyDecl | |
|
Instances
Functor (TyDecl tyname uni) Source # | |
Generic (TyDecl tyname uni ann) Source # | |
(GShow uni, Show ann, Show tyname) ⇒ Show (TyDecl tyname uni ann) Source # | |
type Rep (TyDecl tyname uni ann) Source # | |
Defined in PlutusCore.Core.Type type Rep (TyDecl tyname uni ann) = D1 ('MetaData "TyDecl" "PlutusCore.Core.Type" "plutus-core-1.36.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))))) |
A definition. Pretty much just a pair with more descriptive names.
Instances
Generic (Def var val) Source # | |
(Show var, Show val) ⇒ Show (Def var val) Source # | |
(Eq var, Eq val) ⇒ Eq (Def var val) Source # | |
(Ord var, Ord val) ⇒ Ord (Def var val) Source # | |
Defined in PlutusCore.MkPlc | |
type Rep (Def var val) Source # | |
Defined in PlutusCore.MkPlc type Rep (Def var val) = D1 ('MetaData "Def" "PlutusCore.MkPlc" "plutus-core-1.36.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))) |
type TermDef term tyname name uni ann = Def (VarDecl tyname name uni 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.
FunctionType | |
|
data FunctionDef term tyname name uni fun ann Source #
A PLC function.
FunctionDef | |
|
functionTypeToType ∷ FunctionType tyname uni ann → Type tyname uni ann Source #
Convert a FunctionType
to the corresponding Kind
.
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 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.
∷ 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.
∷ 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 ∷ 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.
∷ TermLike term tyname name uni fun | |
⇒ term () | f |
→ [term ()] | [ x0 ... xn ] |
→ term () | [f x0 ... xn ] |
Make an iterated application with no annotation.
∷ 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 Source #
Make an iterated function type.
mkIterLamAbs ∷ TermLike term tyname name uni fun ⇒ [VarDecl tyname name uni ann] → term ann → term ann Source #
Lambda abstract a list of names.
∷ 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.
∷ 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 Source #
Type abstract a list of names.
∷ 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.
Make an iterated type application with no annotation.
∷ (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 Var
iable and
a function `Term -> Term`, expecting an "in-Term" to form a let-expression.