{-# OPTIONS_GHC -fno-cse #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Agda.Interaction.Base where import Control.Concurrent.STM.TChan import Control.Concurrent.STM.TVar import Control.Monad.Identity import Control.Monad.State import qualified Data.List as List import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (listToMaybe) import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (HighlightingLevel, HighlightingMethod, TCM) import Agda.Syntax.Common (InteractionId (..)) import Agda.Syntax.Position import Agda.Syntax.Scope.Base (ScopeInfo) import {-# SOURCE #-} Agda.Interaction.BasicOps (UseForce) import {-# SOURCE #-} qualified Agda.Interaction.BasicOps as B import Agda.Interaction.Options (CommandLineOptions, defaultOptions) import Agda.Utils.Except (ExceptT, MonadError (throwError), runExceptT) import Agda.Utils.FileName (AbsolutePath, mkAbsolute) import Agda.Utils.Time (ClockTime) ------------------------------------------------------------------------ -- The CommandM monad -- | Auxiliary state of an interactive computation. data CommandState = CommandState { theInteractionPoints :: [InteractionId] -- ^ The interaction points of the buffer, in the order in which -- they appear in the buffer. The interaction points are -- recorded in 'theTCState', but when new interaction points are -- added by give or refine Agda does not ensure that the ranges -- of later interaction points are updated. , theCurrentFile :: Maybe (AbsolutePath, ClockTime) -- ^ The file which the state applies to. Only stored if the -- module was successfully type checked (potentially with -- warnings). The 'ClockTime' is the modification time stamp of -- the file when it was last loaded. , optionsOnReload :: CommandLineOptions -- ^ Reset the options on each reload to these. , oldInteractionScopes :: !OldInteractionScopes -- ^ We remember (the scope of) old interaction points to make it -- possible to parse and compute highlighting information for the -- expression that it got replaced by. , commandQueue :: !CommandQueue -- ^ The command queue. -- -- This queue should only be manipulated by -- 'initialiseCommandQueue' and 'maybeAbort'. } type OldInteractionScopes = Map InteractionId ScopeInfo -- | Initial auxiliary interaction state initCommandState :: CommandQueue -> CommandState initCommandState commandQueue = CommandState { theInteractionPoints = [] , theCurrentFile = Nothing , optionsOnReload = defaultOptions , oldInteractionScopes = Map.empty , commandQueue = commandQueue } -- | Monad for computing answers to interactive commands. -- -- 'CommandM' is 'TCM' extended with state 'CommandState'. type CommandM = StateT CommandState TCM ------------------------------------------------------------------------ -- Command queues -- | A generalised command type. data Command' a = Command !a -- ^ A command. | Done -- ^ Stop processing commands. | Error String -- ^ An error message for a command that could not be parsed. deriving Show -- | IOTCM commands. type Command = Command' IOTCM -- | Command queues. data CommandQueue = CommandQueue { commands :: !(TChan (Integer, Command)) -- ^ Commands that should be processed, in the order in which they -- should be processed. Each command is associated with a number, -- and the numbers are strictly increasing. Abort commands are not -- put on this queue. , abort :: !(TVar (Maybe Integer)) -- ^ When this variable is set to @Just n@ an attempt is made to -- abort all commands with a command number that is at most @n@. } ---------------------------------------------------------------------------- -- | An interactive computation. type Interaction = Interaction' Range data Interaction' range -- | @cmd_load m argv@ loads the module in file @m@, using -- @argv@ as the command-line options. = Cmd_load FilePath [String] -- | @cmd_compile b m argv@ compiles the module in file @m@ using -- the backend @b@, using @argv@ as the command-line options. | Cmd_compile CompilerBackend FilePath [String] | Cmd_constraints -- | Show unsolved metas. If there are no unsolved metas but unsolved constraints -- show those instead. | Cmd_metas -- | Shows all the top-level names in the given module, along with -- their types. Uses the top-level scope. | Cmd_show_module_contents_toplevel B.Rewrite String -- | Shows all the top-level names in scope which mention all the given -- identifiers in their type. | Cmd_search_about_toplevel B.Rewrite String -- | Solve (all goals / the goal at point) whose values are determined by -- the constraints. | Cmd_solveAll B.Rewrite | Cmd_solveOne B.Rewrite InteractionId range String -- | Solve (all goals / the goal at point) by using Auto. | Cmd_autoOne InteractionId range String | Cmd_autoAll -- | Parse the given expression (as if it were defined at the -- top-level of the current module) and infer its type. | Cmd_infer_toplevel B.Rewrite -- Normalise the type? String -- | Parse and type check the given expression (as if it were defined -- at the top-level of the current module) and normalise it. | Cmd_compute_toplevel B.ComputeMode String ------------------------------------------------------------------------ -- Syntax highlighting -- | @cmd_load_highlighting_info source@ loads syntax highlighting -- information for the module in @source@, and asks Emacs to apply -- highlighting info from this file. -- -- If the module does not exist, or its module name is malformed or -- cannot be determined, or the module has not already been visited, -- or the cached info is out of date, then no highlighting information -- is printed. -- -- This command is used to load syntax highlighting information when a -- new file is opened, and it would probably be annoying if jumping to -- the definition of an identifier reset the proof state, so this -- command tries not to do that. One result of this is that the -- command uses the current include directories, whatever they happen -- to be. | Cmd_load_highlighting_info FilePath -- | Tells Agda to compute token-based highlighting information -- for the file. -- -- This command works even if the file's module name does not -- match its location in the file system, or if the file is not -- scope-correct. Furthermore no file names are put in the -- generated output. Thus it is fine to put source code into a -- temporary file before calling this command. However, the file -- extension should be correct. -- -- If the second argument is 'Remove', then the (presumably -- temporary) file is removed after it has been read. | Cmd_tokenHighlighting FilePath Remove -- | Tells Agda to compute highlighting information for the expression just -- spliced into an interaction point. | Cmd_highlight InteractionId range String ------------------------------------------------------------------------ -- Implicit arguments -- | Tells Agda whether or not to show implicit arguments. | ShowImplicitArgs Bool -- Show them? -- | Toggle display of implicit arguments. | ToggleImplicitArgs ------------------------------------------------------------------------ -- | Goal commands -- -- If the range is 'noRange', then the string comes from the -- minibuffer rather than the goal. | Cmd_give UseForce InteractionId range String | Cmd_refine InteractionId range String | Cmd_intro Bool InteractionId range String | Cmd_refine_or_intro Bool InteractionId range String | Cmd_context B.Rewrite InteractionId range String | Cmd_helper_function B.Rewrite InteractionId range String | Cmd_infer B.Rewrite InteractionId range String | Cmd_goal_type B.Rewrite InteractionId range String -- | Grabs the current goal's type and checks the expression in the hole -- against it. Returns the elaborated term. | Cmd_elaborate_give B.Rewrite InteractionId range String -- | Displays the current goal and context. | Cmd_goal_type_context B.Rewrite InteractionId range String -- | Displays the current goal and context /and/ infers the type of an -- expression. | Cmd_goal_type_context_infer B.Rewrite InteractionId range String -- | Grabs the current goal's type and checks the expression in the hole -- against it. | Cmd_goal_type_context_check B.Rewrite InteractionId range String -- | Shows all the top-level names in the given module, along with -- their types. Uses the scope of the given goal. | Cmd_show_module_contents B.Rewrite InteractionId range String | Cmd_make_case InteractionId range String | Cmd_compute B.ComputeMode InteractionId range String | Cmd_why_in_scope InteractionId range String | Cmd_why_in_scope_toplevel String -- | Displays version of the running Agda | Cmd_show_version | Cmd_abort -- ^ Abort the current computation. -- -- Does nothing if no computation is in progress. deriving (Show, Read, Functor, Foldable, Traversable) type IOTCM = IOTCM' Range data IOTCM' range = IOTCM FilePath -- -^ The current file. If this file does not match -- 'theCurrentFile, and the 'Interaction' is not -- \"independent\", then an error is raised. HighlightingLevel HighlightingMethod (Interaction' range) -- -^ What to do deriving (Show, Read, Functor, Foldable, Traversable) -- | Used to indicate whether something should be removed or not. data Remove = Remove | Keep deriving (Show, Read) --------------------------------------------------------- -- Read instances -- | The 'Parse' monad. -- 'StateT' state holds the remaining input. type Parse a = ExceptT String (StateT String Identity) a -- | Converter from the type of 'reads' to 'Parse' -- The first paramter is part of the error message -- in case the parse fails. readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a readsToParse s f = do st <- lift get case f st of Nothing -> throwError s Just (a, st) -> do lift $ put st return a parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)] parseToReadsPrec p i s = case runIdentity . flip runStateT s . runExceptT $ parens' p of (Right a, s) -> [(a,s)] _ -> [] -- | Demand an exact string. exact :: String -> Parse () exact s = readsToParse (show s) $ fmap (\x -> ((),x)) . List.stripPrefix s . dropWhile (==' ') readParse :: Read a => Parse a readParse = readsToParse "read failed" $ listToMaybe . reads parens' :: Parse a -> Parse a parens' p = do exact "(" x <- p exact ")" return x `mplus` p instance Read InteractionId where readsPrec = parseToReadsPrec $ fmap InteractionId readParse -- | Note that the grammar implemented by this instance does not -- necessarily match the current representation of ranges. instance Read a => Read (Range' a) where readsPrec = parseToReadsPrec $ (exact "intervalsToRange" >> liftM2 intervalsToRange readParse readParse) `mplus` (exact "noRange" >> return noRange) instance Read a => Read (Interval' a) where readsPrec = parseToReadsPrec $ do exact "Interval" liftM2 Interval readParse readParse instance Read AbsolutePath where readsPrec = parseToReadsPrec $ do exact "mkAbsolute" fmap mkAbsolute readParse instance Read a => Read (Position' a) where readsPrec = parseToReadsPrec $ do exact "Pn" liftM4 Pn readParse readParse readParse readParse --------------------------------------------------------- -- | Available backends. data CompilerBackend = LaTeX | QuickLaTeX | OtherBackend String deriving (Eq) instance Show CompilerBackend where show LaTeX = "LaTeX" show QuickLaTeX = "QuickLaTeX" show (OtherBackend s) = s instance Read CompilerBackend where readsPrec _ s = do (t, s) <- lex s let b = case t of "LaTeX" -> LaTeX "QuickLaTeX" -> QuickLaTeX _ -> OtherBackend t return (b, s)