0 | module Text.TSV.Encoder
  1 |
  2 | import Data.List
  3 | import Data.String
  4 | import Data.Vect
  5 | import Data.Vect.Quantifiers as VQ
  6 | import Data.List.Quantifiers as LQ
  7 |
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Interface
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| Encodes a multi-field value as a list of strings.
 15 | ||| These can then be written
 16 | ||| to a file, seperated by a tab
 17 | public export
 18 | interface TSVEncoder a where
 19 |   constructor MkTSVEncoder
 20 |   encodeOnto : SnocList String -> a -> SnocList String
 21 |
 22 | --------------------------------------------------------------------------------
 23 | --          Primitives
 24 | --------------------------------------------------------------------------------
 25 |
 26 | export
 27 | TSVEncoder () where encodeOnto sc v = sc :< show v
 28 |
 29 | export
 30 | TSVEncoder Bits8 where encodeOnto sc v = sc :< show v
 31 |
 32 | export
 33 | TSVEncoder Bits16 where encodeOnto sc v = sc :< show v
 34 |
 35 | export
 36 | TSVEncoder Bits32 where encodeOnto sc v = sc :< show v
 37 |
 38 | export
 39 | TSVEncoder Bits64 where encodeOnto sc v = sc :< show v
 40 |
 41 | export
 42 | TSVEncoder Int8 where encodeOnto sc v = sc :< show v
 43 |
 44 | export
 45 | TSVEncoder Int16 where encodeOnto sc v = sc :< show v
 46 |
 47 | export
 48 | TSVEncoder Int32 where encodeOnto sc v = sc :< show v
 49 |
 50 | export
 51 | TSVEncoder Int64 where encodeOnto sc v = sc :< show v
 52 |
 53 | export
 54 | TSVEncoder Int where encodeOnto sc v = sc :< show v
 55 |
 56 | export
 57 | TSVEncoder Integer where encodeOnto sc v = sc :< show v
 58 |
 59 | export
 60 | TSVEncoder Nat where encodeOnto sc v = sc :< show v
 61 |
 62 | export
 63 | TSVEncoder String where encodeOnto sc v = sc :< v
 64 |
 65 | export
 66 | TSVEncoder Double where encodeOnto sc v = sc :< show v
 67 |
 68 | export
 69 | TSVEncoder Bool where encodeOnto sc v = sc :< show v
 70 |
 71 | --------------------------------------------------------------------------------
 72 | --          Derived Encoders
 73 | --------------------------------------------------------------------------------
 74 |
 75 | export
 76 | TSVEncoder a => TSVEncoder (Maybe a) where
 77 |   encodeOnto sc Nothing  = sc :< ""
 78 |   encodeOnto sc (Just v) = encodeOnto sc v
 79 |
 80 | export
 81 | TSVEncoder a => TSVEncoder b => TSVEncoder (a,b) where
 82 |   encodeOnto sc (va, vb) = encodeOnto (encodeOnto sc va) vb
 83 |
 84 | --------------------------------------------------------------------------------
 85 | --          HList and HVect
 86 | --------------------------------------------------------------------------------
 87 |
 88 | encAll :
 89 |      {0 ks : List k}
 90 |   -> {auto _ : All (TSVEncoder . f) ks}
 91 |   -> SnocList String
 92 |   -> All f ks
 93 |   -> SnocList String
 94 | encAll           ss []      = ss
 95 | encAll @{_ :: _} ss (v::vs) = encAll (encodeOnto ss v) vs
 96 |
 97 | encAllV :
 98 |      {0 ks : Vect n k}
 99 |   -> {auto _ : All (TSVEncoder . f) ks}
100 |   -> SnocList String
101 |   -> All f ks
102 |   -> SnocList String
103 | encAllV           ss []      = ss
104 | encAllV @{_ :: _} ss (v::vs) = encAllV (encodeOnto ss v) vs
105 |
106 | export %inline
107 | All (TSVEncoder . f) ks => TSVEncoder (LQ.All.All f ks) where
108 |   encodeOnto sc vs = encAll sc vs
109 |
110 | export %inline
111 | All (TSVEncoder . f) ks => TSVEncoder (VQ.All.All f ks) where
112 |   encodeOnto sc vs = encAllV sc vs
113 |
114 | --------------------------------------------------------------------------------
115 | --          Convertings values to rows and tables
116 | --------------------------------------------------------------------------------
117 |
118 | export
119 | toRow : TSVEncoder a => a -> String
120 | toRow v =
121 |   let ss := encodeOnto [<] v <>> []
122 |    in concat $ intersperse "\t" ss
123 |
124 | export %inline
125 | toTable : TSVEncoder a => List a -> String
126 | toTable = unlines . map toRow
127 |