Cornelis.Offsets

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 Posisitions (pairs of line and column indices) and Intervals (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.

Documentation

data Index (e :: Unit) (i :: Indexing)

The constructor is hidden, use toZeroIndexed and toOneIndexed to construct it, and fromZeroIndexed and fromOneIndexed to destruct it.

Instances

FromJSON (Index e i)

Defined in Cornelis.Offsets

Methods

parseJSON :: Value -> Parser (Index e i)

parseJSONList :: Value -> Parser [Index e i]

omittedField :: Maybe (Index e i)

Read (Index e i)

Defined in Cornelis.Offsets

Methods

readsPrec :: Int -> ReadS (Index e i)

readList :: ReadS [Index e i]

readPrec :: ReadPrec (Index e i)

readListPrec :: ReadPrec [Index e i]

Show (Index e i)

Defined in Cornelis.Offsets

Methods

showsPrec :: Int -> Index e i -> ShowS

show :: Index e i -> String

showList :: [Index e i] -> ShowS

Amor (Index e i)

Ordered monoid action of offsets on indices.

Defined in Cornelis.Offsets

Associated Types

type Trans (Index e i)

Methods

(.+) :: Index e i -> Trans (Index e i) -> Index e i

(.-.?) :: Index e i -> Index e i -> Maybe (Trans (Index e i))

Origin (Index e 'ZeroIndexed)

The zero in zero-indexing.

Defined in Cornelis.Offsets

Methods

origin :: Index e 'ZeroIndexed

Eq (Index e i)

Defined in Cornelis.Offsets

Methods

(==) :: Index e i -> Index e i -> Bool

(/=) :: Index e i -> Index e i -> Bool

Ord (Index e i)

Defined in Cornelis.Offsets

Methods

compare :: Index e i -> Index e i -> Ordering

(<) :: Index e i -> Index e i -> Bool

(<=) :: Index e i -> Index e i -> Bool

(>) :: Index e i -> Index e i -> Bool

(>=) :: Index e i -> Index e i -> Bool

max :: Index e i -> Index e i -> Index e i

min :: Index e i -> Index e i -> Index e i

Pretty (Index e i)

Defined in Cornelis.Offsets

Methods

pretty :: Index e i -> Doc ann

prettyList :: [Index e i] -> Doc ann

type Trans (Index e i)

Defined in Cornelis.Offsets

type Trans (Index e i) = Offset e

data Indexing

Indexing scheme: whether the first index is zero or one.

Constructors

OneIndexed

ZeroIndexed

data Unit

What are we counting?

Constructors

Byte

CodePoint

Line

newtype Offset (e :: Unit)

It doesn't seem worth the trouble to hide this constructor.

Constructors

Offset Int

Instances

FromJSON (Offset e)

Defined in Cornelis.Offsets

Methods

parseJSON :: Value -> Parser (Offset e)

parseJSONList :: Value -> Parser [Offset e]

omittedField :: Maybe (Offset e)

Monoid (Offset e)

Defined in Cornelis.Offsets

Methods

mempty :: Offset e

mappend :: Offset e -> Offset e -> Offset e

mconcat :: [Offset e] -> Offset e

Semigroup (Offset e)

Defined in Cornelis.Offsets

Methods

(<>) :: Offset e -> Offset e -> Offset e

sconcat :: NonEmpty (Offset e) -> Offset e

stimes :: Integral b => b -> Offset e -> Offset e

Read (Offset e)

Defined in Cornelis.Offsets

Methods

readsPrec :: Int -> ReadS (Offset e)

readList :: ReadS [Offset e]

readPrec :: ReadPrec (Offset e)

readListPrec :: ReadPrec [Offset e]

Show (Offset e)

Defined in Cornelis.Offsets

Methods

showsPrec :: Int -> Offset e -> ShowS

show :: Offset e -> String

showList :: [Offset e] -> ShowS

Eq (Offset e)

Defined in Cornelis.Offsets

Methods

(==) :: Offset e -> Offset e -> Bool

(/=) :: Offset e -> Offset e -> Bool

Ord (Offset e)

Defined in Cornelis.Offsets

Methods

compare :: Offset e -> Offset e -> Ordering

(<) :: Offset e -> Offset e -> Bool

(<=) :: Offset e -> Offset e -> Bool

(>) :: Offset e -> Offset e -> Bool

(>=) :: Offset e -> Offset e -> Bool

max :: Offset e -> Offset e -> Offset e

min :: Offset e -> Offset e -> Offset e

Pretty (Offset e)

Defined in Cornelis.Offsets

Methods

pretty :: Offset e -> Doc ann

prettyList :: [Offset e] -> Doc ann

data Pos e i j

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.

Constructors

Pos

Fields

• p_line :: Index 'Line i
• p_col :: Index e j

Instances

FromJSON AgdaInterval

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser AgdaInterval

parseJSONList :: Value -> Parser [AgdaInterval]

omittedField :: Maybe AgdaInterval

Generic (Pos e i j)

Defined in Cornelis.Offsets

Associated Types

type Rep (Pos e i j) :: Type -> Type

Methods

from :: Pos e i j -> Rep (Pos e i j) x

to :: Rep (Pos e i j) x -> Pos e i j

Show (Pos e i j)

Defined in Cornelis.Offsets

Methods

showsPrec :: Int -> Pos e i j -> ShowS

show :: Pos e i j -> String

showList :: [Pos e i j] -> ShowS

Eq (Pos e i j)

Defined in Cornelis.Offsets

Methods

(==) :: Pos e i j -> Pos e i j -> Bool

(/=) :: Pos e i j -> Pos e i j -> Bool

Ord (Pos e i j)

Defined in Cornelis.Offsets

Methods

compare :: Pos e i j -> Pos e i j -> Ordering

(<) :: Pos e i j -> Pos e i j -> Bool

(<=) :: Pos e i j -> Pos e i j -> Bool

(>) :: Pos e i j -> Pos e i j -> Bool

(>=) :: Pos e i j -> Pos e i j -> Bool

max :: Pos e i j -> Pos e i j -> Pos e i j

min :: Pos e i j -> Pos e i j -> Pos e i j

type Rep (Pos e i j)

Defined in Cornelis.Offsets

type Rep (Pos e i j) = D1 ('MetaData "Pos" "Cornelis.Offsets" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "Pos" 'PrefixI 'True) (S1 ('MetaSel ('Just "p_line") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index 'Line i)) :*: S1 ('MetaSel ('Just "p_col") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index e j))))

data Interval p

Constructors

Interval

Fields

• iStart, iEnd :: !p

Instances

FromJSON AgdaInterval

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser AgdaInterval

parseJSONList :: Value -> Parser [AgdaInterval]

omittedField :: Maybe AgdaInterval

Foldable Interval

Defined in Cornelis.Offsets

Methods

fold :: Monoid m => Interval m -> m

foldMap :: Monoid m => (a -> m) -> Interval a -> m

foldMap' :: Monoid m => (a -> m) -> Interval a -> m

foldr :: (a -> b -> b) -> b -> Interval a -> b

foldr' :: (a -> b -> b) -> b -> Interval a -> b

foldl :: (b -> a -> b) -> b -> Interval a -> b

foldl' :: (b -> a -> b) -> b -> Interval a -> b

foldr1 :: (a -> a -> a) -> Interval a -> a

foldl1 :: (a -> a -> a) -> Interval a -> a

toList :: Interval a -> [a]

null :: Interval a -> Bool

length :: Interval a -> Int

elem :: Eq a => a -> Interval a -> Bool

maximum :: Ord a => Interval a -> a

minimum :: Ord a => Interval a -> a

sum :: Num a => Interval a -> a

product :: Num a => Interval a -> a

Traversable Interval

Defined in Cornelis.Offsets

Methods

traverse :: Applicative f => (a -> f b) -> Interval a -> f (Interval b)

sequenceA :: Applicative f => Interval (f a) -> f (Interval a)

mapM :: Monad m => (a -> m b) -> Interval a -> m (Interval b)

sequence :: Monad m => Interval (m a) -> m (Interval a)

Functor Interval

Defined in Cornelis.Offsets

Methods

fmap :: (a -> b) -> Interval a -> Interval b

(<$) :: a -> Interval b -> Interval a

Generic (Interval p)

Defined in Cornelis.Offsets

Associated Types

type Rep (Interval p) :: Type -> Type

Methods

from :: Interval p -> Rep (Interval p) x

to :: Rep (Interval p) x -> Interval p

Show p => Show (Interval p)

Defined in Cornelis.Offsets

Methods

showsPrec :: Int -> Interval p -> ShowS

show :: Interval p -> String

showList :: [Interval p] -> ShowS

Eq p => Eq (Interval p)

Defined in Cornelis.Offsets

Methods

(==) :: Interval p -> Interval p -> Bool

(/=) :: Interval p -> Interval p -> Bool

Ord p => Ord (Interval p)

Defined in Cornelis.Offsets

Methods

compare :: Interval p -> Interval p -> Ordering

(<) :: Interval p -> Interval p -> Bool

(<=) :: Interval p -> Interval p -> Bool

(>) :: Interval p -> Interval p -> Bool

(>=) :: Interval p -> Interval p -> Bool

max :: Interval p -> Interval p -> Interval p

min :: Interval p -> Interval p -> Interval p

type Rep (Interval p)

Defined in Cornelis.Offsets

type Rep (Interval p) = D1 ('MetaData "Interval" "Cornelis.Offsets" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "iStart") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 p) :*: S1 ('MetaSel ('Just "iEnd") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 p)))

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

toZeroIndexed :: Integral a => a -> Index e 'ZeroIndexed

Mark a raw index as zero-indexed.

toOneIndexed :: Integral a => a -> Index e 'OneIndexed

Mark a raw index as one-indexed.

fromZeroIndexed :: Num a => Index e 'ZeroIndexed -> a

Unwrap a raw zero-indexed index.

fromOneIndexed :: Num a => Index e 'OneIndexed -> a

Unwrap a raw zero-indexed index.

zeroIndex :: Index e 'OneIndexed -> Index e 'ZeroIndexed

Convert from one- to zero-indexed.

oneIndex :: Index e 'ZeroIndexed -> Index e 'OneIndexed

Convert from zero- to one-indexed.

incIndex :: Index e i -> Index e i

Increment index.

(.+) :: Index e i -> Offset e -> Index e i

Add an offset to an index.

(.-.) :: Index e i -> Index e i -> Offset e

offsetPlus :: Offset a -> Offset a -> Offset a

textToBytes :: Text -> Int

Number of bytes in a Text.

charToBytes :: Char -> Int

Number of bytes in a Char.

toBytes :: Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed

Convert a character-based index into a byte-indexed one

fromBytes :: HasCallStack => Text -> Index 'Byte 'ZeroIndexed -> Index 'CodePoint 'ZeroIndexed

Convert a byte-based index into a character-indexed one.

containsPoint :: Ord p => Interval p -> p -> Bool

addCol :: Pos e i j -> Offset e -> Pos e i j