toml.bend checks

raw source on the hub · import 0x04b9afdd6d6a56039c5ce6dfb1e55294/toml.bend as Toml

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.

1 import

import Base

Types

type Kv source · line 9 · raw

Data

a key and the string written for it

Kv
```
@key:String -> @val:String -> Kv
```

type Sect source · line 13 · raw

Data

a section header and the pairs under it, in the order they were written

Sect

@name:String -> @pairs:List<&2, Kv> -> Sect

type Line source · line 17 · raw

Data

what one line turned out to be

LSkip
```
Line
```
LHead
```
@name:String -> Line
```
LPair
```
@key:String -> @val:String -> Line
```
LBad
```
@why:String -> Line
```

type Trim source · line 25 · raw

Data

a trim in progress: skip is true until the first non-space, out is the chars kept so far, reversed

Trim

@skip:Bool -> @out:List<&2, Char> -> Trim

type Toml source · line 30 · raw

Data

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.

Toml

@bad:String -> @name:String -> @pairs:List<&2, Kv> -> @done:List<&2, Sect> -> Toml

type Sym source · line 275 · raw

Data

what a header's next character is: the quoting toggles, an unquoted dot cuts, anything else is kept

SQuote
```
Sym
```
SDot
```
Sym
```
SKeep
```
@c:Char -> Sym
```

type Split source · line 287 · raw

Data

a header being cut apart: quoted is true inside quotes, cur is the segment being gathered and out the finished ones, both reversed

Split

@quoted:Bool -> @cur:List<&2, Char> -> @out:List<&2, String> -> Split

Definitions

def trim.keep.go source · line 35 · raw

@sp:Bool -> @c:Char -> @out:List<&2, Char> -> Trim

while skipping, a space is dropped and the skipping goes on; the first other char is kept and ends it

def trim.keep source · line 44 · raw

@+c:Char -> @out:List<&2, Char> -> Trim

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.step source · line 48 · raw

@st:Trim -> @c:Char -> Trim

one char of a trim: skip stays true until a non-space arrives

def trim.out source · line 58 · raw

@st:Trim -> List<&2, Char>

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.walk source · line 66 · raw

@cs:List<&2, Char> -> @st:Trim -> Trim

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.pass source · line 74 · raw

@cs:List<&2, Char> -> List<&2, Char>

the chars with leading spaces dropped, reversed

def trim source · line 79 · raw

@s:String -> String

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 strip.cut source · line 83 · raw

@hit:Bool -> @h:Char -> @t:List<&2, Char> -> List<&2, Char>

drops one leading char when it is the one given

def strip.front source · line 91 · raw

@cs:List<&2, Char> -> @c:Char -> List<&2, Char>

the chars without one leading c, if there is one

def strip.back.go source · line 100 · raw

@t:List<&2, Char> -> @+h:Char -> @+c:Char -> List<&2, Char>

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 source · line 110 · raw

@cs:List<&2, Char> -> @+c:Char -> List<&2, Char>

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 source · line 118 · raw

@s:String -> @a:Char -> @b:Char -> String

the string without one leading a and one trailing b

def pair_of source · line 123 · raw

@parts:List<&2, String> -> Line

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 survives

def head_of source · line 131 · raw

@+s:String -> @shut:Bool -> Line

a header line, once it is known to start with [

def line_of.pair source · line 141 · raw

@here:Bool -> @+s:String -> Line

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.head source · line 149 · raw

@here:Bool -> @+s:String -> Line

the section header decided, and the pair question asked only underneath it

def line_of.comment source · line 158 · raw

@here:Bool -> @+s:String -> Line

a comment, which may hold anything and so is answered before anything is read out of the line

def line_of.blank source · line 168 · raw

@here:Bool -> @+s:String -> Line

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 key

def line_of source · line 183 · raw

@+s:String -> Line

what a trimmed line is. The order matters: a comment may hold anything.

The cascade is four match arms rather than four nested Bool.picks 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 first source · line 187 · raw

@+bad:String -> @why:String -> String

the first error wins, so a later one is dropped

def flush.put source · line 192 · raw

@empty:Bool -> @name:String -> @pairs:List<&2, Kv> -> @done:List<&2, Sect> -> List<&2, Sect>

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 source · line 200 · raw

@+name:String -> @pairs:List<&2, Kv> -> @done:List<&2, Sect> -> List<&2, Sect>

the section being filled, moved into the finished ones

def put.go source · line 205 · raw

@loose:Bool -> @bad:String -> @name:String -> @pairs:List<&2, Kv> -> @done:List<&2, Sect> -> @+key:String -> @val:String -> Toml

a pair belongs to the section being filled, and is an error before the first header

def put source · line 215 · raw

@st:Toml -> @key:String -> @val:String -> Toml

a pair belongs to the section being filled, and is an error before the first header

def step.go source · line 220 · raw

@st:Toml -> @line:Line -> Toml

the state once a line has been classified

def step source · line 233 · raw

@st:Toml -> @raw:String -> Toml

one line against the state

def parse.fin source · line 237 · raw

@r:Toml -> Toml

the last section flushed, and the finished ones put back in order

def parse.walk source · line 242 · raw

@ls:List<&2, String> -> @st:Toml -> Toml

the walk one line at a time, written out rather than folded

def parse source · line 250 · raw

@text:String -> Toml

the sections of a document, and the first error if there was one

def value.at source · line 255 · raw

@kv:Kv -> @rest:String -> @key:String -> String

this pair's value when the key matches, otherwise whatever the rest of the table gave

def value source · line 261 · raw

@pairs:List<&2, Kv> -> @+key:String -> String

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 sects source · line 269 · raw

@t:Toml -> List<&2, Sect>

the sections a parse found, in the order they were written

def seg.sym source · line 281 · raw

@+c:Char -> Sym

a header char classified. +c because it is both asked about and kept.

def seg.done source · line 291 · raw

@cur:List<&2, Char> -> String

the segment gathered so far, in order

def seg.dot source · line 295 · raw

@quoted:Bool -> @cur:List<&2, Char> -> @out:List<&2, String> -> Split

a dot inside quotes is part of the segment; outside, it ends one

def seg.go source · line 303 · raw

@st:Split -> @s:Sym -> Split

the state once a char has been classified

def seg.step source · line 314 · raw

@st:Split -> @c:Char -> Split

one char of a header against the state

def seg.fin source · line 318 · raw

@st:Split -> List<&2, String>

the segment still being gathered, closed, and the rest put back in order

def seg.walk source · line 323 · raw

@cs:List<&2, Char> -> @st:Split -> Split

the walk one char at a time, written out rather than folded

def segments source · line 332 · raw

@s:String -> List<&2, String>

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 quote source · line 337 · raw

@+s:String -> String

a string in quotes, which is how a segment or a key that is not bare is written, and how every value is

def bare.at source · line 342 · raw

@+c:Char -> Bool

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.all.step source · line 349 · raw

@here:Bool -> @rest:(@_:Unit -> Bool) -> Bool

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 source · line 359 · raw

@cs:List<&2, Char> -> Bool

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.