Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
- 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.
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
Monoid (AppContext tyname name uni fun a) Source # | |
Defined in PlutusIR.Contexts 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 # | |
Defined in PlutusIR.Contexts (<>) ∷ 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 #
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.
SplitMatchContext | |
|
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
.