cornelis (empty) → 0.2.0.0
raw patch · 26 files changed
+4319/−0 lines, 26 filesdep +QuickCheckdep +aesondep +asyncsetup-changed
Dependencies added: QuickCheck, aeson, async, base, bytestring, containers, cornelis, diff-loc, directory, filepath, fingertree, generic-lens, hspec, lens, levenshtein, megaparsec, mtl, nvim-hs, nvim-hs-contrib, prettyprinter, process, random, resourcet, temporary, text, transformers, unagi-chan, unliftio-core, vector
Files
- ChangeLog.md +24/−0
- LICENSE +30/−0
- README.md +422/−0
- Setup.hs +2/−0
- app/Main.hs +4/−0
- cornelis.cabal +299/−0
- src/Cornelis/Agda.hs +142/−0
- src/Cornelis/Config.hs +41/−0
- src/Cornelis/Debug.hs +25/−0
- src/Cornelis/Diff.hs +87/−0
- src/Cornelis/Goals.hs +179/−0
- src/Cornelis/Highlighting.hs +215/−0
- src/Cornelis/InfoWin.hs +162/−0
- src/Cornelis/Offsets.hs +235/−0
- src/Cornelis/Pretty.hs +248/−0
- src/Cornelis/Subscripts.hs +130/−0
- src/Cornelis/Types.hs +429/−0
- src/Cornelis/Types/Agda.hs +315/−0
- src/Cornelis/Utils.hs +78/−0
- src/Cornelis/Vim.hs +180/−0
- src/Lib.hs +233/−0
- src/Plugin.hs +383/−0
- test/PropertySpec.hs +170/−0
- test/Spec.hs +1/−0
- test/TestSpec.hs +171/−0
- test/Utils.hs +114/−0
+ ChangeLog.md view
@@ -0,0 +1,24 @@+# Changelog for cornelis++## v0.2.0.0 - 2024-04-17++The first official release, after years in the oven.++### Features++- Agda syntax highlighting+- Support for most `agda_mode` commands+- Tab completion for `agda_mode` command options+- Info windows+- Go to definition+- Increment and decrement unicode subscript/superscript numerals+- `agda_input` bindings+- Optional support for interactive `agda_input` via `vim-which-key`+- Text objects for working inside of holes, implicits and justifications+- Jump to next/previous hole+- Use `%` to jump between unicode matchpairs++++## Unreleased changes+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2022++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Sandy Maguire nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,422 @@+# 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](https://www.youtube.com/watch?v=oKUscEWPVAM)+++## 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.++[agda-mode]: https://agda.readthedocs.io/en/latest/tools/emacs-mode.html++## 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 | <kbd>C-c</kbd><kbd>C-l</kbd> |+| `:CornelisGoals` | Show all goals | <kbd>C-c</kbd><kbd>C-?</kbd> |+| `:CornelisRestart` | Kill and restart the `agda` process | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-r</kbd> |+| `:CornelisAbort` | Abort running command | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-a</kbd> |+| `:CornelisSolve <RW>` | Solve constraints | <kbd>C-c</kbd><kbd>C-s</kbd> |+| `:CornelisGoToDefinition` | Jump to definition of name at cursor | <kbd>M-.</kbd> or middle mouse button |+| `:CornelisPrevGoal` | Jump to previous goal | <kbd>C-c</kbd><kbd>C-b</kbd> |+| `:CornelisNextGoal` | Jump to next goal | <kbd>C-c</kbd><kbd>C-f</kbd> |+| `: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 | <kbd>C-c</kbd><kbd>C-SPC</kbd> |+| `:CornelisRefine` | Refine goal | <kbd>C-c</kbd><kbd>C-r</kbd> |+| `:CornelisElaborate <RW>` | Fill goal with normalized hole contents | <kbd>C-c</kbd><kbd>C-m</kbd> |+| `:CornelisAuto` | [Automatic proof search] | <kbd>C-c</kbd><kbd>C-a</kbd> |+| `:CornelisMakeCase` | Case split | <kbd>C-c</kbd><kbd>C-c</kbd> |+| `:CornelisTypeContext <RW>` | Show goal type and context | <kbd>C-c</kbd><kbd>C-,</kbd> |+| `:CornelisTypeInfer <RW>` | Show inferred type of hole contents | <kbd>C-c</kbd><kbd>C-d</kbd> |+| `:CornelisTypeContextInfer <RW>` | Show goal type, context, and inferred type of hole contents | <kbd>C-c</kbd><kbd>C-.</kbd> |+| `:CornelisNormalize <CM>` | Compute normal of hole contents | <kbd>C-c</kbd><kbd>C-n</kbd> |+| `:CornelisWhyInScope` | Show why given name is in scope | <kbd>C-c</kbd><kbd>C-w</kbd> |+| `:CornelisHelperFunc <RW>` | Copy inferred type to register `"` | <kbd>C-c</kbd><kbd>C-h</kbd> |++[Automatic proof search]: https://agda.readthedocs.io/en/latest/tools/auto.html#auto++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 `abstract`s | <kbd>C-u</kbd> |+| `UseShowInstance` | compute normal form of print using `show` instance | <kbd>C-u</kbd><kbd>C-u</kbd> |+| `HeadCompute` | compute weak-head normal form | <kbd>C-u</kbd><kbd>C-u</kbd><kbd>C-u</kbd> |++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](https://github.com/isovector/cornelis/blob/master/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: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`](https://docs.haskellstack.org/en/stable/install_and_upgrade/) on your PATH!++```viml+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:++- https://github.com/agda/agda/pull/5752+- https://github.com/agda/agda/pull/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.++<details>+<summary>Nix details</summary>++```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 ];+ };+}+```+</details>++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.+++### 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 <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`](./syntax/agda.vim).+These groups are linked to default highlighting groups+([`:h group-name`](https://neovim.io/doc/user/syntax.html#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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,4 @@+module Main (main) where++import Lib (main)+
+ cornelis.cabal view
@@ -0,0 +1,299 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.36.0.+--+-- see: https://github.com/sol/hpack++name: cornelis+version: 0.2.0.0+description: Please see the README on GitHub at <https://github.com/isovector/cornelis#readme>+homepage: https://github.com/isovector/cornelis#readme+bug-reports: https://github.com/isovector/cornelis/issues+author: Sandy Maguire+maintainer: sandy@sandymaguire.me+copyright: Sandy Maguire+license: BSD3+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md+ ChangeLog.md++source-repository head+ type: git+ location: https://github.com/isovector/cornelis++library+ exposed-modules:+ Cornelis.Agda+ Cornelis.Config+ Cornelis.Debug+ Cornelis.Diff+ Cornelis.Goals+ Cornelis.Highlighting+ Cornelis.InfoWin+ Cornelis.Offsets+ Cornelis.Pretty+ Cornelis.Subscripts+ Cornelis.Types+ Cornelis.Types.Agda+ Cornelis.Utils+ Cornelis.Vim+ Lib+ Plugin+ other-modules:+ Paths_cornelis+ hs-source-dirs:+ src+ default-extensions:+ BangPatterns+ BinaryLiterals+ ConstrainedClassMethods+ ConstraintKinds+ DataKinds+ DeriveDataTypeable+ DeriveFoldable+ DeriveFunctor+ DeriveGeneric+ DeriveLift+ DeriveTraversable+ DoAndIfThenElse+ EmptyCase+ EmptyDataDecls+ EmptyDataDeriving+ ExistentialQuantification+ ExplicitForAll+ FlexibleContexts+ FlexibleInstances+ ForeignFunctionInterface+ GADTSyntax+ GeneralisedNewtypeDeriving+ HexFloatLiterals+ ImplicitPrelude+ ImportQualifiedPost+ InstanceSigs+ LambdaCase+ KindSignatures+ MonomorphismRestriction+ MultiParamTypeClasses+ NamedFieldPuns+ NumericUnderscores+ PatternGuards+ PolyKinds+ PostfixOperators+ RankNTypes+ RelaxedPolyRec+ ScopedTypeVariables+ StandaloneDeriving+ StandaloneKindSignatures+ StarIsType+ TraditionalRecordSyntax+ TupleSections+ TypeApplications+ TypeOperators+ TypeSynonymInstances+ ghc-options: -Wall+ build-depends:+ QuickCheck >=2.14.2+ , aeson >=1.5.6.0+ , async+ , base >=4.7 && <5+ , bytestring+ , containers+ , diff-loc >=0.1.0.0+ , directory+ , filepath+ , fingertree >=0.1.4.2+ , generic-lens >=2.1.0.0+ , hspec >=2.7.10+ , lens >=4.19.2+ , levenshtein >=0.1.3.0+ , megaparsec >=9.0.1 && <10+ , mtl+ , nvim-hs >=2.2.0.3 && <3+ , nvim-hs-contrib >=2.0 && <3+ , prettyprinter >=1.7.1 && <2+ , process+ , random+ , resourcet >=1.2.4.3+ , text+ , transformers+ , unagi-chan >=0.4.1.3+ , unliftio-core >=0.2.0.1+ , vector+ default-language: Haskell2010++executable cornelis+ main-is: Main.hs+ other-modules:+ Paths_cornelis+ hs-source-dirs:+ app+ default-extensions:+ BangPatterns+ BinaryLiterals+ ConstrainedClassMethods+ ConstraintKinds+ DataKinds+ DeriveDataTypeable+ DeriveFoldable+ DeriveFunctor+ DeriveGeneric+ DeriveLift+ DeriveTraversable+ DoAndIfThenElse+ EmptyCase+ EmptyDataDecls+ EmptyDataDeriving+ ExistentialQuantification+ ExplicitForAll+ FlexibleContexts+ FlexibleInstances+ ForeignFunctionInterface+ GADTSyntax+ GeneralisedNewtypeDeriving+ HexFloatLiterals+ ImplicitPrelude+ ImportQualifiedPost+ InstanceSigs+ LambdaCase+ KindSignatures+ MonomorphismRestriction+ MultiParamTypeClasses+ NamedFieldPuns+ NumericUnderscores+ PatternGuards+ PolyKinds+ PostfixOperators+ RankNTypes+ RelaxedPolyRec+ ScopedTypeVariables+ StandaloneDeriving+ StandaloneKindSignatures+ StarIsType+ TraditionalRecordSyntax+ TupleSections+ TypeApplications+ TypeOperators+ TypeSynonymInstances+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ QuickCheck >=2.14.2+ , aeson >=1.5.6.0+ , async+ , base >=4.7 && <5+ , bytestring+ , containers+ , cornelis+ , diff-loc >=0.1.0.0+ , directory+ , filepath+ , fingertree >=0.1.4.2+ , generic-lens >=2.1.0.0+ , hspec >=2.7.10+ , lens >=4.19.2+ , levenshtein >=0.1.3.0+ , megaparsec >=9.0.1 && <10+ , mtl+ , nvim-hs >=2.2.0.3 && <3+ , nvim-hs-contrib >=2.0 && <3+ , prettyprinter >=1.7.1 && <2+ , process+ , random+ , resourcet >=1.2.4.3+ , text+ , transformers+ , unagi-chan >=0.4.1.3+ , unliftio-core >=0.2.0.1+ , vector+ default-language: Haskell2010++test-suite test+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ other-modules:+ PropertySpec+ TestSpec+ Utils+ Paths_cornelis+ hs-source-dirs:+ test+ default-extensions:+ BangPatterns+ BinaryLiterals+ ConstrainedClassMethods+ ConstraintKinds+ DataKinds+ DeriveDataTypeable+ DeriveFoldable+ DeriveFunctor+ DeriveGeneric+ DeriveLift+ DeriveTraversable+ DoAndIfThenElse+ EmptyCase+ EmptyDataDecls+ EmptyDataDeriving+ ExistentialQuantification+ ExplicitForAll+ FlexibleContexts+ FlexibleInstances+ ForeignFunctionInterface+ GADTSyntax+ GeneralisedNewtypeDeriving+ HexFloatLiterals+ ImplicitPrelude+ ImportQualifiedPost+ InstanceSigs+ LambdaCase+ KindSignatures+ MonomorphismRestriction+ MultiParamTypeClasses+ NamedFieldPuns+ NumericUnderscores+ PatternGuards+ PolyKinds+ PostfixOperators+ RankNTypes+ RelaxedPolyRec+ ScopedTypeVariables+ StandaloneDeriving+ StandaloneKindSignatures+ StarIsType+ TraditionalRecordSyntax+ TupleSections+ TypeApplications+ TypeOperators+ TypeSynonymInstances+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ QuickCheck >=2.14.2+ , aeson >=1.5.6.0+ , async+ , base >=4.7 && <5+ , bytestring+ , containers+ , cornelis+ , diff-loc >=0.1.0.0+ , directory+ , filepath+ , fingertree >=0.1.4.2+ , generic-lens >=2.1.0.0+ , hspec+ , lens >=4.19.2+ , levenshtein >=0.1.3.0+ , megaparsec >=9.0.1 && <10+ , mtl+ , nvim-hs >=2.2.0.3 && <3+ , nvim-hs-contrib >=2.0 && <3+ , prettyprinter >=1.7.1 && <2+ , process+ , random+ , resourcet >=1.2.4.3+ , temporary+ , text+ , transformers+ , unagi-chan >=0.4.1.3+ , unliftio-core >=0.2.0.1+ , vector+ default-language: Haskell2010
+ src/Cornelis/Agda.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedStrings #-}++module Cornelis.Agda where++import Control.Concurrent.Chan.Unagi (newChan, readChan, writeChan)+import Control.Lens+import Control.Monad (forever, replicateM_, when)+import Control.Monad.IO.Class+import Control.Monad.State+import Cornelis.Debug (reportExceptions)+import Cornelis.InfoWin (buildInfoBuffer)+import Cornelis.Types+import Cornelis.Types.Agda+import Cornelis.Utils+import Data.Aeson+import Data.IORef+import qualified Data.Map as M+import qualified Data.Text as T+import qualified Data.Text.Lazy as LT+import Data.Text.Lazy.Encoding (encodeUtf8)+import qualified Data.Text.Lazy.IO as LT+import Neovim hiding (err)+import Neovim.API.Text+import System.IO hiding (hGetLine)+import System.Process+++------------------------------------------------------------------------------+-- | When true, dump out received JSON as it arrives.+debugJson :: Bool+debugJson = False+++------------------------------------------------------------------------------+-- | Create an 'Agda' environment for the given buffer. This spawns an+-- asynchronous thread that keeps an agda process alive as long as vim is open.+--+-- TODO(sandy): This leaks the process when the buffer is closed.+spawnAgda :: Buffer -> Neovim CornelisEnv Agda+spawnAgda buffer = do+ (m_in, m_out, _, hdl) <-+ liftIO $ createProcess $+ (proc "agda" ["--interaction-json"])+ { std_in = CreatePipe , std_out = CreatePipe }+ (c_in, c_out) <- liftIO newChan+ ready <- liftIO $ newIORef True+ case (m_in, m_out) of+ (Just hin, Just hout) -> do+ liftIO $ do+ hSetBuffering hin NoBuffering+ hSetBuffering hout NoBuffering++ let whenReady act = liftIO $ do+ -- Agda outputs "JSON> " when it is ready+ -- We skip it, and set the ready flag+ c <- hLookAhead hout+ case c of+ 'J' -> replicateM_ 6 (hGetChar hout) >> act+ _ -> pure ()++ -- On the first load, we make ourselves ready before Agda tells us anything+ void $ neovimAsync $ (whenReady (pure ()) >>) . forever $ reportExceptions $ do+ whenReady $ atomicWriteIORef ready True+ resp <- liftIO $ LT.hGetLine hout+ chan <- asks ce_stream+ case eitherDecode @Response $ encodeUtf8 resp of+ _ | LT.null resp -> pure ()+ Left err -> vim_report_error $ T.pack err+ Right res -> do+ case res of+ HighlightingInfo _ _ -> pure ()+ _ -> when debugJson $ vim_report_error $ T.pack $ show resp+ liftIO $ writeChan chan $ AgdaResp buffer res++ void $ neovimAsync $ liftIO $ forever $ do+ msg <- readChan c_out+ atomicWriteIORef ready False+ hPutStrLn hin msg++ pure $ Agda buffer ready c_in hdl+ (_, _) -> error "can't start agda"+++------------------------------------------------------------------------------+-- | Drop a prefix from the text, if it exists.+dropPrefix :: LT.Text -> LT.Text -> LT.Text+dropPrefix pref msg+ | LT.isPrefixOf pref msg = LT.drop (LT.length pref) msg+ | otherwise = msg+++------------------------------------------------------------------------------+-- | Send an 'Interaction' to an 'Agda'.+runIOTCM :: Interaction -> Agda -> Neovim env ()+runIOTCM i agda = do+ iotcm <- buildIOTCM i $ a_buffer agda+ -- liftIO $ appendFile "/tmp/agda.spy" $ show iotcm+ liftIO $ writeChan (a_req agda) (show iotcm)+++------------------------------------------------------------------------------+-- | Construct an 'IOTCM' for a buffer.+buildIOTCM :: Interaction -> Buffer -> Neovim env IOTCM+buildIOTCM i buffer = do+ fp <- buffer_get_name buffer+ pure $ IOTCM fp NonInteractive Direct i+++------------------------------------------------------------------------------+-- | Get the current buffer and run the continuation.+withCurrentBuffer :: (Buffer -> Neovim env a) -> Neovim env a+withCurrentBuffer f = vim_get_current_buffer >>= f+++------------------------------------------------------------------------------+-- | Ensure we have a 'BufferStuff' attached to the current buffer.+withAgda :: Neovim CornelisEnv a -> Neovim CornelisEnv a+withAgda m = do+ buffer <- vim_get_current_buffer+ gets (M.lookup buffer . cs_buffers) >>= \case+ Just _ -> m+ Nothing -> do+ agda <- spawnAgda buffer+ iw <- buildInfoBuffer+ modify' $ #cs_buffers %~ M.insert buffer BufferStuff+ { bs_agda_proc = agda+ , bs_ips = mempty+ , bs_ip_exts = mempty+ , bs_goto_sites = mempty+ , bs_goals = AllGoalsWarnings [] [] [] []+ , bs_info_win = iw+ , bs_code_map = mempty+ }+ m+++------------------------------------------------------------------------------+-- | Get the 'Agda' environment for a given buffer.+getAgda :: Buffer -> Neovim CornelisEnv Agda+getAgda buffer = gets $ bs_agda_proc . (M.! buffer) . cs_buffers+
+ src/Cornelis/Config.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE OverloadedStrings #-}++module Cornelis.Config where++import Cornelis.Types+import Cornelis.Utils (objectToInt, objectToText)+import Data.Maybe (fromMaybe)+import qualified Data.Text as T+import Neovim+import Neovim.API.Text+import Control.Monad ((<=<))+++------------------------------------------------------------------------------+-- | Attempt to get a variable from vim.+getVar :: Text -> Neovim env (Maybe Object)+getVar v+ = catchNeovimException (Just <$> vim_get_var v)+ $ const+ $ pure Nothing+++------------------------------------------------------------------------------+-- | Get the first variable from vim that succeeds. Useful for variable names+-- that have changed over time.+getVarWithAlternatives :: [Text] -> Neovim env (Maybe Object)+getVarWithAlternatives = fmap getFirst . foldMap (fmap First . getVar)+++------------------------------------------------------------------------------+-- | Build a 'CornelisConfig' from .vimrc+getConfig :: Neovim env CornelisConfig+getConfig+ = CornelisConfig+ <$> fmap (fromMaybe 31 . (objectToInt =<<))+ (getVar "cornelis_max_size")+ <*> fmap (fromMaybe 31 . (objectToInt =<<))+ (getVar "cornelis_max_width")+ <*> (fromMaybe Horizontal . (>>= (readSplitLocation . T.unpack <=< objectToText)) <$>+ getVarWithAlternatives ["cornelis_split_location", "cornelis_split_direction"])+
+ src/Cornelis/Debug.hs view
@@ -0,0 +1,25 @@+module Cornelis.Debug where++import Control.Exception (catch, throw)+import Control.Monad.IO.Class+import System.IO.Error (isAlreadyInUseError)+import Neovim+import Neovim.API.String (vim_report_error)+++reportExceptions :: Neovim env () -> Neovim env ()+reportExceptions =+ flip catchNeovimException $ vim_report_error . mappend "UNHANDLED EXCEPTION " . show++traceMX :: Show a => String -> a -> Neovim env ()+traceMX herald a =+ vim_report_error $ "!!!" <> herald <> ": " <> show a++debug :: (Show a, MonadIO m) => a -> m ()+debug x = liftIO $ go 100+ where+ go 0 = pure ()+ go n =+ catch+ (appendFile "/tmp/agda.log" (show x <> "\n"))+ (\e -> if isAlreadyInUseError e then go (n-1 :: Int) else throw e)
+ src/Cornelis/Diff.hs view
@@ -0,0 +1,87 @@+-- | Maintain a Diff between the text that Agda loaded most recently+-- and the current Vim buffer. There is one such diff for every buffer,+-- indexed by 'BufferNum'.+--+-- This exports three functions:+-- - 'resetDiff' empties the diff when reloading Agda+-- - 'recordUpdate' adds a buffer update to the diff.+-- - 'translateInterval' applies the Diff to an interval coming from Agda,+-- turning it into an interval for the current buffer.+module Cornelis.Diff+ ( resetDiff+ , translateInterval+ , recordUpdate+ , Replace(..)+ , Colline(..)+ , Vallee(..)+ ) where++import Data.IORef (atomicModifyIORef')+import qualified Data.Map as Map+import Data.Tuple (swap)+import DiffLoc (Replace(..), Colline(..), Vallee(..))+import qualified DiffLoc as D+import Neovim+import Cornelis.Offsets+import Cornelis.Types++-- | A general function for modifying Diffs, shared between the three functions below.+modifyDiff :: BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a+modifyDiff buf f = do+ csRef <- asks ce_state+ liftIO $ atomicModifyIORef' csRef $ \cs ->+ let (a, ds') = Map.alterF (fmap Just . swap . alter) buf (cs_diff cs)+ in (cs { cs_diff = ds' }, a)+ where+ alter Nothing = f D.emptyDiff+ alter (Just d) = f d++-- These three functions are essentially monadic wrappers, using 'modifyDiff',+-- around the corresponding diff-loc functions:+--+-- @+-- 'D.emptyDiff' :: Diff0+-- 'D.addDiff' :: D.Replace DPos -> Diff0 -> Diff0+-- 'D.mapDiff' :: Diff0 -> D.Interval DPos -> Maybe (D.Interval DPos)+-- @+--+-- This relies on instances of 'D.Amor' and 'D.Origin' implemented in 'Cornelis.Offsets'.++-- | Reset the diff to an empty diff.+resetDiff :: BufferNum -> Neovim CornelisEnv ()+resetDiff buf = modifyDiff buf $ const (D.emptyDiff, ())++-- | Add a buffer update (insertion or deletion) to the diff.+-- The buffer update event coming from Vim is structured exactly how the diff-loc+-- library expects it.+recordUpdate :: BufferNum -> D.Replace DPos -> Neovim CornelisEnv ()+recordUpdate buf r = modifyDiff buf $ \d -> (D.addDiff r d, ())++-- | Given an interval coming from Agda (a pair of start and end positions),+-- find the corresponding interval in the current buffer.+-- If an edit touches the interval, return Nothing.+translateInterval :: BufferNum -> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos))+translateInterval buf sp = modifyDiff buf $ \d -> (d, translate d)+ where+ translate :: Diff0 -> Maybe (Interval VimPos)+ translate d = fmap toInterval . D.mapDiff d =<< fromInterval sp++-- | Convert a Cornelis interval (pair of positions) to a diff-loc interval+-- (start position and a vector towards the end position). This is Nothing+-- if the end precedes the start.+fromInterval :: Interval VimPos -> Maybe (D.Interval DPos)+fromInterval (Interval p1 p2) = (q1 D.:..) <$> (q2 D..-.? q1)+ where+ q1 = fromVimPos p1+ q2 = fromVimPos p2++-- | Inverse of 'fromInterval'.+toInterval :: D.Interval DPos -> Interval VimPos+toInterval (q D.:.. v) = Interval (toVimPos q) (toVimPos (q D..+ v))++-- | Convert from Cornelis positions to diff-loc positions.+fromVimPos :: VimPos -> DPos+fromVimPos (Pos l c) = Colline l c++toVimPos :: DPos -> VimPos+toVimPos (Colline l c) = Pos l c
+ src/Cornelis/Goals.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE OverloadedStrings #-}++module Cornelis.Goals where++import Control.Arrow ((&&&))+import Control.Lens+import Cornelis.Agda (withAgda)+import Cornelis.Offsets+import Cornelis.Types+import Cornelis.Utils+import Cornelis.Vim+import Data.Foldable (toList, fold)+import Data.List+import qualified Data.Map as M+import Data.Maybe+import Data.Ord+import qualified Data.Text as T+import Data.Traversable (for)+import Neovim+import Neovim.API.Text+import Neovim.User.Input (input)+++------------------------------------------------------------------------------+-- | Get the spanning interval of an interaction point. If we already have+-- highlighting information from vim, use the extmark for this goal, otherwise+-- using the interval that Agda knows about.+getIpInterval :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval+getIpInterval b ip = do+ ns <- asks ce_namespace+ extmap <- withBufferStuff b $ pure . bs_ip_exts+ fmap (fromMaybe (ip_interval' ip)) $+ case flip M.lookup extmap $ ip_id ip of+ Just i -> getExtmarkIntervalById ns b i+ Nothing -> pure Nothing+++--------------------------------------------------------------------------------+-- | Move the vim cursor to a goal in the current window+findGoal :: Ord a => (AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()+findGoal hunt = withAgda $ do+ w <- vim_get_current_window+ b <- window_get_buffer w+ withBufferStuff b $ \bs -> do+ pos <- getWindowCursor w+ let goals = toList $ bs_ips bs+ judged_goals <- fmap catMaybes $ for goals $ \ip -> do+ int <- getIpInterval b ip+ pure+ . sequenceA+ . (id &&& hunt pos)+ $ iStart int+ case judged_goals of+ [] -> reportInfo "No hole matching predicate"+ _ -> do+ let pos' = fst $ maximumBy (comparing snd) judged_goals+ setWindowCursor w pos'+++------------------------------------------------------------------------------+-- | Move the vim cursor to the previous interaction point.+prevGoal :: Neovim CornelisEnv ()+prevGoal =+ findGoal $ \pos goal ->+ case pos > goal of+ False -> Nothing+ True -> Just ( p_line goal .-. p_line pos+ , p_col goal .-. p_col pos -- TODO: This formula looks fishy+ )+++------------------------------------------------------------------------------+-- | Move the vim cursor to the next interaction point.+nextGoal :: Neovim CornelisEnv ()+nextGoal =+ findGoal $ \pos goal ->+ case pos < goal of+ False -> Nothing+ True -> Just $ Down ( p_line goal .-. p_line pos+ , p_col goal .-. p_col pos+ )++------------------------------------------------------------------------------+-- | Uses highlighting extmarks to determine what a hole is; since the user+-- might have typed inside of a {! !} goal since they last saved.+getGoalAtCursor :: Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))+getGoalAtCursor = do+ w <- nvim_get_current_win+ b <- window_get_buffer w+ p <- getWindowCursor w+ fmap (b, ) $ getGoalAtPos b p+++getGoalAtPos+ :: Buffer+ -> AgdaPos+ -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))+getGoalAtPos b p = do+ fmap (getFirst . fold) $ withBufferStuff b $ \bs -> do+ for (bs_ips bs) $ \ip -> do+ int <- getIpInterval b ip+ pure $ case containsPoint int p of+ False -> mempty+ True -> pure $ ip { ip_intervalM = Identity int }++------------------------------------------------------------------------------+-- | Run a continuation on a goal at the current position in the current+-- buffer, if it exists.+withGoalAtCursor+ :: (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)+ -> Neovim CornelisEnv (Maybe a)+withGoalAtCursor f = getGoalAtCursor >>= \case+ (_, Nothing) -> do+ reportInfo "No goal at cursor"+ pure Nothing+ (b, Just ip) -> fmap Just $ f b ip++------------------------------------------------------------------------------+-- | Run the first continuation on the goal at the current position,+-- otherwise run the second continuation.+--+-- If there is a non-empty hole, provide its content to the first continuation.+-- If the hole is empty, prompt for input and provide that.+--+-- If there is no goal, prompt the user for input and run the second continuation.+withGoalContentsOrPrompt+ :: String+ -- ^ Text to print when prompting the user for input+ -> (InteractionPoint Identity -> String -> Neovim CornelisEnv a)+ -- ^ Continuation to run on goal, with hole contents+ -> (String -> Neovim CornelisEnv a)+ -- ^ Continuation to run on user input if there's no goal here+ -> Neovim CornelisEnv a+withGoalContentsOrPrompt prompt_str on_goal on_no_goal = getGoalAtCursor >>= \case+ (_, Nothing) ->+ -- If there's no goal here, run `on_no_goal` on user input.+ prompt >>= on_no_goal+ (b, Just ip) -> do+ content <- getGoalContents b ip+ -- If there is a goal under the cursor, but it's contents+ -- are empty, prompt the user for input. Otherwise, unpack+ -- the hole contents are provide that.+ if T.null content+ then prompt >>= on_goal ip+ else on_goal ip (T.unpack content)+ where+ prompt = input prompt_str Nothing Nothing+++------------------------------------------------------------------------------+-- | Get the contents of a goal.+getGoalContentsMaybe :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)+getGoalContentsMaybe b ip = do+ int <- getIpInterval b ip+ iv <- fmap T.strip $ getBufferInterval b int+ pure $ case iv of+ "?" -> Nothing+ -- Chop off {!, !} and trim any spaces.+ _ -> Just $ T.strip $ T.dropEnd 2 $ T.drop 2 iv+++------------------------------------------------------------------------------+-- | Like 'getGoalContents_maybe'.+getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text+getGoalContents b ip = fromMaybe "" <$> getGoalContentsMaybe b ip+++------------------------------------------------------------------------------+-- | Replace all single @?@ tokens with interaction holes.+replaceQuestion :: Text -> Text+replaceQuestion = T.unwords . fmap go . T.words+ where+ go "(?" = "({! !}"+ go "?" = "{! !}"+ go x =+ case T.dropWhileEnd (== ')') x of+ "?" -> "{! !}" <> T.drop 1 x+ _ -> x+
+ src/Cornelis/Highlighting.hs view
@@ -0,0 +1,215 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TypeApplications #-}++module Cornelis.Highlighting where++import Control.Lens ((<>~), (.~))+import Control.Monad.Trans (lift)+import Control.Monad.Trans.Maybe+import Cornelis.Diff+import Cornelis.Offsets+import Cornelis.Pretty+import Cornelis.Types+import Cornelis.Utils+import Cornelis.Vim (unvimify, vimify)+import Data.Coerce (coerce)+import Data.IntervalMap.FingerTree (IntervalMap)+import qualified Data.IntervalMap.FingerTree as IM+import qualified Data.Map as M+import Data.Maybe (listToMaybe, catMaybes, mapMaybe)+import qualified Data.Text as T+import Data.Text.Encoding (encodeUtf8)+import Data.Traversable (for)+import Data.Vector (Vector)+import qualified Data.Vector as V+import Neovim+import Neovim.API.Text++lineIntervalsForBuffer :: Buffer -> Neovim CornelisEnv LineIntervals+lineIntervalsForBuffer b = do+ buf_lines <- nvim_buf_get_lines b 0 (-1) True+ pure $ getLineIntervals buf_lines++updateLineIntervals :: Buffer -> Neovim CornelisEnv ()+updateLineIntervals b = do+ li <- lineIntervalsForBuffer b+ modifyBufferStuff b $ #bs_code_map .~ li++highlightBuffer :: Buffer -> [Highlight] -> Neovim CornelisEnv (M.Map AgdaInterval Extmark)+highlightBuffer b hs = withBufferStuff b $ \bs -> do+ let li = bs_code_map bs+ (holes, exts) <- fmap unzip $ for hs $ \hl -> do+ (hole, mext) <- addHighlight b li hl+ pure (hole, (hl, mext))++ let zs = catMaybes $ do+ (hl, mext) <- exts+ pure $ do+ ext <- mext+ ds <- hl_definitionSite hl+ pure (ext, ds)++ modifyBufferStuff b $ #bs_goto_sites <>~ M.fromList zs+ pure $ mconcat holes++getLineIntervals :: Vector Text -> LineIntervals+getLineIntervals = LineIntervals . go (toOneIndexed @Int 1) (toZeroIndexed @Int 0)+ where+ go+ :: AgdaIndex+ -> LineNumber 'ZeroIndexed+ -> Vector Text+ -> IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)+ go pos line v+ | Just (t, ss) <- V.uncons v =+ let len = T.length t+ pos' = pos .+ Offset len+ in IM.insert (IM.Interval pos pos') (line, t)+ $ go (incIndex pos') (incIndex line) ss+ | otherwise = mempty++lookupPoint :: LineIntervals -> AgdaIndex -> Maybe VimPos+lookupPoint (LineIntervals im) i = do+ (IM.Interval lineStart _, (line, s)) <- listToMaybe $ IM.search i im+ let col = toBytes s (toZeroIndexed @Int 0 .+ (i .-. lineStart))+ pure (Pos line col)++------------------------------------------------------------------------------+-- | Returns any holes it tried to highlight on the left+addHighlight+ :: Buffer+ -> LineIntervals+ -> Highlight+ -> Neovim CornelisEnv (M.Map AgdaInterval Extmark, Maybe Extmark)+addHighlight b lis hl = do+ case Interval+ <$> lookupPoint lis (hl_start hl)+ <*> lookupPoint lis (hl_end hl) of+ Just int@(Interval start end) -> do+ ext <- setHighlight b int $ parseHighlightGroup hl++ fmap (, ext) $ case isHole hl of+ False -> pure mempty+ True -> do+ let vint = Interval start end+ aint <- traverse (unvimify b) vint+ pure $ maybe mempty (M.singleton aint) ext+ Nothing -> pure (mempty, Nothing)+ where+ -- Convert the first atom in a reply to a custom highlight+ -- group, and return whether it is a hole or not.+ --+ -- Note that Agda returns both "aspects" for regular syntax+ -- and "other aspects" for error messages, warnings and hints.+ -- Currently, the latter kind takes precedence, since it is+ -- located first in the message returned by Agda.+ --+ -- See 'Cornelis.Pretty.HighlightGroup' for more details.+ --+ -- TODO: Investigate whether is is possible/feasible to+ -- attach multiple HL groups to buffer locations.+ parseHighlightGroup :: Highlight -> Maybe HighlightGroup+ parseHighlightGroup = listToMaybe . mapMaybe atomToHlGroup . hl_atoms++ isHole :: Highlight -> Bool+ isHole = elem "hole" . hl_atoms++setHighlight+ :: Buffer+ -> Interval VimPos+ -> Maybe HighlightGroup+ -> Neovim CornelisEnv (Maybe Extmark)+setHighlight b i hl = do+ bn <- buffer_get_number b+ mi' <- translateInterval bn i+ case mi' of+ Just i' -> setHighlight' b i' hl+ Nothing -> pure Nothing++setHighlight'+ :: Buffer+ -> Interval VimPos+ -> Maybe HighlightGroup+ -> Neovim CornelisEnv (Maybe Extmark)+setHighlight' b (Interval (Pos sl sc) (Pos el ec)) hl = do+ ns <- asks ce_namespace+ let from0 = fromZeroIndexed+ flip catchNeovimException (const (pure Nothing))+ $ fmap (Just . coerce)+ $ nvim_buf_set_extmark b ns (from0 sl) (from0 sc)+ $ M.fromList+ $ [ ( "end_line"+ , ObjectInt $ from0 el+ )+ , ( "end_col"+ , ObjectInt $ from0 ec+ )+ ] +++ concatMap (\hl' ->+ [ ( "hl_group"+ , ObjectString $ encodeUtf8 $ T.pack $ show hl'+ )+ , ( "priority"+ , ObjectInt $ priority hl'+ )+ ])+ hl+++highlightInterval+ :: Buffer+ -> AgdaInterval+ -> HighlightGroup+ -> Neovim CornelisEnv (Maybe Extmark)+highlightInterval b int hl = do+ int' <- traverse (vimify b) int+ setHighlight b int' $ Just hl+++parseExtmark :: Buffer -> Object -> Neovim CornelisEnv (Maybe ExtmarkStuff)+parseExtmark b+ (ObjectArray ( (objectToInt -> Just ext)+ : (objectToInt @Int -> Just (toZeroIndexed -> start_line))+ : (objectToInt @Int -> Just (toZeroIndexed -> start_col))+ : ObjectMap details+ : _+ )) = runMaybeT $ do+ end_col <- hoistMaybe $ fmap toZeroIndexed+ . objectToInt @Int =<< M.lookup (ObjectString "end_col") details+ end_line <- hoistMaybe $ fmap toZeroIndexed+ . objectToInt @Int =<< M.lookup (ObjectString "end_row") details+ hlgroup <- hoistMaybe $ objectToText =<< M.lookup (ObjectString "hl_group") details+ int <- lift $ traverse (unvimify b) (Interval (Pos start_line start_col) (Pos end_line end_col))+ pure $ ExtmarkStuff+ { es_mark = Extmark ext+ , es_hlgroup = hlgroup+ , es_interval = int+ }+parseExtmark _ _ = pure Nothing++#if __GLASGOW_HASKELL__ <= 904+hoistMaybe :: Applicative m => Maybe a -> MaybeT m a+hoistMaybe = MaybeT . pure+#endif+++getExtmarks :: Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff]+getExtmarks b p = do+ ns <- asks ce_namespace+ vp <- vimify b p+ let -- i = 0 for beginning of line, i = -1 for end of line+ pos i = ObjectArray [ ObjectInt $ fromZeroIndexed (p_line vp)+ , ObjectInt i+ ]+ res <- nvim_buf_get_extmarks b ns (pos 0) (pos (-1)) $ M.singleton "details" $ ObjectBool True+ marks <- fmap catMaybes $ traverse (parseExtmark b) $ V.toList res++ pure $ marks >>= \es ->+ case containsPoint (es_interval es) p of+ False -> mempty+ True -> [es]+
+ src/Cornelis/InfoWin.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE OverloadedStrings #-}++module Cornelis.InfoWin (closeInfoWindows, showInfoWindow, buildInfoBuffer) where++import Prelude hiding (Left, Right)+import Control.Monad (unless)+import Control.Monad.State.Class+import Cornelis.Pretty+import Cornelis.Types+import Cornelis.Utils (withBufferStuff, windowsForBuffer, savingCurrentWindow, visibleBuffers)+import Data.Foldable (for_)+import qualified Data.Map as M+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Traversable (for)+import qualified Data.Vector as V+import Neovim+import Neovim.API.Text+import Prettyprinter (layoutPretty, LayoutOptions (LayoutOptions), PageWidth (AvailablePerLine))+import Prettyprinter.Render.Text (renderStrict)+++cornelisWindowVar :: Text+cornelisWindowVar = "cornelis_window"++getBufferVariableOfWindow :: NvimObject o => Text -> Window -> Neovim env (Maybe o)+getBufferVariableOfWindow variableName window = do+ window_is_valid window >>= \case+ False -> pure Nothing+ True -> do+ buffer <- window_get_buffer window+ let getVariableValue = Just . fromObjectUnsafe <$> buffer_get_var buffer variableName+ getVariableValue `catchNeovimException` const (pure Nothing)++closeInfoWindowsForUnseenBuffers :: Neovim CornelisEnv ()+closeInfoWindowsForUnseenBuffers = do+ seen <- S.fromList . fmap snd <$> visibleBuffers+ bufs <- gets cs_buffers+ let known = M.keysSet bufs+ unseen = known S.\\ seen+ for_ unseen $ \b -> do+ for_ (M.lookup b bufs) $ \bs -> do+ ws <- windowsForBuffer $ iw_buffer $ bs_info_win bs+ for_ ws $ flip nvim_win_close True++closeInfoWindows :: Neovim env ()+closeInfoWindows = do+ ws <- vim_get_windows+ for_ ws $ \w -> getBufferVariableOfWindow cornelisWindowVar w >>= \case+ Just True -> nvim_win_close w True+ _ -> pure ()+++closeInfoWindowForBuffer :: BufferStuff -> Neovim CornelisEnv ()+closeInfoWindowForBuffer bs = do+ let InfoBuffer ib = bs_info_win bs+ ws <- windowsForBuffer ib+ for_ ws $ flip nvim_win_close True++++showInfoWindow :: Buffer -> Doc HighlightGroup -> Neovim CornelisEnv ()+showInfoWindow b doc = withBufferStuff b $ \bs -> do+ let ib = bs_info_win bs+ closeInfoWindowsForUnseenBuffers++ vis <- visibleBuffers+ ns <- asks ce_namespace++ -- Check if the info win still exists, and if so, just modify it+ found <- fmap or $+ for vis $ \(w, vb) -> do+ case vb == iw_buffer ib of+ False -> pure False+ True -> do+ writeInfoBuffer ns ib doc+ resizeInfoWin w ib+ pure True++ -- Otherwise we need to rebuild it+ unless found $ do+ closeInfoWindowForBuffer bs+ writeInfoBuffer ns ib doc+ ws <- windowsForBuffer b+ for_ ws $ buildInfoWindow ib++++buildInfoBuffer :: Neovim env InfoBuffer+buildInfoBuffer = do+ b <-+ -- not listed in the buffer list, is throwaway+ nvim_create_buf False True++ -- Setup things in the buffer+ void $ buffer_set_var b cornelisWindowVar $ ObjectBool True+ nvim_buf_set_option b "modifiable" $ ObjectBool False+ nvim_buf_set_option b "filetype" $ ObjectString "agdainfo"+ pure $ InfoBuffer b+++++buildInfoWindow :: InfoBuffer -> Window -> Neovim CornelisEnv Window+buildInfoWindow (InfoBuffer split_buf) w = savingCurrentWindow $ do+ nvim_set_current_win w+ max_height <- asks $ T.pack . show . cc_max_height . ce_config+ max_width <- asks $ T.pack . show . cc_max_width . ce_config+ asks (cc_split_location . ce_config) >>= \case+ Vertical -> vim_command $ max_width <> " vsplit"+ Horizontal -> vim_command $ max_height <> " split"+ OnLeft -> vim_command $ "topleft " <> max_width <> " vsplit"+ OnRight -> vim_command $ "botright " <> max_width <> " vsplit"+ OnTop -> vim_command $ "topleft " <> max_height <> " split"+ OnBottom -> vim_command $ "botright " <> max_height <> " split"+ split_win <- nvim_get_current_win+ nvim_win_set_buf split_win split_buf++ -- Setup things in the window+ nvim_win_set_option split_win "relativenumber" $ ObjectBool False+ nvim_win_set_option split_win "number" $ ObjectBool False++ resizeInfoWin split_win (InfoBuffer split_buf)++ pure split_win++resizeInfoWin :: Window -> InfoBuffer -> Neovim CornelisEnv ()+resizeInfoWin w ib = do+ t <- nvim_buf_get_lines (iw_buffer ib) 0 (-1) False+ max_size <- asks $ cc_max_height . ce_config+ let size = min max_size $ fromIntegral $ V.length t+ asks (cc_split_location . ce_config) >>= \case+ Vertical -> pure ()+ Horizontal -> window_set_height w size+ OnLeft -> pure ()+ OnRight -> pure ()+ OnTop -> window_set_height w size+ OnBottom -> window_set_height w size++++writeInfoBuffer :: Int64 -> InfoBuffer -> Doc HighlightGroup -> Neovim env ()+writeInfoBuffer ns iw doc = do+ -- TODO(sandy): Bad choice for a window, but good enough?+ w <- nvim_get_current_win+ width <- window_get_width w++ let sds = layoutPretty (LayoutOptions (AvailablePerLine (fromIntegral width) 0.8)) doc+ (hls, sds') = renderWithHlGroups sds+ s = T.lines $ renderStrict sds'++ let b = iw_buffer iw+ nvim_buf_set_option b "modifiable" $ ObjectBool True+ buffer_set_lines b 0 (-1) True $ V.fromList s++ for_ (concatMap spanInfoHighlights hls) $ \(InfoHighlight (l, sc) ec hg) ->+ nvim_buf_add_highlight+ b ns+ (T.pack $ show hg)+ l sc ec+ nvim_buf_set_option b "modifiable" $ ObjectBool False+
+ src/Cornelis/Offsets.hs view
@@ -0,0 +1,235 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TypeFamilies #-}++-- | Strongly typed indices and offsets.+--+-- The goal of this module is to make it as easy as possible to keep track+-- of the various indexing schemes used by functions in the nvim API.+--+-- The core abstraction is the type 'Index' tagged with the sort of things it+-- is indexing (@Byte@, @CodePoint@, @Line@) and whether things are 0-indexed+-- or 1-indexed.+--+-- Two constructors and two destructors are provided: 'toZeroIndexed',+-- 'toOneIndexed', 'fromZeroIndexed', and 'fromOneIndexed'. They should only+-- be used to make external API calls, to unwrap input indices and to wrap+-- output indices. The names of those functions are self-documenting, indicating+-- the indexing scheme used by every index that goes in and out of the external+-- API.+--+-- Within Cornelis, indices remain typed at all times, using dedicated functions+-- to convert between 0/1-indexing ('zeroIndex', 'oneIndex') and between+-- @Byte@ and @CodePoint@ indexing ('toByte', 'fromByte').+--+-- Usually, indices are relative to a common origin (beginning of the same buffer+-- or line), so it doesn't make sense to add them. There is a separate type of+-- 'Offset' which can be added to indices using the operator @('.+')@.+-- And @('.-.')@ gives the offset between two indices.+--+-- @+-- i :: Index 'Byte 'ZeroIndexed+-- i .+ Offset 42 :: Index 'Byte 'ZeroIndexed+-- @+--+-- Types of 'Pos'isitions (pairs of line and column indices) and 'Interval's+-- (pairs of positions or indices) are also provided, and should be used+-- as much as possible to reduce the likelihood of mixing up indices.+--+-- When talking about 'Pos', "(i,j)-indexed" means "i-indexed lines, j-indexed+-- columns".+--+-- Agda's indexing scheme (codepoints, (1,1)-indexed) is the preferred one+-- (0- vs 1-indexing is heavily checked, so it doesn't matter much which+-- we choose; codepoint indexing is preferred for manipulating unicode text+-- (fewer invalid states than byte indexing)).+--+-- A secondary indexing scheme is bytes, (0,0)-indexed, used as a unified+-- low-level representation right before talking to the nvim API.+module Cornelis.Offsets+ ( Index()+ , Indexing(..)+ , Unit(..)+ , Offset(..)+ , Pos(..)+ , Interval(..)+ , LineNumber+ , AgdaIndex+ , AgdaOffset+ , AgdaPos+ , AgdaInterval+ , VimIndex+ , VimOffset+ , VimPos+ , VimInterval+ , toZeroIndexed+ , toOneIndexed+ , fromZeroIndexed+ , fromOneIndexed+ , zeroIndex+ , oneIndex+ , incIndex+ , (.+)+ , (.-.)+ , offsetPlus+ , textToBytes+ , charToBytes+ , toBytes+ , fromBytes+ , containsPoint+ , addCol+ ) where++import Data.Aeson (FromJSON)+import qualified Data.ByteString as BS+import Data.Coerce (coerce)+import Data.Monoid (Sum(..))+import qualified Data.Text as T+import Data.Text.Encoding (encodeUtf8)+import GHC.Generics (Generic)+import GHC.Stack (HasCallStack)+import GHC.Show (showSpace)+import Prettyprinter (Pretty)+import qualified DiffLoc as D++-- | Indexing scheme: whether the first index is zero or one.+data Indexing = OneIndexed | ZeroIndexed++-- | What are we counting?+data Unit = Byte | CodePoint | Line++-- | The constructor is hidden, use 'toZeroIndexed' and 'toOneIndexed' to construct it,+-- and 'fromZeroIndexed' and 'fromOneIndexed' to destruct it.+newtype Index (e :: Unit) (i :: Indexing) = Index Int+ deriving newtype (Eq, Ord, Show, Read, FromJSON, Pretty)++type role Index nominal nominal++-- | It doesn't seem worth the trouble to hide this constructor.+newtype Offset (e :: Unit) = Offset Int+ deriving newtype (Eq, Ord, Show, Read, FromJSON, Pretty)+ deriving (Semigroup, Monoid) via Sum Int++type role Offset nominal++-- | Position in a text file as line-column numbers. This type is indexed by+-- the units of the columns (@Byte@ or @CodePoint@) and by the indexing scheme+-- of lines and columns.+data Pos e i j = Pos+ { p_line :: Index 'Line i+ , p_col :: Index e j+ } deriving (Eq, Ord, Generic)++instance Show (Pos e i j) where+ showsPrec n (Pos l c) =+ showParen (n >= 11) $ showString "Pn () 0 " . showsPrec 11 l . showSpace . showsPrec 11 c++data Interval p = Interval { iStart, iEnd :: !p }+ deriving (Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Show p => Show (Interval p) where+ showsPrec n (Interval s e) =+ showParen (n >= 11) $ showString "Interval " . showsPrec 11 s . showSpace . showsPrec 11 e++-- Common specializations++type LineNumber = Index 'Line++type AgdaIndex = Index 'CodePoint 'OneIndexed+type AgdaOffset = Offset 'CodePoint+type AgdaPos = Pos 'CodePoint 'OneIndexed 'OneIndexed+type AgdaInterval = Interval AgdaPos++type VimIndex = Index 'Byte 'ZeroIndexed+type VimOffset = Offset 'Byte+type VimPos = Pos 'Byte 'ZeroIndexed 'ZeroIndexed+type VimInterval = Interval VimPos++-- To pass indices to and from external sources.++-- | Mark a raw index as zero-indexed.+toZeroIndexed :: Integral a => a -> Index e 'ZeroIndexed+toZeroIndexed a = Index (fromIntegral a)++-- | Mark a raw index as one-indexed.+toOneIndexed :: Integral a => a -> Index e 'OneIndexed+toOneIndexed a = Index (fromIntegral a)++-- | Unwrap a raw zero-indexed index.+fromZeroIndexed :: Num a => Index e 'ZeroIndexed -> a+fromZeroIndexed (Index a) = fromIntegral a++-- | Unwrap a raw zero-indexed index.+fromOneIndexed :: Num a => Index e 'OneIndexed -> a+fromOneIndexed (Index a) = fromIntegral a++-- | Convert from one- to zero-indexed.+zeroIndex :: Index e 'OneIndexed -> Index e 'ZeroIndexed+zeroIndex (Index i) = Index (i - 1)++-- | Convert from zero- to one-indexed.+oneIndex :: Index e 'ZeroIndexed -> Index e 'OneIndexed+oneIndex (Index i) = Index (i + 1)++-- | Increment index.+incIndex :: Index e i -> Index e i+incIndex (Index i) = Index (i + 1)++-- | Add an offset to an index.+(.+) :: Index e i -> Offset e -> Index e i+Index i .+ Offset n = Index (i + n)++(.-.) :: Index e i -> Index e i -> Offset e+Index i .-. Index j = Offset (i - j)++--++offsetPlus :: Offset a -> Offset a -> Offset a+offsetPlus = coerce $ (+) @Int++--++containsPoint :: Ord p => Interval p -> p -> Bool+containsPoint (Interval s e) p = s <= p && p < e++-- | Number of bytes in a 'T.Text'.+textToBytes :: T.Text -> Int+textToBytes t = BS.length (encodeUtf8 t)++-- | Number of bytes in a 'Char'.+charToBytes :: Char -> Int+charToBytes c = textToBytes (T.singleton c)++------------------------------------------------------------------------------+-- | Convert a character-based index into a byte-indexed one+toBytes :: T.Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed+toBytes s (Index i) = Index $ textToBytes $ T.take (fromIntegral i) s++------------------------------------------------------------------------------+-- | Convert a byte-based index into a character-indexed one.+fromBytes :: HasCallStack => T.Text -> Index 'Byte 'ZeroIndexed -> Index 'CodePoint 'ZeroIndexed+fromBytes t (Index i) | i < 0 = error $ "from bytes underflow" <> show (t, i)+fromBytes _ (Index 0) = Index 0+fromBytes t (Index i) | Just (c, str) <- T.uncons t =+ let diff = BS.length $ encodeUtf8 $ T.singleton c+ in case i - diff >= 0 of+ True -> Index $ 1 + coerce (fromBytes str (Index (i - diff)))+ -- We ran out of bytes in the middle of a multibyte character. Just+ -- return the one we're on, and don't underflow!+ False -> Index 0+fromBytes t i = error $ "missing bytes: " <> show (t, i)++addCol :: Pos e i j -> Offset e -> Pos e i j+addCol (Pos l c) dc = Pos l (c .+ dc)++-- | Ordered monoid action of offsets on indices.+instance D.Amor (Index e i) where+ type Trans (Index e i) = Offset e+ (.+) = (Cornelis.Offsets..+)+ i .-.? j | i >= j = Just (i .-. j)+ | otherwise = Nothing++-- | The zero in zero-indexing.+instance D.Origin (Index e 'ZeroIndexed) where+ origin = toZeroIndexed (0 :: Int)
+ src/Cornelis/Pretty.hs view
@@ -0,0 +1,248 @@+{-# LANGUAGE OverloadedStrings #-}++module Cornelis.Pretty where++import Cornelis.Offsets (AgdaPos, Pos(..), Interval(..), AgdaInterval, charToBytes, textToBytes)+import qualified Cornelis.Types as C+import qualified Cornelis.Types as X+import Cornelis.Types hiding (Type)+import Data.Bool (bool)+import Data.Function (on)+import Data.Int+import Data.List (sortOn, groupBy, intersperse)+import qualified Data.Map as M+import Data.Maybe (maybeToList, fromMaybe, fromJust)+import Data.Semigroup (stimes)+import qualified Data.Text as T+import Prettyprinter+import Prettyprinter.Internal.Type+++-- | Custom highlight groups set by the plugin.+--+-- These groups linked to Neovim default highlight groups in @syntax/agda.vim@.+--+-- The suffix after @Cornelis/XXX/@ matches the names as returned by Agda, contained in 'C.hl_atoms'.+-- How these names are generated is not documented on Agda's side, but the implementation can be found at+-- ['Agda.Interaction.Highlighting.Common.toAtoms'](https://github.com/agda/agda/src/full/Agda/Interaction/Highlighting/Common.hs).+-- The correspoding Agda types are found in 'Agda.Interaction.Highlighting.Precise'.+--+-- NOTE:+-- * When modifying this type, remember to sync the changes to @syntax/agda.vim@+-- * This list of highlight groups does not yet cover all variants returned by Agda+data HighlightGroup+ = CornelisError -- ^ InfoWin highlight group of error messages+ | CornelisErrorWarning -- ^ InfoWin highlight group of warnings considered fatal+ | CornelisWarn -- ^ InfoWin highlight group of warnings+ | CornelisTitle -- ^ InfoWin highlight of section titles+ | CornelisName -- ^ InfoWin highlight of names in context+ | CornelisHole -- ^ An open hole (@{! /.../ !}@ and @?@)+ | CornelisUnsolvedMeta -- ^ An unresolved meta variable+ | CornelisUnsolvedConstraint -- ^ An unresolved constraint+ | CornelisKeyword -- ^ An Agda keywords (@where@, @let@, etc.)+ | CornelisSymbol -- ^ A symbol, not part of an identifier (@=@, @:@, @{@, etc.)+ | CornelisType -- ^ A datatype (@Nat@, @Bool@, etc.)+ | CornelisPrimitiveType -- ^ A primitive/builtin Agda type+ | CornelisRecord -- ^ A datatype, defined as a @record@+ | CornelisFunction -- ^ A function, e.g. a top-level declaration+ | CornelisArgument -- ^ The name of an (implicit) argument, i.e. @Foo {/bar/ = 42}@+ | CornelisBound -- ^ A bound identifier, e.g. a variable in a pattern clause or a module parameter+ | CornelisOperator -- ^ A mixfix operator, e.g. @x /∷/ xs@.+ | CornelisField -- ^ Field of a record definition+ | CornelisGeneralizable -- ^ A generalizable variable, defined for example in a @variable@ block+ | CornelisMacro -- ^ A macro, defined in a @macro@ block+ | CornelisInductiveConstructor -- ^ A constructor of an inductive data type (e.g. @data Foo /.../@)+ | CornelisCoinductiveConstructor -- ^ A constructor for a /co/inductive datatype, i.e. a record marked @coinductive@+ | CornelisNumber -- ^ A number literal+ | CornelisComment -- ^ A comment+ | CornelisString -- ^ A string literal+ | CornelisCatchAllClause -- ^ "Catch-all clause". Some sort of fallback; not exactly clear where this is used+ | CornelisTypeChecks -- ^ A location being type-checked right now+ | CornelisModule -- ^ A module name, e.g. in a @module@ block or an @import@+ | CornelisPostulate -- ^ A term, defined in a @postulate@ block+ | CornelisPrimitive -- ^ An Agda primitive, e.g. @Set@+ | CornelisPragma -- ^ The argument to a pragma, e.g. @{-# OPTIONS /--foo/ -#}@+ deriving (Eq, Ord, Show, Read, Enum, Bounded)++-- | Priority of the HighlightGroup. See `:h vim.highlight.priorities` for more information.+--+-- 100 is the default syntax highlighting priority, while 150 is reserved for diagnostics.+priority :: HighlightGroup -> Int64+priority CornelisError = 150+priority CornelisErrorWarning = 150+priority CornelisWarn = 150+priority CornelisUnsolvedMeta = 150+priority CornelisUnsolvedConstraint = 150+priority _ = 100++atomToHlGroup :: Text -> Maybe HighlightGroup+atomToHlGroup atom = M.lookup atom allHlGroups where+ stripCornelis = fromJust . T.stripPrefix "Cornelis"++ toAtomName :: HighlightGroup -> Text+ toAtomName hlGroup = T.toLower $ stripCornelis $ T.pack $ show hlGroup++ allHlGroups :: M.Map Text HighlightGroup+ allHlGroups = M.fromList $+ map (\g -> (toAtomName g, g)) [(minBound :: HighlightGroup) ..]++data InfoHighlight a = InfoHighlight+ { ihl_start :: (Int64, Int64)+ , ihl_end :: a+ , ihl_group :: HighlightGroup+ }+ deriving (Eq, Ord, Show, Functor)++spanInfoHighlights+ :: InfoHighlight (Int64, Int64)+ -> [InfoHighlight Int64]+spanInfoHighlights ih@(InfoHighlight (sl, sc) (el, ec) hg)+ | sl == el = pure $ fmap snd ih+ | otherwise+ = InfoHighlight (sl, sc) (-1) hg+ : InfoHighlight (el, 0) ec hg+ : fmap (\l -> InfoHighlight (l, 0) (-1) hg) [sl + 1 .. el - 1]+++renderWithHlGroups+ :: SimpleDocStream HighlightGroup+ -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)+renderWithHlGroups = go [] 0 0+ where+ go+ :: [InfoHighlight ()]+ -> Int64+ -> Int64+ -> SimpleDocStream HighlightGroup+ -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)+ go _ _ _ SFail = pure SFail+ go _ _ _ SEmpty = pure SEmpty+ go st r c (SChar c' sds) =+ SChar c' <$> go st r (c + fromIntegral (charToBytes c')) sds+ go st r c (SText n txt sds) =+ SText n txt <$> go st r (c + fromIntegral (textToBytes txt)) sds+ go st r _ (SLine n sds) = SLine n <$> go st (r + 1) (fromIntegral n) sds+ go st r c (SAnnPush hg sds) = go (InfoHighlight (r, c) () hg : st) r c sds+ go [] _ _ (SAnnPop _) = error "popping an annotation that doesn't exist"+ go (ih : ihs) r c (SAnnPop sds) = do+ sds' <- go ihs r c sds+ ([(r, c) <$ ih], sds')+++prettyType :: C.Type -> Doc HighlightGroup+prettyType (C.Type ty) = annotate CornelisType $ sep $ fmap pretty $ T.lines ty+++groupScopeSet :: [InScope] -> [[InScope]]+groupScopeSet+ = sortOn (is_refied_name . head)+ . fmap (sortOn is_refied_name)+ . groupBy (on (==) is_type)+ . sortOn is_type++prettyGoals :: DisplayInfo -> Doc HighlightGroup+prettyGoals (AllGoalsWarnings vis invis errs warns) =+ vcat $ punctuate hardline $ filter (not . isEmpty)+ [ section "Warnings" warns $ annotate CornelisWarn . pretty . getMessage+ , section "Visible Goals" vis $+ prettyGoal . fmap (mappend "?" . T.pack . show . ip_id)+ , section "Errors" errs prettyError+ , section "Invisible Goals" invis $ \gi ->+ prettyGoal (fmap np_name gi)+ <+> maybe mempty (brackets . ("at" <+>) . prettyInterval) (np_interval $ gi_ip gi)+ ]+prettyGoals (GoalSpecific _ scoped ty mhave mboundary mconstraints) =+ vcat $ intersperse (stimes @_ @Int 60 "—") $+ [ section "Boundary" (fromMaybe [] mboundary) pretty+ ] <>+ [ annotate CornelisTitle "Goal:" <+> prettyType ty+ ] <>+ [ annotate CornelisTitle "Have:" <+> prettyType have+ | have <- maybeToList mhave+ ] <>+ [ vcat $ fmap prettyInScopeSet $ groupScopeSet scoped+ ] <>+ [ section "Constraints" (fromMaybe [] mconstraints) pretty+ ]+prettyGoals (HelperFunction sig) =+ section "Helper Function"+ [ mempty+ , annotate CornelisType $ pretty sig+ , mempty+ , annotate CornelisComment $ parens "copied to \" register"+ ] id+prettyGoals (InferredType ty) =+ annotate CornelisTitle "Inferred Type:" <+> prettyType ty+prettyGoals (WhyInScope msg) = pretty msg+prettyGoals (NormalForm expr) = pretty expr+prettyGoals (DisplayError err) = annotate CornelisError $ pretty err+prettyGoals (UnknownDisplayInfo v) = annotate CornelisError $ pretty $ show v++prettyInterval :: AgdaInterval -> Doc HighlightGroup+prettyInterval (Interval s e)+ | p_line s == p_line e+ = prettyPoint s <> "-" <> pretty (p_col e)+ | otherwise+ = prettyPoint s <> "-" <> prettyPoint e++prettyPoint :: AgdaPos -> Doc HighlightGroup+prettyPoint p = pretty (p_line p) <> "," <> pretty (p_col p)+++isEmpty :: Doc HighlightGroup -> Bool+isEmpty Empty = True+isEmpty _ = False+++section+ :: Doc HighlightGroup+ -> [a]+ -> (a -> Doc HighlightGroup)+ -> Doc HighlightGroup+section _ [] _ = mempty+section doc as f = vcat $+ annotate CornelisTitle (doc <> ":") : fmap f as+++prettyName :: Text -> Doc HighlightGroup+prettyName = prettyVisibleName True+++prettyVisibleName :: Bool -> Text -> Doc HighlightGroup+prettyVisibleName False t = annotate CornelisComment $ "(" <> pretty t <> ")"+prettyVisibleName True t = annotate CornelisName $ pretty t++prettyInScope :: InScope -> Doc HighlightGroup+prettyInScope (InScope reified _ in_scope ty) =+ hsep+ [ prettyGoal $ GoalInfo reified ty+ , bool+ (pretty (replicate 6 ' ') <+> annotate CornelisComment (parens "not in scope"))+ mempty+ in_scope+ ]++prettyInScopeSet :: [InScope] -> Doc HighlightGroup+prettyInScopeSet is =+ let ty = is_type $ head is+ in prettyManyGoals is ty++prettyManyGoals :: [InScope] -> X.Type -> Doc HighlightGroup+prettyManyGoals is ty =+ hang 4 $ sep+ [ hsep $+ fmap (\i -> prettyVisibleName (is_in_scope i) $ is_refied_name i) is <> [":"]+ , prettyType ty+ ]++prettyGoal :: GoalInfo Text -> Doc HighlightGroup+prettyGoal (GoalInfo name ty) =+ hang 4 $ sep+ [ prettyName name <+> ":"+ , prettyType ty+ ]++prettyError :: Message -> Doc HighlightGroup+prettyError (Message msg) =+ let (hdr, body) = fmap (T.drop 1) $ T.break (== '\n') msg in+ vcat [ annotate CornelisError (pretty hdr) , pretty body ]
+ src/Cornelis/Subscripts.hs view
@@ -0,0 +1,130 @@+module Cornelis.Subscripts where++import Cornelis.Offsets+import Cornelis.Vim (getWindowCursor, getBufferLine, replaceInterval, setWindowCursor, reportError)+import Data.Foldable (asum, foldl', for_)+import Data.Map (Map)+import qualified Data.Map as M+import Data.Maybe (fromMaybe)+import Data.Proxy+import qualified Data.Text as T+import Data.Void (Void)+import Neovim (Neovim)+import Neovim.API.Text (vim_get_current_window, window_get_buffer)+import Text.Megaparsec++type Parser = Parsec Void T.Text+++data Flavor a+ = Digits a+ | Subscript a+ | Superscript a+ deriving (Eq, Ord, Show, Functor)++extract :: Flavor a -> a+extract (Digits a) = a+extract (Subscript a) = a+extract (Superscript a) = a++parseNum :: Num a => Flavor (Char, String) -> Parser (Flavor a)+parseNum f = do+ r <- option id (negate <$ satisfy (== fst (extract f)) ) <*> parseDigits (fmap snd f)+ pure $ r <$ f+++parseDigits :: Num a => Flavor String -> Parser a+parseDigits fv = mkNum <$> takeWhile1P (Just "digit") (flip elem $ extract fv)+ where+ mkNum = foldl' step 0 . chunkToTokens (Proxy :: Proxy T.Text)+ step a c = a * 10 + fromIntegral (digitToInt fv c)+++digitToInt :: Flavor String -> Char -> Int+digitToInt fv+ = fromMaybe (error "digitToInt: not a digit")+ . flip lookup (zip (extract fv) [0..])+++subscripts :: Flavor (Char, String)+subscripts = Subscript ('₋', "₀₁₂₃₄₅₆₇₈₉")+++superscripts :: Flavor (Char, String)+superscripts = Superscript ('⁻', "⁰¹²³⁴⁵⁶⁷⁸⁹")+++digits :: Flavor (Char, String)+digits = Digits ('-', "0123456789")+++mkReplacement :: (Char, String) -> (Char, String) -> Map Char Char+mkReplacement (m1, s1) (m2, s2) = M.fromList $ zip (m1 : s1) (m2 : s2)+++replace :: Map Char Char -> String -> String+replace m = fmap (\c -> fromMaybe c $ M.lookup c m)+++parseFlavor :: Parser (Flavor Int)+parseFlavor = asum+ [ parseNum digits+ , parseNum superscripts+ , parseNum subscripts+ ]++parseLine :: Parser (String, Flavor Int)+parseLine = manyTill_ anySingle $ try parseFlavor+++unparse :: Flavor Int -> String+unparse (Digits n) = unparseWith (extract digits) n+unparse (Subscript n) = unparseWith (extract subscripts) n+unparse (Superscript n) = unparseWith (extract superscripts) n++unparseWith :: (Char, String) -> Int -> String+unparseWith to n =+ let from = extract digits+ rep = mkReplacement from to+ in replace rep $ show n+++applyOver :: (Int -> Int) -> Parser (T.Text, (Int, Int))+applyOver f = do+ (start_str, fv) <- parseLine+ let n = unparse $ fmap f fv+ start = T.pack start_str+ pure+ ( T.pack n+ , (T.length start, length $ show $ extract fv)+ )+++incNextDigitSeq :: Neovim env ()+incNextDigitSeq = overNextDigitSeq (+1)+++decNextDigitSeq :: Neovim env ()+decNextDigitSeq = overNextDigitSeq (subtract 1)+++overNextDigitSeq :: (Int -> Int) -> Neovim env ()+overNextDigitSeq f = do+ w <- vim_get_current_window+ b <- window_get_buffer w+ Pos line col <- getWindowCursor w+ txt <- getBufferLine b (zeroIndex line)+ let later = T.drop (fromZeroIndexed (zeroIndex col)) txt++ reportError $ T.pack $ show later+ for_ (parse (applyOver f) "" later) $ \(result, (before, target)) -> do+ reportError result+ let start_col = col .+ Offset before+ end_col = start_col .+ Offset target+ start_pos = Pos line start_col+ end_pos = Pos line end_col++ replaceInterval b (Interval start_pos end_pos) result++ setWindowCursor w start_pos+
+ src/Cornelis/Types.hs view
@@ -0,0 +1,429 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use camelCase" #-}++module Cornelis.Types+ ( module Cornelis.Types+ , InteractionId+ , Buffer+ , Window+ , Text+ , traceMX+ , HasCallStack+ ) where++import Control.Concurrent.Chan.Unagi (InChan)+import Control.Monad.State.Class+import Cornelis.Debug+import Cornelis.Offsets (Pos(..), Interval(..), AgdaIndex, AgdaPos, AgdaInterval, VimIndex, LineNumber, Indexing(..))+import Cornelis.Types.Agda (InteractionId)+import Data.Aeson hiding (Error)+import Data.Char (toLower)+import Data.Functor.Identity+import Data.Generics.Labels ()+import Data.IORef+import Data.IntervalMap.FingerTree (IntervalMap)+import Data.Map (Map)+import Data.Maybe (listToMaybe)+import Data.Text (Text)+import DiffLoc (Diff, Colline)+import GHC.Generics+import GHC.Stack+import Neovim hiding (err)+import Neovim.API.Text (Buffer(..), Window)+import System.Process (ProcessHandle)++deriving stock instance Ord Buffer++data Agda = Agda+ { a_buffer :: Buffer+ , a_ready :: IORef Bool+ , a_req :: InChan String+ , a_hdl :: ProcessHandle+ }+ deriving Generic++data BufferStuff = BufferStuff+ { bs_agda_proc :: Agda+ , bs_ips :: Map InteractionId (InteractionPoint Identity)+ , bs_ip_exts :: Map InteractionId Extmark+ , bs_goto_sites :: Map Extmark DefinitionSite+ , bs_goals :: DisplayInfo+ , bs_info_win :: InfoBuffer+ , bs_code_map :: LineIntervals+ }+ deriving Generic++newtype InfoBuffer = InfoBuffer+ { iw_buffer :: Buffer+ }+ deriving Generic++data CornelisState = CornelisState+ { cs_buffers :: Map Buffer BufferStuff+ , cs_diff :: Map BufferNum Diff0+ }+ deriving Generic++data SplitLocation+ = Vertical+ | Horizontal+ | OnLeft+ | OnRight+ | OnTop+ | OnBottom+ deriving (Eq, Ord, Enum, Bounded)++instance Show SplitLocation where+ show Vertical = "vertical"+ show Horizontal = "horizontal"+ show OnLeft = "left"+ show OnRight = "right"+ show OnTop = "top"+ show OnBottom = "bottom"++readSplitLocation :: String -> Maybe SplitLocation+readSplitLocation s = case fmap toLower s of+ "vertical" -> Just Vertical+ "horizontal" -> Just Horizontal+ "left" -> Just OnLeft+ "right" -> Just OnRight+ "top" -> Just OnTop+ "bottom" -> Just OnBottom+ _ -> Nothing+++data CornelisConfig = CornelisConfig+ { cc_max_height :: Int64+ , cc_max_width :: Int64+ , cc_split_location :: SplitLocation+ }+ deriving (Show, Generic)++data CornelisEnv = CornelisEnv+ { ce_state :: IORef CornelisState+ , ce_stream :: InChan AgdaResp+ , ce_namespace :: Int64+ , ce_config :: CornelisConfig+ }+ deriving Generic++data AgdaResp = AgdaResp+ { ar_buffer :: Buffer+ , ar_message :: Response+ }+ deriving Generic++instance MonadState CornelisState (Neovim CornelisEnv) where+ get = do+ mv <- asks ce_state+ liftIO $ readIORef mv+ put a = do+ mv <- asks ce_state+ liftIO $ writeIORef mv a++data Response+ = DisplayInfo DisplayInfo+ | ClearHighlighting -- TokenBased+ | HighlightingInfo Bool [Highlight]+ | ClearRunningInfo+ | RunningInfo Int Text+ | Status+ { status_checked :: Bool+ , status_showIrrelevant :: Bool+ , status_showImplicits :: Bool+ }+ | JumpToError FilePath AgdaIndex+ | InteractionPoints [InteractionPoint Maybe]+ | GiveAction Text (InteractionPoint (Const ()))+ | MakeCase MakeCase+ | SolveAll [Solution]+ | Unknown Text Value+ deriving (Eq, Ord, Show)++data DefinitionSite = DefinitionSite+ { ds_filepath :: Text+ , ds_position :: AgdaIndex+ }+ deriving (Eq, Ord, Show)++instance FromJSON DefinitionSite where+ parseJSON = withObject "DefinitionSite" $ \obj ->+ DefinitionSite <$> obj .: "filepath" <*> obj .: "position"++data Highlight = Highlight+ { hl_atoms :: [Text]+ , hl_definitionSite :: Maybe DefinitionSite+ , hl_start :: AgdaIndex+ , hl_end :: AgdaIndex+ }+ deriving (Eq, Ord, Show)++instance FromJSON Highlight where+ parseJSON = withObject "Highlight" $ \obj ->+ Highlight+ <$> obj .: "atoms"+ <*> obj .:? "definitionSite"+ <*> fmap (!! 0) (obj .: "range")+ <*> fmap (!! 1) (obj .: "range")++data MakeCase+ = RegularCase MakeCaseVariant [Text] (InteractionPoint Identity)+ deriving (Eq, Ord, Show, Generic)++data MakeCaseVariant = Function | ExtendedLambda+ deriving stock (Eq, Ord, Show, Generic)+ deriving anyclass (FromJSON)++instance FromJSON MakeCase where+ parseJSON = withObject "MakeCase" $ \obj ->+ RegularCase <$> obj .: "variant" <*> obj .: "clauses" <*> obj .: "interactionPoint"+++data Solution = Solution+ { s_ip :: InteractionId+ , s_expression :: Text+ }+ deriving (Eq, Ord, Show)++data InteractionPoint f = InteractionPoint+ { ip_id :: InteractionId+ , ip_intervalM :: f AgdaInterval+ } deriving Generic++deriving instance Eq (f AgdaInterval) => Eq (InteractionPoint f)+deriving instance Ord (f AgdaInterval) => Ord (InteractionPoint f)+deriving instance Show (f AgdaInterval) => Show (InteractionPoint f)++ip_interval' :: InteractionPoint Identity -> AgdaInterval+ip_interval' (InteractionPoint _ (Identity i)) = i++sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity)+sequenceInteractionPoint (InteractionPoint n f) = pure (InteractionPoint n) <*> fmap Identity f+++data NamedPoint = NamedPoint+ { np_name :: Text+ , np_interval :: Maybe AgdaInterval+ }+ deriving (Eq, Ord, Show)++instance FromJSON AgdaInterval where+ parseJSON = withObject "IntervalWithoutFile" $ \obj -> do+ mkInterval <$> obj .: "start" <*> obj .: "end"+ where+ mkInterval (AgdaPos p) (AgdaPos q) = Interval p q++newtype AgdaPos' = AgdaPos AgdaPos++instance FromJSON AgdaPos' where+ parseJSON = withObject "Position" $ \obj -> do+ AgdaPos <$> (Pos <$> obj .: "line" <*> obj .: "col")++instance FromJSON (InteractionPoint Maybe) where+ parseJSON = withObject "InteractionPoint" $ \obj -> do+ InteractionPoint <$> obj .: "id" <*> fmap listToMaybe (obj .: "range")++instance FromJSON (InteractionPoint Identity) where+ parseJSON = withObject "InteractionPoint" $ \obj -> do+ InteractionPoint <$> obj .: "id" <*> fmap head (obj .: "range")++instance FromJSON (InteractionPoint (Const ())) where+ parseJSON = withObject "InteractionPoint" $ \obj -> do+ InteractionPoint <$> obj .: "id" <*> pure (Const ())++instance FromJSON NamedPoint where+ parseJSON = withObject "InteractionPoint" $ \obj -> do+ NamedPoint <$> obj .: "name" <*> fmap listToMaybe (obj .: "range")++instance FromJSON Solution where+ parseJSON = withObject "Solution" $ \obj ->+ Solution <$> obj .: "interactionPoint" <*> obj .: "expression"++data GoalInfo a = GoalInfo+ { gi_ip :: a+ , gi_type :: Type+ }+ deriving (Eq, Ord, Show, Functor)++instance FromJSON a => FromJSON (GoalInfo a) where+ parseJSON = withObject "GoalInfo" $ \obj ->+ (obj .: "kind") >>= \case+ "OfType" -> GoalInfo <$> obj .: "constraintObj" <*> obj .: "type"+ "JustSort" -> GoalInfo <$> obj .: "constraintObj" <*> pure (Type "Sort")+ (_ :: Text) -> empty++newtype Type = Type Text+ deriving newtype (Eq, Ord, Show, FromJSON)++data InScope = InScope+ { is_refied_name :: Text+ , is_original_name :: Text+ , is_in_scope :: Bool+ , is_type :: Type+ }+ deriving (Eq, Ord, Show)++instance FromJSON InScope where+ parseJSON = withObject "InScope" $ \obj ->+ InScope <$> obj .: "reifiedName" <*> obj .: "originalName" <*> obj .: "inScope" <*> obj .: "binding"++newtype Message = Message { getMessage :: Text }+ deriving (Eq, Ord, Show)++instance FromJSON Message where+ parseJSON = withObject "Message" $ \obj ->+ Message <$> obj .: "message"+++data DisplayInfo+ = AllGoalsWarnings+ { di_all_visible :: [GoalInfo (InteractionPoint Identity)]+ , di_all_invisible :: [GoalInfo NamedPoint]+ , di_errors :: [Message]+ , di_warnings :: [Message]+ }+ | GoalSpecific+ { di_ips :: InteractionPoint Identity+ , di_in_scope :: [InScope]+ , di_type :: Type+ , di_type_aux :: Maybe Type+ , di_boundary :: Maybe [Text]+ , di_output_forms :: Maybe [Text]+ }+ | HelperFunction Text+ | InferredType Type+ | DisplayError Text+ | WhyInScope Text+ | NormalForm Text+ | UnknownDisplayInfo Value+ deriving (Eq, Ord, Show, Generic)++newtype TypeAux = TypeAux+ { ta_expr :: Type+ }++instance FromJSON TypeAux where+ parseJSON = withObject "TypeAux" $ \obj ->+ TypeAux . Type <$> obj .: "expr"++instance FromJSON DisplayInfo where+ parseJSON v = flip (withObject "DisplayInfo") v $ \obj ->+ obj .: "kind" >>= \case+ "AllGoalsWarnings" ->+ AllGoalsWarnings+ <$> obj .: "visibleGoals"+ <*> obj .: "invisibleGoals"+ <*> (obj .: "errors" <|> fmap pure (obj .: "errors"))+ <*> (obj .: "warnings" <|> fmap pure (obj .: "warnings"))+ "Error" ->+ obj .: "error" >>= \err ->+ DisplayError <$> err .: "message"+ "InferredType" ->+ InferredType <$> obj .: "expr"+ "WhyInScope" ->+ WhyInScope <$> obj .: "message"+ "NormalForm" ->+ NormalForm <$> obj .: "expr"+ "GoalSpecific" ->+ (obj .: "goalInfo") >>= \info ->+ (info .: "kind") >>= \case+ "HelperFunction" ->+ HelperFunction <$> info .: "signature"+ "GoalType" ->+ GoalSpecific+ <$> obj .: "interactionPoint"+ <*> info .: "entries"+ <*> info .: "type"+ <*> (fmap (fmap ta_expr) (info .: "typeAux") <|> pure Nothing)+ <*> info .:? "boundary"+ <*> info .:? "outputForms"+ "NormalForm" -> NormalForm <$> info .: "expr"+ "InferredType" ->+ InferredType <$> info .: "expr"+ (_ :: Text) ->+ pure $ UnknownDisplayInfo v+ (_ :: Text) -> pure $ UnknownDisplayInfo v++instance FromJSON Response where+ parseJSON v = flip (withObject "Response") v $ \obj -> do+ obj .: "kind" >>= \case+ "MakeCase" ->+ MakeCase <$> parseJSON v+ "ClearRunningInfo" ->+ pure ClearRunningInfo+ "HighlightingInfo" ->+ (obj .: "info") >>= \info ->+ HighlightingInfo <$> info .: "remove" <*> info .: "payload"+ "ClearHighlighting" ->+ pure ClearHighlighting+ "RunningInfo" ->+ RunningInfo <$> obj .: "debugLevel" <*> obj .: "message"+ "InteractionPoints" ->+ InteractionPoints <$> obj .: "interactionPoints"+ "SolveAll" ->+ SolveAll <$> obj .: "solutions"+ "GiveAction" ->+ (obj .: "giveResult") >>= \result ->+ GiveAction <$> result .: "str" <*> obj .: "interactionPoint"+ "DisplayInfo" ->+ DisplayInfo <$> obj .: "info"+ "JumpToError" ->+ JumpToError <$> obj .: "filepath" <*> obj .: "position"+ "Status" -> do+ (obj .: "status" >>=) $ withObject "Status" $ \s ->+ Status <$> s .: "checked"+ <*> (s .: "showIrrelevantArguments"<|> pure False)+ <*> s .: "showImplicitArguments"+ (_ :: Text) -> Unknown <$> obj .: "kind" <*> pure v++newtype Extmark = Extmark Int64+ deriving (Eq, Ord, Show)++data ExtmarkStuff = ExtmarkStuff+ { es_mark :: Extmark+ , es_hlgroup :: Text+ , es_interval :: AgdaInterval+ }+ deriving (Eq, Ord, Show)+++data DebugCommand+ = DumpIPs+ deriving (Eq, Ord, Show, Read, Enum, Bounded)++-- * Translating Agda indices to Vim indices+--+-- Agda sometimes takes a while to process. We want to be able to modify the+-- buffer in the meantime. But then, Agda's highlighting instructions+-- will be out of sync.+--+-- We record the LineIntervals mapping (in field 'bs_code_map') at the time+-- when we reloaded, to translate old AgdaIndex to old VimPos, and then use the+-- 'Diff0' data structure (in field 'cs_diff') to translate (intervals of) old+-- VimPos to new VimPos.++-- | Data for mapping code point indices to byte indices+newtype LineIntervals = LineIntervals+ { li_intervalMap :: IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)+ -- ^ Mapping from positions to line numbers+ } deriving newtype (Semigroup, Monoid)++-- | Buffer update events give us this instead of a proper Buffer+-- There is buffer_get_number :: Buffer -> Neovim env BufferNum+-- but nothing the other way???+type BufferNum = Int64++-- Data structures from the diff-loc library+type DPos = Colline (LineNumber 'ZeroIndexed) VimIndex+type Diff0 = Diff DPos
+ src/Cornelis/Types/Agda.hs view
@@ -0,0 +1,315 @@+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use camelCase" #-}++module Cornelis.Types.Agda where++import Cornelis.Offsets+import Data.Aeson (ToJSON, FromJSON)+import Data.Foldable (toList)+import Data.Sequence+import qualified Data.Sequence as Seq+import Data.Text (Text)+import qualified Data.Text as T+import GHC.Generics+import GHC.Show (showSpace)++data Rewrite = AsIs | Instantiated | HeadNormal | Simplified | Normalised+ deriving (Show, Read, Eq, Ord, Enum, Bounded)+++data ComputeMode = DefaultCompute | HeadCompute | IgnoreAbstract | UseShowInstance+ deriving (Show, Read, Eq, Ord, Enum, Bounded)++data UseForce+ = WithForce -- ^ Ignore additional checks, like termination/positivity...+ | WithoutForce -- ^ Don't ignore any checks.+ deriving (Eq, Read, Show)+++newtype InteractionId = InteractionId { interactionId :: Int }+ deriving newtype+ ( Eq+ , Ord+ , Show+ , Read+ , Num+ , Integral+ , Real+ , Enum+ , ToJSON+ , FromJSON+ )+++-- | IOTCM commands.++type Command = Command' IOTCM++type IntervalWithoutFile = AgdaInterval++data Command' a+ = Command !a+ -- ^ A command.+ | Done+ -- ^ Stop processing commands.+ | Error String+ -- ^ An error message for a command that could not be parsed.+ deriving Show++data Range' a+ = NoRange+ | Range !a (Seq IntervalWithoutFile)+ deriving+ (Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Show a =>+ Show (Range' a) where+ showsPrec _ NoRange+ = showString "noRange"+ showsPrec+ a_a1hOk+ (Cornelis.Types.Agda.Range b1_a1hOl b2_a1hOm)+ = showParen+ (a_a1hOk >= 11)+ ((.)+ (showString "intervalsToRange ")+ ((.)+ (showsPrec 11 b1_a1hOl)+ ((.)+ showSpace (showsPrec 11 $ toList b2_a1hOm))))++type SrcFile = Maybe AbsolutePath++newtype AbsolutePath = AbsolutePath { textPath :: String }+ deriving (Eq, Ord)++instance Show AbsolutePath where+ showsPrec n (AbsolutePath p) =+ showParen (n >= 11) $ showString "mkAbsolute " . showsPrec 11 p++++type Range = Range' SrcFile++type IOTCM = IOTCM' Range+data IOTCM' range+ = IOTCM+ Text+ -- -^ The current file. If this file does not match+ -- 'theCurrentFile, and the 'Interaction' is not+ -- \"independent\", then an error is raised.+ HighlightingLevel+ HighlightingMethod+ (Interaction' range)+ -- -^ What to do+ deriving (Show, Read, Functor, Foldable, Traversable)+++++data Interaction' range+ -- | @cmd_load m argv@ loads the module in file @m@, using+ -- @argv@ as the command-line options.+ = Cmd_load Text [String]++ | Cmd_constraints++ -- | Show unsolved metas. If there are no unsolved metas but unsolved constraints+ -- show those instead.+ | Cmd_metas Rewrite++ -- | Shows all the top-level names in the given module, along with+ -- their types. Uses the top-level scope.+ | Cmd_show_module_contents_toplevel+ Rewrite+ String++ -- | Shows all the top-level names in scope which mention all the given+ -- identifiers in their type.+ | Cmd_search_about_toplevel Rewrite String++ -- | Solve (all goals / the goal at point) whose values are determined by+ -- the constraints.+ | Cmd_solveAll Rewrite+ | Cmd_solveOne Rewrite InteractionId range String++ -- | Solve (all goals / the goal at point) by using Auto.+ | Cmd_autoOne InteractionId range String+ | Cmd_autoAll++ -- | Parse the given expression (as if it were defined at the+ -- top-level of the current module) and infer its type.+ | Cmd_infer_toplevel Rewrite -- Normalise the type?+ String+++ -- | Parse and type check the given expression (as if it were defined+ -- at the top-level of the current module) and normalise it.+ | Cmd_compute_toplevel ComputeMode+ String++ ------------------------------------------------------------------------+ -- Syntax highlighting++ -- | @cmd_load_highlighting_info source@ loads syntax highlighting+ -- information for the module in @source@, and asks Emacs to apply+ -- highlighting info from this file.+ --+ -- If the module does not exist, or its module name is malformed or+ -- cannot be determined, or the module has not already been visited,+ -- or the cached info is out of date, then no highlighting information+ -- is printed.+ --+ -- This command is used to load syntax highlighting information when a+ -- new file is opened, and it would probably be annoying if jumping to+ -- the definition of an identifier reset the proof state, so this+ -- command tries not to do that. One result of this is that the+ -- command uses the current include directories, whatever they happen+ -- to be.+ | Cmd_load_highlighting_info FilePath++ -- | Tells Agda to compute token-based highlighting information+ -- for the file.+ --+ -- This command works even if the file's module name does not+ -- match its location in the file system, or if the file is not+ -- scope-correct. Furthermore no file names are put in the+ -- generated output. Thus it is fine to put source code into a+ -- temporary file before calling this command. However, the file+ -- extension should be correct.+ --+ -- If the second argument is 'Remove', then the (presumably+ -- temporary) file is removed after it has been read.+ | Cmd_tokenHighlighting FilePath Remove++ -- | Tells Agda to compute highlighting information for the expression just+ -- spliced into an interaction point.+ | Cmd_highlight InteractionId range String++ ------------------------------------------------------------------------+ -- Implicit arguments++ -- | Tells Agda whether or not to show implicit arguments.+ | ShowImplicitArgs Bool -- Show them?+++ -- | Toggle display of implicit arguments.+ | ToggleImplicitArgs++ ------------------------------------------------------------------------+ -- Irrelevant arguments++ -- | Tells Agda whether or not to show irrelevant arguments.+ | ShowIrrelevantArgs Bool -- Show them?+++ -- | Toggle display of irrelevant arguments.+ | ToggleIrrelevantArgs++ ------------------------------------------------------------------------+ -- | Goal commands+ --+ -- If the range is 'noRange', then the string comes from the+ -- minibuffer rather than the goal.++ | Cmd_give UseForce InteractionId range String++ | Cmd_refine InteractionId range String++ | Cmd_intro Bool InteractionId range String++ | Cmd_refine_or_intro Bool InteractionId range String++ | Cmd_context Rewrite InteractionId range String++ | Cmd_helper_function Rewrite InteractionId range String++ | Cmd_infer Rewrite InteractionId range String++ | Cmd_goal_type Rewrite InteractionId range String++ -- | Grabs the current goal's type and checks the expression in the hole+ -- against it. Returns the elaborated term.+ | Cmd_elaborate_give+ Rewrite InteractionId range String++ -- | Displays the current goal and context.+ | Cmd_goal_type_context Rewrite InteractionId range String++ -- | Displays the current goal and context /and/ infers the type of an+ -- expression.+ | Cmd_goal_type_context_infer+ Rewrite InteractionId range String++ -- | Grabs the current goal's type and checks the expression in the hole+ -- against it.+ | Cmd_goal_type_context_check+ Rewrite InteractionId range String++ -- | Shows all the top-level names in the given module, along with+ -- their types. Uses the scope of the given goal.+ | Cmd_show_module_contents+ Rewrite InteractionId range String++ | Cmd_make_case InteractionId range String++ | Cmd_compute ComputeMode+ InteractionId range String++ | Cmd_why_in_scope InteractionId range String+ | Cmd_why_in_scope_toplevel String+ -- | Displays version of the running Agda+ | Cmd_show_version+ | Cmd_abort+ -- ^ Abort the current computation.+ --+ -- Does nothing if no computation is in progress.+ | Cmd_exit+ -- ^ Exit the program.+ deriving (Show, Read, Functor, Foldable, Traversable)++type Interaction = Interaction' Range++data HighlightingLevel+ = None+ | NonInteractive+ | Interactive+ -- ^ This includes both non-interactive highlighting and+ -- interactive highlighting of the expression that is currently+ -- being type-checked.+ deriving (Eq, Ord, Show, Read, Generic)++data HighlightingMethod+ = Direct+ -- ^ Via stdout.+ | Indirect+ -- ^ Both via files and via stdout.+ deriving (Eq, Show, Read, Generic)+++data Remove+ = Remove+ | Keep+ deriving (Show, Read)++noRange :: Range' a+noRange = NoRange+++-- | Converts a file name and an interval to a range.+intervalToRange :: a -> IntervalWithoutFile -> Range' a+intervalToRange f i = Range f (Seq.singleton i)+++-- | Turns a file name plus a list of intervals into a range.+--+-- Precondition: 'consecutiveAndSeparated'.+intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a+intervalsToRange _ [] = NoRange+intervalsToRange f is = Range f (Seq.fromList is)++mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range+mkAbsPathRnage = intervalToRange . Just . AbsolutePath . T.unpack+
+ src/Cornelis/Utils.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedStrings #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Cornelis.Utils where++import Control.Concurrent.Async+import Control.Exception (throwIO)+import Control.Lens ((%~))+import Control.Monad.IO.Unlift (MonadUnliftIO(withRunInIO))+import Control.Monad.Reader (withReaderT)+import Control.Monad.State.Class+import Cornelis.Types+import qualified Data.Map as M+import Data.Maybe+import Data.Text.Encoding (decodeUtf8)+import Data.Traversable+import qualified Data.Vector as V+import Neovim hiding (err)+import Neovim.API.Text+import Neovim.Context.Internal (Neovim(..), retypeConfig)++objectToInt :: Num a => Object -> Maybe a+objectToInt (ObjectUInt w) = Just $ fromIntegral w+objectToInt (ObjectInt w) = Just $ fromIntegral w+objectToInt _ = Nothing++objectToText :: Object -> Maybe Text+objectToText (ObjectString w) = Just $ decodeUtf8 w+objectToText _ = Nothing++neovimAsync :: (MonadUnliftIO m) => m a -> m (Async a)+neovimAsync m =+ withRunInIO $ \lower ->+ liftIO $ async $ lower m++savingCurrentPosition :: Window -> Neovim env a -> Neovim env a+savingCurrentPosition w m = do+ c <- window_get_cursor w+ m <* window_set_cursor w c++savingCurrentWindow :: Neovim env a -> Neovim env a+savingCurrentWindow m = do+ w <- nvim_get_current_win+ m <* nvim_set_current_win w++windowsForBuffer :: Buffer -> Neovim env [Window]+windowsForBuffer b = do+ wins <- fmap V.toList vim_get_windows+ fmap catMaybes $ for wins $ \w -> do+ wb <- window_get_buffer w+ pure $ case wb == b of+ False -> Nothing+ True -> Just w++visibleBuffers :: Neovim env [(Window, Buffer)]+visibleBuffers = do+ wins <- fmap V.toList vim_get_windows+ for wins $ \w -> fmap (w, ) $ window_get_buffer w++criticalFailure :: Text -> Neovim env a+criticalFailure err = do+ vim_report_error err+ liftIO $ throwIO $ ErrorResult "critical error" ObjectNil++modifyBufferStuff :: Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()+modifyBufferStuff b f = modify' $! #cs_buffers %~ M.update (Just . f) b++withBufferStuff :: Monoid a => Buffer -> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a+withBufferStuff b f =+ gets (M.lookup b . cs_buffers) >>= \case+ Nothing -> vim_report_error "no buffer stuff!" >> pure mempty+ Just bs -> f bs++withLocalEnv :: env -> Neovim env a -> Neovim env' a+withLocalEnv env (Neovim t) = Neovim $ flip withReaderT t $ retypeConfig env
+ src/Cornelis/Vim.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ViewPatterns #-}++module Cornelis.Vim where++import Control.Lens ((%~), _head, _last, (&))+import Cornelis.Offsets+import Cornelis.Types+import Cornelis.Utils (objectToInt, savingCurrentPosition, savingCurrentWindow)+import Data.Foldable (toList)+import Data.Int+import qualified Data.Map as M+import qualified Data.Text as T+import Data.Text.Encoding (encodeUtf8)+import qualified Data.Vector as V+import Neovim+import Neovim.API.Text+++vimFirstLine :: Int64+vimFirstLine = 0++vimLastLine :: Int64+vimLastLine = -1++getWindowCursor :: Window -> Neovim env AgdaPos+getWindowCursor w = do+ (toOneIndexed -> row, toZeroIndexed -> col) <- window_get_cursor w+ -- window_get_cursor gives us a 1-indexed line, but that is the same way that+ -- lines are indexed.+ let line = zeroIndex row+ b <- window_get_buffer w+ unvimify b (Pos line col)++-- | TODO(sandy): POSSIBLE BUG HERE. MAKE SURE YOU SET THE CURRENT WINDOW+-- BEFORE CALLING THIS FUNCTION+getpos :: Buffer -> Char -> Neovim env AgdaPos+getpos b mark = do+ -- getpos gives us a (1,1)-indexed position!+ ObjectArray [_, objectToInt @Int -> Just (toOneIndexed -> line), objectToInt @Int -> Just (toOneIndexed -> col), _]+ <- vim_call_function "getpos" $ V.fromList [ObjectString $ encodeUtf8 $ T.singleton mark]+ unvimify b (Pos (zeroIndex line) (zeroIndex col))++data SearchMode = Forward | Backward+ deriving (Eq, Ord, Show)++searchpos :: Buffer -> [Text] -> SearchMode -> Neovim env AgdaPos+searchpos b pats dir = do+ -- unlike getpos, these columns are 0 indexed W T F+ ObjectArray [objectToInt @Int -> Just (toOneIndexed -> line), objectToInt @Int -> Just (toZeroIndexed -> col)]+ <- vim_call_function "searchpos" $ V.fromList+ [ ObjectString $ encodeUtf8 $ T.intercalate "\\|" pats+ , ObjectString $ encodeUtf8 $ case dir of+ Forward -> "n"+ Backward -> "bn"+ ]+ unvimify b (Pos (zeroIndex line) col)++setWindowCursor :: Window -> AgdaPos -> Neovim env ()+setWindowCursor w p = do+ b <- window_get_buffer w+ Pos l c <- vimify b p+ window_set_cursor w (fromOneIndexed (oneIndex l), fromZeroIndexed c)++replaceInterval :: Buffer -> Interval AgdaPos -> Text -> Neovim env ()+replaceInterval b ival str+ = do+ Interval (Pos sl sc) (Pos el ec) <- traverse (vimify b) ival+ nvim_buf_set_text b (from0 sl) (from0 sc) (from0 el) (from0 ec) $ V.fromList $ T.lines str+ where+ from0 = fromZeroIndexed++------------------------------------------------------------------------------+-- | Vim insists on returning byte-based offsets for the cursor positions...+-- why the fuck? This function undoes the problem.+unvimify :: Buffer -> VimPos -> Neovim env AgdaPos+unvimify b (Pos line col) = do+ txt <- getBufferLine b line+ let col' = fromBytes txt col+ pure (Pos (oneIndex line) (oneIndex col'))++vimify :: Buffer -> AgdaPos -> Neovim env VimPos+vimify b (Pos (zeroIndex -> line) (zeroIndex -> col)) = do+ txt <- getBufferLine b line+ let col' = toBytes txt col+ pure (Pos line col')++getIndent :: Buffer -> LineNumber 'ZeroIndexed -> Neovim env Int+getIndent b l = do+ txt <- getBufferLine b l+ pure $ T.length $ T.takeWhile (== ' ') txt+++getBufferLine :: Buffer -> LineNumber 'ZeroIndexed -> Neovim env Text+getBufferLine b l = buffer_get_line b (fromZeroIndexed l)++getBufferInterval :: Buffer -> Interval AgdaPos -> Neovim env Text+getBufferInterval b (Interval start end) = do+ Pos sl _ <- vimify b start+ Pos el _ <- vimify b end+ -- nvim_buf_get_lines is exclusive in its end line, thus the plus 1+ ls <- fmap toList $ nvim_buf_get_lines b (from0 sl) (from0 el + 1) False+ pure $ T.unlines $+ ls & _last %~ T.take (from1 (p_col end))+ & _head %~ T.drop (from1 (p_col start))+ where+ from0 = fromZeroIndexed+ from1 = fromZeroIndexed . zeroIndex -- add 1 to a one-indexed arg before passing it to take/drop++reportError :: Text -> Neovim env ()+reportError = vim_report_error++reportInfo :: Text -> Neovim env ()+reportInfo m = vim_out_write $ m <> "\n"++setreg :: Text -> Text -> Neovim env ()+setreg reg val+ = void+ $ vim_call_function "setreg"+ $ V.fromList+ [ ObjectString $ encodeUtf8 reg+ , ObjectString $ encodeUtf8 val+ ]++getExtmarkIntervalById :: Int64 -> Buffer -> Extmark -> Neovim env (Maybe AgdaInterval)+getExtmarkIntervalById ns b (Extmark x) = do+ res+ <- nvim_call_function "nvim_buf_get_extmark_by_id"+ $ V.fromList+ $ b +: ns +: x +: M.singleton @Text "details" True +: []+ case res of+ ObjectArray [ objectToInt @Int -> Just (toZeroIndexed -> sline)+ , objectToInt @Int -> Just (toZeroIndexed -> scol)+ , ObjectMap details+ ] -> do+ let toZ = fmap toZeroIndexed . objectToInt @Int+ Just eline = toZ $ details M.! ObjectString "end_row"+ Just ecol = toZ $ details M.! ObjectString "end_col"+ fmap Just $ traverse (unvimify b) $ Interval (Pos sline scol) $ Pos eline ecol+ _ -> pure Nothing++------------------------------------------------------------------------------+-- | Awful function that does the motion in visual mode and gives you back+-- where vim thinks the @'<@ and @'>@ marks are.+--+-- I'm so sorry.+getSurroundingMotion+ :: Window+ -> Buffer+ -> Text+ -> AgdaPos+ -> Neovim env (AgdaPos, AgdaPos)+getSurroundingMotion w b motion p = do+ savingCurrentWindow $ do+ savingCurrentPosition w $ do+ nvim_set_current_win w+ setWindowCursor w p+ vim_command $ "normal v" <> motion+ start <- getpos b 'v'+ end <- getpos b '.'+ void $ nvim_input "<esc>"+ pure (start, end)++------------------------------------------------------------------------------+-- | Get an interval to replace for a lambda case split+getLambdaClause+ :: Window+ -> Buffer+ -> AgdaInterval+ -> Neovim env AgdaInterval+getLambdaClause w b (Interval p0 p1) = do+ savingCurrentWindow $ do+ savingCurrentPosition w $ do+ nvim_set_current_win w+ setWindowCursor w p0+ start <- searchpos b ["{", ";"] Backward+ setWindowCursor w p1+ end <- searchpos b [";", "}"] Forward+ pure (Interval start end)+
+ src/Lib.hs view
@@ -0,0 +1,233 @@+{-# LANGUAGE NumDecimals #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++module Lib where++import Control.Arrow ((&&&))+import Control.Concurrent.Chan.Unagi+import Control.Lens+import Control.Monad (forever, when)+import Control.Monad.State.Class (gets)+import Cornelis.Config (getConfig)+import Cornelis.Debug (reportExceptions)+import Cornelis.Goals+import Cornelis.Highlighting (highlightBuffer, getLineIntervals, lookupPoint)+import Cornelis.InfoWin+import Cornelis.Offsets+import Cornelis.Subscripts (incNextDigitSeq, decNextDigitSeq)+import Cornelis.Types+import Cornelis.Utils+import Cornelis.Vim+import Data.Foldable (for_)+import Data.IORef (newIORef)+import qualified Data.Map as M+import Data.Maybe+import qualified Data.Text as T+import Neovim+import Neovim.API.Text+import Neovim.Plugin (CommandOption(CmdComplete))+import Plugin+++getInteractionPoint+ :: Buffer+ -> InteractionId+ -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))+getInteractionPoint b i = gets $ preview $ #cs_buffers . ix b . #bs_ips . ix i+++respondToHelperFunction :: DisplayInfo -> Neovim env ()+respondToHelperFunction (HelperFunction sig) = setreg "\"" sig+respondToHelperFunction _ = pure ()+++respond :: Buffer -> Response -> Neovim CornelisEnv ()+-- Update the buffer's goal map+respond b (DisplayInfo dp) = do+ respondToHelperFunction dp+ when (dp & hasn't #_GoalSpecific) $+ modifyBufferStuff b $ #bs_goals .~ dp+ goalWindow b dp+-- Update the buffer's interaction points map+respond b (InteractionPoints ips) = do+ let ips' = mapMaybe sequenceInteractionPoint ips+ modifyBufferStuff b $ #bs_ips .~ M.fromList (fmap (ip_id &&& id) ips')+-- Replace a function clause+respond b (MakeCase mkcase) = do+ doMakeCase b mkcase+ load+-- Replace the interaction point with a result+respond b (GiveAction result ip) = do+ let i = ip_id ip+ getInteractionPoint b i >>= \case+ Nothing -> reportError $ T.pack $ "Can't find interaction point " <> show i+ Just ip' -> do+ int <- getIpInterval b ip'+ replaceInterval b int $ replaceQuestion result+ load+-- Replace the interaction point with a result+respond b (SolveAll solutions) = do+ for_ solutions $ \(Solution i ex) ->+ getInteractionPoint b i >>= \case+ Nothing -> reportError $ T.pack $ "Can't find interaction point " <> show i+ Just ip -> do+ int <- getIpInterval b ip+ replaceInterval b int $ replaceQuestion ex+ load+respond b ClearHighlighting = do+ -- delete what we know about goto positions and stored extmarks+ modifyBufferStuff b $ \bs -> bs+ & #bs_goto_sites .~ mempty+ & #bs_ip_exts .~ mempty+ -- remove the extmarks and highlighting+ ns <- asks ce_namespace+ nvim_buf_clear_namespace b ns 0 (-1)+respond b (HighlightingInfo _remove hl) = do+ extmap <- highlightBuffer b hl+ modifyBufferStuff b $ \bs -> bs+ & #bs_ip_exts <>~ M.compose extmap (fmap ip_interval' $ bs_ips bs)+respond _ (RunningInfo _ x) = reportInfo x+respond _ ClearRunningInfo = reportInfo ""+respond b (JumpToError _ pos) = do+ -- HACK(sandy): See #113. Agda reports error positions in sent messages+ -- relative to the *bytes* attached to the sent interval. But we can't easily+ -- get this when we send intervals. So instead, we just don't jump backwards+ -- if the absolute position is small, because this is indicative that it is+ -- actually a relative position.+ when (fromOneIndexed @Int pos >= 50) $ do+ buf_lines <- nvim_buf_get_lines b 0 (-1) True+ let li = getLineIntervals buf_lines+ case lookupPoint li pos of+ Nothing -> reportError "invalid error report from Agda"+ Just (Pos l c) -> do+ ws <- fmap listToMaybe $ windowsForBuffer b+ for_ ws $ flip window_set_cursor (fromOneIndexed (oneIndex l), fromZeroIndexed c)+respond _ Status{} = pure ()+respond _ (Unknown k _) = reportError k++{-# HLINT ignore doMakeCase "Functor law" #-}+doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()+doMakeCase b (RegularCase Function clauses ip) = do+ int' <- getIpInterval b ip+ let int = int' & #iStart . #p_col .~ toOneIndexed @Int 1+ ins <- getIndent b (zeroIndex (p_line (iStart int)))+ replaceInterval b int+ $ T.unlines+ $ fmap (T.replicate ins " " <>)+ $ fmap replaceQuestion clauses+-- TODO(sandy): It would be nice if Agda just gave us the bounds we're supposed to replace...+doMakeCase b (RegularCase ExtendedLambda clauses ip) = do+ ws <- windowsForBuffer b+ case listToMaybe ws of+ Nothing ->+ reportError+ "Unable to extend a lambda without having a window that contains the modified buffer. This is a limitation in cornelis."+ Just w -> do+ int' <- getIpInterval b ip+ Interval start end+ <- getLambdaClause w b (int' & #iStart . #p_col %~ (.+ Offset (- 1)))+ -- Subtract one so we are outside of a {! !} goal and the i} movement+ -- works correctly+ -- Add an extra character to the start so we leave a space after the+ -- opening brace, and subtract two characters from the end for the space and the }+ replaceInterval b (Interval (start & #p_col %~ (.+ Offset 1)) (end & #p_col %~ (.+ Offset (- 2))))+ $ T.unlines+ $ fmap replaceQuestion clauses & _tail %~ fmap (indent start)+++------------------------------------------------------------------------------+-- | Indent a string with the given offset.+indent :: AgdaPos -> Text -> Text+indent (Pos _ c) s = mconcat+ [ flip T.replicate " " $ fromZeroIndexed (zeroIndex c) - 1+ , "; "+ , s+ ]+++doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()+doPrevGoal = const prevGoal++doNextGoal :: CommandArguments -> Neovim CornelisEnv ()+doNextGoal = const nextGoal+++doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()+doIncNextDigitSeq = const incNextDigitSeq++doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()+doDecNextDigitSeq = const decNextDigitSeq+++cornelisInit :: Neovim env CornelisEnv+cornelisInit = do+ (inchan, outchan) <- liftIO newChan+ ns <- nvim_create_namespace "cornelis"+ mvar <- liftIO $ newIORef $ CornelisState mempty mempty++ cfg <- getConfig++ let env = CornelisEnv mvar inchan ns cfg+ void $ withLocalEnv env $+ neovimAsync $ do+ forever $ reportExceptions $ do+ AgdaResp buffer next <- liftIO $ readChan outchan+ void $ neovimAsync $ reportExceptions $ respond buffer next+ pure env+++-- Flush the TH environment+$(pure [])+++main :: IO ()+main = neovim defaultConfig { plugins = [cornelis] }+++cornelis :: Neovim () NeovimPlugin+cornelis = do+ env <- cornelisInit+ closeInfoWindows++ let rw_complete = CmdComplete "custom,InternalCornelisRewriteModeCompletion"+ cm_complete = CmdComplete "custom,InternalCornelisComputeModeCompletion"+ debug_complete = CmdComplete "custom,InternalCornelisDebugCommandCompletion"++ wrapPlugin $ Plugin+ { environment = env+ , exports =+ [ $(command "CornelisRestart" 'doRestart) [CmdSync Async]+ , $(command "CornelisAbort" 'doAbort) [CmdSync Async]+ , $(command "CornelisLoad" 'doLoad) [CmdSync Async]+ , $(command "CornelisGoals" 'doAllGoals) [CmdSync Async]+ , $(command "CornelisSolve" 'solveOne) [CmdSync Async, rw_complete]+ , $(command "CornelisAuto" 'autoOne) [CmdSync Async]+ , $(command "CornelisTypeInfer" 'doTypeInfer) [CmdSync Async]+ , $(command "CornelisTypeContext" 'typeContext) [CmdSync Async, rw_complete]+ , $(command "CornelisTypeContextInfer" 'typeContextInfer) [CmdSync Async, rw_complete]+ , $(command "CornelisMakeCase" 'doCaseSplit) [CmdSync Async]+ , $(command "CornelisRefine" 'doRefine) [CmdSync Async]+ , $(command "CornelisGive" 'doGive) [CmdSync Async]+ , $(command "CornelisElaborate" 'doElaborate) [CmdSync Async, rw_complete]+ , $(command "CornelisPrevGoal" 'doPrevGoal) [CmdSync Async]+ , $(command "CornelisNextGoal" 'doNextGoal) [CmdSync Async]+ , $(command "CornelisGoToDefinition" 'doGotoDefinition) [CmdSync Async]+ , $(command "CornelisWhyInScope" 'doWhyInScope) [CmdSync Async]+ , $(command "CornelisNormalize" 'doNormalize) [CmdSync Async, cm_complete]+ , $(command "CornelisHelperFunc" 'doHelperFunc) [CmdSync Async, rw_complete]+ , $(command "CornelisQuestionToMeta" 'doQuestionToMeta) [CmdSync Async]+ , $(command "CornelisInc" 'doIncNextDigitSeq) [CmdSync Async]+ , $(command "CornelisDec" 'doDecNextDigitSeq) [CmdSync Async]+ , $(command "CornelisDebug" 'doDebug) [CmdSync Async, debug_complete]+ , $(command "CornelisCloseInfoWindows" 'doCloseInfoWindows) [CmdSync Sync]+ , $(function "InternalCornelisRewriteModeCompletion" 'rewriteModeCompletion) Sync+ , $(function "InternalCornelisComputeModeCompletion" 'computeModeCompletion) Sync+ , $(function "InternalCornelisDebugCommandCompletion" 'debugCommandCompletion) Sync+ , $(function "InternalCornelisNotifyEdit" 'notifyEdit) Async+ ]+ }+
+ src/Plugin.hs view
@@ -0,0 +1,383 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE OverloadedStrings #-}++module Plugin where++import Control.Lens+import Control.Monad ((>=>))+import Control.Monad.State.Class+import Control.Monad.Trans+import Cornelis.Agda (withCurrentBuffer, runIOTCM, withAgda, getAgda)+import Cornelis.Diff (resetDiff, recordUpdate, Replace(..), Colline(..), Vallee(..))+import Cornelis.Goals+import Cornelis.Highlighting (getExtmarks, highlightInterval, updateLineIntervals)+import Cornelis.InfoWin (showInfoWindow, closeInfoWindows)+import Cornelis.Offsets+import Cornelis.Pretty (prettyGoals, HighlightGroup (CornelisHole))+import Cornelis.Types+import Cornelis.Types.Agda hiding (Error)+import Cornelis.Utils+import Cornelis.Vim+import Data.Bool (bool)+import Data.Foldable (for_, fold, toList)+import Data.IORef (IORef, readIORef, atomicModifyIORef)+import Data.List+import qualified Data.Map as M+import Data.Ord+import qualified Data.Text as T+import Data.Traversable (for)+import qualified Data.Vector as V+import Neovim+import Neovim.API.Text+import Neovim.User.Input (input)+import System.Process (terminateProcess)+import Text.Read (readMaybe)+++runInteraction :: Interaction -> Neovim CornelisEnv ()+runInteraction interaction = withCurrentBuffer $ \b -> do+ agda <- getAgda b+ runIOTCM interaction agda+++getDefinitionSites :: Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)+getDefinitionSites b p = withBufferStuff b $ \bs -> do+ marks <- getExtmarks b p+ pure $ flip foldMap marks $ \es ->+ First $ M.lookup (es_mark es) $ bs_goto_sites bs+++doGotoDefinition :: CommandArguments -> Neovim CornelisEnv ()+doGotoDefinition _ = gotoDefinition+++gotoDefinition :: Neovim CornelisEnv ()+gotoDefinition = withAgda $ do+ w <- nvim_get_current_win+ rc <- getWindowCursor w+ b <- window_get_buffer w+ getDefinitionSites b rc >>= \case+ First Nothing -> reportInfo "No syntax under cursor."+ First (Just ds) -> do+ -- TODO(sandy): escape spaces+ vim_command $ "edit " <> ds_filepath ds+ b' <- window_get_buffer w+ contents <- fmap (T.unlines . V.toList) $ buffer_get_lines b' 0 (-1) False+ let buffer_idx = toBytes contents $ zeroIndex $ ds_position ds+ -- TODO(sandy): use window_set_cursor instead?+ vim_command $ "keepjumps normal! " <> T.pack (show buffer_idx) <> "go"+++doLoad :: CommandArguments -> Neovim CornelisEnv ()+doLoad = const load++atomicSwapIORef :: IORef a -> a -> IO a+atomicSwapIORef r x = atomicModifyIORef r (x,)++load :: Neovim CornelisEnv ()+load = withAgda $ withCurrentBuffer $ \b -> do+ agda <- getAgda b+ ready <- liftIO $ readIORef $ a_ready agda+ if ready then do+ vim_command "noautocmd w"+ name <- buffer_get_name $ a_buffer agda+ flip runIOTCM agda $ Cmd_load name []+ buffer_get_number b >>= resetDiff+ updateLineIntervals b+ else vim_report_error "Agda is busy, not ready to load"++questionToMeta :: Buffer -> Neovim CornelisEnv ()+questionToMeta b = withBufferStuff b $ \bs -> do+ let ips = toList $ bs_ips bs++ res <- fmap fold $ for (sortOn (Down . iStart . ip_interval') ips) $ \ip -> do+ int <- getIpInterval b ip+ getGoalContentsMaybe b ip >>= \case+ -- We only don't have a goal contents if we are a ? goal+ Nothing -> do+ replaceInterval b int "{! !}"+ let int' = int { iEnd = iStart int `addCol` Offset 5 }+ void $ highlightInterval b int' CornelisHole+ modifyBufferStuff b $+ #bs_ips %~ M.insert (ip_id ip) (ip & #ip_intervalM . #_Identity .~ int')++ pure $ Any True+ Just _ -> pure $ Any False++ -- Force a save if we replaced any goals+ case getAny res of+ True -> load+ False -> pure ()+++doAllGoals :: CommandArguments -> Neovim CornelisEnv ()+doAllGoals = const allGoals+++allGoals :: Neovim CornelisEnv ()+allGoals =+ withAgda $ withCurrentBuffer $ \b ->+ withBufferStuff b $ \bs -> do+ goalWindow b $ bs_goals bs+++doRestart :: CommandArguments -> Neovim CornelisEnv ()+doRestart _ = do+ bs <- gets cs_buffers+ modify $ #cs_buffers .~ mempty+ liftIO $ for_ bs $ terminateProcess . a_hdl . bs_agda_proc++doAbort :: CommandArguments -> Neovim CornelisEnv ()+doAbort _ = withAgda $ withCurrentBuffer $ getAgda >=> runIOTCM Cmd_abort++normalizationMode :: Neovim env Rewrite+normalizationMode = pure HeadNormal++computeMode :: Neovim env ComputeMode+computeMode = pure DefaultCompute++solveOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+solveOne _ ms = withNormalizationMode ms $ \mode ->+ withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ flip runIOTCM agda $+ Cmd_solveOne+ mode+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ ""++autoOne :: CommandArguments -> Neovim CornelisEnv ()+autoOne _ = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ t <- getGoalContents b ip+ fp <- buffer_get_name b+ flip runIOTCM agda $+ Cmd_autoOne+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ (T.unpack t)++withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()+withNormalizationMode Nothing f = normalizationMode >>= f+withNormalizationMode (Just s) f =+ case readMaybe s of+ Nothing -> reportError $ "Invalid normalization mode: " <> T.pack s+ Just nm -> f nm++withComputeMode :: Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()+withComputeMode Nothing f = computeMode >>= f+withComputeMode (Just s) f =+ case readMaybe s of+ Nothing -> reportError $ "Invalid compute mode: "+ <> T.pack s+ <> ", expected one of "+ <> T.pack (show [(minBound :: ComputeMode) .. ])+ (Just cm) -> f cm++typeContext :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+typeContext _ ms = withNormalizationMode ms $ \mode ->+ withAgda $ void $ withGoalAtCursor $ \b goal -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ flip runIOTCM agda $+ Cmd_goal_type_context+ mode+ (ip_id goal)+ (mkAbsPathRnage fp $ ip_interval' goal)+ ""++typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+typeContextInfer _ ms = withNormalizationMode ms $ \mode ->+ withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ contents <- getGoalContents b ip+ flip runIOTCM agda+ $ Cmd_goal_type_context_infer+ mode+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ $ T.unpack contents++doRefine :: CommandArguments -> Neovim CornelisEnv ()+doRefine = const refine++refine :: Neovim CornelisEnv ()+refine = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ t <- getGoalContents b ip+ flip runIOTCM agda+ $ Cmd_refine_or_intro+ True+ (ip_id ip)+ -- We intentionally don't pass the range here; since doing so changes+ -- the response from Agda and requires a different codepath to perform+ -- the necessary edits.+ noRange+ $ T.unpack t++doGive :: CommandArguments -> Neovim CornelisEnv ()+doGive = const give++give :: Neovim CornelisEnv ()+give = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ t <- getGoalContents b ip+ flip runIOTCM agda+ $ Cmd_give+ WithoutForce+ (ip_id ip)+ -- We intentionally don't pass the range here; since doing so changes+ -- the response from Agda and requires a different codepath to perform+ -- the necessary edits.+ noRange+ $ T.unpack t++doElaborate :: CommandArguments -> Maybe String-> Neovim CornelisEnv ()+doElaborate _ ms = withNormalizationMode ms elaborate++elaborate :: Rewrite -> Neovim CornelisEnv ()+elaborate mode = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ t <- getGoalContents b ip+ flip runIOTCM agda+ $ Cmd_elaborate_give+ mode+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ $ T.unpack t++doTypeInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+doTypeInfer _ ms = withNormalizationMode ms inferType++inferType :: Rewrite -> Neovim CornelisEnv ()+inferType mode = withAgda $ do+ cmd <- withGoalContentsOrPrompt "Infer type of what?"+ (\goal -> pure . Cmd_infer mode (ip_id goal) NoRange)+ (pure . Cmd_infer_toplevel mode)+ runInteraction cmd+++doWhyInScope :: CommandArguments -> Neovim CornelisEnv ()+doWhyInScope _ = do+ thing <- input "Why is what in scope? " Nothing Nothing+ whyInScope thing++whyInScope :: Text -> Neovim CornelisEnv ()+whyInScope thing = do+ withAgda $ void $ withCurrentBuffer $ \b -> do+ agda <- getAgda b+ flip runIOTCM agda $ Cmd_why_in_scope_toplevel $ T.unpack thing++doNormalize :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+doNormalize _ ms = withComputeMode ms $ \mode ->+ withAgda $ void $ do+ (b , goal) <- getGoalAtCursor+ agda <- getAgda b+ fp <- buffer_get_name b+ case goal of+ Nothing -> do+ thing <- input "Normalize what? " Nothing Nothing+ flip runIOTCM agda $ Cmd_compute_toplevel mode thing+ Just ip -> do+ t <- getGoalContents b ip+ flip runIOTCM agda+ $ Cmd_compute+ mode+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ $ T.unpack t++helperFunc :: Rewrite -> Text -> Neovim CornelisEnv ()+helperFunc mode expr = do+ withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ flip runIOTCM agda+ $ Cmd_helper_function+ mode+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ $ T.unpack expr++doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()+doHelperFunc _ ms = withNormalizationMode ms $ \mode -> do+ expr <- input "Expression: " Nothing Nothing+ helperFunc mode expr++doCaseSplit :: CommandArguments -> Neovim CornelisEnv ()+doCaseSplit _ = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ contents <- fmap T.strip $ getGoalContents b ip+ thing <- bool (pure contents)+ (input @Text "Split on what?" Nothing Nothing)+ $ T.null contents+ caseSplit thing++caseSplit :: Text -> Neovim CornelisEnv ()+caseSplit thing = withAgda $ void $ withGoalAtCursor $ \b ip -> do+ agda <- getAgda b+ fp <- buffer_get_name b+ flip runIOTCM agda+ $ Cmd_make_case+ (ip_id ip)+ (mkAbsPathRnage fp $ ip_interval' ip)+ $ T.unpack thing++doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()+doQuestionToMeta _ = withCurrentBuffer questionToMeta++goalWindow :: Buffer -> DisplayInfo -> Neovim CornelisEnv ()+goalWindow b = showInfoWindow b . prettyGoals++computeModeCompletion :: String -> String -> Int -> Neovim env String+computeModeCompletion _ _ _ =+ pure $ unlines $ fmap show $ enumFromTo @ComputeMode minBound maxBound++rewriteModeCompletion :: String -> String -> Int -> Neovim env String+rewriteModeCompletion _ _ _ =+ pure $ unlines $ fmap show $ enumFromTo @Rewrite minBound maxBound++debugCommandCompletion :: String -> String -> Int -> Neovim env String+debugCommandCompletion _ _ _ =+ pure $ unlines $ fmap show $ enumFromTo @DebugCommand minBound maxBound+++doDebug :: CommandArguments -> String -> Neovim CornelisEnv ()+doDebug _ str =+ case readMaybe str of+ Just DumpIPs ->+ withAgda $ withCurrentBuffer $ \b -> withBufferStuff b $ \bs -> do+ traceMX "ips" $ bs_ips bs+ traceMX "ipexts" $ bs_ip_exts bs+ Nothing ->+ vim_report_error $ T.pack $ "No matching debug command for " <> show str++-- | The @on_bytes@ callback required by @nvim_buf_attach@.+notifyEdit+ :: Text -- ^ the string "bytes"+ -> BufferNum -- ^ buffer handle+ -> Bool -- ^ b:changedtick+ -> Int -- ^ start row of the changed text (zero-indexed)+ -> Int -- ^ start column of the changed text+ -> Int -- ^ byte offset of the changed text (from the start of the buffer)+ -> Int -- ^ old end row of the changed text (relative to the start row)+ -> Int -- ^ old end column of the changed text+ -> Int -- ^ old end byte length of the changed text+ -> Int -- ^ new end row of the changed text (relative to the start row)+ -> Int -- ^ new end column of the changed text+ -> Int -- ^ new end byte length of the changed text+ -> Neovim CornelisEnv Bool -- ^ Return True to detach+notifyEdit _ buf _ sr sc _ er ec _ fr fc _ = do+ recordUpdate buf (Replace (pos sr sc) (range er ec) (range fr fc))+ pure False+ where+ pos l c = Colline (toZeroIndexed l) (toZeroIndexed c)+ range l c = Vallee (Offset l) (Offset c)++doCloseInfoWindows :: CommandArguments -> Neovim CornelisEnv ()+doCloseInfoWindows = const closeInfoWindows
+ test/PropertySpec.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-}++module PropertySpec where++import Cornelis.Offsets+import Cornelis.Vim+import Data.Bool (bool)+import Data.Containers.ListUtils (nubOrd)+import Data.Maybe (mapMaybe)+import qualified Data.Text as T+import qualified Data.Vector as V+import Neovim+import Neovim.API.Text+import Neovim.Test (Seconds(Seconds))+import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck+import Utils+++spec :: Spec+spec = parallel $ do+ prop "fromBytes is an inverse of toBytes" $ do+ UnicodeString str <- arbitrary+ let len = length str+ t = T.pack str+ i <- suchThat arbitrary (\x -> 0 <= x && x <= len)+ let off = toZeroIndexed i+ pure+ $ counterexample (show str)+ $ counterexample (show i)+ $ fromBytes t (toBytes t off) === off++ prop "goto gets there" $ do+ n <- choose @Int (1, 50)+ strs <- vectorOf n $ listOf agdaChar+ row <- choose (1, length strs)+ let rowidx = row - 1+ col <- choose (0, max 0 $ length (strs !! rowidx) - 1)+ let pn = Pos (toOneIndexed row) (toOneIndexed col)+ pure+ $ counterexample (show strs)+ $ counterexample (show row)+ $ counterexample (show col)+ $ counterexample (show pn)+ $ counterexample (show $ strs !! rowidx)+ $ withVim (Seconds 1) $ \w b -> do+ buffer_set_lines b 0 (-1) False $ V.fromList $ fmap T.pack strs+ setWindowCursor w pn+ ObjectInt row' <- vim_call_function "line" $ V.fromList [ObjectString "."]+ ObjectInt col' <- vim_call_function "virtcol" $ V.fromList [ObjectString "."]+ liftIO $ Row row' `shouldBe` Row (fromIntegral row)+ -- virtcol is 1-based....+ liftIO $ Col (col' - 1) `shouldBe` Col (fromIntegral col)++ prop "replaceInterval does as it says" $ do+ str <- T.pack <$> listOf agdaChar+ rep <- T.pack <$> listOf agdaChar+ start <- choose (0, T.length str - 1)+ end <- choose (0, T.length str - start)+ let srow = toOneIndexed @Int 1+ scol = toOneIndexed start+ ecol = toOneIndexed (start + end)+ int = Interval (Pos srow scol) (Pos srow ecol)+ expected = T.take start str <> rep <> T.drop (start + end) str+ pure $+ withVim (Seconds 1) $ \_ b -> do+ buffer_set_lines b 0 (-1) False $ V.fromList $ pure str+ intervention b (mapMaybe simplify [Swap str expected]) $+ replaceInterval b int rep+++agdaChar :: Gen Char+agdaChar = elements $ mconcat+ [ [' ' .. '~']+ , ['¡' .. 'ÿ']+ , [ '→', '←', '∧', '∨', '∎', '∘', '⟨', '⟩', '≡', '≢'+ , '∷', '∀', '∃', '≤', '≥', '′', '⊤', '⊥', '≟', '⊛'+ , '×', '⊕', '▹', '∸', '⦃', '⦄', 'ℕ', '⇒', '∈', '₀'+ , '₁', '₂', '₃', '₄', '₅', '₆', '₇', '₈', '₉', '⁰'+ , '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹'+ , '≠', '∼', '≁', '≈', '≉', '≋', '∻', '≃', '≄', '≂'+ , '≅', '≇', '≊', '≡', '≢', '≣', '≐', '≑', '≔', '≕'+ , '≗', '≘', '≙', '≚', '≛', '≜', '≝', '≞', '≟', '≤'+ , '≥', '≰', '≱', '≰', '≱', '≮', '≯', '≲', '≳', '⋦'+ , '⋧', '≴', '≵', '⊂', '⊃', '⊄', '⊅', '⊆', '⊇', '⊈'+ , '⊉', '⊏', '⊐', '⊑', '⊒', '⋢', '⋣', '∉', '∌', '∧'+ , '∨', '⋀', '⋁', '∩', '∪', '⊎', '⊍', '⋂', '⋃', '⨄'+ , '⨃', '⊓', '⊔', '⨅', '⨆', '⊢', '⊬', '⊣', '⊨', '⊭'+ , '⊩', '⊮', '⊫', '⊯', '⊪', '∣', '∤', '∥', '∦', '∀'+ , '∃', '∄', '∅', '∁', '⌜', '⌈', '⌝', '⌉', '⌞', '⌊'+ , '⌟', '⌋', '∎', '×', '∘', '∘', '∙', '⋆', '∔', '∸'+ , '∷', '∺', '∹', '⊹', '∛', '∜', '∆', '∞', '⅋', '⨟'+ , '⦂', '⊕', '⊖', '⊗', '⊘', '⊙', '⊚', '⊛', '⊜', '⊝'+ , '⨁', '⨂', '⨀', '⍟', '⊞', '⊟', '⊠', '⊡', '←', '←'+ , '⇐', '⇐', '→', '→', '⇒', '⇒', '↑', '⇑', '↓', '⇓'+ , '↕', '⇕', '↔', '↔', '⇔', '⇔', '↖', '⇖', '↗', '⇗'+ , '↘', '⇘', '↙', '⇙', '⇚', '⇇', '⇆', '⇛', '⇉', '⇶'+ , '⇄', '⟰', '⇈', '⇅', '⟱', '⇊', '⇵', '⟵', '⟵', '↜'+ , '⟶', '⟶', '↝', '⟷', '⟷', '↭', '↚', '↚', '⇍', '↛'+ , '↛', '⇏', '⇏', '↮', '↮', '⇎', '⇎', '↤', '↞', '↦'+ , '↠', '↥', '↟', '↧', '↡', '↨', '↢', '↣', '⊸', '⊸'+ , '↯', '▣', '▢', '▰', '▱', '◆', '◇', '◈', '●', '○'+ , '◎', '◌', '◯', '✶', '✴', '✹', '𝔸', '𝔹', 'ℂ', '𝔻'+ , '𝔼', '𝔽', '𝔾', 'ℍ', '𝕀', '𝕁', '𝕂', '𝕃', '𝕄', 'ℕ'+ , '𝕆', 'ℙ', 'ℚ', 'ℝ', '𝕊', '𝕋', '𝕌', '𝕍', '𝕎', '𝕏'+ , '𝕐', 'ℤ', 'ℾ', 'ℿ', '⅀', '𝕒', '𝕓', '𝕔', '𝕕', '𝕖'+ , '𝕗', '𝕘', '𝕙', '𝕚', '𝕛', '𝕜', '𝕝', '𝕞', '𝕟', '𝕠'+ , '𝕡', '𝕢', '𝕣', '𝕤', '𝕥', '𝕦', '𝕧', '𝕨', '𝕩', '𝕪'+ , '𝕫', 'ℽ', 'ℼ', '𝟘', '𝟙', '𝟚', '𝟛', '𝟜', '𝟝', '𝟞'+ , '𝟟', '𝟠', '𝟡', '𝟎', '𝟏', '𝟐', '𝟑', '𝟒', '𝟓', '𝟔'+ , '𝟕', '𝟖', '𝟗', '⟦', '⟧', '⟨', '⟩', '⟪', '⟫', '⦃'+ , '⦄', '⟅', '⟆', '⟅', '⟆', '⦊', '⦈', '⦆', '•', '◦'+ , '‣', '♭', '♯', '\\', '–', '—', '‼', '⁇', '‽', '⁉'+ , '✂', '⁀', '‿', 'α', 'Α'+ , 'β', 'Β', 'γ', 'Γ', 'δ', 'Δ', 'ε', 'Ε', 'ζ', 'Ζ'+ , 'η', 'Η', 'θ', 'Θ', 'ι', 'Ι', 'κ', 'Κ', 'λ', 'Λ'+ , 'ƛ', 'μ', 'Μ', 'ν', 'Ν', 'ξ', 'Ξ', 'ρ', 'Ρ', 'σ'+ , 'Σ', 'τ', 'Τ', 'υ', 'Υ', 'φ', 'Φ', 'χ', 'Χ', 'ψ'+ , 'Ψ', 'ω', 'Ω', '𝐴', '𝐵', '𝐶', '𝐷', '𝐸', '𝐹', '𝐺'+ , '𝐻', '𝐼', '𝐽', '𝐾', '𝐿', '𝑀', '𝑁', '𝑂', '𝑃', '𝑄'+ , '𝑅', '𝑆', '𝑇', '𝑈', '𝑉', '𝑊', '𝑋', '𝑌', '𝑍', '𝑎'+ , '𝑏', '𝑐', '𝑑', '𝑒', '𝑓', '𝑔', 'ℎ', '𝑖', '𝑗', '𝑘'+ , '𝑙', '𝑚', '𝑛', '𝑜', '𝑝', '𝑞', '𝑟', '𝑠', '𝑡', '𝑢'+ , '𝑣', '𝑤', '𝑥', '𝑦', '𝑧', '𝑨', '𝑩', '𝑪', '𝑫', '𝑬'+ , '𝑭', '𝑮', '𝑯', '𝑰', '𝑱', '𝑲', '𝑳', '𝑴', '𝑵', '𝑶'+ , '𝑷', '𝑸', '𝑹', '𝑺', '𝑻', '𝑼', '𝑽', '𝑾', '𝑿', '𝒀'+ , '𝒁', '𝒂', '𝒃', '𝒄', '𝒅', '𝒆', '𝒇', '𝒈', '𝒉', '𝒊'+ , '𝒋', '𝒌', '𝒍', '𝒎', '𝒏', '𝒐', '𝒑', '𝒒', '𝒓', '𝒔'+ , '𝒕', '𝒖', '𝒗', '𝒘', '𝒙', '𝒚', '𝒛', '𝒜', 'ℬ', '𝒞'+ , '𝒟', 'ℰ', 'ℱ', '𝒢', 'ℋ', 'ℐ', '𝒥', '𝒦', 'ℒ', 'ℳ'+ , '𝒩', '𝒪', '𝒫', '𝒬', 'ℛ', '𝒮', '𝒯', '𝒰', '𝒱', '𝒲'+ , '𝒳', '𝒴', '𝒵', '𝒶', '𝒷', '𝒸', '𝒹', 'ℯ', '𝒻', 'ℊ'+ , '𝒽', '𝒾', '𝒿', '𝓀', '𝓁', '𝓂', '𝓃', 'ℴ', '𝓅', '𝓆'+ , '𝓇', '𝓈', '𝓉', '𝓊', '𝓋', '𝓌', '𝓍', '𝓎', '𝓏', '𝓐'+ , '𝓑', '𝓒', '𝓓', '𝓔', '𝓕', '𝓖', '𝓗', '𝓘', '𝓙', '𝓚'+ , '𝓛', '𝓜', '𝓝', '𝓞', '𝓟', '𝓠', '𝓡', '𝓢', '𝓣'+ , '𝓤', '𝓥', '𝓦', '𝓧', '𝓨', '𝓩', '𝓪', '𝓫', '𝓬', '𝓭'+ , '𝓮', '𝓯', '𝓰', '𝓱', '𝓲', '𝓳', '𝓴', '𝓵', '𝓶', '𝓷'+ , '𝓸', '𝓹', '𝓺', '𝓻', '𝓼', '𝓽', '𝓾', '𝓿', '𝔀', '𝔁'+ , '𝔂', '𝔃', '𝔄', '𝔅', 'ℭ', '𝔇', '𝔈', '𝔉', '𝔊', 'ℌ'+ , 'ℑ', '𝔍', '𝔎', '𝔏', '𝔐', '𝔑', '𝔒', '𝔓', '𝔔', 'ℜ'+ , '𝔖', '𝔗', '𝔘', '𝔙', '𝔚', '𝔛', '𝔜', 'ℨ', '𝔞', '𝔟'+ , '𝔠', '𝔡', '𝔢', '𝔣', '𝔤', '𝔥', '𝔦', '𝔧', '𝔨', '𝔩'+ , '𝔪', '𝔫', '𝔬', '𝔭', '𝔮', '𝔯', '𝔰', '𝔱', '𝔲', '𝔳'+ , '𝔴', '𝔵', '𝔶', '𝔷', 'ₐ', 'ₑ', 'ₕ', 'ᵢ', 'ⱼ', 'ₖ'+ , 'ₗ', 'ₘ', 'ₙ', 'ₒ', 'ₚ', 'ᵣ', 'ₛ', 'ₜ', 'ᵤ', 'ᵥ'+ , 'ₓ', 'ᵦ', 'ᵧ', 'ᵨ', 'ᵩ', 'ᵪ', 'ᵃ', 'ᵇ', 'ᶜ', 'ᵈ'+ , 'ᵉ', 'ᶠ', 'ᵍ', 'ʰ', 'ⁱ', 'ʲ', 'ᵏ', 'ˡ', 'ᵐ', 'ⁿ'+ , 'ᵒ', 'ᵖ', 'ʳ', 'ˢ', 'ᵗ', 'ᵘ', 'ᵛ', 'ʷ', 'ˣ', 'ʸ'+ , 'ᶻ', 'ᴬ', 'ᴮ', 'ᴰ', 'ᴱ', 'ᴳ', 'ᴴ', 'ᴵ', 'ᴶ', 'ᴷ'+ , 'ᴸ', 'ᴹ', 'ᴺ', 'ᴼ', 'ᴾ', 'ᴿ', 'ᵀ', 'ᵁ', 'ⱽ', 'ᵂ'+ , 'ᵝ', 'ᵞ', 'ᵟ', 'ᵋ', 'ᶿ', 'ᵠ', 'ᵡ', ' ', '¡', '¢'+ , '¦', '°', '¿', 'ª', 'º'+ ]+ ]+++simplify :: Eq a => Edit a -> Maybe (Edit a)+simplify x@(Swap b a) = bool Nothing (Just x) $ b /= a+simplify x = Just x++subsets :: Ord a => [a] -> [[a]]+subsets [] = [[]]+subsets zs@(x : xs) = nubOrd $ filter (/= zs) $ subsets xs ++ fmap (x :) (subsets xs)++newtype Row a = Row a deriving (Eq, Ord, Show)+newtype Col a = Col a deriving (Eq, Ord, Show)+
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ test/TestSpec.hs view
@@ -0,0 +1,171 @@+{-# LANGUAGE NumDecimals #-}+{-# LANGUAGE OverloadedStrings #-}++module TestSpec where++import Control.Concurrent (threadDelay)+import Control.Monad (void)+import Cornelis.Subscripts (decNextDigitSeq, incNextDigitSeq)+import Cornelis.Types+import Cornelis.Types.Agda (Rewrite (..))+import Cornelis.Utils (withBufferStuff)+import Cornelis.Vim+import qualified Data.Text as T+import qualified Data.Vector as V+import Neovim (liftIO)+import Neovim.API.Text+import Neovim.Test+import Plugin+import Test.Hspec+import Utils+++broken :: String -> SpecWith a -> SpecWith a+broken = before_ . pendingWith++spec :: Spec+spec = focus $ do+ let timeout = Seconds 60+ diffSpec "should refine" timeout "test/Hello.agda"+ [ Swap "unit = ?" "unit = one"] $ \w _ -> do+ goto w 11 8+ refine++ broken "Times out in CI for unknown reasons" $ diffSpec "should support helper functions" timeout "test/Hello.agda"+ [ Swap "" "help_me : Unit"] $ \w _ -> do+ goto w 11 8+ helperFunc Normalised "help_me"+ liftIO $ threadDelay 5e5+ void $ vim_command "normal! G\"\"p"++ diffSpec "should case split (unicode lambda)" timeout "test/Hello.agda"+ [ Add "slap = λ { true → {! !}"+ , Swap "slap = λ { x → ? }" " ; false → {! !} }"+ ] $ \w _ -> do+ goto w 20 16+ caseSplit "x"++ diffSpec "should preserve indents when doing case split" timeout "test/Hello.agda"+ [ Add " testIndent true = {! !}"+ , Swap " testIndent b = ?" " testIndent false = {! !}"+ ] $ \w _ -> do+ goto w 24 18+ caseSplit "b"++ diffSpec "should refine with hints" timeout "test/Hello.agda"+ [ Swap "isEven∘ (suc n) = {! isEven∘ !}" "isEven∘ (suc n) = isEven∘ {! !}"] $ \w _ -> do+ goto w 28 24+ refine++ let case_split_test name row col =+ diffSpec ("should case split (" <> T.unpack name <> ")") timeout "test/Hello.agda"+ (fmap (fmap (name <>))+ [ Add " true = {! !}"+ , Swap " x = ?" " false = {! !}"+ ]+ ) $ \w _ -> do+ goto w row col+ caseSplit "x"++ case_split_test "test" 14 10++ case_split_test "unicodeTest₁" 17 18++ vimSpec "should support why in scope" timeout "test/Hello.agda" $ \_ b -> do+ withBufferStuff b $ \bs -> do+ whyInScope "zero"+ liftIO $ threadDelay 5e5+ res <- buffer_get_lines (iw_buffer $ bs_info_win bs) vimFirstLine vimLastLine False+ liftIO $ V.toList res `shouldContain` ["zero is in scope as"]++ vimSpec "should support goto definition across modules"+ timeout "test/Hello.agda" $ \w _ -> do+ goto w 2 18+ gotoDefinition+ liftIO $ threadDelay 5e5+ b' <- nvim_get_current_buf+ res <- buffer_get_lines b' vimFirstLine vimLastLine False+ liftIO $ V.toList res `shouldContain` ["module Agda.Builtin.Nat where"]++ diffSpec "work with multiple" timeout "test/Hello.agda"+ [ Add "copattern true = {! !}"+ , Swap "copattern = ?" "copattern false = {! !}"+ ] $ \w _ -> do+ goto w 31 13+ caseSplit ""+ liftIO $ threadDelay 5e5+ goto w 31 15+ liftIO $ threadDelay 5e5+ caseSplit "x"++ diffSpec "work with ? in names" timeout "test/Hello.agda"+ [ Swap "foo? ?f = {! !}" "foo? ?f x = {! !}"+ ] $ \w _ -> do+ goto w 34 13+ caseSplit ""++ diffSpec "question to meta" timeout "test/Hello.agda"+ [ Swap "unit = ?" "unit = {! !}"+ , Swap "test x = ?" "test x = {! !}"+ , Swap "unicodeTest\8321 x = ?" "unicodeTest\8321 x = {! !}"+ , Swap "slap = \955 { x \8594 ? }" "slap = \955 { x \8594 {! !} }"+ , Swap " testIndent b = ?" " testIndent b = {! !}"+ , Swap "copattern = ?" "copattern = {! !}"+ ] $ \_ b -> do+ questionToMeta b++ diffSpec "give" timeout "test/Hello.agda"+ [ Swap "give = {! true !}" "give = true"+ ] $ \w _ -> do+ goto w 37 11+ give++ let elaborate_test rw changes row column =+ let title = maybe "default mode" show rw in+ diffSpec ("elaborate (" <> title <> ")") timeout "test/Hello.agda" changes $+ \w _ -> do+ goto w row column+ withNormalizationMode rw elaborate++ elaborate_test (Just "AsIs")+ [Swap "elaborate = {! 3 !}" "elaborate = 3"]+ 40 16++ diffSpec "should dec subscripts" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ : Nat" "sub₋₁and-super⁹ : Nat"] $ \w _ -> do+ goto w 42 1+ decNextDigitSeq++ diffSpec "should inc subscripts" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ : Nat" "sub₁and-super⁹ : Nat"] $ \w _ -> do+ goto w 42 1+ incNextDigitSeq++ diffSpec "should dec superscripts" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ : Nat" "sub₀and-super⁸ : Nat"] $ \w _ -> do+ goto w 42 6+ decNextDigitSeq++ diffSpec "should inc superscripts" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ : Nat" "sub₀and-super¹⁰ : Nat"] $ \w _ -> do+ goto w 42 6+ incNextDigitSeq++ diffSpec "should dec digits" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ = 15" "sub₀and-super⁹ = 14"] $ \w _ -> do+ goto w 43 16+ decNextDigitSeq++ diffSpec "should inc digits" timeout "test/Hello.agda"+ [ Swap "sub₀and-super⁹ = 15" "sub₀and-super⁹ = 16"] $ \w _ -> do+ goto w 43 16+ incNextDigitSeq++ vimSpec "should infer type of local variable" timeout "test/Hello.agda" $ \w b -> do+ withBufferStuff b $ \bs -> do+ goto w 46 14+ inferType AsIs+ liftIO $ threadDelay 5e5+ res <- buffer_get_lines (iw_buffer $ bs_info_win bs) vimFirstLine vimLastLine False+ liftIO $ V.toList res `shouldContain` ["Inferred Type: Bool"]+
+ test/Utils.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE NumDecimals #-}+{-# LANGUAGE OverloadedStrings #-}++module Utils+ ( module Utils+ , Edit (..)+ ) where++import Control.Concurrent (threadDelay)+import Cornelis.Types+import Cornelis.Offsets+import Cornelis.Utils (withLocalEnv)+import Cornelis.Vim+import Data.Foldable.Levenshtein (levenshtein, Edit(..))+import qualified Data.Text as T+import qualified Data.Vector as V+import Lib+import Neovim+import Neovim.API.Text+import Neovim.Test+import Plugin+import System.FilePath (takeBaseName)+import System.IO (hFlush, hPutStr)+import System.IO.Temp (withSystemTempFile)+import Test.Hspec hiding (after, before)+++-- data Diff a+-- = Insert a+-- | Delete a+-- | Modify a a+-- deriving (Eq, Ord, Show, Functor)++isCopy :: Edit a -> Bool+isCopy Copy{} = True+isCopy _ = False++diff :: Show a => Eq a => [a] -> [a] -> [Edit a]+diff = ((filter (not . isCopy) . snd) .) . levenshtein @_ @_ @_ @Int+ -- (snd .) . go+ -- where+ -- go ([]) as = (length as, fmap Insert as)+ -- go bs [] = (length bs, fmap Delete bs)+ -- go (b : bs) (a : as)+ -- | b == a = go bs as+ -- | otherwise = do+ -- let x = traceShowId $ bimap (+1) (Delete b :) $ go bs (a : as)+ -- y = traceShowId $ bimap (+1) (Insert a :) $ go (b : bs) as+ -- z = traceShowId $ bimap (+1) (Modify b a :) $ go bs as+ -- minimumBy (comparing fst) [z, x, y]+++differing :: Buffer -> Neovim env () -> Neovim env [Edit Text]+differing b m = do+ before <- fmap V.toList $ buffer_get_lines b 0 (-1) False+ m+ liftIO $ threadDelay 1e6+ after <- fmap V.toList $ buffer_get_lines b 0 (-1) False+ pure $ diff before after+++intervention :: Buffer -> [Edit Text] -> Neovim env () -> Neovim env ()+intervention b d m = do+ d' <- differing b m+ liftIO $ d' `shouldBe` d++withVim :: Seconds -> (Window -> Buffer -> Neovim () ()) -> IO ()+withVim secs m = do+ let withNeovimEmbedded f = testWithEmbeddedNeovim f secs ()+ withNeovimEmbedded Nothing $ do+ b <- nvim_create_buf False False+ w <- vim_get_current_window+ nvim_win_set_buf w b+ m w b+++diffSpec+ :: String+ -> Seconds+ -> FilePath+ -> [Edit Text]+ -> (Window -> Buffer -> Neovim CornelisEnv ())+ -> Spec+diffSpec name secs fp diffs m =+ vimSpec name secs fp $ \w b -> intervention b diffs $ m w b+++vimSpec+ :: String+ -> Seconds+ -> FilePath+ -> (Window -> Buffer -> Neovim CornelisEnv ())+ -> Spec+vimSpec name secs fp m = do+ let withNeovimEmbedded f = testWithEmbeddedNeovim f secs ()+ it name $ do+ withSystemTempFile "test.agda" $ \fp' h -> do+ hPutStr h $ "module " <> takeBaseName fp' <> " where\n"+ hPutStr h . unlines . tail . lines =<< readFile fp+ hFlush h+ withNeovimEmbedded Nothing $ do+ env <- cornelisInit+ withLocalEnv env $ do+ vim_command $ "edit " <> T.pack fp'+ liftIO $ threadDelay 1e6+ w <- vim_get_current_window+ b <- nvim_win_get_buf w+ load+ liftIO $ threadDelay 5e6+ m w b++goto :: Window -> Int -> Int -> Neovim env ()+goto w row col = setWindowCursor w $ Pos (toOneIndexed row) (toOneIndexed col)+