{-# 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 Agda.Utils.String
import Agda.Utils.List
import Data.Maybe
import qualified Data.List as List
import Data.Function
import Data.Semigroup
import Control.Applicative ((<$>), (<*>))
import Control.Arrow (second)
import Control.Monad
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
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
data Aspect
= Comment
| Option
| Keyword
| String
| Number
| Symbol
| PrimitiveType
| Name (Maybe NameKind) Bool
deriving (Eq, Show)
data NameKind
= Bound
| Constructor Common.Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
| Argument
| Macro
deriving (Eq, Show)
data OtherAspect
= Error
| DottedPattern
| UnsolvedMeta
| UnsolvedConstraint
| TerminationProblem
| PositivityProblem
| ReachabilityProblem
| CoverageProblem
| IncompletePattern
| CatchallClause
| TypeChecks
deriving (Eq, Show, Enum, Bounded)
data Aspects = Aspects
{ aspect :: Maybe Aspect
, otherAspects :: [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, List.nub o, d, t) == (a', List.nub 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 = List.nub $ ((++) `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 = []
, 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)