toml.bend source
toml.bend on the hub · documented module
# eztoml/toml: the slice of TOML for string-valued sectioned docs. A line is# blank, a comment, a `[section]` header, or a `key = "value"` pair. A header is# a dotted path whose segments may be quoted, and a key may be quoted, so a file# path can be one. No arrays, no inline tables, no numbers, because every value# is a string.import Base# a key and the string written for ittype Kv is Data: Kv{key: String, val: String}# a section header and the pairs under it, in the order they were writtentype Sect is Data: Sect{name: String, pairs: List<&2, Kv>}# what one line turned out to betype Line is Data: LSkip{} LHead{name: String} LPair{key: String, val: String} LBad{why: String}# a trim in progress: `skip` is true until the first non-space, `out` is the# chars kept so far, reversedtype Trim is Data: Trim{skip: Bool, out: List<&2, Char>}# the sections read so far, and the first error if there was one. name is the# section being filled, "" before any header; pairs and done are reversed.type Toml is Data: Toml{bad: String, name: String, pairs: List<&2, Kv>, done: List<&2, Sect>}# while skipping, a space is dropped and the skipping goes on; the first other# char is kept and ends itdef trim.keep.go(sp: Bool, c: Char, out: List<&2, Char>) -> Trim: match sp: case True{}: Trim{True{}, out} case False{}: Trim{False{}, c <> out}# a char offered to a trim that is still skipping. `+c` because the char is both# asked about and kept; a fold's step may not take one, so it is split out here.def trim.keep(+c: Char, out: List<&2, Char>) -> Trim: trim.keep.go(Char.is_space(c), c, out)# one char of a trim: `skip` stays true until a non-space arrivesdef trim.step(st: Trim, c: Char) -> Trim: Trim{skip, out} = st match skip: case True{}: trim.keep(c, out) case False{}: Trim{False{}, c <> out}# the chars a finished trim collected. A destructure needs a parameter, never a# local binder, so the fold's result comes in through one.def trim.out(st: Trim) -> List<&2, Char>: Trim{_skip, out} = st out# the walk one char at a time. Base's `List.foldl` applies an erased function# parameter, which puts it outside Bend's termination check and costs every# proof downstream an unsafe annotation; a walk written out is structural and# costs nothing.def trim.walk(cs: List<&2, Char>, st: Trim) -> Trim: match cs: case []: st case h <> t: trim.walk(t, trim.step(st, h))# the chars with leading spaces dropped, reverseddef trim.pass(cs: List<&2, Char>) -> List<&2, Char>: trim.out(trim.walk(cs, Trim{True{}, []}))# the string with no leading or trailing spaces. Two passes: the first reverses# and drops what led, the second drops what trailed and puts it back in order.def trim(s: String) -> String: String.from_list(trim.pass(trim.pass(String.to_list(s))))# drops one leading char when it is the one givendef strip.cut(hit: Bool, h: Char, t: List<&2, Char>) -> List<&2, Char>: match hit: case True{}: t case False{}: h <> t# the chars without one leading `c`, if there is onedef strip.front(cs: List<&2, Char>, c: Char) -> List<&2, Char>: match cs: case []: [] case +h <> t: strip.cut(Char.is_eq(h, c), h, t)# the chars from one already taken off the front, without one trailing `c`.# The list is the first argument because that is the one the walk shrinks.def strip.back.go(t: List<&2, Char>, +h: Char, +c: Char) -> List<&2, Char>: match t: case []: strip.cut(Char.is_eq(h, c), h, []) case +h2 <> t2: h <> strip.back.go(t2, h2, c)# the chars without one trailing `c`, if there is one. Walking to the end is# what a reverse, a cut and a reverse back did before; it is one pass rather# than three, and the end of a list is a case a proof can reach.def strip.back(cs: List<&2, Char>, +c: Char) -> List<&2, Char>: match cs: case []: [] case +h <> t: strip.back.go(t, h, c)# the string without one leading `a` and one trailing `b`def strip(s: String, a: Char, b: Char) -> String: String.from_list(strip.back(strip.front(String.to_list(s), a), b))# a pair line, once it is known to hold an `=`: the key is what precedes the# first one, the value everything after, so an `=` inside a value survivesdef pair_of(parts: List<&2, String>) -> Line: match parts: case []: LBad{"an empty line cannot be a pair"} case h <> t: LPair{strip(trim(h), '"', '"'), strip(trim(String.join(t, "=")), '"', '"')}# a header line, once it is known to start with `[`def head_of(+s: String, shut: Bool) -> Line: match shut: case True{}: LHead{strip(s, '[', ']')} case False{}: LBad{s ++ " is not a section header"}# the last question: a line holding an `=` is a pair, and a line holding none# is neither of the two things a manifest may say. `String.split` is the cost# here, and it is paid only by a line that really is a pair.def line_of.pair(here: Bool, +s: String) -> Line: match here: case True{}: pair_of(String.split(s, '=')) case False{}: LBad{s ++ " is neither a section header nor a key"}# the section header decided, and the pair question asked only underneath itdef line_of.head(here: Bool, +s: String) -> Line: match here: case True{}: head_of(s, String.ends_with(s, "]")) case False{}: line_of.pair(String.contains(s, "="), s)# a comment, which may hold anything and so is answered before anything is# read out of the linedef line_of.comment(here: Bool, +s: String) -> Line: match here: case True{}: LSkip{} case False{}: line_of.head(String.starts_with(s, "["), s)# a blank line, which is the first question because an empty string starts# with nothing and holds nothing, and so would fall all the way through to# being called neither a header nor a keydef line_of.blank(here: Bool, +s: String) -> Line: match here: case True{}: LSkip{} case False{}: line_of.comment(String.starts_with(s, "#"), s)# what a trimmed line is. The order matters: a comment may hold anything.## The cascade is four `match` arms rather than four nested `Bool.pick`s# because `Bool.pick` is an ordinary function: every arm of the nest was built# before any condition was consulted, so `head_of` and `String.split` ran for# every blank line and every comment line of every manifest and lockfile ez# reads. A lock with fifty packages is several hundred lines and each was# parsed two or three times over.def line_of(+s: String) -> Line: line_of.blank(String.is_empty(s), s)# the first error wins, so a later one is droppeddef first(+bad: String, why: String) -> String: Bool.pick(String, String.is_empty(bad), why, bad)# the section being filled, moved into the finished ones. A header with no pairs# is still a section; only the "" before the first header is not.def flush.put(empty: Bool, name: String, pairs: List<&2, Kv>, done: List<&2, Sect>) -> List<&2, Sect>: match empty: case True{}: done case False{}: Sect{name, List.reverse(&2, Kv, pairs)} <> done# the section being filled, moved into the finished onesdef flush(+name: String, pairs: List<&2, Kv>, done: List<&2, Sect>) -> List<&2, Sect>: flush.put(String.is_empty(name), name, pairs, done)# a pair belongs to the section being filled, and is an error before the first# headerdef put.go(loose: Bool, bad: String, name: String, pairs: List<&2, Kv>, done: List<&2, Sect>, +key: String, val: String) -> Toml: match loose: case True{}: Toml{first(bad, key ++ " = is outside any section"), name, pairs, done} case False{}: Toml{bad, name, Kv{key, val} <> pairs, done}# a pair belongs to the section being filled, and is an error before the first# headerdef put(st: Toml, key: String, val: String) -> Toml: Toml{bad, +name, pairs, done} = st put.go(String.is_empty(name), bad, name, pairs, done, key, val)# the state once a line has been classifieddef step.go(st: Toml, line: Line) -> Toml: Toml{bad, name, pairs, done} = st match line: case LSkip{}: Toml{bad, name, pairs, done} case LHead{next}: Toml{bad, next, [], flush(name, pairs, done)} case LPair{key, val}: put(Toml{bad, name, pairs, done}, key, val) case LBad{why}: Toml{first(bad, why), name, pairs, done}# one line against the statedef step(st: Toml, raw: String) -> Toml: step.go(st, line_of(trim(raw)))# the last section flushed, and the finished ones put back in orderdef parse.fin(r: Toml) -> Toml: Toml{bad, name, pairs, done} = r Toml{bad, "", [], List.reverse(&2, Sect, flush(name, pairs, done))}# the walk one line at a time, written out rather than foldeddef parse.walk(ls: List<&2, String>, st: Toml) -> Toml: match ls: case []: st case h <> t: parse.walk(t, step(st, h))# the sections of a document, and the first error if there was onedef parse(text: String) -> Toml: parse.fin(parse.walk(String.lines(text), Toml{"", "", [], []}))# this pair's value when the key matches, otherwise whatever the rest of the# table gavedef value.at(kv: Kv, rest: String, key: String) -> String: Kv{k, v} = kv Bool.pick(String, String.eq(k, key), v, rest)# the value written for a key in a table, or "" when it is absent. The scan# recurses first and picks after, so no recursive call hides inside a branch.def value(pairs: List<&2, Kv>, +key: String) -> String: match pairs: case []: "" case h <> t: value.at(h, value(t, key), key)# the sections a parse found, in the order they were writtendef sects(t: Toml) -> List<&2, Sect>: Toml{_bad, _name, _pairs, done} = t done# what a header's next character is: the quoting toggles, an unquoted dot cuts,# anything else is kepttype Sym is Data: SQuote{} SDot{} SKeep{c: Char}# a header char classified. `+c` because it is both asked about and kept.def seg.sym(+c: Char) -> Sym: Bool.pick(Sym, Char.is_eq(c, '"'), SQuote{}, Bool.pick(Sym, Char.is_eq(c, '.'), SDot{}, SKeep{c}))# a header being cut apart: `quoted` is true inside quotes, `cur` is the segment# being gathered and `out` the finished ones, both reversedtype Split is Data: Split{quoted: Bool, cur: List<&2, Char>, out: List<&2, String>}# the segment gathered so far, in orderdef seg.done(cur: List<&2, Char>) -> String: String.from_list(List.reverse(&2, Char, cur))# a dot inside quotes is part of the segment; outside, it ends onedef seg.dot(quoted: Bool, cur: List<&2, Char>, out: List<&2, String>) -> Split: match quoted: case True{}: Split{True{}, '.' <> cur, out} case False{}: Split{False{}, [], seg.done(cur) <> out}# the state once a char has been classifieddef seg.go(st: Split, s: Sym) -> Split: Split{quoted, cur, out} = st match s: case SQuote{}: Split{Bool.not(quoted), cur, out} case SDot{}: seg.dot(quoted, cur, out) case SKeep{c}: Split{quoted, c <> cur, out}# one char of a header against the statedef seg.step(st: Split, c: Char) -> Split: seg.go(st, seg.sym(c))# the segment still being gathered, closed, and the rest put back in orderdef seg.fin(st: Split) -> List<&2, String>: Split{_quoted, cur, out} = st List.reverse(&2, String, seg.done(cur) <> out)# the walk one char at a time, written out rather than foldeddef seg.walk(cs: List<&2, Char>, st: Split) -> Split: match cs: case []: st case h <> t: seg.walk(t, seg.step(st, h))# a header's segments, unquoted. `packages."0x0a".files` is three of them, and a# quoted segment may hold the dots a bare one may not.def segments(s: String) -> List<&2, String>: seg.fin(seg.walk(String.to_list(s), Split{False{}, [], []}))# a string in quotes, which is how a segment or a key that is not bare is# written, and how every value isdef quote(+s: String) -> String: "\"" ++ s ++ "\""# a char a bare key may hold. `+c` because it is asked four questions; a# predicate handed to a fold may not take one, so it is split out here.def bare.at(+c: Char) -> Bool: Bool.or(Char.is_alpha(c), Bool.or(Char.is_digit(c), Bool.or(Char.is_eq(c, '_'), Char.is_eq(c, '-'))))# one step of the walk, with the head's answer in hand. `Bool.and` runs both# of its sides, so the first char that a bare key may not hold still cost a# walk of the rest of the key.def bare.all.step(here: Bool, rest: Unit -> Bool) -> Bool: match here: case True{}: rest(Unit{}) case False{}: False{}# whether every char of a key is one a bare key may hold. Base's `List.all`# applies an erased function parameter and so falls outside the termination# check; this walk is structural.def bare.all(cs: List<&2, Char>) -> Bool: match cs: case []: True{} case +h <> t: bare.all.step(bare.at(h), _u => bare.all(t))# whether a key can be written without quotesdef bare(+s: String) -> Bool: Bool.and(Bool.not(String.is_empty(s)), bare.all(String.to_list(s)))# a key as it is written: bare when it can be, quoted when it must bedef key(+s: String) -> String: Bool.pick(String, bare(s), s, quote(s))# one `key = "value"` linedef render.pair(kv: Kv) -> String: Kv{k, v} = kv key(k) ++ " = " ++ quote(v) ++ "\n"# every pair of a section, in the order it holds themdef render.pairs(ps: List<&2, Kv>) -> String: match ps: case []: "" case h <> t: render.pair(h) ++ render.pairs(t)# one table: its header, then its pairs. The header is written as it is given,# so a caller that needs a quoted segment quotes it.def render.sect(s: Sect) -> String: Sect{n, ps} = s "[" ++ n ++ "]\n" ++ render.pairs(ps)# every table of a documentdef render.all(ss: List<&2, Sect>) -> List<&2, String>: match ss: case []: [] case h <> t: render.sect(h) <> render.all(t)# a document of tables, one blank line between themdef render(ss: List<&2, Sect>) -> String: String.join(render.all(ss), "\n")# a pair as `key=value`, for a test or a reportdef show.kv(kv: Kv) -> String: Kv{k, v} = kv k ++ "=" ++ v# every pair of a section, showndef show.kvs(ps: List<&2, Kv>) -> List<&2, String>: match ps: case []: [] case h <> t: show.kv(h) <> show.kvs(t)# a section as `name key=value ..`def show.sect(s: Sect) -> String: Sect{n, ps} = s String.join(n <> show.kvs(ps), " ")# every section of a document, showndef show.sects(ss: List<&2, Sect>) -> List<&2, String>: match ss: case []: [] case h <> t: show.sect(h) <> show.sects(t)