-- | 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 :: forall a.
BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a
modifyDiff BufferNum
buf Diff0 -> (Diff0, a)
f = do
  IORef CornelisState
csRef <- (CornelisEnv -> IORef CornelisState)
-> Neovim CornelisEnv (IORef CornelisState)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> IORef CornelisState
ce_state
  IO a -> Neovim CornelisEnv a
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> Neovim CornelisEnv a) -> IO a -> Neovim CornelisEnv a
forall a b. (a -> b) -> a -> b
$ IORef CornelisState
-> (CornelisState -> (CornelisState, a)) -> IO a
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef CornelisState
csRef ((CornelisState -> (CornelisState, a)) -> IO a)
-> (CornelisState -> (CornelisState, a)) -> IO a
forall a b. (a -> b) -> a -> b
$ \CornelisState
cs ->
    let (a
a, Map BufferNum Diff0
ds') = (Maybe Diff0 -> (a, Maybe Diff0))
-> BufferNum -> Map BufferNum Diff0 -> (a, Map BufferNum Diff0)
forall (f :: * -> *) k a.
(Functor f, Ord k) =>
(Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
Map.alterF ((Diff0 -> Maybe Diff0) -> (a, Diff0) -> (a, Maybe Diff0)
forall a b. (a -> b) -> (a, a) -> (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Diff0 -> Maybe Diff0
forall a. a -> Maybe a
Just ((a, Diff0) -> (a, Maybe Diff0))
-> (Maybe Diff0 -> (a, Diff0)) -> Maybe Diff0 -> (a, Maybe Diff0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Diff0, a) -> (a, Diff0)
forall a b. (a, b) -> (b, a)
swap ((Diff0, a) -> (a, Diff0))
-> (Maybe Diff0 -> (Diff0, a)) -> Maybe Diff0 -> (a, Diff0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Diff0 -> (Diff0, a)
alter) BufferNum
buf (CornelisState -> Map BufferNum Diff0
cs_diff CornelisState
cs)
    in (CornelisState
cs { cs_diff = ds' }, a
a)
  where
    alter :: Maybe Diff0 -> (Diff0, a)
alter Maybe Diff0
Nothing = Diff0 -> (Diff0, a)
f Diff0
forall r. Semigroup r => ADiff r
D.emptyDiff
    alter (Just Diff0
d) = Diff0 -> (Diff0, a)
f Diff0
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 :: BufferNum -> Neovim CornelisEnv ()
resetDiff BufferNum
buf = BufferNum -> (Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ()
forall a.
BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a
modifyDiff BufferNum
buf ((Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ())
-> (Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Diff0, ()) -> Diff0 -> (Diff0, ())
forall a b. a -> b -> a
const (Diff0
forall r. Semigroup r => ADiff r
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 :: BufferNum -> Replace DPos -> Neovim CornelisEnv ()
recordUpdate BufferNum
buf Replace DPos
r = BufferNum -> (Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ()
forall a.
BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a
modifyDiff BufferNum
buf ((Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ())
-> (Diff0 -> (Diff0, ())) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Diff0
d -> (Replace DPos -> Diff0 -> Diff0
forall r. Shift r => r -> ADiff r -> ADiff r
D.addDiff Replace DPos
r Diff0
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 :: BufferNum
-> Interval VimPos -> Neovim CornelisEnv (Maybe (Interval VimPos))
translateInterval BufferNum
buf Interval VimPos
sp = BufferNum
-> (Diff0 -> (Diff0, Maybe (Interval VimPos)))
-> Neovim CornelisEnv (Maybe (Interval VimPos))
forall a.
BufferNum -> (Diff0 -> (Diff0, a)) -> Neovim CornelisEnv a
modifyDiff BufferNum
buf ((Diff0 -> (Diff0, Maybe (Interval VimPos)))
 -> Neovim CornelisEnv (Maybe (Interval VimPos)))
-> (Diff0 -> (Diff0, Maybe (Interval VimPos)))
-> Neovim CornelisEnv (Maybe (Interval VimPos))
forall a b. (a -> b) -> a -> b
$ \Diff0
d -> (Diff0
d, Diff0 -> Maybe (Interval VimPos)
translate Diff0
d)
  where
    translate :: Diff0 -> Maybe (Interval VimPos)
    translate :: Diff0 -> Maybe (Interval VimPos)
translate Diff0
d = (Interval DPos -> Interval VimPos)
-> Maybe (Interval DPos) -> Maybe (Interval VimPos)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Interval DPos -> Interval VimPos
toInterval (Maybe (Interval DPos) -> Maybe (Interval VimPos))
-> (Interval DPos -> Maybe (Interval DPos))
-> Interval DPos
-> Maybe (Interval VimPos)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Diff0 -> Block (Replace DPos) -> Maybe (Block (Replace DPos))
forall r. Shift r => ADiff r -> Block r -> Maybe (Block r)
D.mapDiff Diff0
d (Interval DPos -> Maybe (Interval VimPos))
-> Maybe (Interval DPos) -> Maybe (Interval VimPos)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Interval VimPos -> Maybe (Interval DPos)
fromInterval Interval VimPos
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 VimPos -> Maybe (Interval DPos)
fromInterval (Interval VimPos
p1 VimPos
p2) = (DPos
q1 D.:..) (Vallee (Offset 'Line) (Offset 'Byte) -> Interval DPos)
-> Maybe (Vallee (Offset 'Line) (Offset 'Byte))
-> Maybe (Interval DPos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DPos
q2 DPos -> DPos -> Maybe (Trans DPos)
forall p. Amor p => p -> p -> Maybe (Trans p)
D..-.? DPos
q1)
  where
    q1 :: DPos
q1 = VimPos -> DPos
fromVimPos VimPos
p1
    q2 :: DPos
q2 = VimPos -> DPos
fromVimPos VimPos
p2

-- | Inverse of 'fromInterval'.
toInterval :: D.Interval DPos -> Interval VimPos
toInterval :: Interval DPos -> Interval VimPos
toInterval (DPos
q D.:.. Trans DPos
v) = VimPos -> VimPos -> Interval VimPos
forall p. p -> p -> Interval p
Interval (DPos -> VimPos
toVimPos DPos
q) (DPos -> VimPos
toVimPos (DPos
q DPos -> Trans DPos -> DPos
forall p. Amor p => p -> Trans p -> p
D..+ Trans DPos
v))

-- | Convert from Cornelis positions to diff-loc positions.
fromVimPos :: VimPos -> DPos
fromVimPos :: VimPos -> DPos
fromVimPos (Pos Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c) = Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> DPos
forall l c. l -> c -> Colline l c
Colline Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c

toVimPos :: DPos -> VimPos
toVimPos :: DPos -> VimPos
toVimPos (Colline Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c) = Index 'Line 'ZeroIndexed -> Index 'Byte 'ZeroIndexed -> VimPos
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Index 'Line i -> Index e j -> Pos e i j
Pos Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c