core.bend checks

A step of a path. Positions count what was passed on the way, so that following a path never compares two names: AtIndex{i} is element i of a list, AtField{skip, name} the field skip places after this one in the schema, BoundAt{i, key} the bound of element i of a bounded list. The names are for the host to print.

The value under name in an object, or RMissing.

None of the keys of a variant chain is in the object r.

---- a strict object: its keys ----

The names a record or variant chain declares. SStrict refuses a key that is not one of them; wf asks that SStrict wrap such a chain.

Every key of the object r is one of ns (anything but an object has none).

The object r without its first key k (what lookup(k, r) reads).

The tag under k is the string n.

r is a string whose length is in the bounds: what conforms reads at an SStrLen, and what len_err refuses exactly when it fails.

The same bounds as ready-made rules: a project's rule calls them by tag (case 0n: str_len_in(1n, 64n, r)), since a tag carries no numbers. Each refuses only the value it is about -- a string, a number -- and leaves any other kind to the schema's own check; the constructors below read the tests directly, because their bound is in the schema.

k is a key of the object r.

name appears at most once among the keys of the object r. b is whether a key read before r was already name; the flag carries forward, and a key that is name while the flag is set is the second one -- refused here and nowhere else. The value is the first argument because a self-call must read its arguments left to right, unchanged until one shrinks, and only the value shrinks; the value is matched first because a match cannot be nested inside the branch of a match on another parameter. One pass, so a walk costs one key per key, the same as the lookup beside it.

name appears at most once among the keys of the object r: nothing has been read yet.

The repeated key as check reports it: at the key's own name, with no step after it (the second occurrence is not a place in the schema). The test is passed in rather than read here (a match cannot scrutinize a computed value): b is key_once(name, r), so nothing is reported exactly when key_once holds, which is what check_exact needs.

An error found under a step gets the step in front of its path.

At an SStrLen the shape comes first, as everywhere else: a value that is not a string is NotString, a string out of its bounds is LengthNotIn, and a node the codec refused to build or that is absent reads as it does at every kind.

An error found further along a list is one element further: its first step, if it counts elements, counts one more. A plain list's steps are AtIndex; a bounded list's are AtIndex and BoundAt.

An error found in a later field is one field further.

The first of two: the second counts only when the first found nothing.

The reason a value that is not the shape is refused, at the place it was found: an absent slot is Missing, a node the host refused to build (RTooBig) is TooLarge, anything else is the schema kind's own reason. check and the defect helpers both answer through here, so the reason a path reports is the same one for both.

A second key of a variant chain in the object r: the first one found.

The first key of r that is not one of ns, at its own name.

At the end of a tagged chain no case matched: the value is not an object, or its tag is missing, or it names no case.

The count, as an error: at an SListLen the count is read before any element, so a list out of bounds is CountNotIn at the list's own path. A value that is not a list has no count to object to, and is refused as a list schema refuses it: NotList, or Missing/TooLarge for the two nodes that are never a shape (the same reasons check's own arms give them).

The same two reasons at an SNatIn and an SBool, replayed along a path: the value's own kind is the defect when the path ends here, and it is not a defect at all further along (the walk passed it).

The claim about a second key: every key passed is absent, and the key the path names is there.

At a strict object the path is one key, and the replay checks it on its own: the key is there, and it is not one of the names.

The tag key of a tagged case, taken twice, as defect replays it. check reports it before the case's own schema is walked -- there is no place in the schema for the second occurrence -- so the path is one field step at the tag's own name and nothing after it. b is whether the key is not read once, so nothing is reported exactly when key_once holds; a path of any other shape is the case's own report, which the walk below answers.

---- the claim the strict law makes ----

How many keys of r are not in ns, counted rather than walked with a Bool.and: a second algorithm, so that a no_extra that lets a key through (or refuses a named one) disagrees with it.

An absent value reaches the top of what enc writes for s: s is an SOptional, or it hands the value it was given straight to a schema that is (a rule, a strict object, a bound, or the tail of a variant or tagged chain -- and an SOpt, whose Some case passes the value through). Everything else wraps what it writes in a constructor of its own, so an absent value cannot surface.

---- the object a schema's encoding lands in ----

enc writes an object as one flat chain of keys. An SField writes its name and its rest continues that object; an SVariant writes its name and the value under it is a chain of its own (REnd ends it, so it is a value and not a continuation). A wrapper -- a rule, a strict object, a bound, an optional -- writes no key of its own and hands its value straight to its inner schema, so a key reaches the top of the object from inside any of them. A tagged case's schema is the same object the tag key was written into, and so is the rest of its chain.

no_key is that, written down: k does not reach the top of the object enc builds for s, for any value of s. wf asks it of a tagged case's own schema, which is what keeps the tag key from being written twice.

n is not a key of the record chain s (a chain ends in SEnd). Both orders are asked, as fresh_v asks them: which of the two names a step puts first depends on which of them is the value's key there, and asking both spares a proof that String.eq is symmetric.

n is not a key of the variant chain s (a chain ends in SVEnd). Both orders are asked: reading a key compares the names one way, reading past it the other, and asking both spares a proof that String.eq is symmetric.

A record chain (ending in SEnd) or a variant chain (ending in SVEnd): what SStrict may wrap, so every key its encoding writes is a declared name. A chain of keys (SField or SVariant links, ending in SEnd or SVEnd): what SStrict may wrap, so every key its encoding writes is a name it declares.

n names no case of the tagged chain s, whose key is k, and the chain ends in STagEnd{k}: one key for the whole chain.

Every enum value in x is one of its names (encode_conforms' premise).

Every bound a constructor states holds of the value that will be written, at every place one sits in the schema (encode_conforms' second premise, beside names_ok). The encoder writes the meaning unchanged, so a value outside a bound is written out as it is and refused by check on the way back: the host that built it is at fault, and this is where it says so. An SStrLen's bound is read off the string its own schema writes, and an SListLen's count off the list it writes, which is why enc appears here.