Implement: Make the rewrite mode modifiable #41

Author: ivanovs-4

README.md

@@ -69,6 +69,7 @@ These commands can be used in context of a hole:
 Commands with an `<RW>` argument take an optional normalization mode argument,
 one of `AsIs`, `Instantiated`, `HeadNormal`, `Simplified` or `Normalised`. When
 omitted, defaults to `Normalised`.
+This default may be specified in vimrc as `g:cornelis_rewrite_mode`.
 
 Commands with a `<CM>` argument take an optional compute mode argument:
 
@@ -364,6 +365,19 @@ The following configuration options are available:
 - `left`: Opens at the left of the window.
 - `right`: Opens at the right of the window.
 
+Set default rewrite mode to use in commands which take an optional
+normalization mode argument
+
+```viml
+let g:cornelis_rewrite_mode = 'HeadNormal'
+```
+
+The following configuration options are available:
+- `AsIs`
+- `Instantiated`
+- `HeadNormal`
+- `Simplified`
+- `Normalised`
 
 ### Aligning Reasoning Justification
 

src/Cornelis/Config.hs

@@ -3,6 +3,7 @@
 module Cornelis.Config where
 
 import           Cornelis.Types
+import           Cornelis.Types.Agda (Rewrite(..))
 import           Cornelis.Utils (objectToInt, objectToText)
 import           Data.Maybe (fromMaybe)
 import qualified Data.Text as T
@@ -38,4 +39,6 @@ getConfig
         (getVar "cornelis_max_width")
     <*> (fromMaybe Horizontal . (>>= (readSplitLocation . T.unpack <=< objectToText)) <$>
         getVarWithAlternatives ["cornelis_split_location", "cornelis_split_direction"])
+    <*> (fromMaybe HeadNormal . (>>= (readRewrite . T.unpack <=< objectToText)) <$>
+        (getVar "cornelis_rewrite_mode"))
 

src/Cornelis/Types.hs

@@ -26,7 +26,7 @@ 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 Cornelis.Types.Agda (InteractionId, Rewrite(..))
 import Data.Aeson hiding (Error)
 import Data.Char (toLower)
 import Data.Functor.Identity
@@ -102,11 +102,20 @@ readSplitLocation s = case fmap toLower s of
   "bottom"     -> Just OnBottom
   _            -> Nothing
 
+readRewrite :: String -> Maybe Rewrite
+readRewrite s = case fmap toLower s of
+  "asis"         -> Just AsIs
+  "instantiated" -> Just Instantiated
+  "headnormal"   -> Just HeadNormal
+  "simplified"   -> Just Simplified
+  "normalised"   -> Just Normalised
+  _              -> Nothing
 
 data CornelisConfig = CornelisConfig
   { cc_max_height :: Int64
   , cc_max_width :: Int64
   , cc_split_location :: SplitLocation
+  , cc_rewrite_mode :: Rewrite
   }
   deriving (Show, Generic)
 
@@ -115,6 +124,7 @@ data CornelisEnv = CornelisEnv
   , ce_stream :: InChan AgdaResp
   , ce_namespace :: Int64
   , ce_config :: CornelisConfig
+
   }
   deriving Generic
 

src/Plugin.hs

@@ -132,8 +132,8 @@ doRestart _ = do
 doAbort :: CommandArguments -> Neovim CornelisEnv ()
 doAbort _ = withAgda $ withCurrentBuffer $ getAgda >=> runIOTCM Cmd_abort
 
-normalizationMode :: Neovim env Rewrite
-normalizationMode = pure HeadNormal
+normalizationMode :: Neovim CornelisEnv Rewrite
+normalizationMode = asks (cc_rewrite_mode . ce_config)
 
 computeMode :: Neovim env ComputeMode
 computeMode = pure DefaultCompute
@@ -163,7 +163,7 @@ autoOne _ ms = withNormalizationMode ms $ \mode ->
         (mkAbsPathRnage fp $ ip_interval' ip)
         (T.unpack t)
 
-withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
+withNormalizationMode :: Maybe String -> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
 withNormalizationMode Nothing f = normalizationMode >>= f
 withNormalizationMode (Just s) f =
   case readMaybe s of