src/hdr.bend

bend-toon-codec@0.1.0.0 · 165 lines · 26 definitions

1import Base
2import bend-toon-codec@0.1.0.0/src/num.bend as N
3import bend-toon-codec@0.1.0.0/src/head.bend as Hd
4import bend-toon-codec@0.1.0.0/src/text.bend as T
5import bend-toon-codec@0.1.0.0/src/split.bend as S
6import bend-toon-codec@0.1.0.0/src/prim.bend as P
7
8# Array headers (spec section 6): `[N]`, `[N|]`, `[N<TAB>]`, optional
9# `{f1,f2}`, then the colon. `parse` takes the text starting at `[`.
10
11# length, delimiter as a code point, field names (empty: not tabular), and the
12# text after the colon.
13type Hdr is Data:
14  Hdr{n: U32, d: U32, fields: List<&2, String>, rest: String}
15
16def empty() -> Hdr:
17  Hdr{0, 44, Nil{}, SNil{}}
18
19def bad(+m: String) -> Result<&2, &2, String, Hdr>:
20  Fail{m}
21
22# A field name: quoted names are unescaped; a bare name that holds another
23# delimiter than the active one is a delimiter mismatch.
24# A quoted field name keeps its marker (see head.bend).
25def mark.name(+r: Result<&2, &2, String, String>) -> Result<&2, &2, String, String>:
26  match r:
27    case Done{k}:
28      Done{Hd.mark() ++ k}
29    case Fail{e}:
30      Fail{e}
31
32def name.ok(+bare: Bool, +bad_delim: Bool, +tok: String) -> Result<&2, &2, String, String>:
33  match bare bad_delim:
34    case True{} True{}:
35      Fail{"header delimiter mismatch"}
36    case True{} False{}:
37      Done{tok}
38    case False{} _:
39      mark.name(P.key(tok))
40
41def other_delim(+c: U32, +d: U32) -> Bool:
42  (U32.is_eq(c, 44) || U32.is_eq(c, 9) || U32.is_eq(c, 124)) && Bool.not(U32.is_eq(c, d))
43
44def has_other(+s: String, +d: U32) -> Bool:
45  match s:
46    case SNil{}:
47      False{}
48    case SCon{Chr{c}, t}:
49      other_delim(c, d) || has_other(t, d)
50
51def not_quoted(+s: String) -> Bool:
52  Bool.not(Hd.lead(s, 34))
53
54def name(+d: U32, +tok: String) -> Result<&2, &2, String, String>:
55  name.ok(not_quoted(tok), has_other(tok, d), tok)
56
57def names.cons(+r: Result<&2, &2, String, String>, +rest: Result<&2, &2, String, List<&2, String>>) -> Result<&2, &2, String, List<&2, String>>:
58  match r rest:
59    case Done{n} Done{ns}:
60      Done{Con{n, ns}}
61    case Fail{e} _:
62      Fail{e}
63    case _ Fail{e}:
64      Fail{e}
65
66def names(+d: U32, +toks: List<&2, String>) -> Result<&2, &2, String, List<&2, String>>:
67  match toks:
68    case Nil{}:
69      Done{Nil{}}
70    case Con{t, rest}:
71      names.cons(name(d, String.trim(t)), names(d, rest))
72
73def fields.done(+n: U32, +d: U32, +rest: String, +r: Result<&2, &2, String, List<&2, String>>) -> Result<&2, &2, String, Hdr>:
74  match r:
75    case Fail{e}:
76      Fail{e}
77    case Done{ks}:
78      Done{Hdr{n, d, ks, rest}}
79
80def fields.after.pick(+colon: Bool, +n: U32, +d: U32, +inner: String, +s: String) -> Result<&2, &2, String, Hdr>:
81  match colon:
82    case True{}:
83      fields.done(n, d, Hd.drop(s), names(d, S.split(inner, d)))
84    case False{}:
85      bad("expected : after the field list")
86
87# After `}`: the colon follows at once.
88def fields.after(+n: U32, +d: U32, +inner: String, +s: String) -> Result<&2, &2, String, Hdr>:
89  fields.after.pick(Hd.lead(s, 58), n, d, inner, s)
90
91def fields.cut.if(+missing: Bool, +n: U32, +d: U32, +s: String, +i: U32) -> Result<&2, &2, String, Hdr>:
92  match missing:
93    case True{}:
94      bad("unterminated field list")
95    case False{}:
96      fields.after(n, d, String.take(s, U32.to_nat(i)), String.drop(s, U32.to_nat((i + 1 : U32))))
97
98def fields.cut(+n: U32, +d: U32, +s: String, +i: U32) -> Result<&2, &2, String, Hdr>:
99  fields.cut.if(U32.is_eq(i, S.none()), n, d, s, i)
100
101def after.pick(+colon: Bool, +brace: Bool, +n: U32, +d: U32, +s: String) -> Result<&2, &2, String, Hdr>:
102  match colon brace:
103    case True{} _:
104      Done{Hdr{n, d, Nil{}, Hd.drop(s)}}
105    case False{} True{}:
106      fields.cut(n, d, Hd.drop(s), S.find_unq(Hd.drop(s), 125, 0, 0))
107    case False{} False{}:
108      bad("expected : or a field list after the length")
109
110# After `]`: the colon, or a field list.
111def after(+n: U32, +d: U32, +s: String) -> Result<&2, &2, String, Hdr>:
112  after.pick(Hd.lead(s, 58), Hd.lead(s, 123), n, d, s)
113
114def delim.pick(+tab: Bool, +pipe: Bool, +comma: Bool, +n: U32, +s: String) -> Result<&2, &2, String, Hdr>:
115  match tab pipe comma:
116    case True{} _ _:
117      after(n, 9, Hd.drop(Hd.drop(s)))
118    case False{} True{} _:
119      after(n, 124, Hd.drop(Hd.drop(s)))
120    case False{} False{} True{}:
121      after(n, 44, Hd.drop(s))
122    case False{} False{} False{}:
123      bad("invalid array length")
124
125# The delimiter symbol, then `]`.
126def delim(+n: U32, +s: String) -> Result<&2, &2, String, Hdr>:
127  delim.pick(Hd.lead2(s, 9, 93), Hd.lead2(s, 124, 93), Hd.lead(s, 93), n, s)
128
129def len.pick(+ok: Bool, +n: Maybe<&2, U32>, +rest: String) -> Result<&2, &2, String, Hdr>:
130  match ok n:
131    case True{} Some{v}:
132      delim(v, rest)
133    case _ _:
134      bad("invalid array length")
135
136def len.ok.pick(+empty: Bool, +zero: Bool, +lead0: Bool, +ds: String) -> Bool:
137  match empty zero lead0:
138    case True{} _ _:
139      False{}
140    case False{} True{} _:
141      True{}
142    case False{} False{} True{}:
143      False{}
144    case False{} False{} False{}:
145      Nat.is_le(String.length(ds), 9n)
146
147# A length is `0` or digits without a leading zero, at most nine of them.
148def len.ok(+ds: String) -> Bool:
149  len.ok.pick(String.is_empty(ds), String.eq(ds, "0"), Hd.lead(ds, 48), ds)
150
151def len(+r: N.Sp) -> Result<&2, &2, String, Hdr>:
152  match r:
153    case N.Sp{ds, rest}:
154      len.pick(len.ok(ds), U32.read(ds), rest)
155
156def parse.pick(+open: Bool, +s: String) -> Result<&2, &2, String, Hdr>:
157  match open:
158    case True{}:
159      len(N.span_digits(Hd.drop(s)))
160    case False{}:
161      bad("expected [")
162
163# Parse a header from its `[`.
164def parse(+s: String) -> Result<&2, &2, String, Hdr>:
165  parse.pick(Hd.lead(s, 91), s)