-- | Extract highlighting syntax from abstract syntax.
--
-- Implements one big fold over abstract syntax.

-- {-# OPTIONS_GHC -fwarn-unused-imports #-}  -- Data.Semigroup is redundant in later GHC versions
{-# OPTIONS_GHC -fwarn-unused-binds   #-}

module Agda.Interaction.Highlighting.FromAbstract
  ( runHighlighter
  , NameKinds
  ) where

import Prelude hiding (null)

import Control.Applicative
import Control.Monad         ( (<=<) )
import Control.Monad.Reader  ( MonadReader(..), asks, Reader, runReader )

import qualified Data.Map      as Map
import           Data.Maybe
import           Data.Semigroup       ( Semigroup(..) )          -- for ghc 8.0
import           Data.Void            ( Void )

import           Agda.Interaction.Highlighting.Precise hiding ( singleton )
import qualified Agda.Interaction.Highlighting.Precise as H
import           Agda.Interaction.Highlighting.Range   ( rToR )  -- Range is ambiguous

import           Agda.Syntax.Abstract                ( IsProjP(..) )
import qualified Agda.Syntax.Abstract      as A
import           Agda.Syntax.Common        as Common
import           Agda.Syntax.Concrete                ( FieldAssignment'(..) )
import qualified Agda.Syntax.Concrete.Name as C
import           Agda.Syntax.Info                    ( ModuleInfo(..) )
import           Agda.Syntax.Literal
import qualified Agda.Syntax.Position      as P
import           Agda.Syntax.Position                ( Range, HasRange, getRange, noRange )
import           Agda.Syntax.Scope.Base              ( AbstractName(..), ResolvedName(..), exactConName )
import           Agda.Syntax.TopLevelModuleName

import Agda.TypeChecking.Monad
  hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)

import           Agda.Utils.FileName
import           Agda.Utils.Function
import           Agda.Utils.Functor
import           Agda.Utils.List                     ( initLast1 )
import           Agda.Utils.List1                    ( List1 )
import qualified Agda.Utils.List1          as List1
import           Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict   as Strict
import           Agda.Utils.Pretty
import           Agda.Utils.Singleton
import           Agda.Utils.Size

-- Entry point:
-- | Create highlighting info for some piece of syntax.
runHighlighter
  :: Hilite a
  => TopLevelModuleName
     -- ^ The current top-level module's name.
  -> NameKinds -> a -> HighlightingInfoBuilder
runHighlighter :: forall a.
Hilite a =>
TopLevelModuleName -> NameKinds -> a -> HighlightingInfoBuilder
runHighlighter TopLevelModuleName
top NameKinds
kinds a
x =
  forall r a. Reader r a -> r -> a
runReader (forall a. Hilite a => a -> Hiliter
hilite a
x) forall a b. (a -> b) -> a -> b
$
  HiliteEnv
    { hleNameKinds :: NameKinds
hleNameKinds         = NameKinds
kinds
    , hleCurrentModuleName :: TopLevelModuleName
hleCurrentModuleName = TopLevelModuleName
top
    }

-- | Environment of the highlighter.
data HiliteEnv = HiliteEnv
  { HiliteEnv -> NameKinds
hleNameKinds :: NameKinds
      -- ^ Function mapping qualified names to their kind.
  , HiliteEnv -> TopLevelModuleName
hleCurrentModuleName :: TopLevelModuleName
      -- ^ The current top-level module's name. Used for consistency
      -- checking.
  }

-- | A function mapping names to the kind of name they stand for.
type NameKinds = A.QName -> Maybe NameKind

-- | Highlighting monad.
type HiliteM = Reader HiliteEnv

-- | Highlighter.

type Hiliter = HiliteM HighlightingInfoBuilder

instance Monoid Hiliter where
  mempty :: Hiliter
mempty  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  mappend :: Hiliter -> Hiliter -> Hiliter
mappend = forall a. Semigroup a => a -> a -> a
(<>)

-- | Traversal to extract highlighting information.

class Hilite a where
  hilite :: a -> Hiliter

  default hilite :: (Foldable t, Hilite b, t b ~ a) => a -> Hiliter
  hilite = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. Hilite a => a -> Hiliter
hilite

-- * Generic instances
---------------------------------------------------------------------------

instance Hilite a => Hilite [a]
instance Hilite a => Hilite (List1 a)
instance Hilite a => Hilite (Maybe a)
instance Hilite a => Hilite (WithHiding a)

instance Hilite Void where
  hilite :: Void -> Hiliter
hilite Void
_ = forall a. Monoid a => a
mempty

instance (Hilite a, Hilite b) => Hilite (Either a b) where
  hilite :: Either a b -> Hiliter
hilite = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Hilite a => a -> Hiliter
hilite forall a. Hilite a => a -> Hiliter
hilite

instance (Hilite a, Hilite b) => Hilite (a, b) where
  hilite :: (a, b) -> Hiliter
hilite (a
a, b
b) = forall a. Hilite a => a -> Hiliter
hilite a
a forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite b
b

-- * Major syntactic categories
---------------------------------------------------------------------------

-- | Reengineered from the old Geniplate-implemented highlighting extraction.
-- This was the old procedure:
--
-- Traversal over declaration in abstract syntax that collects the
-- following hiliting information:
--
-- [1. @constructorInfo@ (highest prio)]
-- 2. @theRest@ (medium prio)
-- 3. @nameInfo@ (lowest prio)
--
-- @nameInfo@:
--   "All names mentioned in the syntax tree (not bound variables)."
-- For each possibly ambiguous name (QName and AmbiguousQName)
-- that not isExtendedLambdaName,
-- do @hiliteAmbiguous@ (used to be called@generate@).
--
-- @constructorInfo@ (only when highlighting level == Full):
--   "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."
-- This is not computed by recursion over the abstract syntax,
-- but gets the constructor names stDisambiguatedNames
-- that fall within the bounds of the current declaration.
--
-- @theRest@:
--   Bound variables, dotted patterns, record fields, module names,
--   the "as" and "to" symbols and some other things.
--
-- Here is a table what @theRest@ used to collect:
--
-- ---------------------------------------------------------------------
-- | A.Expr
-- ---------------------------------------------------------------------
-- | getVarAndField (Expr) | A.Var                       | bound
-- | getVarAndField        | A.Rec(Update)               | field
-- | getExpr        (Expr) | A.PatternSyn                | patsyn
-- | getExpr               | A.Macro                     | macro
-- ---------------------------------------------------------------------
-- | A.LetBinding
-- ---------------------------------------------------------------------
-- | getLet                | A.LetBind                   | bound
-- | getLet                | A.LetDeclaredVariable       | bound
-- ---------------------------------------------------------------------
-- | A.LamBinding
-- ---------------------------------------------------------------------
-- | getLam                | A.Binder under A.DomainFree | bound
-- | getTyped              | A.Binder under A.TBind      | bound
-- ---------------------------------------------------------------------
-- | A.Pattern'
-- ---------------------------------------------------------------------
-- | getPattern(Syn)       | A.VarP                      | bound
-- | getPattern(Syn)       | A.AsP                       | bound
-- | getPattern(Syn)       | A.DotP (not isProjP)        | DottedPattern
-- | getPattern(Syn)       | A.RecP                      | field
-- | getPattern(Syn)       | A.PatternSynP               | patsyn
-- ---------------------------------------------------------------------
-- | A.Declaration
-- ---------------------------------------------------------------------
-- | getFieldDecl          | A.Field under A.RecDef      | field
-- | getPatSynArgs         | A.PatternSynDef             | bound
-- | getPragma             | A.BuiltinPragma...          | keyword
-- ---------------------------------------------------------------------
-- | A.NamedArg (polymorphism not supported in geniplate)
-- ---------------------------------------------------------------------
-- | getNamedArg           | NamedArg a                  | nameOf
-- | getNamedArgE          | NamedArg Exp                | nameOf
-- | getNamedArgP          | NamedArg Pattern            | nameOf
-- | getNamedArgB          | NamedArg BindName           | nameOf
-- | getNamedArgL          | NamedArg LHSCore            | nameOf
--
-- | getModuleName         | A.MName                     | mod
-- | getModuleInfo         | ModuleInfo                  | asName, (range of as,to)
-- | getQuantityAttr       | Common.Quantity             | Symbol (if range)

instance Hilite A.RecordDirectives where
  hilite :: RecordDirectives -> Hiliter
hilite (RecordDirectives Maybe (Ranged Induction)
_ Maybe HasEta0
_ Maybe Range
_ Maybe QName
c) = forall a. Hilite a => a -> Hiliter
hilite Maybe QName
c

instance Hilite A.Declaration where
  hilite :: Declaration -> Hiliter
hilite = \case
      A.Axiom KindOfName
_ax DefInfo
_di ArgInfo
ai Maybe [Occurrence]
_occ QName
x Type
e            -> forall a. Hilite a => a -> Hiliter
hl ArgInfo
ai forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.Generalize Set QName
_names DefInfo
_di ArgInfo
ai QName
x Type
e         -> forall a. Hilite a => a -> Hiliter
hl ArgInfo
ai forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.Field DefInfo
_di QName
x Arg Type
e                        -> QName -> Hiliter
hlField QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Arg Type
e
      A.Primitive DefInfo
_di QName
x Arg Type
e                    -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Arg Type
e
      A.Mutual MutualInfo
_mi [Declaration]
ds                        -> forall a. Hilite a => a -> Hiliter
hl [Declaration]
ds
      A.Section Range
_r ModuleName
x GeneralizeTelescope
tel [Declaration]
ds                  -> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl GeneralizeTelescope
tel forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Declaration]
ds
      A.Apply ModuleInfo
mi ModuleName
x ModuleApplication
a ScopeCopyInfo
_ci ImportDirective
dir                 -> forall a. Hilite a => a -> Hiliter
hl ModuleInfo
mi forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleApplication
a forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ImportDirective
dir
      A.Import ModuleInfo
mi ModuleName
x ImportDirective
dir                      -> forall a. Hilite a => a -> Hiliter
hl ModuleInfo
mi forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ImportDirective
dir
      A.Open ModuleInfo
mi ModuleName
x ImportDirective
dir                        -> forall a. Hilite a => a -> Hiliter
hl ModuleInfo
mi forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ImportDirective
dir
      A.FunDef DefInfo
_di QName
x Delayed
_delayed [Clause]
cs             -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Clause]
cs
      A.DataSig DefInfo
_di QName
x GeneralizeTelescope
tel Type
e                  -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl GeneralizeTelescope
tel forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.DataDef DefInfo
_di QName
x UniverseCheck
_uc DataDefParams
pars [Declaration]
cs            -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl DataDefParams
pars forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Declaration]
cs
      A.RecSig DefInfo
_di QName
x GeneralizeTelescope
tel Type
e                   -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl GeneralizeTelescope
tel forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.RecDef DefInfo
_di QName
x UniverseCheck
_uc RecordDirectives
dir DataDefParams
bs Type
e [Declaration]
ds         -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl RecordDirectives
dir forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl DataDefParams
bs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Declaration]
ds
      A.PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p                 -> forall a. Hilite a => a -> Hiliter
hl QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Arg BindName]
xs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Pattern' Void
p
      A.UnquoteDecl MutualInfo
_mi [DefInfo]
_di [QName]
xs Type
e             -> forall a. Hilite a => a -> Hiliter
hl [QName]
xs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.UnquoteDef [DefInfo]
_di [QName]
xs Type
e                  -> forall a. Hilite a => a -> Hiliter
hl [QName]
xs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.UnquoteData [DefInfo]
_i QName
xs UniverseCheck
_uc [DefInfo]
_j [QName]
cs Type
e        -> forall a. Hilite a => a -> Hiliter
hl QName
xs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [QName]
cs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.ScopedDecl ScopeInfo
s [Declaration]
ds                      -> forall a. Hilite a => a -> Hiliter
hl [Declaration]
ds
      A.Pragma Range
_r Pragma
pragma                     -> forall a. Hilite a => a -> Hiliter
hl Pragma
pragma
    where
    hl :: a -> Hiliter
hl      a
a = forall a. Hilite a => a -> Hiliter
hilite a
a
    hlField :: QName -> Hiliter
hlField QName
x = [Name] -> Name -> Maybe Range -> Hiliter
hiliteField (QName -> [Name]
concreteQualifier QName
x) (QName -> Name
concreteBase QName
x) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x)

instance Hilite A.Pragma where
  hilite :: Pragma -> Hiliter
hilite = \case
    A.OptionsPragma [String]
_strings     -> forall a. Monoid a => a
mempty
    A.BuiltinPragma RString
b ResolvedName
x          -> forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Keyword RString
b forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite ResolvedName
x
    A.BuiltinNoDefPragma RString
b KindOfName
k QName
x   -> forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Keyword RString
b forall a. Semigroup a => a -> a -> a
<> Maybe NameKind -> QName -> Hiliter
hiliteQName (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ KindOfName -> NameKind
kindOfNameToNameKind KindOfName
k) QName
x
    A.CompilePragma RString
b QName
x String
_foreign -> forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Keyword RString
b forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.RewritePragma Range
r [QName]
xs         -> forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Keyword Range
r forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [QName]
xs
    A.StaticPragma QName
x             -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.EtaPragma QName
x                -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.InjectivePragma QName
x          -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.NotProjectionLikePragma QName
x  -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.InlinePragma Bool
_inline QName
x     -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    A.DisplayPragma QName
x [NamedArg Pattern]
ps Type
e       -> forall a. Hilite a => a -> Hiliter
hilite QName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [NamedArg Pattern]
ps forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite Type
e

instance Hilite A.Expr where
  hilite :: Type -> Hiliter
hilite = \case
      A.Var Name
x                       -> forall a. Hilite a => a -> Hiliter
hl forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.BindName Name
x        -- bound variable like binder
      A.Def' QName
q Suffix
_                    -> Maybe NameKind -> QName -> Hiliter
hiliteQName forall a. Maybe a
Nothing QName
q
      A.Proj ProjOrigin
_o AmbiguousQName
qs                  -> Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName forall a. Maybe a
Nothing AmbiguousQName
qs  -- Issue #4604: not: hiliteProjection qs
                                         -- Names from @open R r@ should not be highlighted as projections
      A.Con AmbiguousQName
qs                      -> Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName forall a. Maybe a
Nothing AmbiguousQName
qs  -- TODO? Con aspect
      A.PatternSyn AmbiguousQName
qs               -> AmbiguousQName -> Hiliter
hilitePatternSynonym AmbiguousQName
qs
      A.Macro QName
q                     -> Maybe NameKind -> QName -> Hiliter
hiliteQName (forall a. a -> Maybe a
Just NameKind
Macro) QName
q
      A.Lit ExprInfo
_r Literal
l                    -> forall a. Hilite a => a -> Hiliter
hl Literal
l
      A.QuestionMark MetaInfo
_mi InteractionId
_ii        -> forall a. Monoid a => a
mempty
      A.Underscore MetaInfo
_mi              -> forall a. Monoid a => a
mempty
      A.Dot ExprInfo
_r Type
e                    -> forall a. Hilite a => a -> Hiliter
hl Type
e                   -- TODO? Projection?
      A.App AppInfo
_r Type
e NamedArg Type
es                 -> forall a. Hilite a => a -> Hiliter
hl Type
e forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl NamedArg Type
es
      A.WithApp ExprInfo
_r Type
e [Type]
es             -> forall a. Hilite a => a -> Hiliter
hl Type
e forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Type]
es
      A.Lam ExprInfo
_r LamBinding
bs Type
e                 -> forall a. Hilite a => a -> Hiliter
hl LamBinding
bs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.AbsurdLam ExprInfo
_r Hiding
_h             -> forall a. Monoid a => a
mempty
      A.ExtendedLam ExprInfo
_r DefInfo
_di Erased
er QName
_q List1 Clause
cs -> forall a. Hilite a => a -> Hiliter
hl Erased
er forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl List1 Clause
cs -- No hilighting of generated extended lambda name!
      A.Pi ExprInfo
_r Telescope1
tel Type
b                 -> forall a. Hilite a => a -> Hiliter
hl Telescope1
tel forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
b
      A.Generalized Set QName
_qs Type
e           -> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.Fun ExprInfo
_r Arg Type
a Type
b                  -> forall a. Hilite a => a -> Hiliter
hl Arg Type
a forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
b
      A.Let ExprInfo
_r List1 LetBinding
bs Type
e                 -> forall a. Hilite a => a -> Hiliter
hl List1 LetBinding
bs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.Rec ExprInfo
_r RecordAssigns
ass                  -> forall a. Hilite a => a -> Hiliter
hl RecordAssigns
ass
      A.RecUpdate ExprInfo
_r Type
e Assigns
ass          -> forall a. Hilite a => a -> Hiliter
hl Type
e forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Assigns
ass
      A.ScopedExpr ScopeInfo
_ Type
e              -> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.Quote ExprInfo
_r                    -> forall a. Monoid a => a
mempty
      A.QuoteTerm ExprInfo
_r                -> forall a. Monoid a => a
mempty
      A.Unquote ExprInfo
_r                  -> forall a. Monoid a => a
mempty
      A.DontCare Type
e                  -> forall a. Hilite a => a -> Hiliter
hl Type
e
    where
    hl :: a -> Hiliter
hl a
a = forall a. Hilite a => a -> Hiliter
hilite a
a

instance (Hilite a, IsProjP a) => Hilite (A.Pattern' a) where
  hilite :: Pattern' a -> Hiliter
hilite = \case
      A.VarP BindName
x               -> forall a. Hilite a => a -> Hiliter
hl BindName
x
      A.ConP ConPatInfo
_i AmbiguousQName
qs NAPs a
es        -> AmbiguousQName -> Hiliter
hiliteInductiveConstructor AmbiguousQName
qs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl NAPs a
es
        -- No matching on coinductive constructors, thus, can determine NameKind here.
      A.ProjP PatInfo
_r ProjOrigin
_o AmbiguousQName
qs       -> AmbiguousQName -> Hiliter
hiliteProjection AmbiguousQName
qs
      A.DefP PatInfo
_r AmbiguousQName
qs NAPs a
es        -> forall a. Hilite a => a -> Hiliter
hl AmbiguousQName
qs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl NAPs a
es
      A.WildP PatInfo
_r             -> forall a. Monoid a => a
mempty
      A.AsP PatInfo
_r BindName
x Pattern' a
p           -> forall a. Hilite a => a -> Hiliter
hl BindName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Pattern' a
p
      A.DotP PatInfo
r a
e             -> case forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP a
e of
                                  Maybe (ProjOrigin, AmbiguousQName)
Nothing       -> forall a. HasRange a => OtherAspect -> a -> Hiliter
singleOtherAspect OtherAspect
DottedPattern PatInfo
r forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl a
e
                                  Just (ProjOrigin
_o, AmbiguousQName
qs) -> AmbiguousQName -> Hiliter
hiliteProjection AmbiguousQName
qs
      A.AbsurdP PatInfo
_r           -> forall a. Monoid a => a
mempty
      A.LitP PatInfo
_r Literal
l            -> forall a. Hilite a => a -> Hiliter
hl Literal
l
      A.PatternSynP PatInfo
_r AmbiguousQName
qs NAPs a
es -> AmbiguousQName -> Hiliter
hilitePatternSynonym AmbiguousQName
qs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl NAPs a
es
      A.RecP PatInfo
_r [FieldAssignment' (Pattern' a)]
ps           -> forall a. Hilite a => a -> Hiliter
hl [FieldAssignment' (Pattern' a)]
ps
      A.EqualP PatInfo
_r [(a, a)]
ps         -> forall a. Hilite a => a -> Hiliter
hl [(a, a)]
ps
      A.WithP PatInfo
_ Pattern' a
p            -> forall a. Hilite a => a -> Hiliter
hl Pattern' a
p
      A.AnnP PatInfo
_r a
a Pattern' a
p          -> forall a. Hilite a => a -> Hiliter
hl Pattern' a
p

    where
    hl :: a -> Hiliter
hl a
a = forall a. Hilite a => a -> Hiliter
hilite a
a

instance Hilite Literal where
  hilite :: Literal -> Hiliter
hilite = \case
    LitNat{}                 -> forall a. Monoid a => a
mempty
    LitWord64{}              -> forall a. Monoid a => a
mempty
    LitFloat{}               -> forall a. Monoid a => a
mempty
    LitString{}              -> forall a. Monoid a => a
mempty
    LitChar{}                -> forall a. Monoid a => a
mempty
    LitQName QName
x               -> forall a. Hilite a => a -> Hiliter
hilite QName
x
    LitMeta TopLevelModuleName
_fileName MetaId
_id    -> forall a. Monoid a => a
mempty

-- * Minor syntactic categories
---------------------------------------------------------------------------

instance Hilite A.LHS where
  hilite :: LHS -> Hiliter
hilite (A.LHS LHSInfo
_r LHSCore
lhs) = forall a. Hilite a => a -> Hiliter
hilite LHSCore
lhs

instance (Hilite a, IsProjP a) => Hilite (A.LHSCore' a) where
  hilite :: LHSCore' a -> Hiliter
hilite = \case
    A.LHSHead QName
q [NamedArg (Pattern' a)]
ps       -> forall a. Hilite a => a -> Hiliter
hilite QName
q   forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [NamedArg (Pattern' a)]
ps
    A.LHSProj AmbiguousQName
q NamedArg (LHSCore' a)
lhs [NamedArg (Pattern' a)]
ps   -> forall a. Hilite a => a -> Hiliter
hilite NamedArg (LHSCore' a)
lhs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite AmbiguousQName
q   forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [NamedArg (Pattern' a)]
ps -- TODO? Projection?
    A.LHSWith LHSCore' a
lhs [Arg (Pattern' a)]
wps [NamedArg (Pattern' a)]
ps -> forall a. Hilite a => a -> Hiliter
hilite LHSCore' a
lhs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [Arg (Pattern' a)]
wps forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [NamedArg (Pattern' a)]
ps

instance Hilite A.RHS where
  hilite :: RHS -> Hiliter
hilite = \case
      A.RHS Type
e Maybe Expr
_ce                          -> forall a. Hilite a => a -> Hiliter
hl Type
e
      RHS
A.AbsurdRHS                          -> forall a. Monoid a => a
mempty
      A.WithRHS QName
_q [WithExpr]
es [Clause]
cs                   -> forall a. Hilite a => a -> Hiliter
hl [WithExpr]
es  forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [Clause]
cs  -- No highlighting for with-function-name!
      A.RewriteRHS [RewriteEqn]
eqs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh -> forall a. Hilite a => a -> Hiliter
hl [RewriteEqn]
eqs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl [ProblemEq]
strippedPats forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl RHS
rhs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl WhereDeclarations
wh
    where
    hl :: a -> Hiliter
hl a
a = forall a. Hilite a => a -> Hiliter
hilite a
a

instance (HasRange n, Hilite p, Hilite e) => Hilite (RewriteEqn' x n p e) where
  hilite :: RewriteEqn' x n p e -> Hiliter
hilite = \case
    Rewrite List1 (x, e)
es    -> forall a. Hilite a => a -> Hiliter
hilite forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd List1 (x, e)
es
    Invert x
_x List1 (Named n (p, e))
pes -> forall a. Hilite a => a -> Hiliter
hilite List1 (Named n (p, e))
pes

instance Hilite a => Hilite (A.Clause' a) where
  hilite :: Clause' a -> Hiliter
hilite (A.Clause a
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
_catchall) =
    forall a. Hilite a => a -> Hiliter
hilite a
lhs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [ProblemEq]
strippedPats forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite RHS
rhs forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite WhereDeclarations
wh

instance Hilite A.ProblemEq where
  hilite :: ProblemEq -> Hiliter
hilite (A.ProblemEq Pattern
p Term
_t Dom Type
_dom) = forall a. Hilite a => a -> Hiliter
hilite Pattern
p

instance Hilite A.WhereDeclarations where
  hilite :: WhereDeclarations -> Hiliter
hilite (A.WhereDecls Maybe ModuleName
m Bool
_ Maybe Declaration
ds) = forall a. Hilite a => a -> Hiliter
hilite Maybe ModuleName
m forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite Maybe Declaration
ds

instance Hilite A.GeneralizeTelescope where
  hilite :: GeneralizeTelescope -> Hiliter
hilite (A.GeneralizeTel Map QName Name
_gen Telescope
tel) = forall a. Hilite a => a -> Hiliter
hilite Telescope
tel

instance Hilite A.DataDefParams where
  hilite :: DataDefParams -> Hiliter
hilite (A.DataDefParams Set Name
_gen [LamBinding]
pars) = forall a. Hilite a => a -> Hiliter
hilite [LamBinding]
pars

instance Hilite A.ModuleApplication where
  hilite :: ModuleApplication -> Hiliter
hilite = \case
    A.SectionApp Telescope
tel ModuleName
x [NamedArg Type]
es    -> forall a. Hilite a => a -> Hiliter
hilite Telescope
tel forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite [NamedArg Type]
es
    A.RecordModuleInstance ModuleName
x -> forall a. Hilite a => a -> Hiliter
hilite ModuleName
x

instance Hilite A.LetBinding where
  hilite :: LetBinding -> Hiliter
hilite = \case
      A.LetBind    LetInfo
_r ArgInfo
ai BindName
x Type
t Type
e     -> forall a. Hilite a => a -> Hiliter
hl ArgInfo
ai forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl BindName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
t forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.LetPatBind LetInfo
_r Pattern
p Type
e          -> forall a. Hilite a => a -> Hiliter
hl Pattern
p  forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl Type
e
      A.LetApply   ModuleInfo
mi ModuleName
x ModuleApplication
es ScopeCopyInfo
_ci ImportDirective
dir -> forall a. Hilite a => a -> Hiliter
hl ModuleInfo
mi forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleApplication
es forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ImportDirective
dir
      A.LetOpen    ModuleInfo
mi ModuleName
x ImportDirective
dir        -> forall a. Hilite a => a -> Hiliter
hl ModuleInfo
mi forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ModuleName
x forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hl ImportDirective
dir
      A.LetDeclaredVariable BindName
x      -> forall a. Hilite a => a -> Hiliter
hl BindName
x
    where
    hl :: a -> Hiliter
hl a
x = forall a. Hilite a => a -> Hiliter
hilite a
x

instance Hilite A.TypedBindingInfo where
  hilite :: TypedBindingInfo -> Hiliter
hilite (A.TypedBindingInfo TacticAttr
x Bool
_) = forall a. Hilite a => a -> Hiliter
hilite TacticAttr
x

instance Hilite A.TypedBinding where
  hilite :: TypedBinding -> Hiliter
hilite = \case
    A.TBind Range
_r TypedBindingInfo
tac List1 (NamedArg Binder)
binds Type
e -> forall a. Hilite a => a -> Hiliter
hilite TypedBindingInfo
tac forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite List1 (NamedArg Binder)
binds forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite Type
e
    A.TLet Range
_r List1 LetBinding
binds        -> forall a. Hilite a => a -> Hiliter
hilite List1 LetBinding
binds

instance Hilite A.LamBinding where
  hilite :: LamBinding -> Hiliter
hilite = \case
    A.DomainFree TacticAttr
tac NamedArg Binder
binds -> forall a. Hilite a => a -> Hiliter
hilite TacticAttr
tac forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite NamedArg Binder
binds
    A.DomainFull TypedBinding
bind      -> forall a. Hilite a => a -> Hiliter
hilite TypedBinding
bind

instance Hilite a => Hilite (A.Binder' a) where
  hilite :: Binder' a -> Hiliter
hilite (A.Binder Maybe Pattern
p a
x) = forall a. Hilite a => a -> Hiliter
hilite Maybe Pattern
p forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite a
x

instance Hilite A.BindName where
  hilite :: BindName -> Hiliter
hilite (A.BindName Name
x) = Name -> Hiliter
hiliteBound Name
x

instance Hilite a => Hilite (FieldAssignment' a) where
  hilite :: FieldAssignment' a -> Hiliter
hilite (FieldAssignment Name
x a
e) = [Name] -> Name -> Maybe Range -> Hiliter
hiliteField [] Name
x forall a. Maybe a
Nothing forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite a
e

instance (Hilite a, HasRange n) => Hilite (Named n a) where
  hilite :: Named n a -> Hiliter
hilite (Named Maybe n
mn a
e)
    =  forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (forall a. a -> Maybe a
Just NameKind
Argument) Bool
False) Maybe n
mn
    forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite a
e

instance Hilite a => Hilite (Arg a) where
  hilite :: Arg a -> Hiliter
hilite (Arg ArgInfo
ai a
e) = forall a. Hilite a => a -> Hiliter
hilite ArgInfo
ai forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite a
e

instance Hilite ArgInfo where
  hilite :: ArgInfo -> Hiliter
hilite (ArgInfo Hiding
_hiding Modality
modality Origin
_origin FreeVariables
_fv Annotation
_a) = forall a. Hilite a => a -> Hiliter
hilite Modality
modality

instance Hilite Modality where
  hilite :: Modality -> Hiliter
hilite (Modality Relevance
_relevance Quantity
quantity Cohesion
_cohesion) = forall a. Hilite a => a -> Hiliter
hilite Quantity
quantity

-- | If the 'Quantity' attribute comes with a 'Range', highlight the
-- corresponding attribute as 'Symbol'.
instance Hilite Quantity where
  hilite :: Quantity -> Hiliter
hilite = forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Symbol

-- | Erasure attributes are highlighted as symbols.
instance Hilite Erased where
  hilite :: Erased -> Hiliter
hilite = forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Symbol

instance Hilite ModuleInfo where
  hilite :: ModuleInfo -> Hiliter
hilite (ModuleInfo Range
_r Range
rAsTo Maybe Name
asName Maybe OpenShortHand
_open Maybe ImportDirective
_impDir)
    =  forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Symbol Range
rAsTo            -- TODO: 'to' already covered by A.ImportDirective
    forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty Name -> Hiliter
hiliteAsName Maybe Name
asName
    -- <> hilite impDir                     -- Should be covered by A.ImportDirective
    where
    hiliteAsName :: C.Name -> Hiliter
    hiliteAsName :: Name -> Hiliter
hiliteAsName Name
n = [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName [] Name
n forall a. Range' a
noRange forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ NameKind -> Bool -> Aspects
nameAsp NameKind
Module

instance (Hilite m, Hilite n, Hilite (RenamingTo m), Hilite (RenamingTo n))
       => Hilite (ImportDirective' m n) where
  hilite :: ImportDirective' m n -> Hiliter
hilite (ImportDirective Range
_r Using' m n
using HidingDirective' m n
hiding RenamingDirective' m n
renaming Maybe Range
_ropen) =
    forall a. Hilite a => a -> Hiliter
hilite Using' m n
using forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite HidingDirective' m n
hiding forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite RenamingDirective' m n
renaming

instance (Hilite m, Hilite n) => Hilite (Using' m n) where
  hilite :: Using' m n -> Hiliter
hilite = \case
    Using' m n
UseEverything -> forall a. Monoid a => a
mempty
    Using [ImportedName' m n]
using   -> forall a. Hilite a => a -> Hiliter
hilite [ImportedName' m n]
using

instance (Hilite m, Hilite n, Hilite (RenamingTo m), Hilite (RenamingTo n))
       => Hilite (Renaming' m n) where
  hilite :: Renaming' m n -> Hiliter
hilite (Renaming ImportedName' m n
from ImportedName' m n
to Maybe Fixity
_fixity Range
rangeKwTo)
    =  forall a. Hilite a => a -> Hiliter
hilite ImportedName' m n
from
    forall a. Semigroup a => a -> a -> a
<> forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
Symbol Range
rangeKwTo
         -- Currently, the "to" is already highlited by rAsTo above.
         -- TODO: remove the "to" ranges from rAsTo.
    forall a. Semigroup a => a -> a -> a
<> forall a. Hilite a => a -> Hiliter
hilite (forall a. a -> RenamingTo a
RenamingTo ImportedName' m n
to)

instance (Hilite m, Hilite n) => Hilite (ImportedName' m n) where
  hilite :: ImportedName' m n -> Hiliter
hilite = \case
    ImportedModule n
m -> forall a. Hilite a => a -> Hiliter
hilite n
m
    ImportedName   m
n -> forall a. Hilite a => a -> Hiliter
hilite m
n

-- * Highlighting of names
---------------------------------------------------------------------------

instance Hilite DisambiguatedName where
  hilite :: DisambiguatedName -> Hiliter
hilite (DisambiguatedName NameKind
k QName
x) = Maybe NameKind -> QName -> Hiliter
hiliteQName (forall a. a -> Maybe a
Just NameKind
k) QName
x

instance Hilite ResolvedName where
  hilite :: ResolvedName -> Hiliter
hilite = \case
    VarName           Name
x BindingSource
_bindSrc -> Name -> Hiliter
hiliteBound Name
x
    DefinedName  Access
_acc AbstractName
x Suffix
_suffix  -> forall a. Hilite a => a -> Hiliter
hilite forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
x
    FieldName         List1 AbstractName
xs         -> AmbiguousQName -> Hiliter
hiliteProjection forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
A.AmbQ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName List1 AbstractName
xs
    ConstructorName Set Induction
i List1 AbstractName
xs         -> Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName Maybe NameKind
k forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
A.AmbQ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName List1 AbstractName
xs
      where k :: Maybe NameKind
k = KindOfName -> NameKind
kindOfNameToNameKind forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *). Foldable t => t Induction -> Maybe KindOfName
exactConName Set Induction
i
    PatternSynResName List1 AbstractName
xs         -> AmbiguousQName -> Hiliter
hilitePatternSynonym forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
A.AmbQ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName List1 AbstractName
xs
    ResolvedName
UnknownName                  -> forall a. Monoid a => a
mempty

instance Hilite A.QName where
  hilite :: QName -> Hiliter
hilite = Maybe NameKind -> QName -> Hiliter
hiliteQName forall a. Maybe a
Nothing

instance Hilite A.AmbiguousQName where
  hilite :: AmbiguousQName -> Hiliter
hilite = Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName forall a. Maybe a
Nothing

instance Hilite A.ModuleName where
  hilite :: ModuleName -> Hiliter
hilite m :: ModuleName
m@(A.MName [Name]
xs) = (Bool, ModuleName) -> Hiliter
hiliteModule (Bool
isTopLevelModule, ModuleName
m)
    where
    isTopLevelModule :: Bool
isTopLevelModule =
      case forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Range -> Maybe TopLevelModuleName
P.rangeModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
A.nameBindingSite) [Name]
xs of
        []      -> Bool
False
        TopLevelModuleName
top : [TopLevelModuleName]
_ ->
          TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName TopLevelModuleName
top forall a. Eq a => a -> a -> Bool
==
          ModuleName -> RawTopLevelModuleName
rawTopLevelModuleNameForModuleName ModuleName
m

  -- Andreas, 2020-09-29, issue #4952.
-- The target of a @renaming@ clause needs to be highlighted in a special way.
newtype RenamingTo a = RenamingTo a

instance Hilite (RenamingTo A.QName) where
  -- Andreas, 2020-09-29, issue #4952.
  -- Do not include the bindingSite, because the HTML backed turns it into garbage.
  hilite :: RenamingTo QName -> Hiliter
hilite (RenamingTo QName
q) = do
    Maybe NameKind
kind <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks HiliteEnv -> NameKinds
hleNameKinds forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a b. (a -> b) -> a -> b
$ QName
q)
    QName -> Bool -> (Bool -> Aspects) -> Hiliter
hiliteAName QName
q Bool
False forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspects
nameAsp' Maybe NameKind
kind

instance Hilite (RenamingTo A.ModuleName) where
  -- Andreas, 2020-09-29, issue #4952.
  -- Do not include the bindingSite, because the HTML backed turns it into garbage.
  hilite :: RenamingTo ModuleName -> Hiliter
hilite (RenamingTo (A.MName [Name]
ns)) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [Name]
ns forall a b. (a -> b) -> a -> b
$ \ Name
n ->
    [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName [] (Name -> Name
A.nameConcrete Name
n) forall a. Range' a
noRange forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ NameKind -> Bool -> Aspects
nameAsp NameKind
Module

instance (Hilite (RenamingTo m), Hilite (RenamingTo n))
       => Hilite (RenamingTo (ImportedName' m n)) where
  hilite :: RenamingTo (ImportedName' m n) -> Hiliter
hilite (RenamingTo ImportedName' m n
x) = case ImportedName' m n
x of
    ImportedModule n
m -> forall a. Hilite a => a -> Hiliter
hilite (forall a. a -> RenamingTo a
RenamingTo n
m)
    ImportedName   m
n -> forall a. Hilite a => a -> Hiliter
hilite (forall a. a -> RenamingTo a
RenamingTo m
n)

hiliteQName
  :: Maybe NameKind   -- ^ Is 'NameKind' already known from the context?
  -> A.QName
  -> Hiliter
hiliteQName :: Maybe NameKind -> QName -> Hiliter
hiliteQName Maybe NameKind
mkind QName
q
  | QName -> Bool
isExtendedLambdaName QName
q = forall a. Monoid a => a
mempty
  | QName -> Bool
isAbsurdLambdaName   QName
q = forall a. Monoid a => a
mempty
  | Bool
otherwise = do
      Maybe NameKind
kind <- forall a b. Maybe a -> (a -> b) -> b -> b
ifJust Maybe NameKind
mkind (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) {-else-} forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks HiliteEnv -> NameKinds
hleNameKinds forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a b. (a -> b) -> a -> b
$ QName
q)
      QName -> Bool -> (Bool -> Aspects) -> Hiliter
hiliteAName QName
q Bool
True forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspects
nameAsp' Maybe NameKind
kind

-- | Takes the first 'NameKind'.  Binding site only included if unique.
hiliteAmbiguousQName
  :: Maybe NameKind   -- ^ Is 'NameKind' already known from the context?
  -> A.AmbiguousQName
  -> Hiliter
hiliteAmbiguousQName :: Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName Maybe NameKind
mkind (A.AmbQ List1 QName
qs) = do
  Maybe NameKind
kind <- forall a b. Maybe a -> (a -> b) -> b -> b
ifJust Maybe NameKind
mkind (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) {-else-} forall a b. (a -> b) -> a -> b
$ do
    NameKinds
kinds <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks HiliteEnv -> NameKinds
hleNameKinds
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. List1 (Maybe a) -> [a]
List1.catMaybes forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameKinds
kinds List1 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.
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap List1 QName
qs forall a b. (a -> b) -> a -> b
$ \ QName
q ->
    QName -> Bool -> (Bool -> Aspects) -> Hiliter
hiliteAName QName
q Bool
include forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspects
nameAsp' Maybe NameKind
kind
  where
  include :: Bool
include = forall a. Eq a => List1 a -> Bool
List1.allEqual forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> Range
bindingSite List1 QName
qs

hiliteBound :: A.Name -> Hiliter
hiliteBound :: Name -> Hiliter
hiliteBound Name
x =
  [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName [] (Name -> Name
A.nameConcrete Name
x) forall a. Range' a
noRange (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Name -> Range
A.nameBindingSite Name
x) forall a b. (a -> b) -> a -> b
$ NameKind -> Bool -> Aspects
nameAsp NameKind
Bound

hiliteInductiveConstructor :: A.AmbiguousQName -> Hiliter
hiliteInductiveConstructor :: AmbiguousQName -> Hiliter
hiliteInductiveConstructor = Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Induction -> NameKind
Constructor Induction
Inductive

hilitePatternSynonym :: A.AmbiguousQName -> Hiliter
hilitePatternSynonym :: AmbiguousQName -> Hiliter
hilitePatternSynonym = AmbiguousQName -> Hiliter
hiliteInductiveConstructor  -- There are no coinductive pattern synonyms!?

hiliteProjection :: A.AmbiguousQName -> Hiliter
hiliteProjection :: AmbiguousQName -> Hiliter
hiliteProjection = Maybe NameKind -> AmbiguousQName -> Hiliter
hiliteAmbiguousQName (forall a. a -> Maybe a
Just NameKind
Field)

hiliteField :: [C.Name] -> C.Name -> Maybe Range -> Hiliter
hiliteField :: [Name] -> Name -> Maybe Range -> Hiliter
hiliteField [Name]
xs Name
x Maybe Range
bindingR = [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName [Name]
xs Name
x forall a. Range' a
noRange Maybe Range
bindingR forall a b. (a -> b) -> a -> b
$ NameKind -> Bool -> Aspects
nameAsp NameKind
Field

-- 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.
hiliteModule :: (Bool, A.ModuleName) -> Hiliter
hiliteModule :: (Bool, ModuleName) -> Hiliter
hiliteModule (Bool
isTopLevelModule, A.MName []) = forall a. Monoid a => a
mempty
hiliteModule (Bool
isTopLevelModule, A.MName (Name
n:[Name]
ns)) =
  [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName
    (forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
A.nameConcrete [Name]
ms)
    (Name -> Name
A.nameConcrete Name
m)
    forall a. Range' a
noRange
    Maybe Range
mR
    (NameKind -> Bool -> Aspects
nameAsp NameKind
Module)
  where
  ([Name]
ms, Name
m) = forall a. a -> [a] -> ([a], a)
initLast1 Name
n [Name]
ns
  mR :: Maybe Range
mR = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
       forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
isTopLevelModule Range -> Range
P.beginningOfFile forall a b. (a -> b) -> a -> b
$
       Name -> Range
A.nameBindingSite Name
m

-- This was Highlighting.Generate.nameToFile:
-- | Converts names to suitable 'File's.
hiliteCName
  :: [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).
  -> Maybe Range
     -- ^ The definition site of the name. The calculated
     --   meta information is extended with this information, if possible.
  -> (Bool -> Aspects)
     -- ^ Meta information to be associated with the name.
     --   The argument is 'True' iff the name is an operator.
  -> Hiliter
hiliteCName :: [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName [Name]
xs Name
x Range
fr Maybe Range
mR Bool -> Aspects
asp = do
  HiliteEnv
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
  -- We don't care if we get any funny ranges.
  if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just (HiliteEnv -> TopLevelModuleName
hleCurrentModuleName HiliteEnv
env)) [Maybe TopLevelModuleName]
moduleNames
  then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    HighlightingInfoBuilder
frFile forall a. Semigroup a => a -> a -> a
<>
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR Range
rs) (Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = Maybe DefinitionSite
mFilePos })
  else forall a. Monoid a => a
mempty
  where
  aspects :: Aspects
aspects     = Bool -> Aspects
asp forall a b. (a -> b) -> a -> b
$ Name -> Bool
C.isOperator Name
x
  moduleNames :: [Maybe TopLevelModuleName]
moduleNames = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Range -> Maybe (Maybe TopLevelModuleName)
P.rangeModule' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasRange a => a -> Range
getRange) (Name
x forall a. a -> [a] -> [a]
: [Name]
xs)
  frFile :: HighlightingInfoBuilder
frFile      = forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR Range
fr) forall a b. (a -> b) -> a -> b
$
                Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = DefinitionSite -> DefinitionSite
notHere forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DefinitionSite
mFilePos }
  rs :: Range
rs          = forall a. HasRange a => a -> Range
getRange (Name
x 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 RangeFile
f, posPos :: forall a. Position' a -> Int32
P.posPos = Int32
p } <- forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r
    TopLevelModuleName
mod <- RangeFile -> Maybe TopLevelModuleName
P.rangeFileName RangeFile
f
    -- 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 = forall a. Int -> [a] -> [a]
drop (forall a. Sized a => a -> Int
size TopLevelModuleName
mod) [Name]
xs
    -- For bound variables, we do not create symbolic anchors.
        local :: Bool
local = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Aspect -> Bool
isLocalAspect forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect Aspects
aspects
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ DefinitionSite
      { defSiteModule :: TopLevelModuleName
defSiteModule = TopLevelModuleName
mod
      , defSitePos :: Int
defSitePos    = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p
        -- Is our current position the definition site?
      , defSiteHere :: Bool
defSiteHere   = Range
r forall a. Eq a => a -> a -> Bool
== forall a. HasRange a => a -> 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 String
defSiteAnchor = if Bool
local Bool -> Bool -> Bool
|| forall a. IsNoName a => a -> Bool
C.isNoName Name
x Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Underscore a => a -> Bool
Common.isUnderscore [Name]
qualifiers
          then forall a. Maybe a
Nothing
          else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow forall a b. (a -> b) -> a -> b
$ 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 (Just NameKind
kind) Bool
_ -> NameKind -> Bool
isLocal NameKind
kind
    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

-- This was Highlighting.Generate.nameToFileA:
-- | A variant of 'hiliteCName' for qualified abstract names.
hiliteAName
  :: 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.
  -> Hiliter
hiliteAName :: QName -> Bool -> (Bool -> Aspects) -> Hiliter
hiliteAName QName
x Bool
include Bool -> Aspects
asp = do
  TopLevelModuleName
currentModule <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks HiliteEnv -> TopLevelModuleName
hleCurrentModuleName
  [Name]
-> Name -> Range -> Maybe Range -> (Bool -> Aspects) -> Hiliter
hiliteCName (QName -> [Name]
concreteQualifier QName
x)
              (QName -> Name
concreteBase QName
x)
              (TopLevelModuleName -> Range
rangeOfFixityDeclaration TopLevelModuleName
currentModule)
              (if Bool
include then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x else forall a. Maybe a
Nothing)
              Bool -> Aspects
asp
    forall a. Semigroup a => a -> a -> a
<> TopLevelModuleName -> Hiliter
notationFile TopLevelModuleName
currentModule
  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 :: TopLevelModuleName -> Range
rangeOfFixityDeclaration TopLevelModuleName
currentModule =
    if Range -> Maybe TopLevelModuleName
P.rangeModule Range
r forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just TopLevelModuleName
currentModule
    then Range
r else forall a. Range' a
noRange
    where
    r :: Range
r = Fixity' -> Range
theNameRange forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x

  notationFile :: TopLevelModuleName -> Hiliter
notationFile TopLevelModuleName
currentModule = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    if Range -> Maybe TopLevelModuleName
P.rangeModule (forall a. HasRange a => a -> Range
getRange Notation
notation) forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just TopLevelModuleName
currentModule
    then forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map NotationPart -> HighlightingInfoBuilder
genPartFile Notation
notation
    else forall a. Monoid a => a
mempty
    where
    notation :: Notation
notation = Fixity' -> Notation
theNotation forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x

    boundAspect :: Aspects
boundAspect = NameKind -> Bool -> Aspects
nameAsp NameKind
Bound Bool
False

    genPartFile :: NotationPart -> HighlightingInfoBuilder
genPartFile (VarPart Range
r Ranged BoundVariablePosition
i)  = forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Ranged BoundVariablePosition
i] Aspects
boundAspect
    genPartFile (HolePart Range
r NamedArg (Ranged Int)
i) = forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange NamedArg (Ranged Int)
i] Aspects
boundAspect
    genPartFile WildPart{}     = forall a. Monoid a => a
mempty
    genPartFile (IdPart RString
x)     = forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange RString
x) (Bool -> Aspects
asp Bool
False)

-- * Short auxiliary functions.
---------------------------------------------------------------------------

singleAspect :: HasRange a => Aspect -> a -> Hiliter
singleAspect :: forall a. HasRange a => Aspect -> a -> Hiliter
singleAspect Aspect
a a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange a
x) forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { aspect :: Maybe Aspect
aspect = forall a. a -> Maybe a
Just Aspect
a }

singleOtherAspect :: HasRange a => OtherAspect -> a -> Hiliter
singleOtherAspect :: forall a. HasRange a => OtherAspect -> a -> Hiliter
singleOtherAspect OtherAspect
a a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a m. IsBasicRangeMap a m => Ranges -> a -> m
H.singleton (Range -> Ranges
rToR forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange a
x) forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = forall el coll. Singleton el coll => el -> coll
singleton OtherAspect
a }

nameAsp' :: Maybe NameKind -> Bool -> Aspects
nameAsp' :: Maybe NameKind -> Bool -> Aspects
nameAsp' Maybe NameKind
k Bool
isOp = Aspects
parserBased { aspect :: Maybe Aspect
aspect = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name Maybe NameKind
k Bool
isOp }

nameAsp :: NameKind -> Bool -> Aspects
nameAsp :: NameKind -> Bool -> Aspects
nameAsp = Maybe NameKind -> Bool -> Aspects
nameAsp' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just

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

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

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