content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- |
  -- Agda strings uses Data.Text [1], which can only represent unicode scalar values [2], excluding
  -- the surrogate code points [3] (@U+D800..U+DFFF@). To allow @primStringFromList@ to be injective
  -- we make sure character values also exclude surrogate code points, mapping them to the replacement
  -- character @U+FFFD@.
  --
  -- See #4999 for more information.
  --
  -- [1] https://hackage.haskell.org/package/text-1.2.4.0/docs/Data-Text.html#g:2
  -- [2] https://www.unicode.org/glossary/#unicode_scalar_value
  -- [3] https://www.unicode.org/glossary/#surrogate_code_point
  
  module Agda.Utils.Char where
  
  import Data.Char
  
  -- | The unicode replacement character � .
  replacementChar :: Char
  replacementChar = '\xFFFD'
  
  -- | Is a character a surrogate code point.
  isSurrogateCodePoint :: Char -> Bool
  isSurrogateCodePoint c = generalCategory c == Surrogate
  
  -- | Map surrogate code points to the unicode replacement character.
  replaceSurrogateCodePoint :: Char -> Char
  replaceSurrogateCodePoint c
    | isSurrogateCodePoint c = replacementChar
    | otherwise              = c
  
  -- | Total function to convert an integer to a character. Maps surrogate code points
  --   to the replacement character @U+FFFD@.
  integerToChar :: Integer -> Char
  integerToChar = replaceSurrogateCodePoint . toEnum . fromIntegral . (`mod` 0x110000)
  
  