content: -- | 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)
    }
    deriving (Show, NFData)
  
  -- | Invariant for 'RangePair'.
  
  rangePairInvariant :: RangePair -> Bool
  rangePairInvariant (RangePair (rs, _)) =
    rangesInvariant 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
    }
    deriving (Show, 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 (Semigroup, Monoid)
  
  instance Show hl => Show (DelayedMerge hl) where
    showsPrec _ (DelayedMerge f) =
      showString "DelayedMerge (Endo (" .
      shows (appEndo f []) .
      showString " ++))"
  
  -- | 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 inv (DelayedMerge f) =
    all inv (appEndo 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 = 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 =
    delayedMergeInvariant rangePairInvariant
  
  ------------------------------------------------------------------------
  -- Creation and conversion
  
  -- | A variant of 'mempty' with 'tokenBased' set to
  -- 'NotOnlyTokenBased'.
  
  parserBased :: Aspects
  parserBased = mempty { tokenBased = NotOnlyTokenBased }
  
  -- | Conversion from classification of the scope checker.
  
  kindOfNameToNameKind :: KindOfName -> NameKind
  kindOfNameToNameKind = \case
    -- Inductive is Constructor default, overwritten by CoInductive
    ConName                  -> Constructor Common.Inductive
    CoConName                -> Constructor Common.CoInductive
    FldName                  -> Field
    PatternSynName           -> Constructor Common.Inductive
    GeneralizeName           -> Generalizable
    DisallowedGeneralizeName -> Generalizable
    MacroName                -> Macro
    QuotableName             -> Function
    DataName                 -> Datatype
    RecName                  -> Record
    FunName                  -> Function
    AxiomName                -> Postulate
    PrimName                 -> Primitive
    OtherDefName             -> Function
  
  instance IsBasicRangeMap Aspects RangePair where
    singleton rs m = RangePair (rs, m)
  
    toList (RangePair (Ranges rs, m)) =
      [ (r, m) | r <- rs, not (null r) ]
  
    toMap f = toMap (convert (DelayedMerge (Endo (f :))) :: PositionMap)
  
  instance IsBasicRangeMap Aspects PositionMap where
    singleton rs m = PositionMap
      { positionMap =
        IntMap.fromDistinctAscList [ (p, m) | p <- rangesToPositions rs ]
      }
  
    toList = map join . List1.groupBy' p . IntMap.toAscList . positionMap
      where
      p (pos1, m1) (pos2, m2) = pos2 == pos1 + 1 && m1 == m2
      join pms = ( Range { from = List1.head ps, to = List1.last ps + 1 }
                 , List1.head ms
                 )
        where (ps, ms) = List1.unzip pms
  
    toMap = positionMap
  
  instance Semigroup a =>
           IsBasicRangeMap a (DelayedMerge (RangeMap a)) where
    singleton r m = DelayedMerge (Endo (singleton r m :))
  
    toMap  f = toMap  (convert f :: RangeMap a)
    toList f = toList (convert f :: RangeMap a)
  
  instance IsBasicRangeMap Aspects (DelayedMerge RangePair) where
    singleton r m = DelayedMerge (Endo (singleton r m :))
  
    toMap  f = toMap  (convert f :: PositionMap)
    toList f = toList (convert f :: RangeMap Aspects)
  
  instance IsBasicRangeMap Aspects (DelayedMerge PositionMap) where
    singleton r m = DelayedMerge (Endo (singleton r m :))
  
    toMap  f = toMap  (convert f :: PositionMap)
    toList f = toList (convert f :: PositionMap)
  
  -- | Conversion between different types.
  
  class Convert a b where
    convert :: a -> b
  
  instance Monoid hl => Convert (DelayedMerge hl) hl where
    convert (DelayedMerge f) = mconcat (appEndo f [])
  
  instance Convert (RangeMap Aspects) (RangeMap Aspects) where
    convert = id
  
  instance Convert PositionMap (RangeMap Aspects) where
    convert =
      RangeMap.fromNonOverlappingNonEmptyAscendingList .
      toList
  
  instance Convert (DelayedMerge PositionMap) (RangeMap Aspects) where
    convert f = convert (convert f :: PositionMap)
  
  instance Convert (DelayedMerge RangePair) PositionMap where
    convert (DelayedMerge f) =
      PositionMap $
      IntMap.fromListWith (flip (<>))
        [ (p, m)
        | RangePair (r, m) <- appEndo f []
        , p                <- rangesToPositions r
        ]
  
  instance Convert (DelayedMerge RangePair) (RangeMap Aspects) where
    convert (DelayedMerge f) =
      mconcat
        [ singleton r m
        | RangePair (r, m) <- appEndo f []
        ]
  
  ------------------------------------------------------------------------
  -- Merging
  
  instance Semigroup TokenBased where
    b1@NotOnlyTokenBased <> b2 = b1
    TokenBased           <> b2 = b2
  
  instance Monoid TokenBased where
    mempty  = TokenBased
    mappend = (<>)
  
  
  instance Semigroup DefinitionSite where
    d1 <> d2 | d1 == d2  = d1
             | otherwise = d1 -- TODO: __IMPOSSIBLE__
  
  -- | Merges meta information.
  
  mergeAspects :: Aspects -> Aspects -> Aspects
  mergeAspects m1 m2 = Aspects
    { aspect       = (unionMaybeWith (<>) `on` aspect) m1 m2
    , otherAspects = (Set.union `on` otherAspects) m1 m2
    , note         = case (note m1, note m2) of
        (n1, "") -> n1
        ("", n2) -> n2
        (n1, n2)
          | n1 == n2  -> n1
          | otherwise -> addFinalNewLine n1 ++ "----\n" ++ n2
    , definitionSite = (unionMaybeWith (<>) `on` definitionSite) m1 m2
    , tokenBased     = tokenBased m1 <> tokenBased m2
    }
  
  instance Semigroup Aspects where
    (<>) = mergeAspects
  
  instance Monoid Aspects where
    mempty = Aspects
      { aspect         = Nothing
      , otherAspects   = Set.empty
      , note           = []
      , definitionSite = Nothing
      , tokenBased     = mempty
      }
    mappend = (<>)
  
  instance Semigroup PositionMap where
    f1 <> f2 = PositionMap
      { positionMap = (IntMap.unionWith mappend `on` positionMap) f1 f2 }
  
  instance Monoid PositionMap where
    mempty  = PositionMap { positionMap = IntMap.empty }
    mappend = (<>)
  