module Agda.Interaction.Highlighting.Precise
( Aspect(..)
, NameKind(..)
, OtherAspect(..)
, MetaInfo(..)
, File
, HighlightingInfo
, singleton
, several
, smallestPos
, toMap
, CompressedFile
, compress
, decompress
, 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.Monad
import Agda.Utils.QuickCheck
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Generics (Typeable, Data)
import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Common as C
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)
data NameKind
= Bound
| Constructor C.Induction
| Datatype
| Field
| Function
| Module
| Postulate
| Primitive
| Record
deriving (Eq, Show, Typeable, Data)
data OtherAspect
= Error
| DottedPattern
| UnsolvedMeta
| TerminationProblem
| IncompletePattern
deriving (Eq, Show, Enum, Bounded, Typeable, Data)
data MetaInfo = MetaInfo
{ aspect :: Maybe Aspect
, otherAspects :: [OtherAspect]
, note :: Maybe String
, definitionSite :: Maybe (SC.TopLevelModuleName, Integer)
}
deriving (Eq, Show, Typeable, Data)
newtype File = File { mapping :: Map Integer MetaInfo }
deriving (Eq, Show, Typeable, Data)
smallestPos :: File -> Maybe Integer
smallestPos = fmap (fst . fst) . Map.minViewWithKey . mapping
type HighlightingInfo = CompressedFile
singleton :: Range -> MetaInfo -> File
singleton r m = File {
mapping = Map.fromAscList [ (p, m) | p <- toList r ] }
prop_singleton r m =
compress (singleton r m) ==
if null (toList r) then [] else [(r, m)]
several :: [Range] -> MetaInfo -> File
several rs m = mconcat $ map (\r -> singleton r m) rs
mergeMetaInfo :: MetaInfo -> MetaInfo -> MetaInfo
mergeMetaInfo m1 m2 = MetaInfo
{ 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 MetaInfo where
mempty = MetaInfo { aspect = Nothing
, otherAspects = []
, note = Nothing
, definitionSite = Nothing
}
mappend = mergeMetaInfo
merge :: File -> File -> File
merge f1 f2 =
File { mapping = (Map.unionWith mappend `on` mapping) f1 f2 }
instance Monoid File where
mempty = File { mapping = Map.empty }
mappend = merge
toMap :: File -> Map Integer MetaInfo
toMap = mapping
type CompressedFile = [(Range, MetaInfo)]
compress :: File -> CompressedFile
compress f = map join $ groupBy' p (Map.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 .
Map.fromList .
concat .
map (\(r, m) -> [ (p, m) | p <- toList r ])
prop_compress f =
decompress c == f
&&
and (map (rangeInvariant . fst) c)
&&
and [ not (overlapping r1 r2) | (r1, r2) <- allPairs (map fst c) ]
where
c = compress f
allPairs [] = []
allPairs (x : xs) = map ((,) x) xs ++ allPairs xs
instance Arbitrary Aspect where
arbitrary =
frequency [ (3, elements [ Comment, Keyword, String, Number
, Symbol, PrimitiveType ])
, (1, liftM2 Name (maybeGen arbitrary) arbitrary)
]
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
]
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
instance Arbitrary OtherAspect where
arbitrary = elements [minBound .. maxBound]
instance CoArbitrary OtherAspect where
coarbitrary = coarbitrary . fromEnum
instance Arbitrary MetaInfo where
arbitrary = do
aspect <- arbitrary
other <- arbitrary
note <- maybeGen string
defSite <- arbitrary
return (MetaInfo { aspect = aspect, otherAspects = other
, note = note, definitionSite = defSite })
where string = listOfElements "abcdefABCDEF/\\.\"'@()åäö\n"
instance CoArbitrary MetaInfo where
coarbitrary (MetaInfo aspect otherAspects note defSite) =
coarbitrary aspect .
coarbitrary otherAspects .
coarbitrary note .
coarbitrary defSite
instance Arbitrary File where
arbitrary = fmap (File . Map.fromList) $ listOf arbitrary
instance CoArbitrary File where
coarbitrary (File rs) = coarbitrary (Map.toAscList rs)
tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Precise"
[ quickCheck' prop_singleton
, quickCheck' prop_compress
]