protect.bend source
protect.bend on the hub · documented module
# Markdown protect regions — port of bible-linkify protect.ts (pure Bend)# Length of protected span at suffix start, or 0n. Phase-carried Bools only.import Basedef char1(+c: Char) -> String: String.from_list(c <> Nil{})def str_drop_go(fuel: Nat, n: Nat, s: String) -> String: match fuel: case 0n: s case 1n+p: match n: case 0n: s case 1n+m: match s: case SNil{}: "" case SCon{h, t}: str_drop_go(p, m, t)def str_drop(+n: Nat, +s: String) -> String: str_drop_go(Nat.add(n, 1n), n, s)def str_take_go(fuel: Nat, n: Nat, s: String, acc: String) -> String: match fuel: case 0n: acc case 1n+p: match n: case 0n: acc case 1n+m: match s: case SNil{}: acc case SCon{+h, +t}: str_take_go(p, m, t, String.append(acc, char1(h)))def str_take(+n: Nat, +s: String) -> String: str_take_go(Nat.add(n, 1n), n, s, "")def is_newline(+c: Char) -> Bool: match c: case Chr{+code}: U32.is_eq(code, 10)def is_hyphen(+c: Char) -> Bool: match c: case Chr{+code}: U32.is_eq(code, 45)# --- Frontmatter ---# Port of protect.ts findFrontmatter: open "---\n" / "---\r\n",# close earliest of "\n---\n" | "\n---\r\n" | "\n---".type FmPh is Data: FmNeedNl{} FmNeedNlDec{nl: Bool, cr: Bool} FmNeedNlAfterCr{} FmNeedNlAfterCrDec{nl: Bool} FmScan{} FmScanDec{nl: Bool} FmDash1{} FmDash1Dec{is_dash: Bool, nl: Bool} FmDash1GoDash{} FmDash1GoNl{} FmDash1GoScan{} FmDash2{} FmDash2Dec{is_dash: Bool} FmDash3{} FmDash3Dec{is_dash: Bool} FmTail{} FmTailDec{nl: Bool, is_cr: Bool} FmTailAfterCr{} FmTailAfterCrDec{nl: Bool}def is_cr(+c: Char) -> Bool: match c: case Chr{+code}: U32.is_eq(code, 13)def pick_dash1_nl(nl: Bool) -> FmPh: match nl: case True{}: FmDash1GoNl{} case False{}: FmDash1GoScan{}def pick_dash1(is_dash: Bool, nl: Bool) -> FmPh: match is_dash: case True{}: FmDash1GoDash{} case False{}: pick_dash1_nl(nl)def frontmatter_go(fuel: Nat, ph: FmPh, +rest: String, +consumed: Nat) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case FmNeedNl{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmNeedNlDec{is_newline(h), is_cr(h)}, SCon{h, t}, consumed) case FmNeedNlDec{nl, cr}: match nl: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmScan{}, t, Nat.add(consumed, 1n)) case False{}: match cr: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmNeedNlAfterCr{}, t, Nat.add(consumed, 1n)) case False{}: 0n case FmNeedNlAfterCr{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmNeedNlAfterCrDec{is_newline(h)}, SCon{h, t}, consumed) case FmNeedNlAfterCrDec{nl}: match nl: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmScan{}, t, Nat.add(consumed, 1n)) case False{}: 0n case FmScan{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmScanDec{is_newline(h)}, SCon{h, t}, consumed) case FmScanDec{nl}: match nl: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmDash1{}, t, Nat.add(consumed, 1n)) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmScan{}, t, Nat.add(consumed, 1n)) case FmDash1{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmDash1Dec{is_hyphen(h), is_newline(h)}, SCon{h, t}, consumed) case FmDash1Dec{is_dash, nl}: frontmatter_go(p, pick_dash1(is_dash, nl), rest, consumed) case FmDash1GoDash{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmDash2{}, t, Nat.add(consumed, 1n)) case FmDash1GoNl{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmDash1{}, t, Nat.add(consumed, 1n)) case FmDash1GoScan{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmScan{}, t, Nat.add(consumed, 1n)) case FmDash2{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmDash2Dec{is_hyphen(h)}, SCon{h, t}, consumed) case FmDash2Dec{is_dash}: match is_dash: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmDash3{}, t, Nat.add(consumed, 1n)) case False{}: frontmatter_go(p, FmScan{}, rest, consumed) case FmDash3{}: match rest: case SNil{}: 0n case SCon{+h, +t}: frontmatter_go(p, FmDash3Dec{is_hyphen(h)}, SCon{h, t}, consumed) case FmDash3Dec{is_dash}: match is_dash: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: frontmatter_go(p, FmTail{}, t, Nat.add(consumed, 1n)) case False{}: frontmatter_go(p, FmScan{}, rest, consumed) case FmTail{}: match rest: case SNil{}: consumed case SCon{+h, +t}: frontmatter_go(p, FmTailDec{is_newline(h), is_cr(h)}, SCon{h, t}, consumed) case FmTailDec{nl, cr}: match nl: case True{}: Nat.add(consumed, 1n) case False{}: match cr: case True{}: frontmatter_go(p, FmTailAfterCr{}, rest, consumed) case False{}: consumed case FmTailAfterCr{}: match rest: case SNil{}: consumed case SCon{h, +t}: match t: case SNil{}: consumed case SCon{+h2, t2}: frontmatter_go(p, FmTailAfterCrDec{is_newline(h2)}, t, consumed) case FmTailAfterCrDec{nl}: match nl: case True{}: Nat.add(consumed, 2n) case False{}: consumeddef frontmatter_len_if(ok: Bool, +s: String) -> Nat: match ok: case False{}: 0n case True{}: frontmatter_go( Nat.add(Nat.mul(4n, String.length(s)), 16n), FmNeedNl{}, str_drop(3n, s), 3n )def frontmatter_len(+s: String) -> Nat: frontmatter_len_if(String.starts_with(s, "---"), s)# --- Fence ---type FsPh is Data: FsOpenRun{want_tick: Bool, +run: Nat} FsOpenDec{want_tick: Bool, +run: Nat, is_tick: Bool, ge3: Bool} FsSkipInfo{want_tick: Bool, +open_n: Nat, +acc: Nat} FsSkipDec{want_tick: Bool, +open_n: Nat, +acc: Nat, nl: Bool} FsBody{want_tick: Bool, +open_n: Nat, +acc: Nat, at_bol: Bool} FsBodyDec{want_tick: Bool, +open_n: Nat, +acc: Nat, at_bol: Bool, is_tick: Bool, nl: Bool} FsCloseRun{want_tick: Bool, +open_n: Nat, +acc: Nat, +run: Nat} FsCloseDec{want_tick: Bool, +open_n: Nat, +acc: Nat, +run: Nat, is_tick: Bool, ge: Bool} FsCloseTail{want_tick: Bool, +open_n: Nat, +acc: Nat} FsTailDec{want_tick: Bool, +open_n: Nat, +acc: Nat, nl: Bool, sp: Bool}def is_tick_char(+want_tick: Bool, +c: Char) -> Bool: match want_tick: case True{}: Char.is_eq(c, '`') case False{}: Char.is_eq(c, '~')def fence_len_go(fuel: Nat, ph: FsPh, rest: String) -> Nat: match fuel: case 0n: match ph: case FsBody{want_tick, open_n, +acc, at_bol}: acc case FsOpenRun{want_tick, run}: 0n case FsOpenDec{want_tick, run, is_tick, ge3}: 0n case FsSkipInfo{want_tick, open_n, +acc}: acc case FsSkipDec{want_tick, open_n, +acc, nl}: acc case FsBodyDec{want_tick, open_n, +acc, at_bol, is_tick, nl}: acc case FsCloseRun{want_tick, open_n, +acc, run}: Nat.add(acc, run) case FsCloseDec{want_tick, open_n, +acc, run, is_tick, ge}: Nat.add(acc, run) case FsCloseTail{want_tick, open_n, +acc}: acc case FsTailDec{want_tick, open_n, +acc, nl, sp}: acc case 1n+p: match ph: case FsOpenRun{+want_tick, +run}: match rest: case SNil{}: 0n case SCon{+h, +t}: fence_len_go( p, FsOpenDec{want_tick, run, is_tick_char(want_tick, h), Nat.is_ge(run, 3n)}, rest ) case FsOpenDec{+want_tick, +run, is_tick, ge3}: match is_tick: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: fence_len_go(p, FsOpenRun{want_tick, Nat.add(run, 1n)}, t) case False{}: match ge3: case True{}: fence_len_go(p, FsSkipInfo{want_tick, run, run}, rest) case False{}: 0n case FsSkipInfo{+want_tick, +open_n, +acc}: match rest: case SNil{}: acc case SCon{+h, +t}: fence_len_go(p, FsSkipDec{want_tick, open_n, acc, is_newline(h)}, SCon{h, t}) case FsSkipDec{+want_tick, +open_n, +acc, nl}: match nl: case True{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), True{}}, t) case False{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsSkipInfo{want_tick, open_n, Nat.add(acc, 1n)}, t) case FsBody{+want_tick, +open_n, +acc, +at_bol}: match rest: case SNil{}: acc case SCon{+h, +t}: fence_len_go( p, FsBodyDec{want_tick, open_n, acc, at_bol, is_tick_char(want_tick, h), is_newline(h)}, rest ) case FsBodyDec{+want_tick, +open_n, +acc, +at_bol, is_tick, nl}: match at_bol: case True{}: match is_tick: case True{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsCloseRun{want_tick, open_n, acc, 1n}, t) case False{}: match nl: case True{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), True{}}, t) case False{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), False{}}, t) case False{}: match nl: case True{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), True{}}, t) case False{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), False{}}, t) case FsCloseRun{+want_tick, +open_n, +acc, +run}: match rest: case SNil{}: Nat.add(acc, run) case SCon{+h, +t}: fence_len_go( p, FsCloseDec{want_tick, open_n, acc, run, is_tick_char(want_tick, h), Nat.is_ge(run, open_n)}, rest ) case FsCloseDec{+want_tick, +open_n, +acc, +run, is_tick, ge}: match is_tick: case True{}: match rest: case SNil{}: Nat.add(acc, run) case SCon{h, t}: fence_len_go(p, FsCloseRun{want_tick, open_n, acc, Nat.add(run, 1n)}, t) case False{}: match ge: case True{}: fence_len_go(p, FsCloseTail{want_tick, open_n, Nat.add(acc, run)}, rest) case False{}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, run), False{}}, rest) case FsCloseTail{+want_tick, +open_n, +acc}: match rest: case SNil{}: acc case SCon{+h, +t}: fence_len_go( p, FsTailDec{want_tick, open_n, acc, is_newline(h), Char.is_space(h)}, rest ) case FsTailDec{+want_tick, +open_n, +acc, nl, sp}: match nl: case True{}: Nat.add(acc, 1n) case False{}: match sp: case True{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsCloseTail{want_tick, open_n, Nat.add(acc, 1n)}, t) case False{}: match rest: case SNil{}: acc case SCon{h, t}: fence_len_go(p, FsBody{want_tick, open_n, Nat.add(acc, 1n), False{}}, t)def fence_len_from_open(+want_tick: Bool, +s: String) -> Nat: fence_len_go( Nat.add(Nat.mul(6n, String.length(s)), 32n), FsOpenRun{want_tick, 0n}, s )type FnGate is Data: FnNo{} FnTick{} FnWave{} FnDec{at_bol: Bool, is_tick: Bool, is_wave: Bool}def fence_len_gate(fuel: Nat, g: FnGate, +s: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match g: case FnNo{}: 0n case FnTick{}: fence_len_from_open(True{}, s) case FnWave{}: fence_len_from_open(False{}, s) case FnDec{at_bol, is_tick, is_wave}: match at_bol: case False{}: 0n case True{}: match is_tick: case True{}: fence_len_gate(p, FnTick{}, s) case False{}: match is_wave: case True{}: fence_len_gate(p, FnWave{}, s) case False{}: 0ndef fence_len(+at_bol: Bool, +s: String) -> Nat: match s: case SNil{}: 0n case SCon{+h, t}: fence_len_gate(4n, FnDec{at_bol, Char.is_eq(h, '`'), Char.is_eq(h, '~')}, s)# --- Inline code ---type IcPh is Data: IcOpen{+run: Nat} IcOpenDec{+run: Nat, is_tick: Bool, run0: Bool, nl: Bool} IcBody{+open_n: Nat, +acc: Nat} IcBodyDec{+open_n: Nat, +acc: Nat, nl: Bool, is_tick: Bool} IcClose{+open_n: Nat, +acc: Nat, +run: Nat} IcCloseDec{+open_n: Nat, +acc: Nat, +run: Nat, is_tick: Bool}def inline_code_go(fuel: Nat, ph: IcPh, rest: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case IcOpen{+run}: match rest: case SNil{}: 0n case SCon{+h, +t}: inline_code_go( p, IcOpenDec{run, Char.is_eq(h, '`'), Nat.is_eq(run, 0n), is_newline(h)}, rest ) case IcOpenDec{+run, is_tick, run0, nl}: match is_tick: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: inline_code_go(p, IcOpen{Nat.add(run, 1n)}, t) case False{}: match run0: case True{}: 0n case False{}: match nl: case True{}: 0n case False{}: inline_code_go(p, IcBody{run, run}, rest) case IcBody{+open_n, +acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: inline_code_go( p, IcBodyDec{open_n, acc, is_newline(h), Char.is_eq(h, '`')}, rest ) case IcBodyDec{+open_n, +acc, nl, is_tick}: match nl: case True{}: 0n case False{}: match is_tick: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: inline_code_go(p, IcClose{open_n, acc, 1n}, t) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: inline_code_go(p, IcBody{open_n, Nat.add(acc, 1n)}, t) case IcClose{+open_n, +acc, +run}: match rest: case SNil{}: Nat.add(acc, run) case SCon{+h, +t}: inline_code_go(p, IcCloseDec{open_n, acc, run, Char.is_eq(h, '`')}, SCon{h, t}) case IcCloseDec{+open_n, +acc, +run, is_tick}: match is_tick: case True{}: match rest: case SNil{}: Nat.add(acc, run) case SCon{h, t}: inline_code_go(p, IcClose{open_n, acc, Nat.add(run, 1n)}, t) case False{}: Nat.add(acc, run)type IcGate is Data: IcGate{ok: Bool}def inline_code_len_gated(g: IcGate, +s: String) -> Nat: match g: case IcGate{ok}: match ok: case True{}: inline_code_go(Nat.add(Nat.mul(4n, String.length(s)), 8n), IcOpen{0n}, s) case False{}: 0ndef inline_code_len(+s: String) -> Nat: match s: case SNil{}: 0n case SCon{+h, t}: inline_code_len_gated(IcGate{Char.is_eq(h, '`')}, s)# --- Wikilink ---type WkPh is Data: WkNeed2{} WkNeed2Dec{is_br: Bool} WkBody{+acc: Nat} WkBodyDec{+acc: Nat, nl: Bool, is_br: Bool} WkClose1{+acc: Nat} WkClose1Dec{+acc: Nat, is_br: Bool}def wikilink_go(fuel: Nat, ph: WkPh, rest: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case WkNeed2{}: match rest: case SNil{}: 0n case SCon{+h, +t}: wikilink_go(p, WkNeed2Dec{Char.is_eq(h, '[')}, SCon{h, t}) case WkNeed2Dec{is_br}: match is_br: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: wikilink_go(p, WkBody{2n}, t) case False{}: 0n case WkBody{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: wikilink_go(p, WkBodyDec{acc, is_newline(h), Char.is_eq(h, ']')}, SCon{h, t}) case WkBodyDec{+acc, nl, is_br}: match nl: case True{}: 0n case False{}: match is_br: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: wikilink_go(p, WkClose1{Nat.add(acc, 1n)}, t) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: wikilink_go(p, WkBody{Nat.add(acc, 1n)}, t) case WkClose1{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: wikilink_go(p, WkClose1Dec{acc, Char.is_eq(h, ']')}, SCon{h, t}) case WkClose1Dec{+acc, is_br}: match is_br: case True{}: Nat.add(acc, 1n) case False{}: 0ntype WkGate is Data: WkGate{ok: Bool}def wikilink_len_gated(g: WkGate, +s: String) -> Nat: match g: case WkGate{ok}: match ok: case True{}: wikilink_go(Nat.add(Nat.mul(3n, String.length(s)), 8n), WkNeed2{}, str_drop(1n, s)) case False{}: 0ndef wikilink_len(+s: String) -> Nat: wikilink_len_gated(WkGate{String.starts_with(s, "[[")}, s)# --- Markdown link ---type MdPh is Data: MdBang{} MdBangDec{is_bang: Bool, is_br: Bool} MdLabel{+acc: Nat} MdLabelDec{+acc: Nat, nl: Bool, is_br: Bool} MdMid{+acc: Nat} MdMidDec{+acc: Nat, is_par: Bool} MdUrl{+acc: Nat} MdUrlDec{+acc: Nat, nl: Bool, is_par: Bool}def md_link_go(fuel: Nat, ph: MdPh, rest: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case MdBang{}: match rest: case SNil{}: 0n case SCon{+h, +t}: md_link_go(p, MdBangDec{Char.is_eq(h, '!'), Char.is_eq(h, '[')}, SCon{h, t}) case MdBangDec{is_bang, is_br}: match is_bang: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdLabel{1n}, t) case False{}: match is_br: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdLabel{1n}, t) case False{}: 0n case MdLabel{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: md_link_go(p, MdLabelDec{acc, is_newline(h), Char.is_eq(h, ']')}, SCon{h, t}) case MdLabelDec{+acc, nl, is_br}: match nl: case True{}: 0n case False{}: match is_br: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdMid{Nat.add(acc, 1n)}, t) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdLabel{Nat.add(acc, 1n)}, t) case MdMid{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: md_link_go(p, MdMidDec{acc, Char.is_eq(h, '(')}, SCon{h, t}) case MdMidDec{+acc, is_par}: match is_par: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdUrl{Nat.add(acc, 1n)}, t) case False{}: 0n case MdUrl{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: md_link_go(p, MdUrlDec{acc, is_newline(h), Char.is_eq(h, ')')}, SCon{h, t}) case MdUrlDec{+acc, nl, is_par}: match nl: case True{}: 0n case False{}: match is_par: case True{}: Nat.add(acc, 1n) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: md_link_go(p, MdUrl{Nat.add(acc, 1n)}, t)type MdGate is Data: MdNo{} MdYes{} MdImgCheck{is_br: Bool} MdHead{is_bang: Bool, is_br: Bool, is_wiki: Bool}def md_link_len_go(fuel: Nat, g: MdGate, +s: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match g: case MdNo{}: 0n case MdYes{}: md_link_go(Nat.add(Nat.mul(3n, String.length(s)), 8n), MdBang{}, s) case MdImgCheck{is_br}: match is_br: case True{}: md_link_len_go(p, MdYes{}, s) case False{}: 0n case MdHead{is_bang, is_br, is_wiki}: match is_bang: case True{}: match s: case SNil{}: 0n case SCon{h, t}: match t: case SNil{}: 0n case SCon{+h2, t2}: md_link_len_go(p, MdImgCheck{Char.is_eq(h2, '[')}, s) case False{}: match is_br: case True{}: match is_wiki: case True{}: 0n case False{}: md_link_len_go(p, MdYes{}, s) case False{}: 0ndef md_link_len(+s: String) -> Nat: match s: case SNil{}: 0n case SCon{+h, t}: md_link_len_go( 6n, MdHead{Char.is_eq(h, '!'), Char.is_eq(h, '['), String.starts_with(s, "[[")}, s )# --- HTML ---type HtPh is Data: HtOpen{} HtOpenDec{is_lt: Bool} HtSlash{} HtSlashDec{is_slash: Bool, is_alpha: Bool} HtName{} HtNameDec{is_alpha: Bool} HtBody{+acc: Nat} HtBodyDec{+acc: Nat, nl: Bool, is_gt: Bool}def html_go(fuel: Nat, ph: HtPh, rest: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case HtOpen{}: match rest: case SNil{}: 0n case SCon{+h, +t}: html_go(p, HtOpenDec{Char.is_eq(h, '<')}, SCon{h, t}) case HtOpenDec{is_lt}: match is_lt: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: html_go(p, HtSlash{}, t) case False{}: 0n case HtSlash{}: match rest: case SNil{}: 0n case SCon{+h, +t}: html_go(p, HtSlashDec{Char.is_eq(h, '/'), Char.is_alpha(h)}, SCon{h, t}) case HtSlashDec{is_slash, is_alpha}: match is_slash: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: html_go(p, HtName{}, t) case False{}: match is_alpha: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: html_go(p, HtBody{2n}, t) case False{}: 0n case HtName{}: match rest: case SNil{}: 0n case SCon{+h, +t}: html_go(p, HtNameDec{Char.is_alpha(h)}, SCon{h, t}) case HtNameDec{is_alpha}: match is_alpha: case True{}: match rest: case SNil{}: 0n case SCon{h, t}: html_go(p, HtBody{3n}, t) case False{}: 0n case HtBody{+acc}: match rest: case SNil{}: 0n case SCon{+h, +t}: html_go(p, HtBodyDec{acc, is_newline(h), Char.is_eq(h, '>')}, SCon{h, t}) case HtBodyDec{+acc, nl, is_gt}: match nl: case True{}: 0n case False{}: match is_gt: case True{}: Nat.add(acc, 1n) case False{}: match rest: case SNil{}: 0n case SCon{h, t}: html_go(p, HtBody{Nat.add(acc, 1n)}, t)def html_len(+s: String) -> Nat: html_go(Nat.add(Nat.mul(3n, String.length(s)), 8n), HtOpen{}, s)# --- Priority pick ---type PkPh is Data: PkFence{n: Nat} PkFenceDec{n: Nat, z: Bool} PkInline{n: Nat} PkInlineDec{n: Nat, z: Bool} PkWiki{n: Nat} PkWikiDec{n: Nat, z: Bool} PkMd{n: Nat} PkMdDec{n: Nat, z: Bool} PkHtml{n: Nat}def protect_len_go(fuel: Nat, ph: PkPh, +at_bol: Bool, +s: String) -> Nat: match fuel: case 0n: 0n case 1n+p: match ph: case PkFence{+n}: protect_len_go(p, PkFenceDec{n, Nat.is_eq(n, 0n)}, at_bol, s) case PkFenceDec{+n, z}: match z: case False{}: n case True{}: protect_len_go(p, PkInline{inline_code_len(s)}, at_bol, s) case PkInline{+n}: protect_len_go(p, PkInlineDec{n, Nat.is_eq(n, 0n)}, at_bol, s) case PkInlineDec{+n, z}: match z: case False{}: n case True{}: protect_len_go(p, PkWiki{wikilink_len(s)}, at_bol, s) case PkWiki{+n}: protect_len_go(p, PkWikiDec{n, Nat.is_eq(n, 0n)}, at_bol, s) case PkWikiDec{+n, z}: match z: case False{}: n case True{}: protect_len_go(p, PkMd{md_link_len(s)}, at_bol, s) case PkMd{+n}: protect_len_go(p, PkMdDec{n, Nat.is_eq(n, 0n)}, at_bol, s) case PkMdDec{+n, z}: match z: case False{}: n case True{}: protect_len_go(p, PkHtml{html_len(s)}, at_bol, s) case PkHtml{+n}: ndef protect_len(+at_bol: Bool, +s: String) -> Nat: protect_len_go(16n, PkFence{fence_len(at_bol, s)}, at_bol, s)type FpGate is Data: FpDoc{fm: Nat, rest: Nat} FpBody{rest: Nat}def pick_nonzero_go(+a: Nat, +b: Nat, z: Bool) -> Nat: match z: case True{}: b case False{}: adef pick_nonzero(+a: Nat, +b: Nat) -> Nat: pick_nonzero_go(a, b, Nat.is_eq(a, 0n))def frontmatter_or_protect(+at_doc_start: Bool, +at_bol: Bool, +s: String) -> Nat: match at_doc_start: case True{}: pick_nonzero(frontmatter_len(s), protect_len(at_bol, s)) case False{}: protect_len(at_bol, s)