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