def nfa.dead

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

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

2958# no position active: nothing accepted
2959def nfa.dead(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +s: List<&2, U32>, +e: {G.AaGNfa.alive(bs) == False{} : Bool}) -> {G.AaGNfa.sem(seq, bs, s) == False{} : Bool}:
2960  match seq:
2961    case Nil{}:
2962      match bs:
2963        case Nil{}:
2964          {==}
2965        case Con{b, rest}:
2966          match b:
2967            case True{}:
2968              b.absurd_tf(Bool, G.AaGNfa.sem(Nil{}, Con{True{}, rest}, s), False{}, e)
2969            case False{}:
2970              {==}
2971    case Con{tok, r}:
2972      match bs:
2973        case Nil{}:
2974          nfa.dead(r, Nil{}, s, {==})
2975        case Con{b, rest}:
2976          match b:
2977            case True{}:
2978              b.absurd_tf(Bool, G.AaGNfa.sem(Con{tok, r}, Con{True{}, rest}, s), False{}, e)
2979            case False{}:
2980              nfa.dead(r, rest, s, e)