{-# LANGUAGE LambdaCase #-}

module UntypedPlutusCore.Contexts where

import UntypedPlutusCore.Core (Term (..))
import UntypedPlutusCore.Core.Instance.Eq ()

-- | A context for an iterated term/type application.
data AppCtx name uni fun a
  = AppCtxTerm a (Term name uni fun a) (AppCtx name uni fun a)
  | AppCtxType a (AppCtx name uni fun a)
  | AppCtxEnd

{-| Takes a term and views it as a head plus an 'AppCtx', e.g.
@
  [{ f t } u v]
  -->
  (f, [{ _ t } u v])
  ==
  f (AppCtxType t (AppCtxTerm u (AppCtxTerm v AppCtxEnd)))
@ -}
splitAppCtx :: Term nam uni fun a -> (Term nam uni fun a, AppCtx nam uni fun a)
splitAppCtx :: forall nam (uni :: * -> *) fun a.
Term nam uni fun a -> (Term nam uni fun a, AppCtx nam uni fun a)
splitAppCtx = AppCtx nam uni fun a
-> Term nam uni fun a -> (Term nam uni fun a, AppCtx nam uni fun a)
forall {name} {uni :: * -> *} {fun} {a}.
AppCtx name uni fun a
-> Term name uni fun a
-> (Term name uni fun a, AppCtx name uni fun a)
go AppCtx nam uni fun a
forall name (uni :: * -> *) fun a. AppCtx name uni fun a
AppCtxEnd
  where
    go :: AppCtx name uni fun a
-> Term name uni fun a
-> (Term name uni fun a, AppCtx name uni fun a)
go AppCtx name uni fun a
appCtx = \case
      Apply a
ann Term name uni fun a
function Term name uni fun a
argument -> AppCtx name uni fun a
-> Term name uni fun a
-> (Term name uni fun a, AppCtx name uni fun a)
go (a
-> Term name uni fun a
-> AppCtx name uni fun a
-> AppCtx name uni fun a
forall name (uni :: * -> *) fun a.
a
-> Term name uni fun a
-> AppCtx name uni fun a
-> AppCtx name uni fun a
AppCtxTerm a
ann Term name uni fun a
argument AppCtx name uni fun a
appCtx) Term name uni fun a
function
      Force a
ann Term name uni fun a
forcedTerm -> AppCtx name uni fun a
-> Term name uni fun a
-> (Term name uni fun a, AppCtx name uni fun a)
go (a -> AppCtx name uni fun a -> AppCtx name uni fun a
forall name (uni :: * -> *) fun a.
a -> AppCtx name uni fun a -> AppCtx name uni fun a
AppCtxType a
ann AppCtx name uni fun a
appCtx) Term name uni fun a
forcedTerm
      Term name uni fun a
term -> (Term name uni fun a
term, AppCtx name uni fun a
appCtx)

-- | Fills in the hole in an 'AppCtx', the inverse of 'splitAppCtx'.
fillAppCtx
  :: Term name uni fun ann
  -> AppCtx name uni fun ann
  -> Term name uni fun ann
fillAppCtx :: forall name (uni :: * -> *) fun ann.
Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
fillAppCtx Term name uni fun ann
term = \case
  AppCtx name uni fun ann
AppCtxEnd -> Term name uni fun ann
term
  AppCtxTerm ann
ann Term name uni fun ann
arg AppCtx name uni fun ann
ctx -> Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
fillAppCtx (ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ann
ann Term name uni fun ann
term Term name uni fun ann
arg) AppCtx name uni fun ann
ctx
  AppCtxType ann
ann AppCtx name uni fun ann
ctx -> Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
fillAppCtx (ann -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ann
ann Term name uni fun ann
term) AppCtx name uni fun ann
ctx