1
{-# LANGUAGE DeriveDataTypeable #-}
3
-- | Types used for precise syntax highlighting.
5
module Agda.Interaction.Highlighting.Precise
11
, HighlightingInfo(..)
19
, Agda.Interaction.Highlighting.Precise.tests
22
import Agda.Utils.TestHelpers
23
import Agda.Utils.String
24
import Agda.Utils.List hiding (tests)
29
import Agda.Utils.QuickCheck
31
import qualified Data.Map as Map
34
import qualified Agda.Syntax.Abstract.Name as A
35
import qualified Agda.Syntax.Common as C
37
import Agda.Interaction.Highlighting.Range
39
------------------------------------------------------------------------
42
-- | Various more or less syntactic aspects of the code. (These cannot
50
| Symbol -- ^ Symbols like forall, =, ->, etc.
51
| PrimitiveType -- ^ Things like Set and Prop.
52
| Name (Maybe NameKind) Bool -- ^ Is the name an operator part?
53
deriving (Eq, Show, Typeable, Data)
56
= Bound -- ^ Bound variable.
57
| Constructor C.Induction -- ^ Inductive or coinductive constructor.
59
| Field -- ^ Record field.
61
| Module -- ^ Module name.
63
| Primitive -- ^ Primitive.
64
| Record -- ^ Record type.
65
deriving (Eq, Show, Typeable, Data)
67
-- | Other aspects. (These can overlap with each other and with
76
-- ^ When this constructor is used it is probably a good idea to
77
-- include a 'note' explaining why the pattern is incomplete.
78
deriving (Eq, Show, Enum, Bounded, Typeable, Data)
80
-- | Meta information which can be associated with a
81
-- character\/character range.
83
data MetaInfo = MetaInfo
84
{ aspect :: Maybe Aspect
85
, otherAspects :: [OtherAspect]
86
, note :: Maybe String
87
-- ^ This note, if present, can be displayed as a tool-tip or
88
-- something like that. It should contain useful information about
89
-- the range (like the module containing a certain identifier, or
90
-- the fixity of an operator).
91
, definitionSite :: Maybe ([String], FilePath, Integer)
92
-- ^ The definition site of the annotated thing, if applicable and
93
-- known. File positions are counted from 1. The list of strings
94
-- is the name of the /top-level/ module in which the thing is
97
deriving (Eq, Show, Typeable, Data)
99
-- | A 'File' is a mapping from file positions to meta information.
101
-- The first position in the file has number 1.
103
newtype File = File { mapping :: Map Integer MetaInfo }
104
deriving (Eq, Show, Typeable, Data)
106
-- | Returns the smallest position, if any, in the 'File'.
108
smallestPos :: File -> Maybe Integer
109
smallestPos = fmap (fst . fst) . Map.minViewWithKey . mapping
111
-- | Syntax highlighting information for a given source file.
113
data HighlightingInfo =
114
HighlightingInfo { source :: FilePath
115
-- ^ The source file.
116
, info :: CompressedFile
117
-- ^ Highlighting info.
119
deriving (Typeable, Data)
121
------------------------------------------------------------------------
124
-- | @'singleton' r m@ is a file whose positions are those in @r@, and
125
-- in which every position is associated with @m@.
127
singleton :: Range -> MetaInfo -> File
128
singleton r m = File {
129
mapping = Map.fromAscList [ (p, m) | p <- toList r ] }
132
compress (singleton r m) ==
133
if null (toList r) then [] else [(r, m)]
135
-- | Like 'singleton', but with several ranges instead of only one.
137
several :: [Range] -> MetaInfo -> File
138
several rs m = mconcat $ map (\r -> singleton r m) rs
140
------------------------------------------------------------------------
143
-- | Merges meta information.
145
mergeMetaInfo :: MetaInfo -> MetaInfo -> MetaInfo
146
mergeMetaInfo m1 m2 = MetaInfo
147
{ aspect = (mplus `on` aspect) m1 m2
148
, otherAspects = nub $ ((++) `on` otherAspects) m1 m2
149
, note = case (note m1, note m2) of
150
(Just n1, Just n2) -> Just $
152
else addFinalNewLine n1 ++ "----\n" ++ n2
153
(Just n1, Nothing) -> Just n1
154
(Nothing, Just n2) -> Just n2
155
(Nothing, Nothing) -> Nothing
156
, definitionSite = (mplus `on` definitionSite) m1 m2
159
instance Monoid MetaInfo where
160
mempty = MetaInfo { aspect = Nothing
163
, definitionSite = Nothing
165
mappend = mergeMetaInfo
169
merge :: File -> File -> File
171
File { mapping = (Map.unionWith mappend `on` mapping) f1 f2 }
173
instance Monoid File where
174
mempty = File { mapping = Map.empty }
177
------------------------------------------------------------------------
180
-- | Convert the 'File' to a map from file positions (counting from 1)
181
-- to meta information.
183
toMap :: File -> Map Integer MetaInfo
186
------------------------------------------------------------------------
189
-- | A compressed 'File', in which consecutive positions with the same
190
-- 'MetaInfo' are stored together.
192
type CompressedFile = [(Range, MetaInfo)]
194
-- | Compresses a file by merging consecutive positions with equal
195
-- meta information into longer ranges.
197
compress :: File -> CompressedFile
198
compress f = map join $ groupBy' p (Map.toAscList $ mapping f)
200
p (pos1, m1) (pos2, m2) = pos2 == pos1 + 1 && m1 == m2
201
join pms = ( Range { from = head ps, to = last ps + 1 }
204
where (ps, ms) = unzip pms
206
-- | Decompresses a compressed file.
208
decompress :: CompressedFile -> File
213
map (\(r, m) -> [ (p, m) | p <- toList r ])
218
and (map (rangeInvariant . fst) c)
220
and [ not (overlapping r1 r2) | (r1, r2) <- allPairs (map fst c) ]
225
allPairs (x : xs) = map ((,) x) xs ++ allPairs xs
227
------------------------------------------------------------------------
230
instance Arbitrary Aspect where
232
frequency [ (3, elements [ Comment, Keyword, String, Number
233
, Symbol, PrimitiveType ])
234
, (1, liftM2 Name (maybeGen arbitrary) arbitrary)
237
instance CoArbitrary Aspect where
238
coarbitrary Comment = variant 0
239
coarbitrary Keyword = variant 1
240
coarbitrary String = variant 2
241
coarbitrary Number = variant 3
242
coarbitrary Symbol = variant 4
243
coarbitrary PrimitiveType = variant 5
244
coarbitrary (Name nk b) =
245
variant 6 . maybeCoGen coarbitrary nk . coarbitrary b
247
instance Arbitrary NameKind where
248
arbitrary = oneof $ [liftM Constructor arbitrary] ++
259
instance CoArbitrary NameKind where
260
coarbitrary Bound = variant 0
261
coarbitrary (Constructor ind) = variant 1 . coarbitrary ind
262
coarbitrary Datatype = variant 2
263
coarbitrary Field = variant 3
264
coarbitrary Function = variant 4
265
coarbitrary Module = variant 5
266
coarbitrary Postulate = variant 6
267
coarbitrary Primitive = variant 7
268
coarbitrary Record = variant 8
270
instance Arbitrary OtherAspect where
271
arbitrary = elements [minBound .. maxBound]
273
instance CoArbitrary OtherAspect where
274
coarbitrary = coarbitrary . fromEnum
276
instance Arbitrary MetaInfo where
278
aspect <- maybeGen arbitrary
280
note <- maybeGen string
281
defSite <- maybeGen (liftM3 (,,) (listOf string) string arbitrary)
282
return (MetaInfo { aspect = aspect, otherAspects = other
283
, note = note, definitionSite = defSite })
284
where string = listOfElements "abcdefABCDEF/\\.\"'@()åäö\n"
286
instance CoArbitrary MetaInfo where
287
coarbitrary (MetaInfo aspect otherAspects note defSite) =
289
coarbitrary otherAspects .
293
instance Arbitrary File where
294
arbitrary = fmap (File . Map.fromList) $ listOf arbitrary
296
instance CoArbitrary File where
297
coarbitrary (File rs) = coarbitrary (Map.toAscList rs)
299
------------------------------------------------------------------------
302
-- | All the properties.
305
tests = runTests "Agda.Interaction.Highlighting.Precise"
306
[ quickCheck' prop_singleton
307
, quickCheck' prop_compress
added
removed
src/full/Agda/Interaction/Highlighting/Precise.hs
