idris2-nvim

Easy setup and extra features for the native LSP client and the Idris2 LSP server.

Prerequisites

• neovim 0.5+
• nvim-lspconfig
• idris2
• idris2-lsp
• nui.nvim (only for extra UI features)

Installation

Using packer (suggested):

use {'ShinKage/idris2-nvim', requires = {'neovim/nvim-lspconfig', 'MunifTanjim/nui.nvim'}}

Using vim-plug:

Plug 'neovim/nvim-lspconfig'
Plug 'MunifTanjim/nui.nvim'
Plug 'ShinKage/idris2-nvim'

Configuration

Setup

Put this in your init.lua or any lua file that is sourced. For most people, the defaults are fine, but for advanced configuration, see below and the plugin docs.

require('idris2').setup({})

NOTE: This is the only line of code necessary for setup, do not also add lines for nvim-lspconfig because the server setup is already handled by the plugin.

Configuration

The options shown below are the defaults. You only need to pass the keys to the setup function that you want to be changed, because the defaults are applied for keys that are not provided.

local opts = {
  client = {
    hover = {
      use_split = false, -- Persistent split instead of popups for hover
      split_size = '30%', -- Size of persistent split, if used
      auto_resize_split = false, -- Should resize split to use minimum space
      split_position = 'bottom', -- bottom, top, left or right
      with_history = false, -- Show history of hovers instead of only last
      use_as_popup = false, -- Close the split on cursor movement
    },
  },
  server = {}, -- Options passed to lspconfig idris2 configuration
  autostart_semantic = true, -- Should start and refresh semantic highlight automatically
  code_action_post_hook = function(action) end, -- Function to execute after a code action is performed:
  use_default_semantic_hl_groups = true, -- Set default highlight groups for semantic tokens
  default_regexp_syntax = true, -- Enable default highlight groups for traditional syntax based highlighting
}
require('idris2').setup(opts)

You can specify a setup function in your configuration at server.on_attach in order specify any vim key bindings or options you want to only be set when connected to the Idris LSP.

local function custom_on_attach(client)
  -- do things like register key bindings
end

require('idris2').setup({server = {on_attach = custom_on_attach}})

Code Action Hook

If you want to perform some action after the LSP completes a Code Action, you can register a hook (a function to be called when any code action is completed). For example, you may want to have the buffer written after the code action which would then trigger the LSP to re-apply semantic highlighting.

local function save_hook(action)
  vim.cmd('silent write')
end

require('idris2').setup({code_action_post_hook = save_hook})

Your function will be called with the chosen code action as its only parameter. This action parameter has a title and optionally an edit. The details of these fields are defined by the Language Server Protocol, but you can use this plugin's introspect_filter() function to quickly determine what code action was taken (see Code Action Filters for the possible return values).

local filters = require('idris2.code_action').filters
local introspect = require('idris2.code_action').introspect_filter
local function save_hook(action)
  if introspect(action) == filters.MAKE_CASE
    or introspect(action) == filters.MAKE_WITH then
      return
  end
  vim.cmd('silent write')
end

Semantic Highlighting

The server uses the regular syntax highlight groups as defaults for semantic highlight groups, if the option use_default_semantic_hl_groups is set to true. Some examples of custom configuration are:

vim.cmd [[highlight link LspSemantic_type Include]] -- Use the same highlight as the Include group
vim.cmd [[highlight LspSemantic_variable guifg=Gray]] -- Use gray as highlight colour

Group name	Description
LspSemantic_variable	Bound variables
LspSemantic_enumMember	Data constructors
LspSemantic_function	Function names
LspSemantic_type	Type constructors
LspSemantic_keyword	Keywords
LspSemantic_namespace	Explicit namespaces
LspSemantic_postulate	Postulates (believe_me, assert_total, ...)
LspSemantic_module	Imported modules

API

Each module provides lua functions that can be mapped to any key you like. More comprehensive documentation on the API is available in the vim docs of the plugin.

vim.cmd [[nnoremap <Leader>cs <Cmd>lua require('idris2.code_action').case_split()<CR>]]

idris2 module

Function	Description
show_implicits	Show implicits in hovers
hide_implicits	Hide implicits in hovers
show_machine_names	Show machine names in hovers
hide_machine_names	Hide machine names in hovers
full_namespace	Show full namespaces in hovers
hide_namespace	Hide namespaces in hovers

idris2.semantic module

Function	Description
request	Requests semantic groups
clear	Clear semantic groups
start	Starts to automatically request semantic groups on save
stop	Stop automatic requests of semantic groups on save

idris2.metavars module

Function	Description
request_all	Open a popup with all the metavars and jump on selection
type_check	Open a popup with the type of the metavar under the cursor, and the types of all related vars
goto_next	Jumps to the next metavar in the buffer
goto_prev	Jumps to the previous metavar in the buffer

idris2.browse module

Function	Description
browse	Asks the user for a namespace and returns the list of names visible in that namespace

idris2.repl module

Function	Description
evaluate	Prompts for an expression that the LSP should evaluate in the context of the current file. Value can be passed also directly or via visual selection, instead of prompting, and in the latter case can be substituted directly

idris2.hover module

Function	Description
open_split	Show hovers in a persistent split window, can show full history
close_split	Show hovers in the default popup

idris2.code_action module

Function	Description
case_split	Case splits a name on the LHS, applies with no confirmation
make_case	Replaces the metavar with a case block, applies with no confirmation
make_with	Replaces the metavar with a with block, applies with no confirmation
make_lemma	Replaces the metavar with a top-level lemma, applies with no confirmation
add_clause	Add a clause for a declaration, applies with no confirmation
expr_search	Tries to fill a metavar, produces multiple results
generate_def	Tries to build a complete definition for a declaration, produces multiple results
refine_hole	Tries to partially fill a metavar with a name
expr_search_hints	Same as refine_hole but asks the user for comma-separated names to give as hints
intro	Tries to fill a metavar, with valid constructors, produces multiple results

Filters

The following filters are defined and can be used to categorize code actions in the code_action_post_hook in addition to filtering which code actions the server should provide upon request.

• CASE_SPLIT
• MAKE_CASE
• MAKE_WITH
• MAKE_LEMMA
• ADD_CLAUSE
• EXPR_SEARCH
• GEN_DEF
• REF_HOLE
• INTRO

Demo

Single code actions | split hover | show implicits toggle

Metavars popup and jump

Expression search without and with hints