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

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.Debug.Complete
  ( CompletionEnv(..)
  , CompletionT
  , runCompletionT
  , runCompletion
  , runCompletionM
  , CompletionType(..)
  , Completions(..)
  , complete
  ) where

import Control.Lens qualified as Lens
import Control.Monad qualified as Monad
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Reader (MonadReader, ReaderT)
import Control.Monad.Reader qualified as Reader
import Control.Monad.Trans (MonadTrans)
import Control.Exception qualified as X
import Data.Foldable (toList)
import Data.Function ((&))
import Data.Functor ((<&>))
import Data.Functor.Identity (Identity, runIdentity)
import Data.List qualified as List
import Data.Map.Strict qualified as Map
import Data.Maybe qualified as Maybe
import Data.Parameterized.Some (Some(Some), viewSome)
import Data.Parameterized.SymbolRepr (symbolRepr)
import Data.Set (Set)
import Data.Text qualified as Text
import Data.Text (Text)
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr)
import Lang.Crucible.Debug.Arg.Type qualified as AType
import Lang.Crucible.Debug.Breakpoint qualified as Break
import Lang.Crucible.Debug.Breakpoint (Breakpoint)
import Lang.Crucible.Debug.Command (CommandExt)
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.FunctionHandle qualified as C
import Lang.Crucible.Simulator.ExecutionTree qualified as C
import Prettyprinter qualified as PP
import System.Directory qualified as Dir
import System.FilePath qualified as FilePath
import What4.FunctionName qualified as W4

data CompletionEnv cExt
  = forall p sym ext r.
    CompletionEnv
  { forall cExt. CompletionEnv cExt -> Set Breakpoint
envBreakpoints :: Set Breakpoint
  , forall cExt. CompletionEnv cExt -> CommandExt cExt
envCommandExt :: CommandExt cExt
  , ()
envState :: C.ExecState p sym ext r
  }

newtype CompletionT cExt m a
  = CompletionT { forall cExt (m :: * -> *) a.
CompletionT cExt m a -> ReaderT (CompletionEnv cExt) m a
runCompletionT :: ReaderT (CompletionEnv cExt) m a }
  deriving (Functor (CompletionT cExt m)
Functor (CompletionT cExt m) =>
(forall a. a -> CompletionT cExt m a)
-> (forall a b.
    CompletionT cExt m (a -> b)
    -> CompletionT cExt m a -> CompletionT cExt m b)
-> (forall a b c.
    (a -> b -> c)
    -> CompletionT cExt m a
    -> CompletionT cExt m b
    -> CompletionT cExt m c)
-> (forall a b.
    CompletionT cExt m a
    -> CompletionT cExt m b -> CompletionT cExt m b)
-> (forall a b.
    CompletionT cExt m a
    -> CompletionT cExt m b -> CompletionT cExt m a)
-> Applicative (CompletionT cExt m)
forall a. a -> CompletionT cExt m a
forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m a
forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
forall a b.
CompletionT cExt m (a -> b)
-> CompletionT cExt m a -> CompletionT cExt m b
forall a b c.
(a -> b -> c)
-> CompletionT cExt m a
-> CompletionT cExt m b
-> CompletionT cExt m c
forall cExt (m :: * -> *).
Applicative m =>
Functor (CompletionT cExt m)
forall cExt (m :: * -> *) a.
Applicative m =>
a -> CompletionT cExt m a
forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m a
forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m (a -> b)
-> CompletionT cExt m a -> CompletionT cExt m b
forall cExt (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> CompletionT cExt m a
-> CompletionT cExt m b
-> CompletionT cExt m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall cExt (m :: * -> *) a.
Applicative m =>
a -> CompletionT cExt m a
pure :: forall a. a -> CompletionT cExt m a
$c<*> :: forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m (a -> b)
-> CompletionT cExt m a -> CompletionT cExt m b
<*> :: forall a b.
CompletionT cExt m (a -> b)
-> CompletionT cExt m a -> CompletionT cExt m b
$cliftA2 :: forall cExt (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> CompletionT cExt m a
-> CompletionT cExt m b
-> CompletionT cExt m c
liftA2 :: forall a b c.
(a -> b -> c)
-> CompletionT cExt m a
-> CompletionT cExt m b
-> CompletionT cExt m c
$c*> :: forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
*> :: forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
$c<* :: forall cExt (m :: * -> *) a b.
Applicative m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m a
<* :: forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m a
Applicative, (forall a b.
 (a -> b) -> CompletionT cExt m a -> CompletionT cExt m b)
-> (forall a b. a -> CompletionT cExt m b -> CompletionT cExt m a)
-> Functor (CompletionT cExt m)
forall a b. a -> CompletionT cExt m b -> CompletionT cExt m a
forall a b.
(a -> b) -> CompletionT cExt m a -> CompletionT cExt m b
forall cExt (m :: * -> *) a b.
Functor m =>
a -> CompletionT cExt m b -> CompletionT cExt m a
forall cExt (m :: * -> *) a b.
Functor m =>
(a -> b) -> CompletionT cExt m a -> CompletionT cExt m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall cExt (m :: * -> *) a b.
Functor m =>
(a -> b) -> CompletionT cExt m a -> CompletionT cExt m b
fmap :: forall a b.
(a -> b) -> CompletionT cExt m a -> CompletionT cExt m b
$c<$ :: forall cExt (m :: * -> *) a b.
Functor m =>
a -> CompletionT cExt m b -> CompletionT cExt m a
<$ :: forall a b. a -> CompletionT cExt m b -> CompletionT cExt m a
Functor, Applicative (CompletionT cExt m)
Applicative (CompletionT cExt m) =>
(forall a b.
 CompletionT cExt m a
 -> (a -> CompletionT cExt m b) -> CompletionT cExt m b)
-> (forall a b.
    CompletionT cExt m a
    -> CompletionT cExt m b -> CompletionT cExt m b)
-> (forall a. a -> CompletionT cExt m a)
-> Monad (CompletionT cExt m)
forall a. a -> CompletionT cExt m a
forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
forall a b.
CompletionT cExt m a
-> (a -> CompletionT cExt m b) -> CompletionT cExt m b
forall cExt (m :: * -> *).
Monad m =>
Applicative (CompletionT cExt m)
forall cExt (m :: * -> *) a. Monad m => a -> CompletionT cExt m a
forall cExt (m :: * -> *) a b.
Monad m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
forall cExt (m :: * -> *) a b.
Monad m =>
CompletionT cExt m a
-> (a -> CompletionT cExt m b) -> CompletionT cExt m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall cExt (m :: * -> *) a b.
Monad m =>
CompletionT cExt m a
-> (a -> CompletionT cExt m b) -> CompletionT cExt m b
>>= :: forall a b.
CompletionT cExt m a
-> (a -> CompletionT cExt m b) -> CompletionT cExt m b
$c>> :: forall cExt (m :: * -> *) a b.
Monad m =>
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
>> :: forall a b.
CompletionT cExt m a
-> CompletionT cExt m b -> CompletionT cExt m b
$creturn :: forall cExt (m :: * -> *) a. Monad m => a -> CompletionT cExt m a
return :: forall a. a -> CompletionT cExt m a
Monad, Monad (CompletionT cExt m)
Monad (CompletionT cExt m) =>
(forall a. String -> CompletionT cExt m a)
-> MonadFail (CompletionT cExt m)
forall a. String -> CompletionT cExt m a
forall cExt (m :: * -> *).
MonadFail m =>
Monad (CompletionT cExt m)
forall cExt (m :: * -> *) a.
MonadFail m =>
String -> CompletionT cExt m a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall cExt (m :: * -> *) a.
MonadFail m =>
String -> CompletionT cExt m a
fail :: forall a. String -> CompletionT cExt m a
MonadFail, Monad (CompletionT cExt m)
Monad (CompletionT cExt m) =>
(forall a. IO a -> CompletionT cExt m a)
-> MonadIO (CompletionT cExt m)
forall a. IO a -> CompletionT cExt m a
forall cExt (m :: * -> *). MonadIO m => Monad (CompletionT cExt m)
forall cExt (m :: * -> *) a.
MonadIO m =>
IO a -> CompletionT cExt m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall cExt (m :: * -> *) a.
MonadIO m =>
IO a -> CompletionT cExt m a
liftIO :: forall a. IO a -> CompletionT cExt m a
MonadIO, MonadReader (CompletionEnv cExt), (forall (m :: * -> *). Monad m => Monad (CompletionT cExt m)) =>
(forall (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a)
-> MonadTrans (CompletionT cExt)
forall cExt (m :: * -> *). Monad m => Monad (CompletionT cExt m)
forall cExt (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
forall (m :: * -> *). Monad m => Monad (CompletionT cExt m)
forall (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall cExt (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
lift :: forall (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
MonadTrans)

-- | Run 'CompletionT' over 'Identity'
runCompletion :: CompletionEnv cExt -> CompletionT cExt Identity a -> a
runCompletion :: forall cExt a.
CompletionEnv cExt -> CompletionT cExt Identity a -> a
runCompletion CompletionEnv cExt
env CompletionT cExt Identity a
s = Identity a -> a
forall a. Identity a -> a
runIdentity (ReaderT (CompletionEnv cExt) Identity a
-> CompletionEnv cExt -> Identity a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
Reader.runReaderT (CompletionT cExt Identity a
-> ReaderT (CompletionEnv cExt) Identity a
forall cExt (m :: * -> *) a.
CompletionT cExt m a -> ReaderT (CompletionEnv cExt) m a
runCompletionT CompletionT cExt Identity a
s) CompletionEnv cExt
env)

-- | Run 'CompletionT' over another monad
--
-- This is kind of poorly named, but I can\'t think of a better name...
runCompletionM :: CompletionEnv cExt -> CompletionT cExt m a -> m a
runCompletionM :: forall cExt (m :: * -> *) a.
CompletionEnv cExt -> CompletionT cExt m a -> m a
runCompletionM CompletionEnv cExt
env CompletionT cExt m a
s = ReaderT (CompletionEnv cExt) m a -> CompletionEnv cExt -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
Reader.runReaderT (CompletionT cExt m a -> ReaderT (CompletionEnv cExt) m a
forall cExt (m :: * -> *) a.
CompletionT cExt m a -> ReaderT (CompletionEnv cExt) m a
runCompletionT CompletionT cExt m a
s) CompletionEnv cExt
env

data CompletionType
  = CBreakpoint
  | CCommand
  | CExactly Text
  | CFunction
  | CPath
  deriving (CompletionType -> CompletionType -> Bool
(CompletionType -> CompletionType -> Bool)
-> (CompletionType -> CompletionType -> Bool) -> Eq CompletionType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompletionType -> CompletionType -> Bool
== :: CompletionType -> CompletionType -> Bool
$c/= :: CompletionType -> CompletionType -> Bool
/= :: CompletionType -> CompletionType -> Bool
Eq, Int -> CompletionType -> ShowS
[CompletionType] -> ShowS
CompletionType -> String
(Int -> CompletionType -> ShowS)
-> (CompletionType -> String)
-> ([CompletionType] -> ShowS)
-> Show CompletionType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompletionType -> ShowS
showsPrec :: Int -> CompletionType -> ShowS
$cshow :: CompletionType -> String
show :: CompletionType -> String
$cshowList :: [CompletionType] -> ShowS
showList :: [CompletionType] -> ShowS
Show)

instance PP.Pretty CompletionType where
  pretty :: forall ann. CompletionType -> Doc ann
pretty =
    \case
      CompletionType
CBreakpoint -> Doc ann
"breakpoint"
      CompletionType
CCommand -> Doc ann
"command"
      CExactly Text
t -> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
t
      CompletionType
CFunction -> Doc ann
"function"
      CompletionType
CPath -> Doc ann
"path"

completionType :: ArgTypeRepr t -> Maybe CompletionType
completionType :: forall (t :: ArgType). ArgTypeRepr t -> Maybe CompletionType
completionType =
  \case
    ArgTypeRepr t
AType.TBreakpointRepr -> CompletionType -> Maybe CompletionType
forall a. a -> Maybe a
Just CompletionType
CBreakpoint
    ArgTypeRepr t
AType.TCommandRepr -> CompletionType -> Maybe CompletionType
forall a. a -> Maybe a
Just CompletionType
CCommand
    AType.TExactlyRepr SymbolRepr s
s -> CompletionType -> Maybe CompletionType
forall a. a -> Maybe a
Just (Text -> CompletionType
CExactly (SymbolRepr s -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr s
s))
    ArgTypeRepr t
AType.TFunctionRepr -> CompletionType -> Maybe CompletionType
forall a. a -> Maybe a
Just CompletionType
CFunction
    ArgTypeRepr t
AType.TIntRepr -> Maybe CompletionType
forall a. Maybe a
Nothing
    ArgTypeRepr t
AType.TPathRepr -> CompletionType -> Maybe CompletionType
forall a. a -> Maybe a
Just CompletionType
CPath
    ArgTypeRepr t
AType.TTextRepr -> Maybe CompletionType
forall a. Maybe a
Nothing

commandsWithPrefix ::
  CompletionEnv cExt ->
  -- | Prefix
  String ->
  [String]
commandsWithPrefix :: forall cExt. CompletionEnv cExt -> String -> [String]
commandsWithPrefix CompletionEnv cExt
cEnv String
pfx = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String
pfx String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf`) [String]
allCmdNames
  where
    allCmdNames :: [String]
    allCmdNames :: [String]
allCmdNames =
      let cExts :: CommandExt cExt
cExts = CompletionEnv cExt -> CommandExt cExt
forall cExt. CompletionEnv cExt -> CommandExt cExt
envCommandExt CompletionEnv cExt
cEnv in
      (Command cExt -> String) -> [Command cExt] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> String
Text.unpack (Text -> String)
-> (Command cExt -> Text) -> Command cExt -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.name CommandExt cExt
cExts) (CommandExt cExt -> [Command cExt]
forall cExt. CommandExt cExt -> [Command cExt]
Cmd.allCmds CommandExt cExt
cExts)

completePath :: FilePath -> IO [String]
completePath :: String -> IO [String]
completePath String
path =
  if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null String
path
  then String -> IO [String]
Dir.listDirectory (String -> IO [String]) -> IO String -> IO [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO String
Dir.getCurrentDirectory
  else do
    Bool
isDir <- String -> IO Bool
Dir.doesDirectoryExist String
path
    if Bool
isDir Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> Bool
FilePath.hasTrailingPathSeparator String
path)
      then [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ShowS
FilePath.addTrailingPathSeparator String
path]
      else do
        let dir :: String
dir = ShowS
FilePath.addTrailingPathSeparator (ShowS
FilePath.takeDirectory String
path)
        [String]
contents <- String -> IO [String]
Dir.listDirectory String
dir
        let file :: String
file = ShowS
FilePath.takeFileName String
path
        if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null String
file
        then [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
dir String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
contents)
        else [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
dir String -> ShowS
forall a. [a] -> [a] -> [a]
++) ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String
file String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf`) [String]
contents))

completionsForType ::
  CompletionEnv cExt ->
  -- | Prefix
  String ->
  CompletionType ->
  IO [String]
completionsForType :: forall cExt.
CompletionEnv cExt -> String -> CompletionType -> IO [String]
completionsForType CompletionEnv cExt
cEnv String
pfx =
  \case
    CompletionType
CBreakpoint ->
      [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$
        Set Breakpoint -> [Breakpoint]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (CompletionEnv cExt -> Set Breakpoint
forall cExt. CompletionEnv cExt -> Set Breakpoint
envBreakpoints CompletionEnv cExt
cEnv) [Breakpoint] -> ([Breakpoint] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
&
          (Breakpoint -> Text) -> [Breakpoint] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Breakpoint -> Text
Break.toText [Text] -> ([Text] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
&
          (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> Text
Text.pack String
pfx Text -> Text -> Bool
`Text.isPrefixOf`) [Text] -> ([Text] -> [String]) -> [String]
forall a b. a -> (a -> b) -> b
&
          (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
Text.unpack
    CompletionType
CCommand -> [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CompletionEnv cExt -> String -> [String]
forall cExt. CompletionEnv cExt -> String -> [String]
commandsWithPrefix CompletionEnv cExt
cEnv String
pfx)
    CExactly Text
s ->
      let s' :: String
s' = Text -> String
Text.unpack Text
s in
      [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if String
pfx String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` String
s' then [String
s'] else [])
    CompletionType
CFunction -> do
      CompletionEnv { envState :: ()
envState = ExecState p sym ext r
execState } <- CompletionEnv cExt -> IO (CompletionEnv cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CompletionEnv cExt
cEnv
      let binds :: FunctionBindings p sym ext
binds = ExecState p sym ext r
execState ExecState p sym ext r
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext r)
     (FunctionBindings p sym ext)
-> FunctionBindings p sym ext
forall s a. s -> Getting a s a -> a
Lens.^. (ExecState p sym ext r -> SimContext p sym ext)
-> (SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> ExecState p sym ext r
-> Const (FunctionBindings p sym ext) (ExecState p sym ext r)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
Lens.to ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ((SimContext p sym ext
  -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
 -> ExecState p sym ext r
 -> Const (FunctionBindings p sym ext) (ExecState p sym ext r))
-> ((FunctionBindings p sym ext
     -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
    -> SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext r)
     (FunctionBindings p sym ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext
 -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
-> SimContext p sym ext
-> Const (FunctionBindings p sym ext) (SimContext p sym ext)
forall p sym ext (f :: * -> *).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
C.functionBindings
      let hdls :: [SomeHandle]
hdls = FnHandleMap (FnState p sym ext) -> [SomeHandle]
forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandleMap f -> [SomeHandle]
C.handleMapToHandles (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings FunctionBindings p sym ext
binds)
      [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SomeHandle -> String) -> [SomeHandle] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(C.SomeHandle FnHandle args ret
hdl) -> Text -> String
Text.unpack (FunctionName -> Text
W4.functionName (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
C.handleName FnHandle args ret
hdl))) [SomeHandle]
hdls)
    CompletionType
CPath ->
      forall e a. Exception e => IO a -> IO (Either e a)
X.try @X.IOException (String -> IO [String]
completePath String
pfx) IO (Either IOException [String])
-> (Either IOException [String] -> [String]) -> IO [String]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
        \case
          Left IOException
_ -> []
          Right [String]
cs -> [String]
cs

data Completions
  = Completions
    { Completions -> CompletionType
completionsType :: CompletionType
    , Completions -> [String]
completions :: [String]
    }

-- | Used in the test suite with @. complete@
instance PP.Pretty Completions where
  pretty :: forall ann. Completions -> Doc ann
pretty (Completions CompletionType
ty [String]
cs) = do
    let def :: Doc ann
def =
          if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
cs
          then CompletionType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CompletionType -> Doc ann
PP.pretty CompletionType
ty
          else
            CompletionType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CompletionType -> Doc ann
PP.pretty CompletionType
ty Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
PP.punctuate Doc ann
"," ((String -> Doc ann) -> [String] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty [String]
cs))
    case CompletionType
ty of
      CompletionType
CBreakpoint -> Doc ann
def
      CompletionType
CCommand -> CompletionType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CompletionType -> Doc ann
PP.pretty CompletionType
ty
      CExactly {} ->
        if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
cs
        then CompletionType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CompletionType -> Doc ann
PP.pretty CompletionType
ty Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"(x)"
        else CompletionType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CompletionType -> Doc ann
PP.pretty CompletionType
ty
      CFunction {} -> Doc ann
def
      CompletionType
CPath -> Doc ann
def

complete ::
  CompletionEnv cExt ->
  -- | Whole line
  String ->
  -- | Word being completed
  String ->
  IO [Completions]
complete :: forall cExt.
CompletionEnv cExt -> String -> String -> IO [Completions]
complete CompletionEnv cExt
cEnv String
input String
word =
  case String -> [String]
words String
input of
    [] -> [Completions] -> IO [Completions]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [CompletionType -> [String] -> Completions
Completions CompletionType
CCommand [String]
allCmdNames]
    [String
_] | Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
word) ->
      [Completions] -> IO [Completions]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [CompletionType -> [String] -> Completions
Completions CompletionType
CCommand (CompletionEnv cExt -> String -> [String]
forall cExt. CompletionEnv cExt -> String -> [String]
commandsWithPrefix CompletionEnv cExt
cEnv String
word)]
    (String
c : [String]
args) -> do
      case CommandExt cExt -> Text -> Maybe (Command cExt)
forall cExt. CommandExt cExt -> Text -> Maybe (Command cExt)
Cmd.parse CommandExt cExt
cExts (String -> Text
Text.pack String
c) of
        Just Command cExt
cmd ->
          case CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
forall cExt.
CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
Cmd.regex CommandExt cExt
cExts Command cExt
cmd of
            Some RegexRepr ArgTypeRepr x
rx -> do
              let (Map Text (Seq (Some ArgTypeRepr))
allTypes, Seq (Some ArgTypeRepr)
next) = CommandExt cExt
-> RegexRepr ArgTypeRepr x
-> [Text]
-> (Map Text (Seq (Some ArgTypeRepr)), Seq (Some ArgTypeRepr))
forall (r :: Regex ArgType) cExt.
CommandExt cExt
-> RegexRepr ArgTypeRepr r
-> [Text]
-> (Map Text (Seq (Some ArgTypeRepr)), Seq (Some ArgTypeRepr))
Arg.types CommandExt cExt
cExts RegexRepr ArgTypeRepr x
rx ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
Text.pack [String]
args)
              let types :: Seq (Some ArgTypeRepr)
types =
                    case Text
-> Map Text (Seq (Some ArgTypeRepr))
-> Maybe (Seq (Some ArgTypeRepr))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String -> Text
Text.pack String
word) Map Text (Seq (Some ArgTypeRepr))
allTypes of
                      Maybe (Seq (Some ArgTypeRepr))
Nothing -> Seq (Some ArgTypeRepr)
next
                      Just Seq (Some ArgTypeRepr)
ts -> Seq (Some ArgTypeRepr)
ts
              let cTypes :: [CompletionType]
cTypes = (Some ArgTypeRepr -> Maybe CompletionType)
-> [Some ArgTypeRepr] -> [CompletionType]
forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe ((forall (t :: ArgType). ArgTypeRepr t -> Maybe CompletionType)
-> Some ArgTypeRepr -> Maybe CompletionType
forall {k} (f :: k -> *) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome ArgTypeRepr tp -> Maybe CompletionType
forall (t :: ArgType). ArgTypeRepr t -> Maybe CompletionType
completionType) (Seq (Some ArgTypeRepr) -> [Some ArgTypeRepr]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Some ArgTypeRepr)
types)
              (CompletionType -> IO Completions)
-> [CompletionType] -> IO [Completions]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
Monad.mapM (\CompletionType
t -> CompletionType -> [String] -> Completions
Completions CompletionType
t ([String] -> Completions) -> IO [String] -> IO Completions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompletionEnv cExt -> String -> CompletionType -> IO [String]
forall cExt.
CompletionEnv cExt -> String -> CompletionType -> IO [String]
completionsForType CompletionEnv cExt
cEnv String
word CompletionType
t) [CompletionType]
cTypes
        Maybe (Command cExt)
Nothing -> [Completions] -> IO [Completions]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  where
    cExts :: CommandExt cExt
cExts = CompletionEnv cExt -> CommandExt cExt
forall cExt. CompletionEnv cExt -> CommandExt cExt
envCommandExt CompletionEnv cExt
cEnv

    allCmdNames :: [String]
    allCmdNames :: [String]
allCmdNames = (Command cExt -> String) -> [Command cExt] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> String
Text.unpack (Text -> String)
-> (Command cExt -> Text) -> Command cExt -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.name CommandExt cExt
cExts) (CommandExt cExt -> [Command cExt]
forall cExt. CommandExt cExt -> [Command cExt]
Cmd.allCmds CommandExt cExt
cExts)