{-# LANGUAGE DeriveDataTypeable #-}

-- | Types used for precise syntax highlighting.

module Agda.Interaction.Highlighting.Precise
  ( Aspect(..)
  , NameKind(..)
  , OtherAspect(..)
  , MetaInfo(..)
  , File
  , HighlightingInfo(..)
  , singleton
  , several
  , smallestPos
  , toMap
  , CompressedFile
  , compress
  , decompress
  , Agda.Interaction.Highlighting.Precise.tests
  ) where

import Agda.Utils.TestHelpers
import Agda.Utils.String
import Agda.Utils.List hiding (tests)
import Data.List
import Data.Function
import Data.Monoid
import Control.Monad
import Agda.Utils.QuickCheck
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Generics

import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Common as C

import Agda.Interaction.Highlighting.Range

------------------------------------------------------------------------
-- Files

-- | Various more or less syntactic aspects of the code. (These cannot
-- overlap.)

data Aspect
  = Comment
  | Keyword
  | String
  | Number
  | Symbol                     -- ^ Symbols like forall, =, ->, etc.
  | PrimitiveType              -- ^ Things like Set and Prop.
  | Name (Maybe NameKind) Bool -- ^ Is the name an operator part?
    deriving (Eq, Show, Typeable, Data)

data NameKind
  = Bound                   -- ^ Bound variable.
  | Constructor C.Induction -- ^ Inductive or coinductive constructor.
  | Datatype
  | Field                   -- ^ Record field.
  | Function
  | Module                  -- ^ Module name.
  | Postulate
  | Primitive               -- ^ Primitive.
  | Record                  -- ^ Record type.
    deriving (Eq, Show, Typeable, Data)

-- | Other aspects. (These can overlap with each other and with
-- 'Aspect's.)

data OtherAspect
  = Error
  | DottedPattern
  | UnsolvedMeta
  | TerminationProblem
  | IncompletePattern
    -- ^ When this constructor is used it is probably a good idea to
    -- include a 'note' explaining why the pattern is incomplete.
    deriving (Eq, Show, Enum, Bounded, Typeable, Data)

-- | Meta information which can be associated with a
-- character\/character range.

data MetaInfo = MetaInfo
  { aspect       :: Maybe Aspect
  , otherAspects :: [OtherAspect]
  , note         :: Maybe String
    -- ^ This note, if present, can be displayed as a tool-tip or
    -- something like that. It should contain useful information about
    -- the range (like the module containing a certain identifier, or
    -- the fixity of an operator).
  , definitionSite :: Maybe ([String], FilePath, Integer)
    -- ^ The definition site of the annotated thing, if applicable and
    --   known. File positions are counted from 1. The list of strings
    --   is the name of the /top-level/ module in which the thing is
    --   defined.
  }
  deriving (Eq, Show, Typeable, Data)

-- | A 'File' is a mapping from file positions to meta information.
--
-- The first position in the file has number 1.

newtype File = File { mapping :: Map Integer MetaInfo }
  deriving (Eq, Show, Typeable, Data)

-- | Returns the smallest position, if any, in the 'File'.

smallestPos :: File -> Maybe Integer
smallestPos = fmap (fst . fst) . Map.minViewWithKey . mapping

-- | Syntax highlighting information for a given source file.

data HighlightingInfo =
  HighlightingInfo { source :: FilePath
                     -- ^ The source file.
                   , info :: CompressedFile
                     -- ^ Highlighting info.
                   }
  deriving (Typeable, Data)

------------------------------------------------------------------------
-- Creation

-- | @'singleton' r m@ is a file whose positions are those in @r@, and
-- in which every position is associated with @m@.

singleton :: Range -> MetaInfo -> File
singleton r m = File {
 mapping = Map.fromAscList [ (p, m) | p <- toList r ] }

prop_singleton r m =
  compress (singleton r m) ==
    if null (toList r) then [] else [(r, m)]

-- | Like 'singleton', but with several ranges instead of only one.

several :: [Range] -> MetaInfo -> File
several rs m = mconcat $ map (\r -> singleton r m) rs

------------------------------------------------------------------------
-- Merging

-- | Merges meta information.

mergeMetaInfo :: MetaInfo -> MetaInfo -> MetaInfo
mergeMetaInfo m1 m2 = MetaInfo
  { aspect       = (mplus `on` aspect) m1 m2
  , otherAspects = nub $ ((++) `on` otherAspects) m1 m2
  , note         = case (note m1, note m2) of
      (Just n1, Just n2) -> Just $
         if n1 == n2 then n1
                     else addFinalNewLine n1 ++ "----\n" ++ n2
      (Just n1, Nothing) -> Just n1
      (Nothing, Just n2) -> Just n2
      (Nothing, Nothing) -> Nothing
  , definitionSite = (mplus `on` definitionSite) m1 m2
  }

instance Monoid MetaInfo where
  mempty = MetaInfo { aspect         = Nothing
                    , otherAspects   = []
                    , note           = Nothing
                    , definitionSite = Nothing
                    }
  mappend = mergeMetaInfo

-- | Merges files.

merge :: File -> File -> File
merge f1 f2 =
  File { mapping = (Map.unionWith mappend `on` mapping) f1 f2 }

instance Monoid File where
  mempty  = File { mapping = Map.empty }
  mappend = merge

------------------------------------------------------------------------
-- Inspection

-- | Convert the 'File' to a map from file positions (counting from 1)
-- to meta information.

toMap :: File -> Map Integer MetaInfo
toMap = mapping

------------------------------------------------------------------------
-- Compression

-- | A compressed 'File', in which consecutive positions with the same
-- 'MetaInfo' are stored together.

type CompressedFile = [(Range, MetaInfo)]

-- | Compresses a file by merging consecutive positions with equal
-- meta information into longer ranges.

compress :: File -> CompressedFile
compress f = map join $ groupBy' p (Map.toAscList $ mapping f)
  where
  p (pos1, m1) (pos2, m2) = pos2 == pos1 + 1 && m1 == m2
  join pms = ( Range { from = head ps, to = last ps + 1 }
             , head ms
             )
    where (ps, ms) = unzip pms

-- | Decompresses a compressed file.

decompress :: CompressedFile -> File
decompress =
  File .
  Map.fromList .
  concat .
  map (\(r, m) -> [ (p, m) | p <- toList r ])

prop_compress f =
  decompress c == f
  &&
  and (map (rangeInvariant . fst) c)
  &&
  and [ not (overlapping r1 r2) | (r1, r2) <- allPairs (map fst c) ]
  where
    c = compress f

    allPairs []       = []
    allPairs (x : xs) = map ((,) x) xs ++ allPairs xs

------------------------------------------------------------------------
-- Generators

instance Arbitrary Aspect where
  arbitrary =
    frequency [ (3, elements [ Comment, Keyword, String, Number
                             , Symbol, PrimitiveType ])
              , (1, liftM2 Name (maybeGen arbitrary) arbitrary)
              ]

instance CoArbitrary Aspect where
  coarbitrary Comment       = variant 0
  coarbitrary Keyword       = variant 1
  coarbitrary String        = variant 2
  coarbitrary Number        = variant 3
  coarbitrary Symbol        = variant 4
  coarbitrary PrimitiveType = variant 5
  coarbitrary (Name nk b)   =
    variant 6 . maybeCoGen coarbitrary nk . coarbitrary b

instance Arbitrary NameKind where
  arbitrary = oneof $ [liftM Constructor arbitrary] ++
                      map return [ Bound
                                 , Datatype
                                 , Field
                                 , Function
                                 , Module
                                 , Postulate
                                 , Primitive
                                 , Record
                                 ]

instance CoArbitrary NameKind where
  coarbitrary Bound             = variant 0
  coarbitrary (Constructor ind) = variant 1 . coarbitrary ind
  coarbitrary Datatype          = variant 2
  coarbitrary Field             = variant 3
  coarbitrary Function          = variant 4
  coarbitrary Module            = variant 5
  coarbitrary Postulate         = variant 6
  coarbitrary Primitive         = variant 7
  coarbitrary Record            = variant 8

instance Arbitrary OtherAspect where
  arbitrary = elements [minBound .. maxBound]

instance CoArbitrary OtherAspect where
  coarbitrary = coarbitrary . fromEnum

instance Arbitrary MetaInfo where
  arbitrary = do
    aspect  <- maybeGen arbitrary
    other   <- arbitrary
    note    <- maybeGen string
    defSite <- maybeGen (liftM3 (,,) (listOf string) string arbitrary)
    return (MetaInfo { aspect = aspect, otherAspects = other
                     , note = note, definitionSite = defSite })
    where string = listOfElements "abcdefABCDEF/\\.\"'@()åäö\n"

instance CoArbitrary MetaInfo where
  coarbitrary (MetaInfo aspect otherAspects note defSite) =
    coarbitrary aspect .
    coarbitrary otherAspects .
    coarbitrary note .
    coarbitrary defSite

instance Arbitrary File where
  arbitrary = fmap (File . Map.fromList) $ listOf arbitrary

instance CoArbitrary File where
  coarbitrary (File rs) = coarbitrary (Map.toAscList rs)

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

-- | All the properties.

tests :: IO Bool
tests = runTests "Agda.Interaction.Highlighting.Precise"
  [ quickCheck' prop_singleton
  , quickCheck' prop_compress
  ]