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. This default may be specified in vimrc as g:cornelis_rewrite_mode.

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:

viml 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:

viml Plug 'liuchengxu/vim-which-key'

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

viml 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:

viml 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:

viml 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:

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

let g:cornelisbindinput_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!

For vim-plug:

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

for lazy.nvim:

lua { 'isovector/cornelis', name = 'cornelis', ft = 'agda', build = 'stack install', dependencies = {'neovimhaskell/nvim-hs.vim', 'kana/vim-textobj-user'}, version = '*', }

Agda Version

If you are having issues, try using a tag which matches your agda major version (e.g. for Agda v2.7.0.1 use cornelis v2.7.*). If there is no matching version that is working for a new version of agda, please create an issue.

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

```nix # 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:

viml let g:cornelis_use_global_binary = 1

Lua:

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:

viml 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.

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

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

```viml 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:

viml let g:cornelis_max_size = 30

and

viml 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.

viml 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.

Set default rewrite mode to use in commands which take an optional normalization mode argument

viml let g:cornelis_rewrite_mode = 'HeadNormal'

The following configuration options are available: - AsIs - Instantiated - HeadNormal - Simplified - Normalised

Aligning Reasoning Justification

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

viml Plug 'junegunn/vim-easy-align'

and add the following configuration for it:

```viml vmap (EasyAlign)

let g:easyaligndelimiters = { \ 'r': { 'pattern': '[≤≡≈∎]', 'leftmargin': 2, 'rightmargin': 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.

```viml " 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.