Skip to content
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.

Conversations between Agda & agda mode

Jump to bottom
Ting-Yen Lai edited this page Jul 23, 2015 · 13 revisions

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] | noRange
data Interval = Interval Position Position
data Position = Pn
  { srcFile :: some shit
  , posPos  :: Int -- character index, counting from 1.
  , posLine :: Int -- line number, counting from 1.
  , posCol  :: Int -- column number, counting from 1.
  }

examples of most usage:

(Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)])

noRange

List of examples (of almost all commands)

load

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_load "/some/path/to/file.agda" [".", "/some/path/to/lib.agda"])

compile

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_compile MAlonzo "/some/path/to/file.agda" [".", "/some/path/to/lib.agda"])

| Cmd_show_module_contents_toplevel B.Rewrite String | Cmd_search_about_toplevel B.Rewrite String | Cmd_solveAll | Cmd_infer_toplevel B.Rewrite -- Normalise the type? String

show constraints

IOTCM "/some/path/to/file.agda" NonInteractive Indirect Cmd_constraints

show metas

IOTCM "/some/path/to/file.agda" NonInteractive Indirect Cmd_metas

show module contents (global)

IOTCM "/some/path/to/file.agda" None Indirect (Cmd_show_module_contents_toplevel Simplified "some expression")

show module contents (goal-specific)

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_show_module_contents Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

solve all constraints

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

infer (global)

IOTCM "/some/path/to/file.agda" None Indirect (Cmd_infer_toplevel Simplified "some expression")

infer (goal-specific)

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_infer Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

compute normal form (global)

IOTCM "/some/path/to/file.agda" None Indirect (Cmd_compute_toplevel False "some expression")

compute normal form (goal-specific)

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_compute False 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

load highlighting info

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

highlight

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_highlight 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

show implicit arguments

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

toggle implicit arguments

IOTCM "/some/path/to/file.agda" NonInteractive Indirect ToggleImplicitArgs

give

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_give 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

refine

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_refine 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

intro

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_intro False 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

refine or intro

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_refine_or_intro False 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

auto

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_auto 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

context

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_context Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

helper function (huh ?)

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_helper_function Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

goal type

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_goal_type Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

goal type & context

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_goal_type_context Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

goal type & context infer

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_goal_type_context_infer Simplified 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

case

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_make_case 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

why in scope (global)

IOTCM "/some/path/to/file.agda" None Indirect (Cmd_why_in_scope_toplevel "some expression")

why in scope (goal-specific)

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_why_in_scope 0 (Range [Interval (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 50 7 7) (Pn (Just (mkAbsolute "/some/path/to/file.agda")) 52 7 9)]) "some expression")

show version

IOTCM "/some/path/to/file.agda" NonInteractive Indirect Cmd_show_version

From agda

Most of the outputs from Agda look like this:

(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking SomeModule (/path/to/SomeModule.agda).\n" t)
(agda2-highlight-load-and-delete-action "/var/folders/wy/2tlbwjxn2wn9_lqjp8m327280000gn/T/agda2-mode90891")
(agda2-info-action "*Type-checking*" "Finished SomeModule.\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Goals*" "?0 : SomeType\n" nil)
((last . 1) . (agda2-goals-action '(0)))

And there're some stuffs we might be interested in.

  • agda2-status-action: most of them are just empty strings, not so insightful.
  • agda2-info-action: the texts you would see on the panel, it's for human.
  • agda2-give-action: comes with a goal index and some contents Agda gave
  • agda2-goals-action: comes with a list of indices of goals
  • agda2-goto: comes with a filepath and a character index which indicates where you should go to.
  • agda2-make-case-action: comes with a list of strings you should rewrite with.
Clone this wiki locally