{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Interaction.Highlighting.Precise
(
Aspect(..)
, NameKind(..)
, OtherAspect(..)
, Aspects(..)
, DefinitionSite(..)
, TokenBased(..)
, File(..)
, HighlightingInfo
, parserBased
, singleton
, several
, merge
, smallestPos
, toMap
, CompressedFile(..)
, compressedFileInvariant
, compress
, decompress
, noHighlightingInRange
, singletonC
, severalC
, splitAtC
, selectC
, smallestPosC
, mergeC
) where
import Control.Applicative ((<$>), (<*>))
import Control.Arrow (second)
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.Set (Set)
import qualified Data.Set as Set
import qualified Agda.Syntax.Position as P
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete as SC
import Agda.Interaction.Highlighting.Range
import Agda.Utils.String
import Agda.Utils.List
data Aspect
= Comment
| Keyword
| String
| Number
| Symbol
| PrimitiveType
| Name (Maybe NameKind) Bool
| Pragma
| Background
| Markup
deriving (Eq, Show)
data NameKind
= Bound
| Generalizable
| Constructor Common.Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
| Argument
| Macro
deriving (Eq, Show)
data OtherAspect
= Error
| DottedPattern
| UnsolvedMeta
| UnsolvedConstraint
| TerminationProblem
| PositivityProblem
| Deadcode
| CoverageProblem
| IncompletePattern
| TypeChecks
| CatchallClause
deriving (Eq, Ord, Show, Enum, Bounded)
data Aspects = Aspects
{ aspect :: Maybe Aspect
, otherAspects :: Set OtherAspect
, note :: Maybe String
, definitionSite :: Maybe DefinitionSite
, tokenBased :: !TokenBased
}
deriving Show
data DefinitionSite = DefinitionSite
{ defSiteModule :: SC.TopLevelModuleName
, defSitePos :: Int
, defSiteHere :: Bool
, defSiteAnchor :: Maybe String
}
deriving Show
instance Eq DefinitionSite where
DefinitionSite m p _ _ == DefinitionSite m' p' _ _ = m == m' && p == p'
data TokenBased = TokenBased | NotOnlyTokenBased
deriving (Eq, Show)
instance Eq Aspects where
Aspects a o _ d t == Aspects a' o' _ d' t' =
(a, o, d, t) == (a', o', d', t')
newtype File = File { mapping :: IntMap Aspects }
deriving (Eq, Show)
type HighlightingInfo = CompressedFile
parserBased :: Aspects
parserBased = mempty { tokenBased = NotOnlyTokenBased }
singleton :: Ranges -> Aspects -> File
singleton rs m = File {
mapping = IntMap.fromAscList [ (p, m) | p <- rangesToPositions rs ] }
several :: [Ranges] -> Aspects -> File
several rs m = mconcat $ map (\r -> singleton r m) rs
instance Semigroup TokenBased where
b1@NotOnlyTokenBased <> b2 = b1
TokenBased <> b2 = b2
instance Monoid TokenBased where
mempty = TokenBased
mappend = (<>)
mergeAspects :: Aspects -> Aspects -> Aspects
mergeAspects m1 m2 = Aspects
{ aspect = (mplus `on` aspect) m1 m2
, otherAspects = (Set.union `on` otherAspects) m1 m2
, note = case (note m1, note m2) of
(Just n1, Just n2) -> Just $
if n1 == n2
then n1
else addFinalNewLine n1 ++ "----\n" ++ n2
(Just n1, Nothing) -> Just n1
(Nothing, Just n2) -> Just n2
(Nothing, Nothing) -> Nothing
, definitionSite = (mplus `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 = Nothing
, definitionSite = Nothing
, tokenBased = mempty
}
mappend = (<>)
merge :: File -> File -> File
merge f1 f2 =
File { mapping = (IntMap.unionWith mappend `on` mapping) f1 f2 }
instance Semigroup File where
(<>) = merge
instance Monoid File where
mempty = File { mapping = IntMap.empty }
mappend = (<>)
smallestPos :: File -> Maybe Int
smallestPos = fmap (fst . fst) . IntMap.minViewWithKey . mapping
toMap :: File -> IntMap Aspects
toMap = mapping
newtype CompressedFile =
CompressedFile { ranges :: [(Range, Aspects)] }
deriving (Eq, Show)
compressedFileInvariant :: CompressedFile -> Bool
compressedFileInvariant (CompressedFile []) = True
compressedFileInvariant (CompressedFile f) =
all rangeInvariant rs &&
all (not . empty) rs &&
and (zipWith (<=) (map to $ init rs) (map from $ tail rs))
where rs = map fst f
compress :: File -> CompressedFile
compress f =
CompressedFile $ map join $ groupBy' p (IntMap.toAscList $ mapping f)
where
p (pos1, m1) (pos2, m2) = pos2 == pos1 + 1 && m1 == m2
join pms = ( Range { from = head ps, to = last ps + 1 }
, head ms
)
where (ps, ms) = unzip pms
decompress :: CompressedFile -> File
decompress =
File .
IntMap.fromList .
concat .
map (\(r, m) -> [ (p, m) | p <- rangeToPositions r ]) .
ranges
noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile
noHighlightingInRange rs (CompressedFile hs) =
CompressedFile $ concatMap clear hs
where
clear (r, i) =
case minus (Ranges [r]) rs of
Ranges [] -> []
Ranges rs -> [ (r, i) | r <- rs ]
singletonC :: Ranges -> Aspects -> CompressedFile
singletonC (Ranges rs) m =
CompressedFile [(r, m) | r <- rs, not (empty r)]
severalC :: [Ranges] -> Aspects -> CompressedFile
severalC rss m = mconcat $ map (\rs -> singletonC rs m) rss
mergeC :: CompressedFile -> CompressedFile -> CompressedFile
mergeC (CompressedFile f1) (CompressedFile f2) =
CompressedFile (mrg f1 f2)
where
mrg [] f2 = f2
mrg f1 [] = f1
mrg (p1@(i1,_):f1) (p2@(i2,_):f2)
| to i1 <= from i2 = p1 : mrg f1 (p2:f2)
| to i2 <= from i1 = p2 : mrg (p1:f1) f2
| to i1 <= to i2 = ps1 ++ mrg f1 (ps2 ++ f2)
| otherwise = ps1 ++ mrg (ps2 ++ f1) f2
where (ps1, ps2) = fuse p1 p2
fuse (i1, m1) (i2, m2) =
( fix [ (Range { from = a, to = b }, ma)
, (Range { from = b, to = c }, mergeAspects m1 m2)
]
, fix [ (Range { from = c, to = d }, md)
]
)
where
[(a, ma), (b, _), (c, _), (d, md)] =
List.sortBy (compare `on` fst)
[(from i1, m1), (to i1, m1), (from i2, m2), (to i2, m2)]
fix = filter (not . empty . fst)
instance Semigroup CompressedFile where
(<>) = mergeC
instance Monoid CompressedFile where
mempty = CompressedFile []
mappend = (<>)
splitAtC :: Int -> CompressedFile ->
(CompressedFile, CompressedFile)
splitAtC p f = (CompressedFile f1, CompressedFile f2)
where
(f1, f2) = split $ ranges f
split [] = ([], [])
split (rx@(r,x) : f)
| p <= from r = ([], rx:f)
| to r <= p = (rx:f1, f2)
| otherwise = ([ (toP, x) ], (fromP, x) : f)
where (f1, f2) = split f
toP = Range { from = from r, to = p }
fromP = Range { from = p, to = to r }
selectC :: P.Range -> CompressedFile -> CompressedFile
selectC r cf = cf'
where
empty = (0,0)
(from, to) = fromMaybe empty (rangeToEndPoints r)
(_, (cf', _)) = (second (splitAtC to)) . splitAtC from $ cf
smallestPosC :: CompressedFile -> Maybe Int
smallestPosC (CompressedFile []) = Nothing
smallestPosC (CompressedFile ((r, _) : _)) = Just (from r)