| 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 :: 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 #
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
| Monoid (AppContext tyname name uni fun a) # | |
Defined in PlutusIR.Contexts Methods mempty :: AppContext tyname name uni fun a # mappend :: AppContext tyname name uni fun a -> AppContext tyname name uni fun a -> AppContext tyname name uni fun a # mconcat :: [AppContext tyname name uni fun a] -> AppContext tyname name uni fun a # | |
| Semigroup (AppContext tyname name uni fun a) # | |
Defined in PlutusIR.Contexts Methods (<>) :: AppContext tyname name uni fun a -> AppContext tyname name uni fun a -> AppContext tyname name uni fun a # sconcat :: NonEmpty (AppContext tyname name uni fun a) -> AppContext tyname name uni fun a # stimes :: Integral b => b -> AppContext tyname name uni fun a -> AppContext tyname name uni fun a # | |
splitApplication :: Term tyname name uni fun ann -> (Term tyname name uni fun ann, AppContext tyname name uni fun ann) #
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 #
Fills in the hole in an AppContext, the inverse of splitApplication.
dropAppContext :: Arity -> Maybe Saturation #
Do the given arguments saturate the given arity?
data SplitMatchContext tyname name uni fun a #
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
| |
extractTyArgs :: AppContext tyname name uni fun a -> Maybe [Type tyname uni a] #
Extract the type application arguments from an AppContext.
Returns Nothing if the context contains a TermAppContext.
See test_extractTyArgs
splitNormalDatatypeMatch :: (TypeUnique) => VarsInfo tyname name uni a -> name -> Prism' (AppContext tyname name uni fun a) (SplitMatchContext tyname name uni fun a) #
Split a normal datatype match.