Agda.Interaction.Command

Documentation

data AgdaCommand

Supported sub-commands for Agda.

Constructors

Reload

Help

Constraints

Context

Give

Refine

Meta

Load

Eval

TypeOf

TypeIn

WakeUp

Scope

Instances

Eq AgdaCommand

Defined in Agda.Interaction.Command

Methods

(==) :: AgdaCommand -> AgdaCommand -> Bool

(/=) :: AgdaCommand -> AgdaCommand -> Bool

Show AgdaCommand

Defined in Agda.Interaction.Command

Methods

showsPrec :: Int -> AgdaCommand -> ShowS

show :: AgdaCommand -> String

showList :: [AgdaCommand] -> ShowS

Generic AgdaCommand

Defined in Agda.Interaction.Command

Associated Types

type Rep AgdaCommand :: Type -> Type

Methods

from :: AgdaCommand -> Rep AgdaCommand x

to :: Rep AgdaCommand x -> AgdaCommand

type Rep AgdaCommand

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

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

matchSupported :: ByteString -> Maybe AgdaCommand

Check user input to identify AgdaCommand.

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

Choose an action based on either AgdaCommand or raw input.

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

Store raw user input in the file given by TCEnv.