{-| 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.List
import Agda.Utils.Null
import Agda.Utils.Pretty

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

instance NFData UnicodeOrAscii

{-# 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
"\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
" \x2984"))
  , _lambda :: Doc
_lambda  = Doc
"\x03bb"
  , _arrow :: Doc
_arrow   = Doc
"\x2192"
  , _forallQ :: Doc
_forallQ = Doc
"\x2200"
  , _leftIdiomBrkt :: Doc
_leftIdiomBrkt  = Doc
"\x2987"
  , _rightIdiomBrkt :: Doc
_rightIdiomBrkt = Doc
"\x2988"
  , _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = 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
"\\"
  , _arrow :: Doc
_arrow   = Doc
"->"
  , _forallQ :: Doc
_forallQ = Doc
"forall"
  , _leftIdiomBrkt :: Doc
_leftIdiomBrkt  = Doc
"(|"
  , _rightIdiomBrkt :: Doc
_rightIdiomBrkt = Doc
"|)"
  , _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = 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
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 = 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