    -- | 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.Arrow (second)
    import Control.DeepSeq
    import Control.Monad

    import Data.Function
    import qualified Data.List as List
    import Data.Maybe
    import Data.Semigroup

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

    import Data.Map.Strict (Map)
    import qualified Data.Map.Strict as Map

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

    import GHC.Generics (Generic)

    import qualified Agda.Syntax.Position as P
    import qualified Agda.Syntax.Common   as Common
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Scope.Base                   ( KindOfName(..) )

    import Agda.Interaction.Highlighting.Range

    import Agda.Utils.List
    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.Utils.String

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- Highlighting information

    -- | Syntactic aspects of the code. (These cannot overlap.)

    data Aspect
      = Comment
      | Keyword
      | String
      | Number
      | Hole
      | Symbol                     -- ^ Symbols like forall, =, ->, etc.
      | PrimitiveType              -- ^ Things like Set and Prop.
      | Name (Maybe NameKind) Bool -- ^ Is the name an operator part?
      | Pragma                     -- ^ Text occurring in pragmas that
                                   --   does not have a more specific
                                   --   aspect.
      | Background                 -- ^ Non-code contents in literate Agda
      | Markup
        -- ^ Delimiters used to separate the Agda code blocks from the
        -- other contents in literate Agda
        deriving (Aspect -> Aspect -> Bool
    (Aspect -> Aspect -> Bool)
    -> (Aspect -> Aspect -> Bool) -> Eq Aspect
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Aspect -> Aspect -> Bool
    $c/= :: Aspect -> Aspect -> Bool
    == :: Aspect -> Aspect -> Bool
    $c== :: Aspect -> Aspect -> Bool
    Eq, Int -> Aspect -> ShowS
    [Aspect] -> ShowS
    Aspect -> String
    (Int -> Aspect -> ShowS)
    -> (Aspect -> String) -> ([Aspect] -> ShowS) -> Show Aspect
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Aspect] -> ShowS
    $cshowList :: [Aspect] -> ShowS
    show :: Aspect -> String
    $cshow :: Aspect -> String
    showsPrec :: Int -> Aspect -> ShowS
    $cshowsPrec :: Int -> Aspect -> ShowS
    Show, (forall x. Aspect -> Rep Aspect x)
    -> (forall x. Rep Aspect x -> Aspect) -> Generic Aspect
    forall x. Rep Aspect x -> Aspect
    forall x. Aspect -> Rep Aspect x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Aspect x -> Aspect
    $cfrom :: forall x. Aspect -> Rep Aspect x
    Generic)

    -- | @NameKind@s are figured out during scope checking.

    data NameKind
      = Bound                         -- ^ Bound variable.
      | Generalizable                 -- ^ Generalizable variable.
                                      --   (This includes generalizable
                                      --   variables that have been
                                      --   generalized).
      | Constructor Common.Induction  -- ^ Inductive or coinductive constructor.
      | Datatype
      | Field                         -- ^ Record field.
      | Function
      | Module                        -- ^ Module name.
      | Postulate
      | Primitive                     -- ^ Primitive.
      | Record                        -- ^ Record type.
      | Argument                      -- ^ Named argument, like x in {x = v}
      | Macro                         -- ^ Macro.
        deriving (NameKind -> NameKind -> Bool
    (NameKind -> NameKind -> Bool)
    -> (NameKind -> NameKind -> Bool) -> Eq NameKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: NameKind -> NameKind -> Bool
    $c/= :: NameKind -> NameKind -> Bool
    == :: NameKind -> NameKind -> Bool
    $c== :: NameKind -> NameKind -> Bool
    Eq, Int -> NameKind -> ShowS
    [NameKind] -> ShowS
    NameKind -> String
    (Int -> NameKind -> ShowS)
    -> (NameKind -> String) -> ([NameKind] -> ShowS) -> Show NameKind
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [NameKind] -> ShowS
    $cshowList :: [NameKind] -> ShowS
    show :: NameKind -> String
    $cshow :: NameKind -> String
    showsPrec :: Int -> NameKind -> ShowS
    $cshowsPrec :: Int -> NameKind -> ShowS
    Show, (forall x. NameKind -> Rep NameKind x)
    -> (forall x. Rep NameKind x -> NameKind) -> Generic NameKind
    forall x. Rep NameKind x -> NameKind
    forall x. NameKind -> Rep NameKind x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep NameKind x -> NameKind
    $cfrom :: forall x. NameKind -> Rep NameKind x
    Generic)

    -- | Other aspects, generated by type checking.
    --   (These can overlap with each other and with 'Aspect's.)

    data OtherAspect
      = Error
      | ErrorWarning
        -- ^ A warning that is considered fatal in the end.
      | DottedPattern
      | UnsolvedMeta
      | UnsolvedConstraint
        -- ^ Unsolved constraint not connected to meta-variable. This
        -- could for instance be an emptyness constraint.
      | TerminationProblem
      | PositivityProblem
      | Deadcode
        -- ^ Used for highlighting unreachable clauses, unreachable RHS
        -- (because of an absurd pattern), etc.
      | ShadowingInTelescope
        -- ^ Used for shadowed repeated variable names in telescopes.
      | CoverageProblem
      | IncompletePattern
        -- ^ When this constructor is used it is probably a good idea to
        -- include a 'note' explaining why the pattern is incomplete.
      | TypeChecks
        -- ^ Code which is being type-checked.
      | MissingDefinition
        -- ^ Function declaration without matching definition
      -- NB: We put CatchallClause last so that it is overwritten by other,
      -- more important, aspects in the emacs mode.
      | CatchallClause
      | ConfluenceProblem
        deriving (OtherAspect -> OtherAspect -> Bool
    (OtherAspect -> OtherAspect -> Bool)
    -> (OtherAspect -> OtherAspect -> Bool) -> Eq OtherAspect
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: OtherAspect -> OtherAspect -> Bool
    $c/= :: OtherAspect -> OtherAspect -> Bool
    == :: OtherAspect -> OtherAspect -> Bool
    $c== :: OtherAspect -> OtherAspect -> Bool
    Eq, Eq OtherAspect
    Eq OtherAspect
    -> (OtherAspect -> OtherAspect -> Ordering)
    -> (OtherAspect -> OtherAspect -> Bool)
    -> (OtherAspect -> OtherAspect -> Bool)
    -> (OtherAspect -> OtherAspect -> Bool)
    -> (OtherAspect -> OtherAspect -> Bool)
    -> (OtherAspect -> OtherAspect -> OtherAspect)
    -> (OtherAspect -> OtherAspect -> OtherAspect)
    -> Ord OtherAspect
    OtherAspect -> OtherAspect -> Bool
    OtherAspect -> OtherAspect -> Ordering
    OtherAspect -> OtherAspect -> OtherAspect
    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
    min :: OtherAspect -> OtherAspect -> OtherAspect
    $cmin :: OtherAspect -> OtherAspect -> OtherAspect
    max :: OtherAspect -> OtherAspect -> OtherAspect
    $cmax :: OtherAspect -> OtherAspect -> OtherAspect
    >= :: OtherAspect -> OtherAspect -> Bool
    $c>= :: OtherAspect -> OtherAspect -> Bool
    > :: OtherAspect -> OtherAspect -> Bool
    $c> :: OtherAspect -> OtherAspect -> Bool
    <= :: OtherAspect -> OtherAspect -> Bool
    $c<= :: OtherAspect -> OtherAspect -> Bool
    < :: OtherAspect -> OtherAspect -> Bool
    $c< :: OtherAspect -> OtherAspect -> Bool
    compare :: OtherAspect -> OtherAspect -> Ordering
    $ccompare :: OtherAspect -> OtherAspect -> Ordering
    Ord, Int -> OtherAspect -> ShowS
    [OtherAspect] -> ShowS
    OtherAspect -> String
    (Int -> OtherAspect -> ShowS)
    -> (OtherAspect -> String)
    -> ([OtherAspect] -> ShowS)
    -> Show OtherAspect
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [OtherAspect] -> ShowS
    $cshowList :: [OtherAspect] -> ShowS
    show :: OtherAspect -> String
    $cshow :: OtherAspect -> String
    showsPrec :: Int -> OtherAspect -> ShowS
    $cshowsPrec :: Int -> OtherAspect -> ShowS
    Show, Int -> OtherAspect
    OtherAspect -> Int
    OtherAspect -> [OtherAspect]
    OtherAspect -> OtherAspect
    OtherAspect -> OtherAspect -> [OtherAspect]
    OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
    (OtherAspect -> OtherAspect)
    -> (OtherAspect -> OtherAspect)
    -> (Int -> OtherAspect)
    -> (OtherAspect -> Int)
    -> (OtherAspect -> [OtherAspect])
    -> (OtherAspect -> OtherAspect -> [OtherAspect])
    -> (OtherAspect -> OtherAspect -> [OtherAspect])
    -> (OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect])
    -> Enum OtherAspect
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
    $cenumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]
    enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
    $cenumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]
    enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
    $cenumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]
    enumFrom :: OtherAspect -> [OtherAspect]
    $cenumFrom :: OtherAspect -> [OtherAspect]
    fromEnum :: OtherAspect -> Int
    $cfromEnum :: OtherAspect -> Int
    toEnum :: Int -> OtherAspect
    $ctoEnum :: Int -> OtherAspect
    pred :: OtherAspect -> OtherAspect
    $cpred :: OtherAspect -> OtherAspect
    succ :: OtherAspect -> OtherAspect
    $csucc :: OtherAspect -> OtherAspect
    Enum, OtherAspect
    OtherAspect -> OtherAspect -> Bounded OtherAspect
    forall a. a -> a -> Bounded a
    maxBound :: OtherAspect
    $cmaxBound :: OtherAspect
    minBound :: OtherAspect
    $cminBound :: OtherAspect
    Bounded, (forall x. OtherAspect -> Rep OtherAspect x)
    -> (forall x. Rep OtherAspect x -> OtherAspect)
    -> Generic OtherAspect
    forall x. Rep OtherAspect x -> OtherAspect
    forall x. OtherAspect -> Rep OtherAspect x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep OtherAspect x -> OtherAspect
    $cfrom :: forall x. OtherAspect -> Rep OtherAspect x
    Generic)

    -- | Meta information which can be associated with a
    -- character\/character range.

    data Aspects = Aspects
      { Aspects -> Maybe Aspect
    aspect       :: Maybe Aspect
      , Aspects -> Set OtherAspect
    otherAspects :: Set OtherAspect
      , Aspects -> String
    note         :: String
        -- ^ This note, if not null, can be displayed as a tool-tip or
        -- something like that. It should contain useful information about
        -- the range (like the module containing a certain identifier, or
        -- the fixity of an operator).
      , Aspects -> Maybe DefinitionSite
    definitionSite :: Maybe DefinitionSite
        -- ^ The definition site of the annotated thing, if applicable and
        --   known.
      , Aspects -> TokenBased
    tokenBased :: !TokenBased
        -- ^ Is this entry token-based?
      }
      deriving (Int -> Aspects -> ShowS
    [Aspects] -> ShowS
    Aspects -> String
    (Int -> Aspects -> ShowS)
    -> (Aspects -> String) -> ([Aspects] -> ShowS) -> Show Aspects
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Aspects] -> ShowS
    $cshowList :: [Aspects] -> ShowS
    show :: Aspects -> String
    $cshow :: Aspects -> String
    showsPrec :: Int -> Aspects -> ShowS
    $cshowsPrec :: Int -> Aspects -> ShowS
    Show, (forall x. Aspects -> Rep Aspects x)
    -> (forall x. Rep Aspects x -> Aspects) -> Generic Aspects
    forall x. Rep Aspects x -> Aspects
    forall x. Aspects -> Rep Aspects x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Aspects x -> Aspects
    $cfrom :: forall x. Aspects -> Rep Aspects x
    Generic)

    data DefinitionSite = DefinitionSite
      { DefinitionSite -> TopLevelModuleName
    defSiteModule :: C.TopLevelModuleName
          -- ^ The defining module.
      , DefinitionSite -> Int
    defSitePos    :: Int
          -- ^ The file position in that module. File positions are
          -- counted from 1.
      , DefinitionSite -> Bool
    defSiteHere   :: Bool
          -- ^ Has this @DefinitionSite@ been created at the defining site of the name?
      , DefinitionSite -> Maybe String
    defSiteAnchor :: Maybe String
          -- ^ A pretty name for the HTML linking.
      }
      deriving (Int -> DefinitionSite -> ShowS
    [DefinitionSite] -> ShowS
    DefinitionSite -> String
    (Int -> DefinitionSite -> ShowS)
    -> (DefinitionSite -> String)
    -> ([DefinitionSite] -> ShowS)
    -> Show DefinitionSite
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [DefinitionSite] -> ShowS
    $cshowList :: [DefinitionSite] -> ShowS
    show :: DefinitionSite -> String
    $cshow :: DefinitionSite -> String
    showsPrec :: Int -> DefinitionSite -> ShowS
    $cshowsPrec :: Int -> DefinitionSite -> ShowS
    Show, (forall x. DefinitionSite -> Rep DefinitionSite x)
    -> (forall x. Rep DefinitionSite x -> DefinitionSite)
    -> Generic DefinitionSite
    forall x. Rep DefinitionSite x -> DefinitionSite
    forall x. DefinitionSite -> Rep DefinitionSite x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep DefinitionSite x -> DefinitionSite
    $cfrom :: forall x. DefinitionSite -> Rep DefinitionSite x
    Generic)

    instance Eq DefinitionSite where
      DefinitionSite TopLevelModuleName
    m Int
    p Bool
    _ Maybe String
    _ == :: DefinitionSite -> DefinitionSite -> Bool
    == DefinitionSite TopLevelModuleName
    m' Int
    p' Bool
    _ Maybe String
    _ = TopLevelModuleName
    m TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == TopLevelModuleName
    m' Bool -> Bool -> Bool
    && Int
    p Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    p'

    -- | Is the highlighting \"token-based\", i.e. based only on
    -- information from the lexer?

    data TokenBased = TokenBased | NotOnlyTokenBased
      deriving (TokenBased -> TokenBased -> Bool
    (TokenBased -> TokenBased -> Bool)
    -> (TokenBased -> TokenBased -> Bool) -> Eq TokenBased
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TokenBased -> TokenBased -> Bool
    $c/= :: TokenBased -> TokenBased -> Bool
    == :: TokenBased -> TokenBased -> Bool
    $c== :: TokenBased -> TokenBased -> Bool
    Eq, Int -> TokenBased -> ShowS
    [TokenBased] -> ShowS
    TokenBased -> String
    (Int -> TokenBased -> ShowS)
    -> (TokenBased -> String)
    -> ([TokenBased] -> ShowS)
    -> Show TokenBased
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TokenBased] -> ShowS
    $cshowList :: [TokenBased] -> ShowS
    show :: TokenBased -> String
    $cshow :: TokenBased -> String
    showsPrec :: Int -> TokenBased -> ShowS
    $cshowsPrec :: Int -> TokenBased -> ShowS
    Show)

    instance Eq Aspects where
      Aspects Maybe Aspect
    a Set OtherAspect
    o String
    _ Maybe DefinitionSite
    d TokenBased
    t == :: Aspects -> Aspects -> Bool
    == Aspects Maybe Aspect
    a' Set OtherAspect
    o' String
    _ Maybe DefinitionSite
    d' TokenBased
    t' =
        (Maybe Aspect
    a, Set OtherAspect
    o, Maybe DefinitionSite
    d, TokenBased
    t) (Maybe Aspect, Set OtherAspect, Maybe DefinitionSite, TokenBased)
    -> (Maybe Aspect, Set OtherAspect, Maybe DefinitionSite,
        TokenBased)
    -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Maybe Aspect
    a', Set OtherAspect
    o', Maybe DefinitionSite
    d', TokenBased
    t')

    -- | 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
    showList :: [RangePair] -> ShowS
    $cshowList :: [RangePair] -> ShowS
    show :: RangePair -> String
    $cshow :: RangePair -> String
    showsPrec :: Int -> RangePair -> ShowS
    $cshowsPrec :: Int -> RangePair -> ShowS
    Show, RangePair -> ()
    (RangePair -> ()) -> NFData RangePair
    forall a. (a -> ()) -> NFData a
    rnf :: RangePair -> ()
    $crnf :: 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
    showList :: [PositionMap] -> ShowS
    $cshowList :: [PositionMap] -> ShowS
    show :: PositionMap -> String
    $cshow :: PositionMap -> String
    showsPrec :: Int -> PositionMap -> ShowS
    $cshowsPrec :: Int -> PositionMap -> ShowS
    Show, PositionMap -> ()
    (PositionMap -> ()) -> NFData PositionMap
    forall a. (a -> ()) -> NFData a
    rnf :: PositionMap -> ()
    $crnf :: 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
    stimes :: forall b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
    $cstimes :: forall hl b. Integral b => b -> DelayedMerge hl -> DelayedMerge hl
    sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl
    $csconcat :: forall hl. NonEmpty (DelayedMerge hl) -> DelayedMerge hl
    <> :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
    $c<> :: forall hl. DelayedMerge hl -> 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
    mconcat :: [DelayedMerge hl] -> DelayedMerge hl
    $cmconcat :: forall hl. [DelayedMerge hl] -> DelayedMerge hl
    mappend :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
    $cmappend :: forall hl. DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl
    mempty :: DelayedMerge hl
    $cmempty :: forall 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 :: DelayedMerge RangePair -> Bool
    highlightingInfoBuilderInvariant =
      (RangePair -> Bool) -> DelayedMerge RangePair -> 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 :: TokenBased
    tokenBased = 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 (DelayedMerge RangePair -> PositionMap
    forall a b. Convert a b => a -> b
    convert (Endo [RangePair] -> DelayedMerge RangePair
    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 :: IntMap Aspects -> PositionMap
    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 :: Int -> Int -> Range
    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 -> DelayedMerge RangePair
    singleton Ranges
    r Aspects
    m = Endo [RangePair] -> DelayedMerge RangePair
    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 :: DelayedMerge RangePair -> IntMap Aspects
    toMap  DelayedMerge RangePair
    f = PositionMap -> IntMap Aspects
    forall a m. IsBasicRangeMap a m => m -> IntMap a
    toMap  (DelayedMerge RangePair -> PositionMap
    forall a b. Convert a b => a -> b
    convert DelayedMerge RangePair
    f :: PositionMap)
      toList :: DelayedMerge RangePair -> [(Range, Aspects)]
    toList DelayedMerge RangePair
    f = HighlightingInfo -> [(Range, Aspects)]
    forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
    toList (DelayedMerge RangePair -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert DelayedMerge RangePair
    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 :: DelayedMerge RangePair -> 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 :: DelayedMerge RangePair -> 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
    (<>)

    -- | Some 'NameKind's are more informative than others.
    instance Semigroup NameKind where
      -- During scope-checking of record, we build a constructor
      -- whose arguments (@Bound@ variables) are the fields.
      -- Later, we process them as @Field@s proper.
      NameKind
    Field    <> :: NameKind -> NameKind -> NameKind
    <> NameKind
    Bound    = NameKind
    Field
      NameKind
    Bound    <> NameKind
    Field    = NameKind
    Field
      -- -- Projections are special functions.
      -- -- TODO necessary?
      -- Field    <> Function = Field
      -- Function <> Field    = Field
      -- TODO: more overwrites?
      NameKind
    k1 <> NameKind
    k2 | NameKind
    k1 NameKind -> NameKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameKind
    k2  = NameKind
    k1
               | Bool
    otherwise = NameKind
    k1 -- TODO: __IMPOSSIBLE__

    -- | @NameKind@ in @Name@ can get more precise.
    instance Semigroup Aspect where
      Name Maybe NameKind
    mk1 Bool
    op1 <> :: Aspect -> Aspect -> Aspect
    <> Name Maybe NameKind
    mk2 Bool
    op2 = Maybe NameKind -> Bool -> Aspect
    Name ((NameKind -> NameKind -> NameKind)
    -> Maybe NameKind -> Maybe NameKind -> Maybe NameKind
    forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
    unionMaybeWith NameKind -> NameKind -> NameKind
    forall a. Semigroup a => a -> a -> a
    (<>) Maybe NameKind
    mk1 Maybe NameKind
    mk2) Bool
    op1
        -- (op1 || op2) breaks associativity
      Aspect
    a1 <> Aspect
    a2 | Aspect
    a1 Aspect -> Aspect -> Bool
    forall a. Eq a => a -> a -> Bool
    == Aspect
    a2  = Aspect
    a1
               | Bool
    otherwise = Aspect
    a1 -- TODO: __IMPOSSIBLE__

    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 :: Maybe Aspect
    -> Set OtherAspect
    -> String
    -> Maybe DefinitionSite
    -> TokenBased
    -> Aspects
    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 :: Maybe Aspect
    -> Set OtherAspect
    -> String
    -> Maybe DefinitionSite
    -> TokenBased
    -> Aspects
    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 :: IntMap Aspects -> PositionMap
    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 :: IntMap Aspects -> PositionMap
    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 NameKind
    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 () -> () -> ()
    `seq` Set OtherAspect -> ()
    forall a. NFData a => a -> ()
    rnf Set OtherAspect
    b () -> () -> ()
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf String
    c () -> () -> ()
    `seq` Maybe DefinitionSite -> ()
    forall a. NFData a => a -> ()
    rnf Maybe DefinitionSite
    d