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

PlutusIR.Contexts

Description

Datatypes representing 'contexts with holes' in Plutus IR terms.

Useful for focussing on a sub-part of a term and then reconstructing the term, but with the context as a reified datatype that can be inspected and modified.

Synopsis

Documentation

data AppContext tyname name uni fun ann Source #

A context for an iterated term/type application, with the hole at the head of the application.

Constructors

TermAppContext (Term tyname name uni fun ann) ann (AppContext tyname name uni fun ann) 
TypeAppContext (Type tyname uni ann) ann (AppContext tyname name uni fun ann) 
AppContextEnd 

Instances

Instances details
Monoid (AppContext tyname name uni fun a) Source # 
Instance details

Defined in PlutusIR.Contexts

Methods

memptyAppContext tyname name uni fun a Source #

mappendAppContext tyname name uni fun a → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

mconcat ∷ [AppContext tyname name uni fun a] → AppContext tyname name uni fun a Source #

Semigroup (AppContext tyname name uni fun a) Source # 
Instance details

Defined in PlutusIR.Contexts

Methods

(<>)AppContext tyname name uni fun a → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

sconcatNonEmpty (AppContext tyname name uni fun a) → AppContext tyname name uni fun a Source #

stimesIntegral b ⇒ b → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

splitApplicationTerm tyname name uni fun ann → (Term tyname name uni fun ann, AppContext tyname name uni fun ann) Source #

Takes a term and views it as a head plus an AppContext, e.g.

    [{ f t } u v]
    -->
    (f, [{ _ t } u v])
    ==
    f (TypeAppContext t (TermAppContext u (TermAppContext v AppContextEnd)))

fillAppContextTerm tyname name uni fun ann → AppContext tyname name uni fun ann → Term tyname name uni fun ann Source #

Fills in the hole in an AppContext, the inverse of splitApplication.

dropAppContextIntAppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

lengthContextAppContext tyname name uni fun a → Int Source #

splitAppContextIntAppContext tyname name uni fun a → (AppContext tyname name uni fun a, AppContext tyname name uni fun a) Source #

appendAppContextAppContext tyname name uni fun a → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

saturatesAppContext tyname name uni fun a → ArityMaybe Saturation Source #

Do the given arguments saturate the given arity?

data SplitMatchContext tyname name uni fun a Source #

A split up version of the AppContext for a datatype match, with the various parts we might want to look at.

We have this datatype to make it easier to abstract over different ways that a match might be constructed at the term level. For example, some builtin "matchers" have the arguments in a different order to the matchers from normal PIR datatypes.

Constructors

SplitMatchContext 

Fields

extractTyArgsAppContext tyname name uni fun a → Maybe [Type tyname uni a] Source #

Extract the type application arguments from an AppContext. Returns Nothing if the context contains a TermAppContext. See test_extractTyArgs

splitNormalDatatypeMatch ∷ (HasUnique name TermUnique, HasUnique tyname TypeUnique) ⇒ VarsInfo tyname name uni a → name → AppContext tyname name uni fun a → Maybe (SplitMatchContext tyname name uni fun a) Source #

Split a normal datatype match.

reconstructNormalDatatypeMatchSplitMatchContext tyname name uni fun a → AppContext tyname name uni fun a Source #

Reconstruct a normal datatype match.

asNormalDatatypeMatch ∷ (HasUnique name TermUnique, HasUnique tyname TypeUnique) ⇒ VarsInfo tyname name uni a → name → Prism' (AppContext tyname name uni fun a) (SplitMatchContext tyname name uni fun a) Source #

Split a normal datatype match.