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
G. Allais edited this page Aug 21, 2018 · 13 revisions

Conversations between Agda & agda-mode

Agda speaks Emacs Lisp to agda-mode, while agda-mode speaks Haskell to Agda.

From agda-mode to Agda

This is what a typical 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 can be best described with datatype declarations (simplified here, for exact definitions, visit the link to the source)

IOTCM: source 

data = IOTCM
        FilePath
        HighlightingLevel
        HighlightingMethod
        Interaction

HighlightingLevel: source 

data HighlightingLevel
  = None           
  | NonInteractive 
  | Interactive

HighlightingMethod: source 

data HighlightingMethod
  = Direct    -- via stdout
  | Indirect  -- both via files and via stdout

Interaction: source

This is where commands are defined, for examples, see the section below.

data Interaction
  = Cmd_load            FilePath [String]         
  | Cmd_constraints          
  | Cmd_infer_toplevel  Rewrite String
  | Cmd_give            InteractionId range String
  ...

Rewrite: source 

data Rewrite = AsIs         -- identity
             | Instantiated -- no normalization (instantiates solved meta variables)
             | HeadNormal   -- head normal form: computes until the term starts with a constructor
             | Simplified   -- "full" normalization which only unfolds definition if that leads to further reductions
             | Normalised   -- full normalization

ComputeMode: source 

data ComputeMode = DefaultCompute  
             | IgnoreAbstract   
             | UseShowInstance    -- does not exist prior to 2.5.2

Thanks @ruhatch for discovering this.

Range: source 

data Range = Range (Seq Interval)
data Interval = Interval 
  { iStart :: Position
  , iEnd   :: Position
  }
data Position = Pn
  { srcFile :: SrcFile -- some shit
  , posPos  :: Int     -- Position, counting from 1.
  , posLine :: Int     -- Line number, counting from 1.
  , posCol  :: Int     -- Column number, counting from 1.
  }
noRange = Range Seq.empty
Example of usage of Range:

Prior to Agda 2.5.1

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

or

noRange

Following Agda 2.5.1

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

or

noRange

List of examples (of all agda-mode commands)

load

Prior to Agda 2.5.0, supply paths of libs

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

Following Agda 2.5.0, leave it empty

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

compile

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

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 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 52 7 9)]) "some expression")

search

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_search_about_toplevel Simplified "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 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 52 7 9)]) "some expression")

compute normal form (global)

Prior to Agda 2.5.2, use False for DefaultCompute and True for IgnoreAbstract

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

Following Agda 2.5.2, supply a value of ComputeMode

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

compute normal form (goal-specific)

Prior to Agda 2.5.2, use False for DefaultCompute and True for IgnoreAbstract

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

Following Agda 2.5.2, supply a value of ComputeMode

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_compute DefaultCompute 0 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 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 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 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 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 52 7 9)]) "some expression")

refine

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

intro

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

refine or intro

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

auto

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

context

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

helper function (goal-specific: given a name and a telescope of explicit arguments, returns the type of the helper with that name)

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

goal type

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

goal type & context

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

goal type & context infer

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

case

IOTCM "/some/path/to/file.agda" NonInteractive Indirect (Cmd_make_case 0 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 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 (intervalsToRange (Just (mkAbsolute "/some/path/to/file.agda")) [Interval (Pn () 50 7 7) (Pn () 52 7 9)]) "some expression")

show version

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

From Agda to agda-mode

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)))

Here are something 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