1-- | Types used for precise syntax highlighting. 2 3module Agda.Interaction.Highlighting.Precise 4 ( -- * Highlighting information 5 Aspect(..) 6 , NameKind(..) 7 , OtherAspect(..) 8 , Aspects(..) 9 , DefinitionSite(..) 10 , TokenBased(..) 11 , RangePair(..) 12 , rangePairInvariant 13 , PositionMap(..) 14 , DelayedMerge(..) 15 , delayedMergeInvariant 16 , HighlightingInfo 17 , highlightingInfoInvariant 18 , HighlightingInfoBuilder 19 , highlightingInfoBuilderInvariant 20 -- ** Operations 21 , parserBased 22 , kindOfNameToNameKind 23 , IsBasicRangeMap(..) 24 , RangeMap.several 25 , Convert(..) 26 , RangeMap.insideAndOutside 27 , RangeMap.restrictTo 28 ) where 29 30import Prelude hiding (null) 31 32import Control.Arrow (second) 33import Control.DeepSeq 34import Control.Monad 35 36import Data.Function 37import qualified Data.List as List 38import Data.Maybe 39import Data.Semigroup 40 41import Data.IntMap (IntMap) 42import qualified Data.IntMap as IntMap 43 44import Data.Map.Strict (Map) 45import qualified Data.Map.Strict as Map 46 47import Data.Set (Set) 48import qualified Data.Set as Set 49 50import GHC.Generics (Generic) 51 52import qualified Agda.Syntax.Position as P 53import qualified Agda.Syntax.Common as Common 54import qualified Agda.Syntax.Concrete as C 55import Agda.Syntax.Scope.Base ( KindOfName(..) ) 56 57import Agda.Interaction.Highlighting.Range 58 59import Agda.Utils.List 60import qualified Agda.Utils.List1 as List1 61import Agda.Utils.Maybe 62import Agda.Utils.Null 63import Agda.Utils.RangeMap (RangeMap, IsBasicRangeMap(..)) 64import qualified Agda.Utils.RangeMap as RangeMap 65import Agda.Utils.String 66 67import Agda.Utils.Impossible 68 69------------------------------------------------------------------------ 70-- Highlighting information 71 72-- | Syntactic aspects of the code. (These cannot overlap.) 73 74data Aspect 75 = Comment 76 | Keyword 77 | String 78 | Number 79 | Hole 80 | Symbol -- ^ Symbols like forall, =, ->, etc. 81 | PrimitiveType -- ^ Things like Set and Prop. 82 | Name (Maybe NameKind) Bool -- ^ Is the name an operator part? 83 | Pragma -- ^ Text occurring in pragmas that 84 -- does not have a more specific 85 -- aspect. 86 | Background -- ^ Non-code contents in literate Agda 87 | Markup 88 -- ^ Delimiters used to separate the Agda code blocks from the 89 -- other contents in literate Agda 90 deriving (Eq, Show, Generic) 91 92-- | @NameKind@s are figured out during scope checking. 93 94data NameKind 95 = Bound -- ^ Bound variable. 96 | Generalizable -- ^ Generalizable variable. 97 -- (This includes generalizable 98 -- variables that have been 99 -- generalized). 100 | Constructor Common.Induction -- ^ Inductive or coinductive constructor. 101 | Datatype 102 | Field -- ^ Record field. 103 | Function 104 | Module -- ^ Module name. 105 | Postulate 106 | Primitive -- ^ Primitive. 107 | Record -- ^ Record type. 108 | Argument -- ^ Named argument, like x in {x = v} 109 | Macro -- ^ Macro. 110 deriving (Eq, Show, Generic) 111 112-- | Other aspects, generated by type checking. 113-- (These can overlap with each other and with 'Aspect's.) 114 115data OtherAspect 116 = Error 117 | ErrorWarning 118 -- ^ A warning that is considered fatal in the end. 119 | DottedPattern 120 | UnsolvedMeta 121 | UnsolvedConstraint 122 -- ^ Unsolved constraint not connected to meta-variable. This 123 -- could for instance be an emptyness constraint. 124 | TerminationProblem 125 | PositivityProblem 126 | Deadcode 127 -- ^ Used for highlighting unreachable clauses, unreachable RHS 128 -- (because of an absurd pattern), etc. 129 | ShadowingInTelescope 130 -- ^ Used for shadowed repeated variable names in telescopes. 131 | CoverageProblem 132 | IncompletePattern 133 -- ^ When this constructor is used it is probably a good idea to 134 -- include a 'note' explaining why the pattern is incomplete. 135 | TypeChecks 136 -- ^ Code which is being type-checked. 137 | MissingDefinition 138 -- ^ Function declaration without matching definition 139 -- NB: We put CatchallClause last so that it is overwritten by other, 140 -- more important, aspects in the emacs mode. 141 | CatchallClause 142 | ConfluenceProblem 143 deriving (Eq, Ord, Show, Enum, Bounded, Generic) 144 145-- | Meta information which can be associated with a 146-- character\/character range. 147 148data Aspects = Aspects 149 { aspect :: Maybe Aspect 150 , otherAspects :: Set OtherAspect 151 , note :: String 152 -- ^ This note, if not null, can be displayed as a tool-tip or 153 -- something like that. It should contain useful information about 154 -- the range (like the module containing a certain identifier, or 155 -- the fixity of an operator). 156 , definitionSite :: Maybe DefinitionSite 157 -- ^ The definition site of the annotated thing, if applicable and 158 -- known. 159 , tokenBased :: !TokenBased 160 -- ^ Is this entry token-based? 161 } 162 deriving (Show, Generic) 163 164data DefinitionSite = DefinitionSite 165 { defSiteModule :: C.TopLevelModuleName 166 -- ^ The defining module. 167 , defSitePos :: Int 168 -- ^ The file position in that module. File positions are 169 -- counted from 1. 170 , defSiteHere :: Bool 171 -- ^ Has this @DefinitionSite@ been created at the defining site of the name? 172 , defSiteAnchor :: Maybe String 173 -- ^ A pretty name for the HTML linking. 174 } 175 deriving (Show, Generic) 176 177instance Eq DefinitionSite where 178 DefinitionSite m p _ _ == DefinitionSite m' p' _ _ = m == m' && p == p' 179 180-- | Is the highlighting \"token-based\", i.e. based only on 181-- information from the lexer? 182 183data TokenBased = TokenBased | NotOnlyTokenBased 184 deriving (Eq, Show) 185 186instance Eq Aspects where 187 Aspects a o _ d t == Aspects a' o' _ d' t' = 188 (a, o, d, t) == (a', o', d', t') 189 190-- | A limited kind of syntax highlighting information: a pair 191-- consisting of 'Ranges' and 'Aspects'. 192-- 193-- Note the invariant which 'RangePair's should satisfy 194-- ('rangePairInvariant'). 195 196newtype RangePair = RangePair 197 { rangePair :: (Ranges, Aspects) 198 } 199 deriving (Show, NFData) 200 201-- | Invariant for 'RangePair'. 202 203rangePairInvariant :: RangePair -> Bool 204rangePairInvariant (RangePair (rs, _)) = 205 rangesInvariant rs 206 207-- | Syntax highlighting information, represented by maps from 208-- positions to 'Aspects'. 209-- 210-- The first position in the file has number 1. 211 212newtype PositionMap = PositionMap 213 { positionMap :: IntMap Aspects 214 } 215 deriving (Show, NFData) 216 217-- | Highlighting info with delayed merging. 218-- 219-- Merging large sets of highlighting info repeatedly might be costly. 220-- The idea of this type is to accumulate small pieces of highlighting 221-- information, and then to merge them all at the end. 222-- 223-- Note the invariant which values of this type should satisfy 224-- ('delayedMergeInvariant'). 225 226newtype DelayedMerge hl = DelayedMerge (Endo [hl]) 227 deriving (Semigroup, Monoid) 228 229instance Show hl => Show (DelayedMerge hl) where 230 showsPrec _ (DelayedMerge f) = 231 showString "DelayedMerge (Endo (" . 232 shows (appEndo f []) . 233 showString " ++))" 234 235-- | Invariant for @'DelayedMerge' hl@, parametrised by the invariant 236-- for @hl@. 237-- 238-- Additionally the endofunction should be extensionally equal to @(fs 239-- '++')@ for some list @fs@. 240 241delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool 242delayedMergeInvariant inv (DelayedMerge f) = 243 all inv (appEndo f []) 244 245-- | Highlighting information. 246-- 247-- Note the invariant which values of this type should satisfy 248-- ('highlightingInfoInvariant'). 249-- 250-- This is a type synonym in order to make it easy to change to 251-- another representation. 252 253type HighlightingInfo = RangeMap Aspects 254 255-- | The invariant for 'HighlightingInfo'. 256 257highlightingInfoInvariant :: HighlightingInfo -> Bool 258highlightingInfoInvariant = RangeMap.rangeMapInvariant 259 260-- | A type that is intended to be used when constructing highlighting 261-- information. 262-- 263-- Note the invariant which values of this type should satisfy 264-- ('highlightingInfoBuilderInvariant'). 265-- 266-- This is a type synonym in order to make it easy to change to 267-- another representation. 268-- 269-- The type should be an instance of @'IsBasicRangeMap' 'Aspects'@, 270-- 'Semigroup' and 'Monoid', and there should be an instance of 271-- @'Convert' 'HighlightingInfoBuilder' 'HighlightingInfo'@. 272 273type HighlightingInfoBuilder = DelayedMerge RangePair 274 275-- | The invariant for 'HighlightingInfoBuilder'. 276-- 277-- Additionally the endofunction should be extensionally equal to @(fs 278-- '++')@ for some list @fs@. 279 280highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool 281highlightingInfoBuilderInvariant = 282 delayedMergeInvariant rangePairInvariant 283 284------------------------------------------------------------------------ 285-- Creation and conversion 286 287-- | A variant of 'mempty' with 'tokenBased' set to 288-- 'NotOnlyTokenBased'. 289 290parserBased :: Aspects 291parserBased = mempty { tokenBased = NotOnlyTokenBased } 292 293-- | Conversion from classification of the scope checker. 294 295kindOfNameToNameKind :: KindOfName -> NameKind 296kindOfNameToNameKind = \case 297 -- Inductive is Constructor default, overwritten by CoInductive 298 ConName -> Constructor Common.Inductive 299 CoConName -> Constructor Common.CoInductive 300 FldName -> Field 301 PatternSynName -> Constructor Common.Inductive 302 GeneralizeName -> Generalizable 303 DisallowedGeneralizeName -> Generalizable 304 MacroName -> Macro 305 QuotableName -> Function 306 DataName -> Datatype 307 RecName -> Record 308 FunName -> Function 309 AxiomName -> Postulate 310 PrimName -> Primitive 311 OtherDefName -> Function 312 313instance IsBasicRangeMap Aspects RangePair where 314 singleton rs m = RangePair (rs, m) 315 316 toList (RangePair (Ranges rs, m)) = 317 [ (r, m) | r <- rs, not (null r) ] 318 319 toMap f = toMap (convert (DelayedMerge (Endo (f :))) :: PositionMap) 320 321instance IsBasicRangeMap Aspects PositionMap where 322 singleton rs m = PositionMap 323 { positionMap = 324 IntMap.fromDistinctAscList [ (p, m) | p <- rangesToPositions rs ] 325 } 326 327 toList = map join . List1.groupBy' p . IntMap.toAscList . positionMap 328 where 329 p (pos1, m1) (pos2, m2) = pos2 == pos1 + 1 && m1 == m2 330 join pms = ( Range { from = List1.head ps, to = List1.last ps + 1 } 331 , List1.head ms 332 ) 333 where (ps, ms) = List1.unzip pms 334 335 toMap = positionMap 336 337instance Semigroup a => 338 IsBasicRangeMap a (DelayedMerge (RangeMap a)) where 339 singleton r m = DelayedMerge (Endo (singleton r m :)) 340 341 toMap f = toMap (convert f :: RangeMap a) 342 toList f = toList (convert f :: RangeMap a) 343 344instance IsBasicRangeMap Aspects (DelayedMerge RangePair) where 345 singleton r m = DelayedMerge (Endo (singleton r m :)) 346 347 toMap f = toMap (convert f :: PositionMap) 348 toList f = toList (convert f :: RangeMap Aspects) 349 350instance IsBasicRangeMap Aspects (DelayedMerge PositionMap) where 351 singleton r m = DelayedMerge (Endo (singleton r m :)) 352 353 toMap f = toMap (convert f :: PositionMap) 354 toList f = toList (convert f :: PositionMap) 355 356-- | Conversion between different types. 357 358class Convert a b where 359 convert :: a -> b 360 361instance Monoid hl => Convert (DelayedMerge hl) hl where 362 convert (DelayedMerge f) = mconcat (appEndo f []) 363 364instance Convert (RangeMap Aspects) (RangeMap Aspects) where 365 convert = id 366 367instance Convert PositionMap (RangeMap Aspects) where 368 convert = 369 RangeMap.fromNonOverlappingNonEmptyAscendingList . 370 toList 371 372instance Convert (DelayedMerge PositionMap) (RangeMap Aspects) where 373 convert f = convert (convert f :: PositionMap) 374 375instance Convert (DelayedMerge RangePair) PositionMap where 376 convert (DelayedMerge f) = 377 PositionMap $ 378 IntMap.fromListWith (flip (<>)) 379 [ (p, m) 380 | RangePair (r, m) <- appEndo f [] 381 , p <- rangesToPositions r 382 ] 383 384instance Convert (DelayedMerge RangePair) (RangeMap Aspects) where 385 convert (DelayedMerge f) = 386 mconcat 387 [ singleton r m 388 | RangePair (r, m) <- appEndo f [] 389 ] 390 391------------------------------------------------------------------------ 392-- Merging 393 394instance Semigroup TokenBased where 395 b1@NotOnlyTokenBased <> b2 = b1 396 TokenBased <> b2 = b2 397 398instance Monoid TokenBased where 399 mempty = TokenBased 400 mappend = (<>) 401 402-- | Some 'NameKind's are more informative than others. 403instance Semigroup NameKind where 404 -- During scope-checking of record, we build a constructor 405 -- whose arguments (@Bound@ variables) are the fields. 406 -- Later, we process them as @Field@s proper. 407 Field <> Bound = Field 408 Bound <> Field = Field 409 -- -- Projections are special functions. 410 -- -- TODO necessary? 411 -- Field <> Function = Field 412 -- Function <> Field = Field 413 -- TODO: more overwrites? 414 k1 <> k2 | k1 == k2 = k1 415 | otherwise = k1 -- TODO: __IMPOSSIBLE__ 416 417-- | @NameKind@ in @Name@ can get more precise. 418instance Semigroup Aspect where 419 Name mk1 op1 <> Name mk2 op2 = Name (unionMaybeWith (<>) mk1 mk2) op1 420 -- (op1 || op2) breaks associativity 421 a1 <> a2 | a1 == a2 = a1 422 | otherwise = a1 -- TODO: __IMPOSSIBLE__ 423 424instance Semigroup DefinitionSite where 425 d1 <> d2 | d1 == d2 = d1 426 | otherwise = d1 -- TODO: __IMPOSSIBLE__ 427 428-- | Merges meta information. 429 430mergeAspects :: Aspects -> Aspects -> Aspects 431mergeAspects m1 m2 = Aspects 432 { aspect = (unionMaybeWith (<>) `on` aspect) m1 m2 433 , otherAspects = (Set.union `on` otherAspects) m1 m2 434 , note = case (note m1, note m2) of 435 (n1, "") -> n1 436 ("", n2) -> n2 437 (n1, n2) 438 | n1 == n2 -> n1 439 | otherwise -> addFinalNewLine n1 ++ "----\n" ++ n2 440 , definitionSite = (unionMaybeWith (<>) `on` definitionSite) m1 m2 441 , tokenBased = tokenBased m1 <> tokenBased m2 442 } 443 444instance Semigroup Aspects where 445 (<>) = mergeAspects 446 447instance Monoid Aspects where 448 mempty = Aspects 449 { aspect = Nothing 450 , otherAspects = Set.empty 451 , note = [] 452 , definitionSite = Nothing 453 , tokenBased = mempty 454 } 455 mappend = (<>) 456 457instance Semigroup PositionMap where 458 f1 <> f2 = PositionMap 459 { positionMap = (IntMap.unionWith mappend `on` positionMap) f1 f2 } 460 461instance Monoid PositionMap where 462 mempty = PositionMap { positionMap = IntMap.empty } 463 mappend = (<>) 464 465------------------------------------------------------------------------ 466-- NFData instances 467 468instance NFData Aspect 469instance NFData NameKind 470instance NFData OtherAspect 471instance NFData DefinitionSite 472 473instance NFData Aspects where 474 rnf (Aspects a b c d _) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d 475