summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/Highlighting/Generate.hs
blob: 0c0fbb14c8eacd7e4a53ae73b48955e1d502424d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RelaxedPolyRec #-}

-- | Generates data used for precise syntax highlighting.

module Agda.Interaction.Highlighting.Generate
  ( Level(..)
  , generateAndPrintSyntaxInfo
  , generateTokenInfo, generateTokenInfoFromString
  , printErrorInfo, errorHighlighting
  , printUnsolvedInfo
  , printHighlightingInfo
  , highlightAsTypeChecked
  , computeUnsolvedMetaWarnings
  , computeUnsolvedConstraints
  , storeDisambiguatedName
  , Agda.Interaction.Highlighting.Generate.tests
  ) where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Monad.Reader
import Control.Applicative
import Control.Arrow ((***), first, second)

import Data.Monoid
import Data.Generics.Geniplate
import Data.HashSet (HashSet)
import qualified Data.HashSet as HSet
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\), isPrefixOf)
import qualified Data.Foldable as Fold (toList, fold, foldMap)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

import Agda.Interaction.FindFile
import Agda.Interaction.Response (Response(Resp_HighlightingInfo))
import Agda.Interaction.Highlighting.Precise hiding (tests)
import Agda.Interaction.Highlighting.Range   hiding (tests)

import qualified Agda.TypeChecking.Errors as E
import Agda.TypeChecking.MetaVars (isBlockedTerm)
import Agda.TypeChecking.Monad
  hiding (MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import Agda.TypeChecking.Pretty
import qualified Agda.TypeChecking.Reduce as R

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common (Delayed(..))
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Info as SI
import qualified Agda.Syntax.Internal as I
import qualified Agda.Syntax.Literal as L
import qualified Agda.Syntax.Parser as Pa
import qualified Agda.Syntax.Parser.Tokens as T
import qualified Agda.Syntax.Position as P

import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.TestHelpers
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap

#include "undefined.h"
import Agda.Utils.Impossible

-- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its
--   result. Additionally, some code may be highlighted:
--
-- * If @r@ is non-empty and not a sub-range of @rPre@ (after
--   'P.continuousPerLine' has been applied to both): @r@ is
--   highlighted as being type-checked while @m@ is running (this
--   highlighting is removed if @m@ completes /successfully/).
--
-- * Otherwise: Highlighting is removed for @rPre - r@ before @m@
--   runs, and if @m@ completes successfully, then @rPre - r@ is
--   highlighted as being type-checked.

highlightAsTypeChecked
  :: MonadTCM tcm
  => P.Range
  -> P.Range
  -> tcm a
  -> tcm a
highlightAsTypeChecked rPre r m
  | r /= P.noRange && delta == rPre' = wrap r'    highlight clear
  | otherwise                        = wrap delta clear     highlight
  where
  rPre'     = rToR (P.continuousPerLine rPre)
  r'        = rToR (P.continuousPerLine r)
  delta     = rPre' `minus` r'
  clear     = mempty
  highlight = mempty { otherAspects = [TypeChecks] }

  wrap rs x y = do
    p rs x
    v <- m
    p rs y
    return v
    where
    p rs x = printHighlightingInfo (singletonC rs x)

-- | Lispify and print the given highlighting information.

printHighlightingInfo :: MonadTCM tcm => HighlightingInfo -> tcm ()
printHighlightingInfo x = do
  modToSrc <- use stModuleToSource
  liftTCM $ reportSLn "highlighting" 50 $
    "Printing highlighting info:\n" ++ show x ++ "\n" ++
    "  modToSrc = " ++ show modToSrc
  unless (null $ ranges x) $ do
    liftTCM $ appInteractionOutputCallback $
        Resp_HighlightingInfo x modToSrc

-- | Highlighting levels.

data Level
  = Full
    -- ^ Full highlighting. Should only be used after typechecking has
    --   completed successfully.
  | Partial
    -- ^ Highlighting without disambiguation of overloaded
    --   constructors.

-- | Generate syntax highlighting information for the given
-- declaration, and (if appropriate) print it. If the
-- 'HighlightingLevel' is @'Full'@, then the state is
-- additionally updated with the new highlighting info (in case of a
-- conflict new info takes precedence over old info).
--
-- The procedure makes use of some of the token highlighting info in
-- 'stTokens' (that corresponding to the interval covered by the
-- declaration). If the 'HighlightingLevel' is @'Full'@,
-- then this token highlighting info is additionally removed from
-- 'stTokens'.

generateAndPrintSyntaxInfo :: A.Declaration -> Level -> TCM ()
generateAndPrintSyntaxInfo decl _ | P.noRange == P.getRange decl = return ()
generateAndPrintSyntaxInfo decl hlLevel = do
  file <- fromMaybe __IMPOSSIBLE__ <$> asks envCurrentPath

  reportSLn "import.iface.create" 15 $
      "Generating syntax info for " ++ filePath file ++ ' ' :
        case hlLevel of
            Full    {} -> "(final)"
            Partial {} -> "(first approximation)"
        ++ "."

  M.ignoreAbstractMode $ do
    modMap <- sourceToModule
    kinds  <- nameKinds hlLevel decl

    let nameInfo = mconcat $ map (generate modMap file kinds) names

    -- Constructors are only highlighted after type checking, since they
    -- can be overloaded.
    constructorInfo <- case hlLevel of
      Full{} -> generateConstructorInfo modMap file kinds decl
      _      -> return mempty

    let (from, to) = case P.rangeToInterval (P.getRange decl) of
          Nothing -> __IMPOSSIBLE__
          Just i  -> ( fromIntegral $ P.posPos $ P.iStart i
                     , fromIntegral $ P.posPos $ P.iEnd i)
    (prevTokens, (curTokens, postTokens)) <-
      (second (splitAtC to)) . splitAtC from <$> use stTokens

    -- theRest needs to be placed before nameInfo here since record
    -- field declarations contain QNames. constructorInfo also needs
    -- to be placed before nameInfo since, when typechecking is done,
    -- constructors are included in both lists. Finally the token
    -- information is placed last since token highlighting is more
    -- crude than the others.
    let syntaxInfo = compress (mconcat [ constructorInfo
                                       , theRest modMap file
                                       , nameInfo
                                       ])
                       `mappend`
                     curTokens

    case hlLevel of
      Full{} -> do stSyntaxInfo %= mappend syntaxInfo
                   stTokens     .= prevTokens `mappend` postTokens
      _      -> return ()

    ifTopLevelAndHighlightingLevelIs NonInteractive $
      printHighlightingInfo syntaxInfo
  where
  -- All names mentioned in the syntax tree (not bound variables).
  names :: [A.AmbiguousQName]
  names =
    (map (A.AmbQ . (:[])) $
     filter (not . extendedLambda) $
     universeBi decl) ++
    universeBi decl
    where
    extendedLambda :: A.QName -> Bool
    extendedLambda = (extendedLambdaName `isPrefixOf`) . show . A.nameConcrete . A.qnameName

  -- Bound variables, dotted patterns, record fields, module names,
  -- the "as" and "to" symbols.
  theRest modMap file = mconcat
    [ Fold.foldMap getFieldDecl   $ universeBi decl
    , Fold.foldMap getVarAndField $ universeBi decl
    , Fold.foldMap getLet         $ universeBi decl
    , Fold.foldMap getLam         $ universeBi decl
    , Fold.foldMap getTyped       $ universeBi decl
    , Fold.foldMap getPattern     $ universeBi decl
    , Fold.foldMap getExpr        $ universeBi decl
    , Fold.foldMap getPatSynArgs  $ universeBi decl
    , Fold.foldMap getModuleName  $ universeBi decl
    , Fold.foldMap getModuleInfo  $ universeBi decl
    , Fold.foldMap getNamedArg    $ universeBi decl
    ]
    where
    bound n = nameToFile modMap file [] (A.nameConcrete n)
                         (\isOp -> mempty { aspect = Just $ Name (Just Bound) isOp })
                         (Just $ A.nameBindingSite n)

    patsyn n = nameToFileA modMap file n True $ \isOp ->
                  mempty { aspect = Just $ Name (Just $ Constructor Common.Inductive) isOp }

    field m n = nameToFile modMap file m n
                           (\isOp -> mempty { aspect = Just $ Name (Just Field) isOp })
                           Nothing
    asName n = nameToFile modMap file []
                          n
                          (\isOp -> mempty { aspect = Just $ Name (Just Module) isOp })
                          Nothing

    mod isTopLevelModule n =
      nameToFile modMap file []
                 (A.nameConcrete n)
                 (\isOp -> mempty { aspect = Just $ Name (Just Module) isOp })
                 (Just $ (if isTopLevelModule then P.beginningOfFile else id)
                           (A.nameBindingSite n))

    getVarAndField :: A.Expr -> File
    getVarAndField (A.Var x)    = bound x
    getVarAndField (A.Rec _ fs) = mconcat $ map (field [] . fst) fs
    getVarAndField _            = mempty

    -- Ulf, 2014-04-09: It would be nicer to have it on Named_ a, but
    -- you can't have polymorphic functions in universeBi.
    getNamedArg :: Common.RString -> File
    getNamedArg x = singleton (rToR $ P.getRange x) mempty{ aspect = Just $ Name (Just Argument) False }

    getLet :: A.LetBinding -> File
    getLet (A.LetBind _ _ x _ _) = bound x
    getLet A.LetPatBind{}        = mempty
    getLet A.LetApply{}          = mempty
    getLet A.LetOpen{}           = mempty

    getLam :: A.LamBinding -> File
    getLam (A.DomainFree _ x) = bound x
    getLam (A.DomainFull {})  = mempty

    getTyped :: A.TypedBinding -> File
    getTyped (A.TBind _ xs _) = mconcat $ map (bound . dget) xs
    getTyped A.TLet{}         = mempty

    getPatSynArgs :: A.Declaration -> File
    getPatSynArgs (A.PatternSynDef _ xs _) = mconcat $ map (bound . Common.unArg) xs
    getPatSynArgs _                        = mempty

    getPattern :: A.Pattern -> File
    getPattern (A.VarP x)    = bound x
    getPattern (A.AsP _ x _) = bound x
    getPattern (A.DotP pi _) =
      singleton (rToR $ P.getRange pi)
                (mempty { otherAspects = [DottedPattern] })
    getPattern (A.PatternSynP _ q _) = patsyn q
    getPattern _             = mempty

    getExpr :: A.Expr -> File
    getExpr (A.PatternSyn q) = patsyn q
    getExpr _                = mempty

    getFieldDecl :: A.Declaration -> File
    getFieldDecl (A.RecDef _ _ _ _ _ _ fs) = Fold.foldMap extractField fs
      where
      extractField (A.ScopedDecl _ ds) = Fold.foldMap extractField ds
      extractField (A.Field _ x _)     = field (concreteQualifier x)
                                               (concreteBase x)
      extractField _                   = mempty
    getFieldDecl _                   = mempty

    getModuleName :: A.ModuleName -> File
    getModuleName m@(A.MName { A.mnameToList = xs }) =
      mconcat $ map (mod isTopLevelModule) xs
      where
      isTopLevelModule =
        case catMaybes $
             map (join .
                  fmap P.srcFile .
                  P.rStart .
                  A.nameBindingSite) xs of
          f : _ -> Map.lookup f modMap ==
                   Just (C.toTopLevelModuleName $ A.mnameToConcrete m)
          []    -> False

    getModuleInfo :: SI.ModuleInfo -> File
    getModuleInfo (SI.ModuleInfo { SI.minfoAsTo   = asTo
                                 , SI.minfoAsName = name }) =
      singleton (rToR asTo) (mempty { aspect = Just Symbol })
        `mappend`
      maybe mempty asName name

-- | Generate and return the syntax highlighting information for the
-- tokens in the given file.

generateTokenInfo
  :: AbsolutePath          -- ^ The module to highlight.
  -> TCM CompressedFile
generateTokenInfo file =
  liftIO $ tokenHighlighting <$> Pa.parseFile' Pa.tokensParser file

-- | Same as 'generateTokenInfo' but takes a string instead of a filename.
generateTokenInfoFromString :: P.Range -> String -> TCM CompressedFile
generateTokenInfoFromString r _ | r == P.noRange = return mempty
generateTokenInfoFromString r s = do
  liftIO $ tokenHighlighting <$> Pa.parsePosString Pa.tokensParser p s
  where
    Just p = P.rStart r

-- | Compute syntax highlighting for the given tokens.
tokenHighlighting :: [T.Token] -> CompressedFile
tokenHighlighting = merge . map tokenToCFile
  where
  -- Converts an aspect and a range to a file.
  aToF a r = singletonC (rToR r) (mempty { aspect = Just a })

  -- Merges /sorted, non-overlapping/ compressed files.
  merge = CompressedFile . concat . map ranges

  tokenToCFile :: T.Token -> CompressedFile
  tokenToCFile (T.TokSetN (i, _))               = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokKeyword T.KwSet  i)        = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokKeyword T.KwProp i)        = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokKeyword T.KwForall i)      = aToF Symbol (P.getRange i)
  tokenToCFile (T.TokKeyword _ i)               = aToF Keyword (P.getRange i)
  tokenToCFile (T.TokSymbol  _ i)               = aToF Symbol (P.getRange i)
  tokenToCFile (T.TokLiteral (L.LitInt    r _)) = aToF Number r
  tokenToCFile (T.TokLiteral (L.LitFloat  r _)) = aToF Number r
  tokenToCFile (T.TokLiteral (L.LitString r _)) = aToF String r
  tokenToCFile (T.TokLiteral (L.LitChar   r _)) = aToF String r
  tokenToCFile (T.TokLiteral (L.LitQName  r _)) = aToF String r
  tokenToCFile (T.TokComment (i, _))            = aToF Comment (P.getRange i)
  tokenToCFile (T.TokTeX (i, _))                = aToF Comment (P.getRange i)
  tokenToCFile (T.TokId {})                     = mempty
  tokenToCFile (T.TokQId {})                    = mempty
  tokenToCFile (T.TokString {})                 = mempty
  tokenToCFile (T.TokDummy {})                  = mempty
  tokenToCFile (T.TokEOF {})                    = mempty

-- | A function mapping names to the kind of name they stand for.

type NameKinds = A.QName -> Maybe NameKind

-- | Builds a 'NameKinds' function.

nameKinds :: Level
             -- ^ This should only be @'Full'@ if
             -- type-checking completed successfully (without any
             -- errors).
          -> A.Declaration
          -> TCM NameKinds
nameKinds hlLevel decl = do
  imported <- fix <$> use stImports
  local    <- case hlLevel of
    Full{} -> fix <$> use stSignature
    _      -> return HMap.empty
      -- Traverses the syntax tree and constructs a map from qualified
      -- names to name kinds. TODO: Handle open public.
  let syntax = foldr ($) HMap.empty $ map declToKind $ universeBi decl
  let merged = HMap.unions [local, imported, syntax]
  return (\n -> HMap.lookup n merged)
  where
  fix = HMap.map (defnToKind . theDef) . sigDefinitions

  -- | The 'M.Axiom' constructor is used to represent various things
  -- which are not really axioms, so when maps are merged 'Postulate's
  -- are thrown away whenever possible. The 'declToKind' function
  -- below can return several explanations for one qualified name; the
  -- 'Postulate's are bogus.
  insert = HMap.insertWith dropPostulates
    where
    dropPostulates Postulate k = k
    dropPostulates k         _ = k

  defnToKind :: Defn -> NameKind
  defnToKind   M.Axiom{}                           = Postulate
  defnToKind d@M.Function{} | isProperProjection d = Field
                            | otherwise            = Function
  defnToKind   M.Datatype{}                        = Datatype
  defnToKind   M.Record{}                          = Record
  defnToKind   M.Constructor{ M.conInd = i }       = Constructor i
  defnToKind   M.Primitive{}                       = Primitive

  declToKind :: A.Declaration ->
                HashMap A.QName NameKind -> HashMap A.QName NameKind
  declToKind (A.Axiom _ _ _ q _)    = insert q Postulate
  declToKind (A.Field _ q _)        = insert q Field -- Function
    -- Note that the name q can be used both as a field name and as a
    -- projection function. Highlighting of field names is taken care
    -- of by "theRest" above, which does not use NameKinds.
  declToKind (A.Primitive _ q _)    = insert q Primitive
  declToKind (A.Mutual {})          = id
  declToKind (A.Section {})         = id
  declToKind (A.Apply {})           = id
  declToKind (A.Import {})          = id
  declToKind (A.Pragma {})          = id
  declToKind (A.ScopedDecl {})      = id
  declToKind (A.Open {})            = id
  declToKind (A.PatternSynDef q _ _) = insert q (Constructor Common.Inductive)
  declToKind (A.FunDef  _ q _ _)    = insert q Function
  declToKind (A.UnquoteDecl _ _ q _) = insert q Function
  declToKind (A.DataSig _ q _ _)    = insert q Datatype
  declToKind (A.DataDef _ q _ cs)   = \m ->
                                      insert q Datatype $
                                      foldr (\d -> insert (A.axiomName d)
                                                          (Constructor Common.Inductive))
                                            m cs
  declToKind (A.RecSig _ q _ _)     = insert q Record
  declToKind (A.RecDef _ q _ c _ _ _) = insert q Record .
                                      case c of
                                        Nothing -> id
                                        Just q  -> insert q (Constructor Common.Inductive)

-- | Generates syntax highlighting information for all constructors
-- occurring in patterns and expressions in the given declaration.
--
-- This function should only be called after type checking.
-- Constructors can be overloaded, and the overloading is resolved by
-- the type checker.

generateConstructorInfo
  :: SourceToModule  -- ^ Maps source file paths to module names.
  -> AbsolutePath    -- ^ The module to highlight.
  -> NameKinds
  -> A.Declaration
  -> TCM File
generateConstructorInfo modMap file kinds decl = do

  -- Get boundaries of current declaration.
  -- @noRange@ should be impossible, but in case of @noRange@
  -- it makes sense to return the empty File.
  ifNull (P.getRange decl) (return mempty) $ \ (P.Range is) -> do
  let start = fromIntegral $ P.posPos $ P.iStart $ head is
      end   = fromIntegral $ P.posPos $ P.iEnd   $ last is

  -- Get all disambiguated names that fall within the range of decl.
  m0 <- use stDisambiguatedNames
  let (_, m1) = IntMap.split (pred start) m0
      (m2, _) = IntMap.split end m1
      constrs = IntMap.elems m2

  -- Return suitable syntax highlighting information.
  let files = for constrs $ \ q -> generate modMap file kinds $ A.AmbQ [q]
  return $ Fold.fold files


-- | Prints syntax highlighting info for an error.

printErrorInfo :: TCErr -> TCM ()
printErrorInfo e = printHighlightingInfo . compress =<< errorHighlighting e

-- | Generate highlighting for error.
--   Does something special for termination errors.

errorHighlighting :: TCErr -> TCM File

errorHighlighting (TypeError s cl@(Closure sig env scope (TerminationCheckFailed termErrs))) =
  -- For termination errors, we keep the previous highlighting,
  -- just additionally mark the bad calls.
  return $ terminationErrorHighlighting termErrs

errorHighlighting e = do

  -- Erase previous highlighting.
  let r     = P.getRange e
      erase = singleton (rToR $ P.continuousPerLine r) mempty

  -- Print new highlighting.
  s <- E.prettyError e
  let error = singleton (rToR r)
         $ mempty { otherAspects = [Error]
                  , note         = Just s
                  }
  return $ mconcat [ erase, error ]

-- | Generate syntax highlighting for termination errors.

terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting termErrs = functionDefs `mappend` callSites
  where
    m            = mempty { otherAspects = [TerminationProblem] }
    functionDefs = Fold.foldMap (\x -> singleton (rToR $ bindingSite x) m) $
                   concatMap M.termErrFunctions termErrs
    callSites    = Fold.foldMap (\r -> singleton (rToR r) m) $
                   concatMap (map M.callInfoRange . M.termErrCalls) termErrs

-- | Generates and prints syntax highlighting information for unsolved
-- meta-variables and certain unsolved constraints.

printUnsolvedInfo :: TCM ()
printUnsolvedInfo = do
  metaInfo       <- computeUnsolvedMetaWarnings
  constraintInfo <- computeUnsolvedConstraints

  printHighlightingInfo
    (compress $ metaInfo `mappend` constraintInfo)

-- | Generates syntax highlighting information for unsolved meta
-- variables.

computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings = do
  is <- getInteractionMetas

  -- We don't want to highlight blocked terms, since
  --   * there is always at least one proper meta responsible for the blocking
  --   * in many cases the blocked term covers the highlighting for this meta
  let notBlocked m = not <$> isBlockedTerm m
  ms <- filterM notBlocked =<< getOpenMetas

  rs <- mapM getMetaRange (ms \\ is)
  return $ several (map (rToR . P.continuousPerLine) rs)
                   (mempty { otherAspects = [UnsolvedMeta] })

-- | Generates syntax highlighting information for unsolved constraints
-- that are not connected to a meta variable.

computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints = do
  cs <- getAllConstraints
  -- get ranges of emptyness constraints
  let rs = [ r | PConstr{ theConstraint = Closure{ clValue = IsEmpty r t }} <- cs ]
  return $ several (map (rToR . P.continuousPerLine) rs)
                   (mempty { otherAspects = [UnsolvedConstraint] })

-- | Generates a suitable file for a possibly ambiguous name.

generate :: SourceToModule
            -- ^ Maps source file paths to module names.
         -> AbsolutePath
            -- ^ The module to highlight.
         -> NameKinds
         -> A.AmbiguousQName
         -> File
generate modMap file kinds (A.AmbQ qs) =
  mconcat $ map (\q -> nameToFileA modMap file q include m) qs
  where
    ks   = map kinds qs
    -- Ulf, 2014-06-03: [issue1064] It's better to pick the first rather
    -- than doing no highlighting if there's an ambiguity between an
    -- inductive and coinductive constructor.
    kind = case [ k | Just k <- ks ] of
             k : _ -> Just k
             []    -> Nothing
    -- kind = case (allEqual ks, ks) of
    --          (True, Just k : _) -> Just k
    --          _                  -> Nothing
    -- Note that all names in an AmbiguousQName should have the same
    -- concrete name, so either they are all operators, or none of
    -- them are.
    m isOp  = mempty { aspect = Just $ Name kind isOp }
    include = allEqual (map bindingSite qs)

-- | Converts names to suitable 'File's.

nameToFile :: SourceToModule
              -- ^ Maps source file paths to module names.
           -> AbsolutePath
              -- ^ The file name of the current module. Used for
              -- consistency checking.
           -> [C.Name]
              -- ^ The name qualifier (may be empty).
           -> C.Name
              -- ^ The base name.
           -> (Bool -> Aspects)
              -- ^ Meta information to be associated with the name.
              -- The argument is 'True' iff the name is an operator.
           -> Maybe P.Range
              -- ^ The definition site of the name. The calculated
              -- meta information is extended with this information,
              -- if possible.
           -> File
nameToFile modMap file xs x m mR =
  -- We don't care if we get any funny ranges.
  if all (== Just file) fileNames then
    several (map rToR rs)
            ((m $ C.isOperator x) { definitionSite = mFilePos })
   else
    mempty
  where
  fileNames  = catMaybes $ map (fmap P.srcFile . P.rStart . P.getRange) (x : xs)
  rs         = map P.getRange (x : xs)
  mFilePos   = do
    r <- mR
    P.Pn { P.srcFile = Just f, P.posPos = p } <- P.rStart r
    mod <- Map.lookup f modMap
    return (mod, fromIntegral p)

-- | A variant of 'nameToFile' for qualified abstract names.

nameToFileA
  :: SourceToModule
     -- ^ Maps source file paths to module names.
  -> AbsolutePath
     -- ^ The file name of the current module. Used for
     -- consistency checking.
  -> A.QName
     -- ^ The name.
  -> Bool
     -- ^ Should the binding site be included in the file?
  -> (Bool -> Aspects)
     -- ^ Meta information to be associated with the name.
     -- ^ The argument is 'True' iff the name is an operator.
  -> File
nameToFileA modMap file x include m =
  nameToFile modMap
             file
             (concreteQualifier x)
             (concreteBase x)
             m
             (if include then Just $ bindingSite x else Nothing)

concreteBase :: I.QName -> C.Name
concreteBase = A.nameConcrete . A.qnameName

concreteQualifier :: I.QName -> [C.Name]
concreteQualifier = map A.nameConcrete . A.mnameToList . A.qnameModule

bindingSite :: I.QName -> P.Range
bindingSite = A.nameBindingSite . A.qnameName

-- | Remember a name disambiguation (during type checking).
--   To be used later during syntax highlighting.
storeDisambiguatedName :: A.QName -> TCM ()
storeDisambiguatedName q = whenJust (start $ P.getRange q) $ \ i ->
  stDisambiguatedNames %= IntMap.insert i q
  where
    start (P.Range [])    = Nothing
    start (P.Range (i:_)) = Just $ fromIntegral $ P.posPos $ P.iStart i
    -- TODO: Move start to Agda.Syntax.Position

------------------------------------------------------------------------
-- All tests

-- | All the properties.

tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Generate" []