VIM Editing

Syntax Highlighting in VIM

The Agda compiler has an option to generate VIM syntax files. To generate a VIM syntax file for a specific Agda file named file.agda, simply use "agda --vim file.agda". This will generate a file named .file.vim in the current directory. It will also recursively generate VIM syntax files for all the corresponding Agda source files for each imported module and place them in the directory where the source files reside.

For generic Agda syntax highlighting, copy the VIM syntax file to ~/.vim/syntax/agda.vim . An example of such a file is given later in this document. To use the syntax file, add the following line to ~/.vim/filetype.vim :

au BufNewFile,BufRead *.agda setf agda

The above command causes VIM to automatically load the file ~/.vim/syntax/agda.vim each time a file with the file extension .agda is opened for editing.

To get the local VIM syntax highlighting file to load after the generic syntax highlighting file, you can either manually execute :source .%.vim in command mode. For automatic loading of syntax files, you can create a file named ~/.vim/after/syntax/agda.vim and add the following:

function! ReloadSyntax()
  syntax clear
  runtime syntax/agda.vim
  let f = expand('%:h') . "/." . expand('%:t') . ".vim"
  if filereadable(f)
    exec "source " . escape(f, '*')
  endif
endfunction

call ReloadSyntax()

map ,rs :call ReloadSyntax()<CR>

This will cause the local syntax file to be loaded after generic Agda syntax file. Furthermore, you can execute ,rs in command to reload the local syntax file.

Work has begun on a generic Agda syntax highlighting file, however, it is still incomplete:

" File: ~/.vim/syntax/agda.vim

if version < 600
  syn clear
elseif exists("b:current_syntax")
  finish
endif

" To tokenize, the best pattern I've found so far is this:
"   (^|\s|[.(){};])@<=token($|\s|[.(){};])@=
" The patterns @<= and @= look behind and ahead, respectively, without matching.

" `agda --vim` extends these groups:
"   agdaConstructor
"   agdaFunction
"   agdaInfixConstructor
"   agdaInfixFunction

syn match   agdaKeywords     "\v(^|\s|[.(){};])@<=(abstract|data|hiding|import|as|infix|infixl|infixr|module|mutual|open|primitive|private|public|record|renaming|rewrite|using|where|with|field|constructor|infix|infixl|infixr|syntax)($|\s|[.(){};])@="
syn match   agdaDubious      "\v(^|\s|[.(){};])@<=(postulate|codata)($|\s|[.(){};])@="
syn match   agdaOperator     "\v(^|\s|[.(){};])@<=(let|in|forall|&#955;|&#8594;|-\>|:|&#8704;|\=|\||\\)($|\s|[.(){};])@="
syn match   agdaFunction     "\v(^|\s|[.(){};])@<=(Set[0-9&#8320;-&#8329;]*)($|\s|[.(){};])@="
syn match   agdaNumber       "\v(^|\s|[.(){};])@<=[0-9]+($|\s|[.(){};])@="
syn match   agdaCharCode     contained "\\\([0-9]\+\|o[0-7]\+\|x[0-9a-fA-F]\+\|[\"\\'&\\abfnrtv]\|^[A-Z^_\[\\\]]\)"
syn match   agdaCharCode     contained "\v\\(NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|SP|DEL)"
syn match   agdaCharCodeErr  contained "\\&\|'''\+"
syn region  agdaString       start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=agdaCharCode
syn match   agdaHole         "\v(^|\s|[.(){};])@<=(\?)($|\s|[.(){};])@="
syn region  agdaX            matchgroup=agdaHole start="{!" end="!}" contains=ALL
syn match   agdaLineComment  "\v(^|\s|[.(){};])@<=--.*$" contains=@agdaInComment
syn region  agdaBlockComment start="{-"  end="-}" contains=agdaBlockComment,@agdaInComment
syn region  agdaPragma       start="{-#" end="#-}"
syn cluster agdaInComment    contains=agdaTODO,agdaFIXME,agdaXXX
syn keyword agdaTODO         contained TODO
syn keyword agdaFIXME        contained FIXME
syn keyword agdaXXX          contained XXX

hi def link agdaNumber           Number
hi def link agdaString           String
hi def link agdaConstructor      Constant
hi def link agdaCharCode         SpecialChar
hi def link agdaCharCodeErr      Error
hi def link agdaHole             WarningMsg
hi def link agdaDubious          WarningMsg
hi def link agdaKeywords         Structure
hi def link agdaFunction         Macro
hi def link agdaOperator         Operator
hi def link agdaInfixConstructor Operator
hi def link agdaInfixFunction    Operator
hi def link agdaLineComment      Comment
hi def link agdaBlockComment     Comment
hi def link agdaPragma           Comment
hi def      agdaTODO             cterm=bold,underline ctermfg=2 " green
hi def      agdaFIXME            cterm=bold,underline ctermfg=3 " yellow
hi def      agdaXXX              cterm=bold,underline ctermfg=1 " red

Typing Unicode Characters

Agda code commonly uses unicode characters for many mathematical and logical notations like:

∀ → λ Σ ∃ ≡

The best way is to use XCompose.

Another easy way to enter unicode in vim is to create mappings in insert mode:

imap <buffer> \forall
imap <buffer> \to
imap <buffer> \lambda λ
imap <buffer> \Sigma Σ
imap <buffer> \exists
imap <buffer> \equiv

Then to get a , just type \forall in insert mode. Many more example mappings can be found in agda-utf8.vim and unicode-keys.vim. Add mappings to ~/after/syntax/agda.vim (or ~/.vimrc, if you want them available globally). More information can be found on the vim wiki: Entering Special Characters.

Holes in vim

There is some preliminary, unofficial support for using holes a la the emacs mode at agda-vim as well as a compilation of a selection of the scripts referenced above.

Emulating vi inside emacs

It's worth mentioning that using agda-mode in emacs is more than syntax highlighting and utf-8 insertion, holes and all features that come with them makes a big difference.

A good option is to use Evil.

  ;;; Maps C-c C-<key> to \<key in evil-normal-state
  (eval-after-load 'agda2
    '(progn
       (evil-define-key 'normal agda2-mode-map
         "\\a" 'agda2-auto
         "\\k" 'agda2-previous-goal
         "\\j" 'agda2-next-goal
         "\\c" 'agda2-make-case
         "\\d" 'agda2-infer-type-maybe-toplevel
         "\\e" 'agda2-show-context
         "\\l" 'agda2-load
         "\\n" 'agda2-compute-normalised-maybe-toplevel
         "\\o" 'agda2-module-contents-maybe-toplevel
         "\\r" 'agda2-refine
         "\\s" 'agda2-solveAll
         "\\t" 'agda2-goal-type
         "\\ " 'agda2-give
         "\\," 'agda2-goal-and-context
         "\\." 'agda2-goal-and-context-and-inferred
         "\\=" 'agda2-show-constraints
         "\\?" 'agda2-show-goals
         "\\xc" 'agda2-compile
         "\\xd" 'agda2-remove-annotations
         "\\xh" 'agda2-display-implicit-arguments
         "\\xl" 'agda2-load
         "\\xq" 'agda2-quit
         "\\xr" 'agda2-restart)))

Alternatively, add the following to your .emacs to emulate vi keybindings inside emacs:

; Viper mode emulates basic vi keys, part of emacs.
(setq viper-mode t)
(require 'viper)

; Vimpulse emulates some more advanced vim keys, needs to be downloaded
; and put into emacs load-path.
; http://www.emacswiki.org/emacs/vimpulse.el
; (require 'vimpulse)

; Rect-mark improves visual mode (I think), also needs to be downloaded
; and put into emacs load-path.
; http://www.emacswiki.org/cgi-bin/wiki/download/rect-mark.el
; (require 'rect-mark)

; If you choose level 5 (I think you should) when viper asks what
; skill level you are, you will get access to all of emacs key
; bindings on top of vi's -- this can be annoying, when you by accident
; use some of emacs' bindings. The following disables some emacs bindings
; you probably won't miss anyway:

(global-unset-key (kbd "M-k"))
(global-unset-key (kbd "M-j"))
(global-unset-key (kbd "M-h"))
(global-unset-key (kbd "M-l"))
(global-unset-key (kbd "M-o"))
(global-unset-key (kbd "C-x C-l"))
(global-unset-key (kbd "C-x C-d"))
(global-unset-key (kbd "M-:"))
(global-unset-key (kbd "M-u"))

; If you use emacs from a terminal you want to add the following bindings,
; for some reason they work in GUI mode but not in terminal mode.
(global-set-key (kbd "C-c ,") 'agda2-goal-and-context)
(global-set-key (kbd "C-c .") 'agda2-goal-and-context-and-inferred)
(global-set-key (kbd "C-c C-@") 'agda2-give)

For unicode input in evil, you need to set a hook that when you go into insert mode, Agda input is turned on. Add this to your .emacs,

(add-hook 'evil-insert-state-entry-hook (lambda () (set-input-method "Agda")))
(add-hook 'evil-insert-state-exit-hook (lambda () (set-input-method nil)))