diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -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 + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,422 @@ +# cornelis + +![Cornelis in Action](https://raw.githubusercontent.com/isovector/cornelis/master/cast.gif) + + +## 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 | C-cC-l | +| `:CornelisGoals` | Show all goals | C-cC-? | +| `:CornelisRestart` | Kill and restart the `agda` process | C-cC-xC-r | +| `:CornelisAbort` | Abort running command | C-cC-xC-a | +| `:CornelisSolve ` | Solve constraints | C-cC-s | +| `:CornelisGoToDefinition` | Jump to definition of name at cursor | M-. or middle mouse button | +| `:CornelisPrevGoal` | Jump to previous goal | C-cC-b | +| `:CornelisNextGoal` | Jump to next goal | C-cC-f | +| `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ | +| `:CornelisInc` | Like `` but also targets sub- and superscripts | _(none)_ | +| `:CornelisDec` | Like `` but also targets sub- and superscripts | _(none)_ | +| `:CornelisCloseInfoWindows` | Close (all) info windows cornelis has opened | _(none)_ | + +### Commands in context of a goal + +These commands can be used in context of a hole: + +| Vim command | Description | Equivalent agda-mode keybinding | +| :--- | :--- | :--- | +| `:CornelisGive` | Fill goal with hole contents | C-cC-SPC | +| `:CornelisRefine` | Refine goal | C-cC-r | +| `:CornelisElaborate ` | Fill goal with normalized hole contents | C-cC-m | +| `:CornelisAuto` | [Automatic proof search] | C-cC-a | +| `:CornelisMakeCase` | Case split | C-cC-c | +| `:CornelisTypeContext ` | Show goal type and context | C-cC-, | +| `:CornelisTypeInfer ` | Show inferred type of hole contents | C-cC-d | +| `:CornelisTypeContextInfer ` | Show goal type, context, and inferred type of hole contents | C-cC-. | +| `:CornelisNormalize ` | Compute normal of hole contents | C-cC-n | +| `:CornelisWhyInScope` | Show why given name is in scope | C-cC-w | +| `:CornelisHelperFunc ` | Copy inferred type to register `"` | C-cC-h | + +[Automatic proof search]: https://agda.readthedocs.io/en/latest/tools/auto.html#auto + +Commands with an `` argument take an optional normalization mode argument, +one of `AsIs`, `Instantiated`, `HeadNormal`, `Simplified` or `Normalised`. When +omitted, defaults to `Normalised`. + +Commands with a `` argument take an optional compute mode argument: + +| `` | Description | Equivalent agda-mode prefix | +| :--- | :--- | :--- | +| `DefaultCompute` | default, used if `` is omitted | no prefix, default | +| `IgnoreAbstract` | compute normal form, ignoring `abstract`s | C-u | +| `UseShowInstance` | compute normal form of print using `show` instance | C-uC-u | +| `HeadCompute` | compute weak-head normal form | C-uC-uC-u | + +If Agda is stuck executing a command (e.g. if normalization takes too long), +abort the command with `:CornelisAbort`. + +If you need to restart the plugin (eg if Agda is stuck in a loop), you can +restart everything via `:CornelisRestart`. + +### Agda Input + +There is reasonably good support for agda-input via your `` 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 ``, add the following +to your `.vimrc`: + +```viml +let g:cornelis_agda_prefix = "" " 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 :call cornelis#prompt_input() +``` + + +#### 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 `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..cornelis` and the +vim plugin as `cornelis.packages..cornelis-vim`. Below is a sample +configuration to help you understand where everything plugs in. + +
+Nix details + +```nix +# flake.nix +{ + description = "my-config"; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; + home-manager = { + url = "github:nix-community/home-manager"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + cornelis.url = "github:isovector/cornelis"; + cornelis.inputs.nixpkgs.follows = "nixpkgs"; + }; + outputs = + { home-manager + , nixpkgs + , cornelis + , ... + }: { + nixosConfigurations = { + bellerophon = nixpkgs.lib.nixosSystem { + system = "x86_64-linux"; + modules = [ + home-manager.nixosModules.home-manager + { + nixpkgs.overlays = [cornelis.overlays.cornelis]; + home-manager.useGlobalPkgs = true; + home-manager.useUserPackages = true; + home-manager.users.my-home = import ./my-home.nix; + } + ]; + }; + }; + }; +} + +# my-home.nix +{pkgs, ...}: +{ + home.packages = [ pkgs.agda ]; + programs.neovim = { + enable = true; + extraConfig = builtins.readFile ./init.vim; + plugins = [ + { + # plugin packages in required Vim plugin dependencies + plugin = pkgs.vimPlugins.cornelis; + config = "let g:cornelis_use_global_binary = 1"; + } + ]; + extraPackages = [ pkgs.cornelis ]; + }; +} +``` +
+ +Make sure you enable the global binary option in your vim config. Since +`/nix/store` is immutable cornelis will fail when `nvim-hs` tries to run stack, +which it will do if the global binary option isn't enabled. + + +#### Use global binary instead of stack + +Vimscript: + +```viml +let g:cornelis_use_global_binary = 1 +``` + +Lua: + +```lua +vim.g.cornelis_use_global_binary = 1 +``` + + +## Example Configuration + +Once you have `cornelis` installed, you'll probably want to add some keybindings +for it! This is enough to get you started: + +```viml +au BufRead,BufNewFile *.agda call AgdaFiletype() +au QuitPre *.agda :CornelisCloseInfoWindows +function! AgdaFiletype() + nnoremap l :CornelisLoad + nnoremap r :CornelisRefine + nnoremap d :CornelisMakeCase + nnoremap , :CornelisTypeContext + nnoremap . :CornelisTypeContextInfer + nnoremap n :CornelisSolve + nnoremap a :CornelisAuto + nnoremap gd :CornelisGoToDefinition + nnoremap [/ :CornelisPrevGoal + nnoremap ]/ :CornelisNextGoal + nnoremap :CornelisInc + nnoremap :CornelisDec +endfunction +``` + +Feeling spicy? Automatically run `CornelisLoad` every time you save the file. + +```viml +au BufWritePost *.agda execute "normal! :CornelisLoad\" +``` + +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 (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 `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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,4 @@ +module Main (main) where + +import Lib (main) + diff --git a/cornelis.cabal b/cornelis.cabal new file mode 100644 --- /dev/null +++ b/cornelis.cabal @@ -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 +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 diff --git a/src/Cornelis/Agda.hs b/src/Cornelis/Agda.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Agda.hs @@ -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 + diff --git a/src/Cornelis/Config.hs b/src/Cornelis/Config.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Config.hs @@ -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"]) + diff --git a/src/Cornelis/Debug.hs b/src/Cornelis/Debug.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Debug.hs @@ -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) diff --git a/src/Cornelis/Diff.hs b/src/Cornelis/Diff.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Diff.hs @@ -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 diff --git a/src/Cornelis/Goals.hs b/src/Cornelis/Goals.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Goals.hs @@ -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 + diff --git a/src/Cornelis/Highlighting.hs b/src/Cornelis/Highlighting.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Highlighting.hs @@ -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] + diff --git a/src/Cornelis/InfoWin.hs b/src/Cornelis/InfoWin.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/InfoWin.hs @@ -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 + diff --git a/src/Cornelis/Offsets.hs b/src/Cornelis/Offsets.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Offsets.hs @@ -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) diff --git a/src/Cornelis/Pretty.hs b/src/Cornelis/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Pretty.hs @@ -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 ] diff --git a/src/Cornelis/Subscripts.hs b/src/Cornelis/Subscripts.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Subscripts.hs @@ -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 + diff --git a/src/Cornelis/Types.hs b/src/Cornelis/Types.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Types.hs @@ -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 diff --git a/src/Cornelis/Types/Agda.hs b/src/Cornelis/Types/Agda.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Types/Agda.hs @@ -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 + diff --git a/src/Cornelis/Utils.hs b/src/Cornelis/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Utils.hs @@ -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 diff --git a/src/Cornelis/Vim.hs b/src/Cornelis/Vim.hs new file mode 100644 --- /dev/null +++ b/src/Cornelis/Vim.hs @@ -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 "" + 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) + diff --git a/src/Lib.hs b/src/Lib.hs new file mode 100644 --- /dev/null +++ b/src/Lib.hs @@ -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 + ] + } + diff --git a/src/Plugin.hs b/src/Plugin.hs new file mode 100644 --- /dev/null +++ b/src/Plugin.hs @@ -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 diff --git a/test/PropertySpec.hs b/test/PropertySpec.hs new file mode 100644 --- /dev/null +++ b/test/PropertySpec.hs @@ -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) + diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-} diff --git a/test/TestSpec.hs b/test/TestSpec.hs new file mode 100644 --- /dev/null +++ b/test/TestSpec.hs @@ -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"] + diff --git a/test/Utils.hs b/test/Utils.hs new file mode 100644 --- /dev/null +++ b/test/Utils.hs @@ -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) +