{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}

module UntypedPlutusCore.Evaluation.Machine.SteppableCek.DebugDriver
  ( Breakpointable (..)
  , CekState
  , Cmd (..)
  , runDriverT
  , DebugF (..)
    -- | Reexport some functions for convenience
  , mkCekTrans
  , CekTrans
  , F.MonadFree
  , F.iterM
  , F.iterTM
  , F.partialIterT
  , F.cutoff
  , FreeT
  ) where

import UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal

import Control.Lens hiding (Context)
import Control.Monad (void)
import Control.Monad.Reader (MonadReader, ask, local, runReaderT)
import Control.Monad.Trans.Free as F
import Data.Function
import Data.Text

{- Note [Stepping the driver]

The client instructs the driver to do a single step of the Cek (`Step` Cmd) or multiple steps until
a condition is met (`Continue`,`Next`,`Finish`). The driver upon receiving a Command (via `inputF`)
fires a series of `stepF` actions to fulfill the command. A `stepF` action is supposed to move the
underlying CEK machine a *single* step forward. Since the driver is written as a free monad, the
interpretation of the `stepF` action is left open.

When the driver calls `stepF state`, it yields its coroutine with the current driver/cek state
(before the stepping interpretation). The interpreter of `stepF` receives the currentState and
calculates a newstate from it (e.g. **actually stepping the cek machine**). The interpreter then
resumes the driver coroutine with the new state.

The sensible interpretation to this is the CEK's state transition function (`cekTrans oldState
===> newState`), but other exotic options may be: logging the before/after states, or even
"mutating" the running program's variables in the environment before/after the state transition
(similar to C debuggers). The interpreter can even supply a different state transition function
(e.g. `id`), but we see little benefit in it at the moment. Currently all interpreters
(brick,repl,testing) just call`cekTrans`.
-}

{-| Leave abstract the types of annotation and breakpoints.
The only thing the driver requires is an inclusion relation of breakpoints into the Annotation -}
class Breakpointable ann bps | ann -> bps where
  -- MAYBE: we cannot know which breakpoint fired, return instead `Maybe Breakpoint`?
  hasBreakpoints :: ann -> bps -> Bool

-- | The commands that the driver may receive from the client (tui,cli,test,etc)
data Cmd bps
  = {-| Instruct the driver to a *SINGLE* step.
    Note: No need to pass breakpoints here because the stepping granularity is *minimal*. -}
    Step
  | -- | Instruct to multi-step until end-of-program or until breakpoint reached
    Continue bps
  | -- | Instruct to multi-step over the function call at point or until breakpoint reached
    Next bps
  | -- | Instruct to multi-step to end of current function or until breakpoint reached
    Finish bps
  deriving stock (Int -> Cmd bps -> ShowS
[Cmd bps] -> ShowS
Cmd bps -> String
(Int -> Cmd bps -> ShowS)
-> (Cmd bps -> String) -> ([Cmd bps] -> ShowS) -> Show (Cmd bps)
forall bps. Show bps => Int -> Cmd bps -> ShowS
forall bps. Show bps => [Cmd bps] -> ShowS
forall bps. Show bps => Cmd bps -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall bps. Show bps => Int -> Cmd bps -> ShowS
showsPrec :: Int -> Cmd bps -> ShowS
$cshow :: forall bps. Show bps => Cmd bps -> String
show :: Cmd bps -> String
$cshowList :: forall bps. Show bps => [Cmd bps] -> ShowS
showList :: [Cmd bps] -> ShowS
Show, ReadPrec [Cmd bps]
ReadPrec (Cmd bps)
Int -> ReadS (Cmd bps)
ReadS [Cmd bps]
(Int -> ReadS (Cmd bps))
-> ReadS [Cmd bps]
-> ReadPrec (Cmd bps)
-> ReadPrec [Cmd bps]
-> Read (Cmd bps)
forall bps. Read bps => ReadPrec [Cmd bps]
forall bps. Read bps => ReadPrec (Cmd bps)
forall bps. Read bps => Int -> ReadS (Cmd bps)
forall bps. Read bps => ReadS [Cmd bps]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall bps. Read bps => Int -> ReadS (Cmd bps)
readsPrec :: Int -> ReadS (Cmd bps)
$creadList :: forall bps. Read bps => ReadS [Cmd bps]
readList :: ReadS [Cmd bps]
$creadPrec :: forall bps. Read bps => ReadPrec (Cmd bps)
readPrec :: ReadPrec (Cmd bps)
$creadListPrec :: forall bps. Read bps => ReadPrec [Cmd bps]
readListPrec :: ReadPrec [Cmd bps]
Read)

-- | The drivers's suspension functor
data DebugF uni fun ann bps a
  = -- | Await for the client (e.g. TUI) to tell what to do next (Cmd).
    InputF (Cmd bps -> a)
  | -- | The debug driver wants to log something
    DriverLogF Text a
  | {-| An enumeratee of Driver State (generator+iteratee):
    Yield a state before doing a step, then await for a state to resume after the step.
    See Note [Stepping the driver]. -}
    StepF
      (CekState uni fun ann)
      -- ^ yield with the current driver's state before running a step
      (CekState uni fun ann -> a)
      {-^ resume back with a state after the step interpretation
      | A generator of CekState to yield to client (e.g. TUI) -}
  | UpdateClientF (CekState uni fun ann) a
  deriving stock ((forall a b.
 (a -> b) -> DebugF uni fun ann bps a -> DebugF uni fun ann bps b)
-> (forall a b.
    a -> DebugF uni fun ann bps b -> DebugF uni fun ann bps a)
-> Functor (DebugF uni fun ann bps)
forall a b.
a -> DebugF uni fun ann bps b -> DebugF uni fun ann bps a
forall a b.
(a -> b) -> DebugF uni fun ann bps a -> DebugF uni fun ann bps b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (uni :: * -> *) fun ann bps a b.
a -> DebugF uni fun ann bps b -> DebugF uni fun ann bps a
forall (uni :: * -> *) fun ann bps a b.
(a -> b) -> DebugF uni fun ann bps a -> DebugF uni fun ann bps b
$cfmap :: forall (uni :: * -> *) fun ann bps a b.
(a -> b) -> DebugF uni fun ann bps a -> DebugF uni fun ann bps b
fmap :: forall a b.
(a -> b) -> DebugF uni fun ann bps a -> DebugF uni fun ann bps b
$c<$ :: forall (uni :: * -> *) fun ann bps a b.
a -> DebugF uni fun ann bps b -> DebugF uni fun ann bps a
<$ :: forall a b.
a -> DebugF uni fun ann bps b -> DebugF uni fun ann bps a
Functor)

-- | The monad that the driver operates in
type Driving m uni fun ann bps =
  ( MonadReader (CekState uni fun ann) m -- the state of the debugger
  , MonadFree (DebugF uni fun ann bps) m -- the effects of the driver
  , Breakpointable ann bps
  )

-- | Entrypoint of the driver
runDriverT
  :: forall uni fun ann bps m
   . (Breakpointable ann bps, MonadFree (DebugF uni fun ann bps) m)
  => NTerm uni fun ann -> m ()
runDriverT :: forall (uni :: * -> *) fun ann bps (m :: * -> *).
(Breakpointable ann bps, MonadFree (DebugF uni fun ann bps) m) =>
NTerm uni fun ann -> m ()
runDriverT = m () -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m () -> m ())
-> (NTerm uni fun ann -> m ()) -> NTerm uni fun ann -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT (CekState uni fun ann) m () -> CekState uni fun ann -> m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (CekState uni fun ann) m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
m ()
driver (CekState uni fun ann -> m ())
-> (NTerm uni fun ann -> CekState uni fun ann)
-> NTerm uni fun ann
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NTerm uni fun ann -> CekState uni fun ann
initState
  where
    initState :: NTerm uni fun ann -> CekState uni fun ann
    initState :: NTerm uni fun ann -> CekState uni fun ann
initState = NTerm uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
NTerm uni fun ann -> CekState uni fun ann
Starting

-- | The driver action. The driver repeatedly:

---
-- 1) waits for a `Cmd`
-- 2) runs one or more CEK steps
-- 3) informs the client for CEK updates&logs
---
-- The driver computation exits when it reaches a CEK `Terminating` state.
driver :: Driving m uni fun ann bps => m ()
driver :: forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
m ()
driver =
  m (Cmd bps)
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
m (Cmd bps)
inputF m (Cmd bps) -> (Cmd bps -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- Condition immediately satisfied
    Cmd bps
Step -> (CekState uni fun ann -> Bool) -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil ((CekState uni fun ann -> Bool) -> m ())
-> (CekState uni fun ann -> Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> CekState uni fun ann -> Bool
forall a b. a -> b -> a
const Bool
True
    Continue bps
bs -> (CekState uni fun ann -> Bool) -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil ((CekState uni fun ann -> Bool) -> m ())
-> (CekState uni fun ann -> Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> (ann -> Bool) -> Maybe ann -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ann -> bps -> Bool
forall ann bps. Breakpointable ann bps => ann -> bps -> Bool
`hasBreakpoints` bps
bs) (Maybe ann -> Bool)
-> (CekState uni fun ann -> Maybe ann)
-> CekState uni fun ann
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekState uni fun ann -> Maybe ann
forall (uni :: * -> *) fun ann. CekState uni fun ann -> Maybe ann
cekStateAnn
    Next bps
bs -> do
      CekState uni fun ann
startState <- m (CekState uni fun ann)
forall r (m :: * -> *). MonadReader r m => m r
ask
      (CekState uni fun ann -> Bool) -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil ((CekState uni fun ann -> Bool) -> m ())
-> (CekState uni fun ann -> Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ \CekState uni fun ann
curState ->
        Bool -> (ann -> Bool) -> Maybe ann -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ann -> bps -> Bool
forall ann bps. Breakpointable ann bps => ann -> bps -> Bool
`hasBreakpoints` bps
bs) (CekState uni fun ann -> Maybe ann
forall (uni :: * -> *) fun ann. CekState uni fun ann -> Maybe ann
cekStateAnn CekState uni fun ann
curState)
          Bool -> Bool -> Bool
||
          -- has activation record length been restored?
          let leCtx :: CekState uni fun ann -> CekState uni fun ann -> Bool
leCtx = (Maybe Word -> Maybe Word -> Bool)
-> CekState uni fun ann -> CekState uni fun ann -> Bool
forall state (uni :: * -> *) fun ann ctxLen a.
(state ~ CekState uni fun ann, ctxLen ~ Maybe Word) =>
(ctxLen -> ctxLen -> a) -> state -> state -> a
onCtxLen Maybe Word -> Maybe Word -> Bool
forall a. Ord a => a -> a -> Bool
(<)
           in CekState uni fun ann
curState CekState uni fun ann -> CekState uni fun ann -> Bool
forall {uni :: * -> *} {fun} {ann}.
CekState uni fun ann -> CekState uni fun ann -> Bool
`leCtx` CekState uni fun ann
startState
    Finish bps
bs -> do
      CekState uni fun ann
startState <- m (CekState uni fun ann)
forall r (m :: * -> *). MonadReader r m => m r
ask
      (CekState uni fun ann -> Bool) -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil ((CekState uni fun ann -> Bool) -> m ())
-> (CekState uni fun ann -> Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ \CekState uni fun ann
curState ->
        Bool -> (ann -> Bool) -> Maybe ann -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ann -> bps -> Bool
forall ann bps. Breakpointable ann bps => ann -> bps -> Bool
`hasBreakpoints` bps
bs) (CekState uni fun ann -> Maybe ann
forall (uni :: * -> *) fun ann. CekState uni fun ann -> Maybe ann
cekStateAnn CekState uni fun ann
curState)
          Bool -> Bool -> Bool
||
          -- has activation record length become smaller?
          let ltCtx :: CekState uni fun ann -> CekState uni fun ann -> Bool
ltCtx = (Maybe Word -> Maybe Word -> Bool)
-> CekState uni fun ann -> CekState uni fun ann -> Bool
forall state (uni :: * -> *) fun ann ctxLen a.
(state ~ CekState uni fun ann, ctxLen ~ Maybe Word) =>
(ctxLen -> ctxLen -> a) -> state -> state -> a
onCtxLen Maybe Word -> Maybe Word -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
           in CekState uni fun ann
curState CekState uni fun ann -> CekState uni fun ann -> Bool
forall {uni :: * -> *} {fun} {ann}.
CekState uni fun ann -> CekState uni fun ann -> Bool
`ltCtx` CekState uni fun ann
startState
  where
    -- \| Comparison on states' contexts
    onCtxLen
      :: ( state ~ CekState uni fun ann
         , ctxLen ~ Maybe Word -- `Maybe` because ctx can be missing if terminating
         )
      => (ctxLen -> ctxLen -> a)
      -> state
      -> state
      -> a
    onCtxLen :: forall state (uni :: * -> *) fun ann ctxLen a.
(state ~ CekState uni fun ann, ctxLen ~ Maybe Word) =>
(ctxLen -> ctxLen -> a) -> state -> state -> a
onCtxLen = ((ctxLen -> ctxLen -> a) -> (state -> ctxLen) -> state -> state -> a
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Getting (First Word) (CekState uni fun ann) Word
-> CekState uni fun ann -> Maybe Word
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview ((Context uni fun ann -> Const (First Word) (Context uni fun ann))
-> CekState uni fun ann
-> Const (First Word) (CekState uni fun ann)
forall (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Context uni fun ann -> f (Context uni fun ann))
-> CekState uni fun ann -> f (CekState uni fun ann)
cekStateContext ((Context uni fun ann -> Const (First Word) (Context uni fun ann))
 -> CekState uni fun ann
 -> Const (First Word) (CekState uni fun ann))
-> ((Word -> Const (First Word) Word)
    -> Context uni fun ann -> Const (First Word) (Context uni fun ann))
-> Getting (First Word) (CekState uni fun ann) Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Context uni fun ann -> Word)
-> (Word -> Const (First Word) Word)
-> Context uni fun ann
-> Const (First Word) (Context uni fun ann)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Context uni fun ann -> Word
lenContext))

-- | Do one or more cek steps until Terminating state is reached or condition on 'CekState' is met.
multiStepUntil
  :: Driving m uni fun ann bp
  => (CekState uni fun ann -> Bool) -> m ()
multiStepUntil :: forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil CekState uni fun ann -> Bool
cond = do
  Text -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
Text -> m ()
driverLogF Text
"Driver is going to do a single step"
  CekState uni fun ann
newState <- CekState uni fun ann -> m (CekState uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
CekState uni fun ann -> m (CekState uni fun ann)
stepF (CekState uni fun ann -> m (CekState uni fun ann))
-> m (CekState uni fun ann) -> m (CekState uni fun ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (CekState uni fun ann)
forall r (m :: * -> *). MonadReader r m => m r
ask
  case CekState uni fun ann
newState of
    Terminating {} ->
      -- don't recurse to driver, but EXIT the driver
      CekState uni fun ann -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
CekState uni fun ann -> m ()
updateClientF CekState uni fun ann
newState
    CekState uni fun ann
_ ->
      -- update state
      (CekState uni fun ann -> CekState uni fun ann) -> m () -> m ()
forall a.
(CekState uni fun ann -> CekState uni fun ann) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (CekState uni fun ann
-> CekState uni fun ann -> CekState uni fun ann
forall a b. a -> b -> a
const CekState uni fun ann
newState) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        if CekState uni fun ann -> Bool
cond CekState uni fun ann
newState
          then do
            CekState uni fun ann -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
CekState uni fun ann -> m ()
updateClientF CekState uni fun ann
newState
            m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
m ()
driver -- tail recurse
          else
            (CekState uni fun ann -> Bool) -> m ()
forall (m :: * -> *) (uni :: * -> *) fun ann bp.
Driving m uni fun ann bp =>
(CekState uni fun ann -> Bool) -> m ()
multiStepUntil CekState uni fun ann -> Bool
cond -- tail recurse

-- * boilerplate "suspension actions"

-- Being in 'Driving' monad here is too constraining, but it does not matter.
inputF :: Driving m uni fun ann bps => m (Cmd bps)
inputF :: forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
m (Cmd bps)
inputF = DebugF uni fun ann bps (Cmd bps) -> m (Cmd bps)
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (DebugF uni fun ann bps (Cmd bps) -> m (Cmd bps))
-> DebugF uni fun ann bps (Cmd bps) -> m (Cmd bps)
forall a b. (a -> b) -> a -> b
$ (Cmd bps -> Cmd bps) -> DebugF uni fun ann bps (Cmd bps)
forall (uni :: * -> *) fun ann bps a.
(Cmd bps -> a) -> DebugF uni fun ann bps a
InputF Cmd bps -> Cmd bps
forall a. a -> a
id
driverLogF :: Driving m uni fun ann bps => Text -> m ()
driverLogF :: forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
Text -> m ()
driverLogF Text
text = DebugF uni fun ann bps () -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (DebugF uni fun ann bps () -> m ())
-> DebugF uni fun ann bps () -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> () -> DebugF uni fun ann bps ()
forall (uni :: * -> *) fun ann bps a.
Text -> a -> DebugF uni fun ann bps a
DriverLogF Text
text ()
updateClientF :: Driving m uni fun ann bps => CekState uni fun ann -> m ()
updateClientF :: forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
CekState uni fun ann -> m ()
updateClientF CekState uni fun ann
dState = DebugF uni fun ann bps () -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (DebugF uni fun ann bps () -> m ())
-> DebugF uni fun ann bps () -> m ()
forall a b. (a -> b) -> a -> b
$ CekState uni fun ann -> () -> DebugF uni fun ann bps ()
forall (uni :: * -> *) fun ann bps a.
CekState uni fun ann -> a -> DebugF uni fun ann bps a
UpdateClientF CekState uni fun ann
dState ()
stepF :: Driving m uni fun ann bps => CekState uni fun ann -> m (CekState uni fun ann)
stepF :: forall (m :: * -> *) (uni :: * -> *) fun ann bps.
Driving m uni fun ann bps =>
CekState uni fun ann -> m (CekState uni fun ann)
stepF CekState uni fun ann
yieldState = DebugF uni fun ann bps (CekState uni fun ann)
-> m (CekState uni fun ann)
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (DebugF uni fun ann bps (CekState uni fun ann)
 -> m (CekState uni fun ann))
-> DebugF uni fun ann bps (CekState uni fun ann)
-> m (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ CekState uni fun ann
-> (CekState uni fun ann -> CekState uni fun ann)
-> DebugF uni fun ann bps (CekState uni fun ann)
forall (uni :: * -> *) fun ann bps a.
CekState uni fun ann
-> (CekState uni fun ann -> a) -> DebugF uni fun ann bps a
StepF CekState uni fun ann
yieldState CekState uni fun ann -> CekState uni fun ann
forall a. a -> a
id