# 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 Base

def 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 ---
type FmPh is Data:
  FmNeedNl{}
  FmNeedNlDec{nl: Bool}
  FmScan{}
  FmScanDec{nl: Bool}
  FmDash1{}
  FmDash1Dec{is_dash: Bool, nl: Bool}
  FmDash1GoDash{}
  FmDash1GoNl{}
  FmDash1GoScan{}
  FmDash2{}
  FmDash2Dec{is_dash: Bool}
  FmDash3{}
  FmDash3Dec{nl: Bool}

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)}, SCon{h, t}, consumed)
        case FmNeedNlDec{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{}:
              consumed
            case SCon{+h, +t}:
              frontmatter_go(p, FmDash3Dec{is_newline(h)}, SCon{h, t}, consumed)
        case FmDash3Dec{nl}:
          match nl:
            case True{}:
              Nat.add(consumed, 1n)
            case False{}:
              frontmatter_go(p, FmScan{}, rest, consumed)

def 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)), 8n),
        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{}:
                      0n

def 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{}:
          0n

def 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{}:
              0n

type 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{}:
          0n

def 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{}:
                  0n

def 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}:
          n

def 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{}:
      a

def 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)