    -- | A abstract 'Range' type dedicated to keyword occurrences in the source.

    module Agda.Syntax.Common.KeywordRange
      ( KwRange  -- Do not export the constructor.
      , kwRange
      ) where

    import Control.DeepSeq ( NFData(rnf) )

    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Position

    import Agda.Utils.Null

    -- | Range dedicated to a keyword or fixed token sequence.
    --
    -- Motivation: by lacking a 'SetRange' instance we indicate that it cannot be updated.

    newtype KwRange = KwRange { KwRange -> Range
    theKwRange :: Range }
      deriving (KwRange -> KwRange -> Bool
    (KwRange -> KwRange -> Bool)
    -> (KwRange -> KwRange -> Bool) -> Eq KwRange
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: KwRange -> KwRange -> Bool
    == :: KwRange -> KwRange -> Bool
    $c/= :: KwRange -> KwRange -> Bool
    /= :: KwRange -> KwRange -> Bool
    Eq, Eq KwRange
    Eq KwRange =>
    (KwRange -> KwRange -> Ordering)
    -> (KwRange -> KwRange -> Bool)
    -> (KwRange -> KwRange -> Bool)
    -> (KwRange -> KwRange -> Bool)
    -> (KwRange -> KwRange -> Bool)
    -> (KwRange -> KwRange -> KwRange)
    -> (KwRange -> KwRange -> KwRange)
    -> Ord KwRange
    KwRange -> KwRange -> Bool
    KwRange -> KwRange -> Ordering
    KwRange -> KwRange -> KwRange
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: KwRange -> KwRange -> Ordering
    compare :: KwRange -> KwRange -> Ordering
    $c< :: KwRange -> KwRange -> Bool
    < :: KwRange -> KwRange -> Bool
    $c<= :: KwRange -> KwRange -> Bool
    <= :: KwRange -> KwRange -> Bool
    $c> :: KwRange -> KwRange -> Bool
    > :: KwRange -> KwRange -> Bool
    $c>= :: KwRange -> KwRange -> Bool
    >= :: KwRange -> KwRange -> Bool
    $cmax :: KwRange -> KwRange -> KwRange
    max :: KwRange -> KwRange -> KwRange
    $cmin :: KwRange -> KwRange -> KwRange
    min :: KwRange -> KwRange -> KwRange
    Ord, Int -> KwRange -> ShowS
    [KwRange] -> ShowS
    KwRange -> String
    (Int -> KwRange -> ShowS)
    -> (KwRange -> String) -> ([KwRange] -> ShowS) -> Show KwRange
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> KwRange -> ShowS
    showsPrec :: Int -> KwRange -> ShowS
    $cshow :: KwRange -> String
    show :: KwRange -> String
    $cshowList :: [KwRange] -> ShowS
    showList :: [KwRange] -> ShowS
    Show, KwRange
    KwRange -> Bool
    KwRange -> (KwRange -> Bool) -> Null KwRange
    forall a. a -> (a -> Bool) -> Null a
    $cempty :: KwRange
    empty :: KwRange
    $cnull :: KwRange -> Bool
    null :: KwRange -> Bool
    Null)

    -- | Create a keyword range.

    kwRange :: HasRange a => a -> KwRange
    kwRange :: forall a. HasRange a => a -> KwRange
    kwRange = Range -> KwRange
    KwRange (Range -> KwRange) -> (a -> Range) -> a -> KwRange
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Range
    forall a. HasRange a => a -> Range
    getRange

    -- Instances

    instance HasRange KwRange where
      getRange :: KwRange -> Range
    getRange = KwRange -> Range
    theKwRange

    instance KillRange KwRange where
      killRange :: KwRange -> KwRange
    killRange KwRange
    _ = KwRange
    forall a. Null a => a
    empty

    -- no SetRange instance!!

    instance NFData KwRange where
      rnf :: KwRange -> ()
    rnf KwRange
    _ = ()

    instance Pretty KwRange where
      prettyPrec :: Int -> KwRange -> Doc
    prettyPrec Int
    i = Int -> Range -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    i (Range -> Doc) -> (KwRange -> Range) -> KwRange -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KwRange -> Range
    theKwRange