cornelis

Dedication

I'll ask to stand up
With a show about a rooster,
Which was old and worn out,
Impotent and weathered.
The chickens complained and whined
Because he did not satisfy them.

-- Cornelis Vreeswijk

Overview

cornelis is agda-mode, but for neovim. It's written in Haskell, which means it's maintainable and significantly less likely to bit-rot like any vimscript/lua implementations.

Features

It supports highlighting, goal listing, type-context, refinement, auto, solving, case splitting, go-to definition, normalization, and helper functions. These are exposed via vim commands. Most commands have an equivalent in agda-mode.

Global commands

Vim command	Description	Equivalent agda-mode keybinding
:CornelisLoad	Load and type-check buffer	C-cC-l
:CornelisGoals	Show all goals	C-cC-?
:CornelisRestart	Kill and restart the agda process	C-cC-xC-r
:CornelisAbort	Abort running command	C-cC-xC-a
:CornelisSolve <RW>	Solve constraints	C-cC-s
:CornelisGoToDefinition	Jump to definition of name at cursor	M-. or middle mouse button
:CornelisPrevGoal	Jump to previous goal	C-cC-b
:CornelisNextGoal	Jump to next goal	C-cC-f
:CornelisQuestionToMeta	Expand ?-holes to {! !}	(none)
:CornelisInc	Like <C-A> but also targets sub- and superscripts	(none)
:CornelisDec	Like <C-X> but also targets sub- and superscripts	(none)
:CornelisCloseInfoWindows	Close (all) info windows cornelis has opened	(none)

Commands in context of a goal

These commands can be used in context of a hole:

Vim command	Description	Equivalent agda-mode keybinding
:CornelisGive	Fill goal with hole contents	C-cC-SPC
:CornelisRefine	Refine goal	C-cC-r
:CornelisElaborate <RW>	Fill goal with normalized hole contents	C-cC-m
:CornelisAuto	Automatic proof search	C-cC-a
:CornelisMakeCase	Case split	C-cC-c
:CornelisTypeContext <RW>	Show goal type and context	C-cC-,
:CornelisTypeInfer <RW>	Show inferred type of hole contents	C-cC-d
:CornelisTypeContextInfer <RW>	Show goal type, context, and inferred type of hole contents	C-cC-.
:CornelisNormalize <CM>	Compute normal of hole contents	C-cC-n
:CornelisWhyInScope	Show why given name is in scope	C-cC-w
:CornelisHelperFunc <RW>	Copy inferred type to register "	C-cC-h

Commands with an <RW> argument take an optional normalization mode argument, one of AsIs, Instantiated, HeadNormal, Simplified or Normalised. When omitted, defaults to Normalised.

Commands with a <CM> argument take an optional compute mode argument:

<CM>	Description	Equivalent agda-mode prefix
DefaultCompute	default, used if <CM> is omitted	no prefix, default
IgnoreAbstract	compute normal form, ignoring abstracts	C-u
UseShowInstance	compute normal form of print using show instance	C-uC-u
HeadCompute	compute weak-head normal form	C-uC-uC-u

If Agda is stuck executing a command (e.g. if normalization takes too long), abort the command with :CornelisAbort.

If you need to restart the plugin (eg if Agda is stuck in a loop), you can restart everything via :CornelisRestart.

Agda Input

There is reasonably good support for agda-input via your <LocalLeader> in insert mode. See agda-input.vim for available bindings.

If you'd like to use a prefix other than your <LocalLeader>, add the following to your .vimrc:

let g:cornelis_agda_prefix = "<Tab>" " Replace with your desired prefix

Interactive Unicode Selection

If you'd like an interactive prompt for choosing unicode characters, additionally install vim-which-key:

Plug 'liuchengxu/vim-which-key'

and map a call to cornelis#prompt_input() in insert mode:

inoremap <localleader> <C-O>:call cornelis#prompt_input()<CR>

Disabling Default Bindings

If you don't want any of the default bindings, add the following to your .vimrc:

let g:cornelis_no_agda_input = 1

Adding Bindings

Custom bindings can be added by calling the cornelis#bind_input function in .vimrc. For example:

call cornelis#bind_input("nat", "ℕ")

will add <LocalLeader>nat as an input remapping for ℕ.

Custom Hooks

If you'd prefer to manage agda-input entirely on your own (perhaps in a snippet system), you can set the following:

function! MyCustomHook(key, character)
  " do something
endfunction

let g:cornelis_bind_input_hook = "MyCustomHook"

You can invoke cornelis#standard_bind_input with the same arguments if you'd like to run your hook in addition to the standard one.

Text Objects

Use the iz/az text objects to operate on text between ⟨ and ⟩. Somewhat surprisingly for i/a text objects, iz targets the spaces between these brackets, and az targets the spaces. Neither textobj targets the brackets themselves.

Also ii/ai will operate on ⦃ and ⦄, but in the way you'd expect text objects to behave.

ih/ah will operate on {! and !}.

Installation

Make sure you have stack on your PATH!

Plug 'kana/vim-textobj-user'
Plug 'neovimhaskell/nvim-hs.vim'
Plug 'isovector/cornelis', { 'do': 'stack build' }

Agda Version

cornelis is tested only against agda-2.6.3. If you run into weird error messages from vim, it's probably because you're running an old version of agda. If possible, try upgrading, if not, file a bug and I'll see if I can help.

In addition, there are some bugs in the most recent version of agda that negatively affect cornelis. For best results, build from head, ensuring you have the following patches:

• agda/agda#5752
• agda/agda#5776

Installation with Nix

You can install both the vim plugin and the cornelis binary using nix flakes! You can access the binary as cornelis.packages.<my-system>.cornelis and the vim plugin as cornelis.packages.<my-system>.cornelis-vim. Below is a sample configuration to help you understand where everything plugs in.

Nix details

# flake.nix
{
  description = "my-config";

  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
    home-manager = {
      url = "github:nix-community/home-manager";
      inputs.nixpkgs.follows = "nixpkgs";
    };
    cornelis.url = "github:isovector/cornelis";
    cornelis.inputs.nixpkgs.follows = "nixpkgs";
  };
  outputs =
    { home-manager
    , nixpkgs
    , cornelis
    , ...
    }: {
    nixosConfigurations = {
      bellerophon = nixpkgs.lib.nixosSystem {
        system = "x86_64-linux";
        modules = [
          home-manager.nixosModules.home-manager
          {
            nixpkgs.overlays = [cornelis.overlays.cornelis];
            home-manager.useGlobalPkgs = true;
            home-manager.useUserPackages = true;
            home-manager.users.my-home = import ./my-home.nix;
          }
        ];
      };
    };
  };
}

# my-home.nix
{pkgs, ...}:
{
  home.packages = [ pkgs.agda ];
  programs.neovim = {
    enable = true;
    extraConfig = builtins.readFile ./init.vim;
    plugins = [
      {
        # plugin packages in required Vim plugin dependencies
        plugin = pkgs.vimPlugins.cornelis;
        config = "let g:cornelis_use_global_binary = 1";
      }
    ];
    extraPackages = [ pkgs.cornelis ];
  };
}

Make sure you enable the global binary option in your vim config. Since /nix/store is immutable cornelis will fail when nvim-hs tries to run stack, which it will do if the global binary option isn't enabled.

Use global binary instead of stack

Vimscript:

let g:cornelis_use_global_binary = 1

Lua:

vim.g.cornelis_use_global_binary = 1

Example Configuration

Once you have cornelis installed, you'll probably want to add some keybindings for it! This is enough to get you started:

au BufRead,BufNewFile *.agda call AgdaFiletype()
au QuitPre *.agda :CornelisCloseInfoWindows
function! AgdaFiletype()
    nnoremap <buffer> <leader>l :CornelisLoad<CR>
    nnoremap <buffer> <leader>r :CornelisRefine<CR>
    nnoremap <buffer> <leader>d :CornelisMakeCase<CR>
    nnoremap <buffer> <leader>, :CornelisTypeContext<CR>
    nnoremap <buffer> <leader>. :CornelisTypeContextInfer<CR>
    nnoremap <buffer> <leader>n :CornelisSolve<CR>
    nnoremap <buffer> <leader>a :CornelisAuto<CR>
    nnoremap <buffer> gd        :CornelisGoToDefinition<CR>
    nnoremap <buffer> [/        :CornelisPrevGoal<CR>
    nnoremap <buffer> ]/        :CornelisNextGoal<CR>
    nnoremap <buffer> <C-A>     :CornelisInc<CR>
    nnoremap <buffer> <C-X>     :CornelisDec<CR>
endfunction

Feeling spicy? Automatically run CornelisLoad every time you save the file.

au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"

If you'd like to automatically load files when you open them too, try this:

function! CornelisLoadWrapper()
  if exists(":CornelisLoad") ==# 2
    CornelisLoad
  endif
endfunction

au BufReadPre *.agda call CornelisLoadWrapper()
au BufReadPre *.lagda* call CornelisLoadWrapper()

This won't work on the first Agda file you open due to a bug, but it will successfully load subsequent files.

Configuring Cornelis' Behavior

The max height and width of the info window can be set via:

let g:cornelis_max_size = 30

and

let g:cornelis_max_width = 40

If you'd prefer your info window to appear somewhere else, you can set g:cornelis_split_location (previously g:cornelis_split_direction), e.g.

let g:cornelis_split_location = 'vertical'

The following configuration options are available:

• horizontal: The default, opens in a horizontal split respecting splitbelow.
• vertical: Opens in a vertical split respecting splitright.
• top: Opens at the top of the window.
• bottom: Opens at the bottom of the window.
• left: Opens at the left of the window.
• right: Opens at the right of the window.

Aligning Reasoning Justification

If you're interested in automatically aligning your reasoning justifications, also install the following plugin:

Plug 'junegunn/vim-easy-align'

and add the following configuration for it:

vmap <leader><space> <Plug>(EasyAlign)

let g:easy_align_delimiters = {
\ 'r': { 'pattern': '[≤≡≈∎]', 'left_margin': 2, 'right_margin': 0 },
\ }

You can now align justifications by visually selecting the proof, and then typing <leader><space>r.

Customizing Syntax Highlighting

Syntax highlighting is controlled by syntax groups named Cornelis*, defined in syntax/agda.vim. These groups are linked to default highlighting groups (:h group-name), and can be customized by overriding them in user configuration.

" Highlight holes with a yellow undercurl/underline:
highlight CornelisHole ctermfg=yellow ctermbg=NONE cterm=undercurl

" Highlight "generalizables" (declarations in `variable` blocks) like constants:
highlight link CornelisGeneralizable Constant

Contributing

I'm a noob at Agda, and I don't know what I don't know. If this plugin doesn't have some necessary feature for you to get work done, please file a bug, including both what's missing, and how you use it in your workflow. I'd love to learn how to use Agda better! I can move quickly on feature requests.

If you'd like to get involved, feel free to tackle an issue on the tracker and send a PR. I'd love to have you on board!

Architecture

Cornelis spins up a new BufferStuff for each Agda buffer it encounters. BufferStuff contains a handle to a unique agda instance, which can be used to send commands. It also tracks things like the information window buffer, in-scope goals, and whatever the last DisplayInfo response from agda was.

For each BufferStuff, we also spin up a new thread, blocking on responses from agda. These responses all get redirected to a global worker thread, which is responsible for dispatching on each command. Commands are typesafe, parsed from JSON, and associated with the buffer they came from.