module Plutarch.Docs.PatternMatching (pisJust) where 
import Plutarch.Prelude

We've shown how to construct Terms out of the data constructors of types with kind PType (i.e., pcon . PJust). Next, it is natural that we may want to pattern match on Term with a known PType tag (i.e., of a value with type Term s (PMaybe a)) to produce another Term (i.e., depending on whether the value matches PJust _ or Nothing.)

The function that we need is a method of the PMatch typeclass. For the time being, we will ignore the details of implementation and only look at the type:

pmatch :: 
  forall (a :: PType) (b :: PType) (s :: S).
  ( PlutusType a       -- `a` has to be a `PlutusType` instance. 
  ) => Term s a        -- Given a `Term` tagged with `a` and
  -> (a s -> Term s b) -- a continuation from `a s` to a Term s b`, 
  -> Term s b          -- produce a `Term s b`.

The annotation of the second argument deserves some focus; the second argument has its type displayed as (a s -> Term s b). First, recall that a is declared to have kind PType, and PType is a kind synonym for S -> Type. Thus, since s has kind S, we have that a s has the kind Type. That is, it is a regular Haskell type.

What this means, in practice, is that pmatch matches on the possible values of the result of evaluating a Term s a -- specifically, it matches on values of a type that has kind PType -- and branches accordingly. The second argument to pmatch is a continuation; it determines how the program continues once pmatch has done its work.

We have already introduced a type with kind PType suitable for branching: PMaybe. Here is an example:

{- | This function takes in a Haskell-level `PMaybe s` value (specifically, _not_ a `Term`)
     and returns a `Term` depending on the Haskell-level pattern match on `PMaybe`s data
     constructors.
-}
continuation :: PMaybe a s -> Term s PBool
continuation = \case
  PJust _ -> pcon PTrue
  PNothing -> pcon PFalse

{- | A Haskell-level `isJust` on Plutarch `Term`s. `pmatch` can match on
     the possibilities of `PJust _` or `PNothing` being the result of an evaluated
     `Term`.
-}
hisJust :: Term s (PMaybe a) -> Term s PBool
hisJust x = pmatch x continuation

-- | A Plutarch-level `isJust`
pisJust :: Term s (PMaybe a :--> PBool)
pisJust = plam hisJust

Readers should note that this is not the most ergonomic way to deal with pattern matching (Plutarch provides two versions of do syntax), but it is how the more ergonomic methods work under the hood.