def gr_char

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:146

import Base
import bend-osdev-apparmor@0.1.0.0/text.bend as X
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

146# a first piece that starts with h: a single-byte token takes h and leaves
147# an empty piece
148def gr_char(+c: U32, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_eq(h, c), fe_any(r, ds)) : Bool}:
149  match ds:
150    case Nil{}:
151      Equal.sym(Bool, Bool.and(U32.is_eq(h, c), False{}), False{}, b.and_false_r(U32.is_eq(h, c)))
152    case Con{d, t}:
153      match d:
154        case Nil{}:
155          gr_char(c, r, h, t)
156        case Con{p, ps}:
157          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_eq(h, c), fe_any(r, t)), gr_char(c, r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_eq(h, c), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_eq(h, c), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
158          b.factor(U32.is_eq(h, c), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))