-- | Generates data used for precise syntax highlighting.

module Agda.Interaction.Highlighting.Generate
  ( Level(..)
  , generateAndPrintSyntaxInfo
  , generateTokenInfo, generateTokenInfoFromSource
  , generateTokenInfoFromString
  , printSyntaxInfo
  , printErrorInfo, errorHighlighting
  , printUnsolvedInfo
  , printHighlightingInfo
  , highlightAsTypeChecked
  , highlightWarning, warningHighlighting
  , computeUnsolvedMetaWarnings
  , computeUnsolvedConstraints
  , storeDisambiguatedName, disambiguateRecordFields
  ) where

import Prelude hiding (null)

import Control.Monad
import Control.Arrow (second)

import Data.Generics.Geniplate
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\))
import qualified Data.List as List
import qualified Data.Foldable as Fold (fold, foldMap, toList)
import qualified Data.IntMap as IntMap
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text.Lazy as T
import Data.Void

import Agda.Interaction.Response
  ( Response( Resp_HighlightingInfo )
  , RemoveTokenBasedHighlighting( KeepHighlighting )
  )
import Agda.Interaction.Highlighting.Precise as P
import Agda.Interaction.Highlighting.Range (rToR, minus)  -- Range is ambiguous

import qualified Agda.TypeChecking.Errors as E
import Agda.TypeChecking.MetaVars (isBlockedTerm)
import Agda.TypeChecking.Monad
  hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Warnings (runPM)

import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..) )
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Info ( ModuleInfo(..), defMacro )
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.Syntax.Position (Range, HasRange, getRange, noRange)

import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- | Highlighting levels.

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

-- | Highlight a warning.
highlightWarning :: TCWarning -> TCM ()
highlightWarning :: TCWarning -> TCM ()
highlightWarning TCWarning
tcwarn = do
  let h :: CompressedFile
h = File -> CompressedFile
compress (File -> CompressedFile) -> File -> CompressedFile
forall a b. (a -> b) -> a -> b
$ TCWarning -> File
warningHighlighting TCWarning
tcwarn
  Lens' CompressedFile TCState
-> (CompressedFile -> CompressedFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' CompressedFile TCState
stSyntaxInfo (CompressedFile
h CompressedFile -> CompressedFile -> CompressedFile
forall a. Semigroup a => a -> a -> a
<>)
  HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting CompressedFile
h

-- | Generate syntax highlighting information for the given
-- declaration, and (if appropriate) print it. If the boolean is
-- 'True', 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 boolean is 'True', then this token
-- highlighting info is additionally removed from 'stTokens'.

generateAndPrintSyntaxInfo
  :: A.Declaration
  -> Level
  -> Bool
     -- ^ Update the state?
  -> TCM ()
generateAndPrintSyntaxInfo :: Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
decl Level
_ Bool
_ | Range -> Bool
forall a. Null a => a -> Bool
null (Range -> Bool) -> Range -> Bool
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
generateAndPrintSyntaxInfo Declaration
decl Level
hlLevel Bool
updateState = do
  AbsolutePath
file <- TCMT IO AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath

  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"import.iface.create" VerboseLevel
15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
      VerboseKey
"Generating syntax info for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> VerboseKey
filePath AbsolutePath
file VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Char
' ' Char -> VerboseKey -> VerboseKey
forall a. a -> [a] -> [a]
:
        case Level
hlLevel of
            Full    {} -> VerboseKey
"(final)"
            Partial {} -> VerboseKey
"(first approximation)"
        VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"."

  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"highlighting.names" VerboseLevel
60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"highlighting names = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [AmbiguousQName] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [AmbiguousQName]
names

  TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
M.ignoreAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    SourceToModule
modMap <- TCM SourceToModule
sourceToModule
    NameKinds
kinds  <- Level -> Declaration -> TCM NameKinds
nameKinds Level
hlLevel Declaration
decl

    let nameInfo :: File
nameInfo = [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (AmbiguousQName -> File) -> [AmbiguousQName] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate SourceToModule
modMap AbsolutePath
file NameKinds
kinds) [AmbiguousQName]
names

    -- After the code has been type checked more information may be
    -- available for overloaded constructors, and
    -- generateConstructorInfo takes advantage of this information.
    -- Note, however, that highlighting for overloaded constructors is
    -- included also in nameInfo.
    File
constructorInfo <- case Level
hlLevel of
      Full{} -> SourceToModule
-> AbsolutePath -> NameKinds -> Declaration -> TCMT IO File
generateConstructorInfo SourceToModule
modMap AbsolutePath
file NameKinds
kinds Declaration
decl
      Level
_      -> File -> TCMT IO File
forall (m :: * -> *) a. Monad m => a -> m a
return File
forall a. Monoid a => a
mempty

    SrcFile
cm <- Range -> SrcFile
P.rangeFile (Range -> SrcFile) -> TCMT IO Range -> TCMT IO SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Range TCEnv -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Range TCEnv
eRange
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"highlighting.warning" VerboseLevel
60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"current path = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ SrcFile -> VerboseKey
forall a. Show a => a -> VerboseKey
show SrcFile
cm

    let (VerboseLevel
from, VerboseLevel
to) = case Range -> Maybe IntervalWithoutFile
forall a. Range' a -> Maybe IntervalWithoutFile
P.rangeToInterval (Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl) of
          Maybe IntervalWithoutFile
Nothing -> (VerboseLevel, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
          Just IntervalWithoutFile
i  -> ( Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iStart IntervalWithoutFile
i
                     , Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd IntervalWithoutFile
i)
    (CompressedFile
prevTokens, (CompressedFile
curTokens, CompressedFile
postTokens)) <-
      (CompressedFile -> (CompressedFile, CompressedFile))
-> (CompressedFile, CompressedFile)
-> (CompressedFile, (CompressedFile, CompressedFile))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (VerboseLevel -> CompressedFile -> (CompressedFile, CompressedFile)
splitAtC VerboseLevel
to) ((CompressedFile, CompressedFile)
 -> (CompressedFile, (CompressedFile, CompressedFile)))
-> (CompressedFile -> (CompressedFile, CompressedFile))
-> CompressedFile
-> (CompressedFile, (CompressedFile, CompressedFile))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> CompressedFile -> (CompressedFile, CompressedFile)
splitAtC VerboseLevel
from (CompressedFile
 -> (CompressedFile, (CompressedFile, CompressedFile)))
-> TCMT IO CompressedFile
-> TCMT IO (CompressedFile, (CompressedFile, CompressedFile))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' CompressedFile TCState -> TCMT IO CompressedFile
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' CompressedFile TCState
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 :: CompressedFile
syntaxInfo = File -> CompressedFile
compress ([File] -> File
forall a. Monoid a => [a] -> a
mconcat [ File
constructorInfo
                                       , SourceToModule -> AbsolutePath -> File
theRest SourceToModule
modMap AbsolutePath
file
                                       , File
nameInfo
                                       ])
                       CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
`mappend`
                     CompressedFile
curTokens

    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
updateState (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Lens' CompressedFile TCState
stSyntaxInfo Lens' CompressedFile TCState
-> (CompressedFile -> CompressedFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
mappend CompressedFile
syntaxInfo
      Lens' CompressedFile TCState
stTokens     Lens' CompressedFile TCState -> CompressedFile -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` (CompressedFile
prevTokens CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
`mappend` CompressedFile
postTokens)

    HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting CompressedFile
syntaxInfo
  where
  -- All names mentioned in the syntax tree (not bound variables).
  names :: [A.AmbiguousQName]
  names :: [AmbiguousQName]
names =
    ((QName -> AmbiguousQName) -> [QName] -> [AmbiguousQName]
forall a b. (a -> b) -> [a] -> [b]
map QName -> AmbiguousQName
I.unambiguous ([QName] -> [AmbiguousQName]) -> [QName] -> [AmbiguousQName]
forall a b. (a -> b) -> a -> b
$
     (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool
isExtendedLambdaName) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$
     Declaration -> [QName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl) [AmbiguousQName] -> [AmbiguousQName] -> [AmbiguousQName]
forall a. [a] -> [a] -> [a]
++
    Declaration -> [AmbiguousQName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl

  -- Bound variables, dotted patterns, record fields, module names,
  -- the "as" and "to" symbols and some other things.
  theRest :: SourceToModule -> AbsolutePath -> File
  theRest :: SourceToModule -> AbsolutePath -> File
theRest SourceToModule
modMap AbsolutePath
file = [File] -> File
forall a. Monoid a => [a] -> a
mconcat
    [ (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getFieldDecl   ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Expr -> File) -> [Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Expr -> File
getVarAndField ([Expr] -> File) -> [Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (LetBinding -> File) -> [LetBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap LetBinding -> File
getLet         ([LetBinding] -> File) -> [LetBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [LetBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (LamBinding -> File) -> [LamBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap LamBinding -> File
getLam         ([LamBinding] -> File) -> [LamBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [LamBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (TypedBinding -> File) -> [TypedBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap TypedBinding -> File
getTyped       ([TypedBinding] -> File) -> [TypedBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [TypedBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Pattern -> File) -> [Pattern] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Pattern -> File
getPattern     ([Pattern] -> File) -> [Pattern] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Pattern]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Pattern' Void -> File) -> [Pattern' Void] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Pattern' Void -> File
getPatternSyn  ([Pattern' Void] -> File) -> [Pattern' Void] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Pattern' Void]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Expr -> File) -> [Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Expr -> File
getExpr        ([Expr] -> File) -> [Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getPatSynArgs  ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (ModuleName -> File) -> [ModuleName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap ModuleName -> File
getModuleName  ([ModuleName] -> File) -> [ModuleName] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [ModuleName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (ModuleInfo -> File) -> [ModuleInfo] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap ModuleInfo -> File
getModuleInfo  ([ModuleInfo] -> File) -> [ModuleInfo] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [ModuleInfo]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (NamedArg Expr -> File) -> [NamedArg Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg Expr -> File
getNamedArgE   ([NamedArg Expr] -> File) -> [NamedArg Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (NamedArg Pattern -> File) -> [NamedArg Pattern] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg Pattern -> File
getNamedArgP   ([NamedArg Pattern] -> File) -> [NamedArg Pattern] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg Pattern]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (NamedArg BindName -> File) -> [NamedArg BindName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg BindName -> File
getNamedArgB   ([NamedArg BindName] -> File) -> [NamedArg BindName] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg BindName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (NamedArg LHSCore -> File) -> [NamedArg LHSCore] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg LHSCore -> File
getNamedArgL   ([NamedArg LHSCore] -> File) -> [NamedArg LHSCore] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg LHSCore]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Quantity -> File) -> [Quantity] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Quantity -> File
getQuantityAttr([Quantity] -> File) -> [Quantity] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Quantity]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    , (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getPragma      ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
    ]
    where
    bound :: BindName -> File
bound A.BindName{ unBind :: BindName -> Name
unBind = Name
n } =
      SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file [] (Name -> Name
A.nameConcrete Name
n) Range
forall a. Range' a
noRange
                 (\Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
                             Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Bound) Bool
isOp })
                 (Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Name -> Range
A.nameBindingSite Name
n)

    patsyn :: AmbiguousQName -> File
patsyn AmbiguousQName
n =               -- TODO: resolve overloading
              SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file (AmbiguousQName -> QName
I.headAmbQ AmbiguousQName
n) Bool
True ((Bool -> Aspects) -> File) -> (Bool -> Aspects) -> File
forall a b. (a -> b) -> a -> b
$ \Bool
isOp ->
                  Aspects
parserBased { aspect :: Maybe Aspect
aspect =
                    Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just (NameKind -> Maybe NameKind) -> NameKind -> Maybe NameKind
forall a b. (a -> b) -> a -> b
$ Induction -> NameKind
Constructor Induction
Common.Inductive) Bool
isOp }

    macro :: QName -> File
macro QName
n = SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file QName
n Bool
True ((Bool -> Aspects) -> File) -> (Bool -> Aspects) -> File
forall a b. (a -> b) -> a -> b
$ \Bool
isOp ->
                  Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Macro) Bool
isOp }

    field :: [C.Name] -> C.Name -> File
    field :: [Name] -> Name -> File
field [Name]
m Name
n = SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file [Name]
m Name
n Range
forall a. Range' a
noRange
                           (\Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
                                       Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Field) Bool
isOp })
                           Maybe Range
forall a. Maybe a
Nothing

    asName :: C.Name -> File
    asName :: Name -> File
asName Name
n = SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file []
                          Name
n Range
forall a. Range' a
noRange
                          (\Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
                                      Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Module) Bool
isOp })
                          Maybe Range
forall a. Maybe a
Nothing

    -- For top level modules, we set the binding site to the beginning of the file
    -- so that clicking on an imported module will jump to the beginning of the file
    -- which defines this module.
    mod :: Bool -> Name -> File
mod Bool
isTopLevelModule Name
n =
      SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file []
                 (Name -> Name
A.nameConcrete Name
n) Range
forall a. Range' a
noRange
                 (\Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
                             Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Module) Bool
isOp })
                 (Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Bool -> (Range -> Range) -> Range -> Range
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
isTopLevelModule Range -> Range
P.beginningOfFile (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$
                           Name -> Range
A.nameBindingSite Name
n)

    getVarAndField :: A.Expr -> File
    getVarAndField :: Expr -> File
getVarAndField (A.Var Name
x)            = BindName -> File
bound (BindName -> File) -> BindName -> File
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName Name
x
    -- Andreas, 2018-06-09, issue #3120
    -- The highlighting for record field tags is now created by the type checker in
    -- function disambiguateRecordFields.
    -- Andreas, Nisse, 2018-10-26, issue #3322
    -- Still, we extract the highlighting info here for uses such as QuickLatex.
    -- The aspects from the disambiguation will be merged in.
    getVarAndField (A.Rec       ExprInfo
_ RecordAssigns
fs)   = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x | Left (FieldAssignment Name
x Expr
_) <- RecordAssigns
fs ]
    getVarAndField (A.RecUpdate ExprInfo
_ Expr
_ Assigns
fs) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x |      (FieldAssignment Name
x Expr
_) <- Assigns
fs ]
    getVarAndField Expr
_                    = File
forall a. Monoid a => a
mempty

    -- Ulf, 2019-01-30: It would be nicer to not have to specialize it, but
    -- you can't have polymorphic functions in universeBi.
    getNamedArgE :: Common.NamedArg A.Expr -> File
    getNamedArgE :: NamedArg Expr -> File
getNamedArgE = NamedArg Expr -> File
forall a. NamedArg a -> File
getNamedArg
    getNamedArgP :: Common.NamedArg A.Pattern -> File
    getNamedArgP :: NamedArg Pattern -> File
getNamedArgP = NamedArg Pattern -> File
forall a. NamedArg a -> File
getNamedArg
    getNamedArgB :: Common.NamedArg A.BindName -> File
    getNamedArgB :: NamedArg BindName -> File
getNamedArgB = NamedArg BindName -> File
forall a. NamedArg a -> File
getNamedArg
    getNamedArgL :: Common.NamedArg A.LHSCore -> File
    getNamedArgL :: NamedArg LHSCore -> File
getNamedArgL = NamedArg LHSCore -> File
forall a. NamedArg a -> File
getNamedArg

    getNamedArg :: Common.NamedArg a -> File
    getNamedArg :: NamedArg a -> File
getNamedArg NamedArg a
x = Maybe NamedName -> File -> (NamedName -> File) -> File
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Named NamedName a -> Maybe NamedName
forall name a. Named name a -> Maybe name
Common.nameOf (Named NamedName a -> Maybe NamedName)
-> Named NamedName a -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ NamedArg a -> Named NamedName a
forall e. Arg e -> e
Common.unArg NamedArg a
x) File
forall a. Monoid a => a
mempty ((NamedName -> File) -> File) -> (NamedName -> File) -> File
forall a b. (a -> b) -> a -> b
$ \ NamedName
s ->
      Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ NamedName -> Range
forall t. HasRange t => t -> Range
getRange NamedName
s) (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$
        Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Argument) Bool
False }

    getBinder :: A.Binder -> File
    getBinder :: Binder -> File
getBinder (A.Binder Maybe Pattern
_ BindName
n) = BindName -> File
bound BindName
n

    getLet :: A.LetBinding -> File
    getLet :: LetBinding -> File
getLet (A.LetBind LetInfo
_ ArgInfo
_ BindName
x Expr
_ Expr
_)     = BindName -> File
bound BindName
x
    getLet A.LetPatBind{}            = File
forall a. Monoid a => a
mempty
    getLet A.LetApply{}              = File
forall a. Monoid a => a
mempty
    getLet A.LetOpen{}               = File
forall a. Monoid a => a
mempty
    getLet (A.LetDeclaredVariable BindName
x) = BindName -> File
bound BindName
x

    getLam :: A.LamBinding -> File
    getLam :: LamBinding -> File
getLam (A.DomainFree TacticAttr
_ NamedArg Binder
xs) = Binder -> File
getBinder (NamedArg Binder -> Binder
forall a. NamedArg a -> a
Common.namedArg NamedArg Binder
xs)
    getLam (A.DomainFull {})   = File
forall a. Monoid a => a
mempty

    getTyped :: A.TypedBinding -> File
    getTyped :: TypedBinding -> File
getTyped (A.TBind Range
_ TacticAttr
_ [NamedArg Binder]
xs Expr
_) = (NamedArg Binder -> File) -> [NamedArg Binder] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (Binder -> File
getBinder (Binder -> File)
-> (NamedArg Binder -> Binder) -> NamedArg Binder -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Binder -> Binder
forall a. NamedArg a -> a
Common.namedArg) [NamedArg Binder]
xs
    getTyped A.TLet{}           = File
forall a. Monoid a => a
mempty

    getPatSynArgs :: A.Declaration -> File
    getPatSynArgs :: Declaration -> File
getPatSynArgs (A.PatternSynDef QName
_ [Arg Name]
xs Pattern' Void
_) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (Arg Name -> File) -> [Arg Name] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (BindName -> File
bound (BindName -> File) -> (Arg Name -> BindName) -> Arg Name -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
A.mkBindName (Name -> BindName) -> (Arg Name -> Name) -> Arg Name -> BindName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Name -> Name
forall e. Arg e -> e
Common.unArg) [Arg Name]
xs
    getPatSynArgs Declaration
_                        = File
forall a. Monoid a => a
mempty

    -- Issue #4361, highlight BUILTINs like NAT, EQUALITY etc. in keyword color.
    getPragma :: A.Declaration -> File
    getPragma :: Declaration -> File
getPragma = \case
      A.Pragma Range
_ Pragma
p ->
        case Pragma
p of
          A.BuiltinPragma RString
b ResolvedName
_      -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
          A.BuiltinNoDefPragma RString
b QName
_ -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
          A.CompilePragma RString
b QName
_ VerboseKey
_    -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
          A.RewritePragma Range
r [QName]
_      -> Range -> File
forall a. HasRange a => a -> File
keyword Range
r
          A.OptionsPragma{}   -> File
forall a. Monoid a => a
mempty
          A.StaticPragma{}    -> File
forall a. Monoid a => a
mempty
          A.EtaPragma{}       -> File
forall a. Monoid a => a
mempty
          A.InjectivePragma{} -> File
forall a. Monoid a => a
mempty
          A.InlinePragma{}    -> File
forall a. Monoid a => a
mempty
          A.DisplayPragma{}   -> File
forall a. Monoid a => a
mempty
      Declaration
_ -> File
forall a. Monoid a => a
mempty

    keyword :: HasRange a => a -> File
    keyword :: a -> File
keyword a
x = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ a -> Range
forall t. HasRange t => t -> Range
getRange a
x) (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Keyword }

    getPattern' :: IsProjP e => A.Pattern' e -> File
    getPattern' :: Pattern' e -> File
getPattern' (A.VarP BindName
x)    = BindName -> File
bound BindName
x
    getPattern' (A.AsP PatInfo
_ BindName
x Pattern' e
_) = BindName -> File
bound BindName
x
    getPattern' (A.DotP PatInfo
pi e
e)
      | Just (ProjOrigin, AmbiguousQName)
_ <- e -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP e
e = File
forall a. Monoid a => a
mempty
      | Bool
otherwise =
          Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ PatInfo -> Range
forall t. HasRange t => t -> Range
getRange PatInfo
pi)
                (Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
DottedPattern })
    getPattern' (A.PatternSynP PatInfo
_ AmbiguousQName
q NAPs e
_) = AmbiguousQName -> File
patsyn AmbiguousQName
q
    -- Andreas, 2018-06-09, issue #3120
    -- The highlighting for record field tags is now created by the type checker in
    -- function disambiguateRecordFields.
    -- Andreas, Nisse, 2018-10-26, issue #3322
    -- Still, we extract the highlighting info here for uses such as QuickLatex.
    -- The aspects from the disambiguation will be merged in.
    getPattern' (A.RecP PatInfo
_ [FieldAssignment' (Pattern' e)]
fs) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x | FieldAssignment Name
x Pattern' e
_ <- [FieldAssignment' (Pattern' e)]
fs ]
    getPattern' Pattern' e
_             = File
forall a. Monoid a => a
mempty

    getPattern :: A.Pattern -> File
    getPattern :: Pattern -> File
getPattern = Pattern -> File
forall e. IsProjP e => Pattern' e -> File
getPattern'

    getPatternSyn :: A.Pattern' Void -> File
    getPatternSyn :: Pattern' Void -> File
getPatternSyn = Pattern' Void -> File
forall e. IsProjP e => Pattern' e -> File
getPattern'

    getExpr :: A.Expr -> File
    getExpr :: Expr -> File
getExpr (A.PatternSyn AmbiguousQName
q) = AmbiguousQName -> File
patsyn AmbiguousQName
q
    getExpr (A.Macro QName
q)      = QName -> File
macro QName
q
    getExpr Expr
_                = File
forall a. Monoid a => a
mempty

    getFieldDecl :: A.Declaration -> File
    getFieldDecl :: Declaration -> File
getFieldDecl (A.RecDef DefInfo
_ QName
_ UniverseCheck
_ Maybe (Ranged Induction)
_ Maybe HasEta
_ Maybe QName
_ DataDefParams
_ Expr
_ [Declaration]
fs) = (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
extractField [Declaration]
fs
      where
      extractField :: Declaration -> File
extractField (A.ScopedDecl ScopeInfo
_ [Declaration]
ds) = (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
extractField [Declaration]
ds
      extractField (A.Field DefInfo
_ QName
x Arg Expr
_)     = [Name] -> Name -> File
field (QName -> [Name]
concreteQualifier QName
x)
                                               (QName -> Name
concreteBase QName
x)
      extractField Declaration
_                   = File
forall a. Monoid a => a
mempty
    getFieldDecl Declaration
_                   = File
forall a. Monoid a => a
mempty

    getModuleName :: A.ModuleName -> File
    getModuleName :: ModuleName -> File
getModuleName m :: ModuleName
m@(A.MName { mnameToList :: ModuleName -> [Name]
A.mnameToList = [Name]
xs }) =
      [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (Name -> File) -> [Name] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Name -> File
mod Bool
isTopLevelModule) [Name]
xs
      where
      isTopLevelModule :: Bool
isTopLevelModule =
        case (Name -> Maybe AbsolutePath) -> [Name] -> [AbsolutePath]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Maybe AbsolutePath) -> Maybe AbsolutePath
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe AbsolutePath) -> Maybe AbsolutePath)
-> (Name -> Maybe (Maybe AbsolutePath))
-> Name
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  (Position' SrcFile -> Maybe AbsolutePath)
-> Maybe (Position' SrcFile) -> Maybe (Maybe AbsolutePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcFile -> Maybe AbsolutePath
forall a. Maybe a -> Maybe a
Strict.toLazy (SrcFile -> Maybe AbsolutePath)
-> (Position' SrcFile -> SrcFile)
-> Position' SrcFile
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' SrcFile -> SrcFile
forall a. Position' a -> a
P.srcFile) (Maybe (Position' SrcFile) -> Maybe (Maybe AbsolutePath))
-> (Name -> Maybe (Position' SrcFile))
-> Name
-> Maybe (Maybe AbsolutePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart (Range -> Maybe (Position' SrcFile))
-> (Name -> Range) -> Name -> Maybe (Position' SrcFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  Name -> Range
A.nameBindingSite) [Name]
xs of
          AbsolutePath
f : [AbsolutePath]
_ -> AbsolutePath -> SourceToModule -> Maybe TopLevelModuleName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AbsolutePath
f SourceToModule
modMap Maybe TopLevelModuleName -> Maybe TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
==
                   TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just (QName -> TopLevelModuleName
C.toTopLevelModuleName (QName -> TopLevelModuleName) -> QName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
A.mnameToConcrete ModuleName
m)
          []    -> Bool
False

    getModuleInfo :: ModuleInfo -> File
    getModuleInfo :: ModuleInfo -> File
getModuleInfo (ModuleInfo{ Range
minfoAsTo :: ModuleInfo -> Range
minfoAsTo :: Range
minfoAsTo, Maybe Name
minfoAsName :: ModuleInfo -> Maybe Name
minfoAsName :: Maybe Name
minfoAsName }) =
      Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
minfoAsTo) (Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Symbol })
        File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend`
      File -> (Name -> File) -> Maybe Name -> File
forall b a. b -> (a -> b) -> Maybe a -> b
maybe File
forall a. Monoid a => a
mempty Name -> File
asName Maybe Name
minfoAsName

    -- If the Quantity attribute comes with a Range, highlight the
    -- corresponding attribute as Symbol.
    getQuantityAttr :: Common.Quantity -> File
    getQuantityAttr :: Quantity -> File
getQuantityAttr Quantity
q = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Quantity -> Range
forall t. HasRange t => t -> Range
getRange Quantity
q) (Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Symbol })

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

generateTokenInfo :: AbsolutePath -> TCM CompressedFile
generateTokenInfo :: AbsolutePath -> TCMT IO CompressedFile
generateTokenInfo AbsolutePath
file =
  AbsolutePath -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromSource AbsolutePath
file (VerboseKey -> TCMT IO CompressedFile)
-> (Text -> VerboseKey) -> Text -> TCMT IO CompressedFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> VerboseKey
T.unpack (Text -> TCMT IO CompressedFile)
-> TCMT IO Text -> TCMT IO CompressedFile
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    PM Text -> TCMT IO Text
forall a. PM a -> TCM a
runPM (AbsolutePath -> PM Text
Pa.readFilePM AbsolutePath
file)

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

generateTokenInfoFromSource
  :: AbsolutePath
     -- ^ The module to highlight.
  -> String
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> TCM CompressedFile
generateTokenInfoFromSource :: AbsolutePath -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromSource AbsolutePath
file VerboseKey
input =
  PM CompressedFile -> TCMT IO CompressedFile
forall a. PM a -> TCM a
runPM (PM CompressedFile -> TCMT IO CompressedFile)
-> PM CompressedFile -> TCMT IO CompressedFile
forall a b. (a -> b) -> a -> b
$ [Token] -> CompressedFile
tokenHighlighting ([Token] -> CompressedFile)
-> (([Token], FileType) -> [Token])
-> ([Token], FileType)
-> CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Token], FileType) -> [Token]
forall a b. (a, b) -> a
fst (([Token], FileType) -> CompressedFile)
-> PM ([Token], FileType) -> PM CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token]
-> AbsolutePath -> VerboseKey -> PM ([Token], FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> VerboseKey -> PM (a, FileType)
Pa.parseFile Parser [Token]
Pa.tokensParser AbsolutePath
file VerboseKey
input

-- | Generate and return the syntax highlighting information for the
-- tokens in the given string, which is assumed to correspond to the
-- given range.

generateTokenInfoFromString :: Range -> String -> TCM CompressedFile
generateTokenInfoFromString :: Range -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromString Range
r VerboseKey
_ | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
forall a. Range' a
noRange = CompressedFile -> TCMT IO CompressedFile
forall (m :: * -> *) a. Monad m => a -> m a
return CompressedFile
forall a. Monoid a => a
mempty
generateTokenInfoFromString Range
r VerboseKey
s = do
  PM CompressedFile -> TCMT IO CompressedFile
forall a. PM a -> TCM a
runPM (PM CompressedFile -> TCMT IO CompressedFile)
-> PM CompressedFile -> TCMT IO CompressedFile
forall a b. (a -> b) -> a -> b
$ [Token] -> CompressedFile
tokenHighlighting ([Token] -> CompressedFile) -> PM [Token] -> PM CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] -> Position' SrcFile -> VerboseKey -> PM [Token]
forall a. Parser a -> Position' SrcFile -> VerboseKey -> PM a
Pa.parsePosString Parser [Token]
Pa.tokensParser Position' SrcFile
p VerboseKey
s
  where
    Just Position' SrcFile
p = Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r

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

  -- Merges /sorted, non-overlapping/ compressed files.
  merge :: [CompressedFile] -> CompressedFile
merge = [(Range, Aspects)] -> CompressedFile
CompressedFile ([(Range, Aspects)] -> CompressedFile)
-> ([CompressedFile] -> [(Range, Aspects)])
-> [CompressedFile]
-> CompressedFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Range, Aspects)]] -> [(Range, Aspects)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Range, Aspects)]] -> [(Range, Aspects)])
-> ([CompressedFile] -> [[(Range, Aspects)]])
-> [CompressedFile]
-> [(Range, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CompressedFile -> [(Range, Aspects)])
-> [CompressedFile] -> [[(Range, Aspects)]]
forall a b. (a -> b) -> [a] -> [b]
map CompressedFile -> [(Range, Aspects)]
ranges

  tokenToCFile :: T.Token -> CompressedFile
  tokenToCFile :: Token -> CompressedFile
tokenToCFile (T.TokSetN (Interval
i, Integer
_))               = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokPropN (Interval
i, Integer
_))              = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokKeyword Keyword
T.KwSet  Interval
i)        = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokKeyword Keyword
T.KwProp Interval
i)        = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokKeyword Keyword
T.KwForall Interval
i)      = Aspect -> Range -> CompressedFile
aToF Aspect
Symbol (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokKeyword Keyword
T.KwREWRITE Interval
_)     = CompressedFile
forall a. Monoid a => a
mempty  -- #4361, REWRITE is not always a Keyword
  tokenToCFile (T.TokKeyword Keyword
_ Interval
i)               = Aspect -> Range -> CompressedFile
aToF Aspect
Keyword (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokSymbol  Symbol
_ Interval
i)               = Aspect -> Range -> CompressedFile
aToF Aspect
Symbol (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokLiteral (L.LitNat    Range
r Integer
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
  tokenToCFile (T.TokLiteral (L.LitWord64 Range
r Word64
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
  tokenToCFile (T.TokLiteral (L.LitFloat  Range
r Double
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
  tokenToCFile (T.TokLiteral (L.LitString Range
r VerboseKey
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
  tokenToCFile (T.TokLiteral (L.LitChar   Range
r Char
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
  tokenToCFile (T.TokLiteral (L.LitQName  Range
r QName
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
  tokenToCFile (T.TokLiteral (L.LitMeta Range
r AbsolutePath
_ MetaId
_)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
  tokenToCFile (T.TokComment (Interval
i, VerboseKey
_))            = Aspect -> Range -> CompressedFile
aToF Aspect
Comment (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokTeX (Interval
i, VerboseKey
_))                = Aspect -> Range -> CompressedFile
aToF Aspect
Background (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokMarkup (Interval
i, VerboseKey
_))             = Aspect -> Range -> CompressedFile
aToF Aspect
Markup (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokId {})                     = CompressedFile
forall a. Monoid a => a
mempty
  tokenToCFile (T.TokQId {})                    = CompressedFile
forall a. Monoid a => a
mempty
  tokenToCFile (T.TokString (Interval
i,VerboseKey
s))              = Aspect -> Range -> CompressedFile
aToF Aspect
Pragma (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
  tokenToCFile (T.TokDummy {})                  = CompressedFile
forall a. Monoid a => a
mempty
  tokenToCFile (T.TokEOF {})                    = CompressedFile
forall a. Monoid a => a
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 :: Level -> Declaration -> TCM NameKinds
nameKinds Level
hlLevel Declaration
decl = do
  HashMap QName Definition
imported <- Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' (HashMap QName Definition) TCState
 -> TCMT IO (HashMap QName Definition))
-> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stImports ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
  HashMap QName Definition
local    <- case Level
hlLevel of
    Full{} -> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' (HashMap QName Definition) TCState
 -> TCMT IO (HashMap QName Definition))
-> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
    Level
_      -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. Monad m => a -> m a
return HashMap QName Definition
forall k v. HashMap k v
HMap.empty
  Map QName PatternSynDefn
impPatSyns <- Lens' (Map QName PatternSynDefn) TCState
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSynImports
  Map QName PatternSynDefn
locPatSyns <- case Level
hlLevel of
    Full{} -> Lens' (Map QName PatternSynDefn) TCState
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSyns
    Level
_      -> Map QName PatternSynDefn -> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. Monad m => a -> m a
return Map QName PatternSynDefn
forall a. Null a => a
empty
      -- Traverses the syntax tree and constructs a map from qualified
      -- names to name kinds. TODO: Handle open public.
  let syntax :: HashMap QName NameKind
syntax = ((HashMap QName NameKind -> HashMap QName NameKind)
 -> HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> [HashMap QName NameKind -> HashMap QName NameKind]
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind -> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
($) HashMap QName NameKind
forall k v. HashMap k v
HMap.empty ([HashMap QName NameKind -> HashMap QName NameKind]
 -> HashMap QName NameKind)
-> [HashMap QName NameKind -> HashMap QName NameKind]
-> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
$ (Declaration -> HashMap QName NameKind -> HashMap QName NameKind)
-> [Declaration]
-> [HashMap QName NameKind -> HashMap QName NameKind]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> HashMap QName NameKind -> HashMap QName NameKind
declToKind ([Declaration]
 -> [HashMap QName NameKind -> HashMap QName NameKind])
-> [Declaration]
-> [HashMap QName NameKind -> HashMap QName NameKind]
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
  NameKinds -> TCM NameKinds
forall (m :: * -> *) a. Monad m => a -> m a
return (NameKinds -> TCM NameKinds) -> NameKinds -> TCM NameKinds
forall a b. (a -> b) -> a -> b
$ \ QName
n -> (NameKind -> NameKind -> NameKind)
-> [Maybe NameKind] -> Maybe NameKind
forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
unionsMaybeWith NameKind -> NameKind -> NameKind
merge
    [ Defn -> NameKind
defnToKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
local
    , NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
locPatSyns
    , Defn -> NameKind
defnToKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
imported
    , NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
impPatSyns
    , QName -> HashMap QName NameKind -> Maybe NameKind
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName NameKind
syntax
    ]
  where

  -- | 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.
  merge :: NameKind -> NameKind -> NameKind
merge NameKind
Postulate NameKind
k = NameKind
k
  merge NameKind
_     NameKind
Macro = NameKind
Macro  -- If the abstract syntax says macro, it's a macro.
  merge NameKind
k         NameKind
_ = NameKind
k

  insert :: QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert = (NameKind -> NameKind -> NameKind)
-> QName
-> NameKind
-> HashMap QName NameKind
-> HashMap QName NameKind
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith NameKind -> NameKind -> NameKind
merge

  defnToKind :: Defn -> NameKind
  defnToKind :: Defn -> NameKind
defnToKind   M.Axiom{}                           = NameKind
Postulate
  defnToKind   M.DataOrRecSig{}                    = NameKind
Postulate
  defnToKind   M.GeneralizableVar{}                = NameKind
Generalizable
  defnToKind d :: Defn
d@M.Function{} | Defn -> Bool
isProperProjection Defn
d = NameKind
Field
                            | Bool
otherwise            = NameKind
Function
  defnToKind   M.Datatype{}                        = NameKind
Datatype
  defnToKind   M.Record{}                          = NameKind
Record
  defnToKind   M.Constructor{ conInd :: Defn -> Induction
M.conInd = Induction
i }       = Induction -> NameKind
Constructor Induction
i
  defnToKind   M.Primitive{}                       = NameKind
Primitive
  defnToKind   M.AbstractDefn{}                    = NameKind
forall a. HasCallStack => a
__IMPOSSIBLE__

  declToKind :: A.Declaration ->
                HashMap A.QName NameKind -> HashMap A.QName NameKind
  declToKind :: Declaration -> HashMap QName NameKind -> HashMap QName NameKind
declToKind (A.Axiom Axiom
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_)
    | DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
Common.MacroDef = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Macro
    | Bool
otherwise                     = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Postulate
  declToKind (A.Field DefInfo
_ QName
q Arg Expr
_)        = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
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 DefInfo
_ QName
q Expr
_)    = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Primitive
  declToKind (A.Mutual {})          = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.Section {})         = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.Apply {})           = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.Import {})          = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.Pragma {})          = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.ScopedDecl {})      = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.Open {})            = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
  declToKind (A.PatternSynDef QName
q [Arg Name]
_ Pattern' Void
_) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
con
  declToKind (A.Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
q Expr
_) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Generalizable
  declToKind (A.FunDef  DefInfo
_ QName
q Delayed
_ [Clause]
_)     = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function
  declToKind (A.UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
qs Expr
_) = (QName
 -> (HashMap QName NameKind -> HashMap QName NameKind)
 -> HashMap QName NameKind
 -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> [QName]
-> HashMap QName NameKind
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ QName
q HashMap QName NameKind -> HashMap QName NameKind
f -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap QName NameKind -> HashMap QName NameKind
f) HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id [QName]
qs
  declToKind (A.UnquoteDef [DefInfo]
_ [QName]
qs Expr
_)    = (QName
 -> (HashMap QName NameKind -> HashMap QName NameKind)
 -> HashMap QName NameKind
 -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> [QName]
-> HashMap QName NameKind
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ QName
q HashMap QName NameKind -> HashMap QName NameKind
f -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap QName NameKind -> HashMap QName NameKind
f) HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id [QName]
qs
  declToKind (A.DataSig DefInfo
_ QName
q GeneralizeTelescope
_ Expr
_)      = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Datatype
  declToKind (A.DataDef DefInfo
_ QName
q UniverseCheck
_ DataDefParams
_ [Declaration]
cs)   = \HashMap QName NameKind
m ->
                                      QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Datatype (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind -> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
$
                                      (Declaration -> HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> [Declaration]
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Declaration
d -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert (Declaration -> QName
A.axiomName Declaration
d) NameKind
con)
                                            HashMap QName NameKind
m [Declaration]
cs
  declToKind (A.RecSig DefInfo
_ QName
q GeneralizeTelescope
_ Expr
_)       = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Record
  declToKind (A.RecDef DefInfo
_ QName
q UniverseCheck
_ Maybe (Ranged Induction)
_ Maybe HasEta
_ Maybe QName
c DataDefParams
_ Expr
_ [Declaration]
_) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Record (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName NameKind -> HashMap QName NameKind)
-> (QName -> HashMap QName NameKind -> HashMap QName NameKind)
-> Maybe QName
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id (QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
`insert` NameKind
con) Maybe QName
c

  con :: NameKind
  con :: NameKind
con = Induction -> NameKind
Constructor Induction
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 :: SourceToModule
-> AbsolutePath -> NameKinds -> Declaration -> TCMT IO File
generateConstructorInfo SourceToModule
modMap AbsolutePath
file NameKinds
kinds Declaration
decl = do

  -- Get boundaries of current declaration.
  -- @noRange@ should be impossible, but in case of @noRange@
  -- it makes sense to return the empty File.
  [IntervalWithoutFile]
-> TCMT IO File
-> ([IntervalWithoutFile] -> TCMT IO File)
-> TCMT IO File
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Range -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals (Range -> [IntervalWithoutFile]) -> Range -> [IntervalWithoutFile]
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl)
         (File -> TCMT IO File
forall (m :: * -> *) a. Monad m => a -> m a
return File
forall a. Monoid a => a
mempty) (([IntervalWithoutFile] -> TCMT IO File) -> TCMT IO File)
-> ([IntervalWithoutFile] -> TCMT IO File) -> TCMT IO File
forall a b. (a -> b) -> a -> b
$ \[IntervalWithoutFile]
is -> do
    let start :: VerboseLevel
start = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iStart (IntervalWithoutFile -> Position' ())
-> IntervalWithoutFile -> Position' ()
forall a b. (a -> b) -> a -> b
$ [IntervalWithoutFile] -> IntervalWithoutFile
forall a. [a] -> a
head [IntervalWithoutFile]
is
        end :: VerboseLevel
end   = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd   (IntervalWithoutFile -> Position' ())
-> IntervalWithoutFile -> Position' ()
forall a b. (a -> b) -> a -> b
$ [IntervalWithoutFile] -> IntervalWithoutFile
forall a. [a] -> a
last [IntervalWithoutFile]
is

    -- Get all disambiguated names that fall within the range of decl.
    DisambiguatedNames
m0 <- Lens' DisambiguatedNames TCState -> TCMT IO DisambiguatedNames
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisambiguatedNames TCState
stDisambiguatedNames
    let (DisambiguatedNames
_, DisambiguatedNames
m1) = VerboseLevel
-> DisambiguatedNames -> (DisambiguatedNames, DisambiguatedNames)
forall a. VerboseLevel -> IntMap a -> (IntMap a, IntMap a)
IntMap.split (VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
pred VerboseLevel
start) DisambiguatedNames
m0
        (DisambiguatedNames
m2, DisambiguatedNames
_) = VerboseLevel
-> DisambiguatedNames -> (DisambiguatedNames, DisambiguatedNames)
forall a. VerboseLevel -> IntMap a -> (IntMap a, IntMap a)
IntMap.split VerboseLevel
end DisambiguatedNames
m1
        constrs :: [QName]
constrs = DisambiguatedNames -> [QName]
forall a. IntMap a -> [a]
IntMap.elems DisambiguatedNames
m2

    -- Return suitable syntax highlighting information.
    let files :: [File]
files = [QName] -> (QName -> File) -> [File]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [QName]
constrs ((QName -> File) -> [File]) -> (QName -> File) -> [File]
forall a b. (a -> b) -> a -> b
$ \ QName
q -> SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate SourceToModule
modMap AbsolutePath
file NameKinds
kinds (AmbiguousQName -> File) -> AmbiguousQName -> File
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
I.unambiguous QName
q
    File -> TCMT IO File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCMT IO File) -> File -> TCMT IO File
forall a b. (a -> b) -> a -> b
$ [File] -> File
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [File]
files

printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo Range
r = do
  CompressedFile
syntaxInfo <- Lens' CompressedFile TCState -> TCMT IO CompressedFile
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' CompressedFile TCState
stSyntaxInfo
  HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Range -> CompressedFile -> CompressedFile
selectC Range
r CompressedFile
syntaxInfo)

-- | Prints syntax highlighting info for an error.

printErrorInfo :: TCErr -> TCM ()
printErrorInfo :: TCErr -> TCM ()
printErrorInfo TCErr
e =
  RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (CompressedFile -> TCM ())
-> (File -> CompressedFile) -> File -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> CompressedFile
compress (File -> TCM ()) -> TCMT IO File -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
    TCErr -> TCMT IO File
errorHighlighting TCErr
e

-- | Generate highlighting for error.

errorHighlighting :: TCErr -> TCM File
errorHighlighting :: TCErr -> TCMT IO File
errorHighlighting TCErr
e = do

  -- Erase previous highlighting.
  let r :: Range
r     = TCErr -> Range
forall t. HasRange t => t -> Range
getRange TCErr
e
      erase :: File
erase = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
forall a. Monoid a => a
mempty

  -- Print new highlighting.
  VerboseKey
s <- TCErr -> TCMT IO VerboseKey
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
E.prettyError TCErr
e
  let error :: File
error = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
r)
         (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
Error
                       , note :: Maybe VerboseKey
note         = VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just VerboseKey
s
                       }
  File -> TCMT IO File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCMT IO File) -> File -> TCMT IO File
forall a b. (a -> b) -> a -> b
$ [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ File
erase, File
error ]

-- | Generate syntax highlighting for warnings.

warningHighlighting :: TCWarning -> File
warningHighlighting :: TCWarning -> File
warningHighlighting TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of
  TerminationIssue [TerminationError]
terrs     -> [TerminationError] -> File
terminationErrorHighlighting [TerminationError]
terrs
  NotStrictlyPositive QName
d Seq OccursWhere
ocs  -> QName -> Seq OccursWhere -> File
positivityErrorHighlighting QName
d Seq OccursWhere
ocs
  -- #3965 highlight each unreachable clause independently: they
  -- may be interleaved with actually reachable clauses!
  UnreachableClauses QName
_ [Range]
rs    -> (Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Range -> File
deadcodeHighlighting [Range]
rs
  CoverageIssue{}            -> Range -> File
coverageErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  CoverageNoExactSplit{}     -> Range -> File
catchallHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  UnsolvedConstraints Constraints
cs     -> Constraints -> File
constraintsHighlighting Constraints
cs
  UnsolvedMetaVariables [Range]
rs   -> [Range] -> File
metasHighlighting [Range]
rs
  AbsurdPatternRequiresNoRHS{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  ModuleDoesntExport{}         -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  FixityInRenamingModule NonEmpty Range
rs    -> (Range -> File) -> NonEmpty Range -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Range -> File
deadcodeHighlighting NonEmpty Range
rs
  -- expanded catch-all case to get a warning for new constructors
  CantGeneralizeOverSorts{}  -> File
forall a. Monoid a => a
mempty
  UnsolvedInteractionMetas{} -> File
forall a. Monoid a => a
mempty
  OldBuiltin{}               -> File
forall a. Monoid a => a
mempty
  EmptyRewritePragma{}       -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  IllformedAsClause{}        -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  UselessPublic{}            -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  UselessInline{}            -> File
forall a. Monoid a => a
mempty
  ClashesViaRenaming NameOrModule
_ [Name]
xs    -> (Name -> File) -> [Name] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (Range -> File
deadcodeHighlighting (Range -> File) -> (Name -> Range) -> Name -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
forall t. HasRange t => t -> Range
getRange) [Name]
xs
    -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
    -- Should we have a different color?
  WrongInstanceDeclaration{} -> File
forall a. Monoid a => a
mempty
  InstanceWithExplicitArg{}  -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  InstanceNoOutputTypeName{} -> File
forall a. Monoid a => a
mempty
  InstanceArgWithExplicitArg{} -> File
forall a. Monoid a => a
mempty
  ParseWarning{}             -> File
forall a. Monoid a => a
mempty
  InversionDepthReached{}    -> File
forall a. Monoid a => a
mempty
  GenericWarning{}           -> File
forall a. Monoid a => a
mempty
  GenericNonFatalError{}     -> File
forall a. Monoid a => a
mempty
  SafeFlagPostulate{}        -> File
forall a. Monoid a => a
mempty
  SafeFlagPragma{}           -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagNonTerminating     -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagTerminating        -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagWithoutKFlagPrimEraseEquality -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagEta                -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagInjective          -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagNoCoverageCheck    -> File
forall a. Monoid a => a
mempty
  Warning
WithoutKFlagPrimEraseEquality -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagNoPositivityCheck  -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagPolarity           -> File
forall a. Monoid a => a
mempty
  Warning
SafeFlagNoUniverseCheck    -> File
forall a. Monoid a => a
mempty
  DeprecationWarning{}       -> File
forall a. Monoid a => a
mempty
  UserWarning{}              -> File
forall a. Monoid a => a
mempty
  LibraryWarning{}           -> File
forall a. Monoid a => a
mempty
  InfectiveImport{}          -> File
forall a. Monoid a => a
mempty
  CoInfectiveImport{}        -> File
forall a. Monoid a => a
mempty
  RewriteNonConfluent{}      -> Range -> File
confluenceErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  RewriteMaybeNonConfluent{} -> Range -> File
confluenceErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  PragmaCompileErased{}      -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  NotInScopeW{}              -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
  NicifierIssue DeclarationWarning
w           -> case DeclarationWarning
w of
    -- we intentionally override the binding of `w` here so that our pattern of
    -- using `getRange w` still yields the most precise range information we
    -- can get.
    NotAllowedInMutual{}             -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyAbstract{}                  -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyInstance{}                  -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyMacro{}                     -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyMutual{}                    -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyPostulate{}                 -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyPrimitive{}                 -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyPrivate{}                   -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyGeneralize{}                -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    EmptyField{}                     -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    UselessAbstract{}                -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    UselessInstance{}                -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    UselessPrivate{}                 -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    InvalidNoPositivityCheckPragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    InvalidNoUniverseCheckPragma{}   -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    InvalidTerminationCheckPragma{}  -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    InvalidCoverageCheckPragma{}     -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    OpenPublicAbstract{}             -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    OpenPublicPrivate{}              -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    W.ShadowingInTelescope [(Name, [Range])]
nrs       -> ((Name, [Range]) -> File) -> [(Name, [Range])] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap
                                          ([Range] -> File
shadowingTelHighlighting ([Range] -> File)
-> ((Name, [Range]) -> [Range]) -> (Name, [Range]) -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Range]) -> [Range]
forall a b. (a, b) -> b
snd)
                                          [(Name, [Range])]
nrs
    MissingDefinitions{}             -> Range -> File
missingDefinitionHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
    -- TODO: explore highlighting opportunities here!
    InvalidCatchallPragma{}           -> File
forall a. Monoid a => a
mempty
    PolarityPragmasButNotPostulates{} -> File
forall a. Monoid a => a
mempty
    PragmaNoTerminationCheck{}        -> File
forall a. Monoid a => a
mempty
    PragmaCompiled{}                  -> File
forall a. Monoid a => a
mempty
    UnknownFixityInMixfixDecl{}       -> File
forall a. Monoid a => a
mempty
    UnknownNamesInFixityDecl{}        -> File
forall a. Monoid a => a
mempty
    UnknownNamesInPolarityPragmas{}   -> File
forall a. Monoid a => a
mempty


-- | Generate syntax highlighting for termination errors.

terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting [TerminationError]
termErrs = File
functionDefs File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
callSites
  where
    m :: Aspects
m            = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
TerminationProblem }
    functionDefs :: File
functionDefs = (QName -> File) -> [QName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\QName
x -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x) Aspects
m) ([QName] -> File) -> [QName] -> File
forall a b. (a -> b) -> a -> b
$
                   (TerminationError -> [QName]) -> [TerminationError] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
M.termErrFunctions [TerminationError]
termErrs
    callSites :: File
callSites    = (Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\Range
r -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
r) Aspects
m) ([Range] -> File) -> [Range] -> File
forall a b. (a -> b) -> a -> b
$
                   (TerminationError -> [Range]) -> [TerminationError] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CallInfo -> Range) -> [CallInfo] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> Range
M.callInfoRange ([CallInfo] -> [Range])
-> (TerminationError -> [CallInfo]) -> TerminationError -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TerminationError -> [CallInfo]
M.termErrCalls) [TerminationError]
termErrs

-- | Generate syntax highlighting for not-strictly-positive inductive
-- definitions.

positivityErrorHighlighting :: I.QName -> Seq OccursWhere -> File
positivityErrorHighlighting :: QName -> Seq OccursWhere -> File
positivityErrorHighlighting QName
q Seq OccursWhere
os =
  [Ranges] -> Aspects -> File
several (Range -> Ranges
rToR (Range -> Ranges) -> [Range] -> [Ranges]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Range
forall t. HasRange t => t -> Range
getRange QName
q Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rs) Aspects
m
  where
    rs :: [Range]
rs = (OccursWhere -> Range) -> [OccursWhere] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\(OccursWhere Range
r Seq Where
_ Seq Where
_) -> Range
r) (Seq OccursWhere -> [OccursWhere]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq OccursWhere
os)
    m :: Aspects
m  = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
PositivityProblem }

deadcodeHighlighting :: Range -> File
deadcodeHighlighting :: Range -> File
deadcodeHighlighting Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
Deadcode }

coverageErrorHighlighting :: Range -> File
coverageErrorHighlighting :: Range -> File
coverageErrorHighlighting Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
CoverageProblem }

shadowingTelHighlighting :: [Range] -> File
shadowingTelHighlighting :: [Range] -> File
shadowingTelHighlighting =
  -- we do not want to highlight the one variable in scope so we take
  -- the @init@ segment of the ranges in question
  (Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\Range
r -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous Range
r) Aspects
m) ([Range] -> File) -> ([Range] -> [Range]) -> [Range] -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range] -> [Range]
forall a. [a] -> [a]
init
  where
  m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects =
                      OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
P.ShadowingInTelescope }

catchallHighlighting :: Range -> File
catchallHighlighting :: Range -> File
catchallHighlighting Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
CatchallClause }

confluenceErrorHighlighting :: Range -> File
confluenceErrorHighlighting :: Range -> File
confluenceErrorHighlighting Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
ConfluenceProblem }

missingDefinitionHighlighting :: Range -> File
missingDefinitionHighlighting :: Range -> File
missingDefinitionHighlighting Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
  where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
MissingDefinition }

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

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

  RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting
    (File -> CompressedFile
compress (File -> CompressedFile) -> File -> CompressedFile
forall a b. (a -> b) -> a -> b
$ File
metaInfo File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
constraintInfo)

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

computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings :: TCMT IO File
computeUnsolvedMetaWarnings = do
  [MetaId]
is <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
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 :: MetaId -> TCMT IO Bool
notBlocked MetaId
m = Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
m
  [MetaId]
ms <- (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
notBlocked ([MetaId] -> TCMT IO [MetaId])
-> TCMT IO [MetaId] -> TCMT IO [MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas

  [Range]
rs <- (MetaId -> TCMT IO Range) -> [MetaId] -> TCMT IO [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange ([MetaId]
ms [MetaId] -> [MetaId] -> [MetaId]
forall a. Eq a => [a] -> [a] -> [a]
\\ [MetaId]
is)
  File -> TCMT IO File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCMT IO File) -> File -> TCMT IO File
forall a b. (a -> b) -> a -> b
$ [Range] -> File
metasHighlighting [Range]
rs

metasHighlighting :: [Range] -> File
metasHighlighting :: [Range] -> File
metasHighlighting [Range]
rs = [Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
                     (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
UnsolvedMeta }

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

computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints :: TCMT IO File
computeUnsolvedConstraints = Constraints -> File
constraintsHighlighting (Constraints -> File) -> TCMT IO Constraints -> TCMT IO File
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints

constraintsHighlighting :: Constraints -> File
constraintsHighlighting :: Constraints -> File
constraintsHighlighting Constraints
cs =
  [Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
          (Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
UnsolvedConstraint })
  where
  -- get ranges of interesting unsolved constraints
  rs :: [Range]
rs = ((Closure Constraint -> Maybe Range)
-> [Closure Constraint] -> [Range]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` ((ProblemConstraint -> Closure Constraint)
-> Constraints -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint Constraints
cs)) ((Closure Constraint -> Maybe Range) -> [Range])
-> (Closure Constraint -> Maybe Range) -> [Range]
forall a b. (a -> b) -> a -> b
$ \case
    Closure{ clValue :: forall a. Closure a -> a
clValue = IsEmpty Range
r Type
t           } -> Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ValueCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ElimCmp{}  } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = TelCmp{}   } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = SortCmp{}  } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = LevelCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = CheckSizeLtSat{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
    Closure Constraint
_ -> Maybe Range
forall a. Maybe a
Nothing

-- | 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 :: SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate SourceToModule
modMap AbsolutePath
file NameKinds
kinds (A.AmbQ NonEmpty QName
qs) =
  (QName -> File) -> NonEmpty QName -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\ QName
q -> SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file QName
q Bool
include Bool -> Aspects
m) NonEmpty QName
qs
  where
    ks :: [Maybe NameKind]
ks   = NameKinds -> [QName] -> [Maybe NameKind]
forall a b. (a -> b) -> [a] -> [b]
map NameKinds
kinds (NonEmpty QName -> [QName]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty QName
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 :: Maybe NameKind
kind = case [ NameKind
k | Just NameKind
k <- [Maybe NameKind]
ks ] of
             NameKind
k : [NameKind]
_ -> NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
k
             []    -> Maybe NameKind
forall a. Maybe a
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 :: Bool -> Aspects
m Bool
isOp  = Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name Maybe NameKind
kind Bool
isOp }
    include :: Bool
include = [Range] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((QName -> Range) -> [QName] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Range
bindingSite ([QName] -> [Range]) -> [QName] -> [Range]
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> [QName]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty QName
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.
           -> Range
              -- ^ The 'Range' of the name in its fixity declaration (if any).
           -> (Bool -> Aspects)
              -- ^ Meta information to be associated with the name.
              -- The argument is 'True' iff the name is an operator.
           -> Maybe Range
              -- ^ The definition site of the name. The calculated
              -- meta information is extended with this information,
              -- if possible.
           -> File
nameToFile :: SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file [Name]
xs Name
x Range
fr Bool -> Aspects
m Maybe Range
mR =
  -- We don't care if we get any funny ranges.
  if (SrcFile -> Bool) -> [SrcFile] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file) [SrcFile]
fileNames then
    File
frFile File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend`
    [Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Ranges
rToR [Range]
rs)
            (Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = Maybe DefinitionSite
mFilePos })
   else
    File
forall a. Monoid a => a
mempty
  where
  aspects :: Aspects
aspects    = Bool -> Aspects
m (Bool -> Aspects) -> Bool -> Aspects
forall a b. (a -> b) -> a -> b
$ Name -> Bool
C.isOperator Name
x
  fileNames :: [SrcFile]
fileNames  = (Name -> Maybe SrcFile) -> [Name] -> [SrcFile]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Position' SrcFile -> SrcFile)
-> Maybe (Position' SrcFile) -> Maybe SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Position' SrcFile -> SrcFile
forall a. Position' a -> a
P.srcFile (Maybe (Position' SrcFile) -> Maybe SrcFile)
-> (Name -> Maybe (Position' SrcFile)) -> Name -> Maybe SrcFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart (Range -> Maybe (Position' SrcFile))
-> (Name -> Range) -> Name -> Maybe (Position' SrcFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
forall t. HasRange t => t -> Range
getRange) (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
xs)
  frFile :: File
frFile     = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
fr) (Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = DefinitionSite -> DefinitionSite
notHere (DefinitionSite -> DefinitionSite)
-> Maybe DefinitionSite -> Maybe DefinitionSite
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DefinitionSite
mFilePos })
  rs :: [Range]
rs         = (Name -> Range) -> [Name] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
forall t. HasRange t => t -> Range
getRange (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
xs)

  -- The fixity declaration should not get a symbolic anchor.
  notHere :: DefinitionSite -> DefinitionSite
notHere DefinitionSite
d = DefinitionSite
d { defSiteHere :: Bool
defSiteHere = Bool
False }

  mFilePos  :: Maybe DefinitionSite
  mFilePos :: Maybe DefinitionSite
mFilePos   = do
    Range
r <- Maybe Range
mR
    P.Pn { srcFile :: forall a. Position' a -> a
P.srcFile = Strict.Just AbsolutePath
f, posPos :: forall a. Position' a -> Int32
P.posPos = Int32
p } <- Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r
    TopLevelModuleName
mod <- AbsolutePath -> SourceToModule -> Maybe TopLevelModuleName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AbsolutePath
f SourceToModule
modMap
    -- Andreas, 2017-06-16, Issue #2604: Symbolic anchors.
    -- We drop the file name part from the qualifiers, since
    -- this is contained in the html file name already.
    -- We want to get anchors of the form:
    -- @<a name="TopLevelModule.html#LocalModule.NestedModule.identifier">@
    let qualifiers :: [Name]
qualifiers = VerboseLevel -> [Name] -> [Name]
forall a. VerboseLevel -> [a] -> [a]
drop ([VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([VerboseKey] -> VerboseLevel) -> [VerboseKey] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [VerboseKey]
C.moduleNameParts TopLevelModuleName
mod) [Name]
xs
    -- For bound variables, we do not create symbolic anchors.
        local :: Bool
local = Bool -> (Aspect -> Bool) -> Maybe Aspect -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Aspect -> Bool
isLocalAspect (Maybe Aspect -> Bool) -> Maybe Aspect -> Bool
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect Aspects
aspects
    DefinitionSite -> Maybe DefinitionSite
forall (m :: * -> *) a. Monad m => a -> m a
return (DefinitionSite -> Maybe DefinitionSite)
-> DefinitionSite -> Maybe DefinitionSite
forall a b. (a -> b) -> a -> b
$ DefinitionSite :: TopLevelModuleName
-> VerboseLevel -> Bool -> Maybe VerboseKey -> DefinitionSite
DefinitionSite
      { defSiteModule :: TopLevelModuleName
defSiteModule = TopLevelModuleName
mod
      , defSitePos :: VerboseLevel
defSitePos    = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p
        -- Is our current position the definition site?
      , defSiteHere :: Bool
defSiteHere   = Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x
        -- For bound variables etc. we do not create a symbolic anchor name.
        -- Also not for names that include anonymous modules,
        -- otherwise, we do not get unique anchors.
      , defSiteAnchor :: Maybe VerboseKey
defSiteAnchor = if Bool
local Bool -> Bool -> Bool
|| Name -> Bool
forall a. IsNoName a => a -> Bool
C.isNoName Name
x Bool -> Bool -> Bool
|| (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Name -> Bool
forall a. Underscore a => a -> Bool
Common.isUnderscore [Name]
qualifiers
          then Maybe VerboseKey
forall a. Maybe a
Nothing
          else VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just (VerboseKey -> Maybe VerboseKey) -> VerboseKey -> Maybe VerboseKey
forall a b. (a -> b) -> a -> b
$ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (QName -> VerboseKey) -> QName -> VerboseKey
forall a b. (a -> b) -> a -> b
$ (Name -> QName -> QName) -> QName -> [Name] -> QName
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
C.Qual (Name -> QName
C.QName Name
x) [Name]
qualifiers
      }

  -- Is the name a bound variable or similar? If in doubt, yes.
  isLocalAspect :: Aspect -> Bool
  isLocalAspect :: Aspect -> Bool
isLocalAspect = \case
    Name Maybe NameKind
mkind Bool
_ -> Bool -> (NameKind -> Bool) -> Maybe NameKind -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True NameKind -> Bool
isLocal Maybe NameKind
mkind
    Aspect
_ -> Bool
True
  isLocal :: NameKind -> Bool
  isLocal :: NameKind -> Bool
isLocal = \case
    NameKind
Bound         -> Bool
True
    NameKind
Generalizable -> Bool
True
    NameKind
Argument      -> Bool
True
    Constructor{} -> Bool
False
    NameKind
Datatype      -> Bool
False
    NameKind
Field         -> Bool
False
    NameKind
Function      -> Bool
False
    NameKind
Module        -> Bool
False
    NameKind
Postulate     -> Bool
False
    NameKind
Primitive     -> Bool
False
    NameKind
Record        -> Bool
False
    NameKind
Macro         -> Bool
False

-- | 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 :: SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file QName
x Bool
include Bool -> Aspects
m =
  SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap
             AbsolutePath
file
             (QName -> [Name]
concreteQualifier QName
x)
             (QName -> Name
concreteBase QName
x)
             Range
rangeOfFixityDeclaration
             Bool -> Aspects
m
             (if Bool
include then Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x else Maybe Range
forall a. Maybe a
Nothing)
    File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
notationFile
  where
  -- TODO: Currently we highlight fixity and syntax declarations by
  -- producing highlighting something like once per occurrence of the
  -- related name(s) in the file of the declaration (and we explicitly
  -- avoid doing this for other files). Perhaps it would be better to
  -- only produce this highlighting once.

  rangeOfFixityDeclaration :: Range
rangeOfFixityDeclaration =
    if Range -> SrcFile
P.rangeFile Range
r SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file
    then Range
r else Range
forall a. Range' a
noRange
    where
    r :: Range
r = Fixity' -> Range
Common.theNameRange (Fixity' -> Range) -> Fixity' -> Range
forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity (Name -> Fixity') -> Name -> Fixity'
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x

  notationFile :: File
notationFile =
    if Range -> SrcFile
P.rangeFile (Notation -> Range
forall t. HasRange t => t -> Range
getRange Notation
notation) SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file
    then [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (GenPart -> File) -> Notation -> [File]
forall a b. (a -> b) -> [a] -> [b]
map GenPart -> File
genPartFile Notation
notation
    else File
forall a. Monoid a => a
mempty
    where
    notation :: Notation
notation = Fixity' -> Notation
Common.theNotation (Fixity' -> Notation) -> Fixity' -> Notation
forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity (Name -> Fixity') -> Name -> Fixity'
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x

    boundAspect :: Aspects
boundAspect = Aspects
parserBased{ aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Bound) Bool
False }

    genPartFile :: GenPart -> File
genPartFile (Common.BindHole Range
r Ranged VerboseLevel
i)   = [Ranges] -> Aspects -> File
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Ranged VerboseLevel -> Range
forall t. HasRange t => t -> Range
getRange Ranged VerboseLevel
i] Aspects
boundAspect
    genPartFile (Common.NormalHole Range
r NamedArg (Ranged VerboseLevel)
i) = [Ranges] -> Aspects -> File
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ NamedArg (Ranged VerboseLevel) -> Range
forall t. HasRange t => t -> Range
getRange NamedArg (Ranged VerboseLevel)
i] Aspects
boundAspect
    genPartFile Common.WildHole{}       = File
forall a. Monoid a => a
mempty
    genPartFile (Common.IdPart RString
x)       = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ RString -> Range
forall t. HasRange t => t -> Range
getRange RString
x) (Bool -> Aspects
m Bool
False)

concreteBase :: I.QName -> C.Name
concreteBase :: QName -> Name
concreteBase = Name -> Name
A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName

concreteQualifier :: I.QName -> [C.Name]
concreteQualifier :: QName -> [Name]
concreteQualifier = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
A.nameConcrete ([Name] -> [Name]) -> (QName -> [Name]) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
A.mnameToList (ModuleName -> [Name]) -> (QName -> ModuleName) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
A.qnameModule

bindingSite :: I.QName -> Range
bindingSite :: QName -> Range
bindingSite = Name -> Range
A.nameBindingSite (Name -> Range) -> (QName -> Name) -> QName -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName

-- | Remember a name disambiguation (during type checking).
--   To be used later during syntax highlighting.
storeDisambiguatedName :: A.QName -> TCM ()
storeDisambiguatedName :: QName -> TCM ()
storeDisambiguatedName QName
q = Maybe VerboseLevel -> (VerboseLevel -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Range -> Maybe VerboseLevel
forall b a. Num b => Range' a -> Maybe b
start (Range -> Maybe VerboseLevel) -> Range -> Maybe VerboseLevel
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall t. HasRange t => t -> Range
getRange QName
q) ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i ->
  Lens' DisambiguatedNames TCState
stDisambiguatedNames Lens' DisambiguatedNames TCState
-> (DisambiguatedNames -> DisambiguatedNames) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` VerboseLevel -> QName -> DisambiguatedNames -> DisambiguatedNames
forall a. VerboseLevel -> a -> IntMap a -> IntMap a
IntMap.insert VerboseLevel
i QName
q
  where
  start :: Range' a -> Maybe b
start Range' a
r = Int32 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> b) -> (Position' () -> Int32) -> Position' () -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> b) -> Maybe (Position' ()) -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range' a -> Maybe (Position' ())
forall a. Range' a -> Maybe (Position' ())
P.rStart' Range' a
r

-- | Store a disambiguation of record field tags for the purpose of highlighting.
disambiguateRecordFields
  :: [C.Name]   -- ^ Record field names in a record expression.
  -> [A.QName]  -- ^ Record field names in the corresponding record type definition
  -> TCM ()
disambiguateRecordFields :: [Name] -> [QName] -> TCM ()
disambiguateRecordFields [Name]
cxs [QName]
axs = [Name] -> (Name -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Name]
cxs ((Name -> TCM ()) -> TCM ()) -> (Name -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Name
cx -> do
  Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((QName -> Bool) -> [QName] -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
cx Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool) -> (QName -> Name) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName) [QName]
axs) (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
ax -> do
    QName -> TCM ()
storeDisambiguatedName QName
ax { qnameName :: Name
A.qnameName = (QName -> Name
A.qnameName QName
ax) { nameConcrete :: Name
A.nameConcrete = Name
cx } }