def gr_star

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

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

184# ... a star takes h if it is not '/', and goes on
185def gr_star(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, ds)) : Bool}:
186  match ds:
187    case Nil{}:
188      Equal.sym(Bool, Bool.and(U32.is_ne(h, 47), False{}), False{}, b.and_false_r(U32.is_ne(h, 47)))
189    case Con{d, t}:
190      match d:
191        case Nil{}:
192          gr_star(r, h, t)
193        case Con{p, ps}:
194          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t)), gr_star(r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_ne(h, 47), G.AaGPiece.no_slash(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_ne(h, 47), Bool.or(Bool.and(G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps)), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))) : Bool}
195          b.factor(U32.is_ne(h, 47), G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))