-- | Types used for precise syntax highlighting.

module Agda.Interaction.Highlighting.Precise
  ( -- * Highlighting information
    Aspect(..)
  , NameKind(..)
  , OtherAspect(..)
  , Aspects(..)
  , DefinitionSite(..)
  , TokenBased(..)
  , RangePair(..)
  , rangePairInvariant
  , PositionMap(..)
  , DelayedMerge(..)
  , delayedMergeInvariant
  , HighlightingInfo
  , highlightingInfoInvariant
  , HighlightingInfoBuilder
  , highlightingInfoBuilderInvariant
    -- ** Operations
  , parserBased
  , kindOfNameToNameKind
  , IsBasicRangeMap(..)
  , RangeMap.several
  , Convert(..)
  , RangeMap.insideAndOutside
  , RangeMap.restrictTo
  ) where

import Prelude hiding (null)

import Control.DeepSeq

import Data.Function (on)
import Data.Semigroup ( Endo(..) )

import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Set (Set)
import qualified Data.Set as Set

import GHC.Generics (Generic)

import qualified Agda.Syntax.Common   as Common
import Agda.Syntax.TopLevelModuleName
import Agda.Syntax.Scope.Base                   ( KindOfName(..) )

import Agda.Utils.Range

import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.RangeMap (RangeMap, IsBasicRangeMap(..))
import qualified Agda.Utils.RangeMap as RangeMap

import Agda.Syntax.Common.Aspect
import Agda.Utils.String

import Agda.Utils.Impossible

-- | A limited kind of syntax highlighting information: a pair
-- consisting of 'Ranges' and 'Aspects'.
--
-- Note the invariant which 'RangePair's should satisfy
-- ('rangePairInvariant').

newtype RangePair = RangePair
  { RangePair -> (Ranges, Aspects)
rangePair :: (Ranges, Aspects)
  }
  deriving (Int -> RangePair -> ShowS
[RangePair] -> ShowS
RangePair -> String
(Int -> RangePair -> ShowS)
-> (RangePair -> String)
-> ([RangePair] -> ShowS)
-> Show RangePair
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RangePair -> ShowS
showsPrec :: Int -> RangePair -> ShowS
$cshow :: RangePair -> String
show :: RangePair -> String
$cshowList :: [RangePair] -> ShowS
showList :: [RangePair] -> ShowS
Show, RangePair -> ()
(RangePair -> ()) -> NFData RangePair
forall a. (a -> ()) -> NFData a
$crnf :: RangePair -> ()
rnf :: RangePair -> ()
NFData)

-- | Invariant for 'RangePair'.

rangePairInvariant :: RangePair -> Bool
rangePairInvariant :: RangePair -> Bool
rangePairInvariant (RangePair (Ranges
rs, Aspects
_)) =
  Ranges -> Bool
rangesInvariant Ranges
rs

-- | Syntax highlighting information, represented by maps from
-- positions to 'Aspects'.
--
-- The first position in the file has number 1.

newtype PositionMap = PositionMap
  { PositionMap -> IntMap Aspects
positionMap :: IntMap Aspects
  }
  deriving (Int -> PositionMap -> ShowS
[PositionMap] -> ShowS
PositionMap -> String
(Int -> PositionMap -> ShowS)
-> (PositionMap -> String)
-> ([PositionMap] -> ShowS)
-> Show PositionMap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PositionMap -> ShowS
showsPrec :: Int -> PositionMap -> ShowS
$cshow :: PositionMap -> String
show :: PositionMap -> String
$cshowList :: [PositionMap] -> ShowS
showList :: [PositionMap] -> ShowS
Show, PositionMap -> ()
(PositionMap -> ()) -> NFData PositionMap
forall a. (a -> ()) -> NFData a
$crnf :: PositionMap -> ()
rnf :: PositionMap -> ()
NFData)

-- | Highlighting info with delayed merging.
--
-- Merging large sets of highlighting info repeatedly might be costly.
-- The idea of this type is to accumulate small pieces of highlighting
-- information, and then to merge them all at the end.
--
-- Note the invariant which values of this type should satisfy
-- ('delayedMergeInvariant').

newtype DelayedMerge hl = DelayedMerge (Endo [hl])
  deriving (NonEmpty (DelayedMerge hl) -> DelayedMerge hl
DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
(DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl)
-> (NonEmpty (DelayedMerge hl) -> DelayedMerge hl)
-> (forall b.
    Integral b =>
    b -> DelayedMerge hl -> DelayedMerge hl)
-> Semigroup (DelayedMerge hl)
forall b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
forall hl. NonEmpty (DelayedMerge hl) -> DelayedMerge hl
forall hl. DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall hl b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
$c<> :: forall hl. DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
<> :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
$csconcat :: forall hl. NonEmpty (DelayedMerge hl) -> DelayedMerge hl
sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl
$cstimes :: forall hl b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
stimes :: forall b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
Semigroup, Semigroup (DelayedMerge hl)
DelayedMerge hl
Semigroup (DelayedMerge hl) =>
DelayedMerge hl
-> (DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl)
-> ([DelayedMerge hl] -> DelayedMerge hl)
-> Monoid (DelayedMerge hl)
[DelayedMerge hl] -> DelayedMerge hl
DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
forall hl. Semigroup (DelayedMerge hl)
forall hl. DelayedMerge hl
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall hl. [DelayedMerge hl] -> DelayedMerge hl
forall hl. DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
$cmempty :: forall hl. DelayedMerge hl
mempty :: DelayedMerge hl
$cmappend :: forall hl. DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
mappend :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
$cmconcat :: forall hl. [DelayedMerge hl] -> DelayedMerge hl
mconcat :: [DelayedMerge hl] -> DelayedMerge hl
Monoid)

instance Show hl => Show (DelayedMerge hl) where
  showsPrec :: Int -> DelayedMerge hl -> ShowS
showsPrec Int
_ (DelayedMerge Endo [hl]
f) =
    String -> ShowS
showString String
"DelayedMerge (Endo (" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    [hl] -> ShowS
forall a. Show a => a -> ShowS
shows (Endo [hl] -> [hl] -> [hl]
forall a. Endo a -> a -> a
appEndo Endo [hl]
f []) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> ShowS
showString String
" ++))"

-- | Invariant for @'DelayedMerge' hl@, parametrised by the invariant
-- for @hl@.
--
-- Additionally the endofunction should be extensionally equal to @(fs
-- '++')@ for some list @fs@.

delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool
delayedMergeInvariant :: forall hl. (hl -> Bool) -> DelayedMerge hl -> Bool
delayedMergeInvariant hl -> Bool
inv (DelayedMerge Endo [hl]
f) =
  (hl -> Bool) -> [hl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all hl -> Bool
inv (Endo [hl] -> [hl] -> [hl]
forall a. Endo a -> a -> a
appEndo Endo [hl]
f [])

-- | Highlighting information.
--
-- Note the invariant which values of this type should satisfy
-- ('highlightingInfoInvariant').
--
-- This is a type synonym in order to make it easy to change to
-- another representation.

type HighlightingInfo = RangeMap Aspects

-- | The invariant for 'HighlightingInfo'.

highlightingInfoInvariant :: HighlightingInfo -> Bool
highlightingInfoInvariant :: HighlightingInfo -> Bool
highlightingInfoInvariant = HighlightingInfo -> Bool
forall a. RangeMap a -> Bool
RangeMap.rangeMapInvariant

-- | A type that is intended to be used when constructing highlighting
-- information.
--
-- Note the invariant which values of this type should satisfy
-- ('highlightingInfoBuilderInvariant').
--
-- This is a type synonym in order to make it easy to change to
-- another representation.
--
-- The type should be an instance of @'IsBasicRangeMap' 'Aspects'@,
-- 'Semigroup' and 'Monoid', and there should be an instance of
-- @'Convert' 'HighlightingInfoBuilder' 'HighlightingInfo'@.

type HighlightingInfoBuilder = DelayedMerge RangePair

-- | The invariant for 'HighlightingInfoBuilder'.
--
-- Additionally the endofunction should be extensionally equal to @(fs
-- '++')@ for some list @fs@.

highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool
highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool
highlightingInfoBuilderInvariant =
  (RangePair -> Bool) -> HighlightingInfoBuilder -> Bool
forall hl. (hl -> Bool) -> DelayedMerge hl -> Bool
delayedMergeInvariant RangePair -> Bool
rangePairInvariant

------------------------------------------------------------------------
-- Creation and conversion

-- | A variant of 'mempty' with 'tokenBased' set to
-- 'NotOnlyTokenBased'.

parserBased :: Aspects
parserBased :: Aspects
parserBased = Aspects
forall a. Monoid a => a
mempty { tokenBased = NotOnlyTokenBased }

-- | Conversion from classification of the scope checker.

kindOfNameToNameKind :: KindOfName -> NameKind
kindOfNameToNameKind :: KindOfName -> NameKind
kindOfNameToNameKind = \case
  -- Inductive is Constructor default, overwritten by CoInductive
  KindOfName
ConName                  -> Induction -> NameKind
Constructor Induction
Common.Inductive
  KindOfName
CoConName                -> Induction -> NameKind
Constructor Induction
Common.CoInductive
  KindOfName
FldName                  -> NameKind
Field
  KindOfName
PatternSynName           -> Induction -> NameKind
Constructor Induction
Common.Inductive
  KindOfName
GeneralizeName           -> NameKind
Generalizable
  KindOfName
DisallowedGeneralizeName -> NameKind
Generalizable
  KindOfName
MacroName                -> NameKind
Macro
  KindOfName
QuotableName             -> NameKind
Function
  KindOfName
DataName                 -> NameKind
Datatype
  KindOfName
RecName                  -> NameKind
Record
  KindOfName
FunName                  -> NameKind
Function
  KindOfName
AxiomName                -> NameKind
Postulate
  KindOfName
PrimName                 -> NameKind
Primitive
  KindOfName
OtherDefName             -> NameKind
Function

instance IsBasicRangeMap Aspects RangePair where
  singleton :: Ranges -> Aspects -> RangePair
singleton Ranges
rs Aspects
m = (Ranges, Aspects) -> RangePair
RangePair (Ranges
rs, Aspects
m)

  toList :: RangePair -> [(Range, Aspects)]
toList (RangePair (Ranges [Range]
rs, Aspects
m)) =
    [ (Range
r, Aspects
m) | Range
r <- [Range]
rs, Bool -> Bool
not (Range -> Bool
forall a. Null a => a -> Bool
null Range
r) ]

  toMap :: RangePair -> IntMap Aspects
toMap RangePair
f = PositionMap -> IntMap Aspects
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap (HighlightingInfoBuilder -> PositionMap
forall a b. Convert a b => a -> b
convert (Endo [RangePair] -> HighlightingInfoBuilder
forall hl. Endo [hl] -> DelayedMerge hl
DelayedMerge (([RangePair] -> [RangePair]) -> Endo [RangePair]
forall a. (a -> a) -> Endo a
Endo (RangePair
f RangePair -> [RangePair] -> [RangePair]
forall a. a -> [a] -> [a]
:))) :: PositionMap)

instance IsBasicRangeMap Aspects PositionMap where
  singleton :: Ranges -> Aspects -> PositionMap
singleton Ranges
rs Aspects
m = PositionMap
    { positionMap :: IntMap Aspects
positionMap =
      [(Int, Aspects)] -> IntMap Aspects
forall a. [(Int, a)] -> IntMap a
IntMap.fromDistinctAscList [ (Int
p, Aspects
m) | Int
p <- Ranges -> [Int]
rangesToPositions Ranges
rs ]
    }

  toList :: PositionMap -> [(Range, Aspects)]
toList = (NonEmpty (Int, Aspects) -> (Range, Aspects))
-> [NonEmpty (Int, Aspects)] -> [(Range, Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty (Int, Aspects) -> (Range, Aspects)
forall {b}. NonEmpty (Int, b) -> (Range, b)
join ([NonEmpty (Int, Aspects)] -> [(Range, Aspects)])
-> (PositionMap -> [NonEmpty (Int, Aspects)])
-> PositionMap
-> [(Range, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Aspects) -> (Int, Aspects) -> Bool)
-> [(Int, Aspects)] -> [NonEmpty (Int, Aspects)]
forall a. (a -> a -> Bool) -> [a] -> [List1 a]
List1.groupBy' (Int, Aspects) -> (Int, Aspects) -> Bool
forall {a} {a}. (Num a, Eq a, Eq a) => (a, a) -> (a, a) -> Bool
p ([(Int, Aspects)] -> [NonEmpty (Int, Aspects)])
-> (PositionMap -> [(Int, Aspects)])
-> PositionMap
-> [NonEmpty (Int, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap Aspects -> [(Int, Aspects)]
forall a. IntMap a -> [(Int, a)]
IntMap.toAscList (IntMap Aspects -> [(Int, Aspects)])
-> (PositionMap -> IntMap Aspects)
-> PositionMap
-> [(Int, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PositionMap -> IntMap Aspects
positionMap
    where
    p :: (a, a) -> (a, a) -> Bool
p (a
pos1, a
m1) (a
pos2, a
m2) = a
pos2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
pos1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 Bool -> Bool -> Bool
&& a
m1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
m2
    join :: NonEmpty (Int, b) -> (Range, b)
join NonEmpty (Int, b)
pms = ( Range { from :: Int
from = NonEmpty Int -> Int
forall a. NonEmpty a -> a
List1.head NonEmpty Int
ps, to :: Int
to = NonEmpty Int -> Int
forall a. NonEmpty a -> a
List1.last NonEmpty Int
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
               , NonEmpty b -> b
forall a. NonEmpty a -> a
List1.head NonEmpty b
ms
               )
      where (NonEmpty Int
ps, NonEmpty b
ms) = NonEmpty (Int, b) -> (NonEmpty Int, NonEmpty b)
forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
List1.unzip NonEmpty (Int, b)
pms

  toMap :: PositionMap -> IntMap Aspects
toMap = PositionMap -> IntMap Aspects
positionMap

instance Semigroup a =>
         IsBasicRangeMap a (DelayedMerge (RangeMap a)) where
  singleton :: Ranges -> a -> DelayedMerge (RangeMap a)
singleton Ranges
r a
m = Endo [RangeMap a] -> DelayedMerge (RangeMap a)
forall hl. Endo [hl] -> DelayedMerge hl
DelayedMerge (([RangeMap a] -> [RangeMap a]) -> Endo [RangeMap a]
forall a. (a -> a) -> Endo a
Endo (Ranges -> a -> RangeMap a
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
r a
m RangeMap a -> [RangeMap a] -> [RangeMap a]
forall a. a -> [a] -> [a]
:))

  toMap :: DelayedMerge (RangeMap a) -> IntMap a
toMap  DelayedMerge (RangeMap a)
f = RangeMap a -> IntMap a
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap  (DelayedMerge (RangeMap a) -> RangeMap a
forall a b. Convert a b => a -> b
convert DelayedMerge (RangeMap a)
f :: RangeMap a)
  toList :: DelayedMerge (RangeMap a) -> [(Range, a)]
toList DelayedMerge (RangeMap a)
f = RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList (DelayedMerge (RangeMap a) -> RangeMap a
forall a b. Convert a b => a -> b
convert DelayedMerge (RangeMap a)
f :: RangeMap a)

instance IsBasicRangeMap Aspects (DelayedMerge RangePair) where
  singleton :: Ranges -> Aspects -> HighlightingInfoBuilder
singleton Ranges
r Aspects
m = Endo [RangePair] -> HighlightingInfoBuilder
forall hl. Endo [hl] -> DelayedMerge hl
DelayedMerge (([RangePair] -> [RangePair]) -> Endo [RangePair]
forall a. (a -> a) -> Endo a
Endo (Ranges -> Aspects -> RangePair
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
r Aspects
m RangePair -> [RangePair] -> [RangePair]
forall a. a -> [a] -> [a]
:))

  toMap :: HighlightingInfoBuilder -> IntMap Aspects
toMap  HighlightingInfoBuilder
f = PositionMap -> IntMap Aspects
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap  (HighlightingInfoBuilder -> PositionMap
forall a b. Convert a b => a -> b
convert HighlightingInfoBuilder
f :: PositionMap)
  toList :: HighlightingInfoBuilder -> [(Range, Aspects)]
toList HighlightingInfoBuilder
f = HighlightingInfo -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList (HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert HighlightingInfoBuilder
f :: RangeMap Aspects)

instance IsBasicRangeMap Aspects (DelayedMerge PositionMap) where
  singleton :: Ranges -> Aspects -> DelayedMerge PositionMap
singleton Ranges
r Aspects
m = Endo [PositionMap] -> DelayedMerge PositionMap
forall hl. Endo [hl] -> DelayedMerge hl
DelayedMerge (([PositionMap] -> [PositionMap]) -> Endo [PositionMap]
forall a. (a -> a) -> Endo a
Endo (Ranges -> Aspects -> PositionMap
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
r Aspects
m PositionMap -> [PositionMap] -> [PositionMap]
forall a. a -> [a] -> [a]
:))

  toMap :: DelayedMerge PositionMap -> IntMap Aspects
toMap  DelayedMerge PositionMap
f = PositionMap -> IntMap Aspects
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap  (DelayedMerge PositionMap -> PositionMap
forall a b. Convert a b => a -> b
convert DelayedMerge PositionMap
f :: PositionMap)
  toList :: DelayedMerge PositionMap -> [(Range, Aspects)]
toList DelayedMerge PositionMap
f = PositionMap -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList (DelayedMerge PositionMap -> PositionMap
forall a b. Convert a b => a -> b
convert DelayedMerge PositionMap
f :: PositionMap)

-- | Conversion between different types.

class Convert a b where
  convert :: a -> b

instance Monoid hl => Convert (DelayedMerge hl) hl where
  convert :: DelayedMerge hl -> hl
convert (DelayedMerge Endo [hl]
f) = [hl] -> hl
forall a. Monoid a => [a] -> a
mconcat (Endo [hl] -> [hl] -> [hl]
forall a. Endo a -> a -> a
appEndo Endo [hl]
f [])

instance Convert (RangeMap Aspects) (RangeMap Aspects) where
  convert :: HighlightingInfo -> HighlightingInfo
convert = HighlightingInfo -> HighlightingInfo
forall a. a -> a
id

instance Convert PositionMap (RangeMap Aspects) where
  convert :: PositionMap -> HighlightingInfo
convert =
    [(Range, Aspects)] -> HighlightingInfo
forall a. [(Range, a)] -> RangeMap a
RangeMap.fromNonOverlappingNonEmptyAscendingList ([(Range, Aspects)] -> HighlightingInfo)
-> (PositionMap -> [(Range, Aspects)])
-> PositionMap
-> HighlightingInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    PositionMap -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList

instance Convert (DelayedMerge PositionMap) (RangeMap Aspects) where
  convert :: DelayedMerge PositionMap -> HighlightingInfo
convert DelayedMerge PositionMap
f = PositionMap -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (DelayedMerge PositionMap -> PositionMap
forall a b. Convert a b => a -> b
convert DelayedMerge PositionMap
f :: PositionMap)

instance Convert (DelayedMerge RangePair) PositionMap where
  convert :: HighlightingInfoBuilder -> PositionMap
convert (DelayedMerge Endo [RangePair]
f) =
    IntMap Aspects -> PositionMap
PositionMap (IntMap Aspects -> PositionMap) -> IntMap Aspects -> PositionMap
forall a b. (a -> b) -> a -> b
$
    (Aspects -> Aspects -> Aspects)
-> [(Int, Aspects)] -> IntMap Aspects
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMap.fromListWith ((Aspects -> Aspects -> Aspects) -> Aspects -> Aspects -> Aspects
forall a b c. (a -> b -> c) -> b -> a -> c
flip Aspects -> Aspects -> Aspects
forall a. Semigroup a => a -> a -> a
(<>))
      [ (Int
p, Aspects
m)
      | RangePair (Ranges
r, Aspects
m) <- Endo [RangePair] -> [RangePair] -> [RangePair]
forall a. Endo a -> a -> a
appEndo Endo [RangePair]
f []
      , Int
p                <- Ranges -> [Int]
rangesToPositions Ranges
r
      ]

instance Convert (DelayedMerge RangePair) (RangeMap Aspects) where
  convert :: HighlightingInfoBuilder -> HighlightingInfo
convert (DelayedMerge Endo [RangePair]
f) =
    [HighlightingInfo] -> HighlightingInfo
forall a. Monoid a => [a] -> a
mconcat
      [ Ranges -> Aspects -> HighlightingInfo
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
r Aspects
m
      | RangePair (Ranges
r, Aspects
m) <- Endo [RangePair] -> [RangePair] -> [RangePair]
forall a. Endo a -> a -> a
appEndo Endo [RangePair]
f []
      ]

------------------------------------------------------------------------
-- Merging

instance Semigroup TokenBased where
  b1 :: TokenBased
b1@TokenBased
NotOnlyTokenBased <> :: TokenBased -> TokenBased -> TokenBased
<> TokenBased
b2 = TokenBased
b1
  TokenBased
TokenBased           <> TokenBased
b2 = TokenBased
b2

instance Monoid TokenBased where
  mempty :: TokenBased
mempty  = TokenBased
TokenBased
  mappend :: TokenBased -> TokenBased -> TokenBased
mappend = TokenBased -> TokenBased -> TokenBased
forall a. Semigroup a => a -> a -> a
(<>)


instance Semigroup DefinitionSite where
  DefinitionSite
d1 <> :: DefinitionSite -> DefinitionSite -> DefinitionSite
<> DefinitionSite
d2 | DefinitionSite
d1 DefinitionSite -> DefinitionSite -> Bool
forall a. Eq a => a -> a -> Bool
== DefinitionSite
d2  = DefinitionSite
d1
           | Bool
otherwise = DefinitionSite
d1 -- TODO: __IMPOSSIBLE__

-- | Merges meta information.

mergeAspects :: Aspects -> Aspects -> Aspects
mergeAspects :: Aspects -> Aspects -> Aspects
mergeAspects Aspects
m1 Aspects
m2 = Aspects
  { aspect :: Maybe Aspect
aspect       = ((Aspect -> Aspect -> Aspect)
-> Maybe Aspect -> Maybe Aspect -> Maybe Aspect
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith Aspect -> Aspect -> Aspect
forall a. Semigroup a => a -> a -> a
(<>) (Maybe Aspect -> Maybe Aspect -> Maybe Aspect)
-> (Aspects -> Maybe Aspect) -> Aspects -> Aspects -> Maybe Aspect
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Aspects -> Maybe Aspect
aspect) Aspects
m1 Aspects
m2
  , otherAspects :: Set OtherAspect
otherAspects = (Set OtherAspect -> Set OtherAspect -> Set OtherAspect
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set OtherAspect -> Set OtherAspect -> Set OtherAspect)
-> (Aspects -> Set OtherAspect)
-> Aspects
-> Aspects
-> Set OtherAspect
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Aspects -> Set OtherAspect
otherAspects) Aspects
m1 Aspects
m2
  , note :: String
note         = case (Aspects -> String
note Aspects
m1, Aspects -> String
note Aspects
m2) of
      (String
n1, String
"") -> String
n1
      (String
"", String
n2) -> String
n2
      (String
n1, String
n2)
        | String
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n2  -> String
n1
        | Bool
otherwise -> ShowS
addFinalNewLine String
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"----\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n2
  , definitionSite :: Maybe DefinitionSite
definitionSite = ((DefinitionSite -> DefinitionSite -> DefinitionSite)
-> Maybe DefinitionSite
-> Maybe DefinitionSite
-> Maybe DefinitionSite
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith DefinitionSite -> DefinitionSite -> DefinitionSite
forall a. Semigroup a => a -> a -> a
(<>) (Maybe DefinitionSite
 -> Maybe DefinitionSite -> Maybe DefinitionSite)
-> (Aspects -> Maybe DefinitionSite)
-> Aspects
-> Aspects
-> Maybe DefinitionSite
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Aspects -> Maybe DefinitionSite
definitionSite) Aspects
m1 Aspects
m2
  , tokenBased :: TokenBased
tokenBased     = Aspects -> TokenBased
tokenBased Aspects
m1 TokenBased -> TokenBased -> TokenBased
forall a. Semigroup a => a -> a -> a
<> Aspects -> TokenBased
tokenBased Aspects
m2
  }

instance Semigroup Aspects where
  <> :: Aspects -> Aspects -> Aspects
(<>) = Aspects -> Aspects -> Aspects
mergeAspects

instance Monoid Aspects where
  mempty :: Aspects
mempty = Aspects
    { aspect :: Maybe Aspect
aspect         = Maybe Aspect
forall a. Maybe a
Nothing
    , otherAspects :: Set OtherAspect
otherAspects   = Set OtherAspect
forall a. Set a
Set.empty
    , note :: String
note           = []
    , definitionSite :: Maybe DefinitionSite
definitionSite = Maybe DefinitionSite
forall a. Maybe a
Nothing
    , tokenBased :: TokenBased
tokenBased     = TokenBased
forall a. Monoid a => a
mempty
    }
  mappend :: Aspects -> Aspects -> Aspects
mappend = Aspects -> Aspects -> Aspects
forall a. Semigroup a => a -> a -> a
(<>)

instance Semigroup PositionMap where
  PositionMap
f1 <> :: PositionMap -> PositionMap -> PositionMap
<> PositionMap
f2 = PositionMap
    { positionMap :: IntMap Aspects
positionMap = ((Aspects -> Aspects -> Aspects)
-> IntMap Aspects -> IntMap Aspects -> IntMap Aspects
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith Aspects -> Aspects -> Aspects
forall a. Monoid a => a -> a -> a
mappend (IntMap Aspects -> IntMap Aspects -> IntMap Aspects)
-> (PositionMap -> IntMap Aspects)
-> PositionMap
-> PositionMap
-> IntMap Aspects
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PositionMap -> IntMap Aspects
positionMap) PositionMap
f1 PositionMap
f2 }

instance Monoid PositionMap where
  mempty :: PositionMap
mempty  = PositionMap { positionMap :: IntMap Aspects
positionMap = IntMap Aspects
forall a. IntMap a
IntMap.empty }
  mappend :: PositionMap -> PositionMap -> PositionMap
mappend = PositionMap -> PositionMap -> PositionMap
forall a. Semigroup a => a -> a -> a
(<>)

------------------------------------------------------------------------
-- NFData instances

instance NFData Aspect
instance NFData OtherAspect
instance NFData DefinitionSite

instance NFData Aspects where
  rnf :: Aspects -> ()
rnf (Aspects Maybe Aspect
a Set OtherAspect
b String
c Maybe DefinitionSite
d TokenBased
_) = Maybe Aspect -> ()
forall a. NFData a => a -> ()
rnf Maybe Aspect
a () -> () -> ()
forall a b. a -> b -> b
`seq` Set OtherAspect -> ()
forall a. NFData a => a -> ()
rnf Set OtherAspect
b () -> () -> ()
forall a b. a -> b -> b
`seq` String -> ()
forall a. NFData a => a -> ()
rnf String
c () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe DefinitionSite -> ()
forall a. NFData a => a -> ()
rnf Maybe DefinitionSite
d