0 | module Text.TSV.Decoder
  1 |
  2 | import Data.List
  3 | import Data.List.Quantifiers as LQ
  4 | import Data.String
  5 | import Data.Vect
  6 | import Data.Vect.Quantifiers as VQ
  7 | import Text.Lex.Manual.Syntax
  8 | import Text.Parse.Manual
  9 |
 10 | %default total
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          CSV Decoders
 14 | --------------------------------------------------------------------------------
 15 |
 16 | public export
 17 | interface TSVDecoder a where
 18 |   constructor MkTSVDecoder
 19 |   decodeFrom : Tok False e a
 20 |
 21 | str' : SnocList Char -> AutoTok e String
 22 | str' sc [] = Succ (pack $ sc <>> []) []
 23 | str' sc (x :: xs) =
 24 |   if isControl x then Succ (pack $ sc <>> []) (x::xs) else str' (sc :< x) xs
 25 |
 26 | export
 27 | str : Tok False e String
 28 | str []      = Succ "" []
 29 | str (x::xs) = if isControl x then Succ "" (x::xs) else weaken $ str' [<x] xs
 30 |
 31 | export
 32 | refine : Tok b1 e a -> (a -> Maybe b) -> Tok False e b
 33 | refine f g cs = case weaken (f cs) of
 34 |   Succ va cs2 => case g va of
 35 |     Just vb => Succ vb cs2
 36 |     Nothing => unknownRange Same cs2
 37 |   Fail x y z => Fail x y z
 38 |
 39 | export
 40 | refineNum : Tok b1 e a -> (a -> Maybe b) -> Tok False e b
 41 | refineNum f g cs = case weaken (f cs) of
 42 |   Succ va cs2 @{p} => case g va of
 43 |     Just vb => Succ vb cs2
 44 |     Nothing => range (OutOfBounds $ packPrefix p) Same cs2
 45 |   Fail x y z => Fail x y z
 46 |
 47 | export %inline
 48 | natural : (Nat -> Maybe a) -> Tok False e a
 49 | natural = refineNum (tok dec)
 50 |
 51 | export %inline
 52 | boundedNat : Cast Nat a => Nat -> Tok False e a
 53 | boundedNat m = natural $ \x => if x <= m then Just (cast x) else Nothing
 54 |
 55 | export %inline
 56 | integral : (Integer -> Maybe a) -> Tok False e a
 57 | integral = refineNum (tok int)
 58 |
 59 | export %inline
 60 | boundedInt : Cast Integer a => Integer -> Integer -> Tok False e a
 61 | boundedInt l u = integral $ \x =>
 62 |   if x >= l && x <= u then Just (cast x) else Nothing
 63 |
 64 | export %inline
 65 | float : (Double -> Maybe a) -> Tok False e a
 66 | float = refineNum double
 67 |
 68 | export %inline
 69 | TSVDecoder Bits8 where
 70 |   decodeFrom = boundedNat 0xff
 71 |
 72 | export %inline
 73 | TSVDecoder Bits16 where
 74 |   decodeFrom = boundedNat 0xffff
 75 |
 76 | export %inline
 77 | TSVDecoder Bits32 where
 78 |   decodeFrom = boundedNat 0xffff_ffff
 79 |
 80 | export %inline
 81 | TSVDecoder Bits64 where
 82 |   decodeFrom = boundedNat 0xffff_ffff_ffff_ffff
 83 |
 84 | export %inline
 85 | TSVDecoder Int8 where
 86 |   decodeFrom = boundedInt (-0x80) 0x7f
 87 |
 88 | export %inline
 89 | TSVDecoder Int16 where
 90 |   decodeFrom = boundedInt (-0x8000) 0x7fff
 91 |
 92 | export %inline
 93 | TSVDecoder Int32 where
 94 |   decodeFrom = boundedInt (-0x8000_0000) 0x7fff_ffff
 95 |
 96 | export %inline
 97 | TSVDecoder Int64 where
 98 |   decodeFrom = boundedInt (-0x8000_0000_0000_0000) 0x7fff_ffff_ffff_ffff
 99 |
100 | export %inline
101 | TSVDecoder Nat where
102 |   decodeFrom cs = weaken $ dec cs
103 |
104 | export %inline
105 | TSVDecoder Integer where
106 |   decodeFrom cs = weaken $ int cs
107 |
108 | export %inline
109 | TSVDecoder Double where
110 |   decodeFrom cs = weaken $ double cs
111 |
112 | export %inline
113 | TSVDecoder String where
114 |   decodeFrom = str
115 |
116 | export
117 | TSVDecoder Bool where
118 |   decodeFrom = refine str $ \case
119 |     "True"  => Just True
120 |     "False" => Just False
121 |     "true"  => Just True
122 |     "false" => Just False
123 |     _       => Nothing
124 |
125 | --------------------------------------------------------------------------------
126 | --          Derived Decoders
127 | --------------------------------------------------------------------------------
128 |
129 | export
130 | TSVDecoder a => TSVDecoder (Maybe a) where
131 |   decodeFrom [] = Succ Nothing []
132 |   decodeFrom (x :: xs) =
133 |     if isControl x then Succ Nothing (x::xs)
134 |     else Just <$> decodeFrom (x::xs)
135 |
136 | export
137 | TSVDecoder a => TSVDecoder b => TSVDecoder (a,b) where
138 |   decodeFrom = Tok.[| MkPair decodeFrom decodeFrom |]
139 |
140 | --------------------------------------------------------------------------------
141 | --          HList and HVect
142 | --------------------------------------------------------------------------------
143 |
144 | export
145 | tab : Tok False e ()
146 | tab ('\t' :: xs) = Succ () xs
147 | tab (x :: xs)    = single (Expected ["<tab>"] (singleton x)) Same
148 | tab []           = eoiAt Same
149 |
150 | decAll : All (TSVDecoder . f) ks => Tok False e (LQ.All.All f ks)
151 | decAll @{[]}   = pure []
152 | decAll @{[_]}  = \cs => (::[]) <$> decodeFrom cs
153 | decAll @{_::_} = Tok.do
154 |   v  <- decodeFrom
155 |   tab
156 |   vs <- decAll
157 |   pure $ v :: vs
158 |
159 | decAllV : All (TSVDecoder . f) ks => Tok False e (VQ.All.All f ks)
160 | decAllV @{[]}   = pure []
161 | decAllV @{[_]}  = \cs => (::[]) <$> decodeFrom cs
162 | decAllV @{_::_} = Tok.do
163 |   v  <- decodeFrom
164 |   tab
165 |   vs <- decAllV
166 |   pure $ v :: vs
167 |
168 | export %inline
169 | All (TSVDecoder . f) ks => TSVDecoder (LQ.All.All f ks) where
170 |   decodeFrom = decAll
171 |
172 | export %inline
173 | All (TSVDecoder . f) ks => TSVDecoder (VQ.All.All f ks) where
174 |   decodeFrom = decAllV
175 |
176 | --------------------------------------------------------------------------------
177 | --          Decoding Tables
178 | --------------------------------------------------------------------------------
179 |
180 | readTable' :
181 |      {auto _ : TSVDecoder a}
182 |   -> SnocList a
183 |   -> Position
184 |   -> (cs : List Char)
185 |   -> (0 acc : SuffixAcc cs)
186 |   -> Either (Bounded $ InnerError e) (List a)
187 | readTable' sx pos []              _      = Right (sx <>> [])
188 | readTable' sx pos xs              (SA r) = case decodeFrom {a} xs of
189 |   Succ v xs2 @{p} => case xs2 of
190 |     []               => Right (sx <>> [v])
191 |     '\n' ::       t2 => readTable' (sx :< v) (incLine pos) t2 r
192 |     '\r'::'\n' :: t2 => readTable' (sx :< v) (incLine pos) t2 r
193 |     c :: _           =>
194 |       let bs := Bounds.oneChar (move pos p)
195 |        in if isControl c then Left $ B (InvalidControl c) bs
196 |           else unexpected (B (show c) bs)
197 |   Fail x y z => Left (boundedErr pos x y z)
198 |
199 | export
200 | readTable :
201 |      {auto _ : TSVDecoder a}
202 |   -> Origin
203 |   -> String
204 |   -> Either (ParseError e) (List a)
205 | readTable o s =
206 |   mapFst (toParseError o s) (readTable' [<] begin (unpack s) suffixAcc)
207 |