Core.bounds_ok: def of bend-schema-lib@0.4.1.0
Import: import bend-schema-lib@0.4.1.0/core.bend as Core
Lines 1910-1962 of bend-schema-lib@0.4.1.0/core.bend: https://jend.leeeet.dev/read.txt?path=bend-schema-lib@0.4.1.0/core.bend&start_line=1910&end_line=1962

import Base

# Every bound a constructor states holds of the value that will be written, at
# every place one sits in the schema (encode_conforms' second premise, beside
# names_ok). The encoder writes the meaning unchanged, so a value outside a
# bound is written out as it is and refused by check on the way back: the host
# that built it is at fault, and this is where it says so. An SStrLen's bound
# is read off the string its own schema writes, and an SListLen's count off the
# list it writes, which is why enc appears here.
def bounds_ok(s: Schema, x: Meaning(s)) -> Bool:
  match s x:
    case SOpt{i} None{}:
      True{}
    case SOpt{i} Some{v}:
      bounds_ok(i, v)
    case SList{e} Nil{}:
      True{}
    case SList{+e} h <> t:
      Bool.and(bounds_ok(e, h), bounds_ok(SList{e}, t))
    case SField{n, fs, rest} Both{a, b}:
      Bool.and(bounds_ok(fs, a), bounds_ok(rest, b))
    case SRule{s2, tag} v:
      bounds_ok(s2, v)
    case SStrict{s2} v:
      bounds_ok(s2, v)
    case STagged{k, n, cs, rest} Inl{a}:
      bounds_ok(cs, a)
    case STagged{k, n, cs, rest} Inr{b}:
      bounds_ok(rest, b)
    case SNatIn{+lo, +hi} n:
      num_ok(lo, hi, n)
    case SStrLen{+lo, +hi, +s2} +v:
      Bool.and(bounds_ok(s2, v), len_ok(lo, hi, enc(s2, v)))
    case SListLen{+lo, +hi, +s2} +v:
      Bool.and(bounds_ok(s2, v), list_len_ok(lo, hi, enc(s2, v)))
    case SOptional{i} None{}:
      True{}
    case SOptional{i} Some{v}:
      bounds_ok(i, v)
    case SVariant{n, vs, rest} Inl{a}:
      bounds_ok(vs, a)
    case SVariant{n, vs, rest} Inr{b}:
      bounds_ok(rest, b)
    case STuple{ts, rest} Both{a, b}:
      Bool.and(bounds_ok(ts, a), bounds_ok(rest, b))
    case SJson{} value:
      valid_json(value)
    case SIntIn{+lo, +hi} i:
      int_ok(lo, hi, i)
    case SEither{l, r} Inl{a}:
      bounds_ok(l, a)
    case SEither{l, r} Inr{b}:
      bounds_ok(r, b)
    case _ _:
      True{}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Meaning
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Schema
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=enc
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=int_ok
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=len_ok
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=list_len_ok
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=num_ok
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=valid_json