Safe Haskell	Safe-Inferred
Language	Haskell2010

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

data AppContext tyname name uni fun ann
- = 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
splitApplication ∷ Term tyname name uni fun ann → (Term tyname name uni fun ann, AppContext tyname name uni fun ann)
fillAppContext ∷ Term tyname name uni fun ann → AppContext tyname name uni fun ann → Term tyname name uni fun ann
dropAppContext ∷ Int → AppContext tyname name uni fun a → AppContext tyname name uni fun a
lengthContext ∷ AppContext tyname name uni fun a → Int
splitAppContext ∷ Int → AppContext tyname name uni fun a → (AppContext tyname name uni fun a, AppContext tyname name uni fun a)
appendAppContext ∷ AppContext tyname name uni fun a → AppContext tyname name uni fun a → AppContext tyname name uni fun a
data Saturation
- = Oversaturated
- | Undersaturated
- | Saturated
saturates ∷ AppContext tyname name uni fun a → Arity → Maybe Saturation
data SplitMatchContext tyname name uni fun a = SplitMatchContext {
- smTyVars ∷ AppContext tyname name uni fun a
- smScrutinee ∷ (Term tyname name uni fun a, Type tyname uni (), a)
- smResTy ∷ (Type tyname uni a, a)
- smBranches ∷ AppContext tyname name uni fun a
}
extractTyArgs ∷ AppContext tyname name uni fun a → Maybe [Type tyname uni a]
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)
reconstructNormalDatatypeMatch ∷ SplitMatchContext tyname name uni fun a → AppContext tyname name uni fun a
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)

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 mempty ∷ AppContext tyname name uni fun a Source # mappend ∷ AppContext 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 # sconcat ∷ NonEmpty (AppContext tyname name uni fun a) → AppContext tyname name uni fun a Source # stimes ∷ Integral b ⇒ b → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

splitApplication ∷ Term 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)))

fillAppContext ∷ Term 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.

dropAppContext ∷ Int → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

lengthContext ∷ AppContext tyname name uni fun a → Int Source #

splitAppContext ∷ Int → AppContext tyname name uni fun a → (AppContext tyname name uni fun a, AppContext tyname name uni fun a) Source #

appendAppContext ∷ AppContext tyname name uni fun a → AppContext tyname name uni fun a → AppContext tyname name uni fun a Source #

data Saturation Source #

Constructors

Oversaturated
Undersaturated
Saturated

saturates ∷ AppContext tyname name uni fun a → Arity → Maybe 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 smTyVars ∷ AppContext tyname name uni fun a smScrutinee ∷ (Term tyname name uni fun a, Type tyname uni (), a) smResTy ∷ (Type tyname uni a, a) smBranches ∷ AppContext tyname name uni fun a

extractTyArgs ∷ AppContext 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.

reconstructNormalDatatypeMatch ∷ SplitMatchContext 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.