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

Agda.Interaction.Command

Synopsis

Documentation

data AgdaCommand Source #

Supported sub-commands for Agda.

Instances

Instances details
Eq AgdaCommand Source # 
Instance details

Defined in Agda.Interaction.Command

Show AgdaCommand Source # 
Instance details

Defined in Agda.Interaction.Command

Generic AgdaCommand Source # 
Instance details

Defined in Agda.Interaction.Command

Associated Types

type Rep AgdaCommand :: Type -> Type #

type Rep AgdaCommand Source # 
Instance details

Defined in Agda.Interaction.Command

type Rep AgdaCommand = D1 ('MetaData "AgdaCommand" "Agda.Interaction.Command" "proof-assistant-bot-0.2.0-inplace" 'False) (((C1 ('MetaCons "Reload" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Help" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constraints" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Context" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Give" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Refine" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Meta" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Load" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Eval" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeOf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeIn" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WakeUp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Scope" 'PrefixI 'False) (U1 :: Type -> Type)))))

supportedCommands :: HashMap ByteString AgdaCommand Source #

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

matchSupported :: ByteString -> Maybe AgdaCommand Source #

Check user input to identify AgdaCommand.

chooseCommand :: AgdaState -> Either () AgdaCommand -> ByteString -> IO (TCM ByteString) Source #

Choose an action based on either AgdaCommand or raw input.

storeRequestContent :: AbsolutePath -> ByteString -> IO () Source #

Store raw user input in the file given by TCEnv.