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

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Debug.Command.Base
  ( BaseCommand(..)
  , name
  , abbrev
  , detail
  , help
  , regex
  -- * Regular expressions
  , rBacktrace
  , rBlock
  , rBreak
  , rCall
  , rCfg
  , rClear
  , rComment
  , rDelete
  , rDone
  , rFinish
  , rFrame
  , rHelp
  , rLoad
  , rLocation
  , rObligation
  , rPathCondition
  , rProve
  , rQuit
  , rRegister
  , rRun
  , SecretRegex
  , rSecret
  , rSource
  , rStep
  , rTrace
  , rUsage
  ) where

import Data.Parameterized.Classes (knownRepr)
import Data.Parameterized.Some (Some(Some))
import Data.Text (Text)
import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr)
import Lang.Crucible.Debug.Arg.Type qualified as AType
import Lang.Crucible.Debug.Regex qualified as Rgx
import Prettyprinter qualified as PP

data BaseCommand
  = Backtrace
  | Block
  | Break
  | Call
  | Cfg
  | Clear
  | Comment
  | Delete
  | Done
  | Finish
  | Frame
  | Help
  | Load
  | Location
  | Obligation
  | PathCondition
  | Prove
  | Quit
  | Register
  | Run
  | Secret
  | Source
  | Step
  | Trace
  | Usage
  deriving (BaseCommand
BaseCommand -> BaseCommand -> Bounded BaseCommand
forall a. a -> a -> Bounded a
$cminBound :: BaseCommand
minBound :: BaseCommand
$cmaxBound :: BaseCommand
maxBound :: BaseCommand
Bounded, Int -> BaseCommand
BaseCommand -> Int
BaseCommand -> [BaseCommand]
BaseCommand -> BaseCommand
BaseCommand -> BaseCommand -> [BaseCommand]
BaseCommand -> BaseCommand -> BaseCommand -> [BaseCommand]
(BaseCommand -> BaseCommand)
-> (BaseCommand -> BaseCommand)
-> (Int -> BaseCommand)
-> (BaseCommand -> Int)
-> (BaseCommand -> [BaseCommand])
-> (BaseCommand -> BaseCommand -> [BaseCommand])
-> (BaseCommand -> BaseCommand -> [BaseCommand])
-> (BaseCommand -> BaseCommand -> BaseCommand -> [BaseCommand])
-> Enum BaseCommand
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BaseCommand -> BaseCommand
succ :: BaseCommand -> BaseCommand
$cpred :: BaseCommand -> BaseCommand
pred :: BaseCommand -> BaseCommand
$ctoEnum :: Int -> BaseCommand
toEnum :: Int -> BaseCommand
$cfromEnum :: BaseCommand -> Int
fromEnum :: BaseCommand -> Int
$cenumFrom :: BaseCommand -> [BaseCommand]
enumFrom :: BaseCommand -> [BaseCommand]
$cenumFromThen :: BaseCommand -> BaseCommand -> [BaseCommand]
enumFromThen :: BaseCommand -> BaseCommand -> [BaseCommand]
$cenumFromTo :: BaseCommand -> BaseCommand -> [BaseCommand]
enumFromTo :: BaseCommand -> BaseCommand -> [BaseCommand]
$cenumFromThenTo :: BaseCommand -> BaseCommand -> BaseCommand -> [BaseCommand]
enumFromThenTo :: BaseCommand -> BaseCommand -> BaseCommand -> [BaseCommand]
Enum, Int -> BaseCommand -> ShowS
[BaseCommand] -> ShowS
BaseCommand -> [Char]
(Int -> BaseCommand -> ShowS)
-> (BaseCommand -> [Char])
-> ([BaseCommand] -> ShowS)
-> Show BaseCommand
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BaseCommand -> ShowS
showsPrec :: Int -> BaseCommand -> ShowS
$cshow :: BaseCommand -> [Char]
show :: BaseCommand -> [Char]
$cshowList :: [BaseCommand] -> ShowS
showList :: [BaseCommand] -> ShowS
Show)

instance PP.Pretty BaseCommand where
  pretty :: forall ann. BaseCommand -> Doc ann
pretty = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Text -> Doc ann)
-> (BaseCommand -> Text) -> BaseCommand -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseCommand -> Text
name

name :: BaseCommand -> Text
name :: BaseCommand -> Text
name =
  \case
    BaseCommand
Backtrace -> Text
"backtrace"
    BaseCommand
Block -> Text
"block"
    BaseCommand
Break -> Text
"break"
    BaseCommand
Call -> Text
"call"
    BaseCommand
Cfg -> Text
"cfg"
    BaseCommand
Clear -> Text
"clear"
    BaseCommand
Comment -> Text
"#"
    BaseCommand
Delete -> Text
"delete"
    BaseCommand
Done -> Text
"done"
    BaseCommand
Finish -> Text
"finish"
    BaseCommand
Frame -> Text
"frame"
    BaseCommand
Help -> Text
"help"
    BaseCommand
Load -> Text
"load"
    BaseCommand
Location -> Text
"location"
    BaseCommand
Obligation -> Text
"obligation"
    BaseCommand
PathCondition -> Text
"path-condition"
    BaseCommand
Prove -> Text
"prove"
    BaseCommand
Quit -> Text
"quit"
    BaseCommand
Register -> Text
"register"
    BaseCommand
Run -> Text
"run"
    BaseCommand
Secret -> Text
"secret"
    BaseCommand
Step -> Text
"step"
    BaseCommand
Source -> Text
"source"
    BaseCommand
Trace -> Text
"trace"
    BaseCommand
Usage -> Text
"usage"

abbrev :: BaseCommand -> Text
abbrev :: BaseCommand -> Text
abbrev =
  \case
    BaseCommand
Backtrace -> Text
"bt"
    BaseCommand
Block -> Text
"blk"
    BaseCommand
Break -> Text
"b"
    BaseCommand
Call -> Text
"cl"
    BaseCommand
Cfg -> Text
"cg"
    BaseCommand
Clear -> Text
"cr"
    BaseCommand
Comment -> Text
"#"
    BaseCommand
Delete -> Text
"d"
    BaseCommand
Done -> Text
"done"
    BaseCommand
Finish -> Text
"fh"
    BaseCommand
Frame -> Text
"fr"
    BaseCommand
Help -> Text
"h"
    BaseCommand
Load -> Text
"l"
    BaseCommand
Location -> Text
"loc"
    BaseCommand
Obligation -> Text
"o"
    BaseCommand
PathCondition -> Text
"pcond"
    BaseCommand
Prove -> Text
"p"
    BaseCommand
Quit -> Text
"q"
    BaseCommand
Register -> Text
"reg"
    BaseCommand
Run -> Text
"r"
    BaseCommand
Secret -> Text
"."
    BaseCommand
Step -> Text
"s"
    BaseCommand
Source -> Text
"src"
    BaseCommand
Trace -> Text
"trace"
    BaseCommand
Usage -> Text
"u"

-- | See 'Lang.Crucible.Debug.Command.extDetail'
detail :: BaseCommand -> Maybe Text
detail :: BaseCommand -> Maybe Text
detail =
  \case
    BaseCommand
Backtrace -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Block -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Break -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Call -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Cfg -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Clear -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Comment -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Delete -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Done -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Finish -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Frame -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Help -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Load -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Location -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Obligation -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
PathCondition -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Prove -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Quit -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Register -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"\
      \When given no arguments, prints all values in scope. \
      \Otherwise, prints the values with the given numbers, one per line.\
      \\n\n\

      \The value numbering scheme is based on the structure of Crucible CFGs. \
      \A Crucible CFG (function) is made up of *basic blocks*. \
      \Each basic block takes a list of arguments. \
      \The first block in the function is the *entry* block; \
      \the entry block takes the same arguments as the function. \
      \Each block contains a number of *statements*, which may define values. \
      \The value defined by a statement is in scope for the rest of the block.\
      \\n\n\

      \Values are then numbered as follows: \
      \The first argument to the current block is numbered 0. \
      \Increasing numbers refer to later arguments. \
      \After arguments, higher numbers refer to values defined by statements.\
      \"
    BaseCommand
Run -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Secret -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Step -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Source -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Trace -> Maybe Text
forall a. Maybe a
Nothing
    BaseCommand
Usage -> Maybe Text
forall a. Maybe a
Nothing

-- | See 'Lang.Crucible.Debug.Command.extHelp'
help :: BaseCommand -> Text
help :: BaseCommand -> Text
help =
  \case
    BaseCommand
Backtrace -> Text
"Print the backtrace (AKA stack trace)"
    BaseCommand
Block -> Text
"Print the statements in the current block"
    BaseCommand
Break -> Text
"Set a breakpoint at the entry to a function"
    BaseCommand
Call -> Text
"Call a function (must take no arguments and return the unit type)"
    BaseCommand
Cfg -> Text
"Print the CFG of a function (the current function if none is provided)"
    BaseCommand
Clear -> Text
"Drop the current proof obligations"
    BaseCommand
Comment -> Text
"Ignore all arguments and do nothing"
    BaseCommand
Delete -> Text
"Remove a breakpoint"
    BaseCommand
Done -> Text
"Like `quit`, but only applies when symbolic execution has finished"
    BaseCommand
Finish -> Text
"Execute to the end of the current function"
    BaseCommand
Frame -> Text
"Print information about the active stack frame"
    BaseCommand
Help -> Text
"Display help text"
    BaseCommand
Load -> Text
"Load a Crucible S-expression program from a file"
    BaseCommand
Location -> Text
"Print the current program location"
    BaseCommand
Obligation -> Text
"Print the current proof obligations"
    BaseCommand
PathCondition -> Text
"Print the current path condition"
    BaseCommand
Prove -> Text
"Prove the current goals"
    BaseCommand
Quit -> Text
"Exit the debugger"
    BaseCommand
Register -> Text
"Print registers (including block/function arguments)"
    BaseCommand
Run -> Text
"Continue to the next breakpoint or the end of execution"
    BaseCommand
Secret -> Text
"Maintenance commands, used for testing"
    BaseCommand
Step -> Text
"Continue N steps of execution (default: 1)"
    BaseCommand
Source -> Text
"Execute a file containing debugger commands"
    BaseCommand
Trace -> Text
"Print the N most recently executed basic blocks (default: 2)"
    BaseCommand
Usage -> Text
"Display command usage hint"

regex :: BaseCommand -> Some (Rgx.RegexRepr ArgTypeRepr)
regex :: BaseCommand -> Some (RegexRepr ArgTypeRepr)
regex =
  \case
    BaseCommand
Backtrace -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rBacktrace
    BaseCommand
Block -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rBlock
    BaseCommand
Break -> RegexRepr ArgTypeRepr Function -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Function
rBreak
    BaseCommand
Call -> RegexRepr ArgTypeRepr Function -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Function
rCall
    BaseCommand
Cfg -> RegexRepr ArgTypeRepr (Empty :| Function)
-> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Empty :| Function)
rCfg
    BaseCommand
Clear -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rClear
    BaseCommand
Comment -> RegexRepr ArgTypeRepr (Star Text) -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Star Text)
rComment
    BaseCommand
Delete -> RegexRepr ArgTypeRepr Breakpoint -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Breakpoint
rDelete
    BaseCommand
Done -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rDone
    BaseCommand
Finish -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rFinish
    BaseCommand
Frame -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rFrame
    BaseCommand
Help -> RegexRepr ArgTypeRepr (Empty :| Command)
-> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Empty :| Command)
rHelp
    BaseCommand
Load -> RegexRepr ArgTypeRepr Path -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Path
rLoad
    BaseCommand
Location -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rLocation
    BaseCommand
Obligation -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rObligation
    BaseCommand
PathCondition -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rPathCondition
    BaseCommand
Prove -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rProve
    BaseCommand
Quit -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rQuit
    BaseCommand
Register -> RegexRepr ArgTypeRepr (Star Int) -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Star Int)
rRegister
    BaseCommand
Run -> RegexRepr ArgTypeRepr Empty -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Empty
rRun
    BaseCommand
Secret -> RegexRepr ArgTypeRepr SecretRegex -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr SecretRegex
rSecret
    BaseCommand
Step -> RegexRepr ArgTypeRepr (Empty :| Int)
-> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Empty :| Int)
rStep
    BaseCommand
Source -> RegexRepr ArgTypeRepr Path -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Path
rSource
    BaseCommand
Trace -> RegexRepr ArgTypeRepr (Empty :| Int)
-> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr (Empty :| Int)
rTrace
    BaseCommand
Usage -> RegexRepr ArgTypeRepr Command -> Some (RegexRepr ArgTypeRepr)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some RegexRepr ArgTypeRepr Command
rUsage

rBacktrace :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rBacktrace :: RegexRepr ArgTypeRepr Empty
rBacktrace = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rBlock :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rBlock :: RegexRepr ArgTypeRepr Empty
rBlock = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rBreak :: Rgx.RegexRepr ArgTypeRepr AType.Function
rBreak :: RegexRepr ArgTypeRepr Function
rBreak = RegexRepr ArgTypeRepr Function
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rCall :: Rgx.RegexRepr ArgTypeRepr AType.Function
rCall :: RegexRepr ArgTypeRepr Function
rCall = RegexRepr ArgTypeRepr Function
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rCfg :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Function)
rCfg :: RegexRepr ArgTypeRepr (Empty :| Function)
rCfg = RegexRepr ArgTypeRepr (Empty :| Function)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rClear :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rClear :: RegexRepr ArgTypeRepr Empty
rClear = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rComment :: Rgx.RegexRepr ArgTypeRepr (Rgx.Star AType.Text)
rComment :: RegexRepr ArgTypeRepr (Star Text)
rComment = RegexRepr ArgTypeRepr (Star Text)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rDelete :: Rgx.RegexRepr ArgTypeRepr AType.Breakpoint
rDelete :: RegexRepr ArgTypeRepr Breakpoint
rDelete = RegexRepr ArgTypeRepr Breakpoint
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rDone :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rDone :: RegexRepr ArgTypeRepr Empty
rDone = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rFinish :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rFinish :: RegexRepr ArgTypeRepr Empty
rFinish = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rFrame :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rFrame :: RegexRepr ArgTypeRepr Empty
rFrame = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rHelp :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Command)
rHelp :: RegexRepr ArgTypeRepr (Empty :| Command)
rHelp = RegexRepr ArgTypeRepr (Empty :| Command)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rLoad :: Rgx.RegexRepr ArgTypeRepr AType.Path
rLoad :: RegexRepr ArgTypeRepr Path
rLoad = RegexRepr ArgTypeRepr Path
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rLocation :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rLocation :: RegexRepr ArgTypeRepr Empty
rLocation = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rObligation :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rObligation :: RegexRepr ArgTypeRepr Empty
rObligation = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rPathCondition :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rPathCondition :: RegexRepr ArgTypeRepr Empty
rPathCondition = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rProve :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rProve :: RegexRepr ArgTypeRepr Empty
rProve = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rQuit :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rQuit :: RegexRepr ArgTypeRepr Empty
rQuit = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rRegister :: Rgx.RegexRepr ArgTypeRepr (Rgx.Star AType.Int)
rRegister :: RegexRepr ArgTypeRepr (Star Int)
rRegister = RegexRepr ArgTypeRepr (Star Int)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rRun :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
rRun :: RegexRepr ArgTypeRepr Empty
rRun = RegexRepr ArgTypeRepr Empty
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

type CompleteRegex
  = Rgx.Then (AType.Exactly "complete") (Rgx.Then AType.Command (Rgx.Star AType.Text))

type StyleRegex
  = Rgx.Then (AType.Exactly "style") (Rgx.Then AType.Command (Rgx.Star AType.Text))

type SecretRegex
  = CompleteRegex Rgx.:| StyleRegex

rSecret :: Rgx.RegexRepr ArgTypeRepr SecretRegex
rSecret :: RegexRepr ArgTypeRepr SecretRegex
rSecret = RegexRepr ArgTypeRepr SecretRegex
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rSource :: Rgx.RegexRepr ArgTypeRepr AType.Path
rSource :: RegexRepr ArgTypeRepr Path
rSource = RegexRepr ArgTypeRepr Path
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rStep :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int)
rStep :: RegexRepr ArgTypeRepr (Empty :| Int)
rStep = RegexRepr ArgTypeRepr (Empty :| Int)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rTrace :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int)
rTrace :: RegexRepr ArgTypeRepr (Empty :| Int)
rTrace = RegexRepr ArgTypeRepr (Empty :| Int)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

rUsage :: Rgx.RegexRepr ArgTypeRepr AType.Command
rUsage :: RegexRepr ArgTypeRepr Command
rUsage = RegexRepr ArgTypeRepr Command
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr