{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances.Highlighting where
import qualified Agda.Interaction.Highlighting.Range as HR
import qualified Agda.Interaction.Highlighting.Precise as HP
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common ()
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 ()
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 _ = malformed
instance EmbPrj HP.OtherAspect where
icod_ HP.Error = icodeN 0 ()
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 [] = 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 HP.CompressedFile where
icod_ (HP.CompressedFile f) = icodeN' HP.CompressedFile f
value = valueN HP.CompressedFile
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