{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DataKinds #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use camelCase" #-} module Cornelis.Types.Agda where import Cornelis.Offsets import Data.Aeson (ToJSON, FromJSON) import Data.Foldable (toList) import Data.Sequence import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as T import GHC.Generics import GHC.Show (showSpace) data Rewrite = AsIs | Instantiated | HeadNormal | Simplified | Normalised deriving (Show, Read, Eq, Ord, Enum, Bounded) data ComputeMode = DefaultCompute | HeadCompute | IgnoreAbstract | UseShowInstance deriving (Show, Read, Eq, Ord, Enum, Bounded) data UseForce = WithForce -- ^ Ignore additional checks, like termination/positivity... | WithoutForce -- ^ Don't ignore any checks. deriving (Eq, Read, Show) newtype InteractionId = InteractionId { interactionId :: Int } deriving newtype ( Eq , Ord , Show , Read , Num , Integral , Real , Enum , ToJSON , FromJSON ) -- | IOTCM commands. type Command = Command' IOTCM type IntervalWithoutFile = AgdaInterval 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 data Range' a = NoRange | Range !a (Seq IntervalWithoutFile) deriving (Eq, Ord, Functor, Foldable, Traversable, Generic) instance Show a => Show (Range' a) where showsPrec _ NoRange = showString "noRange" showsPrec a_a1hOk (Cornelis.Types.Agda.Range b1_a1hOl b2_a1hOm) = showParen (a_a1hOk >= 11) ((.) (showString "intervalsToRange ") ((.) (showsPrec 11 b1_a1hOl) ((.) showSpace (showsPrec 11 $ toList b2_a1hOm)))) type SrcFile = Maybe AbsolutePath newtype AbsolutePath = AbsolutePath { textPath :: String } deriving (Eq, Ord) instance Show AbsolutePath where showsPrec n (AbsolutePath p) = showParen (n >= 11) $ showString "mkAbsolute " . showsPrec 11 p type Range = Range' SrcFile type IOTCM = IOTCM' Range data IOTCM' range = IOTCM Text -- -^ 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) data Interaction' range -- | @cmd_load m argv@ loads the module in file @m@, using -- @argv@ as the command-line options. = Cmd_load Text [String] | Cmd_constraints -- | Show unsolved metas. If there are no unsolved metas but unsolved constraints -- show those instead. | Cmd_metas Rewrite -- | Shows all the top-level names in the given module, along with -- their types. Uses the top-level scope. | Cmd_show_module_contents_toplevel Rewrite String -- | Shows all the top-level names in scope which mention all the given -- identifiers in their type. | Cmd_search_about_toplevel Rewrite String -- | Solve (all goals / the goal at point) whose values are determined by -- the constraints. | Cmd_solveAll Rewrite | Cmd_solveOne 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 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 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 ------------------------------------------------------------------------ -- Irrelevant arguments -- | Tells Agda whether or not to show irrelevant arguments. | ShowIrrelevantArgs Bool -- Show them? -- | Toggle display of irrelevant arguments. | ToggleIrrelevantArgs ------------------------------------------------------------------------ -- | 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 Rewrite InteractionId range String | Cmd_helper_function Rewrite InteractionId range String | Cmd_infer Rewrite InteractionId range String | Cmd_goal_type 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 Rewrite InteractionId range String -- | Displays the current goal and context. | Cmd_goal_type_context Rewrite InteractionId range String -- | Displays the current goal and context /and/ infers the type of an -- expression. | Cmd_goal_type_context_infer Rewrite InteractionId range String -- | Grabs the current goal's type and checks the expression in the hole -- against it. | Cmd_goal_type_context_check 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 Rewrite InteractionId range String | Cmd_make_case InteractionId range String | Cmd_compute 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. | Cmd_exit -- ^ Exit the program. deriving (Show, Read, Functor, Foldable, Traversable) type Interaction = Interaction' Range data HighlightingLevel = None | NonInteractive | Interactive -- ^ This includes both non-interactive highlighting and -- interactive highlighting of the expression that is currently -- being type-checked. deriving (Eq, Ord, Show, Read, Generic) data HighlightingMethod = Direct -- ^ Via stdout. | Indirect -- ^ Both via files and via stdout. deriving (Eq, Show, Read, Generic) data Remove = Remove | Keep deriving (Show, Read) noRange :: Range' a noRange = NoRange -- | Converts a file name and an interval to a range. intervalToRange :: a -> IntervalWithoutFile -> Range' a intervalToRange f i = Range f (Seq.singleton i) -- | Turns a file name plus a list of intervals into a range. -- -- Precondition: 'consecutiveAndSeparated'. intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a intervalsToRange _ [] = NoRange intervalsToRange f is = Range f (Seq.fromList is) mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range mkAbsPathRnage = intervalToRange . Just . AbsolutePath . T.unpack