-- | Common syntax highlighting functions for Emacs and JSON

module Agda.Interaction.Highlighting.Common
  ( toAtoms
  , chooseHighlightingMethod
  ) where

import Agda.Interaction.Highlighting.Precise
import Agda.Syntax.Common
import Agda.TypeChecking.Monad (HighlightingMethod(..))
import Data.Maybe (maybeToList)
import Data.Char (toLower)
import qualified Data.Set as Set

-- | Converts the 'aspect' and 'otherAspects' fields to strings that are
-- friendly to editors.
toAtoms :: Aspects -> [String]
toAtoms :: Aspects -> [String]
toAtoms Aspects
m = (OtherAspect -> String) -> [OtherAspect] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> String
forall a. Show a => a -> String
toAtom (Set OtherAspect -> [OtherAspect]
forall a. Set a -> [a]
Set.toList (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect -> [OtherAspect]
forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects Aspects
m)
         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Maybe Aspect -> [String]
toAtoms' (Aspects -> Maybe Aspect
aspect Aspects
m)
  where

  toAtom :: Show a => a -> String
  toAtom :: a -> String
toAtom = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show

  kindToAtom :: NameKind -> String
kindToAtom (Constructor Induction
Inductive)   = String
"inductiveconstructor"
  kindToAtom (Constructor Induction
CoInductive) = String
"coinductiveconstructor"
  kindToAtom NameKind
k                         = NameKind -> String
forall a. Show a => a -> String
toAtom NameKind
k

  toAtoms' :: Maybe Aspect -> [String]
toAtoms' Maybe Aspect
Nothing               = []
  toAtoms' (Just (Name Maybe NameKind
mKind Bool
op)) =
    (NameKind -> String) -> [NameKind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NameKind -> String
kindToAtom (Maybe NameKind -> [NameKind]
forall a. Maybe a -> [a]
maybeToList Maybe NameKind
mKind) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
opAtom
    where opAtom :: [String]
opAtom | Bool
op        = [String
"operator"]
                 | Bool
otherwise = []
  toAtoms' (Just Aspect
a) = [Aspect -> String
forall a. Show a => a -> String
toAtom Aspect
a]

-- | Choose which method to use based on HighlightingInfo and HighlightingMethod
chooseHighlightingMethod
  :: HighlightingInfo
  -> HighlightingMethod
  -> HighlightingMethod
chooseHighlightingMethod :: HighlightingInfo -> HighlightingMethod -> HighlightingMethod
chooseHighlightingMethod HighlightingInfo
info HighlightingMethod
method = case HighlightingInfo -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
info of
  [(Range, Aspects)]
_             | HighlightingMethod
method HighlightingMethod -> HighlightingMethod -> Bool
forall a. Eq a => a -> a -> Bool
== HighlightingMethod
Direct -> HighlightingMethod
Direct
  ((Range
_, Aspects
mi) : [(Range, Aspects)]
_) | Aspects -> Bool
check Aspects
mi         -> HighlightingMethod
Direct
  [(Range, Aspects)]
_                                -> HighlightingMethod
Indirect

  where check :: Aspects -> Bool
check Aspects
mi = Aspects -> Set OtherAspect
otherAspects Aspects
mi Set OtherAspect -> Set OtherAspect -> Bool
forall a. Eq a => a -> a -> Bool
== OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
TypeChecks
                Bool -> Bool -> Bool
|| Aspects
mi Aspects -> Aspects -> Bool
forall a. Eq a => a -> a -> Bool
== Aspects
forall a. Monoid a => a
mempty