Conversations between Agda & agda mode

Conversations between Agda & agda-mode

To agda

This is what a message to agda looks like:

IOTCM "/some/path/to/file.agda" NonInteractive Indirect ( Cmd_load_highlighting_info "/some/path/to/file.agda" )

It's basically just a value of some datatype in Haskell, which could be best described with datatype declarations (for exact definitions, visit the source as attached)

IOTCM: source

data = IOTCM
        FilePath
        HighlightingLevel
        HighlightingMethod
        Interaction

HighlightingLevel: source

data HighlightingLevel
  = None            -- ?
  | NonInteractive  -- ?
  | Interactive     -- ?

HighlightingMethod: source

data HighlightingMethod
  = Direct    -- via stdout
  | Indirect  -- via file system

Interaction: source

data Interaction
  = Cmd_load            FilePath [FilePath]
  | Cmd_constraints
  | Cmd_infer_toplevel  Rewrite Expression
  | Cmd_give            GoalIndex Range Expression
  ...

 type GoalIndex = Int
 type Expression = String

Rewrite: source

data Rewrite = AsIs         -- ?
             | Instantiated -- no normalization
             | HeadNormal   -- ?
             | Simplified   -- something in between
             | Normalised   -- full normalization

Range: source

data Range = Range [Interval]
data Interval = Interval Position Position
data Position = Pn
  { srcFile :: FilePath
  , posPos  :: Int -- character index, counting from 1.
  , posLine :: Int -- line number, counting from 1.
  , posCol  :: Int -- column number, counting from 1.
  }