{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- | 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