{-|
Copyright        : (c) Galois, Inc. 2025
Maintainer       : Langston Barrett <langston@galois.com>
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.Debug.Context
  ( RunningState(..)
  , DebuggerState(..)
  , CommandImpl(..)
  , ExtImpl(..)
  , voidImpl
  , EvalResult(..)
  , Context(..)
  , initCtx
  , toCompletionEnv
  , toStyleEnv
  ) where

import Data.Parameterized.NatRepr (knownNat)
import Data.Set qualified as Set
import Data.Set (Set)
import Data.Void (Void, absurd)
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Arg.Type qualified as AType
import Lang.Crucible.Debug.Breakpoint (Breakpoint)
import Lang.Crucible.Debug.Command (CommandExt)
import Lang.Crucible.Debug.Complete (CompletionT, CompletionEnv)
import Lang.Crucible.Debug.Complete qualified as Complete
import Lang.Crucible.Debug.Inputs (Inputs)
import Lang.Crucible.Debug.Outputs (Outputs)
import Lang.Crucible.Debug.Regex qualified as Rgx
import Lang.Crucible.Debug.Response (Response)
import Lang.Crucible.Debug.Statement (Statement)
import Lang.Crucible.Debug.Style qualified as Style
import Lang.Crucible.Debug.Style (StyleT, StyleEnv)
import Lang.Crucible.Debug.Trace (Trace)
import Lang.Crucible.Debug.Trace qualified as Trace
import Lang.Crucible.Pretty (IntrinsicPrinters)
import Lang.Crucible.Simulator.EvalStmt qualified as C
import Lang.Crucible.Simulator qualified as C
import Lang.Crucible.Types (TypeRepr)
import What4.Interface qualified as W4

data RunningState
  = -- | User issued 'Cmd.Finish'
    Finish
    -- | User issued 'Cmd.Run'
  | Run
    -- | User issued 'Cmd.Step'
  | Step {-# UNPACK #-} !Int

data DebuggerState
  = Running RunningState
    -- | User issued 'Cmd.Quit'
  | Quit
  | Stopped

data CommandImpl cExt p sym ext t
  = forall r.
    CommandImpl
    { -- | A regular expression describing what kinds of arguments this command
      -- takes. See "Lang.Crucible.Debug.Regex".
      ()
implRegex :: Rgx.RegexRepr AType.ArgTypeRepr r
      -- | The implementation of the command, taking the arguments that result
      -- from matching 'implRegex' against the command line provided by the
      -- user.
    , ()
implBody ::
        Context cExt p sym ext t ->
        C.ExecState p sym ext (C.RegEntry sym t) ->
        Rgx.Match (Arg.Arg cExt) r ->
        IO (EvalResult cExt p sym ext t)
    }

newtype ExtImpl cExt p sym ext t
  = ExtImpl { forall cExt p sym ext (t :: CrucibleType).
ExtImpl cExt p sym ext t -> cExt -> CommandImpl cExt p sym ext t
getExtImpl :: cExt -> CommandImpl cExt p sym ext t }

voidImpl :: ExtImpl Void p sym ext t
voidImpl :: forall p sym ext (t :: CrucibleType). ExtImpl Void p sym ext t
voidImpl = (Void -> CommandImpl Void p sym ext t) -> ExtImpl Void p sym ext t
forall cExt p sym ext (t :: CrucibleType).
(cExt -> CommandImpl cExt p sym ext t) -> ExtImpl cExt p sym ext t
ExtImpl Void -> CommandImpl Void p sym ext t
forall a. Void -> a
absurd

-- | The result of evaluating a 'Statement'
data EvalResult cExt p sym ext t
  = EvalResult
  { forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t -> Context cExt p sym ext t
evalCtx :: Context cExt p sym ext t
  , forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
evalFeatureResult :: C.ExecutionFeatureResult p sym ext (C.RegEntry sym t)
  , forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t -> Response cExt
evalResp :: Response cExt
  }

-- | Debugger state.
--
-- Type parameters:
--
-- * 'cExt' is the command extension type, see 'CommandExt'
-- * 'p', 'sym', 'ext' are as in @OverrideSim@
-- * 't' is the Crucible type of the @RegValue@ returned by the program
--
-- 'cExt' is different from 'ext' because it\'s not necessarily true that you
-- would want the debugger command extensions to be tied in a 1:1 fashion with
-- the syntax extension (source language).
data Context cExt p sym ext t
  = Context
  { forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Set Breakpoint
dbgBreakpoints :: Set Breakpoint
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> CommandExt cExt
dbgCommandExt :: CommandExt cExt
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> ExtImpl cExt p sym ext t
dbgExtImpl :: ExtImpl cExt p sym ext t
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
dbgInputs :: Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Outputs IO (Response cExt)
dbgOutputs :: Outputs IO (Response cExt)
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> IntrinsicPrinters sym
dbgPpIntrinsic :: IntrinsicPrinters sym
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> TypeRepr t
dbgRetTy :: TypeRepr t
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> DebuggerState
dbgState :: DebuggerState
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Bool
dbgStopOnAbort :: Bool
  , forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Trace ext
dbgTrace :: Trace ext
  }

initCtx ::
  W4.IsExpr (W4.SymExpr sym) =>
  CommandExt cExt ->
  ExtImpl cExt p sym ext t ->
  IntrinsicPrinters sym ->
  Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) ->
  Outputs IO (Response cExt) ->
  TypeRepr t ->
  IO (Context cExt p sym ext t)
initCtx :: forall sym cExt p ext (t :: CrucibleType).
IsExpr (SymExpr sym) =>
CommandExt cExt
-> ExtImpl cExt p sym ext t
-> IntrinsicPrinters sym
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr t
-> IO (Context cExt p sym ext t)
initCtx CommandExt cExt
cExts ExtImpl cExt p sym ext t
impl IntrinsicPrinters sym
iFns Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
ins Outputs IO (Response cExt)
outs TypeRepr t
rTy = do
  Trace ext
t <- NatRepr 512 -> IO (Trace ext)
forall (n :: Natural) ext. (1 <= n) => NatRepr n -> IO (Trace ext)
Trace.empty (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @512)  -- arbitrary max size
  Context cExt p sym ext t -> IO (Context cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> IO (Context cExt p sym ext t))
-> Context cExt p sym ext t -> IO (Context cExt p sym ext t)
forall a b. (a -> b) -> a -> b
$
    Context
    { dbgBreakpoints :: Set Breakpoint
dbgBreakpoints = Set Breakpoint
forall a. Set a
Set.empty
    , dbgCommandExt :: CommandExt cExt
dbgCommandExt = CommandExt cExt
cExts
    , dbgExtImpl :: ExtImpl cExt p sym ext t
dbgExtImpl = ExtImpl cExt p sym ext t
impl
    , dbgInputs :: Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
dbgInputs = Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
ins
    , dbgOutputs :: Outputs IO (Response cExt)
dbgOutputs = Outputs IO (Response cExt)
outs
    , dbgPpIntrinsic :: IntrinsicPrinters sym
dbgPpIntrinsic = IntrinsicPrinters sym
iFns
    , dbgRetTy :: TypeRepr t
dbgRetTy = TypeRepr t
rTy
    , dbgState :: DebuggerState
dbgState = DebuggerState
Stopped
    , dbgStopOnAbort :: Bool
dbgStopOnAbort = Bool
False
    , dbgTrace :: Trace ext
dbgTrace = Trace ext
t
    }

toCompletionEnv ::
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  CompletionEnv cExt
toCompletionEnv :: forall cExt p sym ext (t :: CrucibleType) r.
Context cExt p sym ext t
-> ExecState p sym ext r -> CompletionEnv cExt
toCompletionEnv Context cExt p sym ext t
ctxt ExecState p sym ext r
execState =
  Complete.CompletionEnv
  { envBreakpoints :: Set Breakpoint
Complete.envBreakpoints = Context cExt p sym ext t -> Set Breakpoint
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Set Breakpoint
dbgBreakpoints Context cExt p sym ext t
ctxt
  , envCommandExt :: CommandExt cExt
Complete.envCommandExt = Context cExt p sym ext t -> CommandExt cExt
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> CommandExt cExt
dbgCommandExt Context cExt p sym ext t
ctxt
  , envState :: ExecState p sym ext r
Complete.envState = ExecState p sym ext r
execState
  }

toStyleEnv ::
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  StyleEnv cExt
toStyleEnv :: forall cExt p sym ext (t :: CrucibleType) r.
Context cExt p sym ext t -> ExecState p sym ext r -> StyleEnv cExt
toStyleEnv Context cExt p sym ext t
ctxt ExecState p sym ext r
execState =
  Style.StyleEnv
  { envBreakpoints :: Set Breakpoint
Style.envBreakpoints = Context cExt p sym ext t -> Set Breakpoint
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Set Breakpoint
dbgBreakpoints Context cExt p sym ext t
ctxt
  , envCommandExt :: CommandExt cExt
Style.envCommandExt = Context cExt p sym ext t -> CommandExt cExt
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> CommandExt cExt
dbgCommandExt Context cExt p sym ext t
ctxt
  , envState :: ExecState p sym ext r
Style.envState = ExecState p sym ext r
execState
  }