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