
   0 | module Data.Regex.DateAndTime
   1 | 
   2 | import TyRE.StringRE
   3 | 
   4 | public export
   5 | record Date where
   6 |     constructor D
   7 |     year : Integer
   8 |     month : Integer
   9 |     day : Integer
  10 | 
  11 | public export
  12 | Show Date where
  13 |     show (D y m d) = show y ++ "-" ++ show m ++ "-" ++ show d
  14 | 
  15 | public export
  16 | record Time where
  17 |     constructor T
  18 |     hours : Integer
  19 |     min : Integer
  20 |     sec : Integer
  21 |     milis : Integer
  22 | 
  23 | public export
  24 | Show Time where
  25 |     show (T h m s ms) = show h ++ ":" ++ show m ++ ":" ++ show s ++ "." ++ show ms
  26 | 
  27 | public export
  28 | record DateTime where
  29 |     constructor DT
  30 |     date : Date
  31 |     time : Time
  32 | 
  33 | public export
  34 | Show DateTime where
  35 |     show (DT d t) = show d ++ "T" ++ show t
  36 | 
  37 | int : Char -> Integer
  38 | int c = cast c - cast '0'
  39 | 
  40 | hourConv : Either (Char, Char) Char -> Integer
  41 | hourConv (Left (t, d)) = 10 * int t + int d
  42 | hourConv (Right d) = 20 + int d
  43 | 
  44 | yearConv : (Integer, Integer, Integer, Integer) -> Integer
  45 | yearConv (th, h, t, d) = 1000 * th + 100 * h + 10 * t + d
  46 | 
  47 | dayConv : Either (Bool, Char) (Char, Char) -> Integer
  48 | dayConv (Left (_, d)) = int d
  49 | dayConv (Right (t, d)) = 10 * int t + int d
  50 | 
  51 | monthConv : Either (Bool, Char) Char -> Integer
  52 | monthConv (Left (_, c)) = int c
  53 | monthConv (Right c) = 10 + int c
  54 | 
  55 | ||| hour regex
  56 | hour : TyRE Integer 
  57 | hour = hourConv `map` r "(([01][0-9])|(2[0-4]))!"
  58 | 
  59 | ||| minutes or seconds regex
  60 | mOrS : TyRE Integer 
  61 | mOrS = (\case(t, d) => 10 * int t + int d) `map` r ":([0-5][0-9])!"
  62 | 
  63 | milis : TyRE Integer
  64 | milis = (\case (h, t, d) => 100 * h + 10 * t + d) `map` match '.' *> digit <*> (digit <*> digit)
  65 | 
  66 | ||| year regex
  67 | year : TyRE Integer
  68 | year = yearConv `map` repTimes 4 digit
  69 | 
  70 | ||| day regex from 01 to 20
  71 | day : TyRE Integer
  72 | day = dayConv `map` r "((0?[1-9])|([12][0-9]))!"
  73 | 
  74 | ||| month regex
  75 | month : TyRE Integer
  76 | month = monthConv `map` r "((0?[1-9])|(1[0-2]))!"
  77 | 
  78 | ||| Date regex pattern: DD/MM/YYYY (24.03.1999)
  79 | export
  80 | date : TyRE Date
  81 | date = 
  82 |     let thirtieth := map   ((withSnd 30) . monthConv)
  83 |                             (r "(30/((0?[13456789])|(1[012])))!")
  84 |         thirtyfirst := map ((withSnd 31) . monthConv)
  85 |                             (r "(31/((0?[13578])|(1[02])))!")
  86 |     in map (\case ((d, m), y) => D y m d) $ 
  87 |             ((((day <* match '/') <*> month) `or` thirtieth) `or` thirtyfirst) 
  88 |                 <*> (match '/' *> year) where
  89 |     withSnd : Integer -> (Integer -> (Integer, Integer))
  90 |     withSnd fst snd = (fst, snd)
  91 | 
  92 | ||| Time regex pattern: 
  93 | |||     HH:mm (22:53)
  94 | |||     HH:mm:ss (22:53:34)
  95 | export
  96 | time : TyRE Time
  97 | time = conv `map` hour <*> (mOrS <*> option mOrS) where
  98 |     conv : (Integer, Integer, Maybe Integer) -> Time
  99 |     conv (h, m, Just s) = T h m s 0
 100 |     conv (h, m, Nothing) = T h m 0 0
 101 | 
 102 | ||| ISO date
 103 | ||| supported patterns:
 104 | |||     YYYY-MM-DD (1999-03-24)
 105 | |||     YYYY-MM-DDTHH:mm (1999-03-24T22:53)
 106 | |||     YYYY-MM-DDTHH:mm:ss (1999-03-24T22:53:34)
 107 | |||     YYYY-MM-DDTHH:mm:ss.sss (1999-03-24T22:53:34.011)
 108 | |||     YYYY-MM-DDTHH:mm:ss.sss(+-)HH:mm (1999-03-24T22:53:34.011+01:00)
 109 | export
 110 | iso : TyRE DateTime
 111 | iso =
 112 |     let thirtieth := ((withFst 30) . monthConv) `map` r "(((0?[13456789])|(1[012]))\\-30)!"
 113 |         thirtyfirst := ((withFst 31) . monthConv) `map` r "(((0?[13578])|(1[02]))\\-31)!"
 114 |         date := map (\case (y, m, d) => D y m d) $
 115 |                     (year <* match '-') <*> 
 116 |                     ((((month <* match '-') <*> day) `or` thirtieth) `or` thirtyfirst)
 117 |         time := convTime `map` hour <*> (mOrS <*> option (mOrS <*> option milis))
 118 |         timeZone := match 'Z' <|> ((match '+' <|> match '-') <*> (hour <*> mOrS))
 119 |     in conv `map` (date <*> option (convTimeWithZone `map` (match 'T' *> time <*> option timeZone))) where
 120 |         withFst : Integer -> (Integer -> (Integer, Integer))
 121 |         withFst snd fst = (fst, snd)
 122 | 
 123 |         convTime : (Integer, Integer, Maybe (Integer, Maybe Integer)) -> Time
 124 |         convTime (h, m, Just (s, Just ms)) = T h m s ms
 125 |         convTime (h, m, Just (s, _)) = T h m s 0
 126 |         convTime (h, m, _) = T h m 0 0
 127 | 
 128 |         convTimeWithZone : (Time, Maybe (Either () ((Either () ()), Integer, Integer))) -> (Time, Maybe Bool)
 129 |         convTimeWithZone (T hr min sec milis, Just (Right (Right _, h, m))) =
 130 |             let totMin := min + m
 131 |                 (minutes, plusHour) := if totMin > 59 then (totMin - 60, 1) else (totMin, 0)
 132 |                 totHr := hr + h + plusHour
 133 |                 (hours, plusDay) := if totHr > 23 then (totHr - 24, Just True) else (totHr, Nothing)
 134 |             in (T hours minutes sec milis, plusDay)
 135 |         convTimeWithZone (T hr min sec milis, Just (Right (Left _, h, m))) =
 136 |             let totMin := min - m
 137 |                 (minutes, minHour) := if totMin < 0 then (totMin + 60, 1) else (totMin, 0)
 138 |                 totHr := hr - h - minHour
 139 |                 (hours, minDay) := if totHr < 0 then (totHr + 24, Just False) else (totHr, Nothing)
 140 |             in (T hours minutes sec milis, minDay)
 141 |         convTimeWithZone (time, _) = (time, Nothing)
 142 | 
 143 |         conv : (Date, Maybe (Time, Maybe Bool)) -> DateTime
 144 |         conv (D y m d, Just (time, Just True)) = 
 145 |             let date :=
 146 |                 if      (d == 30 && (m == 4 || m == 6 || m == 9 || m == 11)) 
 147 |                     ||  (d == 31 && (m == 1 || m == 3 || m == 5 || m == 7 || m == 8 || m == 10))
 148 |                     ||  (m == 2 && 
 149 |                         (   (d == 29 && mod y 4 == 0 && mod y 100 /= 0) 
 150 |                         ||  (d == 28 && (mod y 4 /= 0 || mod y 100 == 0)))) 
 151 |                     then D 1 (m + 1) y 
 152 |                     else if (d == 31 && m == 12) then D 1 1 (y + 1) else D (d + 1) m y
 153 |             in DT date time
 154 |         conv (D y m d, Just (time, Just False)) = 
 155 |             let date := 
 156 |                     if d == 1 
 157 |                         then if m == 1 then D (y - 1) 12 31
 158 |                             else 
 159 |                                 if (m == 5 || m == 7 || m == 10 || m == 12) 
 160 |                                     then D y (m - 1) 31
 161 |                                     else
 162 |                                         if (m == 2 || m == 4 || m == 6 || m == 8 || m == 9 || m == 11)
 163 |                                             then D y (m - 1) 30
 164 |                                             else
 165 |                                                 if (mod y 4 == 0 && mod y 100 /= 0)
 166 |                                                     then D y (m - 1) 29
 167 |                                                     else D y (m - 1) 28
 168 |                         else D y m (d - 1)
 169 |             in DT date time
 170 | 
 171 |         conv (date, Just (time, _)) = DT date time
 172 |         conv (date, _) = DT date (T 0 0 0 0)