{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

module UntypedPlutusCore.Contexts where

import PlutusCore.Arity
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
arg -> 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
arg 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

data Saturation = Oversaturated | Undersaturated | Saturated

-- | Do the given arguments saturate the given arity?
saturates :: AppCtx name uni fun a -> Arity -> Maybe Saturation
-- Exactly right
saturates :: forall name (uni :: * -> *) fun a.
AppCtx name uni fun a -> Arity -> Maybe Saturation
saturates AppCtx name uni fun a
AppCtxEnd [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Saturated
-- Parameters left - undersaturated
saturates AppCtx name uni fun a
AppCtxEnd Arity
_ = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Undersaturated
-- Match a term parameter to a term arg
saturates (AppCtxTerm a
_ Term name uni fun a
_ AppCtx name uni fun a
ctx) (Param
TermParam : Arity
arities) = AppCtx name uni fun a -> Arity -> Maybe Saturation
forall name (uni :: * -> *) fun a.
AppCtx name uni fun a -> Arity -> Maybe Saturation
saturates AppCtx name uni fun a
ctx Arity
arities
-- Match a type parameter to a type arg
saturates (AppCtxType a
_ AppCtx name uni fun a
ctx) (Param
TypeParam : Arity
arities) = AppCtx name uni fun a -> Arity -> Maybe Saturation
forall name (uni :: * -> *) fun a.
AppCtx name uni fun a -> Arity -> Maybe Saturation
saturates AppCtx name uni fun a
ctx Arity
arities
-- Param/arg mismatch
saturates (AppCtxTerm {}) (Param
TypeParam : Arity
_) = Maybe Saturation
forall a. Maybe a
Nothing
saturates (AppCtxType {}) (Param
TermParam : Arity
_) = Maybe Saturation
forall a. Maybe a
Nothing
-- Arguments left - undersaturated
saturates (AppCtxTerm {}) [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Oversaturated
saturates (AppCtxType {}) [] = Saturation -> Maybe Saturation
forall a. a -> Maybe a
Just Saturation
Oversaturated