-- | 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 m :: 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 Inductive)   = "inductiveconstructor"
  kindToAtom (Constructor CoInductive) = "coinductiveconstructor"
  kindToAtom k :: NameKind
k                         = NameKind -> String
forall a. Show a => a -> String
toAtom NameKind
k

  toAtoms' :: Maybe Aspect -> [String]
toAtoms' Nothing               = []
  toAtoms' (Just (Name mKind :: Maybe NameKind
mKind op :: 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        = ["operator"]
                 | Bool
otherwise = []
  toAtoms' (Just a :: 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 info :: HighlightingInfo
info method :: HighlightingMethod
method = case HighlightingInfo -> [(Range, Aspects)]
ranges HighlightingInfo
info of
  _             | HighlightingMethod
method HighlightingMethod -> HighlightingMethod -> Bool
forall a. Eq a => a -> a -> Bool
== HighlightingMethod
Direct -> HighlightingMethod
Direct
  ((_, mi :: Aspects
mi) : _) | Aspects -> Bool
check Aspects
mi         -> HighlightingMethod
Direct
  _                                -> HighlightingMethod
Indirect

  where check :: Aspects -> Bool
check mi :: 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