def bounds_ok

bend-schema-lib@0.4.1.0 · core.bend:1910

import Base

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.
1917def 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{}