core.bend
bend-schema-lib@0.1.0.0 · 1,585 lines · 0 definitions
1import Base
2
3# bend-schema: a schema, and one check for every schema, proved once.
4#
5# The host turns any JSON value into a Raw with one universal codec that knows
6# no schema: numbers that are whole and within the runtime's Nat become RNum,
7# every other number, boolean or unsupported value becomes RBad. A list or an
8# object past the codec's budget becomes one RTooBig, in its place: the codec
9# counts elements and keys so that these walks never receive a value the
10# runtime cannot carry, and a size becomes an error (TooLarge, at the node's
11# path) rather than a crash. Lists and objects are chains built into Raw
12# (RNil/RCons, REnd/RKey), so that every walk here is structural. RMissing is
13# never produced by the codec: it is what looking up an absent key gives.
14#
15# A Schema says what a valid value is (`conforms`), and `check` finds the
16# first thing wrong, with the path to it: depth first, lists in element order,
17# objects in the schema's field order; an element of a bounded list is read
18# whole before its bound, and an SListLen's element count is read before any
19# element. Keys the schema does not name are ignored; a key it names must be
20# present, and two constructors say what may be there instead: SOpt is a value
21# that may be null, SOptional a field that may be absent (the host writes no
22# key at all, so it is well-formed only as a field's own schema).
23#
24# Both walk the schema and the value together, in one self-recursive def: a
25# step into a field or an optional shrinks the schema, a step along a list
26# keeps it and shrinks the value (the checker reads the arguments left to
27# right until one shrinks). A project's rules arrive as one template
28# parameter, `~rule: Nat -> Raw -> Maybe<Err>`: at an SRule the value must
29# conform to the rule's schema first, then the rule decides (the tag picks
30# the rule; the rule's error path is relative to the value it was given).
31# Template defs cannot cross the bundler, so the host calls the closed forms
32# below (check0, conforms0). `prev` is carried but no case reads it today; a
33# stateful combinator would.
34
35type Raw is Data:
36 RNum{n: Nat}
37 RBool{b: Bool}
38 RNull{}
39 RStr{s: String}
40 RBad{}
41 RTooBig{}
42 RMissing{}
43 RNil{}
44 RCons{head: Raw, tail: Raw}
45 REnd{}
46 RKey{key: String, val: Raw, rest: Raw}
47
48type Schema is Data:
49 SNat{}
50 SNatIn{lo: Nat, hi: Nat}
51 SStr{}
52 SStrLen{lo: Nat, hi: Nat, s: Schema}
53 SOpt{inner: Schema}
54 SList{elem: Schema}
55 SField{name: String, s: Schema, rest: Schema}
56 SEnd{}
57 SRule{s: Schema, tag: Nat}
58 SStrict{s: Schema}
59 STagged{key: String, name: String, s: Schema, rest: Schema}
60 STagEnd{key: String}
61 SBool{}
62 STrue{}
63 SEnum{names: List<&2, String>}
64 SVariant{name: String, s: Schema, rest: Schema}
65 SVEnd{}
66 STuple{s: Schema, rest: Schema}
67 STEnd{}
68 SOptional{inner: Schema}
69 SListLen{lo: Nat, hi: Nat, s: Schema}
70
71# A step of a path. Positions count what was passed on the way, so that
72# following a path never compares two names: AtIndex{i} is element i of a
73# list, AtField{skip, name} the field `skip` places after this one in the
74# schema, BoundAt{i, key} the bound of element i of a bounded list. The names
75# are for the host to print.
76type Step is Data:
77 AtIndex{i: Nat}
78 AtField{skip: Nat, name: String}
79 BoundAt{i: Nat, key: String}
80 AtKey{key: String}
81
82type Why is Data:
83 Missing{}
84 NotNat{}
85 NotString{}
86 NotBool{}
87 NotList{}
88 NotObject{}
89 NoElements{}
90 OpenNotLast{}
91 LastNotOpen{}
92 NotIncreasing{prev: Nat, got: Nat}
93 NotTrue{}
94 NotOneOf{}
95 NoVariant{}
96 TwoVariants{}
97 TooShort{}
98 TooLong{}
99 LengthNotIn{lo: Nat, hi: Nat}
100 NotIn{lo: Nat, hi: Nat}
101 UnknownKey{}
102 RepeatedKey{key: String}
103 TooLarge{}
104 CountNotIn{lo: Nat, hi: Nat}
105
106type Err is Data:
107 Err{path: List<&2, Step>, why: Why}
108
109# ---- reading a value ----
110
111def pick_raw(b: Bool, +x: Raw, +y: Raw) -> Raw:
112 match b:
113 case True{}:
114 x
115 case False{}:
116 y
117
118# The value under `name` in an object, or RMissing.
119def lookup(+name: String, r: Raw) -> Raw:
120 match r:
121 case RKey{k, +v, rest}:
122 pick_raw(String.eq(k, name), v, lookup(name, rest))
123 case _:
124 RMissing{}
125
126def pick_bool(b: Bool, +x: Bool, +y: Bool) -> Bool:
127 match b:
128 case True{}:
129 x
130 case False{}:
131 y
132
133def is_rnil(r: Raw) -> Bool:
134 match r:
135 case RNil{}:
136 True{}
137 case _:
138 False{}
139
140# ---- the helpers of the choices: true, one of some names, one of some keys ----
141
142def is_missing(v: Raw) -> Bool:
143 match v:
144 case RMissing{}:
145 True{}
146 case _:
147 False{}
148
149def in_names(+x: String, names: List<&2, String>) -> Bool:
150 match names:
151 case Nil{}:
152 False{}
153 case n <> t:
154 Bool.or(String.eq(x, n), in_names(x, t))
155
156# None of the keys of a variant chain is in the object r.
157def none_present(s: Schema, +r: Raw) -> Bool:
158 match s:
159 case SVariant{n, vs, rest}:
160 Bool.and(is_missing(lookup(n, r)), none_present(rest, r))
161 case _:
162 True{}
163
164# ---- a strict object: its keys ----
165#
166# The names a record or variant chain declares. SStrict refuses a key that is
167# not one of them; wf asks that SStrict wrap such a chain.
168def key_names(s: Schema) -> List<&2, String>:
169 match s:
170 case SField{n, fs, rest}:
171 n <> key_names(rest)
172 case SVariant{n, vs, rest}:
173 n <> key_names(rest)
174 case _:
175 Nil{}
176
177# Every key of the object r is one of ns (anything but an object has none).
178def no_extra(+ns: List<&2, String>, r: Raw) -> Bool:
179 match r:
180 case RKey{+k, v, o}:
181 Bool.and(in_names(k, ns), no_extra(ns, o))
182 case _:
183 True{}
184
185# ---- a tagged union: its tag, and the object a case sees ----
186#
187# STagged{key, name, s, rest} is one case of a chain ending in STagEnd{key}:
188# when the value under `key` is the string `name`, the object without that
189# key must conform to s; otherwise the chain goes on. The case does not see
190# the tag, so an SStrict case need not name it.
191
192# The object r without its first key k (what lookup(k, r) reads).
193def drop_key(+k: String, r: Raw) -> Raw:
194 match r:
195 case RKey{+j, +v, +o}:
196 pick_raw(String.eq(j, k), o, RKey{j, v, drop_key(k, o)})
197 case x:
198 x
199
200def is_str(+n: String, v: Raw) -> Bool:
201 match v:
202 case RStr{x}:
203 String.eq(x, n)
204 case _:
205 False{}
206
207# The tag under k is the string n.
208def is_tag(+k: String, +n: String, r: Raw) -> Bool:
209 is_str(n, lookup(k, r))
210
211# ---- a bound, as a test and as a reason ----
212#
213# SStrLen{lo, hi, s} is a string in the bounds that also satisfies s, SListLen
214# the same over a list's elements, SNatIn is a number in the bounds, and SBool
215# is a boolean. The bound travels with the schema instead of with a rule's tag,
216# which is what lets a host build one (a rule is chosen by a number, and a
217# number carries no bounds).
218#
219# A rule and a constructor state the same bounds, and these defs are where they
220# are written once: str_len_ok and num_ok are the tests, in_err is how a failing
221# test becomes an error at the value's own path, and len_ok is the same test
222# read as a Bool (what conforms asks at an SStrLen). Both ends are included;
223# lo > hi is not an error but an empty range, in which nothing is in bounds.
224
225def in_err(b: Bool, w: Why) -> Maybe<&2, Err>:
226 match b:
227 case True{}:
228 None{}
229 case False{}:
230 Some{Err{Nil{}, w}}
231
232def str_len_ok(+lo: Nat, +hi: Nat, +x: String) -> Bool:
233 Bool.and(Nat.is_le(lo, String.length(x)), Nat.is_le(String.length(x), hi))
234
235def num_ok(+lo: Nat, +hi: Nat, +n: Nat) -> Bool:
236 Bool.and(Nat.is_le(lo, n), Nat.is_le(n, hi))
237
238# r is a string whose length is in the bounds: what conforms reads at an
239# SStrLen, and what len_err refuses exactly when it fails.
240def len_ok(+lo: Nat, +hi: Nat, r: Raw) -> Bool:
241 match r:
242 case RStr{+x}:
243 str_len_ok(lo, hi, x)
244 case _:
245 False{}
246
247# The same bounds as ready-made rules: a project's rule calls them by tag
248# (`case 0n: str_len_in(1n, 64n, r)`), since a tag carries no numbers. Each
249# refuses only the value it is about -- a string, a number -- and leaves any
250# other kind to the schema's own check; the constructors below read the tests
251# directly, because their bound is in the schema.
252def str_len_in(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
253 match r:
254 case RStr{+x}:
255 in_err(str_len_ok(lo, hi, x), LengthNotIn{lo, hi})
256 case _:
257 None{}
258
259def nat_in(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
260 match r:
261 case RNum{+n}:
262 in_err(num_ok(lo, hi, n), NotIn{lo, hi})
263 case _:
264 None{}
265
266def is_bool(r: Raw) -> Bool:
267 match r:
268 case RBool{b}:
269 True{}
270 case _:
271 False{}
272
273# A list's element count, as a test. SListLen{lo, hi, s} is a list whose
274# element count is in the bounds that also satisfies s: the same shape an
275# SStrLen has, over elements instead of characters. raw_list is "r is a list at
276# all", raw_len counts a proper list's elements (0 for anything else, which is
277# why every use asks raw_list too), count_ok is the bound read as a Bool, and
278# list_len_ok is both together -- what conforms asks at an SListLen, and what
279# count_err refuses exactly when it fails. Both ends are included; lo > hi is
280# not an error but an empty range, in which no list is in bounds.
281
282def raw_list(r: Raw) -> Bool:
283 match r:
284 case RNil{}:
285 True{}
286 case RCons{h, t}:
287 raw_list(t)
288 case _:
289 False{}
290
291def raw_len(r: Raw) -> Nat:
292 match r:
293 case RCons{h, t}:
294 1n+raw_len(t)
295 case _:
296 0n
297
298def count_ok(+lo: Nat, +hi: Nat, +r: Raw) -> Bool:
299 Bool.and(Nat.is_le(lo, raw_len(r)), Nat.is_le(raw_len(r), hi))
300
301def list_len_ok(+lo: Nat, +hi: Nat, +r: Raw) -> Bool:
302 Bool.and(raw_list(r), count_ok(lo, hi, r))
303
304# ---- a key the schema reads ----
305#
306# A key the schema reads as a field key (SField) or as a variant key (SVariant)
307# must appear at most once in the value: with a key repeated, lookup reads the
308# first one and the second is unreachable, so the value says something the
309# schema cannot mean. A key the schema does not name is never read, so
310# repeating it is unobservable and is left alone.
311#
312# The tag key of a tagged case is read the same way -- it is how the chain
313# picks its case -- so it is checked the same way, and at the case the tag
314# names: conforms, check and defect all ask key_once at the value's own tag
315# key, and a case whose tag matched is refused when the key is there twice.
316# The check sits at the case and not at the chain because a value whose tag
317# names no case is refused at the chain's end whatever its keys are, and
318# because the case is the only place the question has an answer: the case is
319# checked against the object with the tag key taken out, which is the object
320# its own schema is about.
321#
322# So the other half is wf's: a case's own schema may not read the tag key at
323# all (no_key, above wf). If it did, enc would write that key twice -- the tag
324# first, then the case's own field -- and the host builds the object as a JS
325# object, where the second write overwrites the first, so the value written
326# could not be read back. Refusing the schema is what keeps encode_conforms
327# true.
328
329# k is a key of the object r.
330def has_key(+k: String, r: Raw) -> Bool:
331 match r:
332 case RKey{j, v, o}:
333 Bool.or(String.eq(k, j), has_key(k, o))
334 case _:
335 False{}
336
337# name appears at most once among the keys of the object r. b is whether a key
338# read before r was already name; the flag carries forward, and a key that is
339# name while the flag is set is the second one -- refused here and nowhere
340# else. The value is the first argument because a self-call must read its
341# arguments left to right, unchanged until one shrinks, and only the value
342# shrinks; the value is matched first because a match cannot be nested inside
343# the branch of a match on another parameter. One pass, so a walk costs one
344# key per key, the same as the lookup beside it.
345def key_once_at(r: Raw, +b: Bool, +name: String) -> Bool:
346 match r:
347 case RKey{+k, +v, +o}:
348 Bool.and(Bool.not(Bool.and(b, String.eq(k, name))), key_once_at(o, Bool.or(b, String.eq(k, name)), name))
349 case _:
350 True{}
351
352# name appears at most once among the keys of the object r: nothing has been
353# read yet.
354def key_once(+name: String, r: Raw) -> Bool:
355 key_once_at(r, False{}, name)
356
357# The repeated key as check reports it: at the key's own name, with no step
358# after it (the second occurrence is not a place in the schema). The test is
359# passed in rather than read here (a match cannot scrutinize a computed value):
360# b is key_once(name, r), so nothing is reported exactly when key_once holds,
361# which is what check_exact needs.
362def key_err(b: Bool, +name: String) -> Maybe<&2, Err>:
363 match b:
364 case True{}:
365 None{}
366 case False{}:
367 Some{Err{AtField{0n, name} <> Nil{}, RepeatedKey{name}}}
368
369# ---- what a valid value is ----
370
371def conforms(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>) -> Bool:
372 match s r:
373 case SNat{} RNum{n}:
374 True{}
375 case SNatIn{+lo, +hi} RNum{+n}:
376 num_ok(lo, hi, n)
377 case SStr{} RStr{x}:
378 True{}
379 case SStrLen{+lo, +hi, +s2} +x:
380 Bool.and(conforms(~rule, s2, x, prev), len_ok(lo, hi, x))
381 case SListLen{+lo, +hi, +s2} +r:
382 Bool.and(list_len_ok(lo, hi, r), conforms(~rule, s2, r, None{}))
383 case SOpt{inner} RNull{}:
384 True{}
385 case SOpt{inner} x:
386 conforms(~rule, inner, x, None{})
387 case SOptional{+inner} +x:
388 Bool.or(is_missing(x), conforms(~rule, inner, x, None{}))
389 case SList{e} RNil{}:
390 True{}
391 case SList{+e} RCons{h, t}:
392 Bool.and(conforms(~rule, e, h, None{}), conforms(~rule, SList{e}, t, None{}))
393 case SField{+name, fs, rest} REnd{}:
394 Bool.and(conforms(~rule, fs, RMissing{}, None{}), conforms(~rule, rest, REnd{}, None{}))
395 case SField{+name, fs, rest} RKey{+k, +v, +o}:
396 Bool.and(key_once(name, RKey{k, v, o}), Bool.and(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), conforms(~rule, rest, RKey{k, v, o}, None{})))
397 case SEnd{} REnd{}:
398 True{}
399 case SEnd{} RKey{k, v, o}:
400 True{}
401 case SRule{+s2, +tag} +x:
402 Bool.and(conforms(~rule, s2, x, prev), Maybe.is_none(&2, Err, rule(tag, x)))
403 case SStrict{+s2} +x:
404 Bool.and(conforms(~rule, s2, x, prev), no_extra(key_names(s2), x))
405 case STagged{+k, +n, cs, rest} +x:
406 pick_bool(is_tag(k, n, x), Bool.and(key_once(k, x), conforms(~rule, cs, drop_key(k, x), None{})), conforms(~rule, rest, x, None{}))
407 case STagEnd{k} x:
408 False{} # the end of a tagged chain: no case matched
409 case SBool{} RBool{b}:
410 True{} # any boolean is a boolean, and nothing else is
411 case STrue{} RBool{b}:
412 b
413 case SEnum{names} RStr{+x}:
414 in_names(x, names)
415 case SVariant{+name, +vs, +rest} REnd{}:
416 conforms(~rule, rest, REnd{}, None{})
417 case SVariant{+name, +vs, +rest} RKey{+k, +v, +o}:
418 pick_bool(is_missing(lookup(name, RKey{k, v, o})), conforms(~rule, rest, RKey{k, v, o}, None{}), Bool.and(key_once(name, RKey{k, v, o}), Bool.and(conforms(~rule, vs, lookup(name, RKey{k, v, o}), None{}), none_present(rest, RKey{k, v, o}))))
419 case STuple{ts, rest} RCons{h, t}:
420 Bool.and(conforms(~rule, ts, h, None{}), conforms(~rule, rest, t, None{}))
421 case STEnd{} RNil{}:
422 True{}
423 case _ _:
424 False{}
425
426# ---- the first thing wrong ----
427
428def here(w: Why) -> Maybe<&2, Err>:
429 Some{Err{Nil{}, w}}
430
431# An error found under a step gets the step in front of its path.
432def under(+st: Step, m: Maybe<&2, Err>) -> Maybe<&2, Err>:
433 match m:
434 case None{}:
435 None{}
436 case Some{Err{p, w}}:
437 Some{Err{st <> p, w}}
438
439# At an SStrLen the shape comes first, as everywhere else: a value that is not
440# a string is NotString, a string out of its bounds is LengthNotIn, and a node
441# the codec refused to build or that is absent reads as it does at every kind.
442def len_err(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
443 match r:
444 case RStr{+x}:
445 in_err(str_len_ok(lo, hi, x), LengthNotIn{lo, hi})
446 case RMissing{}:
447 here(Missing{})
448 case RTooBig{}:
449 here(TooLarge{})
450 case _:
451 here(NotString{})
452
453# An error found further along a list is one element further: its first
454# step, if it counts elements, counts one more. A plain list's steps are
455# AtIndex; a bounded list's are AtIndex and BoundAt.
456def later_l_path(p: List<&2, Step>) -> List<&2, Step>:
457 match p:
458 case AtIndex{j} <> q:
459 AtIndex{1n+j} <> q
460 case q:
461 q
462
463def later_l(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
464 match m:
465 case None{}:
466 None{}
467 case Some{Err{p, w}}:
468 Some{Err{later_l_path(p), w}}
469
470def later_i_path(p: List<&2, Step>) -> List<&2, Step>:
471 match p:
472 case AtIndex{j} <> q:
473 AtIndex{1n+j} <> q
474 case BoundAt{j, key} <> q:
475 BoundAt{1n+j, key} <> q
476 case q:
477 q
478
479def later_i(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
480 match m:
481 case None{}:
482 None{}
483 case Some{Err{p, w}}:
484 Some{Err{later_i_path(p), w}}
485
486# An error found in a later field is one field further.
487def later_f_path(p: List<&2, Step>) -> List<&2, Step>:
488 match p:
489 case AtField{k, n} <> q:
490 AtField{1n+k, n} <> q
491 case q:
492 q
493
494def later_f(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
495 match m:
496 case None{}:
497 None{}
498 case Some{Err{p, w}}:
499 Some{Err{later_f_path(p), w}}
500
501# The first of two: the second counts only when the first found nothing.
502def first(m: Maybe<&2, Err>, n: Maybe<&2, Err>) -> Maybe<&2, Err>:
503 match m:
504 case None{}:
505 n
506 case Some{e}:
507 Some{e}
508
509# The reason a value that is not the shape is refused, at the place it was
510# found: an absent slot is Missing, a node the host refused to build (RTooBig)
511# is TooLarge, anything else is the schema kind's own reason. check and the
512# defect helpers both answer through here, so the reason a path reports is the
513# same one for both.
514def missing_or(r: Raw, w: Why) -> Why:
515 match r:
516 case RMissing{}:
517 Missing{}
518 case RTooBig{}:
519 TooLarge{}
520 case _:
521 w
522
523def pick_err(b: Bool, +x: Maybe<&2, Err>, +y: Maybe<&2, Err>) -> Maybe<&2, Err>:
524 match b:
525 case True{}:
526 x
527 case False{}:
528 y
529
530def true_err(b: Bool) -> Maybe<&2, Err>:
531 match b:
532 case True{}:
533 None{}
534 case False{}:
535 here(NotTrue{})
536
537def enum_err(b: Bool) -> Maybe<&2, Err>:
538 match b:
539 case True{}:
540 None{}
541 case False{}:
542 here(NotOneOf{})
543
544# A second key of a variant chain in the object r: the first one found.
545def dup_err(s: Schema, +r: Raw) -> Maybe<&2, Err>:
546 match s:
547 case SVariant{+n, vs, rest}:
548 pick_err(is_missing(lookup(n, r)), later_f(dup_err(rest, r)), Some{Err{AtField{0n, n} <> Nil{}, TwoVariants{}}})
549 case _:
550 None{}
551
552# The first key of r that is not one of ns, at its own name.
553def extra_err(+ns: List<&2, String>, r: Raw) -> Maybe<&2, Err>:
554 match r:
555 case RKey{+k, v, o}:
556 pick_err(in_names(k, ns), extra_err(ns, o), Some{Err{AtKey{k} <> Nil{}, UnknownKey{}}})
557 case _:
558 None{}
559
560# At the end of a tagged chain no case matched: the value is not an object,
561# or its tag is missing, or it names no case.
562def tag_err(+k: String, r: Raw) -> Maybe<&2, Err>:
563 match r:
564 case REnd{}:
565 Some{Err{AtKey{k} <> Nil{}, Missing{}}}
566 case RKey{j, v, o}:
567 Some{Err{AtKey{k} <> Nil{}, missing_or(lookup(k, RKey{j, v, o}), NotOneOf{})}}
568 case x:
569 here(missing_or(x, NotObject{}))
570
571# The count, as an error: at an SListLen the count is read before any element,
572# so a list out of bounds is CountNotIn at the list's own path. A value that is
573# not a list has no count to object to, and is refused as a list schema refuses
574# it: NotList, or Missing/TooLarge for the two nodes that are never a shape
575# (the same reasons check's own arms give them).
576def count_err(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
577 match r:
578 case RNil{}:
579 in_err(list_len_ok(lo, hi, r), CountNotIn{lo, hi})
580 case RCons{h, t}:
581 in_err(list_len_ok(lo, hi, r), CountNotIn{lo, hi})
582 case _:
583 here(missing_or(r, NotList{}))
584
585def check(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>) -> Maybe<&2, Err>:
586 match s r:
587 case SNat{} RNum{n}:
588 None{}
589 case SNat{} x:
590 here(missing_or(x, NotNat{}))
591 case SStr{} RStr{x}:
592 None{}
593 case SStr{} x:
594 here(missing_or(x, NotString{}))
595 case SNatIn{+lo, +hi} RNum{+n}:
596 nat_in(lo, hi, RNum{n})
597 case SNatIn{lo_, hi_} +x:
598 here(missing_or(x, NotNat{}))
599 case SStrLen{+lo, +hi, +s2} +x:
600 first(check(~rule, s2, x, prev), len_err(lo, hi, x))
601 case SListLen{+lo, +hi, +s2} +r:
602 first(count_err(lo, hi, r), check(~rule, s2, r, None{}))
603 case SOpt{inner} RNull{}:
604 None{}
605 case SOpt{inner} x:
606 check(~rule, inner, x, None{})
607 case SOptional{inner} RMissing{}:
608 None{}
609 case SOptional{inner} x:
610 check(~rule, inner, x, None{})
611 case SList{e} RNil{}:
612 None{}
613 case SList{+e} RCons{h, t}:
614 first(under(AtIndex{0n}, check(~rule, e, h, None{})), later_l(check(~rule, SList{e}, t, None{})))
615 case SList{e} x:
616 here(missing_or(x, NotList{}))
617 case SField{+name, fs, rest} REnd{}:
618 first(under(AtField{0n, name}, check(~rule, fs, RMissing{}, None{})), later_f(check(~rule, rest, REnd{}, None{})))
619 case SField{+name, fs, rest} RKey{+k, +v, +o}:
620 first(key_err(key_once(name, RKey{k, v, o}), name), first(under(AtField{0n, name}, check(~rule, fs, lookup(name, RKey{k, v, o}), None{})), later_f(check(~rule, rest, RKey{k, v, o}, None{}))))
621 case SField{name, fs, rest} x:
622 here(missing_or(x, NotObject{}))
623 case SEnd{} REnd{}:
624 None{}
625 case SEnd{} RKey{k, v, o}:
626 None{}
627 case SEnd{} x:
628 here(missing_or(x, NotObject{}))
629 case SRule{+s2, +tag} +x:
630 first(check(~rule, s2, x, prev), rule(tag, x))
631 case SStrict{+s2} +x:
632 first(check(~rule, s2, x, prev), extra_err(key_names(s2), x))
633 case STagged{+k, +n, cs, rest} +x:
634 pick_err(is_tag(k, n, x), first(key_err(key_once(k, x), k), check(~rule, cs, drop_key(k, x), None{})), check(~rule, rest, x, None{}))
635 case STagEnd{k} x:
636 tag_err(k, x)
637 case SBool{} RBool{b}:
638 None{}
639 case SBool{} +x:
640 here(missing_or(x, NotBool{}))
641 case STrue{} RBool{b}:
642 true_err(b)
643 case STrue{} x:
644 here(missing_or(x, NotTrue{}))
645 case SEnum{names} RStr{+x}:
646 enum_err(in_names(x, names))
647 case SEnum{names} x:
648 here(missing_or(x, NotOneOf{}))
649 case SVariant{+name, +vs, +rest} REnd{}:
650 later_f(check(~rule, rest, REnd{}, None{}))
651 case SVariant{+name, +vs, +rest} RKey{+k, +v, +o}:
652 pick_err(is_missing(lookup(name, RKey{k, v, o})), later_f(check(~rule, rest, RKey{k, v, o}, None{})), first(key_err(key_once(name, RKey{k, v, o}), name), first(under(AtField{0n, name}, check(~rule, vs, lookup(name, RKey{k, v, o}), None{})), later_f(dup_err(rest, RKey{k, v, o})))))
653 case SVariant{+name, +vs, +rest} x:
654 here(missing_or(x, NotObject{}))
655 case SVEnd{} REnd{}:
656 here(NoVariant{})
657 case SVEnd{} RKey{k, v, o}:
658 here(NoVariant{})
659 case SVEnd{} x:
660 here(missing_or(x, NotObject{}))
661 case STuple{ts, rest} RCons{h, t}:
662 first(under(AtIndex{0n}, check(~rule, ts, h, None{})), later_l(check(~rule, rest, t, None{})))
663 case STuple{ts, rest} RNil{}:
664 here(TooShort{})
665 case STuple{ts, rest} x:
666 here(missing_or(x, NotList{}))
667 case STEnd{} RNil{}:
668 None{}
669 case STEnd{} RCons{h, t}:
670 here(TooLong{})
671 case STEnd{} x:
672 here(missing_or(x, NotList{}))
673
674# ---- the claim the accuracy law makes ----
675#
676# defect follows a path instead of searching for one. Everything it passes on
677# the way must conform, a step's name must be the schema's, and at the end of
678# the path it answers what is wrong there. A path that does not fit the value
679# leads nowhere (None).
680
681def guard(b: Bool, m: Maybe<&2, Why>) -> Maybe<&2, Why>:
682 match b:
683 case True{}:
684 m
685 case False{}:
686 None{}
687
688# The same two reasons at an SNatIn and an SBool, replayed along a path: the
689# value's own kind is the defect when the path ends here, and it is not a
690# defect at all further along (the walk passed it).
691def nat_in_defect(+lo: Nat, +hi: Nat, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
692 match r p:
693 case RNum{+n} Nil{}:
694 guard(Bool.not(num_ok(lo, hi, n)), Some{NotIn{lo, hi}})
695 case RNum{n} st <> q:
696 None{}
697 case x Nil{}:
698 Some{missing_or(x, NotNat{})}
699 case x st <> q:
700 None{}
701
702def bool_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
703 match r p:
704 case RBool{b} _:
705 None{}
706 case x Nil{}:
707 Some{missing_or(x, NotBool{})}
708 case x st <> q:
709 None{}
710
711# ---- a rule, its replay, and the closed forms ----
712#
713# A rule reports its first error with a path relative to the value it was
714# given. defect replays it by running the rule again: its path must be the
715# reported one (path_eq, which never compares two names), and the claim of
716# the accuracy law at an SRule is that the value conforms to the rule's
717# schema and the rule itself reported this error.
718
719def no_rule(tag: Nat, r: Raw) -> Maybe<&2, Err>:
720 None{}
721
722def first_why(m: Maybe<&2, Why>, +n: Maybe<&2, Why>) -> Maybe<&2, Why>:
723 match m:
724 case None{}:
725 n
726 case Some{w}:
727 Some{w}
728
729def step_eq(x: Step, y: Step) -> Bool:
730 match x y:
731 case AtIndex{i} AtIndex{j}:
732 Nat.is_eq(i, j)
733 case AtField{a, n} AtField{b, m}:
734 Bool.and(Nat.is_eq(a, b), String.eq(n, m))
735 case BoundAt{i, k} BoundAt{j, m}:
736 Bool.and(Nat.is_eq(i, j), String.eq(k, m))
737 case AtKey{k} AtKey{m}:
738 String.eq(k, m)
739 case _ _:
740 False{}
741
742def path_eq(x: List<&2, Step>, y: List<&2, Step>) -> Bool:
743 match x y:
744 case Nil{} Nil{}:
745 True{}
746 case a <> at b <> bt:
747 Bool.and(step_eq(a, b), path_eq(at, bt))
748 case _ _:
749 False{}
750
751def rule_defect(m: Maybe<&2, Err>, +p: List<&2, Step>) -> Maybe<&2, Why>:
752 match m:
753 case Some{Err{q, w}}:
754 guard(path_eq(q, p), Some{w})
755 case None{}:
756 None{}
757
758def not_list(x: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
759 match p:
760 case Nil{}:
761 Some{missing_or(x, NotList{})}
762 case st <> q:
763 None{}
764
765def not_object(x: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
766 match p:
767 case Nil{}:
768 Some{missing_or(x, NotObject{})}
769 case st <> q:
770 None{}
771
772def nat_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
773 match r p:
774 case RNum{n} _:
775 None{}
776 case x Nil{}:
777 Some{missing_or(x, NotNat{})}
778 case x st <> q:
779 None{}
780
781def str_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
782 match r p:
783 case RStr{x} _:
784 None{}
785 case x Nil{}:
786 Some{missing_or(x, NotString{})}
787 case x st <> q:
788 None{}
789
790def pick_why(b: Bool, +x: Maybe<&2, Why>, +y: Maybe<&2, Why>) -> Maybe<&2, Why>:
791 match b:
792 case True{}:
793 x
794 case False{}:
795 y
796
797def true_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
798 match r p:
799 case RBool{True{}} _:
800 None{}
801 case RBool{False{}} Nil{}:
802 Some{NotTrue{}}
803 case x Nil{}:
804 Some{missing_or(x, NotTrue{})}
805 case x st <> q:
806 None{}
807
808def enum_defect(names: List<&2, String>, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
809 match r p:
810 case RStr{x} Nil{}:
811 guard(Bool.not(in_names(x, names)), Some{NotOneOf{}})
812 case RStr{x} st <> q:
813 None{}
814 case x Nil{}:
815 Some{missing_or(x, NotOneOf{})}
816 case x st <> q:
817 None{}
818
819def no_variant(p: List<&2, Step>) -> Maybe<&2, Why>:
820 match p:
821 case Nil{}:
822 Some{NoVariant{}}
823 case st <> q:
824 None{}
825
826# The claim about a second key: every key passed is absent, and the key the
827# path names is there.
828def dup_defect(s: Schema, +r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
829 match s p:
830 case SVariant{+n2, vs, rr} AtField{0n, m} <> Nil{}:
831 guard(Bool.and(String.eq(m, n2), Bool.not(is_missing(lookup(n2, r)))), Some{TwoVariants{}})
832 case SVariant{+n2, vs, rr} AtField{1n+j, m} <> q:
833 guard(is_missing(lookup(n2, r)), dup_defect(rr, r, AtField{j, m} <> q))
834 case _ _:
835 None{}
836
837def at_end(w: Why, p: List<&2, Step>) -> Maybe<&2, Why>:
838 match p:
839 case Nil{}:
840 Some{w}
841 case st <> q:
842 None{}
843
844# At a strict object the path is one key, and the replay checks it on its
845# own: the key is there, and it is not one of the names.
846def extra_defect(ns: List<&2, String>, +r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
847 match p:
848 case AtKey{+k} <> Nil{}:
849 guard(Bool.and(has_key(k, r), Bool.not(in_names(k, ns))), Some{UnknownKey{}})
850 case _:
851 None{}
852
853def tag_defect(+k: String, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
854 match r p:
855 case REnd{} AtKey{j} <> Nil{}:
856 guard(String.eq(j, k), Some{Missing{}})
857 case RKey{+j, +v, +o} AtKey{i} <> Nil{}:
858 guard(String.eq(i, k), Some{missing_or(lookup(k, RKey{j, v, o}), NotOneOf{})})
859 case REnd{} q:
860 None{}
861 case RKey{j, v, o} q:
862 None{}
863 case x Nil{}:
864 Some{missing_or(x, NotObject{})}
865 case x q:
866 None{}
867
868# The tag key of a tagged case, taken twice, as defect replays it. check
869# reports it before the case's own schema is walked -- there is no place in the
870# schema for the second occurrence -- so the path is one field step at the
871# tag's own name and nothing after it. b is whether the key is not read once,
872# so nothing is reported exactly when key_once holds; a path of any other shape
873# is the case's own report, which the walk below answers.
874def tag_key_defect(b: Bool, +k: String, p: List<&2, Step>) -> Maybe<&2, Why>:
875 match b p:
876 case False{} q:
877 None{}
878 case True{} AtField{0n, +j} <> Nil{}:
879 pick_why(String.eq(j, k), Some{RepeatedKey{k}}, None{})
880 case True{} q:
881 None{}
882
883def defect(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>, p: List<&2, Step>) -> Maybe<&2, Why>:
884 match s r p:
885 case SNat{} x q:
886 nat_defect(x, q)
887 case SStr{} x q:
888 str_defect(x, q)
889 case SNatIn{+lo, +hi} x q:
890 nat_in_defect(lo, hi, x, q)
891 case SStrLen{+lo, +hi, +s2} +x +q:
892 pick_why(conforms(~rule, s2, x, prev), rule_defect(len_err(lo, hi, x), q), defect(~rule, s2, x, prev, q))
893 case SListLen{+lo, +hi, +s2} +r +q:
894 # The count came first in check, so the count's own error is the one
895 # reported here exactly when there was one to report -- for a list out of
896 # bounds and for a value that is not a list at all (list_len_ok is False
897 # for both, and count_err reported something for both).
898 pick_why(Bool.not(list_len_ok(lo, hi, r)), rule_defect(count_err(lo, hi, r), q), defect(~rule, s2, r, None{}, q))
899 case SOpt{inner} RNull{} q:
900 None{}
901 case SOpt{inner} x q:
902 defect(~rule, inner, x, None{}, q)
903 case SOptional{inner} RMissing{} q:
904 None{} # absent is not wrong, at this path or below it
905 case SOptional{inner} x q:
906 defect(~rule, inner, x, None{}, q)
907 case SList{e} RNil{} q:
908 None{}
909 case SList{e} RCons{h, t} AtIndex{0n} <> q:
910 defect(~rule, e, h, None{}, q)
911 case SList{+e} RCons{h, t} AtIndex{1n+j} <> q:
912 guard(conforms(~rule, e, h, None{}), defect(~rule, SList{e}, t, None{}, AtIndex{j} <> q))
913 case SList{+e} RCons{h, t} q:
914 guard(conforms(~rule, e, h, None{}), defect(~rule, SList{e}, t, None{}, q))
915 case SList{e} x q:
916 not_list(x, q)
917 case SField{+name, fs, rest} REnd{} AtField{0n, n} <> q:
918 guard(String.eq(n, name), defect(~rule, fs, RMissing{}, None{}, q))
919 case SField{+name, fs, rest} REnd{} AtField{1n+k, n} <> q:
920 guard(conforms(~rule, fs, RMissing{}, None{}), defect(~rule, rest, REnd{}, None{}, AtField{k, n} <> q))
921 case SField{+name, fs, rest} REnd{} q:
922 guard(conforms(~rule, fs, RMissing{}, None{}), defect(~rule, rest, REnd{}, None{}, q))
923 case SField{+name, fs, rest} RKey{+k, +v, +o} AtField{0n, n} <> +q:
924 pick_why(Bool.not(key_once(name, RKey{k, v, o})), at_end(RepeatedKey{name}, q), guard(String.eq(n, name), defect(~rule, fs, lookup(name, RKey{k, v, o}), None{}, q)))
925 case SField{+name, fs, rest} RKey{+k, +v, +o} AtField{1n+j, n} <> q:
926 guard(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{j, n} <> q))
927 case SField{+name, fs, rest} RKey{+k, +v, +o} q:
928 guard(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), defect(~rule, rest, RKey{k, v, o}, None{}, q))
929 case SField{name, fs, rest} x q:
930 not_object(x, q)
931 case SEnd{} REnd{} q:
932 None{}
933 case SEnd{} RKey{k, v, o} q:
934 None{}
935 case SEnd{} x q:
936 not_object(x, q)
937 case SRule{+s2, +tag} +x +q:
938 pick_why(conforms(~rule, s2, x, prev), rule_defect(rule(tag, x), q), defect(~rule, s2, x, prev, q))
939 case SStrict{+s2} +x +q:
940 pick_why(conforms(~rule, s2, x, prev), extra_defect(key_names(s2), x, q), defect(~rule, s2, x, prev, q))
941 case STagged{+k, +n, cs, rest} +x +q:
942 pick_why(is_tag(k, n, x), first_why(tag_key_defect(Bool.not(key_once(k, x)), k, q), defect(~rule, cs, drop_key(k, x), None{}, q)), defect(~rule, rest, x, None{}, q))
943 case STagEnd{k} x q:
944 tag_defect(k, x, q)
945 case SBool{} x q:
946 bool_defect(x, q)
947 case STrue{} x q:
948 true_defect(x, q)
949 case SEnum{names} x q:
950 enum_defect(names, x, q)
951 case SVariant{+name, +vs, +rest} REnd{} AtField{1n+j, n} <> q:
952 defect(~rule, rest, REnd{}, None{}, AtField{j, n} <> q)
953 case SVariant{+name, +vs, +rest} REnd{} q:
954 defect(~rule, rest, REnd{}, None{}, q)
955 case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} AtField{0n, +n} <> +q:
956 pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{0n, n} <> q), pick_why(Bool.not(key_once(name, RKey{k, v, o})), at_end(RepeatedKey{name}, q), guard(String.eq(n, name), defect(~rule, vs, lookup(name, RKey{k, v, o}), None{}, q))))
957 case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} AtField{1n+j, +n} <> +q:
958 pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{j, n} <> q), guard(conforms(~rule, vs, lookup(name, RKey{k, v, o}), None{}), dup_defect(rest, RKey{k, v, o}, AtField{j, n} <> q)))
959 case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} +q:
960 pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, q), None{})
961 case SVariant{+name, +vs, +rest} x q:
962 not_object(x, q)
963 case SVEnd{} REnd{} q:
964 no_variant(q)
965 case SVEnd{} RKey{k, v, o} q:
966 no_variant(q)
967 case SVEnd{} x q:
968 not_object(x, q)
969 case STuple{ts, rest} RCons{h, t} AtIndex{0n} <> q:
970 defect(~rule, ts, h, None{}, q)
971 case STuple{+ts, rest} RCons{h, t} AtIndex{1n+j} <> q:
972 guard(conforms(~rule, ts, h, None{}), defect(~rule, rest, t, None{}, AtIndex{j} <> q))
973 case STuple{+ts, rest} RCons{h, t} q:
974 guard(conforms(~rule, ts, h, None{}), defect(~rule, rest, t, None{}, q))
975 case STuple{ts, rest} RNil{} q:
976 at_end(TooShort{}, q)
977 case STuple{ts, rest} x q:
978 not_list(x, q)
979 case STEnd{} RNil{} q:
980 None{}
981 case STEnd{} RCons{h, t} q:
982 at_end(TooLong{}, q)
983 case STEnd{} x q:
984 not_list(x, q)
985
986# The closed forms: template defs cannot cross the bundler, so the host
987# calls these (a project with no rules).
988
989def check0(s: Schema, r: Raw) -> Maybe<&2, Err>:
990 check(~no_rule, s, r, None{})
991
992def conforms0(s: Schema, r: Raw) -> Bool:
993 conforms(~no_rule, s, r, None{})
994
995# ---- the claims the choice laws make ----
996#
997# A second reading of a variant chain, by counting: the value is an object,
998# exactly one of the chain's keys is in it, and every key that is there holds
999# a value that conforms. A key that is there is read the way conforms reads
1000# it, key_once included: a key the chain names, taken twice, is not read once,
1001# so the counting reading refuses it exactly where conforms does.
1002
1003def is_chain(s: Schema) -> Bool:
1004 match s:
1005 case SVariant{n, vs, rest}:
1006 is_chain(rest)
1007 case SVEnd{}:
1008 True{}
1009 case _:
1010 False{}
1011
1012def is_object(r: Raw) -> Bool:
1013 match r:
1014 case REnd{}:
1015 True{}
1016 case RKey{k, v, o}:
1017 True{}
1018 case _:
1019 False{}
1020
1021def one_if_there(b: Bool) -> Nat:
1022 match b:
1023 case True{}:
1024 0n
1025 case False{}:
1026 1n
1027
1028def count_present(s: Schema, +r: Raw) -> Nat:
1029 match s:
1030 case SVariant{+n, vs, rest}:
1031 Nat.add(one_if_there(is_missing(lookup(n, r))), count_present(rest, r))
1032 case _:
1033 0n
1034
1035def present_conform(~rule: Nat -> Raw -> Maybe<&2, Err>, +s: Schema, +r: Raw) -> Bool:
1036 match s:
1037 case SVariant{+n, vs, rest}:
1038 pick_bool(is_missing(lookup(n, r)), present_conform(~rule, rest, r), Bool.and(key_once(n, r), Bool.and(conforms(~rule, vs, lookup(n, r), None{}), present_conform(~rule, rest, r))))
1039 case _:
1040 True{}
1041
1042# ---- the claim the tuple law makes ----
1043#
1044# A second reading of a tuple, over plain lists: the schema is built from a
1045# list of schemas, and the value conforms when it is a list of the same
1046# length and each position conforms to the schema at the same position.
1047
1048def tuple_of(ss: List<&2, Schema>) -> Schema:
1049 match ss:
1050 case Nil{}:
1051 STEnd{}
1052 case h <> t:
1053 STuple{h, tuple_of(t)}
1054
1055# raw_list and raw_len (a list, and how many elements it has) sit with the
1056# other bound helpers, above: an SListLen's test reads them.
1057
1058def at_raw(r: Raw, +i: Nat) -> Raw:
1059 match r i:
1060 case RCons{h, t} 0n:
1061 h
1062 case RCons{h, t} 1n+j:
1063 at_raw(t, j)
1064 case _ _:
1065 RMissing{}
1066
1067def each_pos(~rule: Nat -> Raw -> Maybe<&2, Err>, ss: List<&2, Schema>, +r: Raw, +i: Nat) -> Bool:
1068 match ss:
1069 case Nil{}:
1070 True{}
1071 case h <> t:
1072 Bool.and(conforms(~rule, h, at_raw(r, i), None{}), each_pos(~rule, t, r, 1n+i))
1073
1074# ---- the claim the strict law makes ----
1075#
1076# How many keys of r are not in ns, counted rather than walked with a
1077# Bool.and: a second algorithm, so that a no_extra that lets a key through
1078# (or refuses a named one) disagrees with it.
1079def count_unknown(+ns: List<&2, String>, r: Raw) -> Nat:
1080 match r:
1081 case RKey{+k, v, o}:
1082 Nat.add(one_if_there(in_names(k, ns)), count_unknown(ns, o))
1083 case _:
1084 0n
1085
1086# ---- a schema's meaning, and reading a value into it ----
1087#
1088# Meaning(s) is the Bend type a schema describes: a record is its fields,
1089# nested pairs ending in Unit; a variant chain is nested Eithers ending in
1090# Empty; a value that may be null (SOpt) or absent (SOptional) is a Maybe. A
1091# rule refines a shape and does not change its meaning. `enc` writes a
1092# meaning as the host's JSON would be; `dec` reads one back. Both are written
1093# once, for every schema, and LAWS.bend proves the round trip once.
1094#
1095# dec is a reader, not a check: run it on a value check accepted
1096# (checked_decodes says it then succeeds). On a value check refuses it may
1097# still read something, since a record reads its keys and ignores the rest.
1098#
1099# The round trip needs a well-formed schema (wf): a key named once in its
1100# object or chain (lookup reads the first), and an optional value that is not
1101# itself nullable (Some{None} and None would both be written null).
1102
1103type Both<A: Data, B: Data> is Data:
1104 Both{a: A, b: B}
1105
1106def Meaning(s: Schema) -> Data:
1107 match s:
1108 case SNat{}:
1109 Nat
1110 case SNatIn{lo, hi}:
1111 Nat
1112 case SStr{}:
1113 String
1114 case SStrLen{lo, hi, s2}:
1115 Meaning(s2)
1116 case SListLen{lo, hi, s2}:
1117 Meaning(s2)
1118 case SOpt{i}:
1119 Maybe<&2, Meaning(i)>
1120 case SOptional{i}:
1121 Maybe<&2, Meaning(i)>
1122 case SList{e}:
1123 List<&2, Meaning(e)>
1124 case SField{n, fs, rest}:
1125 Both<Meaning(fs), Meaning(rest)>
1126 case SEnd{}:
1127 Unit
1128 case SRule{s2, tag}:
1129 Meaning(s2)
1130 case SStrict{s2}:
1131 Meaning(s2)
1132 case STagged{k, n, cs, rest}:
1133 Either<&2, &2, Meaning(cs), Meaning(rest)>
1134 case STagEnd{k}:
1135 Empty
1136 case SBool{}:
1137 Bool
1138 case STrue{}:
1139 Unit
1140 case SEnum{names}:
1141 String
1142 case SVariant{n, vs, rest}:
1143 Either<&2, &2, Meaning(vs), Meaning(rest)>
1144 case SVEnd{}:
1145 Empty
1146 case STuple{ts, rest}:
1147 Both<Meaning(ts), Meaning(rest)>
1148 case STEnd{}:
1149 Unit
1150
1151def enc(s: Schema, x: Meaning(s)) -> Raw:
1152 match s x:
1153 case SNat{} n:
1154 RNum{n}
1155 case SNatIn{lo_, hi_} n:
1156 RNum{n}
1157 case SStr{} x:
1158 RStr{x}
1159 case SStrLen{lo_, hi_, s2} v:
1160 enc(s2, v)
1161 case SListLen{lo_, hi_, s2} v:
1162 enc(s2, v)
1163 case SOpt{i} None{}:
1164 RNull{}
1165 case SOpt{i} Some{v}:
1166 enc(i, v)
1167 case SOptional{i} None{}:
1168 RMissing{} # absent: the host writes no key where this one lands
1169 case SOptional{i} Some{v}:
1170 enc(i, v)
1171 case SList{e} Nil{}:
1172 RNil{}
1173 case SList{+e} h <> t:
1174 RCons{enc(e, h), enc(SList{e}, t)}
1175 case SField{n, fs, rest} Both{a, b}:
1176 RKey{n, enc(fs, a), enc(rest, b)}
1177 case SEnd{} Unit{}:
1178 REnd{}
1179 case SRule{s2, tag} v:
1180 enc(s2, v)
1181 case SStrict{s2} v:
1182 enc(s2, v)
1183 case STagged{k, n, cs, rest} Inl{a}:
1184 RKey{k, RStr{n}, enc(cs, a)}
1185 case STagged{k, n, cs, rest} Inr{b}:
1186 enc(rest, b)
1187 case STagEnd{k} e:
1188 Empty.absurd(Raw, e)
1189 case STrue{} Unit{}:
1190 RBool{True{}}
1191 case SBool{} b:
1192 RBool{b}
1193 case SEnum{names} x:
1194 RStr{x}
1195 case SVariant{n, vs, rest} Inl{a}:
1196 RKey{n, enc(vs, a), REnd{}}
1197 case SVariant{n, vs, rest} Inr{b}:
1198 enc(rest, b)
1199 case SVEnd{} e:
1200 Empty.absurd(Raw, e)
1201 case STuple{ts, rest} Both{a, b}:
1202 RCons{enc(ts, a), enc(rest, b)}
1203 case STEnd{} Unit{}:
1204 RNil{}
1205
1206def lcons(-A: Data, h: Maybe<&2, A>, t: Maybe<&2, List<&2, A>>) -> Maybe<&2, List<&2, A>>:
1207 match h t:
1208 case Some{x} Some{xs}:
1209 Some{x <> xs}
1210 case _ _:
1211 None{}
1212
1213def both(-A: Data, -B: Data, p: Maybe<&2, A>, q: Maybe<&2, B>) -> Maybe<&2, Both<A, B>>:
1214 match p q:
1215 case Some{x} Some{y}:
1216 Some{Both{x, y}}
1217 case _ _:
1218 None{}
1219
1220def opt_some(-A: Data, m: Maybe<&2, A>) -> Maybe<&2, Maybe<&2, A>>:
1221 match m:
1222 case Some{v}:
1223 Some{Some{v}}
1224 case None{}:
1225 None{}
1226
1227def map_inl(-A: Data, -B: Data, m: Maybe<&2, A>) -> Maybe<&2, Either<&2, &2, A, B>>:
1228 match m:
1229 case Some{v}:
1230 Some{Inl{v}}
1231 case None{}:
1232 None{}
1233
1234def map_inr(-A: Data, -B: Data, m: Maybe<&2, B>) -> Maybe<&2, Either<&2, &2, A, B>>:
1235 match m:
1236 case Some{v}:
1237 Some{Inr{v}}
1238 case None{}:
1239 None{}
1240
1241def pick_m(-A: Data, b: Bool, x: A, y: A) -> A:
1242 match b:
1243 case True{}:
1244 x
1245 case False{}:
1246 y
1247
1248def true_unit(b: Bool) -> Maybe<&2, Unit>:
1249 match b:
1250 case True{}:
1251 Some{Unit{}}
1252 case False{}:
1253 None{}
1254
1255def nullish(r: Raw) -> Bool:
1256 match r:
1257 case RNull{}:
1258 True{}
1259 case RMissing{}:
1260 True{}
1261 case _:
1262 False{}
1263
1264def dec(s: Schema, r: Raw) -> Maybe<&2, Meaning(s)>:
1265 match s r:
1266 case SNat{} RNum{n}:
1267 Some{n}
1268 case SNatIn{lo_, hi_} RNum{n}:
1269 Some{n}
1270 case SStr{} RStr{x}:
1271 Some{x}
1272 case SStrLen{lo_, hi_, s2} x:
1273 dec(s2, x)
1274 case SListLen{lo_, hi_, s2} x:
1275 dec(s2, x)
1276 case SOpt{+i} +x:
1277 pick_m(Maybe<&2, Maybe<&2, Meaning(i)>>, nullish(x), Some{None{}}, opt_some(Meaning(i), dec(i, x)))
1278 case SOptional{+i} +x:
1279 pick_m(Maybe<&2, Maybe<&2, Meaning(i)>>, is_missing(x), Some{None{}}, opt_some(Meaning(i), dec(i, x)))
1280 case SList{e} RNil{}:
1281 Some{Nil{}}
1282 case SList{+e} RCons{h, t}:
1283 lcons(Meaning(e), dec(e, h), dec(SList{e}, t))
1284 case SField{+n, +fs, +rest} +x:
1285 both(Meaning(fs), Meaning(rest), dec(fs, lookup(n, x)), dec(rest, x))
1286 case SEnd{} x:
1287 Some{Unit{}}
1288 case SRule{s2, tag} x:
1289 dec(s2, x)
1290 case SStrict{s2} x:
1291 dec(s2, x)
1292 case STagged{+k, +n, +cs, +rest} +x:
1293 pick_m(Maybe<&2, Either<&2, &2, Meaning(cs), Meaning(rest)>>, is_tag(k, n, x), map_inl(Meaning(cs), Meaning(rest), dec(cs, drop_key(k, x))), map_inr(Meaning(cs), Meaning(rest), dec(rest, x)))
1294 case STrue{} RBool{b}:
1295 true_unit(b)
1296 case SBool{} RBool{b}:
1297 Some{b}
1298 case SEnum{names} RStr{x}:
1299 Some{x}
1300 case SVariant{+n, +vs, +rest} +x:
1301 pick_m(Maybe<&2, Either<&2, &2, Meaning(vs), Meaning(rest)>>, is_missing(lookup(n, x)), map_inr(Meaning(vs), Meaning(rest), dec(rest, x)), map_inl(Meaning(vs), Meaning(rest), dec(vs, lookup(n, x))))
1302 case STuple{+ts, +rest} RCons{h, t}:
1303 both(Meaning(ts), Meaning(rest), dec(ts, h), dec(rest, t))
1304 case STEnd{} RNil{}:
1305 Some{Unit{}}
1306 case _ _:
1307 None{}
1308
1309# ---- a well-formed schema ----
1310#
1311# wf is what the round trip needs: a key named once in its object or chain
1312# (lookup reads the first), an optional value that is not itself nullable, and
1313# a tagged case whose own schema leaves the tag key alone.
1314# Three constructors ask more than their own shape:
1315#
1316# STagged writes its key and then the case's own object beside it, so the
1317# case's schema may not put that key anywhere in the same object (no_key).
1318# A case that names its own tag key encodes to a document holding the key
1319# twice: enc writes the tag and the case's own field writes it again, and
1320# the host builds that document as a JS object, where the second write --
1321# the spread of the case's own fields -- overwrites the first. What the
1322# encoder wrote is then not what the decoder reads, so refusing the schema
1323# is what keeps encode_conforms true.
1324#
1325# SOptional is where a field may be absent, so it belongs immediately under
1326# a field and nowhere else: every other place a schema sits is guarded by
1327# opt_at, which asks whether an absent value can reach the top of what enc
1328# writes for it. That excludes an SOptional anywhere but a field's schema,
1329# and also a schema that would pass one straight through (SOpt{SOptional{i}}
1330# writes RMissing for Some{None}, where nothing can tell it from an absent
1331# key). An SOptional's own inner is guarded the same way: None and
1332# Some{None} would both be written as an absent key.
1333#
1334# SOpt's inner may not be nullable at all (its own None and the inner's null
1335# would both be written null), and nullable asks an SOptional too.
1336
1337# An absent value reaches the top of what enc writes for s: s is an SOptional,
1338# or it hands the value it was given straight to a schema that is (a rule, a
1339# strict object, a bound, or the tail of a variant or tagged chain -- and an
1340# SOpt, whose Some case passes the value through). Everything else wraps what
1341# it writes in a constructor of its own, so an absent value cannot surface.
1342def opt_at(s: Schema) -> Bool:
1343 match s:
1344 case SOptional{i}:
1345 True{}
1346 case SOpt{i}:
1347 opt_at(i)
1348 case SRule{s2, tag}:
1349 opt_at(s2)
1350 case SStrict{s2}:
1351 opt_at(s2)
1352 case SStrLen{lo, hi, s2}:
1353 opt_at(s2)
1354 case SListLen{lo, hi, s2}:
1355 opt_at(s2)
1356 case STagged{k, n, cs, rest}:
1357 opt_at(rest)
1358 case SVariant{n, vs, rest}:
1359 opt_at(rest)
1360 case _:
1361 False{}
1362
1363def nullable(s: Schema) -> Bool:
1364 match s:
1365 case SOpt{i}:
1366 True{}
1367 case SOptional{i}:
1368 True{} # absent and the inner's own null read as the same None
1369 case SRule{s2, tag}:
1370 nullable(s2)
1371 case SStrict{s2}:
1372 nullable(s2)
1373 case SStrLen{lo, hi, s2}:
1374 nullable(s2)
1375 case SListLen{lo, hi, s2}:
1376 nullable(s2)
1377 case STagged{k, n, cs, rest}:
1378 nullable(rest)
1379 case SVariant{n, vs, rest}:
1380 nullable(rest)
1381 case _:
1382 False{}
1383
1384# ---- the object a schema's encoding lands in ----
1385#
1386# enc writes an object as one flat chain of keys. An SField writes its name and
1387# its rest continues that object; an SVariant writes its name and the value
1388# under it is a chain of its own (REnd ends it, so it is a value and not a
1389# continuation). A wrapper -- a rule, a strict object, a bound, an optional --
1390# writes no key of its own and hands its value straight to its inner schema,
1391# so a key reaches the top of the object from inside any of them. A tagged
1392# case's schema is the same object the tag key was written into, and so is the
1393# rest of its chain.
1394#
1395# no_key is that, written down: k does not reach the top of the object enc
1396# builds for s, for any value of s. wf asks it of a tagged case's own schema,
1397# which is what keeps the tag key from being written twice.
1398def no_key(+k: String, s: Schema) -> Bool:
1399 match s:
1400 case SField{+n, fs, rest}:
1401 Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
1402 case SVariant{+n, vs, rest}:
1403 Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
1404 case SStrict{s2}:
1405 no_key(k, s2)
1406 case SRule{s2, tag}:
1407 no_key(k, s2)
1408 case SStrLen{lo, hi, s2}:
1409 no_key(k, s2)
1410 case SListLen{lo, hi, s2}:
1411 no_key(k, s2)
1412 case SOpt{i}:
1413 no_key(k, i)
1414 case SOptional{i}:
1415 no_key(k, i)
1416 case STagged{+k2, n2, cs2, rest2}:
1417 Bool.and(Bool.not(String.eq(k2, k)), Bool.and(Bool.not(String.eq(k, k2)), Bool.and(no_key(k, cs2), no_key(k, rest2))))
1418 case _:
1419 True{}
1420
1421# n is not a key of the record chain s (a chain ends in SEnd). Both orders are
1422# asked, as fresh_v asks them: which of the two names a step puts first depends
1423# on which of them is the value's key there, and asking both spares a proof
1424# that String.eq is symmetric.
1425def fresh_f(+n: String, s: Schema) -> Bool:
1426 match s:
1427 case SField{+m, fs, rest}:
1428 Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_f(n, rest)))
1429 case SEnd{}:
1430 True{}
1431 case _:
1432 False{}
1433
1434# n is not a key of the variant chain s (a chain ends in SVEnd). Both orders
1435# are asked: reading a key compares the names one way, reading past it the
1436# other, and asking both spares a proof that String.eq is symmetric.
1437def fresh_v(+n: String, s: Schema) -> Bool:
1438 match s:
1439 case SVariant{+m, vs, rest}:
1440 Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_v(n, rest)))
1441 case SVEnd{}:
1442 True{}
1443 case _:
1444 False{}
1445
1446# A record chain (ending in SEnd) or a variant chain (ending in SVEnd): what
1447# SStrict may wrap, so every key its encoding writes is a declared name.
1448# A chain of keys (SField or SVariant links, ending in SEnd or SVEnd): what
1449# SStrict may wrap, so every key its encoding writes is a name it declares.
1450def is_keyed(s: Schema) -> Bool:
1451 match s:
1452 case SField{n, fs, rest}:
1453 is_keyed(rest)
1454 case SEnd{}:
1455 True{}
1456 case SVariant{n, vs, rest}:
1457 is_keyed(rest)
1458 case SVEnd{}:
1459 True{}
1460 case _:
1461 False{}
1462
1463# n names no case of the tagged chain s, whose key is k, and the chain ends
1464# in STagEnd{k}: one key for the whole chain.
1465def fresh_t(+k: String, +n: String, s: Schema) -> Bool:
1466 match s:
1467 case STagged{+k2, +m, cs, rest}:
1468 Bool.and(String.eq(k2, k), Bool.and(Bool.not(String.eq(m, n)), fresh_t(k, n, rest)))
1469 case STagEnd{k2}:
1470 String.eq(k2, k)
1471 case _:
1472 False{}
1473
1474def wf(s: Schema) -> Bool:
1475 match s:
1476 case SOpt{+i}:
1477 Bool.and(Bool.not(nullable(i)), wf(i))
1478 case SOptional{+i}:
1479 Bool.and(Bool.not(opt_at(i)), wf(i))
1480 case SList{+e}:
1481 Bool.and(Bool.not(opt_at(e)), wf(e))
1482 case SListLen{lo_, hi_, +s2}:
1483 Bool.and(Bool.not(opt_at(s2)), wf(s2))
1484 case SStrLen{lo_, hi_, +s2}:
1485 Bool.and(Bool.not(opt_at(s2)), wf(s2))
1486 case SField{+n, fs, +rest}:
1487 Bool.and(wf(fs), Bool.and(fresh_f(n, rest), wf(rest)))
1488 case SRule{+s2, tag}:
1489 Bool.and(Bool.not(opt_at(s2)), wf(s2))
1490 case SStrict{+s2}:
1491 Bool.and(is_keyed(s2), Bool.and(Bool.not(opt_at(s2)), wf(s2)))
1492 case STagged{+k, +n, +cs, +rest}:
1493 Bool.and(Bool.not(opt_at(cs)), Bool.and(wf(cs), Bool.and(no_key(k, cs), Bool.and(fresh_t(k, n, rest), wf(rest)))))
1494 case SVariant{+n, +vs, +rest}:
1495 Bool.and(Bool.not(opt_at(vs)), Bool.and(wf(vs), Bool.and(fresh_v(n, rest), wf(rest))))
1496 case STuple{+ts, +rest}:
1497 Bool.and(Bool.not(opt_at(ts)), Bool.and(wf(ts), Bool.and(Bool.not(opt_at(rest)), wf(rest))))
1498 case _:
1499 True{}
1500
1501# Every enum value in x is one of its names (encode_conforms' premise).
1502def names_ok(s: Schema, x: Meaning(s)) -> Bool:
1503 match s x:
1504 case SOpt{i} None{}:
1505 True{}
1506 case SOpt{i} Some{v}:
1507 names_ok(i, v)
1508 case SList{e} Nil{}:
1509 True{}
1510 case SList{+e} h <> t:
1511 Bool.and(names_ok(e, h), names_ok(SList{e}, t))
1512 case SField{n, fs, rest} Both{a, b}:
1513 Bool.and(names_ok(fs, a), names_ok(rest, b))
1514 case SRule{s2, tag} v:
1515 names_ok(s2, v)
1516 case SStrict{s2} v:
1517 names_ok(s2, v)
1518 case SStrLen{lo_, hi_, s2} v:
1519 names_ok(s2, v)
1520 case SListLen{lo_, hi_, s2} v:
1521 names_ok(s2, v)
1522 case SOptional{i} None{}:
1523 True{}
1524 case SOptional{i} Some{v}:
1525 names_ok(i, v)
1526 case STagged{k, n, cs, rest} Inl{a}:
1527 names_ok(cs, a)
1528 case STagged{k, n, cs, rest} Inr{b}:
1529 names_ok(rest, b)
1530 case SEnum{names} x:
1531 in_names(x, names)
1532 case SVariant{n, vs, rest} Inl{a}:
1533 names_ok(vs, a)
1534 case SVariant{n, vs, rest} Inr{b}:
1535 names_ok(rest, b)
1536 case STuple{ts, rest} Both{a, b}:
1537 Bool.and(names_ok(ts, a), names_ok(rest, b))
1538 case _ _:
1539 True{}
1540
1541# Every bound a constructor states holds of the value that will be written, at
1542# every place one sits in the schema (encode_conforms' second premise, beside
1543# names_ok). The encoder writes the meaning unchanged, so a value outside a
1544# bound is written out as it is and refused by check on the way back: the host
1545# that built it is at fault, and this is where it says so. An SStrLen's bound
1546# is read off the string its own schema writes, and an SListLen's count off the
1547# list it writes, which is why enc appears here.
1548def bounds_ok(s: Schema, x: Meaning(s)) -> Bool:
1549 match s x:
1550 case SOpt{i} None{}:
1551 True{}
1552 case SOpt{i} Some{v}:
1553 bounds_ok(i, v)
1554 case SList{e} Nil{}:
1555 True{}
1556 case SList{+e} h <> t:
1557 Bool.and(bounds_ok(e, h), bounds_ok(SList{e}, t))
1558 case SField{n, fs, rest} Both{a, b}:
1559 Bool.and(bounds_ok(fs, a), bounds_ok(rest, b))
1560 case SRule{s2, tag} v:
1561 bounds_ok(s2, v)
1562 case SStrict{s2} v:
1563 bounds_ok(s2, v)
1564 case STagged{k, n, cs, rest} Inl{a}:
1565 bounds_ok(cs, a)
1566 case STagged{k, n, cs, rest} Inr{b}:
1567 bounds_ok(rest, b)
1568 case SNatIn{+lo, +hi} n:
1569 num_ok(lo, hi, n)
1570 case SStrLen{+lo, +hi, +s2} +v:
1571 Bool.and(bounds_ok(s2, v), len_ok(lo, hi, enc(s2, v)))
1572 case SListLen{+lo, +hi, +s2} +v:
1573 Bool.and(bounds_ok(s2, v), list_len_ok(lo, hi, enc(s2, v)))
1574 case SOptional{i} None{}:
1575 True{}
1576 case SOptional{i} Some{v}:
1577 bounds_ok(i, v)
1578 case SVariant{n, vs, rest} Inl{a}:
1579 bounds_ok(vs, a)
1580 case SVariant{n, vs, rest} Inr{b}:
1581 bounds_ok(rest, b)
1582 case STuple{ts, rest} Both{a, b}:
1583 Bool.and(bounds_ok(ts, a), bounds_ok(rest, b))
1584 case _ _:
1585 True{}