Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- parseProgram :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Program TyName Name DefaultUni DefaultFun SourcePos )
- parseTerm :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Term TyName Name DefaultUni DefaultFun SourcePos )
- parseType :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Type TyName DefaultUni SourcePos )
- parseScoped :: MonadQuote f => ByteString -> f ( Program TyName Name DefaultUni DefaultFun SourcePos )
- topSourcePos :: SourcePos
- 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 `Includes` a => a -> Some ( ValueOf uni)
- someValueType :: Some ( ValueOf uni) -> SomeTypeIn uni
- data Esc a
- class Contains uni a where
- type Includes uni = Permits ( Contains uni)
-
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
- deriveGEq :: DeriveGEQ t => t -> Q [ Dec ]
-
class
HasUniApply
(uni ::
Type
->
Type
)
where
- matchUniApply :: uni tb -> r -> ( forall k l (f :: k -> l) a. tb ~ Esc (f a) => uni ( Esc f) -> uni ( Esc a) -> r) -> r
- 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
-
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 [])
- DefaultUniProtoPair :: DefaultUni ( Esc (,) )
- DefaultUniApply :: !( DefaultUni ( Esc f)) -> !( DefaultUni ( Esc a)) -> DefaultUni ( Esc (f a))
- DefaultUniData :: DefaultUni ( Esc Data )
- pattern DefaultUniList :: forall a k1 k2 (f :: k1 -> k2) (a1 :: k1). () => forall . (a ~ Esc (f a1), Esc f ~ Esc []) => 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
-
data
Term
tyname name uni fun ann
- = Var ann name
- | TyAbs ann tyname ( Kind ann) ( Term tyname name uni fun ann)
- | 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)
- | Constant ann ( Some ( ValueOf uni))
- | Builtin ann fun
- | TyInst ann ( Term tyname name uni fun ann) ( Type tyname uni ann)
- | Unwrap ann ( Term tyname name uni fun ann)
- | IWrap ann ( Type tyname uni ann) ( Type tyname uni ann) ( Term tyname name uni fun ann)
- | 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)
- 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)
- typeSubtypes :: Traversal' ( Type tyname uni ann) ( Type tyname uni ann)
- data Kind ann
- data ParseError
- data Version ann = Version ann Natural Natural Natural
- data Program tyname name uni fun ann = Program { }
-
data
Name
=
Name
{
- nameString :: Text
- nameUnique :: Unique
- newtype TyName = TyName { }
- newtype Unique = Unique { }
-
newtype
UniqueMap
unique a =
UniqueMap
{
- unUniqueMap :: IntMap a
-
newtype
Normalized
a =
Normalized
{
- unNormalized :: a
- defaultVersion :: ann -> Version ann
- 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 k (fun :: k) ann k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) ann) ann ann
- varDeclName :: forall tyname name uni k (fun :: k) ann name k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) ann) name name
- varDeclType :: forall tyname name uni k (fun :: k) ann tyname uni k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) 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 ann)
- 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 { }
-
data
NamedDeBruijn
=
NamedDeBruijn
{
- ndbnString :: Text
- ndbnIndex :: Index
- 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)
- data SourcePos
- format :: ( Monad m, PrettyBy config ( Program TyName Name DefaultUni DefaultFun SourcePos )) => config -> ByteString -> m Text
- type family HasUniques a :: Constraint
-
class
Rename
a
where
- rename :: MonadQuote m => a -> m a
- class ToKind (uni :: Type -> Type )
- type Typecheckable uni fun = ( ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun)
-
newtype
BuiltinTypes
uni fun =
BuiltinTypes
{
- unBuiltinTypes :: Maybe ( Array fun ( Dupable ( Normalized ( Type TyName uni ()))))
-
newtype
TypeCheckConfig
uni fun =
TypeCheckConfig
{
- _tccBuiltinTypes :: BuiltinTypes uni fun
- tccBuiltinTypes :: HasTypeCheckConfig c uni fun => Lens' c ( BuiltinTypes uni fun)
- builtinMeaningsToTypes :: ( MonadError err m, AsTypeError err term uni fun ann, Typecheckable uni fun) => ann -> m ( BuiltinTypes uni fun)
- getDefTypeCheckConfig :: ( MonadError err m, AsTypeError err term uni fun ann, Typecheckable uni fun) => ann -> m ( TypeCheckConfig uni fun)
- inferKind :: ( MonadQuote m, MonadError err m, AsTypeError err term uni fun ann, ToKind uni) => TypeCheckConfig uni fun -> Type TyName uni ann -> m ( Kind ())
- checkKind :: ( MonadQuote m, MonadError err m, AsTypeError err term uni fun ann, ToKind uni) => TypeCheckConfig uni fun -> ann -> Type TyName uni ann -> Kind () -> m ()
- inferType :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> Term TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ()))
- checkType :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> ann -> Term TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m ()
- inferTypeOfProgram :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> Program TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ()))
- checkTypeOfProgram :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> ann -> Program TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m ()
- printType :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun SourcePos , MonadError e m) => ByteString -> m Text
- normalizeTypesIn :: ( HasUnique tyname TypeUnique , HasUnique name TermUnique , MonadQuote m, HasUniApply uni) => Term tyname name uni fun ann -> m ( Term tyname name uni fun ann)
- normalizeTypesInProgram :: ( HasUnique tyname TypeUnique , HasUnique name TermUnique , MonadQuote m, HasUniApply uni) => 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 (), Kind (), Kind ())
- _TypeMismatch :: Prism' r (ann, term, Type TyName uni (), Normalized ( Type TyName uni ()))
- _FreeTypeVariableE :: Prism' r (ann, TyName )
- _FreeVariableE :: Prism' r (ann, Name )
- _UnknownBuiltinFunctionE :: Prism' r (ann, fun)
- data TypeError term uni fun ann
- parseTypecheck :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun SourcePos , MonadError e m, MonadQuote m) => TypeCheckConfig DefaultUni DefaultFun -> ByteString -> m ( Normalized ( Type TyName DefaultUni ()))
- typecheckPipeline :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun a, MonadError e m, MonadQuote m) => TypeCheckConfig DefaultUni DefaultFun -> Program TyName Name DefaultUni DefaultFun a -> m ( Normalized ( Type TyName DefaultUni ()))
-
data
Error
uni fun ann
- = ParseErrorE ParseError
- | 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 ParseError
- _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
-
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
-
class
AsFreeVariableError
r
where
- _FreeVariableError :: Prism' r FreeVariableError
- _FreeUnique :: Prism' r Unique
- _FreeIndex :: Prism' r Index
-
data
TermF
(tyname ::
Type
) (name ::
Type
) (uni ::
Type
->
Type
) (fun ::
Type
) (ann ::
Type
) r
- = VarF ann name
- | TyAbsF ann tyname ( Kind ann) r
- | LamAbsF ann name ( Type tyname uni ann) r
- | ApplyF ann r r
- | ConstantF ann ( Some ( ValueOf uni))
- | BuiltinF ann fun
- | TyInstF ann r ( Type tyname uni ann)
- | UnwrapF ann r
- | IWrapF ann ( Type tyname uni ann) ( Type tyname uni ann) r
- | ErrorF ann ( Type tyname uni ann)
-
data
TypeF
(tyname ::
Type
) (uni ::
Type
->
Type
) (ann ::
Type
) r
- = TyVarF ann tyname
- | TyFunF ann r r
- | TyIFixF ann r r
- | TyForallF ann tyname ( Kind ann) r
- | TyBuiltinF ann ( SomeTypeIn uni)
- | TyLamF ann tyname ( Kind ann) r
- | TyAppF ann r r
- 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
- data UnliftingMode
- applyProgram :: Monoid a => Program tyname name uni fun a -> Program tyname name uni fun a -> 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
- defaultBuiltinCostModel :: BuiltinCostModel
- defaultBuiltinsRuntime :: HasConstantIn DefaultUni term => BuiltinsRuntime DefaultFun term
- defaultCekCostModel :: CostModel CekMachineCosts BuiltinCostModel
- defaultCekMachineCosts :: CekMachineCosts
- defaultCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
- defaultCostModelParams :: Maybe CostModelParams
- defaultUnliftingMode :: UnliftingMode
- unitCekParameters :: MachineParameters CekMachineCosts CekValue DefaultUni DefaultFun
- cekMachineCostsPrefix :: Text
- data CekMachineCosts = CekMachineCosts { }
Parser
parseProgram :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Program TyName Name DefaultUni DefaultFun SourcePos ) Source #
Parse a PLC program. The resulting program will have fresh names. The underlying monad must be capable of handling any parse errors.
parseTerm :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Term TyName Name DefaultUni DefaultFun SourcePos ) Source #
Parse a PLC term. The resulting program will have fresh names. The underlying monad must be capable of handling any parse errors.
parseType :: ByteString -> Either ( ParseErrorBundle Text ParseError ) ( Type TyName DefaultUni SourcePos ) Source #
Parse a PLC type. The resulting program will have fresh names. The underlying monad must be capable of handling any parse errors.
parseScoped :: MonadQuote f => ByteString -> f ( Program TyName Name DefaultUni DefaultFun SourcePos ) Source #
Parse and rewrite so that names are globally unique, not just unique within their scope. don't require there to be no free variables at this point, we might be parsing an open term
Builtins
data Some (tag :: k -> Type ) where Source #
Existential. This is type is useful to hide GADTs' parameters.
>>>
data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool
>>>
instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
>>>
classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
>>>
instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <- lex s, r <- classify con ]
You can either use
PatternSynonyms
(available with GHC >= 8.0)
>>>
let x = Some TagInt
>>>
x
Some TagInt
>>>
case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
"I"
or you can use functions
>>>
let y = mkSome TagBool
>>>
y
Some TagBool
>>>
withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
"B"
The implementation of
mapSome
is
safe
.
>>>
let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
>>>
mapSome f y
Some TagBool
but you can also use:
>>>
withSome y (mkSome . f)
Some TagBool
>>>
read "Some TagBool" :: Some Tag
Some TagBool
>>>
read "mkSome TagInt" :: Some Tag
Some TagInt
Instances
GEq tag => Eq ( Some tag) | |
GCompare tag => Ord ( Some tag) | |
Defined in Data.Some.Newtype |
|
GRead f => Read ( Some f) | |
GShow tag => Show ( Some tag) | |
Applicative m => Semigroup ( Some m) | |
Applicative m => Monoid ( Some m) | |
GNFData tag => NFData ( Some tag) | |
Defined in Data.Some.Newtype |
|
( Closed uni, Everywhere uni Flat ) => Flat ( Some ( ValueOf uni)) Source # | |
( Closed uni, Everywhere uni PrettyConst ) => Pretty ( Some ( ValueOf uni)) Source # | |
( Closed uni, Everywhere uni ExMemoryUsage ) => ExMemoryUsage ( Some ( ValueOf uni)) Source # | |
Defined in PlutusCore.Evaluation.Machine.ExMemory |
data SomeTypeIn uni Source #
A particular type from a universe.
forall k (a :: k). SomeTypeIn !(uni ( Esc a)) |
Instances
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 `Includes` 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 Int
UList (UList UInt)
can be encoded to
[0,0,1]
where
0
and
1
are the integer tags of the
UList
and
UInt
constructors, respectively.
type Everywhere uni (constr :: Type -> Constraint ) :: Constraint Source #
A constrant for "
constr a
holds for any
a
from
uni
".
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 type Everywhere DefaultUni constr Source # 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 #
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 Source #
Show
-like class for 1-type-parameter GADTs.
GShow t => ...
is equivalent to something
like
(forall a. Show (t a)) => ...
. The easiest way to create instances would probably be
to write (or derive) an
instance Show (T a)
, and then simply say:
instance GShow t where gshowsPrec = showsPrec
gshowsPrec :: forall (a :: k). Int -> t a -> ShowS Source #
Instances
GShow DefaultUni Source # | |
Defined in PlutusCore.Default.Universe gshowsPrec :: forall (a :: k). Int -> DefaultUni a -> ShowS Source # |
|
( GShow uni, Closed uni, Everywhere uni Show ) => GShow ( ValueOf uni :: Type -> Type ) Source # | |
Defined in Universe.Core |
|
GShow uni => GShow ( Kinded uni :: Type -> Type ) Source # | |
Defined in Universe.Core |
|
GShow ( TypeRep :: k -> Type ) | |
Defined in Data.GADT.Internal |
|
GShow ( GOrdering a :: k -> Type ) | |
Defined in Data.GADT.Internal |
|
GShow ( (:~:) a :: k -> Type ) | |
Defined in Data.GADT.Internal |
|
( GShow a, GShow b) => GShow ( Sum a b :: k -> Type ) |
|
Defined in Data.GADT.Internal |
|
( GShow a, GShow b) => GShow ( Product a b :: k -> Type ) |
|
Defined in Data.GADT.Internal |
class GEq (f :: k -> Type ) where Source #
A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.
geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) Source #
Produce a witness of type-equality, if one exists.
A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:
extract :: GEq tag => tag a -> DSum tag -> Maybe a extract t1 (t2 :=> x) = do Refl <- geq t1 t2 return x
Or in a list comprehension:
extractMany :: GEq tag => tag a -> [DSum tag] -> [a] extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]
(Making use of the
DSum
type from
Data.Dependent.Sum
in both examples)
Instances
GEq DefaultUni Source # | |
Defined in PlutusCore.Default.Universe geq :: forall (a :: k) (b :: k). DefaultUni a -> DefaultUni b -> Maybe (a :~: b) Source # |
|
( 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 ( Sum a b :: k -> Type ) | |
( GEq a, GEq b) => GEq ( Product a b :: k -> Type ) | |
class HasUniApply (uni :: Type -> Type ) where Source #
A class for "
uni
has general type application".
:: 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 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 |
Semigroupoid ( (:~:) :: k -> k -> Type ) | |
TestEquality ( (:~:) a :: k -> Type ) |
Since: base-4.7.0.0 |
Defined in Data.Type.Equality |
|
GShow ( (:~:) a :: k -> Type ) | |
Defined in Data.GADT.Internal |
|
GRead ( (:~:) a :: k -> Type ) | |
Defined in Data.GADT.Internal |
|
GEq ( (:~:) a :: k -> Type ) | |
GCompare ( (:~:) a :: k -> Type ) | |
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 => 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 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 # |
|
Eq (a :~: b) |
Since: base-4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) |
Since: base-4.7.0.0 |
Defined in Data.Data 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 # |
|
Ord (a :~: b) |
Since: base-4.7.0.0 |
Defined in Data.Type.Equality |
|
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 |
type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2 Source #
A constraint for "
uni1
is a subuniverse of
uni2
".
data DefaultUni a where Source #
The universe used by default.
DefaultUniInteger :: DefaultUni ( Esc Integer ) | |
DefaultUniByteString :: DefaultUni ( Esc ByteString ) | |
DefaultUniString :: DefaultUni ( Esc Text ) | |
DefaultUniUnit :: DefaultUni ( Esc ()) | |
DefaultUniBool :: DefaultUni ( Esc Bool ) | |
DefaultUniProtoList :: DefaultUni ( Esc []) | |
DefaultUniProtoPair :: DefaultUni ( Esc (,) ) | |
DefaultUniApply :: !( DefaultUni ( Esc f)) -> !( DefaultUni ( Esc a)) -> DefaultUni ( Esc (f a)) | |
DefaultUniData :: DefaultUni ( Esc Data ) |
Instances
pattern DefaultUniList :: forall a k1 k2 (f :: k1 -> k2) (a1 :: k1). () => forall . (a ~ Esc (f a1), Esc f ~ Esc []) => 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 and protocol versions]
Instances
AST
data Term tyname name uni fun ann Source #
Var ann name |
a named variable |
TyAbs ann tyname ( Kind ann) ( Term tyname name uni fun ann) | |
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) | |
Constant ann ( Some ( ValueOf uni)) |
a constant term |
Builtin ann fun | |
TyInst ann ( Term tyname name uni fun ann) ( Type tyname uni ann) | |
Unwrap ann ( Term tyname name uni fun ann) | |
IWrap ann ( Type tyname uni ann) ( Type tyname uni ann) ( Term tyname name uni fun ann) | |
Error ann ( Type tyname uni ann) |
Instances
tyname ~ TyName => Reference TyName ( Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source # |
|
name ~ Name => Reference Name ( Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> Name -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source # |
|
DefaultPrettyPlcStrategy ( Term tyname name uni fun ann) => PrettyBy PrettyConfigPlc ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Plc prettyBy :: PrettyConfigPlc -> Term tyname name uni fun ann -> Doc ann0 Source # prettyListBy :: PrettyConfigPlc -> [ Term tyname name uni fun ann] -> Doc ann0 Source # |
|
( PrettyReadableBy configName tyname, PrettyReadableBy configName name, GShow uni, Closed uni, Everywhere uni PrettyConst , Pretty fun) => PrettyBy ( PrettyConfigReadable configName) ( Term tyname name uni fun a) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Readable prettyBy :: PrettyConfigReadable configName -> Term tyname name uni fun a -> Doc ann Source # prettyListBy :: PrettyConfigReadable configName -> [ Term tyname name uni fun a] -> Doc ann Source # |
|
( PrettyClassicBy configName tyname, PrettyClassicBy configName name, GShow uni, Closed uni, Everywhere uni PrettyConst , Pretty fun, Pretty ann) => PrettyBy ( PrettyConfigClassic configName) ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Classic prettyBy :: PrettyConfigClassic configName -> Term tyname name uni fun ann -> Doc ann0 Source # prettyListBy :: PrettyConfigClassic configName -> [ Term tyname name uni fun ann] -> Doc ann0 Source # |
|
AsTypeError ( Error uni fun ann) ( Term TyName Name uni fun ()) uni fun ann Source # | |
Defined in PlutusCore.Error _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 (), Kind (), Kind ()) Source # _TypeMismatch :: Prism' ( Error uni fun ann) (ann, Term TyName Name uni fun (), Type TyName uni (), Normalized ( Type TyName uni ())) 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 # |
|
Functor ( Term tyname name uni fun) Source # | |
(tyname ~ TyName , name ~ Name ) => CollectScopeInfo ( Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping collectScopeInfo :: Term tyname name uni fun NameAnn -> ScopeErrorOrInfo Source # |
|
(tyname ~ TyName , name ~ Name ) => EstablishScoping ( Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping |
|
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 # termLet :: ann -> TermDef ( Term tyname name uni fun) tyname name uni fun 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 # |
|
( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term TyName Name uni fun ann) Source # | |
( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term TyDeBruijn DeBruijn uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Eq (==) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source # (/=) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source # |
|
( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Eq (==) :: Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> Bool Source # (/=) :: Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> Bool Source # |
|
( Everywhere uni Show , GShow uni, Closed uni, Show ann, Show name, Show tyname, Show fun) => Show ( Term tyname name uni fun ann) Source # | |
Generic ( Term tyname name uni fun ann) Source # | |
( Everywhere uni NFData , Closed uni, NFData ann, NFData name, NFData tyname, NFData fun) => NFData ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type |
|
( Closed uni, Everywhere uni Flat , Flat fun, Flat ann, Flat tyname, Flat name) => Flat ( Term tyname name uni fun ann) Source # | |
( PrettyClassic tyname, PrettyClassic name, GShow uni, Closed uni, Everywhere uni PrettyConst , Pretty fun, Pretty ann) => Pretty ( Term tyname name uni fun ann) Source # | |
Recursive ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive project :: Term tyname name uni fun ann -> Base ( Term tyname name uni fun ann) ( Term tyname name uni fun ann) Source # cata :: ( Base ( Term tyname name uni fun ann) a -> a) -> Term tyname name uni fun ann -> a Source # para :: ( Base ( Term tyname name uni fun ann) ( Term tyname name uni fun ann, a) -> a) -> Term tyname name uni fun ann -> a Source # gpara :: ( Corecursive ( Term tyname name uni fun ann), Comonad w) => ( forall b. Base ( Term tyname name uni fun ann) (w b) -> w ( Base ( Term tyname name uni fun ann) b)) -> ( Base ( Term tyname name uni fun ann) ( EnvT ( Term tyname name uni fun ann) w a) -> a) -> Term tyname name uni fun ann -> a Source # prepro :: Corecursive ( Term tyname name uni fun ann) => ( forall b. Base ( Term tyname name uni fun ann) b -> Base ( Term tyname name uni fun ann) b) -> ( Base ( Term tyname name uni fun ann) a -> a) -> Term tyname name uni fun ann -> a Source # gprepro :: ( Corecursive ( Term tyname name uni fun ann), Comonad w) => ( forall b. Base ( Term tyname name uni fun ann) (w b) -> w ( Base ( Term tyname name uni fun ann) b)) -> ( forall c. Base ( Term tyname name uni fun ann) c -> Base ( Term tyname name uni fun ann) c) -> ( Base ( Term tyname name uni fun ann) (w a) -> a) -> Term tyname name uni fun ann -> a Source # |
|
Corecursive ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive embed :: Base ( Term tyname name uni fun ann) ( Term tyname name uni fun ann) -> Term tyname name uni fun ann Source # ana :: (a -> Base ( Term tyname name uni fun ann) a) -> a -> Term tyname name uni fun ann Source # apo :: (a -> Base ( Term tyname name uni fun ann) ( Either ( Term tyname name uni fun ann) a)) -> a -> Term tyname name uni fun ann Source # postpro :: Recursive ( Term tyname name uni fun ann) => ( forall b. Base ( Term tyname name uni fun ann) b -> Base ( Term tyname name uni fun ann) b) -> (a -> Base ( Term tyname name uni fun ann) a) -> a -> Term tyname name uni fun ann Source # gpostpro :: ( Recursive ( Term tyname name uni fun ann), Monad m) => ( forall b. m ( Base ( Term tyname name uni fun ann) b) -> Base ( Term tyname name uni fun ann) (m b)) -> ( forall c. Base ( Term tyname name uni fun ann) c -> Base ( Term tyname name uni fun ann) c) -> (a -> Base ( Term tyname name uni fun ann) (m a)) -> a -> Term tyname name uni fun ann Source # |
|
HasUniques ( Term tyname name uni fun ann) => Rename ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Rename |
|
HasConstant ( Term TyName Name uni fun ()) Source # | |
Defined in PlutusCore.Builtin.HasConstant |
|
type Rep ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Type
type
Rep
(
Term
tyname name uni fun ann) =
D1
('
MetaData
"Term" "PlutusCore.Core.Type" "plutus-core-1.0.0.1-76bWF9ZEWyb4eDyjHx0kCS" '
False
) (((
C1
('
MetaCons
"Var" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
name))
:+:
C1
('
MetaCons
"TyAbs" '
PrefixI
'
False
) ((
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
tyname))
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Kind
ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann)))))
:+:
(
C1
('
MetaCons
"LamAbs" '
PrefixI
'
False
) ((
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
name))
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))))
:+:
(
C1
('
MetaCons
"Apply" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))))
:+:
C1
('
MetaCons
"Constant" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Some
(
ValueOf
uni)))))))
:+:
((
C1
('
MetaCons
"Builtin" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
fun))
:+:
C1
('
MetaCons
"TyInst" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann)))))
:+:
(
C1
('
MetaCons
"Unwrap" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann)))
:+:
(
C1
('
MetaCons
"IWrap" '
PrefixI
'
False
) ((
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann)))
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))))
:+:
C1
('
MetaCons
"Error" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann)))))))
|
|
type Base ( Term tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive |
|
type UniOf ( Term 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
)
|
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 #
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 ( CkValue uni fun) Source # | |
Defined in PlutusCore.Evaluation.Machine.Ck |
|
type UniOf ( CekValue uni fun) 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 UniOf ( Term tyname name uni fun ann) Source # | |
Defined in PlutusIR.Core.Type |
data Type tyname uni ann Source #
A
Type
assigned to expressions.
TyVar ann tyname | |
TyFun ann ( Type tyname uni ann) ( Type tyname uni ann) | |
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) | |
TyBuiltin ann ( SomeTypeIn uni) |
Builtin type |
TyLam ann tyname ( Kind ann) ( Type tyname uni ann) | |
TyApp ann ( Type tyname uni ann) ( Type tyname uni ann) |
Instances
typeSubtypes :: Traversal' ( Type tyname uni ann) ( Type tyname uni ann) Source #
Instances
data ParseError Source #
An error encountered during parsing.
UnknownBuiltinType Text SourcePos | |
BuiltinTypeNotAStar Text SourcePos | |
UnknownBuiltinFunction Text SourcePos | |
InvalidBuiltinConstant Text Text SourcePos |
Instances
Version of Plutus Core to be used for the program.
Instances
data Program tyname name uni fun ann Source #
Instances
DefaultPrettyPlcStrategy ( Program tyname name uni fun ann) => PrettyBy PrettyConfigPlc ( Program tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Pretty.Plc prettyBy :: PrettyConfigPlc -> Program tyname name uni fun ann -> Doc ann0 Source # prettyListBy :: PrettyConfigPlc -> [ Program tyname name uni fun ann] -> Doc ann0 Source # |
|
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 prettyBy :: PrettyConfigReadable configName -> Program tyname name uni fun a -> Doc ann Source # prettyListBy :: PrettyConfigReadable configName -> [ Program tyname name uni fun a] -> Doc ann Source # |
|
( 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 prettyBy :: PrettyConfigClassic configName -> Program tyname name uni fun ann -> Doc ann0 Source # prettyListBy :: PrettyConfigClassic configName -> [ Program tyname name uni fun ann] -> Doc ann0 Source # |
|
Functor ( Program tyname name uni fun) Source # | |
(tyname ~ TyName , name ~ Name ) => CollectScopeInfo ( Program tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping 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 |
|
( 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 # | |
( Everywhere uni Show , GShow uni, Closed uni, Show ann, Show name, Show tyname, Show fun) => Show ( Program tyname name uni fun ann) Source # | |
Generic ( Program tyname name uni fun ann) Source # | |
( Everywhere uni NFData , Closed uni, NFData ann, NFData name, NFData tyname, NFData fun) => 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) Source # | |
( PrettyClassic tyname, PrettyClassic name, GShow uni, Closed uni, Everywhere uni PrettyConst , Pretty fun, Pretty ann) => Pretty ( 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 |
|
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.0.0.1-76bWF9ZEWyb4eDyjHx0kCS" '
False
) (
C1
('
MetaCons
"Program" '
PrefixI
'
True
) (
S1
('
MetaSel
('
Just
"_progAnn") '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
(
S1
('
MetaSel
('
Just
"_progVer") '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Version
ann))
:*:
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.
Name | |
|
Instances
We use a
newtype
to enforce separation between names used for types and
those used for terms.
Instances
Eq TyName Source # | |
Ord TyName Source # | |
Show TyName Source # | |
Generic TyName Source # | |
Hashable TyName Source # | |
NFData TyName Source # | |
Defined in PlutusCore.Name |
|
Flat TyName Source # | |
Wrapped TyName Source # | |
ToScopedName TyName Source # | |
Defined in PlutusCore.Check.Scoping toScopedName :: TyName -> ScopedName Source # |
|
Lift TyName Source # | |
HasPrettyConfigName config => PrettyBy config TyName Source # | |
HasUnique TyName TypeUnique Source # | |
Defined in PlutusCore.Name |
|
tyname ~ TyName => Reference TyName ( Type tyname uni) Source # | |
Defined in PlutusCore.Core.Instance.Scoping 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 referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source # |
|
tyname ~ TyName => Reference TyName ( Term tyname name uni fun) Source # | |
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source # |
|
tyname ~ TyName => Reference TyName ( Binding tyname name uni fun) Source # | |
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> Binding tyname name uni fun NameAnn -> Binding tyname name uni fun NameAnn Source # |
|
tyname ~ TyName => Reference TyName ( Datatype tyname name uni fun) Source # |
Scoping for data types is hard, so we employ some extra paranoia and reference the provided
|
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> Datatype tyname name uni fun NameAnn -> Datatype tyname name uni fun NameAnn Source # |
|
tyname ~ TyName => Reference TyName ( VarDecl tyname name uni fun) Source # | |
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name0. ToScopedName name0 => name0 -> NameAnn ) -> TyName -> VarDecl tyname name uni fun NameAnn -> VarDecl tyname name uni fun NameAnn Source # |
|
Flat ( Binder TyName ) Source # | |
( 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 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 # termLet :: ann -> TermDef ( Term name uni fun) TyName name uni fun 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 _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 (), Kind (), Kind ()) Source # _TypeMismatch :: Prism' ( Error uni fun ann) (ann, Term TyName Name uni fun (), Type TyName uni (), Normalized ( Type TyName uni ())) 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 ( Error uni fun a) ( Term TyName Name uni fun ()) uni fun a Source # | |
Defined in PlutusIR.Error _TypeError :: Prism' ( Error uni fun a) ( TypeError ( Term TyName Name uni fun ()) uni fun a) Source # _KindMismatch :: Prism' ( Error uni fun a) (a, Type TyName uni (), Kind (), Kind ()) Source # _TypeMismatch :: Prism' ( Error uni fun a) (a, Term TyName Name uni fun (), Type TyName uni (), Normalized ( Type TyName uni ())) Source # _FreeTypeVariableE :: Prism' ( Error uni fun a) (a, TyName ) Source # _FreeVariableE :: Prism' ( Error uni fun a) (a, Name ) Source # _UnknownBuiltinFunctionE :: Prism' ( Error uni fun a) (a, 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 # | |
Defined in PlutusCore.Builtin.HasConstant |
|
( Reference TyName t, Reference Name t) => Reference ( Binding TyName Name uni fun ann) t Source # | |
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name. ToScopedName name => name -> NameAnn ) -> Binding TyName Name uni fun ann -> t NameAnn -> t NameAnn Source # |
|
( Reference TyName t, Reference Name t) => Reference ( Datatype TyName Name uni fun ann) t Source # | |
Defined in PlutusIR.Core.Instance.Scoping referenceVia :: ( forall name. ToScopedName name => name -> NameAnn ) -> Datatype TyName Name uni fun ann -> t NameAnn -> t NameAnn Source # |
|
type Rep TyName Source # | |
Defined in PlutusCore.Name |
|
type Unwrapped TyName Source # | |
Defined in PlutusCore.Name |
A unique identifier
Instances
Enum Unique Source # | |
Defined in PlutusCore.Name 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 # |
|
Eq Unique Source # | |
Ord Unique Source # | |
Show Unique Source # | |
Hashable Unique Source # | |
NFData Unique Source # | |
Defined in PlutusCore.Name |
|
Flat Unique Source # | |
Pretty Unique Source # | |
ExMemoryUsage Unique Source # | |
Defined in PlutusCore.Evaluation.Machine.ExMemory memoryUsage :: Unique -> ExMemory Source # |
|
Lift Unique Source # | |
HasUnique Unique Unique Source # | |
newtype UniqueMap unique a Source #
A mapping from uniques to values of type
a
.
UniqueMap | |
|
newtype Normalized a Source #
Normalized | |
|
Instances
defaultVersion :: ann -> Version ann Source #
The default 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 k (fun :: k) ann k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) ann) ann ann Source #
varDeclName :: forall tyname name uni k (fun :: k) ann name k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) ann) name name Source #
varDeclType :: forall tyname name uni k (fun :: k) ann tyname uni k (fun :: k). Lens ( VarDecl tyname name uni (fun :: k) ann) ( VarDecl tyname name uni (fun :: k) 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 #
progVer :: forall tyname name uni fun ann. Lens' ( Program tyname name uni fun ann) ( Version 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
Eq DeBruijn Source # | |
Show DeBruijn Source # | |
Generic DeBruijn Source # | |
NFData DeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal |
|
Flat DeBruijn Source # | |
HasIndex DeBruijn Source # | |
HasPrettyConfigName config => PrettyBy config DeBruijn Source # | |
Flat ( Binder DeBruijn ) Source # | |
( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term DeBruijn uni fun ann) Source # | |
( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term TyDeBruijn DeBruijn uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Eq (==) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source # (/=) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source # |
|
type Rep DeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal |
data NamedDeBruijn Source #
A term name as a de Bruijn index.
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
TyName
s and
Name
s into a
Term
with
NamedTyDeBruijn
s and
NamedDeBruijn
s.
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
NamedTyDeBruijn
s and
NamedDeBruijn
s into a
Term
with
TyName
s and
Name
s.
Will throw an error if a free variable is encountered.
Lexer
The data type
SourcePos
represents source positions. It contains the
name of the source file, a line number, and a column number. Source line
and column positions change intensively during parsing, so we need to
make them strict to avoid memory leaks.
Instances
Eq SourcePos | |
Data SourcePos | |
Defined in Text.Megaparsec.Pos 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 # |
|
Ord SourcePos | |
Defined in Text.Megaparsec.Pos |
|
Read SourcePos | |
Show SourcePos | |
Generic SourcePos | |
NFData SourcePos | |
Defined in Text.Megaparsec.Pos |
|
Pretty SourcePos Source # | |
type Rep SourcePos | |
Defined in Text.Megaparsec.Pos
type
Rep
SourcePos
=
D1
('
MetaData
"SourcePos" "Text.Megaparsec.Pos" "megaparsec-9.2.1-EI4cRL0SAfYAOxBOfPeCV9" '
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
))))
|
Formatting
format :: ( Monad m, PrettyBy config ( Program TyName Name DefaultUni DefaultFun SourcePos )) => config -> ByteString -> m Text Source #
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
)
|
|
type HasUniques ( Program tyname name uni fun ann) Source # | |
Defined in PlutusIR.Core.Type |
|
type HasUniques ( Term tyname name uni fun ann) Source # | |
Defined in PlutusIR.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.
rename :: MonadQuote m => a -> m a Source #
Rename
Unique
s 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 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 |
|
HasUniques ( Term tyname name uni fun ann) => Rename ( Program tyname name uni fun ann) Source # | |
Defined in PlutusIR.Transform.Rename |
|
HasUniques ( Term tyname name uni fun ann) => Rename ( Term tyname name uni fun ann) Source # | |
Defined in PlutusIR.Transform.Rename |
Type checking
class ToKind (uni :: Type -> Type ) Source #
For computing the Plutus kind of a built-in type. See
kindOfBuiltinType
.
Instances
ToKind DefaultUni Source # | |
Defined in PlutusCore.Default.Universe toSingKind :: forall k (a :: k). DefaultUni ( Esc a) -> SingKind k Source # |
type Typecheckable uni fun = ( ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun) Source #
Configuration.
newtype BuiltinTypes uni fun Source #
BuiltinTypes | |
|
newtype TypeCheckConfig uni fun Source #
Configuration of the type checker.
TypeCheckConfig | |
|
tccBuiltinTypes :: HasTypeCheckConfig c uni fun => Lens' c ( BuiltinTypes uni fun) Source #
builtinMeaningsToTypes :: ( MonadError err m, AsTypeError err term uni fun ann, Typecheckable uni fun) => ann -> m ( BuiltinTypes uni fun) Source #
Extract the
TypeScheme
from a
BuiltinMeaning
and convert it to the
corresponding
Type
for each built-in function.
getDefTypeCheckConfig :: ( MonadError err m, AsTypeError err term uni fun ann, Typecheckable uni fun) => ann -> m ( TypeCheckConfig uni fun) Source #
Get the default type checking config.
Kind type inference checking.
inferKind :: ( MonadQuote m, MonadError err m, AsTypeError err term uni fun ann, ToKind uni) => TypeCheckConfig uni fun -> Type TyName uni ann -> m ( Kind ()) Source #
Infer the kind of a type.
checkKind :: ( MonadQuote m, MonadError err m, AsTypeError err term uni fun ann, ToKind uni) => TypeCheckConfig uni fun -> ann -> Type TyName uni ann -> Kind () -> m () Source #
Check a type against a kind.
Infers the kind of the type and checks that it's equal to the given kind
throwing a
TypeError
(annotated with the value of the
ann
argument) otherwise.
inferType :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> Term TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ())) Source #
Infer the type of a term.
checkType :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> ann -> Term TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m () Source #
Check a term against a type.
Infers the type of the term and checks that it's equal to the given type
throwing a
TypeError
(annotated with the value of the
ann
argument) otherwise.
inferTypeOfProgram :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> Program TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ())) Source #
Infer the type of a program.
checkTypeOfProgram :: ( MonadError err m, MonadQuote m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, GEq uni, Ix fun) => TypeCheckConfig uni fun -> ann -> Program TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m () Source #
Check a program against a type.
Infers the type of the program and checks that it's equal to the given type
throwing a
TypeError
(annotated with the value of the
ann
argument) otherwise.
printType :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun SourcePos , MonadError e m) => ByteString -> m Text Source #
normalizeTypesIn :: ( HasUnique tyname TypeUnique , HasUnique name TermUnique , MonadQuote m, HasUniApply uni) => Term tyname name uni fun ann -> m ( Term tyname name uni fun ann) Source #
normalizeTypesInProgram :: ( HasUnique tyname TypeUnique , HasUnique name TermUnique , MonadQuote m, HasUniApply uni) => 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 #
_TypeError :: Prism' r ( TypeError term uni fun ann) Source #
_KindMismatch :: Prism' r (ann, Type TyName uni (), Kind (), Kind ()) Source #
_TypeMismatch :: Prism' r (ann, term, Type TyName uni (), Normalized ( Type TyName uni ())) Source #
_FreeTypeVariableE :: Prism' r (ann, TyName ) Source #
_FreeVariableE :: Prism' r (ann, Name ) Source #
_UnknownBuiltinFunctionE :: Prism' r (ann, fun) Source #
Instances
data TypeError term uni fun ann Source #
Instances
parseTypecheck :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun SourcePos , MonadError e m, MonadQuote m) => TypeCheckConfig DefaultUni DefaultFun -> ByteString -> m ( Normalized ( Type TyName DefaultUni ())) Source #
Parse a program and typecheck it.
typecheckPipeline :: ( AsTypeError e ( Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun a, MonadError e m, MonadQuote m) => TypeCheckConfig DefaultUni DefaultFun -> Program TyName Name DefaultUni DefaultFun a -> m ( Normalized ( Type TyName DefaultUni ())) Source #
Typecheck a program.
Errors
data Error uni fun ann Source #
ParseErrorE ParseError | |
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 #
_Error :: Prism' r ( Error uni fun ann) Source #
_ParseErrorE :: Prism' r ParseError 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 #
Instances
AsError ( Error uni fun ann) uni fun ann Source # | |
Defined in PlutusCore.Error _Error :: Prism' ( Error uni fun ann) ( Error uni fun ann) Source # _ParseErrorE :: Prism' ( Error uni fun ann) ParseError 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 #
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 prettyBy :: config -> NormCheckError tyname name uni fun ann -> Doc ann0 Source # prettyListBy :: config -> [ NormCheckError tyname name uni fun ann] -> Doc ann0 Source # |
|
Functor ( NormCheckError tyname name uni fun) Source # | |
Defined in PlutusCore.Error 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 # |
|
( 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 (==) :: 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 # |
|
( Everywhere uni Show , GShow uni, Closed uni, Show ann, Show tyname, Show name, Show fun) => Show ( NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error |
|
Generic ( NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error 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 # |
|
( Everywhere uni NFData , Closed uni, NFData ann, NFData tyname, NFData name, NFData fun) => NFData ( NormCheckError tyname name uni fun ann) Source # | |
Defined in PlutusCore.Error rnf :: NormCheckError tyname name uni fun ann -> () Source # |
|
HasErrorCode ( NormCheckError _a _b _c _d _e) Source # | |
Defined in PlutusCore.Error errorCode :: NormCheckError _a _b _c _d _e -> ErrorCode Source # |
|
AsNormCheckError ( NormCheckError tyname name uni fun ann) tyname name uni fun ann Source # | |
Defined in PlutusCore.Error _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.0.0.1-76bWF9ZEWyb4eDyjHx0kCS" '
False
) (
C1
('
MetaCons
"BadType" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Type
tyname uni ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
Text
)))
:+:
C1
('
MetaCons
"BadTerm" '
PrefixI
'
False
) (
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
ann)
:*:
(
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
(
Term
tyname name uni fun ann))
:*:
S1
('
MetaSel
('
Nothing
::
Maybe
Symbol
) '
NoSourceUnpackedness
'
NoSourceStrictness
'
DecidedLazy
) (
Rec0
Text
))))
|
class AsNormCheckError r tyname name uni fun ann | r -> tyname name uni fun ann where Source #
_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 # | |
Defined in PlutusCore.Error |
|
AsNormCheckError ( NormCheckError tyname name uni fun ann) tyname name uni fun ann Source # | |
Defined in PlutusCore.Error _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 #
MultiplyDefined Unique ann ann | |
IncoherentUsage Unique ann ann | |
FreeVariable Unique ann |
Instances
class AsUniqueError r ann | r -> ann where Source #
_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 _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 _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.
Instances
class AsFreeVariableError r where Source #
_FreeVariableError :: Prism' r FreeVariableError Source #
_FreeUnique :: Prism' r Unique Source #
_FreeIndex :: Prism' r Index Source #
Instances
AsFreeVariableError FreeVariableError Source # | |
AsFreeVariableError ( Error uni fun ann) Source # | |
Defined in PlutusCore.Error _FreeVariableError :: Prism' ( Error uni fun ann) FreeVariableError Source # |
|
AsFreeVariableError ( Error uni fun a) Source # | |
Defined in PlutusIR.Error _FreeVariableError :: Prism' ( Error uni fun a) FreeVariableError Source # |
Base functors
data TermF (tyname :: Type ) (name :: Type ) (uni :: Type -> Type ) (fun :: Type ) (ann :: Type ) r Source #
VarF ann name | |
TyAbsF ann tyname ( Kind ann) r | |
LamAbsF ann name ( Type tyname uni ann) r | |
ApplyF ann r r | |
ConstantF ann ( Some ( ValueOf uni)) | |
BuiltinF ann fun | |
TyInstF ann r ( Type tyname uni ann) | |
UnwrapF ann r | |
IWrapF ann ( Type tyname uni ann) ( Type tyname uni ann) r | |
ErrorF ann ( Type tyname uni ann) |
Instances
Functor ( TermF tyname name uni fun ann) Source # | |
Foldable ( TermF tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive fold :: Monoid m => TermF tyname name uni fun ann m -> m Source # foldMap :: Monoid m => (a -> m) -> TermF tyname name uni fun ann a -> m Source # foldMap' :: Monoid m => (a -> m) -> TermF tyname name uni fun ann a -> m Source # foldr :: (a -> b -> b) -> b -> TermF tyname name uni fun ann a -> b Source # foldr' :: (a -> b -> b) -> b -> TermF tyname name uni fun ann a -> b Source # foldl :: (b -> a -> b) -> b -> TermF tyname name uni fun ann a -> b Source # foldl' :: (b -> a -> b) -> b -> TermF tyname name uni fun ann a -> b Source # foldr1 :: (a -> a -> a) -> TermF tyname name uni fun ann a -> a Source # foldl1 :: (a -> a -> a) -> TermF tyname name uni fun ann a -> a Source # toList :: TermF tyname name uni fun ann a -> [a] Source # null :: TermF tyname name uni fun ann a -> Bool Source # length :: TermF tyname name uni fun ann a -> Int Source # elem :: Eq a => a -> TermF tyname name uni fun ann a -> Bool Source # maximum :: Ord a => TermF tyname name uni fun ann a -> a Source # minimum :: Ord a => TermF tyname name uni fun ann a -> a Source # sum :: Num a => TermF tyname name uni fun ann a -> a Source # product :: Num a => TermF tyname name uni fun ann a -> a Source # |
|
Traversable ( TermF tyname name uni fun ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive traverse :: Applicative f => (a -> f b) -> TermF tyname name uni fun ann a -> f ( TermF tyname name uni fun ann b) Source # sequenceA :: Applicative f => TermF tyname name uni fun ann (f a) -> f ( TermF tyname name uni fun ann a) Source # mapM :: Monad m => (a -> m b) -> TermF tyname name uni fun ann a -> m ( TermF tyname name uni fun ann b) Source # sequence :: Monad m => TermF tyname name uni fun ann (m a) -> m ( TermF tyname name uni fun ann a) Source # |
data TypeF (tyname :: Type ) (uni :: Type -> Type ) (ann :: Type ) r Source #
TyVarF ann tyname | |
TyFunF ann r r | |
TyIFixF ann r r | |
TyForallF ann tyname ( Kind ann) r | |
TyBuiltinF ann ( SomeTypeIn uni) | |
TyLamF ann tyname ( Kind ann) r | |
TyAppF ann r r |
Instances
Functor ( TypeF tyname uni ann) Source # | |
Foldable ( TypeF tyname uni ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive fold :: Monoid m => TypeF tyname uni ann m -> m Source # foldMap :: Monoid m => (a -> m) -> TypeF tyname uni ann a -> m Source # foldMap' :: Monoid m => (a -> m) -> TypeF tyname uni ann a -> m Source # foldr :: (a -> b -> b) -> b -> TypeF tyname uni ann a -> b Source # foldr' :: (a -> b -> b) -> b -> TypeF tyname uni ann a -> b Source # foldl :: (b -> a -> b) -> b -> TypeF tyname uni ann a -> b Source # foldl' :: (b -> a -> b) -> b -> TypeF tyname uni ann a -> b Source # foldr1 :: (a -> a -> a) -> TypeF tyname uni ann a -> a Source # foldl1 :: (a -> a -> a) -> TypeF tyname uni ann a -> a Source # toList :: TypeF tyname uni ann a -> [a] Source # null :: TypeF tyname uni ann a -> Bool Source # length :: TypeF tyname uni ann a -> Int Source # elem :: Eq a => a -> TypeF tyname uni ann a -> Bool Source # maximum :: Ord a => TypeF tyname uni ann a -> a Source # minimum :: Ord a => TypeF tyname uni ann a -> a Source # |
|
Traversable ( TypeF tyname uni ann) Source # | |
Defined in PlutusCore.Core.Instance.Recursive traverse :: Applicative f => (a -> f b) -> TypeF tyname uni ann a -> f ( TypeF tyname uni ann b) Source # sequenceA :: Applicative f => TypeF tyname uni ann (f a) -> f ( TypeF tyname uni ann a) Source # mapM :: Monad m => (a -> m b) -> TypeF tyname uni ann a -> m ( TypeF tyname uni ann b) Source # sequence :: Monad m => TypeF tyname uni ann (m a) -> m ( TypeF tyname uni ann a) 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 # | |
MonadReader r m => MonadReader r ( QuoteT m) Source # | |
MonadState s m => MonadState s ( QuoteT m) Source # | |
MonadError e m => MonadError e ( QuoteT m) Source # | |
Defined in PlutusCore.Quote throwError :: e -> QuoteT m a Source # catchError :: QuoteT m a -> (e -> QuoteT m a) -> QuoteT m a Source # |
|
MonadWriter w m => MonadWriter w ( QuoteT m) Source # | |
Monad m => Monad ( QuoteT m) Source # | |
Functor m => Functor ( QuoteT m) Source # | |
Monad m => Applicative ( QuoteT m) Source # | |
Defined in PlutusCore.Quote |
|
MonadIO m => MonadIO ( QuoteT m) Source # | |
Monad m => MonadQuote ( QuoteT m) Source # | |
MFunctor QuoteT 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 ( MaybeT m) Source # | |
MonadQuote m => MonadQuote ( PropertyT m) Source # | |
MonadQuote m => MonadQuote ( GenT m) Source # | |
Monad m => MonadQuote ( QuoteT m) Source # | |
MonadQuote m => MonadQuote ( ReaderT r m) Source # | |
MonadQuote m => MonadQuote ( StateT s m) Source # | |
MonadQuote m => MonadQuote ( ExceptT e m) Source # | |
MonadQuote m => MonadQuote ( RenameT ren m) Source # | |
( Stream s, MonadQuote m) => MonadQuote ( ParsecT e s m) Source # | |
MonadQuote m => MonadQuote ( NormalizeTypeT m tyname uni ann) Source # | |
Defined in PlutusCore.Normalize.Internal liftQuote :: Quote a -> NormalizeTypeT m tyname uni ann a Source # |
|
MonadQuote m => MonadQuote ( DefT key uni fun ann m) 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
.
Instances
data UnliftingMode Source #
Determines how to unlift arguments. The difference is that with
UnliftingImmediate
unlifting
is performed immediately after a builtin gets the argument and so can fail immediately too, while
with deferred unlifting all arguments are unlifted upon full saturation, hence no failure can
occur until that. The former makes it much harder to specify the behaviour of builtins and
so
UnliftingDeferred
is the preferred mode.
Combining programs
applyProgram :: Monoid a => Program tyname name uni fun a -> Program tyname name uni fun a -> Program tyname name uni fun a Source #
Take one PLC program and apply it to another.
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.
Budgeting defaults
defaultBuiltinCostModel :: BuiltinCostModel Source #
The default cost model for built-in functions.
defaultBuiltinsRuntime :: HasConstantIn DefaultUni term => BuiltinsRuntime DefaultFun term Source #
defaultCekMachineCosts :: CekMachineCosts Source #
Default costs for CEK machine instructions.
defaultCostModelParams :: Maybe CostModelParams Source #
The default cost model data. This is exposed to the ledger, so let's not confuse anybody by mentioning the CEK machine
CEK machine costs
cekMachineCostsPrefix :: Text Source #
The prefix of the field names in the CekMachineCosts type, used for extracting the CekMachineCosts component of the ledger's cost model parameters. See Note [Cost model parameters] in CostModelInterface.
data CekMachineCosts Source #
Costs for evaluating AST nodes. Times should be specified in picoseconds, memory sizes in bytes.
CekMachineCosts | |
|