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 {}
- data SrcSpans
- data Some (tag ∷ k → Type) where
- data SomeTypeIn uni = ∀ k (a ∷ k). SomeTypeIn !(uni (Esc a))
- data Kinded uni ta where
- data ValueOf uni a = ValueOf !(uni (Esc a)) !a
- someValueOf ∷ ∀ a uni. uni (Esc a) → a → Some (ValueOf uni)
- someValue ∷ ∀ 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 ∷ (∀ 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 ∷ ∀ (a ∷ k). Int → t a → ShowS
- show ∷ Show a ⇒ a → String
- class GEq (f ∷ k → Type) where
- class HasUniApply (uni ∷ Type → Type) where
- checkStar ∷ ∀ uni a (x ∷ a). Typeable a ⇒ uni (Esc x) → Maybe (a :~: Type)
- withApplicable ∷ ∀ (a ∷ Type) (ab ∷ Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) ⇒ uni (Esc (f ∷ ab)) → uni (Esc (x ∷ a)) → (∀ (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 ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc List) ⇒ DefaultUni (Esc a1) → DefaultUni a
- pattern DefaultUniPair ∷ ∀ {a} {k1} {k2} {f1 ∷ k1 → k2} {a1 ∷ k1} {k3} {k4} {f2 ∷ k3 → k4} {a2 ∷ k3}. () ⇒ ∀. (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
- | CaseList
- | CaseData
- | DropList
- 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 ∷ ∀ tyname tyname' name name' uni fun ann. (tyname → tyname') → (name → name') → Term tyname name uni fun ann → Term tyname' name' uni fun ann
- programMapNames ∷ ∀ 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 ∷ ∀ 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 {}
- 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 ∷ ∀ tyname ann. Lens' (TyVarDecl tyname ann) ann
- tyVarDeclName ∷ ∀ tyname ann tyname. Lens (TyVarDecl tyname ann) (TyVarDecl tyname ann) tyname tyname
- tyVarDeclKind ∷ ∀ tyname ann. Lens' (TyVarDecl tyname ann) (Kind ann)
- varDeclAnn ∷ ∀ tyname name uni ann. Lens' (VarDecl tyname name uni ann) ann
- varDeclName ∷ ∀ tyname name uni ann name. Lens (VarDecl tyname name uni ann) (VarDecl tyname name uni ann) name name
- varDeclType ∷ ∀ 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 ∷ ∀ tyname uni ann. Lens' (TyDecl tyname uni ann) ann
- tyDeclType ∷ ∀ tyname uni ann tyname uni. Lens (TyDecl tyname uni ann) (TyDecl tyname uni ann) (Type tyname uni ann) (Type tyname uni ann)
- tyDeclKind ∷ ∀ tyname uni ann. Lens' (TyDecl tyname uni ann) (Kind ann)
- progAnn ∷ ∀ tyname name uni fun ann. Lens' (Program tyname name uni fun ann) ann
- progVer ∷ ∀ tyname name uni fun ann. Lens' (Program tyname name uni fun ann) Version
- progTerm ∷ ∀ 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.
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
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 Source #
Existential. This is type is useful to hide GADTs' parameters.
>>>
data Tag :: Type -> Type 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
(Closed uni, Everywhere uni PrettyConst) ⇒ PrettyBy ConstConfig (Some (ValueOf uni)) Source # | |
Defined in PlutusCore.Pretty.PrettyConst Methods prettyBy ∷ ConstConfig → Some (ValueOf uni) → Doc ann Source # prettyListBy ∷ ConstConfig → [Some (ValueOf uni)] → Doc ann Source # | |
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)) Source # | |
GEq tag ⇒ Eq (Some tag) | |
GCompare tag ⇒ Ord (Some tag) | |
(Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) ⇒ Hashable (Some (ValueOf uni)) Source # | |
(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
∀ 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 | |
(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 Source # prettyList ∷ [SomeTypeIn (Kinded uni)] → Doc ann Source # | |
GShow uni ⇒ Show (Kinded uni ta) Source # | |
A value of a particular type from a universe.
Instances
someValueOf ∷ ∀ a uni. uni (Esc a) → a → Some (ValueOf uni) Source #
Wrap a value into Some (ValueOf uni)
, given its explicit type tag.
someValue ∷ ∀ 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 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.
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 ∷ (∀ 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 ∷ (∀ 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 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 = defaultGshowsPrec
Methods
gshowsPrec ∷ ∀ (a ∷ k). Int → t a → ShowS Source #
Instances
GShow SNat | |
Defined in Data.GADT.Internal | |
GShow SChar | |
Defined in Data.GADT.Internal | |
GShow SSymbol | |
Defined in Data.GADT.Internal | |
GShow DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods gshowsPrec ∷ ∀ (a ∷ k). Int → DefaultUni a → ShowS Source # | |
GShow uni ⇒ GShow (Kinded uni ∷ Type → Type) Source # | |
Defined in Universe.Core | |
(GShow uni, Closed uni, Everywhere uni Show) ⇒ GShow (ValueOf uni ∷ Type → Type) Source # | |
Defined in Universe.Core | |
GShow (TypeRep ∷ k → Type) | |
Defined in Data.GADT.Internal | |
GShow ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
GShow (GOrdering a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
(GShow a, GShow b) ⇒ GShow (Product a b ∷ k → Type) |
|
Defined in Data.GADT.Internal | |
(GShow a, GShow b) ⇒ GShow (Sum a b ∷ k → Type) |
|
Defined in Data.GADT.Internal | |
GShow ((:~~:) a ∷ k → Type) | Since: some-1.0.4 |
Defined in Data.GADT.Internal | |
(GShow a, GShow b) ⇒ GShow (a :*: b ∷ k → Type) |
Since: some-1.0.4 |
Defined in Data.GADT.Internal | |
(GShow a, GShow b) ⇒ GShow (a :+: b ∷ k → Type) |
Since: some-1.0.4 |
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.
This class is sometimes confused with TestEquality
from base.
TestEquality
only checks type equality.
Consider
>>>
data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int
The correct
instance isTestEquality
Tag
>>>
:{
instance TestEquality Tag where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt1 TagInt2 = Just Refl testEquality TagInt2 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl :}
While we can define
instanceGEq
Tag wheregeq
=testEquality
this will mean we probably want to have
instanceEq
Tag where _==
_ = True
Note: In the future version of some
package (to be released around GHC-9.6 / 9.8) the
forall a. Eq (f a)
constraint will be added as a constraint to GEq
,
with a law relating GEq
and Eq
:
geq
x y = Just Refl ⇒ x == y = True ∀ (x :: f a) (y :: f b) x == y ≡ isJust (geq
x y) ∀ (x, y :: f a)
So, the more useful
instance would differentiate between
different constructors:GEq
Tag
>>>
:{
instance GEq Tag where geq TagInt1 TagInt1 = Just Refl geq TagInt1 TagInt2 = Nothing geq TagInt2 TagInt1 = Nothing geq TagInt2 TagInt2 = Just Refl :}
which is consistent with a derived Eq
instance for Tag
>>>
deriving instance Eq (Tag a)
Note that even if a ~ b
, the
may
be geq
(x :: f a) (y :: f b)Nothing
(when value terms are inequal).
The consistency of GEq
and Eq
is easy to check by exhaustion:
>>>
let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True
>>>
(checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)
(True,True,True,True)
>>>
let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)
>>>
(checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)
(True,True,True,True)
Methods
geq ∷ ∀ (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 SNat | |
GEq SChar | |
GEq SSymbol | |
GEq DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods geq ∷ ∀ (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 (Product a b ∷ k → Type) | |
(GEq a, GEq b) ⇒ GEq (Sum a b ∷ k → Type) | |
GEq ((:~~:) a ∷ k → Type) | Since: some-1.0.4 |
(GEq a, GEq b) ⇒ GEq (a :*: b ∷ k → Type) | Since: some-1.0.4 |
(GEq f, GEq g) ⇒ GEq (f :+: g ∷ k → Type) | Since: some-1.0.4 |
class HasUniApply (uni ∷ Type → Type) where Source #
A class for "uni
has general type application".
Methods
uniApply ∷ ∀ 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. |
→ (∀ 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 ∷ ∀ k l (f ∷ k → l) (a ∷ k). DefaultUni (Esc f) → DefaultUni (Esc a) → DefaultUni (Esc (f a)) Source # matchUniApply ∷ DefaultUni tb → r → (∀ k l (f ∷ k → l) (a ∷ k). tb ~ Esc (f a) ⇒ DefaultUni (Esc f) → DefaultUni (Esc a) → r) → r Source # |
checkStar ∷ ∀ 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 ∷ ∀ (a ∷ Type) (ab ∷ Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) ⇒ uni (Esc (f ∷ ab)) → uni (Esc (x ∷ a)) → (∀ (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) | Since: some-1.0.3 |
Defined in Data.GADT.DeepSeq | |
GCompare ((:~:) a ∷ k → Type) | |
GEq ((:~:) a ∷ k → Type) | |
GRead ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
GShow ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
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 ∷ (∀ d b0. Data d ⇒ c (d → b0) → d → c b0) → (∀ g. g → c g) → (a :~: b) → c (a :~: b) Source # gunfold ∷ (∀ b0 r. Data b0 ⇒ c (b0 → r) → c r) → (∀ r. r → c r) → Constr → c (a :~: b) Source # toConstr ∷ (a :~: b) → Constr Source # dataTypeOf ∷ (a :~: b) → DataType Source # dataCast1 ∷ Typeable t ⇒ (∀ d. Data d ⇒ c (t d)) → Maybe (c (a :~: b)) Source # dataCast2 ∷ Typeable t ⇒ (∀ d e. (Data d, Data e) ⇒ c (t d e)) → Maybe (c (a :~: b)) Source # gmapT ∷ (∀ b0. Data b0 ⇒ b0 → b0) → (a :~: b) → a :~: b Source # gmapQl ∷ (r → r' → r) → r → (∀ d. Data d ⇒ d → r') → (a :~: b) → r Source # gmapQr ∷ ∀ r r'. (r' → r → r) → r → (∀ d. Data d ⇒ d → r') → (a :~: b) → r Source # gmapQ ∷ (∀ d. Data d ⇒ d → u) → (a :~: b) → [u] Source # gmapQi ∷ Int → (∀ d. Data d ⇒ d → u) → (a :~: b) → u Source # gmapM ∷ Monad m ⇒ (∀ d. Data d ⇒ d → m d) → (a :~: b) → m (a :~: b) Source # gmapMp ∷ MonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → (a :~: b) → m (a :~: b) Source # gmapMo ∷ MonadPlus m ⇒ (∀ 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 ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc List) ⇒ DefaultUni (Esc a1) → DefaultUni a Source #
pattern DefaultUniPair ∷ ∀ {a} {k1} {k2} {f1 ∷ k1 → k2} {a1 ∷ k1} {k3} {k4} {f2 ∷ k3 → k4} {a2 ∷ k3}. () ⇒ ∀. (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