A specialised variant of showsPrec, using precedence context zero, and returning an ordinary String.

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 TestEquality Tag instance is

>>> :{
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

instance GEq Tag where
   geq = testEquality

this will mean we probably want to have

instance Eq 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 GEq Tag instance would differentiate between different constructors:

>>> :{
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 geq (x :: f a) (y :: f b) may be 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)

A class for "uni has general type application".

Check if the kind of the given type from the universe is Type.

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.

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

The version of Plutus Core used by this program.

The intention is to convey different levels of backwards compatibility for existing scripts: - Major version changes are backwards-incompatible - Minor version changes are backwards-compatible - Patch version changes should be entirely invisible (and we will likely not use this level)

The version used should be changed only when the language itself changes. For example, adding a new kind of term to the language would require a minor version bump; removing a kind of term would require a major version bump.

Similarly, changing the semantics of the language will require a version bump, typically a major one. This is the main reason why the version is actually tracked in the AST: we can have two language versions with identical ASTs but different semantics, so we need to track the version explicitly.

Compatibility is about compatibility for specific scripts, not about e.g. tools which consume scripts. Adding a new kind of term does not change how existing scripts behave, but does change what tools would need to do to process scripts.

We use a newtype to enforce separation between names used for types and those used for terms.

A unique identifier This is normally a positive integral number, except in topUnique where we make use of a negative unique to signify top-level.

A mapping from Uniques to arbitrary values of type a. Since Unique is equivalent to Int (see PlutusCore.Name.Unique), we can use an IntMap representation for this type.

A set containing Uniques. Since Unique is equivalent to Int (see PlutusCore.Name.Unique), we can use an IntSet representation for this type.

Convert a Term with TyNames and Names into a Term with NamedTyDeBruijns and NamedDeBruijns. Will throw an error if a free variable is encountered.

Convert a Term with NamedTyDeBruijns and NamedDeBruijns into a Term with TyNames and Names. Will throw an error if a free variable is encountered.

All kinds of uniques an entity contains.

The class of things that can be renamed. I.e. things that are capable of satisfying the global uniqueness condition.

Normalize every Kind in a Term.

Normalize every Kind in a Program.

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.

A non-transformer version of QuoteT.

See runQuoteT.

The "quotation" monad transformer. Within this monad you can do safe construction of PLC terms using quasiquotation, fresh-name generation, and parsing.

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.

The parameterized type of results various evaluation engines return.

Applies one program to another. Fails if the versions do not match and tries to merge annotations.

Count the number of AST nodes in a term.

Count the number of AST nodes in a type.

Count the number of AST nodes in a kind.

>>> kindAstSize $ Type ()
AstSize {unAstSize = 1}
>>> kindAstSize $ KindArrow () (KindArrow () (Type ()) (Type ())) (Type ())
AstSize {unAstSize = 5} 

Count the number of AST nodes in a program.