    {-# OPTIONS_GHC -Wunused-imports #-}

    {-| Choice of Unicode or ASCII glyphs.
    -}
    module Agda.Syntax.Concrete.Glyph
      ( UnicodeOrAscii(..)
      , unsafeSetUnicodeOrAscii
      , specialCharactersForGlyphs
      , braces', dbraces
      , forallQ
      , leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt
      , arrow, lambda
      , SpecialCharacters(..)
      ) where

    import Control.DeepSeq

    import Data.IORef (IORef, newIORef, readIORef, writeIORef)
    import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)

    import GHC.Generics (Generic)

    import Agda.Utils.Boolean
    import Agda.Utils.List
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty

    -- | We want to know whether we are allowed to insert unicode characters or not.
    data UnicodeOrAscii
      = UnicodeOk  -- ^ 'true': Unicode characters are allowed.
      | AsciiOnly  -- ^ 'false: Stick to ASCII.
      deriving (Int -> UnicodeOrAscii -> ShowS
    [UnicodeOrAscii] -> ShowS
    UnicodeOrAscii -> String
    (Int -> UnicodeOrAscii -> ShowS)
    -> (UnicodeOrAscii -> String)
    -> ([UnicodeOrAscii] -> ShowS)
    -> Show UnicodeOrAscii
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnicodeOrAscii -> ShowS
    showsPrec :: Int -> UnicodeOrAscii -> ShowS
    $cshow :: UnicodeOrAscii -> String
    show :: UnicodeOrAscii -> String
    $cshowList :: [UnicodeOrAscii] -> ShowS
    showList :: [UnicodeOrAscii] -> ShowS
    Show, UnicodeOrAscii -> UnicodeOrAscii -> Bool
    (UnicodeOrAscii -> UnicodeOrAscii -> Bool)
    -> (UnicodeOrAscii -> UnicodeOrAscii -> Bool) -> Eq UnicodeOrAscii
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: UnicodeOrAscii -> UnicodeOrAscii -> Bool
    == :: UnicodeOrAscii -> UnicodeOrAscii -> Bool
    $c/= :: UnicodeOrAscii -> UnicodeOrAscii -> Bool
    /= :: UnicodeOrAscii -> UnicodeOrAscii -> Bool
    Eq, Int -> UnicodeOrAscii
    UnicodeOrAscii -> Int
    UnicodeOrAscii -> [UnicodeOrAscii]
    UnicodeOrAscii -> UnicodeOrAscii
    UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    UnicodeOrAscii
    -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    (UnicodeOrAscii -> UnicodeOrAscii)
    -> (UnicodeOrAscii -> UnicodeOrAscii)
    -> (Int -> UnicodeOrAscii)
    -> (UnicodeOrAscii -> Int)
    -> (UnicodeOrAscii -> [UnicodeOrAscii])
    -> (UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii])
    -> (UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii])
    -> (UnicodeOrAscii
        -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii])
    -> Enum UnicodeOrAscii
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: UnicodeOrAscii -> UnicodeOrAscii
    succ :: UnicodeOrAscii -> UnicodeOrAscii
    $cpred :: UnicodeOrAscii -> UnicodeOrAscii
    pred :: UnicodeOrAscii -> UnicodeOrAscii
    $ctoEnum :: Int -> UnicodeOrAscii
    toEnum :: Int -> UnicodeOrAscii
    $cfromEnum :: UnicodeOrAscii -> Int
    fromEnum :: UnicodeOrAscii -> Int
    $cenumFrom :: UnicodeOrAscii -> [UnicodeOrAscii]
    enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii]
    $cenumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    $cenumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    $cenumFromThenTo :: UnicodeOrAscii
    -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    enumFromThenTo :: UnicodeOrAscii
    -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
    Enum, UnicodeOrAscii
    UnicodeOrAscii -> UnicodeOrAscii -> Bounded UnicodeOrAscii
    forall a. a -> a -> Bounded a
    $cminBound :: UnicodeOrAscii
    minBound :: UnicodeOrAscii
    $cmaxBound :: UnicodeOrAscii
    maxBound :: UnicodeOrAscii
    Bounded, (forall x. UnicodeOrAscii -> Rep UnicodeOrAscii x)
    -> (forall x. Rep UnicodeOrAscii x -> UnicodeOrAscii)
    -> Generic UnicodeOrAscii
    forall x. Rep UnicodeOrAscii x -> UnicodeOrAscii
    forall x. UnicodeOrAscii -> Rep UnicodeOrAscii x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. UnicodeOrAscii -> Rep UnicodeOrAscii x
    from :: forall x. UnicodeOrAscii -> Rep UnicodeOrAscii x
    $cto :: forall x. Rep UnicodeOrAscii x -> UnicodeOrAscii
    to :: forall x. Rep UnicodeOrAscii x -> UnicodeOrAscii
    Generic)

    instance NFData UnicodeOrAscii

    instance Boolean UnicodeOrAscii where
      fromBool :: Bool -> UnicodeOrAscii
    fromBool = \case
        Bool
    True -> UnicodeOrAscii
    UnicodeOk
        Bool
    False -> UnicodeOrAscii
    AsciiOnly

    instance IsBool UnicodeOrAscii where
      toBool :: UnicodeOrAscii -> Bool
    toBool = \case
        UnicodeOrAscii
    UnicodeOk -> Bool
    True
        UnicodeOrAscii
    AsciiOnly -> Bool
    False

    {-# NOINLINE unsafeUnicodeOrAsciiIORef #-}
    unsafeUnicodeOrAsciiIORef :: IORef UnicodeOrAscii
    unsafeUnicodeOrAsciiIORef :: IORef UnicodeOrAscii
    unsafeUnicodeOrAsciiIORef = IO (IORef UnicodeOrAscii) -> IORef UnicodeOrAscii
    forall a. IO a -> a
    UNSAFE.unsafePerformIO (IO (IORef UnicodeOrAscii) -> IORef UnicodeOrAscii)
    -> IO (IORef UnicodeOrAscii) -> IORef UnicodeOrAscii
    forall a b. (a -> b) -> a -> b
    $ UnicodeOrAscii -> IO (IORef UnicodeOrAscii)
    forall a. a -> IO (IORef a)
    newIORef UnicodeOrAscii
    UnicodeOk

    {-# NOINLINE unsafeSetUnicodeOrAscii #-}
    unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()
    unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()
    unsafeSetUnicodeOrAscii = IORef UnicodeOrAscii -> UnicodeOrAscii -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef IORef UnicodeOrAscii
    unsafeUnicodeOrAsciiIORef

    -- | Are we allowed to use unicode supscript characters?
    unsafeUnicodeOrAscii :: UnicodeOrAscii
    unsafeUnicodeOrAscii :: UnicodeOrAscii
    unsafeUnicodeOrAscii = IO UnicodeOrAscii -> UnicodeOrAscii
    forall a. IO a -> a
    UNSAFE.unsafePerformIO (IORef UnicodeOrAscii -> IO UnicodeOrAscii
    forall a. IORef a -> IO a
    readIORef IORef UnicodeOrAscii
    unsafeUnicodeOrAsciiIORef)

    -- | Picking the appropriate set of special characters depending on
    -- whether we are allowed to use unicode or have to limit ourselves
    -- to ascii.

    data SpecialCharacters = SpecialCharacters
      { SpecialCharacters -> Doc -> Doc
    _dbraces :: Doc -> Doc
      , SpecialCharacters -> Doc
    _lambda  :: Doc
      , SpecialCharacters -> Doc
    _arrow   :: Doc
      , SpecialCharacters -> Doc
    _forallQ :: Doc
      , SpecialCharacters -> Doc
    _leftIdiomBrkt  :: Doc
      , SpecialCharacters -> Doc
    _rightIdiomBrkt :: Doc
      , SpecialCharacters -> Doc
    _emptyIdiomBrkt :: Doc
      }

    specialCharactersUnicode :: SpecialCharacters
    specialCharactersUnicode :: SpecialCharacters
    specialCharactersUnicode = SpecialCharacters
      { _dbraces :: Doc -> Doc
    _dbraces        = ((Doc -> Doc
    hlSymbol Doc
    "\x2983 " Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <>) (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    hlSymbol Doc
    " \x2984"))
      , _lambda :: Doc
    _lambda         = Doc -> Doc
    hlSymbol Doc
    "\x03bb"
      , _arrow :: Doc
    _arrow          = Doc -> Doc
    hlSymbol Doc
    "\x2192"
      , _forallQ :: Doc
    _forallQ        = Doc -> Doc
    hlSymbol Doc
    "\x2200"
      , _leftIdiomBrkt :: Doc
    _leftIdiomBrkt  = Doc -> Doc
    hlSymbol Doc
    "\x2987"
      , _rightIdiomBrkt :: Doc
    _rightIdiomBrkt = Doc -> Doc
    hlSymbol Doc
    "\x2988"
      , _emptyIdiomBrkt :: Doc
    _emptyIdiomBrkt = Doc -> Doc
    hlSymbol Doc
    "\x2987\x2988"
      }

    specialCharactersAscii :: SpecialCharacters
    specialCharactersAscii :: SpecialCharacters
    specialCharactersAscii = SpecialCharacters
      { _dbraces :: Doc -> Doc
    _dbraces        = Doc -> Doc
    braces (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Doc
    braces'
      , _lambda :: Doc
    _lambda         = Doc -> Doc
    hlSymbol Doc
    "\\"
      , _arrow :: Doc
    _arrow          = Doc -> Doc
    hlSymbol Doc
    "->"
      , _forallQ :: Doc
    _forallQ        = Doc -> Doc
    hlSymbol Doc
    "forall"
      , _leftIdiomBrkt :: Doc
    _leftIdiomBrkt  = Doc -> Doc
    hlSymbol Doc
    "(|"
      , _rightIdiomBrkt :: Doc
    _rightIdiomBrkt = Doc -> Doc
    hlSymbol Doc
    "|)"
      , _emptyIdiomBrkt :: Doc
    _emptyIdiomBrkt = Doc -> Doc
    hlSymbol Doc
    "(|)"
      }

    -- | Return the glyph set based on a given (unicode or ascii) glyph mode
    specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters
    specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters
    specialCharactersForGlyphs UnicodeOrAscii
    UnicodeOk = SpecialCharacters
    specialCharactersUnicode
    specialCharactersForGlyphs UnicodeOrAscii
    AsciiOnly = SpecialCharacters
    specialCharactersAscii

    -- | Choose the glyph set based on the unsafe IORef.
    {-# NOINLINE specialCharacters #-}
    specialCharacters :: SpecialCharacters
    specialCharacters :: SpecialCharacters
    specialCharacters = UnicodeOrAscii -> SpecialCharacters
    specialCharactersForGlyphs UnicodeOrAscii
    unsafeUnicodeOrAscii

    braces' :: Doc -> Doc
    braces' :: Doc -> Doc
    braces' Doc
    d = String -> Doc -> (Char -> String -> Doc) -> Doc
    forall a b. [a] -> b -> (a -> [a] -> b) -> b
    caseList (Doc -> String
    forall a. Doc a -> String
    render Doc
    d) (Doc -> Doc
    braces Doc
    d) {-else-} ((Char -> String -> Doc) -> Doc) -> (Char -> String -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ \ Char
    c String
    cs ->
      Doc -> Doc
    braces (Char -> Doc
    forall {a}. (IsString a, Null a) => Char -> a
    spaceIfDash Char
    c Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    d Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Char -> Doc
    forall {a}. (IsString a, Null a) => Char -> a
    spaceIfDash (Char -> String -> Char
    forall a. a -> [a] -> a
    last1 Char
    c String
    cs))
      -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
      -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
      where
      spaceIfDash :: Char -> a
    spaceIfDash Char
    '-' = a
    " "
      spaceIfDash Char
    _   = a
    forall a. Null a => a
    empty

    -- double braces...
    dbraces :: Doc -> Doc
    dbraces :: Doc -> Doc
    dbraces = SpecialCharacters -> Doc -> Doc
    _dbraces SpecialCharacters
    specialCharacters

    -- forall quantifier
    forallQ :: Doc
    forallQ :: Doc
    forallQ = Doc -> Doc
    hlSymbol (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ SpecialCharacters -> Doc
    _forallQ SpecialCharacters
    specialCharacters

    -- left, right, and empty idiom bracket
    leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Doc
    leftIdiomBrkt :: Doc
    leftIdiomBrkt  = SpecialCharacters -> Doc
    _leftIdiomBrkt  SpecialCharacters
    specialCharacters
    rightIdiomBrkt :: Doc
    rightIdiomBrkt = SpecialCharacters -> Doc
    _rightIdiomBrkt SpecialCharacters
    specialCharacters
    emptyIdiomBrkt :: Doc
    emptyIdiomBrkt = SpecialCharacters -> Doc
    _emptyIdiomBrkt SpecialCharacters
    specialCharacters

    arrow, lambda :: Doc
    arrow :: Doc
    arrow  = SpecialCharacters -> Doc
    _arrow SpecialCharacters
    specialCharacters
    lambda :: Doc
    lambda = SpecialCharacters -> Doc
    _lambda SpecialCharacters
    specialCharacters