| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore
Synopsis
- parseProgram :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Program TyName Name DefaultUni DefaultFun SrcSpan)
- parseTerm :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Term TyName Name DefaultUni DefaultFun SrcSpan)
- parseType :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Type TyName DefaultUni SrcSpan)
- data SourcePos
- data SrcSpan = SrcSpan {
- srcSpanFile :: FilePath
- srcSpanSLine :: Int
- srcSpanSCol :: Int
- srcSpanELine :: Int
- srcSpanECol :: Int
- data SrcSpans
- data Some (tag :: k -> Type) where
- data SomeTypeIn uni = forall k (a :: k). SomeTypeIn !(uni (Esc a))
- data Kinded uni ta where
- data ValueOf uni a = ValueOf !(uni (Esc a)) !a
- someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni)
- someValue :: forall a uni. uni `Contains` a => a -> Some (ValueOf uni)
- someValueType :: Some (ValueOf uni) -> SomeTypeIn uni
- data Esc a
- class Contains uni a where
- class Closed uni where
- type Everywhere uni (constr :: Type -> Constraint) :: Constraint
- encodeUni :: uni a -> [Int]
- withDecodedUni :: (forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r) -> DecodeUniM r
- bring :: uni `Everywhere` constr => proxy constr -> uni (Esc a) -> (constr a => r) -> r
- type family EverywhereAll uni constrs where ...
- knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a)
- class GShow (t :: k -> Type) where
- gshowsPrec :: forall (a :: k). Int -> t a -> ShowS
- show :: Show a => a -> String
- class GEq (f :: k -> Type) where
- class HasUniApply (uni :: Type -> Type) where
- checkStar :: forall uni a (x :: a). Typeable a => uni (Esc x) -> Maybe (a :~: Type)
- withApplicable :: forall (a :: Type) (ab :: Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) => uni (Esc (f :: ab)) -> uni (Esc (x :: a)) -> (forall (b :: Type). (Typeable b, ab ~ (a -> b)) => m r) -> m r
- data (a :: k) :~: (b :: k) where
- type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2
- 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)
- data DefaultUni a where
- DefaultUniInteger :: DefaultUni (Esc Integer)
- DefaultUniByteString :: DefaultUni (Esc ByteString)
- DefaultUniString :: DefaultUni (Esc Text)
- DefaultUniUnit :: DefaultUni (Esc ())
- DefaultUniBool :: DefaultUni (Esc Bool)
- DefaultUniProtoList :: DefaultUni (Esc List)
- DefaultUniProtoPair :: DefaultUni (Esc (,))
- DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
- DefaultUniData :: DefaultUni (Esc Data)
- DefaultUniBLS12_381_G1_Element :: DefaultUni (Esc Element)
- DefaultUniBLS12_381_G2_Element :: DefaultUni (Esc Element)
- DefaultUniBLS12_381_MlResult :: DefaultUni (Esc MlResult)
- pattern DefaultUniList :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}. () => forall. (a ~ Esc (f a1), Esc f ~ Esc List) => DefaultUni (Esc a1) -> DefaultUni a
- pattern DefaultUniPair :: forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4} {f2 :: k3 -> k4} {a2 :: k3}. () => forall. (a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) => DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
- data DefaultFun
- = AddInteger
- | SubtractInteger
- | MultiplyInteger
- | DivideInteger
- | QuotientInteger
- | RemainderInteger
- | ModInteger
- | EqualsInteger
- | LessThanInteger
- | LessThanEqualsInteger
- | AppendByteString
- | ConsByteString
- | SliceByteString
- | LengthOfByteString
- | IndexByteString
- | EqualsByteString
- | LessThanByteString
- | LessThanEqualsByteString
- | Sha2_256
- | Sha3_256
- | Blake2b_256
- | VerifyEd25519Signature
- | VerifyEcdsaSecp256k1Signature
- | VerifySchnorrSecp256k1Signature
- | AppendString
- | EqualsString
- | EncodeUtf8
- | DecodeUtf8
- | IfThenElse
- | ChooseUnit
- | Trace
- | FstPair
- | SndPair
- | ChooseList
- | MkCons
- | HeadList
- | TailList
- | NullList
- | ChooseData
- | ConstrData
- | MapData
- | ListData
- | IData
- | BData
- | UnConstrData
- | UnMapData
- | UnListData
- | UnIData
- | UnBData
- | EqualsData
- | SerialiseData
- | MkPairData
- | MkNilData
- | MkNilPairData
- | Bls12_381_G1_add
- | Bls12_381_G1_neg
- | Bls12_381_G1_scalarMul
- | Bls12_381_G1_equal
- | Bls12_381_G1_hashToGroup
- | Bls12_381_G1_compress
- | Bls12_381_G1_uncompress
- | Bls12_381_G2_add
- | Bls12_381_G2_neg
- | Bls12_381_G2_scalarMul
- | Bls12_381_G2_equal
- | Bls12_381_G2_hashToGroup
- | Bls12_381_G2_compress
- | Bls12_381_G2_uncompress
- | Bls12_381_millerLoop
- | Bls12_381_mulMlResult
- | Bls12_381_finalVerify
- | Keccak_256
- | Blake2b_224
- | IntegerToByteString
- | ByteStringToInteger
- | AndByteString
- | OrByteString
- | XorByteString
- | ComplementByteString
- | ReadBit
- | WriteBits
- | ReplicateByte
- | ShiftByteString
- | RotateByteString
- | CountSetBits
- | FindFirstSetBit
- | Ripemd_160
- | ExpModInteger
- data Term tyname name uni fun ann
- = Var ann name
- | LamAbs ann name (Type tyname uni ann) (Term tyname name uni fun ann)
- | Apply ann (Term tyname name uni fun ann) (Term tyname name uni fun ann)
- | TyAbs ann tyname (Kind ann) (Term tyname name uni fun ann)
- | TyInst ann (Term tyname name uni fun ann) (Type tyname uni ann)
- | IWrap ann (Type tyname uni ann) (Type tyname uni ann) (Term tyname name uni fun ann)
- | Unwrap ann (Term tyname name uni fun ann)
- | Constr ann (Type tyname uni ann) Word64 [Term tyname name uni fun ann]
- | Case ann (Type tyname uni ann) (Term tyname name uni fun ann) [Term tyname name uni fun ann]
- | Constant ann (Some (ValueOf uni))
- | Builtin ann fun
- | Error ann (Type tyname uni ann)
- termSubterms :: Traversal' (Term tyname name uni fun ann) (Term tyname name uni fun ann)
- termSubtypes :: Traversal' (Term tyname name uni fun ann) (Type tyname uni ann)
- termMapNames :: forall tyname tyname' name name' uni fun ann. (tyname -> tyname') -> (name -> name') -> Term tyname name uni fun ann -> Term tyname' name' uni fun ann
- programMapNames :: forall tyname tyname' name name' uni fun ann. (tyname -> tyname') -> (name -> name') -> Program tyname name uni fun ann -> Program tyname' name' uni fun ann
- type family UniOf a :: Type -> Type
- data Type tyname uni ann
- = TyVar ann tyname
- | TyFun ann (Type tyname uni ann) (Type tyname uni ann)
- | TyIFix ann (Type tyname uni ann) (Type tyname uni ann)
- | TyForall ann tyname (Kind ann) (Type tyname uni ann)
- | TyBuiltin ann (SomeTypeIn uni)
- | TyLam ann tyname (Kind ann) (Type tyname uni ann)
- | TyApp ann (Type tyname uni ann) (Type tyname uni ann)
- | TySOP ann [[Type tyname uni ann]]
- typeSubtypes :: Traversal' (Type tyname uni ann) (Type tyname uni ann)
- typeMapNames :: forall tyname tyname' uni ann. (tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann
- data Kind ann
- toPatFuncKind :: Kind () -> Kind ()
- fromPatFuncKind :: Kind () -> Maybe (Kind ())
- argsFunKind :: Kind ann -> [Kind ann]
- data ParserError
- data Version = Version {}
- data Program tyname name uni fun ann = Program {}
- data Name = Name {
- _nameText :: Text
- _nameUnique :: Unique
- newtype TyName = TyName {}
- newtype Unique = Unique {}
- newtype UniqueMap unique a = UniqueMap {
- unUniqueMap :: IntMap a
- newtype UniqueSet unique = UniqueSet {}
- newtype Normalized a = Normalized {
- unNormalized :: a
- latestVersion :: Version
- termAnn :: Term tyname name uni fun ann -> ann
- typeAnn :: Type tyname uni ann -> ann
- tyVarDeclAnn :: forall tyname ann. Lens' (TyVarDecl tyname ann) ann
- tyVarDeclName :: forall tyname ann tyname. Lens (TyVarDecl tyname ann) (TyVarDecl tyname ann) tyname tyname
- tyVarDeclKind :: forall tyname ann. Lens' (TyVarDecl tyname ann) (Kind ann)
- varDeclAnn :: forall tyname name uni ann. Lens' (VarDecl tyname name uni ann) ann
- varDeclName :: forall tyname name uni ann name. Lens (VarDecl tyname name uni ann) (VarDecl tyname name uni ann) name name
- varDeclType :: forall tyname name uni ann tyname uni. Lens (VarDecl tyname name uni ann) (VarDecl tyname name uni ann) (Type tyname uni ann) (Type tyname uni ann)
- tyDeclAnn :: forall tyname uni ann. Lens' (TyDecl tyname uni ann) ann
- tyDeclType :: forall tyname uni ann tyname uni. Lens (TyDecl tyname uni ann) (TyDecl tyname uni ann) (Type tyname uni ann) (Type tyname uni ann)
- tyDeclKind :: forall tyname uni ann. Lens' (TyDecl tyname uni ann) (Kind ann)
- progAnn :: forall tyname name uni fun ann. Lens' (Program tyname name uni fun ann) ann
- progVer :: forall tyname name uni fun ann. Lens' (Program tyname name uni fun ann) Version
- progTerm :: forall tyname name uni fun ann tyname name uni fun. Lens (Program tyname name uni fun ann) (Program tyname name uni fun ann) (Term tyname name uni fun ann) (Term tyname name uni fun ann)
- mapFun :: (fun -> fun') -> Term tyname name uni fun ann -> Term tyname name uni fun' ann
- newtype DeBruijn = DeBruijn {}
- newtype TyDeBruijn = TyDeBruijn DeBruijn
- data NamedDeBruijn = NamedDeBruijn {
- ndbnString :: !Text
- ndbnIndex :: !Index
- newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
- deBruijnTerm :: (AsFreeVariableError e, MonadError e m) => Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
- unDeBruijnTerm :: (MonadQuote m, AsFreeVariableError e, MonadError e m) => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann)
- type family HasUniques a :: Constraint
- class Rename a where
- rename :: MonadQuote m => a -> m a
- module PlutusCore.TypeCheck
- normalizeTypesIn :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, MonadNormalizeType uni m) => Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
- normalizeTypesInProgram :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, MonadNormalizeType uni m) => Program tyname name uni fun ann -> m (Program tyname name uni fun ann)
- class AsTypeError r term uni fun ann | r -> term uni fun ann where
- _TypeError :: Prism' r (TypeError term uni fun ann)
- _KindMismatch :: Prism' r (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ())
- _TypeMismatch :: Prism' r (ann, term, ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ()))
- _TyNameMismatch :: Prism' r (ann, TyName, TyName)
- _NameMismatch :: Prism' r (ann, Name, Name)
- _FreeTypeVariableE :: Prism' r (ann, TyName)
- _FreeVariableE :: Prism' r (ann, Name)
- _UnknownBuiltinFunctionE :: Prism' r (ann, fun)
- data TypeError term uni fun ann
- data Error uni fun ann
- = ParseErrorE !ParserErrorBundle
- | UniqueCoherencyErrorE !(UniqueError ann)
- | TypeErrorE !(TypeError (Term TyName Name uni fun ()) uni fun ann)
- | NormCheckErrorE !(NormCheckError TyName Name uni fun ann)
- | FreeVariableErrorE !FreeVariableError
- class AsError r uni fun ann | r -> uni fun ann where
- _Error :: Prism' r (Error uni fun ann)
- _ParseErrorE :: Prism' r ParserErrorBundle
- _UniqueCoherencyErrorE :: Prism' r (UniqueError ann)
- _TypeErrorE :: Prism' r (TypeError (Term TyName Name uni fun ()) uni fun ann)
- _NormCheckErrorE :: Prism' r (NormCheckError TyName Name uni fun ann)
- _FreeVariableErrorE :: Prism' r FreeVariableError
- data NormCheckError tyname name uni fun ann
- class AsNormCheckError r tyname name uni fun ann | r -> tyname name uni fun ann where
- _NormCheckError :: Prism' r (NormCheckError tyname name uni fun ann)
- _BadType :: Prism' r (ann, Type tyname uni ann, Text)
- _BadTerm :: Prism' r (ann, Term tyname name uni fun ann, Text)
- data UniqueError ann
- = MultiplyDefined !Unique !ann !ann
- | IncoherentUsage !Unique !ann !ann
- | FreeVariable !Unique !ann
- class AsUniqueError r ann | r -> ann where
- _UniqueError :: Prism' r (UniqueError ann)
- _MultiplyDefined :: Prism' r (Unique, ann, ann)
- _IncoherentUsage :: Prism' r (Unique, ann, ann)
- _FreeVariable :: Prism' r (Unique, ann)
- data FreeVariableError
- = FreeUnique !Unique
- | FreeIndex !Index
- class AsFreeVariableError r where
- _FreeVariableError :: Prism' r FreeVariableError
- _FreeUnique :: Prism' r Unique
- _FreeIndex :: Prism' r Index
- type Quote = QuoteT Identity
- runQuote :: Quote a -> a
- data QuoteT m a
- runQuoteT :: Monad m => QuoteT m a -> m a
- class Monad m => MonadQuote m
- liftQuote :: MonadQuote m => Quote a -> m a
- freshUnique :: MonadQuote m => m Unique
- freshName :: MonadQuote m => Text -> m Name
- freshTyName :: MonadQuote m => Text -> m TyName
- data EvaluationResult a
- applyProgram :: (MonadError ApplyProgramError m, Semigroup a) => Program tyname name uni fun a -> Program tyname name uni fun a -> m (Program tyname name uni fun a)
- termSize :: Term tyname name uni fun ann -> Size
- typeSize :: Type tyname uni ann -> Size
- kindSize :: Kind a -> Size
- programSize :: Program tyname name uni fun ann -> Size
- serialisedSize :: Flat a => a -> Integer
Parser
parseProgram :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Program TyName Name DefaultUni DefaultFun SrcSpan) Source #
parseTerm :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Term TyName Name DefaultUni DefaultFun SrcSpan) Source #
Parse a PLC term. The resulting program will have fresh names. The underlying monad must be capable of handling any parse errors.
parseType :: (AsParserErrorBundle e, MonadError e m, MonadQuote m) => Text -> m (Type TyName DefaultUni SrcSpan) Source #
Parse a PLC type. The resulting program will have fresh names. The underlying monad must be capable of handling any parse errors.
Instances
| Data SourcePos | |
Defined in Text.Megaparsec.Pos Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SourcePos -> c SourcePos Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SourcePos Source # toConstr :: SourcePos -> Constr Source # dataTypeOf :: SourcePos -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SourcePos) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SourcePos) Source # gmapT :: (forall b. Data b => b -> b) -> SourcePos -> SourcePos Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SourcePos -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SourcePos -> r Source # gmapQ :: (forall d. Data d => d -> u) -> SourcePos -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> SourcePos -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos Source # | |
| Generic SourcePos | |
| Read SourcePos | |
| Show SourcePos | |
| NFData SourcePos | |
Defined in Text.Megaparsec.Pos | |
| Eq SourcePos | |
| Ord SourcePos | |
Defined in Text.Megaparsec.Pos | |
| Pretty SourcePos Source # | |
Defined in PlutusCore.Error | |
| type Rep SourcePos | |
Defined in Text.Megaparsec.Pos type Rep SourcePos = D1 ('MetaData "SourcePos" "Text.Megaparsec.Pos" "megaparsec-9.6.1-2y4TSvMYdIdIGL4Xdwvkcx" 'False) (C1 ('MetaCons "SourcePos" 'PrefixI 'True) (S1 ('MetaSel ('Just "sourceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "sourceLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedUnpack) (Rec0 Pos) :*: S1 ('MetaSel ('Just "sourceColumn") 'NoSourceUnpackedness 'SourceStrict 'DecidedUnpack) (Rec0 Pos)))) | |
The span between two source locations.
This corresponds roughly to the SrcSpan used by GHC,
but we define our own version so we don't have to depend on ghc to use it.
The line and column numbers are 1-based, and the unit is Unicode code point (or Char).
Constructors
| SrcSpan | |
Fields
| |
Instances
Instances
Builtins
data Some (tag :: k -> Type) where #
Instances
| (Closed uni, Everywhere uni PrettyConst) => PrettyBy ConstConfig (Some (ValueOf uni)) Source # | |
Defined in PlutusCore.Pretty.PrettyConst Methods prettyBy :: ConstConfig -> Some (ValueOf uni) -> Doc ann # prettyListBy :: ConstConfig -> [Some (ValueOf uni)] -> Doc ann # | |
| Applicative m => Monoid (Some m) | |
| Applicative m => Semigroup (Some m) | |
| GRead f => Read (Some f) | |
| GShow tag => Show (Some tag) | |
| GNFData tag => NFData (Some tag) | |
Defined in Data.Some.Newtype | |
| (Closed uni, Everywhere uni Flat) => Flat (Some (ValueOf uni)) | |
| GEq tag => Eq (Some tag) | |
| GCompare tag => Ord (Some tag) | |
Defined in Data.Some.Newtype | |
| (Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) => Hashable (Some (ValueOf uni)) Source # | |
Defined in Universe.Core | |
| (Closed uni, Everywhere uni ExMemoryUsage) => ExMemoryUsage (Some (ValueOf uni)) Source # | |
Defined in PlutusCore.Evaluation.Machine.ExMemoryUsage | |
| (Closed uni, Everywhere uni PrettyConst) => Pretty (Some (ValueOf uni)) Source # | |
data SomeTypeIn uni Source #
A particular type from a universe.
Constructors
| forall k (a :: k). SomeTypeIn !(uni (Esc a)) |
Instances
data Kinded uni ta where Source #
Instances
| GShow uni => GShow (Kinded uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> Kinded uni a -> ShowS # | |
| (Typeable k, Contains uni a) => Contains (Kinded uni) (a :: k) Source # | A |
| Pretty (SomeTypeIn uni) => Pretty (SomeTypeIn (Kinded uni)) Source # | |
Defined in PlutusCore.Pretty.PrettyConst Methods pretty :: SomeTypeIn (Kinded uni) -> Doc ann # prettyList :: [SomeTypeIn (Kinded uni)] -> Doc ann # | |
| GShow uni => Show (Kinded uni ta) Source # | |
A value of a particular type from a universe.
Instances
someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni) Source #
Wrap a value into Some (ValueOf uni), given its explicit type tag.
someValue :: forall a uni. uni `Contains` a => a -> Some (ValueOf uni) Source #
Wrap a value into Some (ValueOf uni), provided its type is in the universe.
someValueType :: Some (ValueOf uni) -> SomeTypeIn uni Source #
class Contains uni a where Source #
A class for enumerating types and fully instantiated type formers that uni contains.
For example, a particular ExampleUni may have monomorphic types in it:
instance ExampleUni Contains Integer where ...
instance ExampleUni Contains Bool where ...
as well as polymorphic ones:
instance ExampleUni Contains [] where ...
instance ExampleUni Contains (,) where ...
as well as their instantiations:
instance ExampleUni Contains a => ExampleUni Contains [a] where ...
instance (ExampleUni Contains a, ExampleUni Contains b) => ExampleUni Contains (a, b) where ...
(a universe can have any subset of the mentioned sorts of types, for example it's fine to have instantiated polymorphic types and not have uninstantiated ones and vice versa)
Note that when used as a constraint of a function Contains does not allow you to directly
express things like "uni has the Integer, Bool and [] types and type formers",
because [] is not fully instantiated. So you can only say "uni has Integer, Bool,
[Integer], [Bool], [[Integer]], [[Bool]] etc" and such manual enumeration is annoying,
so we'd really like to be able to say that uni has lists of arbitrary built-in types
(including lists of lists etc). Contains does not allow that, but Includes does.
For example, in the body of the following definition:
foo :: (uni Includes Integer, uni Includes Bool, uni Includes []) => ...
foo = ...
you can make use of the fact that uni has lists of arbitrary included types (integers,
booleans and lists).
Hence most of the time opt for using the more flexible Includes.
Includes is defined in terms of Contains, so you only need to provide a Contains instance
per type from the universe and you'll get Includes for free.
Instances
class Closed uni where Source #
A universe is Closed, if it's known how to constrain every type from the universe and
every type can be encoded to / decoded from a sequence of integer tags.
The universe doesn't have to be finite and providing support for infinite universes is the
reason why we encode a type as a sequence of integer tags as opposed to a single integer tag.
For example, given
data U a where
UList :: !(U a) -> U [a]
UInt :: U IntUList (UList UInt) can be encoded to [0,0,1] where 0 and 1 are the integer tags of the
UList and UInt constructors, respectively.
Associated Types
type Everywhere uni (constr :: Type -> Constraint) :: Constraint Source #
A constrant for "constr a holds for any a from uni".
Methods
encodeUni :: uni a -> [Int] Source #
Encode a type as a sequence of Int tags.
The opposite of decodeUni.
withDecodedUni :: (forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r) -> DecodeUniM r Source #
Decode a type and feed it to the continuation.
bring :: uni `Everywhere` constr => proxy constr -> uni (Esc a) -> (constr a => r) -> r Source #
Bring a constr a instance in scope, provided a is a type from the universe and
constr holds for any type from the universe.
Instances
| Closed DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Associated Types type Everywhere DefaultUni constr Source # Methods encodeUni :: DefaultUni a -> [Int] Source # withDecodedUni :: (forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r) -> DecodeUniM r Source # bring :: Everywhere DefaultUni constr => proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r Source # | |
type family EverywhereAll uni constrs where ... Source #
Equations
| EverywhereAll uni '[] = () | |
| EverywhereAll uni (constr ': constrs) = (uni `Everywhere` constr, uni `EverywhereAll` constrs) |
knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a) Source #
Same as knownUni, but receives a proxy.
class GShow (t :: k -> Type) where #
Methods
gshowsPrec :: forall (a :: k). Int -> t a -> ShowS #
Instances
| GShow SNat | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS # | |
| GShow SChar | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SChar a -> ShowS # | |
| GShow SSymbol | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SSymbol a -> ShowS # | |
| GShow DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods gshowsPrec :: forall (a :: k). Int -> DefaultUni a -> ShowS # | |
| GShow uni => GShow (Kinded uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> Kinded uni a -> ShowS # | |
| (GShow uni, Closed uni, Everywhere uni Show) => GShow (ValueOf uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> ValueOf uni a -> ShowS # | |
| GShow (TypeRep :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k0). Int -> TypeRep a -> ShowS # | |
| GShow ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS # | |
| GShow (GOrdering a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (Product a b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> Product a b a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (Sum a b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> Sum a b a0 -> ShowS # | |
| GShow ((:~~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~~: a0) -> ShowS # | |
| (GShow a, GShow b) => GShow (a :*: b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :*: b) a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (a :+: b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :+: b) a0 -> ShowS # | |
class GEq (f :: k -> Type) where #
Instances
| GEq SNat | |
| GEq SChar | |
| GEq SSymbol | |
| GEq DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods geq :: forall (a :: k) (b :: k). DefaultUni a -> DefaultUni b -> Maybe (a :~: b) # | |
| (GEq uni, Closed uni, Everywhere uni Eq) => GEq (ValueOf uni :: Type -> Type) Source # | |
| GEq (TypeRep :: k -> Type) | |
| GEq ((:~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (Product a b :: k -> Type) | |
| (GEq a, GEq b) => GEq (Sum a b :: k -> Type) | |
| GEq ((:~~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (a :*: b :: k -> Type) | |
| (GEq f, GEq g) => GEq (f :+: g :: k -> Type) | |
class HasUniApply (uni :: Type -> Type) where Source #
A class for "uni has general type application".
Methods
uniApply :: forall k l (f :: k -> l) a. uni (Esc f) -> uni (Esc a) -> uni (Esc (f a)) Source #
Apply a type constructor to an argument.
Arguments
| :: uni tb | The type. |
| -> r | What to return if the type is not an application. |
| -> (forall k l (f :: k -> l) a. tb ~ Esc (f a) => uni (Esc f) -> uni (Esc a) -> r) | The continuation taking a function and an argument. |
| -> r |
Deconstruct a type application into the function and the argument and feed them to the continuation. If the type is not an application, then return the default value.
Instances
| HasUniApply DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods uniApply :: forall k l (f :: k -> l) (a :: k). DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a)) Source # matchUniApply :: DefaultUni tb -> r -> (forall k l (f :: k -> l) (a :: k). tb ~ Esc (f a) => DefaultUni (Esc f) -> DefaultUni (Esc a) -> r) -> r Source # | |
checkStar :: forall uni a (x :: a). Typeable a => uni (Esc x) -> Maybe (a :~: Type) Source #
Check if the kind of the given type from the universe is Type.
withApplicable :: forall (a :: Type) (ab :: Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) => uni (Esc (f :: ab)) -> uni (Esc (x :: a)) -> (forall (b :: Type). (Typeable b, ab ~ (a -> b)) => m r) -> m r Source #
Check if one type from the universe can be applied to another (i.e. check that the expected
kind of the argument matches the actual one) and call the continuation in the refined context.
Fail with mzero otherwise.
data (a :: k) :~: (b :: k) where infix 4 Source #
Propositional equality. If a :~: b is inhabited by some terminating
value, then the type a is the same as the type b. To use this equality
in practice, pattern-match on the a :~: b to get out the Refl constructor;
in the body of the pattern-match, the compiler knows that a ~ b.
Since: base-4.7.0.0
Instances
| Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| GNFData ((:~:) a :: k -> Type) | |
Defined in Data.GADT.DeepSeq | |
| GCompare ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal | |
| GEq ((:~:) a :: k -> Type) | |
| GRead ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS ((:~:) a) | |
| GShow ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS # | |
| NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| (a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source # toConstr :: (a :~: b) -> Constr Source # dataTypeOf :: (a :~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # | |
| a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b Source # pred :: (a :~: b) -> a :~: b Source # toEnum :: Int -> a :~: b Source # fromEnum :: (a :~: b) -> Int Source # enumFrom :: (a :~: b) -> [a :~: b] Source # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source # | |
| a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2 Source #
A constraint for "uni1 is a subuniverse of uni2".
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.
data DefaultUni a where Source #
The universe used by default.
Constructors
| DefaultUniInteger :: DefaultUni (Esc Integer) | |
| DefaultUniByteString :: DefaultUni (Esc ByteString) | |
| DefaultUniString :: DefaultUni (Esc Text) | |
| DefaultUniUnit :: DefaultUni (Esc ()) | |
| DefaultUniBool :: DefaultUni (Esc Bool) | |
| DefaultUniProtoList :: DefaultUni (Esc List) | |
| DefaultUniProtoPair :: DefaultUni (Esc (,)) | |
| DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a)) | |
| DefaultUniData :: DefaultUni (Esc Data) | |
| DefaultUniBLS12_381_G1_Element :: DefaultUni (Esc Element) | |
| DefaultUniBLS12_381_G2_Element :: DefaultUni (Esc Element) | |
| DefaultUniBLS12_381_MlResult :: DefaultUni (Esc MlResult) |
Instances
pattern DefaultUniList :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}. () => forall. (a ~ Esc (f a1), Esc f ~ Esc List) => DefaultUni (Esc a1) -> DefaultUni a Source #
pattern DefaultUniPair :: forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4} {f2 :: k3 -> k4} {a2 :: k3}. () => forall. (a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) => DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a Source #
data DefaultFun Source #
Default built-in functions.
When updating these, make sure to add them to the protocol version listing! See Note [New builtins/language versions and protocol versions]
Constructors
Instances
AST
data Term tyname name uni fun ann Source #
Constructors
| Var ann name | a named variable |
| LamAbs ann name (Type tyname uni ann) (Term tyname name uni fun ann) | lambda abstraction |
| Apply ann (Term tyname name uni fun ann) (Term tyname name uni fun ann) | application |
| TyAbs ann tyname (Kind ann) (Term tyname name uni fun ann) | type abstraction |
| TyInst ann (Term tyname name uni fun ann) (Type tyname uni ann) | instantiation |
| IWrap ann (Type tyname uni ann) (Type tyname uni ann) (Term tyname name uni fun ann) | wrapping |
| Unwrap ann (Term tyname name uni fun ann) | unwrapping See Note [Constr tag type] |
| Constr ann (Type tyname uni ann) Word64 [Term tyname name uni fun ann] | constructor |
| Case ann (Type tyname uni ann) (Term tyname name uni fun ann) [Term tyname name uni fun ann] | case |
| Constant ann (Some (ValueOf uni)) | constants |
| Builtin ann fun | builtin functions |
| Error ann (Type tyname uni ann) | fail with error |
Instances
termSubterms :: Traversal' (Term tyname name uni fun ann) (Term tyname name uni fun ann) Source #
termSubtypes :: Traversal' (Term tyname name uni fun ann) (Type tyname uni ann) Source #
termMapNames :: forall tyname tyname' name name' uni fun ann. (tyname -> tyname') -> (name -> name') -> Term tyname name uni fun ann -> Term tyname' name' uni fun ann Source #
programMapNames :: forall tyname tyname' name name' uni fun ann. (tyname -> tyname') -> (name -> name') -> Program tyname name uni fun ann -> Program 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 | |
data Type tyname uni ann Source #
A Kind assigned to expressions.
Constructors
| TyVar ann tyname | Type variable |
| TyFun ann (Type tyname uni ann) (Type tyname uni ann) | Function type |
| TyIFix ann (Type tyname uni ann) (Type tyname uni ann) | Fix-point type, for constructing self-recursive types |
| TyForall ann tyname (Kind ann) (Type tyname uni ann) | Polymorphic type |
| TyBuiltin ann (SomeTypeIn uni) | Builtin type |
| TyLam ann tyname (Kind ann) (Type tyname uni ann) | Type lambda |
| TyApp ann (Type tyname uni ann) (Type tyname uni ann) | Type application |
| TySOP ann [[Type tyname uni ann]] | Sum-of-products type |
Instances
typeSubtypes :: Traversal' (Type tyname uni ann) (Type tyname uni ann) Source #
typeMapNames :: forall tyname tyname' uni ann. (tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann Source #
Instances
toPatFuncKind :: Kind () -> Kind () Source #
argsFunKind :: Kind ann -> [Kind ann] Source #
Extract all a_i from a_0 -> a_1 -> ... -> r.
data ParserError Source #
An error encountered during parsing.
Constructors
| BuiltinTypeNotAStar !Text !SourcePos | |
| UnknownBuiltinFunction !Text !SourcePos ![Text] | |
| InvalidBuiltinConstant !Text !Text !SourcePos |
Instances
The version of Plutus Core used by this program.
The intention is to convey different levels of backwards compatibility for existing scripts: - Major version changes are backwards-incompatible - Minor version changes are backwards-compatible - Patch version changes should be entirely invisible (and we will likely not use this level)
The version used should be changed only when the language itself changes. For example, adding a new kind of term to the language would require a minor version bump; removing a kind of term would require a major version bump.
Similarly, changing the semantics of the language will require a version bump, typically a major one. This is the main reason why the version is actually tracked in the AST: we can have two language versions with identical ASTs but different semantics, so we need to track the version explicitly.
Compatibility is about compatibility for specific scripts, not about e.g. tools which consume scripts. Adding a new kind of term does not change how existing scripts behave, but does change what tools would need to do to process scripts.
Constructors
| Version | |
Fields | |
Instances
| Generic Version Source # | |
| Show Version Source # | |
| NFData Version Source # | |
Defined in PlutusCore.Version | |
| Flat Version | |
| Eq Version Source # | |
| Ord Version Source # | |
Defined in PlutusCore.Version | |
| Hashable Version Source # | |
Defined in PlutusCore.Version | |
| Pretty Version Source # | |
Defined in PlutusCore.Version | |
| type Rep Version Source # | |
Defined in PlutusCore.Version type Rep Version = D1 ('MetaData "Version" "PlutusCore.Version" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "Version" 'PrefixI 'True) (S1 ('MetaSel ('Just "_versionMajor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural) :*: (S1 ('MetaSel ('Just "_versionMinor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural) :*: S1 ('MetaSel ('Just "_versionPatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural)))) | |
data Program tyname name uni fun ann Source #
Constructors
| Program | |
Instances
| DefaultPrettyPlcStrategy (Program tyname name uni fun ann) => PrettyBy PrettyConfigPlc (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Plc Methods prettyBy :: PrettyConfigPlc -> Program tyname name uni fun ann -> Doc ann0 # prettyListBy :: PrettyConfigPlc -> [Program tyname name uni fun ann] -> Doc ann0 # | |
| (PrettyClassicBy configName (Term tyname name uni fun ann), Pretty ann) => PrettyBy (PrettyConfigClassic configName) (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Classic Methods prettyBy :: PrettyConfigClassic configName -> Program tyname name uni fun ann -> Doc ann0 # prettyListBy :: PrettyConfigClassic configName -> [Program tyname name uni fun ann] -> Doc ann0 # | |
| PrettyReadableBy configName (Term tyname name uni fun a) => PrettyBy (PrettyConfigReadable configName) (Program tyname name uni fun a) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Readable Methods prettyBy :: PrettyConfigReadable configName -> Program tyname name uni fun a -> Doc ann # prettyListBy :: PrettyConfigReadable configName -> [Program tyname name uni fun a] -> Doc ann # | |
| Functor (Program tyname name uni fun) Source # | |
| (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Program tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping Methods collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo Source # | |
| (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping | |
| Generic (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type | |
| (Show tyname, Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni) => Show (Program tyname name uni fun ann) Source # | |
| (NFData tyname, NFData name, Everywhere uni NFData, NFData fun, NFData ann, Closed uni) => NFData (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type | |
| (Flat ann, Flat (Term tyname name uni fun ann)) => Flat (Program tyname name uni fun ann) | |
| (GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann, Eq (Term tyname name uni fun ann)) => Eq (Program tyname name uni fun ann) Source # | |
| HasUniques (Program tyname name uni fun ann) => Rename (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Rename | |
| (PrettyClassic tyname, PrettyClassic name, PrettyUni uni, Pretty fun, Pretty ann) => Pretty (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Default | |
| type Rep (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type type Rep (Program tyname name uni fun ann) = D1 ('MetaData "Program" "PlutusCore.Core.Type" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "Program" 'PrefixI 'True) (S1 ('MetaSel ('Just "_progAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :*: (S1 ('MetaSel ('Just "_progVer") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Version) :*: S1 ('MetaSel ('Just "_progTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term tyname name uni fun ann))))) | |
| type HasUniques (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type | |
A Name represents variables/names in Plutus Core.
Constructors
| Name | |
Fields
| |
Instances
We use a newtype to enforce separation between names used for types and
those used for terms.
Instances
| Generic TyName Source # | |
| Show TyName Source # | |
| NFData TyName Source # | |
Defined in PlutusCore.Name.Unique | |
| Flat TyName | |
| Eq TyName Source # | |
| Ord TyName Source # | |
| Hashable TyName Source # | |
Defined in PlutusCore.Name.Unique | |
| Wrapped TyName Source # | |
Defined in PlutusCore.Name.Unique Associated Types type Unwrapped TyName | |
| ToScopedName TyName Source # | |
Defined in PlutusCore.Check.Scoping Methods toScopedName :: TyName -> ScopedName Source # | |
| HasText TyName Source # | |
| Pretty TyName Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Default | |
| HasUnique TyName TypeUnique Source # | |
Defined in PlutusCore.Name.Unique | |
| HasPrettyConfigName config => PrettyBy config TyName Source # | |
Defined in PlutusCore.Name.Unique | |
| Lift TyName Source # | |
| tyname ~ TyName => Reference TyName (Type tyname uni) Source # | |
Defined in PlutusCore.Core.Instance.Scoping Methods referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn Source # | |
| tyname ~ TyName => Reference TyName (Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping Methods referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source # | |
| Flat (Binder TyName) | |
| (GEq uni, Eq ann) => Eq (Type TyName uni ann) Source # | |
| TermLike (Term name uni fun) TyName name uni fun Source # | |
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 # | |
| AsTypeError (Error uni fun ann) (Term TyName Name uni fun ()) uni fun ann Source # | |
Defined in PlutusCore.Error Methods _TypeError :: Prism' (Error uni fun ann) (TypeError (Term TyName Name uni fun ()) uni fun ann) Source # _KindMismatch :: Prism' (Error uni fun ann) (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ()) Source # _TypeMismatch :: Prism' (Error uni fun ann) (ann, Term TyName Name uni fun (), ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ())) Source # _TyNameMismatch :: Prism' (Error uni fun ann) (ann, TyName, TyName) Source # _NameMismatch :: Prism' (Error uni fun ann) (ann, Name, Name) Source # _FreeTypeVariableE :: Prism' (Error uni fun ann) (ann, TyName) Source # _FreeVariableE :: Prism' (Error uni fun ann) (ann, Name) Source # _UnknownBuiltinFunctionE :: Prism' (Error uni fun ann) (ann, fun) Source # | |
| (GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term TyName Name uni fun ann) Source # | |
| HasConstant (Term TyName Name uni fun ()) Source # | |
| type Rep TyName Source # | |
Defined in PlutusCore.Name.Unique | |
| type Unwrapped TyName Source # | |
Defined in PlutusCore.Name.Unique | |
A unique identifier
Instances
| Enum Unique Source # | |
Defined in PlutusCore.Name.Unique Methods succ :: Unique -> Unique Source # pred :: Unique -> Unique Source # toEnum :: Int -> Unique Source # fromEnum :: Unique -> Int Source # enumFrom :: Unique -> [Unique] Source # enumFromThen :: Unique -> Unique -> [Unique] Source # enumFromTo :: Unique -> Unique -> [Unique] Source # enumFromThenTo :: Unique -> Unique -> Unique -> [Unique] Source # | |
| Show Unique Source # | |
| NFData Unique Source # | |
Defined in PlutusCore.Name.Unique | |
| Flat Unique | |
| Eq Unique Source # | |
| Ord Unique Source # | |
| Hashable Unique Source # | |
Defined in PlutusCore.Name.Unique | |
| Pretty Unique Source # | |
Defined in PlutusCore.Name.Unique | |
| HasUnique Unique Unique Source # | |
| Lift Unique Source # | |
newtype UniqueMap unique a Source #
A mapping from Uniques to arbitrary values of type a.
Since Unique is equivalent to Int (see PlutusCore.Name.Unique),
we can use an IntMap representation for this type.
Constructors
| UniqueMap | |
Fields
| |
Instances
| Foldable (UniqueMap unique) Source # | |
Defined in PlutusCore.Name.UniqueMap Methods fold :: Monoid m => UniqueMap unique m -> m Source # foldMap :: Monoid m => (a -> m) -> UniqueMap unique a -> m Source # foldMap' :: Monoid m => (a -> m) -> UniqueMap unique a -> m Source # foldr :: (a -> b -> b) -> b -> UniqueMap unique a -> b Source # foldr' :: (a -> b -> b) -> b -> UniqueMap unique a -> b Source # foldl :: (b -> a -> b) -> b -> UniqueMap unique a -> b Source # foldl' :: (b -> a -> b) -> b -> UniqueMap unique a -> b Source # foldr1 :: (a -> a -> a) -> UniqueMap unique a -> a Source # foldl1 :: (a -> a -> a) -> UniqueMap unique a -> a Source # toList :: UniqueMap unique a -> [a] Source # null :: UniqueMap unique a -> Bool Source # length :: UniqueMap unique a -> Int Source # elem :: Eq a => a -> UniqueMap unique a -> Bool Source # maximum :: Ord a => UniqueMap unique a -> a Source # minimum :: Ord a => UniqueMap unique a -> a Source # | |
| Functor (UniqueMap unique) Source # | |
| Monoid (UniqueMap unique a) Source # | |
| Semigroup (UniqueMap unique a) Source # | |
| Show a => Show (UniqueMap unique a) Source # | |
| Eq a => Eq (UniqueMap unique a) Source # | |
newtype UniqueSet unique Source #
A set containing Uniques. Since Unique is equivalent to Int
(see PlutusCore.Name.Unique), we can use an IntSet representation for this type.
Constructors
| UniqueSet | |
Fields | |
newtype Normalized a Source #
Constructors
| Normalized | |
Fields
| |
Instances
latestVersion :: Version Source #
The latest version of Plutus Core supported by this library.
tyVarDeclAnn :: forall tyname ann. Lens' (TyVarDecl tyname ann) ann Source #
tyVarDeclName :: forall tyname ann tyname. Lens (TyVarDecl tyname ann) (TyVarDecl tyname ann) tyname tyname Source #
varDeclAnn :: forall tyname name uni ann. Lens' (VarDecl tyname name uni ann) ann Source #
varDeclName :: forall tyname name uni ann name. Lens (VarDecl tyname name uni ann) (VarDecl tyname name uni ann) name name Source #
varDeclType :: forall tyname name uni ann tyname uni. Lens (VarDecl tyname name uni ann) (VarDecl tyname name uni ann) (Type tyname uni ann) (Type tyname uni ann) Source #
tyDeclType :: forall tyname uni ann tyname uni. Lens (TyDecl tyname uni ann) (TyDecl tyname uni ann) (Type tyname uni ann) (Type tyname uni ann) Source #
progTerm :: forall tyname name uni fun ann tyname name uni fun. Lens (Program tyname name uni fun ann) (Program tyname name uni fun ann) (Term tyname name uni fun ann) (Term tyname name uni fun ann) Source #
mapFun :: (fun -> fun') -> Term tyname name uni fun ann -> Term tyname name uni fun' ann Source #
Map a function over the set of built-in functions.
DeBruijn representation
A term name as a de Bruijn index, without the name string.
Instances
newtype TyDeBruijn Source #
A type name as a de Bruijn index, without the name string.
Constructors
| TyDeBruijn DeBruijn |
Instances
data NamedDeBruijn Source #
A term name as a de Bruijn index.
Constructors
| NamedDeBruijn | |
Fields
| |
Instances
newtype NamedTyDeBruijn Source #
A type name as a de Bruijn index.
Constructors
| NamedTyDeBruijn NamedDeBruijn |
Instances
deBruijnTerm :: (AsFreeVariableError e, MonadError e m) => Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source #
Convert a Term with TyNames and Names into a Term with NamedTyDeBruijns and
NamedDeBruijns. Will throw an error if a free variable is encountered.
unDeBruijnTerm :: (MonadQuote m, AsFreeVariableError e, MonadError e m) => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) Source #
Convert a Term with NamedTyDeBruijns and NamedDeBruijns into a Term with TyNames and
Names. Will throw an error if a free variable is encountered.
Processing
type family HasUniques a :: Constraint Source #
All kinds of uniques an entity contains.
Instances
| type HasUniques (Kind ann) Source # | |
Defined in PlutusCore.Core.Type | |
| type HasUniques (Type tyname uni ann) Source # | |
Defined in PlutusCore.Core.Type | |
| type HasUniques (Program name uni fun ann) Source # | |
Defined in UntypedPlutusCore.Core.Type | |
| type HasUniques (Term name uni fun ann) Source # | |
Defined in UntypedPlutusCore.Core.Type | |
| type HasUniques (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type | |
| type HasUniques (Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type type HasUniques (Term tyname name uni fun ann) = (HasUnique tyname TypeUnique, HasUnique name TermUnique) | |
The class of things that can be renamed. I.e. things that are capable of satisfying the global uniqueness condition.
Methods
rename :: MonadQuote m => a -> m a Source #
Rename Uniques so that they're globally unique.
In case there are any free variables, they must be left untouched and bound variables
must not get renamed to free ones.
Must always assign new names to bound variables,
so that rename can be used for alpha-renaming as well.
Instances
| Rename a => Rename (Normalized a) Source # | |
Defined in PlutusCore.Rename Methods rename :: MonadQuote m => Normalized a -> m (Normalized a) Source # | |
| HasUniques (Type tyname uni ann) => Rename (Type tyname uni ann) Source # | |
Defined in PlutusCore.Rename | |
| HasUniques (Program name uni fun ann) => Rename (Program name uni fun ann) Source # | |
Defined in UntypedPlutusCore.Rename | |
| HasUniques (Term name uni fun ann) => Rename (Term name uni fun ann) Source # | |
Defined in UntypedPlutusCore.Rename | |
| HasUniques (Program tyname name uni fun ann) => Rename (Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Rename | |
| HasUniques (Term tyname name uni fun ann) => Rename (Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Rename | |
Type checking
module PlutusCore.TypeCheck
normalizeTypesIn :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, MonadNormalizeType uni m) => Term tyname name uni fun ann -> m (Term tyname name uni fun ann) Source #
normalizeTypesInProgram :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, MonadNormalizeType uni m) => Program tyname name uni fun ann -> m (Program tyname name uni fun ann) Source #
class AsTypeError r term uni fun ann | r -> term uni fun ann where Source #
Minimal complete definition
Methods
_TypeError :: Prism' r (TypeError term uni fun ann) Source #
_KindMismatch :: Prism' r (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ()) Source #
_TypeMismatch :: Prism' r (ann, term, ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ())) Source #
_TyNameMismatch :: Prism' r (ann, TyName, TyName) Source #
_NameMismatch :: Prism' r (ann, Name, Name) Source #
_FreeTypeVariableE :: Prism' r (ann, TyName) Source #
_FreeVariableE :: Prism' r (ann, Name) Source #
_UnknownBuiltinFunctionE :: Prism' r (ann, fun) Source #
Instances
| AsTypeError (Error uni fun ann) (Term TyName Name uni fun ()) uni fun ann Source # | |
Defined in PlutusCore.Error Methods _TypeError :: Prism' (Error uni fun ann) (TypeError (Term TyName Name uni fun ()) uni fun ann) Source # _KindMismatch :: Prism' (Error uni fun ann) (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ()) Source # _TypeMismatch :: Prism' (Error uni fun ann) (ann, Term TyName Name uni fun (), ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ())) Source # _TyNameMismatch :: Prism' (Error uni fun ann) (ann, TyName, TyName) Source # _NameMismatch :: Prism' (Error uni fun ann) (ann, Name, Name) Source # _FreeTypeVariableE :: Prism' (Error uni fun ann) (ann, TyName) Source # _FreeVariableE :: Prism' (Error uni fun ann) (ann, Name) Source # _UnknownBuiltinFunctionE :: Prism' (Error uni fun ann) (ann, fun) Source # | |
| AsTypeError (TypeError term uni fun ann) term uni fun ann Source # | |
Defined in PlutusCore.Error Methods _TypeError :: Prism' (TypeError term uni fun ann) (TypeError term uni fun ann) Source # _KindMismatch :: Prism' (TypeError term uni fun ann) (ann, Type TyName uni (), ExpectedShapeOr (Kind ()), Kind ()) Source # _TypeMismatch :: Prism' (TypeError term uni fun ann) (ann, term, ExpectedShapeOr (Type TyName uni ()), Normalized (Type TyName uni ())) Source # _TyNameMismatch :: Prism' (TypeError term uni fun ann) (ann, TyName, TyName) Source # _NameMismatch :: Prism' (TypeError term uni fun ann) (ann, Name, Name) Source # _FreeTypeVariableE :: Prism' (TypeError term uni fun ann) (ann, TyName) Source # _FreeVariableE :: Prism' (TypeError term uni fun ann) (ann, Name) Source # _UnknownBuiltinFunctionE :: Prism' (TypeError term uni fun ann) (ann, fun) Source # | |
data TypeError term uni fun ann Source #
Instances
Errors
data Error uni fun ann Source #
Constructors
| ParseErrorE !ParserErrorBundle | |
| UniqueCoherencyErrorE !(UniqueError ann) | |
| TypeErrorE !(TypeError (Term TyName Name uni fun ()) uni fun ann) | |
| NormCheckErrorE !(NormCheckError TyName Name uni fun ann) | |
| FreeVariableErrorE !FreeVariableError |
Instances
class AsError r uni fun ann | r -> uni fun ann where Source #
Minimal complete definition
Methods
_Error :: Prism' r (Error uni fun ann) Source #
_ParseErrorE :: Prism' r ParserErrorBundle Source #
_UniqueCoherencyErrorE :: Prism' r (UniqueError ann) Source #
_TypeErrorE :: Prism' r (TypeError (Term TyName Name uni fun ()) uni fun ann) Source #
_NormCheckErrorE :: Prism' r (NormCheckError TyName Name uni fun ann) Source #
_FreeVariableErrorE :: Prism' r FreeVariableError Source #
Instances
| AsError (Error uni fun ann) uni fun ann Source # | |
Defined in PlutusCore.Error Methods _Error :: Prism' (Error uni fun ann) (Error uni fun ann) Source # _ParseErrorE :: Prism' (Error uni fun ann) ParserErrorBundle Source # _UniqueCoherencyErrorE :: Prism' (Error uni fun ann) (UniqueError ann) Source # _TypeErrorE :: Prism' (Error uni fun ann) (TypeError (Term TyName Name uni fun ()) uni fun ann) Source # _NormCheckErrorE :: Prism' (Error uni fun ann) (NormCheckError TyName Name uni fun ann) Source # _FreeVariableErrorE :: Prism' (Error uni fun ann) FreeVariableError Source # | |
data NormCheckError tyname name uni fun ann Source #
Constructors
| BadType !ann !(Type tyname uni ann) !Text | |
| BadTerm !ann !(Term tyname name uni fun ann) !Text |
Instances
| (Pretty ann, PrettyBy config (Type tyname uni ann), PrettyBy config (Term tyname name uni fun ann)) => PrettyBy config (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error Methods prettyBy :: config -> NormCheckError tyname name uni fun ann -> Doc ann0 # prettyListBy :: config -> [NormCheckError tyname name uni fun ann] -> Doc ann0 # | |
| Functor (NormCheckError tyname name uni fun) Source # | |
Defined in PlutusCore.Error Methods fmap :: (a -> b) -> NormCheckError tyname name uni fun a -> NormCheckError tyname name uni fun b Source # (<$) :: a -> NormCheckError tyname name uni fun b -> NormCheckError tyname name uni fun a Source # | |
| Generic (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error Methods from :: NormCheckError tyname name uni fun ann -> Rep (NormCheckError tyname name uni fun ann) x Source # to :: Rep (NormCheckError tyname name uni fun ann) x -> NormCheckError tyname name uni fun ann Source # | |
| (Show tyname, Show name, Closed uni, Everywhere uni Show, Show fun, Show ann, GShow uni) => Show (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error | |
| (NFData tyname, NFData name, Closed uni, Everywhere uni NFData, NFData fun, NFData ann) => NFData (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error Methods rnf :: NormCheckError tyname name uni fun ann -> () Source # | |
| (Eq (Term tyname name uni fun ann), Eq (Type tyname uni ann), GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error Methods (==) :: NormCheckError tyname name uni fun ann -> NormCheckError tyname name uni fun ann -> Bool Source # (/=) :: NormCheckError tyname name uni fun ann -> NormCheckError tyname name uni fun ann -> Bool Source # | |
| AsNormCheckError (NormCheckError tyname name uni fun ann) tyname name uni fun ann Source # | |
Defined in PlutusCore.Error Methods _NormCheckError :: Prism' (NormCheckError tyname name uni fun ann) (NormCheckError tyname name uni fun ann) Source # _BadType :: Prism' (NormCheckError tyname name uni fun ann) (ann, Type tyname uni ann, Text) Source # _BadTerm :: Prism' (NormCheckError tyname name uni fun ann) (ann, Term tyname name uni fun ann, Text) Source # | |
| type Rep (NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error type Rep (NormCheckError tyname name uni fun ann) = D1 ('MetaData "NormCheckError" "PlutusCore.Error" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "BadType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ann) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Type tyname uni ann)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text))) :+: C1 ('MetaCons "BadTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ann) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Term tyname name uni fun ann)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)))) | |
class AsNormCheckError r tyname name uni fun ann | r -> tyname name uni fun ann where Source #
Minimal complete definition
Methods
_NormCheckError :: Prism' r (NormCheckError tyname name uni fun ann) Source #
_BadType :: Prism' r (ann, Type tyname uni ann, Text) Source #
_BadTerm :: Prism' r (ann, Term tyname name uni fun ann, Text) Source #
Instances
| (tyname ~ TyName, name ~ Name) => AsNormCheckError (Error uni fun ann) tyname name uni fun ann Source # | |
| AsNormCheckError (NormCheckError tyname name uni fun ann) tyname name uni fun ann Source # | |
Defined in PlutusCore.Error Methods _NormCheckError :: Prism' (NormCheckError tyname name uni fun ann) (NormCheckError tyname name uni fun ann) Source # _BadType :: Prism' (NormCheckError tyname name uni fun ann) (ann, Type tyname uni ann, Text) Source # _BadTerm :: Prism' (NormCheckError tyname name uni fun ann) (ann, Term tyname name uni fun ann, Text) Source # | |
data UniqueError ann Source #
Constructors
| MultiplyDefined !Unique !ann !ann | |
| IncoherentUsage !Unique !ann !ann | |
| FreeVariable !Unique !ann |
Instances
class AsUniqueError r ann | r -> ann where Source #
Minimal complete definition
Methods
_UniqueError :: Prism' r (UniqueError ann) Source #
_MultiplyDefined :: Prism' r (Unique, ann, ann) Source #
_IncoherentUsage :: Prism' r (Unique, ann, ann) Source #
_FreeVariable :: Prism' r (Unique, ann) Source #
Instances
| AsUniqueError (UniqueError ann) ann Source # | |
Defined in PlutusCore.Error Methods _UniqueError :: Prism' (UniqueError ann) (UniqueError ann) Source # _MultiplyDefined :: Prism' (UniqueError ann) (Unique, ann, ann) Source # _IncoherentUsage :: Prism' (UniqueError ann) (Unique, ann, ann) Source # _FreeVariable :: Prism' (UniqueError ann) (Unique, ann) Source # | |
| AsUniqueError (Error uni fun ann) ann Source # | |
Defined in PlutusCore.Error Methods _UniqueError :: Prism' (Error uni fun ann) (UniqueError ann) Source # _MultiplyDefined :: Prism' (Error uni fun ann) (Unique, ann, ann) Source # _IncoherentUsage :: Prism' (Error uni fun ann) (Unique, ann, ann) Source # _FreeVariable :: Prism' (Error uni fun ann) (Unique, ann) Source # | |
data FreeVariableError Source #
We cannot do a correct translation to or from de Bruijn indices if the program is not well-scoped. So we throw an error in such a case.
Constructors
| FreeUnique !Unique | |
| FreeIndex !Index |
Instances
class AsFreeVariableError r where Source #
Minimal complete definition
Methods
_FreeVariableError :: Prism' r FreeVariableError Source #
_FreeUnique :: Prism' r Unique Source #
_FreeIndex :: Prism' r Index Source #
Instances
| AsFreeVariableError FreeVariableError Source # | |
Defined in PlutusCore.DeBruijn.Internal Methods _FreeVariableError :: Prism' FreeVariableError FreeVariableError Source # _FreeUnique :: Prism' FreeVariableError Unique Source # _FreeIndex :: Prism' FreeVariableError Index Source # | |
| AsFreeVariableError (Error uni fun ann) Source # | |
Defined in PlutusCore.Error Methods _FreeVariableError :: Prism' (Error uni fun ann) FreeVariableError Source # _FreeUnique :: Prism' (Error uni fun ann) Unique Source # _FreeIndex :: Prism' (Error uni fun ann) Index Source # | |
Quotation and term construction
The "quotation" monad transformer. Within this monad you can do safe construction of PLC terms using quasiquotation, fresh-name generation, and parsing.
Instances
| MonadTrans QuoteT Source # | |
| MFunctor QuoteT Source # | |
Defined in PlutusCore.Quote | |
| MonadError e m => MonadError e (QuoteT m) Source # | |
Defined in PlutusCore.Quote Methods throwError :: e -> QuoteT m a Source # catchError :: QuoteT m a -> (e -> QuoteT m a) -> QuoteT m a Source # | |
| MonadReader r m => MonadReader r (QuoteT m) Source # | |
| MonadState s m => MonadState s (QuoteT m) Source # | |
| MonadWriter w m => MonadWriter w (QuoteT m) Source # | |
| MonadFix m => MonadFix (QuoteT m) Source # | |
| MonadIO m => MonadIO (QuoteT m) Source # | |
| Monad m => Applicative (QuoteT m) Source # | |
Defined in PlutusCore.Quote | |
| Functor m => Functor (QuoteT m) Source # | |
| Monad m => Monad (QuoteT m) Source # | |
| Monad m => MonadQuote (QuoteT m) Source # | |
runQuoteT :: Monad m => QuoteT m a -> m a Source #
Run a quote from an empty identifier state. Note that the resulting term cannot necessarily
be safely combined with other terms - that should happen inside QuoteT.
class Monad m => MonadQuote m Source #
A monad that allows lifting of quoted expressions.
Instances
| MonadQuote m => MonadQuote (GenT m) Source # | |
Defined in PlutusCore.Quote | |
| MonadQuote m => MonadQuote (PropertyT m) Source # | |
Defined in PlutusCore.Quote | |
| Monad m => MonadQuote (QuoteT m) Source # | |
| MonadQuote m => MonadQuote (MaybeT m) Source # | |
| MonadQuote m => MonadQuote (RenameT ren m) Source # | |
| MonadQuote m => MonadQuote (ExceptT e m) Source # | |
| MonadQuote m => MonadQuote (ReaderT r m) Source # | |
| MonadQuote m => MonadQuote (StateT s m) Source # | |
| (Stream s, MonadQuote m) => MonadQuote (ParsecT e s m) Source # | |
Defined in PlutusCore.Parser.ParserCommon | |
| MonadQuote m => MonadQuote (NormalizeTypeT m tyname uni ann) Source # | |
Defined in PlutusCore.Normalize.Internal Methods liftQuote :: Quote a -> NormalizeTypeT m tyname uni ann a Source # | |
liftQuote :: MonadQuote m => Quote a -> m a Source #
Name generation
freshUnique :: MonadQuote m => m Unique Source #
Get a fresh Unique.
freshTyName :: MonadQuote m => Text -> m TyName Source #
Evaluation
data EvaluationResult a Source #
The parameterized type of results various evaluation engines return.
On the PLC side this becomes (via makeKnown) either a call to Error or
a value of the PLC counterpart of type a.
Constructors
| EvaluationSuccess !a | |
| EvaluationFailure |
Instances
Combining programs
applyProgram :: (MonadError ApplyProgramError m, Semigroup a) => Program tyname name uni fun a -> Program tyname name uni fun a -> m (Program tyname name uni fun a) Source #
Applies one program to another. Fails if the versions do not match and tries to merge annotations.
Benchmarking
kindSize :: Kind a -> Size Source #
Count the number of AST nodes in a kind.
>>>kindSize $ Type ()Size {unSize = 1}>>>kindSize $ KindArrow () (KindArrow () (Type ()) (Type ())) (Type ())Size {unSize = 5}
programSize :: Program tyname name uni fun ann -> Size Source #
Count the number of AST nodes in a program.
serialisedSize :: Flat a => a -> Integer Source #
Compute the size of the serializabled form of a value.