proof-assistant-bot-0.2.0: Telegram bot for proof assistants
Safe HaskellNone
LanguageHaskell2010

Idris.Interaction.Command

Synopsis

Documentation

data IdrisCommand Source #

Supported sub-commands for Idris 2.

Constructors

Load 
TypeOf 
Help 

Instances

Instances details
Eq IdrisCommand Source # 
Instance details

Defined in Idris.Interaction.Command

Show IdrisCommand Source # 
Instance details

Defined in Idris.Interaction.Command

Generic IdrisCommand Source # 
Instance details

Defined in Idris.Interaction.Command

Associated Types

type Rep IdrisCommand :: Type -> Type #

type Rep IdrisCommand Source # 
Instance details

Defined in Idris.Interaction.Command

type Rep IdrisCommand = D1 ('MetaData "IdrisCommand" "Idris.Interaction.Command" "proof-assistant-bot-0.2.0-inplace" 'False) (C1 ('MetaCons "Load" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TypeOf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Help" 'PrefixI 'False) (U1 :: Type -> Type)))

supportedCommands :: HashMap ByteString IdrisCommand Source #

Map of supported Idris 2 sub-commands. We use it instead of parser.

matchSupported :: ByteString -> Maybe IdrisCommand Source #

Check user input to identify IdrisCommand.

textResponse :: String -> IO (ExitCode, String, String) Source #

Helper to wrap given text as stdout.

withResource :: ExternalInterpreterSettings -> InterpreterRequest -> (FilePath -> IO (ExitCode, String, String)) -> IO (IO (ExitCode, String, String)) Source #

Wrapper around temp directory that will try to identify whether associated file exists. And if file exists given action will be performed.

runProcess :: ExternalInterpreterSettings -> String -> FilePath -> IO (ExitCode, String, String) Source #

Wrapper around CLI execution.

validateCmd :: ByteString -> ByteString Source #

We are trying to filter out some potentially dangerous operations such as :x.