0 | module Text.Time.Lexer
  1 |
  2 | import Data.Maybe
  3 | import Data.Time.Time
  4 | import Text.Lex.Manual
  5 |
  6 | public export
  7 | readInt : Integer -> List Char -> Maybe Integer
  8 | readInt n []       = Just n
  9 | readInt n (h :: t) =
 10 |   if isDigit h then readInt (n*10 + cast (digit h)) t else Nothing
 11 |
 12 | public export %inline
 13 | readYear : List Char -> Maybe Year
 14 | readYear cs = readInt 0 cs >>= refineYear
 15 |
 16 | public export %inline
 17 | readMonth : List Char -> Maybe Month
 18 | readMonth cs = readInt 0 cs >>= intToMonth
 19 |
 20 | public export %inline
 21 | readDay : {m : _} -> List Char -> Maybe (Day m)
 22 | readDay cs = readInt 0 cs >>= refineDay {m}
 23 |
 24 | public export %inline
 25 | readHour : List Char -> Maybe Hour
 26 | readHour cs = readInt 0 cs >>= refineHour
 27 |
 28 | public export %inline
 29 | readMinute : List Char -> Maybe Minute
 30 | readMinute cs = readInt 0 cs >>= refineMinute
 31 |
 32 | public export %inline
 33 | readSecond : List Char -> Maybe Second
 34 | readSecond cs = readInt 0 cs >>= refineSecond
 35 |
 36 | --------------------------------------------------------------------------------
 37 | --          Date
 38 | --------------------------------------------------------------------------------
 39 |
 40 | export
 41 | date : StrictTok e Date
 42 | date (y1::y2::y3::y4::'-'::m1::m2::'-'::d1::d2::t) =
 43 |   let Just y := readYear [y1,y2,y3,y4] | Nothing => unknownRange p t
 44 |       Just m := readMonth [m1,m2]      | Nothing => unknownRange p t
 45 |       Just d := readDay {m} [d1,d2]    | Nothing => unknownRange p t
 46 |    in Succ (MkDate y m d) t
 47 | date xs = fail p
 48 |
 49 | --------------------------------------------------------------------------------
 50 | --          LocalTime
 51 | --------------------------------------------------------------------------------
 52 |
 53 | toMS : (digs,cur : Nat) -> Maybe MicroSecond
 54 | toMS 0     cur = refineMicroSecond (cast cur)
 55 | toMS (S k) cur = toMS k (cur * 10)
 56 |
 57 | export
 58 | prec' : Hour -> Minute -> Second -> (digs,cur : Nat) -> SafeTok LocalTime
 59 | prec' h m s digs cur (d::t) = case isDigit d of
 60 |   False => Succ (LT h m s $ toMS digs cur) (d::t)
 61 |   True  =>  case digs of
 62 |     Z   => prec' h m s 0 cur t
 63 |     S k => prec' h m s k (cur * 10 + digit d) t
 64 | prec' h m s digs cur [] = Succ (LT h m s $ toMS digs cur) []
 65 |
 66 | export
 67 | prec : Hour -> Minute -> Second -> AutoTok e LocalTime
 68 | prec h m s ('.'::d::t) =
 69 |   if isDigit d then prec' h m s 5 (digit d) t else unknownRange p t
 70 | prec h m s xs = Succ (LT h m s Nothing) xs
 71 |
 72 | export
 73 | localTime : StrictTok e LocalTime
 74 | localTime (h1::h2::':'::m1::m2::':'::s1::s2::t) =
 75 |   let Just hh := readHour   [h1,h2] | Nothing => unknownRange p t
 76 |       Just mm := readMinute [m1,m2] | Nothing => unknownRange p t
 77 |       Just ss := readSecond [s1,s2] | Nothing => unknownRange p t
 78 |    in prec hh mm ss t
 79 | localTime (h1::h2::':'::m1::m2::t) =
 80 |   let Just hh := readHour   [h1,h2] | Nothing => unknownRange p t
 81 |       Just mm := readMinute [m1,m2] | Nothing => unknownRange p t
 82 |    in prec hh mm 0 t
 83 | localTime xs = fail p
 84 |
 85 | --------------------------------------------------------------------------------
 86 | --          OffsetTime
 87 | --------------------------------------------------------------------------------
 88 |
 89 | sign : Char -> Maybe Sign
 90 | sign '-' = Just Minus
 91 | sign '+' = Just Plus
 92 | sign _   = Nothing
 93 |
 94 | offset : AutoTok e Offset
 95 | offset ('Z'::t) = Succ Z t
 96 | offset ('z'::t) = Succ Z t
 97 | offset (s::h1::h2::':'::m1::m2::t) =
 98 |   let Just ss := sign s | Nothing => unknownRange p t
 99 |       Just hh :=readHour [h1,h2]   | Nothing => unknownRange p t
100 |       Just mm :=readMinute [m1,m2] | Nothing => unknownRange p t
101 |    in Succ (O ss hh mm) t
102 | offset xs = unknownRange p xs
103 |
104 | export
105 | offsetTime : StrictTok e OffsetTime
106 | offsetTime xs =
107 |   let Succ lt ys := localTime xs | Fail s e r => Fail s e r
108 |    in OT lt <$> offset ys
109 |
110 | --------------------------------------------------------------------------------
111 | --          AnyTime
112 | --------------------------------------------------------------------------------
113 |
114 | anyTimeOnly : StrictTok e (Either LocalTime OffsetTime)
115 | anyTimeOnly xs =
116 |   let Succ lt ys := localTime xs  | Fail s e r => Fail s e r
117 |       Succ o  zs := offset {e} ys | Fail {} => Succ (Left lt) ys
118 |    in Succ (Right $ OT lt o) zs
119 |
120 | %inline
121 | addDate : Date -> Either LocalTime OffsetTime -> AnyTime
122 | addDate x = either (ATLocalDateTime . LDT x) (ATOffsetDateTime . ODT x)
123 |
124 | export
125 | anyTime : StrictTok e AnyTime
126 | anyTime xs =
127 |   let Succ dt ys := date {e} xs | Fail {} => ATLocalTime <$> localTime xs
128 |    in case ys of
129 |         'T'::t => addDate dt <$> autoTok anyTimeOnly t
130 |         't'::t => addDate dt <$> autoTok anyTimeOnly t
131 |         ' '::t =>
132 |           let Succ at zs := autoTok anyTimeOnly {e} t
133 |                 | Fail {} => Succ (ATDate dt) (' ' :: t)
134 |            in Succ (addDate dt at) zs
135 |         _      => Succ (ATDate dt) ys
136 |