module Agda.Interaction.Highlighting.Precise
(
Aspect(..)
, NameKind(..)
, OtherAspect(..)
, Aspects(..)
, File
, HighlightingInfo
, singleton
, several
, smallestPos
, toMap
, CompressedFile(..)
, compressedFileInvariant
, compress
, decompress
, noHighlightingInRange
, singletonC
, severalC
, splitAtC
, smallestPosC
, Agda.Interaction.Highlighting.Precise.tests
) where
import Agda.Utils.TestHelpers
import Agda.Utils.String
import Agda.Utils.List hiding (tests)
import Data.List
import Data.Function
import Data.Monoid
import Control.Applicative ((<$>), (<*>))
import Control.Monad
import Agda.Utils.QuickCheck
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Typeable (Typeable)
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete as SC
import Agda.Interaction.Highlighting.Range
data Aspect
= Comment
| Keyword
| String
| Number
| Symbol
| PrimitiveType
| Name (Maybe NameKind) Bool
deriving (Eq, Show, Typeable)
data NameKind
= Bound
| Constructor Common.Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
| Argument
deriving (Eq, Show, Typeable)
data OtherAspect
= Error
| DottedPattern
| UnsolvedMeta
| UnsolvedConstraint
| TerminationProblem
| IncompletePattern
| TypeChecks
deriving (Eq, Show, Enum, Bounded, Typeable)
data Aspects = Aspects
{ aspect :: Maybe Aspect
, otherAspects :: [OtherAspect]
, note :: Maybe String
, definitionSite :: Maybe (SC.TopLevelModuleName, Int)
}
deriving (Eq, Show, Typeable)
newtype File = File { mapping :: IntMap Aspects }
deriving (Eq, Show, Typeable)
type HighlightingInfo = CompressedFile
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
mergeAspects :: Aspects -> Aspects -> Aspects
mergeAspects m1 m2 = Aspects
{ aspect = (mplus `on` aspect) m1 m2
, otherAspects = 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
}
instance Monoid Aspects where
mempty = Aspects
{ aspect = Nothing
, otherAspects = []
, note = Nothing
, definitionSite = Nothing
}
mappend = mergeAspects
merge :: File -> File -> File
merge f1 f2 =
File { mapping = (IntMap.unionWith mappend `on` mapping) f1 f2 }
instance Monoid File where
mempty = File { mapping = IntMap.empty }
mappend = merge
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, Typeable)
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
prop_compress :: File -> Bool
prop_compress f =
compressedFileInvariant c
&&
decompress c == f
where c = compress f
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)]
prop_singleton :: Ranges -> Aspects -> Bool
prop_singleton rs m = singleton rs m == decompress (singletonC rs m)
severalC :: [Ranges] -> Aspects -> CompressedFile
severalC rss m = mconcat $ map (\rs -> singletonC rs m) rss
prop_several :: [Ranges] -> Aspects -> Bool
prop_several rss m = several rss m == decompress (severalC rss m)
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)] =
sortBy (compare `on` fst)
[(from i1, m1), (to i1, m1), (from i2, m2), (to i2, m2)]
fix = filter (not . empty . fst)
prop_merge :: File -> File -> Bool
prop_merge f1 f2 =
merge f1 f2 == decompress (mergeC (compress f1) (compress f2))
instance Monoid CompressedFile where
mempty = CompressedFile []
mappend = mergeC
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 }
prop_splitAtC :: Int -> CompressedFile -> Bool
prop_splitAtC p f =
all (< p) (positions f1) &&
all (>= p) (positions f2) &&
decompress (mergeC f1 f2) == decompress f
where
(f1, f2) = splitAtC p f
positions = IntMap.keys . toMap . decompress
smallestPosC :: CompressedFile -> Maybe Int
smallestPosC (CompressedFile []) = Nothing
smallestPosC (CompressedFile ((r, _) : _)) = Just (from r)
prop_smallestPos :: CompressedFile -> Bool
prop_smallestPos f = smallestPos (decompress f) == smallestPosC f
instance Arbitrary Aspect where
arbitrary =
frequency [ (3, elements [ Comment, Keyword, String, Number
, Symbol, PrimitiveType ])
, (1, liftM2 Name (maybeGen arbitrary) arbitrary)
]
shrink Name{} = [Comment]
shrink _ = []
instance CoArbitrary Aspect where
coarbitrary Comment = variant 0
coarbitrary Keyword = variant 1
coarbitrary String = variant 2
coarbitrary Number = variant 3
coarbitrary Symbol = variant 4
coarbitrary PrimitiveType = variant 5
coarbitrary (Name nk b) =
variant 6 . maybeCoGen coarbitrary nk . coarbitrary b
instance Arbitrary NameKind where
arbitrary = oneof $ [liftM Constructor arbitrary] ++
map return [ Bound
, Datatype
, Field
, Function
, Module
, Postulate
, Primitive
, Record
]
shrink Constructor{} = [Bound]
shrink _ = []
instance CoArbitrary NameKind where
coarbitrary Bound = variant 0
coarbitrary (Constructor ind) = variant 1 . coarbitrary ind
coarbitrary Datatype = variant 2
coarbitrary Field = variant 3
coarbitrary Function = variant 4
coarbitrary Module = variant 5
coarbitrary Postulate = variant 6
coarbitrary Primitive = variant 7
coarbitrary Record = variant 8
coarbitrary Argument = variant 9
instance Arbitrary OtherAspect where
arbitrary = elements [minBound .. maxBound]
instance CoArbitrary OtherAspect where
coarbitrary = coarbitrary . fromEnum
instance Arbitrary Aspects where
arbitrary = do
aspect <- arbitrary
other <- arbitrary
note <- maybeGen string
defSite <- arbitrary
return (Aspects { aspect = aspect, otherAspects = other
, note = note, definitionSite = defSite })
where string = listOfElements "abcdefABCDEF/\\.\"'@()åäö\n"
shrink (Aspects a o n d) =
[ Aspects a o n d | a <- shrink a ] ++
[ Aspects a o n d | o <- shrink o ] ++
[ Aspects a o n d | n <- shrink n ] ++
[ Aspects a o n d | d <- shrink d ]
instance CoArbitrary Aspects where
coarbitrary (Aspects aspect otherAspects note defSite) =
coarbitrary aspect .
coarbitrary otherAspects .
coarbitrary note .
coarbitrary defSite
instance Arbitrary File where
arbitrary = fmap (File . IntMap.fromList) $ listOf arbitrary
shrink = map (File . IntMap.fromList) . shrink . IntMap.toList . toMap
instance CoArbitrary File where
coarbitrary (File rs) = coarbitrary (IntMap.toAscList rs)
instance Arbitrary CompressedFile where
arbitrary = do
rs <- (\ns1 ns2 -> toRanges $ sort $
ns1 ++ concatMap (\n -> [n, succ n]) (ns2 :: [Int])) <$>
arbitrary <*> arbitrary
CompressedFile <$> mapM (\r -> (,) r <$> arbitrary) rs
where
toRanges (f : t : rs)
| f == t = toRanges (t : rs)
| otherwise = Range { from = f, to = t } :
toRanges (case rs of
f : rs | t == f -> rs
_ -> rs)
toRanges _ = []
shrink (CompressedFile f) = CompressedFile <$> shrink f
tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Precise"
[ quickCheck' compressedFileInvariant
, quickCheck' (all compressedFileInvariant . shrink)
, quickCheck' (\r m -> compressedFileInvariant $ singletonC r m)
, quickCheck' (\rs m -> compressedFileInvariant $ severalC rs m)
, quickCheck' (\f1 f2 -> compressedFileInvariant $ mergeC f1 f2)
, quickCheck' (\i f -> all compressedFileInvariant $
(\(f1, f2) -> [f1, f2]) $
splitAtC i f)
, quickCheck' prop_compress
, quickCheck' prop_singleton
, quickCheck' prop_several
, quickCheck' prop_merge
, quickCheck' prop_splitAtC
, quickCheck' prop_smallestPos
]