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