feat: Agda-specific plugin (Cornelius)

docs/languages/AGDA.md

@@ -0,0 +1,71 @@
+# `agda` layer
+
+The `agda` layer enables support for the Agda proof assistant/programming
+language via:
+- [`cornelis` interactive development](https://github.com/isovector/cornelis);
+- integration with the [`treesitter`](../layers/TREESITTER.md) layer.
+
+## Prerequisites
+
+To use `cornelis`, you have to invoke `stack build` to generate its binary
+within the corresponding plugin folder. This should be
+`${XDG_DATA_HOME:-$HOME/.local/share}"/nvim/site/pack/paks/start/cornelis`.
+Alternatively, if you want to use a binary available on your `$PATH`, you can
+set `cornelis.use_global_binary` to `1`.
+
+As no language server for Agda is currently available on Mason, you need to
+install one yourself on your system.
+
+## Bindings
+
+All the sample bindings and autocommands listed in `cornelis`'s [sample
+configuration](https://github.com/isovector/cornelis#example-configuration) are
+available out of the box as default bindings.
+
+## Configuration
+
+Some fields are available:
+- `cornelis` (`table`) configures `cornelis`'s behavior. Any vim **global**
+  variable listed [in Cornelis's README](https://github.com/isovector/cornelis)
+  is also a valid subfield for this field as long as you strip the `cornelis_`
+  prefix;
+- `binds` (default bindings as explained above) is a list of bindings for
+  `cornelis`, as would be passed to the [`binds` layer](BINDS.md) layer;
+- the usual `lsp` and `lspconfig` fields [shared by most language layers
+  configurations](../layers/LANGUAGES.md#configuration) are also available.
+  However, Agda does not have a language server on Mason, and thus these can
+  only be configured if `lsp` specifies a preinstalled executable for the
+  language server.
+
+## Examples
+
+```lua
+-- path/of/your/vim/config/init.lua
+
+require("visimp")({
+  agda = {
+    cornelis = {
+      split_location = 'vertical' -- different position for info window
+    },
+    bindings = { -- add a new Cornelis binding
+      [{
+        mode = 'n',
+        bind = '<leader>nm',
+        desc = 'Expand ?-holes to "{! !}"',
+      }] = function() vim.cmd("CornelisQuestionToMeta") end,
+    },
+    lsp = "als", -- Agda Language Server executable installed by the user
+    lspconfig = {
+      -- config for the Agda Language Server
+    },
+  },
+  languages = {
+    "agda"
+  }
+})
+```
+
+## Documentation
+
+Documentation for `cornelis` is available within [its own
+README.md](https://github.com/isovector/cornelis).

docs/layers/LANGUAGES.md

@@ -28,7 +28,8 @@ settings:
 
 Several language layers diverge from this basic configuration:
 
-- `agda` and `ampl` do not have LSs on Mason, and thus can only be configured if
+- `agda` has [its own doc page](../languages/AGDA.md);
+- `ampl` does not have a LS on Mason, and thus can only be configured if
   a preinstalled executable is specified;
 - `bash` adds the `fish` option (defaults to `false`) which, if set to true,
   adds support for the Fish shell;

lua/visimp/languages/agda.lua

@@ -1,4 +1,84 @@
 local L = require('visimp.language').new_language 'agda'
+local bind = require('visimp.bind').bind
+local layer = require 'visimp.layer'
+
+---Constructs callbacks that simply invoke the specified vim command
+---@param command string Vim command to invoke (w/o the colon prefix)
+---@return function cb The constructed callback
+local function vim_cmd_cb(command)
+  return function()
+    vim.cmd(command)
+  end
+end
+
+L.default_config = {
+  --Settings for the cornelis plugin (https://github.com/isovector/cornelis).
+  --The value of each field X will be treated as a value for the global
+  --vimscript variable vim.g.cornelis_X.
+  cornelis = {},
+  binds = {
+    [{
+      mode = 'n',
+      bind = '<leader>l',
+      desc = 'Load and type-check buffer',
+    }] = vim_cmd_cb 'CornelisLoad',
+    [{
+      mode = 'n',
+      bind = '<leader>r',
+      desc = 'Refine goal',
+    }] = vim_cmd_cb 'CornelisRefine',
+    [{
+      mode = 'n',
+      bind = '<leader>d',
+      desc = 'Case split',
+    }] = vim_cmd_cb 'CornelisMakeCase',
+    [{
+      mode = 'n',
+      bind = '<leader>,',
+      desc = 'Show Goal type and context',
+    }] = vim_cmd_cb 'CornelisTypeContext',
+    [{
+      mode = 'n',
+      bind = '<leader>.',
+      desc = 'Show inferred type of hole contents',
+    }] = vim_cmd_cb 'CornelisTypeContextInfer',
+    [{
+      mode = 'n',
+      bind = '<leader>n',
+      desc = 'Solve constraints',
+    }] = vim_cmd_cb 'CornelisSolve',
+    [{
+      mode = 'n',
+      bind = '<leader>a',
+      desc = 'Automatic proof search',
+    }] = vim_cmd_cb 'CornelisAuto',
+    [{
+      mode = 'n',
+      bind = 'gd',
+      desc = 'Jump to definition of name at cursor',
+    }] = vim_cmd_cb 'CornelisGoToDefinition',
+    [{
+      mode = 'n',
+      bind = '<leader>[/',
+      desc = 'Jump to previous goal',
+    }] = vim_cmd_cb 'CornelisPrevGoal',
+    [{
+      mode = 'n',
+      bind = ']//',
+      desc = 'Jump to next goal',
+    }] = vim_cmd_cb 'CornelisNextGoal',
+    [{
+      mode = 'n',
+      bind = '<C-A>',
+      desc = '<C-A> (also sub-/superscripts)',
+    }] = vim_cmd_cb 'CornelisInc',
+    [{
+      mode = 'n',
+      bind = 'CornelisDec',
+      desc = '<C-A> (also sub-/superscripts)',
+    }] = vim_cmd_cb 'CornelisDec',
+  },
+}
 
 function L.filetypes()
   return {
@@ -10,6 +90,54 @@ function L.filetypes()
   }
 end
 
+function L.packages()
+  return {
+    'kana/vim-textobj-user',
+    'neovimhaskell/nvim-hs.vim',
+    -- requires running "stack build" after install: see
+    -- https://github.com/isovector/cornelis#installation
+    'isovector/cornelis',
+  }
+end
+
+---Adds all the Agda-specific bindings specified in this layer's config.
+local function add_agda_bindings()
+  bind(L.config.binds, nil)
+end
+
+---Adds Agda-specific autocommands to be triggered when using (literate) Agda
+---files.
+local function create_autocommands()
+  local patterns = { '*.agda', '*.lagda' }
+  vim.api.nvim_create_autocmd({ 'BufRead', 'BufNewFile' }, {
+    pattern = patterns,
+    callback = add_agda_bindings,
+  })
+  vim.api.nvim_create_autocmd({ 'QuitPre' }, {
+    pattern = patterns,
+    command = 'CorneliusCloseInfoWindows',
+  })
+  vim.api.nvim_create_autocmd({ 'BufWritePost' }, {
+    pattern = patterns,
+    command = 'CornelisLoad',
+  })
+  vim.api.nvim_create_autocmd({ 'BufReadPre' }, {
+    pattern = patterns,
+    callback = function()
+      if vim.fn.exists 'CornelisLoad' then
+        -- From https://github.com/isovector/cornelis#example-configuration:
+        -- "this won't work on the first Agda file you open due to a bug"
+        vim.cmd 'silent! CornelisLoad'
+      end
+    end,
+  })
+end
+
+function L.load()
+  layer.to_vimscript_config(L, 'cornelis_', true, 'cornelis')
+  create_autocommands()
+end
+
 function L.grammars()
   return { 'agda' }
 end