
   0 | module IotaTime.Locale
   1 | 
   2 | import Data.Vect
   3 | import IotaTime.Locale.Unix.Platform
   4 | import IotaTime.Locale.Windows.Platform
   5 | import System
   6 | import System.Info
   7 | import Derive.Prelude
   8 | 
   9 | %language ElabReflection
  10 | 
  11 | %default total
  12 | 
  13 | ||| Locale data used by Gregorian date and local-time patterns.
  14 | |||
  15 | ||| Values are acquired from the operating system or supplied by the built-in
  16 | ||| locales. The representation is hidden so all name tables retain their sizes.
  17 | export
  18 | record Locale where
  19 |   constructor MkLocale
  20 |   storedLocaleId : String
  21 |   storedMonthNames : Vect 12 String
  22 |   storedMonthNamesShort : Vect 12 String
  23 |   storedDayNames : Vect 7 String
  24 |   storedDayNamesShort : Vect 7 String
  25 |   storedAmName : String
  26 |   storedPmName : String
  27 |   storedRawDateFormat : String
  28 |   storedRawTimeFormat : String
  29 |   storedRawDateTimeFormat : String
  30 | 
  31 | ||| The operating-system identifier or stable identifier of a locale.
  32 | public export
  33 | localeId : Locale -> String
  34 | localeId = storedLocaleId
  35 | 
  36 | ||| Full Gregorian month names ordered January through December.
  37 | public export
  38 | monthNames : Locale -> Vect 12 String
  39 | monthNames = storedMonthNames
  40 | 
  41 | ||| Abbreviated Gregorian month names ordered January through December.
  42 | public export
  43 | monthNamesShort : Locale -> Vect 12 String
  44 | monthNamesShort = storedMonthNamesShort
  45 | 
  46 | ||| Full weekday names ordered Sunday through Saturday.
  47 | public export
  48 | dayNames : Locale -> Vect 7 String
  49 | dayNames = storedDayNames
  50 | 
  51 | ||| Abbreviated weekday names ordered Sunday through Saturday.
  52 | public export
  53 | dayNamesShort : Locale -> Vect 7 String
  54 | dayNamesShort = storedDayNamesShort
  55 | 
  56 | ||| The locale's ante-meridiem designator, which may be empty.
  57 | public export
  58 | amName : Locale -> String
  59 | amName = storedAmName
  60 | 
  61 | ||| The locale's post-meridiem designator, which may be empty.
  62 | public export
  63 | pmName : Locale -> String
  64 | pmName = storedPmName
  65 | 
  66 | export
  67 | rawDateFormat : Locale -> String
  68 | rawDateFormat = storedRawDateFormat
  69 | 
  70 | export
  71 | rawTimeFormat : Locale -> String
  72 | rawTimeFormat = storedRawTimeFormat
  73 | 
  74 | export
  75 | rawDateTimeFormat : Locale -> String
  76 | rawDateTimeFormat = storedRawDateTimeFormat
  77 | 
  78 | %runElab derive `{Locale} [Eq]
  79 | 
  80 | public export
  81 | Show Locale where
  82 |   show value = "<Locale " ++ show value.storedLocaleId ++ ">"
  83 | 
  84 | ||| A failure to acquire locale data from the operating system.
  85 | public export
  86 | data LocaleError
  87 |   = LocaleNotFound String
  88 |   | LocalePlatformError String
  89 | 
  90 | public export
  91 | Eq LocaleError where
  92 |   LocaleNotFound left == LocaleNotFound right = left == right
  93 |   LocalePlatformError left == LocalePlatformError right = left == right
  94 |   _ == _ = False
  95 | 
  96 | public export
  97 | Show LocaleError where
  98 |   show (LocaleNotFound name) = "locale is not installed: " ++ name
  99 |   show (LocalePlatformError message) = message
 100 | 
 101 | fromUnixData : String -> UnixLocaleData -> Locale
 102 | fromUnixData valueId localeData = MkLocale
 103 |   valueId
 104 |   (localeMonthNames localeData)
 105 |   (localeMonthNamesShort localeData)
 106 |   (localeDayNames localeData)
 107 |   (localeDayNamesShort localeData)
 108 |   (localeAmName localeData)
 109 |   (localePmName localeData)
 110 |   (localeDateFormat localeData)
 111 |   (localeTimeFormat localeData)
 112 |   (localeDateTimeFormat localeData)
 113 | 
 114 | unixLocaleByName : String -> IO (Either LocaleError Locale)
 115 | unixLocaleByName name = do
 116 |   loaded <- loadUnixLocaleData name
 117 |   pure (case loaded of
 118 |     Nothing => Left (LocaleNotFound name)
 119 |     Just localeData => Right (fromUnixData name localeData))
 120 | 
 121 | currentLocaleId : IO String
 122 | currentLocaleId = do
 123 |   all <- getEnv "LC_ALL"
 124 |   time <- getEnv "LC_TIME"
 125 |   language <- getEnv "LANG"
 126 |   pure (firstPresent [all, time, language])
 127 |   where
 128 |     firstPresent : List (Maybe String) -> String
 129 |     firstPresent [] = "C"
 130 |     firstPresent (Nothing :: rest) = firstPresent rest
 131 |     firstPresent (Just "" :: rest) = firstPresent rest
 132 |     firstPresent (Just value :: rest) = value
 133 | 
 134 | unixCurrentLocale : IO (Either LocaleError Locale)
 135 | unixCurrentLocale = do
 136 |   valueId <- currentLocaleId
 137 |   loaded <- loadUnixLocaleData ""
 138 |   case loaded of
 139 |     Just localeData => pure (Right (fromUnixData valueId localeData))
 140 |     Nothing => do
 141 |       fallback <- loadUnixLocaleData "C"
 142 |       pure (case fallback of
 143 |         Just localeData => Right (fromUnixData "C" localeData)
 144 |         Nothing => Left (LocalePlatformError
 145 |           "native Unix locale access could not load the POSIX C locale"))
 146 | 
 147 | fromWindowsData : WindowsLocaleData -> Locale
 148 | fromWindowsData localeData =
 149 |   let dateFormat = IotaTime.Locale.Windows.Platform.localeDateFormat localeData
 150 |       timeFormat = IotaTime.Locale.Windows.Platform.localeTimeFormat localeData
 151 |    in MkLocale
 152 |         (localeIdentifier localeData)
 153 |         (IotaTime.Locale.Windows.Platform.localeMonthNames localeData)
 154 |         (IotaTime.Locale.Windows.Platform.localeMonthNamesShort localeData)
 155 |         (IotaTime.Locale.Windows.Platform.localeDayNames localeData)
 156 |         (IotaTime.Locale.Windows.Platform.localeDayNamesShort localeData)
 157 |         (IotaTime.Locale.Windows.Platform.localeAmName localeData)
 158 |         (IotaTime.Locale.Windows.Platform.localePmName localeData)
 159 |         dateFormat
 160 |         timeFormat
 161 |         (dateFormat ++ " " ++ timeFormat)
 162 | 
 163 | windowsLocaleByName : String -> IO (Either LocaleError Locale)
 164 | windowsLocaleByName name = do
 165 |   loaded <- loadWindowsLocaleData False name
 166 |   pure (case loaded of
 167 |     Nothing => Left (LocaleNotFound name)
 168 |     Just localeData => Right (fromWindowsData localeData))
 169 | 
 170 | windowsCurrentLocale : IO (Either LocaleError Locale)
 171 | windowsCurrentLocale = do
 172 |   loaded <- loadWindowsLocaleData True ""
 173 |   pure (case loaded of
 174 |     Nothing => Left (LocalePlatformError
 175 |       "native Windows locale access could not load the user locale")
 176 |     Just localeData => Right (fromWindowsData localeData))
 177 | 
 178 | ||| Read a named locale from the operating system locale database.
 179 | public export
 180 | localeByName : String -> IO (Either LocaleError Locale)
 181 | localeByName name = if isWindows
 182 |   then windowsLocaleByName name
 183 |   else unixLocaleByName name
 184 | 
 185 | ||| Read the locale selected by LC_ALL, LC_TIME, or LANG.
 186 | public export
 187 | currentLocale : IO (Either LocaleError Locale)
 188 | currentLocale = if isWindows
 189 |   then windowsCurrentLocale
 190 |   else unixCurrentLocale
 191 | 
 192 | ||| Built-in United States English locale data.
 193 | public export
 194 | enUS : Locale
 195 | enUS = MkLocale
 196 |   "en_US"
 197 |   [ "January", "February", "March", "April", "May", "June"
 198 |   , "July", "August", "September", "October", "November", "December"
 199 |   ]
 200 |   [ "Jan", "Feb", "Mar", "Apr", "May", "Jun"
 201 |   , "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
 202 |   ]
 203 |   [ "Sunday", "Monday", "Tuesday", "Wednesday", "Thursday", "Friday"
 204 |   , "Saturday"
 205 |   ]
 206 |   [ "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat" ]
 207 |   "AM"
 208 |   "PM"
 209 |   "%m/%d/%Y"
 210 |   "%r"
 211 |   "%a %d %b %Y %r %Z"
 212 | 
 213 | ||| Built-in German locale data for Germany.
 214 | public export
 215 | deDE : Locale
 216 | deDE = MkLocale
 217 |   "de_DE"
 218 |   [ "Januar", "Februar", "März", "April", "Mai", "Juni"
 219 |   , "Juli", "August", "September", "Oktober", "November", "Dezember"
 220 |   ]
 221 |   [ "Jan", "Feb", "Mär", "Apr", "Mai", "Jun"
 222 |   , "Jul", "Aug", "Sep", "Okt", "Nov", "Dez"
 223 |   ]
 224 |   [ "Sonntag", "Montag", "Dienstag", "Mittwoch", "Donnerstag", "Freitag"
 225 |   , "Samstag"
 226 |   ]
 227 |   [ "So", "Mo", "Di", "Mi", "Do", "Fr", "Sa" ]
 228 |   ""
 229 |   ""
 230 |   "%d.%m.%Y"
 231 |   "%T"
 232 |   "%a %d %b %Y %T %Z"
 233 | 
 234 | ||| Built-in Japanese locale data for Japan.
 235 | public export
 236 | jaJP : Locale
 237 | jaJP = MkLocale
 238 |   "ja_JP"
 239 |   [ "1月", "2月", "3月", "4月", "5月", "6月"
 240 |   , "7月", "8月", "9月", "10月", "11月", "12月"
 241 |   ]
 242 |   [ "1月", "2月", "3月", "4月", "5月", "6月"
 243 |   , "7月", "8月", "9月", "10月", "11月", "12月"
 244 |   ]
 245 |   [ "日曜日", "月曜日", "火曜日", "水曜日", "木曜日", "金曜日", "土曜日" ]
 246 |   [ "日", "月", "火", "水", "木", "金", "土" ]
 247 |   "午前"
 248 |   "午後"
 249 |   "%Y年%m月%d日"
 250 |   "%H時%M分%S秒"
 251 |   "%Y年%m月%d日 %H時%M分%S秒"
 252 |