def names_ok

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

import Base

1864# Every enum value in x is one of its names (encode_conforms' premise).
1865def 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{}