plutus-core-1.36.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.Builtin.KnownTypeAst

Synopsis

Documentation

data TyNameRep (kind ∷ Type) Source #

Representation of a type variable: its name and unique and an implicit kind.

Constructors

TyNameRep Symbol Nat 

Instances

Instances details
(name ~ ('TyNameRep text uniq ∷ TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (MetaForall name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

Associated Types

type IsBuiltin uni (MetaForall name a) ∷ Bool Source #

type ToHoles uni (MetaForall name a) ∷ [Hole] Source #

type ToBinds uni acc (MetaForall name a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

KnownMonotype val args res ⇒ KnownPolytype ('[] ∷ [Some TyNameRep]) val args res Source #

Once we've run out of type-level arguments, we start handling term-level ones.

Instance details

Defined in PlutusCore.Builtin.Meaning

(TypeError NoStandalonePolymorphicDataErrMsg ∷ Constraint) ⇒ Contains uni (TyVarRepTyNameRep kind → kind) Source # 
Instance details

Defined in PlutusCore.Builtin.Polymorphism

Methods

knownUni ∷ uni (Esc TyVarRep) Source #

(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res) ⇒ KnownPolytype ('Some ('TyNameRep name uniq ∷ TyNameRep kind) ': binds) val args res Source #

Every type-level argument becomes a TypeSchemeAll.

Instance details

Defined in PlutusCore.Builtin.Meaning

type ToBinds uni acc (MetaForall name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

type ToBinds uni acc (MetaForall name a ∷ Type) = ToBinds uni (Insert ('Some name) acc) a
type IsBuiltin uni (MetaForall name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

type IsBuiltin uni (MetaForall name a ∷ Type) = 'False
type ToHoles uni (MetaForall name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

type ToHoles uni (MetaForall name a ∷ Type) = '[TypeHole a ∷ Hole]

data family TyVarRep (name ∷ TyNameRep kind) ∷ kind Source #

Representation of an intrinsically-kinded type variable: a name.

Instances

Instances details
(tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep a), KnownSymbol text, KnownNat uniq) ⇒ KnownTypeAst tyname uni (TyVarRep name ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyVarRep name) ∷ Bool Source #

type ToHoles uni (TyVarRep name) ∷ [Hole] Source #

type ToBinds uni acc (TyVarRep name) ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname uni () Source #

(TypeError NoStandalonePolymorphicDataErrMsg ∷ Constraint) ⇒ Contains uni (TyVarRepTyNameRep kind → kind) Source # 
Instance details

Defined in PlutusCore.Builtin.Polymorphism

Methods

knownUni ∷ uni (Esc TyVarRep) Source #

type ToBinds uni acc (TyVarRep name ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToBinds uni acc (TyVarRep name ∷ a) = Insert ('Some name) acc
type IsBuiltin uni (TyVarRep name ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type IsBuiltin uni (TyVarRep name ∷ a) = 'False
type ToHoles uni (TyVarRep name ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToHoles uni (TyVarRep name ∷ a) = '[] ∷ [Hole]

data family TyAppRep (fun ∷ dom → cod) (arg ∷ dom) ∷ cod Source #

Representation of an intrinsically-kinded type application: a function and an argument.

Instances

Instances details
(KnownTypeAst tyname uni fun, KnownTypeAst tyname uni arg) ⇒ KnownTypeAst tyname uni (TyAppRep fun arg ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyAppRep fun arg) ∷ Bool Source #

type ToHoles uni (TyAppRep fun arg) ∷ [Hole] Source #

type ToBinds uni acc (TyAppRep fun arg) ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname uni () Source #

type ToBinds uni acc (TyAppRep fun arg ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToBinds uni acc (TyAppRep fun arg ∷ a) = ToBinds uni (ToBinds uni acc fun) arg
type IsBuiltin uni (TyAppRep fun arg ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type IsBuiltin uni (TyAppRep fun arg ∷ a) = IsBuiltin uni fun && IsBuiltin uni arg
type ToHoles uni (TyAppRep fun arg ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToHoles uni (TyAppRep fun arg ∷ a) = '[RepHole fun ∷ Hole, RepHole arg ∷ Hole]

data family TyForallRep (name ∷ TyNameRep kind) (a ∷ Type) ∷ Type Source #

Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.

Instances

Instances details
(tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (TyForallRep name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyForallRep name a) ∷ Bool Source #

type ToHoles uni (TyForallRep name a) ∷ [Hole] Source #

type ToBinds uni acc (TyForallRep name a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

type ToBinds uni acc (TyForallRep name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToBinds uni acc (TyForallRep name a ∷ Type) = Delete ('Some name) (ToBinds uni acc a)
type IsBuiltin uni (TyForallRep name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type IsBuiltin uni (TyForallRep name a ∷ Type) = 'False
type ToHoles uni (TyForallRep name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

type ToHoles uni (TyForallRep name a ∷ Type) = '[RepHole a ∷ Hole]

data Hole Source #

The kind of holes.

data family RepHole x Source #

A hole in the Rep context.

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 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 HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x) Source #

The product of HasTypeLevel and HasTermLevel.

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.

data family TypeHole a Source #

A hole in the Type context.

type KnownBuiltinTypeAst tyname uni x = AllBuiltinArgs uni (KnownTypeAst tyname uni) x Source #

A constraint for "a is a KnownTypeAst by means of being included in uni".

class KnownTypeAst tyname uni x where Source #

This class allows one to convert the type-level Haskell representation of a Plutus type into the corresponding Plutus type. Associated type families are needed to help elaboration.

Depending on the universe converting a Haskell type to a Plutus team can give different results (e.g. Int can be a built-in type instead of being encoded via built-in Integer), hence this class takes a uni argument. Plus, elaboration is universe-specific too.

Minimal complete definition

Nothing

Associated Types

type IsBuiltin uni x ∷ Bool Source #

Whether x is a built-in type.

type IsBuiltin uni x = IsBuiltin uni (ElaborateBuiltin uni x)

type ToHoles uni x ∷ [Hole] Source #

Return every part of the type that can be a to-be-instantiated type variable. For example, in Integer there's no such types and in (a, b) it's the two arguments (a and b) and the same applies to a -> b (to mention a type that is not built-in).

type ToHoles uni x = ToHoles uni (ElaborateBuiltin uni x)

type ToBinds uni (acc ∷ [Some TyNameRep]) x ∷ [Some TyNameRep] Source #

Collect all unique variables (a variable consists of a textual name, a unique and a kind) in an accumulator and return the accumulator once a leaf is reached.

type ToBinds uni acc x = ToBinds uni acc (ElaborateBuiltin uni x)

Methods

typeAstType tyname uni () Source #

The Plutus counterpart of the x type.

default typeAstKnownTypeAst tyname uni (ElaborateBuiltin uni x) ⇒ Type tyname uni () Source #

Instances

Instances details
tyname ~ TyNameKnownTypeAst tyname DefaultUni Void Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Int16 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Int32 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Int64 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Int8 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Word16 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Word32 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Word64 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Word8 Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni ByteStringKnownTypeAst tyname DefaultUni ByteString Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni ElementKnownTypeAst tyname DefaultUni Element Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni ElementKnownTypeAst tyname DefaultUni Element Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni MlResultKnownTypeAst tyname DefaultUni MlResult Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni DataKnownTypeAst tyname DefaultUni Data Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni IntegerCostedLiterally Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni NumBytesCostedAsNumWords Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni TextKnownTypeAst tyname DefaultUni Text Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni IntegerKnownTypeAst tyname DefaultUni Integer Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Natural Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni () ⇒ KnownTypeAst tyname DefaultUni () Source # 
Instance details

Defined in PlutusCore.Default.Universe

Associated Types

type IsBuiltin DefaultUni () ∷ Bool Source #

type ToHoles DefaultUni () ∷ [Hole] Source #

type ToBinds DefaultUni acc () ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni BoolKnownTypeAst tyname DefaultUni Bool Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Int Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni Word Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType tyname DefaultUni () Source #

KnownTypeAst tyname DefaultUni a ⇒ KnownTypeAst tyname DefaultUni (ListCostedByLength a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

typeAstType0 tyname DefaultUni () Source #

KnownBuiltinTypeAst tyname DefaultUni [a] ⇒ KnownTypeAst tyname DefaultUni ([a] ∷ Type) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Associated Types

type IsBuiltin DefaultUni [a] ∷ Bool Source #

type ToHoles DefaultUni [a] ∷ [Hole] Source #

type ToBinds DefaultUni acc [a] ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname DefaultUni () Source #

KnownTypeAst tyname uni a ⇒ KnownTypeAst tyname uni (BuiltinResult a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (BuiltinResult a) ∷ Bool Source #

type ToHoles uni (BuiltinResult a) ∷ [Hole] Source #

type ToBinds uni acc (BuiltinResult a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

KnownTypeAst tyname uni a ⇒ KnownTypeAst tyname uni (EvaluationResult a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (EvaluationResult a) ∷ Bool Source #

type ToHoles uni (EvaluationResult a) ∷ [Hole] Source #

type ToBinds uni acc (EvaluationResult a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

(tyname ~ TyName, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (PlcListRep a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

Associated Types

type IsBuiltin uni (PlcListRep a) ∷ Bool Source #

type ToHoles uni (PlcListRep a) ∷ [Hole] Source #

type ToBinds uni acc (PlcListRep a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

KnownBuiltinTypeAst tyname DefaultUni (a, b) ⇒ KnownTypeAst tyname DefaultUni ((a, b) ∷ Type) Source # 
Instance details

Defined in PlutusCore.Default.Universe

Associated Types

type IsBuiltin DefaultUni (a, b) ∷ Bool Source #

type ToHoles DefaultUni (a, b) ∷ [Hole] Source #

type ToBinds DefaultUni acc (a, b) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname DefaultUni () Source #

KnownTypeAst tyname uni rep ⇒ KnownTypeAst tyname uni (Opaque val rep ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (Opaque val rep) ∷ Bool Source #

type ToHoles uni (Opaque val rep) ∷ [Hole] Source #

type ToBinds uni acc (Opaque val rep) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

KnownTypeAst tyname uni rep ⇒ KnownTypeAst tyname uni (SomeConstant uni rep ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (SomeConstant uni rep) ∷ Bool Source #

type ToHoles uni (SomeConstant uni rep) ∷ [Hole] Source #

type ToBinds uni acc (SomeConstant uni rep) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

(KnownTypeAst tyname uni a, KnownTypeAst tyname uni b) ⇒ KnownTypeAst tyname uni (a → b ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (a → b) ∷ Bool Source #

type ToHoles uni (a → b) ∷ [Hole] Source #

type ToBinds uni acc (a → b) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

Contains uni f ⇒ KnownTypeAst tyname uni (BuiltinHead f ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (BuiltinHead f) ∷ Bool Source #

type ToHoles uni (BuiltinHead f) ∷ [Hole] Source #

type ToBinds uni acc (BuiltinHead f) ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname uni () Source #

(tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep a), KnownSymbol text, KnownNat uniq) ⇒ KnownTypeAst tyname uni (TyVarRep name ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyVarRep name) ∷ Bool Source #

type ToHoles uni (TyVarRep name) ∷ [Hole] Source #

type ToBinds uni acc (TyVarRep name) ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname uni () Source #

(tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (TyForallRep name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyForallRep name a) ∷ Bool Source #

type ToHoles uni (TyForallRep name a) ∷ [Hole] Source #

type ToBinds uni acc (TyForallRep name a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

(name ~ ('TyNameRep text uniq ∷ TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (MetaForall name a ∷ Type) Source # 
Instance details

Defined in PlutusCore.Examples.Builtins

Associated Types

type IsBuiltin uni (MetaForall name a) ∷ Bool Source #

type ToHoles uni (MetaForall name a) ∷ [Hole] Source #

type ToBinds uni acc (MetaForall name a) ∷ [Some TyNameRep] Source #

Methods

typeAstType0 tyname uni () Source #

(KnownTypeAst tyname uni fun, KnownTypeAst tyname uni arg) ⇒ KnownTypeAst tyname uni (TyAppRep fun arg ∷ a) Source # 
Instance details

Defined in PlutusCore.Builtin.KnownTypeAst

Associated Types

type IsBuiltin uni (TyAppRep fun arg) ∷ Bool Source #

type ToHoles uni (TyAppRep fun arg) ∷ [Hole] Source #

type ToBinds uni acc (TyAppRep fun arg) ∷ [Some TyNameRep] Source #

Methods

typeAstType tyname uni () Source #

toTypeAst ∷ ∀ a tyname uni (x ∷ a) proxy. KnownTypeAst tyname uni x ⇒ proxy x → Type tyname uni () Source #

Return the Plutus counterpart of the x type.

type family Insert x xs where ... Source #

Insert x into xs unless it's already there.

Equations

Insert x '[] = '[x] 
Insert x (x : xs) = x ': xs 
Insert x (y : xs) = y ': Insert x xs 

type family Delete x xs where ... Source #

Delete the first x from a list. Which is okay since we only ever put things in once.

Equations

Delete _ '[] = '[] 
Delete x (x ': xs) = xs 
Delete x (y ': xs) = y ': Delete x xs