1{-| Choice of Unicode or ASCII glyphs.
2-}
3module Agda.Syntax.Concrete.Glyph
4  ( UnicodeOrAscii(..)
5  , unsafeSetUnicodeOrAscii
6  , specialCharactersForGlyphs
7  , braces', dbraces
8  , forallQ
9  , leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt
10  , arrow, lambda
11  , SpecialCharacters(..)
12  ) where
13
14import Control.DeepSeq
15
16import Data.IORef (IORef, newIORef, readIORef, writeIORef)
17import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)
18
19import GHC.Generics (Generic)
20
21import Agda.Utils.List
22import Agda.Utils.Null
23import Agda.Utils.Pretty
24
25-- | We want to know whether we are allowed to insert unicode characters or not.
26data UnicodeOrAscii
27  = UnicodeOk
28  | AsciiOnly
29  deriving (Show, Eq, Enum, Bounded, Generic)
30
31instance NFData UnicodeOrAscii
32
33{-# NOINLINE unsafeUnicodeOrAsciiIORef #-}
34unsafeUnicodeOrAsciiIORef :: IORef UnicodeOrAscii
35unsafeUnicodeOrAsciiIORef = UNSAFE.unsafePerformIO $ newIORef UnicodeOk
36
37{-# NOINLINE unsafeSetUnicodeOrAscii #-}
38unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()
39unsafeSetUnicodeOrAscii = writeIORef unsafeUnicodeOrAsciiIORef
40
41-- | Are we allowed to use unicode supscript characters?
42unsafeUnicodeOrAscii :: UnicodeOrAscii
43unsafeUnicodeOrAscii = UNSAFE.unsafePerformIO (readIORef unsafeUnicodeOrAsciiIORef)
44
45-- | Picking the appropriate set of special characters depending on
46-- whether we are allowed to use unicode or have to limit ourselves
47-- to ascii.
48
49data SpecialCharacters = SpecialCharacters
50  { _dbraces :: Doc -> Doc
51  , _lambda  :: Doc
52  , _arrow   :: Doc
53  , _forallQ :: Doc
54  , _leftIdiomBrkt  :: Doc
55  , _rightIdiomBrkt :: Doc
56  , _emptyIdiomBrkt :: Doc
57  }
58
59specialCharactersUnicode :: SpecialCharacters
60specialCharactersUnicode = SpecialCharacters
61  { _dbraces = (("\x2983 " <>) . (<> " \x2984"))
62  , _lambda  = "\x03bb"
63  , _arrow   = "\x2192"
64  , _forallQ = "\x2200"
65  , _leftIdiomBrkt  = "\x2987"
66  , _rightIdiomBrkt = "\x2988"
67  , _emptyIdiomBrkt = "\x2987\x2988"
68  }
69
70specialCharactersAscii :: SpecialCharacters
71specialCharactersAscii = SpecialCharacters
72  { _dbraces = braces . braces'
73  , _lambda  = "\\"
74  , _arrow   = "->"
75  , _forallQ = "forall"
76  , _leftIdiomBrkt  = "(|"
77  , _rightIdiomBrkt = "|)"
78  , _emptyIdiomBrkt = "(|)"
79  }
80
81-- | Return the glyph set based on a given (unicode or ascii) glyph mode
82specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters
83specialCharactersForGlyphs UnicodeOk = specialCharactersUnicode
84specialCharactersForGlyphs AsciiOnly = specialCharactersAscii
85
86-- | Choose the glyph set based on the unsafe IORef.
87{-# NOINLINE specialCharacters #-}
88specialCharacters :: SpecialCharacters
89specialCharacters = specialCharactersForGlyphs unsafeUnicodeOrAscii
90
91braces' :: Doc -> Doc
92braces' d = caseList (render d) (braces d) {-else-} $ \ c cs ->
93  braces (spaceIfDash c <> d <> spaceIfDash (last1 c cs))
94  -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
95  -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
96  where
97  spaceIfDash '-' = " "
98  spaceIfDash _   = empty
99
100-- double braces...
101dbraces :: Doc -> Doc
102dbraces = _dbraces specialCharacters
103
104-- forall quantifier
105forallQ :: Doc
106forallQ = _forallQ specialCharacters
107
108-- left, right, and empty idiom bracket
109leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Doc
110leftIdiomBrkt  = _leftIdiomBrkt  specialCharacters
111rightIdiomBrkt = _rightIdiomBrkt specialCharacters
112emptyIdiomBrkt = _emptyIdiomBrkt specialCharacters
113
114arrow, lambda :: Doc
115arrow  = _arrow specialCharacters
116lambda = _lambda specialCharacters
117