Arg.hs

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

For the sake of correctness, consistency, and concision, it is desirable to
declaratively specify the types of arguments expected by 'Cmd.Command's. These
specifications are used to:

* Parse said arguments (see 'match')
* Generate usage hints for @usage@ (see 'usage')
* Perform syntax highlighting (see "Lang.Crucible.Debug.Style")
* Provide tab-completions (see 'complete')

Perhaps the simplest workable argument specification would be a list of basic
types (e.g., integer, string). However, the purpose of the command language
is to be convenient for interactive use. In particular, users should not have
to remember the names of several variants of a command that do fundamentally
similar tasks. To provide sufficient flexibilty to unite such variants under
a single command, the specification should allow (in increasing order of
sophistication):

* sequencing (i.e., arity higher than 1),
* disjunction (at the very least, in a limited form), and
* quantification (optionality, repetition, and in particular, variable arity).

To justify the necessity of such features, consider the following examples of
each, taken from the bread-and-butter commands of the @gdb@ command language:

* sequencing: @break@ takes several (optional) arguments
* optionality: @step@ takes an optional integer argument
* quantification: @delete@ takes a variable number of breakpoint numbers

The basic list-of-types specification clearly lacks such features. Luckily,
there is a well-understood specification language that allows all of the above,
namely, regular expressions. Thus, the debugger\'s commands are specified
using the facilities provided by "Lang.Crucible.Debug.Regex". The tokens of
the regular expression are basic types (see 'ArgTypeRepr'). Operations like
'derivative' are used internally to provide the high-level functionality
described at the beginning of this documentation.

Commands that are not well-suited to this kind of argument validation can simply
accept @TEXT*@ and perform their own parsing (or not) at the cost of lacking
helpful documentation and completion. This is exactly the specification of the
comment (@#@) command, for example.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Debug.Arg
  ( Arg(..)
  -- * Parsers
  , ArgParseError(..)
  , ArgParser(..)
  , convert
  -- * Operations
  , match
  , derivative
  , types
  , usage
  ) where

import Data.Coerce (coerce)
import Data.Foldable qualified as Foldable
import Data.Kind (Type)
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Parameterized.Some (Some(Some))
import Data.Parameterized.SymbolRepr (SymbolRepr, symbolRepr)
import Data.Parameterized.TraversableFC (fmapFC)
import Data.Sequence (Seq)
import Data.Text qualified as Text
import Lang.Crucible.Debug.Arg.Type (type ArgType(..), ArgTypeRepr(..))
import Lang.Crucible.Debug.Breakpoint (Breakpoint(BreakFunction))
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Regex qualified as Rgx
import Prelude hiding (Int)
import Prelude qualified as Prelude
import Prettyprinter qualified as PP
import Text.Read (readMaybe)
import What4.FunctionName qualified as W4

type Arg :: Type -> ArgType -> Type
data Arg cExt i where
  ABreakpoint :: Breakpoint -> Arg cExt 'TBreakpoint
  ACommand :: Cmd.Command cExt -> Arg cExt 'TCommand
  AExactly :: SymbolRepr s -> Arg cExt ('TExactly s)
  AFunction :: W4.FunctionName -> Arg cExt 'TFunction
  AInt :: Prelude.Int -> Arg cExt 'TInt
  APath :: Text.Text -> Arg cExt 'TPath
  AText :: Text.Text -> Arg cExt 'TText

data ArgParseError
  = NotACommand Text.Text
  | NotAnInt Text.Text
  | NotExactly Text.Text Text.Text
  deriving Show

instance PP.Pretty ArgParseError where
  pretty =
    \case
      NotACommand t -> PP.squotes (PP.pretty t) PP.<+> "is not a command"
      NotAnInt t -> PP.squotes (PP.pretty t) PP.<+> "is not an integer"
      NotExactly e t -> PP.squotes (PP.pretty t) PP.<+> "is not" PP.<+> PP.squotes (PP.pretty e)

newtype ArgParser cExt t
  = ArgParser { _runArgParser :: Rgx.TokenParser Text.Text ArgParseError (Arg cExt) t }

argParser :: (Text.Text -> Either ArgParseError (Arg cExt t)) -> ArgParser cExt t
argParser = ArgParser . Rgx.TokenParser

-- | Helper, not exported
maybeToEither :: e -> Maybe a -> Either e a
maybeToEither e =
  \case
    Nothing -> Left e
    Just a -> Right a

breakpoint :: ArgParser cExt 'TBreakpoint
breakpoint =
  argParser (Right . ABreakpoint . BreakFunction . W4.functionNameFromText)

function :: ArgParser cExt 'TFunction
function =
  argParser (Right . AFunction .  W4.functionNameFromText)

command :: Cmd.CommandExt cExt -> ArgParser cExt 'TCommand
command cExt = argParser (\t -> ACommand <$> maybeToEither (NotACommand t) (Cmd.parse cExt t))

exactly :: SymbolRepr s -> ArgParser cExt ('TExactly s)
exactly s =
  argParser $ \t ->
    if t == symbolRepr s
    then Right (AExactly s)
    else Left (NotExactly (symbolRepr s) t)

int :: ArgParser cExt 'TInt
int = argParser (\t -> AInt <$> maybeToEither (NotAnInt t) (readMaybe (Text.unpack t)))

path :: ArgParser cExt 'TPath
path = argParser (Right . APath)

text :: ArgParser cExt 'TText
text = argParser (Right . AText)

parser :: Cmd.CommandExt cExt -> ArgTypeRepr t -> ArgParser cExt t
parser cExt =
  \case
    TBreakpointRepr -> breakpoint
    TCommandRepr -> command cExt
    TExactlyRepr s -> exactly s
    TFunctionRepr -> function
    TIntRepr -> int
    TPathRepr -> path
    TTextRepr -> text

convert ::
  Cmd.CommandExt cExt ->
  Rgx.RegexRepr ArgTypeRepr r ->
  Rgx.RegexRepr (ArgParser cExt) r
convert cExt = fmapFC (parser cExt)

match ::
  forall r cExt.
  Rgx.RegexRepr (ArgParser cExt) r ->
  [Text.Text] ->
  Either (Rgx.MatchError Text.Text ArgParseError) (Rgx.Match (Arg cExt) r)
match r toks =
  case Rgx.match @_ @_ @(Arg cExt) (coerce r) toks of
    Left e -> Left e
    Right (m, []) -> Right m
    Right (_, as) -> Left (Rgx.NotEmpty as)

derivative ::
  forall cExt r.
  Cmd.CommandExt cExt ->
  Text.Text ->
  Rgx.RegexRepr ArgTypeRepr r ->
  Rgx.DerivativeResult ArgTypeRepr (Arg cExt)
derivative cExt =
  Rgx.derivative
    (coerce @_ @(Rgx.TokenParser _ ArgParseError (Arg cExt) _) . parser cExt)

-- | Get the potential types that the regex assigns each argument, plus what it
-- would assign to the next one.
types ::
  forall r cExt.
  Cmd.CommandExt cExt ->
  Rgx.RegexRepr ArgTypeRepr r ->
  [Text.Text] ->
  (Map Text.Text (Seq (Some ArgTypeRepr)), Seq (Some ArgTypeRepr))
types cExt r =
  \case
    [] -> (Map.empty, Rgx.nextLits r)
    (t : ts) ->
      case derivative cExt t r of
        Rgx.DerivativeResult (Some r') _ ->
          let (m, final) = types cExt r' ts in
          (Map.insertWith (<>) t (Rgx.nextLits r) m, final)

usage :: Rgx.RegexRepr ArgTypeRepr r -> [PP.Doc ann]
usage r =
  Foldable.toList $
    fmap (\(Some r') -> Rgx.prettySugar " " PP.pretty r') (Rgx.liftOrs (Rgx.sugar r))