{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Serialise.Instances.Highlighting where

import qualified Data.Map.Strict as Map
import Data.Strict.Tuple (Pair(..))

import qualified Agda.Interaction.Highlighting.Range   as HR
import qualified Agda.Interaction.Highlighting.Precise as HP
import qualified Agda.Utils.RangeMap                   as RM

import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common () --instance only

instance EmbPrj HR.Range where
  icod_ (HR.Range a b) = icodeN' HR.Range a b

  value = valueN HR.Range

instance EmbPrj HP.NameKind where
  icod_ HP.Bound           = icodeN' HP.Bound
  icod_ (HP.Constructor a) = icodeN 1 HP.Constructor a
  icod_ HP.Datatype        = icodeN 2 ()
  icod_ HP.Field           = icodeN 3 ()
  icod_ HP.Function        = icodeN 4 ()
  icod_ HP.Module          = icodeN 5 ()
  icod_ HP.Postulate       = icodeN 6 ()
  icod_ HP.Primitive       = icodeN 7 ()
  icod_ HP.Record          = icodeN 8 ()
  icod_ HP.Argument        = icodeN 9 ()
  icod_ HP.Macro           = icodeN 10 ()
  icod_ HP.Generalizable   = icodeN 11 ()

  value = vcase valu where
    valu []      = valuN HP.Bound
    valu [1 , a] = valuN HP.Constructor a
    valu [2]     = valuN HP.Datatype
    valu [3]     = valuN HP.Field
    valu [4]     = valuN HP.Function
    valu [5]     = valuN HP.Module
    valu [6]     = valuN HP.Postulate
    valu [7]     = valuN HP.Primitive
    valu [8]     = valuN HP.Record
    valu [9]     = valuN HP.Argument
    valu [10]    = valuN HP.Macro
    valu [11]    = valuN HP.Generalizable
    valu _       = malformed

instance EmbPrj HP.Aspect where
  icod_ HP.Comment        = icodeN 0 ()
  icod_ HP.Keyword       = icodeN 1 ()
  icod_ HP.String        = icodeN 2 ()
  icod_ HP.Number        = icodeN 3 ()
  icod_ HP.Symbol        = icodeN' HP.Symbol
  icod_ HP.PrimitiveType = icodeN 4 ()
  icod_ (HP.Name mk b)   = icodeN 5 HP.Name mk b
  icod_ HP.Pragma        = icodeN 6 ()
  icod_ HP.Background    = icodeN 7 ()
  icod_ HP.Markup        = icodeN 8 ()
  icod_ HP.Hole          = icodeN 9 ()

  value = vcase valu where
    valu [0]        = valuN HP.Comment
    valu [1]        = valuN HP.Keyword
    valu [2]        = valuN HP.String
    valu [3]        = valuN HP.Number
    valu []         = valuN HP.Symbol
    valu [4]        = valuN HP.PrimitiveType
    valu [5, mk, b] = valuN HP.Name mk b
    valu [6]        = valuN HP.Pragma
    valu [7]        = valuN HP.Background
    valu [8]        = valuN HP.Markup
    valu [9]        = valuN HP.Hole
    valu _          = malformed

instance EmbPrj HP.OtherAspect where
  icod_ HP.Error                = icodeN 0 ()
  icod_ HP.ErrorWarning         = icodeN 1 ()
  icod_ HP.DottedPattern        = icodeN' HP.DottedPattern
  icod_ HP.UnsolvedMeta         = icodeN 2 ()
  icod_ HP.TerminationProblem   = icodeN 3 ()
  icod_ HP.IncompletePattern    = icodeN 4 ()
  icod_ HP.TypeChecks           = icodeN 5 ()
  icod_ HP.UnsolvedConstraint   = icodeN 6 ()
  icod_ HP.PositivityProblem    = icodeN 7 ()
  icod_ HP.Deadcode             = icodeN 8 ()
  icod_ HP.CoverageProblem      = icodeN 9 ()
  icod_ HP.CatchallClause       = icodeN 10 ()
  icod_ HP.ConfluenceProblem    = icodeN 11 ()
  icod_ HP.MissingDefinition    = icodeN 12 ()
  icod_ HP.ShadowingInTelescope = icodeN 13 ()

  value = vcase valu where
    valu [0] = valuN HP.Error
    valu [1] = valuN HP.ErrorWarning
    valu []  = valuN HP.DottedPattern
    valu [2] = valuN HP.UnsolvedMeta
    valu [3] = valuN HP.TerminationProblem
    valu [4] = valuN HP.IncompletePattern
    valu [5] = valuN HP.TypeChecks
    valu [6] = valuN HP.UnsolvedConstraint
    valu [7] = valuN HP.PositivityProblem
    valu [8] = valuN HP.Deadcode
    valu [9] = valuN HP.CoverageProblem
    valu [10] = valuN HP.CatchallClause
    valu [11] = valuN HP.ConfluenceProblem
    valu [12] = valuN HP.MissingDefinition
    valu [13] = valuN HP.ShadowingInTelescope
    valu _   = malformed

instance EmbPrj HP.Aspects where
  icod_ (HP.Aspects a b c d e) = icodeN' HP.Aspects a b c d e

  value = valueN HP.Aspects

instance EmbPrj HP.DefinitionSite where
  icod_ (HP.DefinitionSite a b c d) = icodeN' HP.DefinitionSite a b c d

  value = valueN HP.DefinitionSite

instance EmbPrj a => EmbPrj (RM.RangeMap a) where
  -- Write the RangeMap as flat list rather than a list of (Int, (Int, x)). Much
  -- like Map, we need to call `convert' in the tail position and so the output
  -- list is written (and read) in reverse order.
  icod_ (RM.RangeMap f) = icodeNode =<< convert [] (Map.toAscList f) where
    convert ys [] = return ys
    convert ys ((start, RM.PairInt (end :!: entry)):xs) = do
      start <- icode start
      end <- icode end
      entry <- icode entry
      convert (start:end:entry:ys) xs

  value = vcase (fmap (RM.RangeMap . Map.fromDistinctAscList) . convert []) where
    convert ys [] = return ys
    convert ys (start:end:entry:xs) = do
      start <- value start
      end <- value end
      entry <- value entry
      convert ((start, RM.PairInt (end :!: entry)):ys) xs
    convert _ _ = malformed

instance EmbPrj HP.TokenBased where
  icod_ HP.TokenBased        = icodeN 0 ()
  icod_ HP.NotOnlyTokenBased = icodeN' HP.NotOnlyTokenBased

  value = vcase valu where
    valu [0] = valuN HP.TokenBased
    valu []  = valuN HP.NotOnlyTokenBased
    valu _   = malformed