perf(frontend): use verified tail recursive parsing and resolution

  "bind (Error e) f = Error e"

| "bind (Ok x) f = f x"

lemma bind_assoc: "bind (bind r f) g = bind r (\<lambda>x. bind (f x) g)"

  by (cases r) auto

function decimal :: "nat \<Rightarrow> string" where

  "decimal n = (if n < 10 then [char_of_nat (48 + n)] else decimal (n div 10) @ [char_of_nat (48 + n mod 10)])"

  by pat_completeness auto

| "parse_lines n (s # ss) = bind (parse_line n (words s)) (\<lambda>xs.

    bind (parse_lines (Suc n) ss) (\<lambda>ys. Ok (xs @ ys)))"

fun parse_acc :: "nat \<Rightarrow> string list \<Rightarrow> statement list \<Rightarrow> statement list result" where

  "parse_acc n [] acc = Ok (rev acc)"

| "parse_acc n (s # ss) acc = (case parse_line n (words s) of Error e \<Rightarrow> Error e

    | Ok xs \<Rightarrow> parse_acc (Suc n) ss (rev xs @ acc))"

lemma parse_acc_correct:

  "parse_acc n ss acc = bind (parse_lines n ss) (\<lambda>xs. Ok (rev acc @ xs))"

  by (induction ss arbitrary: n acc) (auto simp: bind_assoc split: result.splits)

declare parse_lines.simps [code drop]

lemma parse_lines_code [code]: "parse_lines n ss = parse_acc n ss []"

  by (cases "parse_lines n ss") (simp_all add: parse_acc_correct)

fun count :: "statement \<Rightarrow> nat" where

  "count (Label l) = 0"

| "count (Emit op) = 1"

    bind (resolve_all env ss) (\<lambda>xs. Ok (x # xs)))"

| "resolve_all env (Pad n # ss) = bind (resolve_all env ss) (\<lambda>xs. Ok (replicate n Nop @ xs))"

fun resolve_acc :: "(string \<times> nat) list \<Rightarrow> statement list \<Rightarrow> nat instruction list \<Rightarrow> nat instruction list result" where

  "resolve_acc env [] acc = Ok (rev acc)"

| "resolve_acc env (Label l # ss) acc = resolve_acc env ss acc"

| "resolve_acc env (Emit op # ss) acc = (case resolve env op of Error e \<Rightarrow> Error e

    | Ok x \<Rightarrow> resolve_acc env ss (x # acc))"

| "resolve_acc env (Pad n # ss) acc = resolve_acc env ss (replicate n Nop @ acc)"

lemma resolve_acc_correct:

  "resolve_acc env ss acc = bind (resolve_all env ss) (\<lambda>xs. Ok (rev acc @ xs))"

proof (induction ss arbitrary: acc)

  case Nil

  then show ?case by simp

next

  case (Cons s ss)

  then show ?case by (cases s) (auto simp: bind_assoc split: result.splits)

qed

declare resolve_all.simps [code drop]

lemma resolve_all_code [code]: "resolve_all env ss = resolve_acc env ss []"

  by (cases "resolve_all env ss") (simp_all add: resolve_acc_correct)

definition source :: "string \<Rightarrow> nat instruction list result" where

  "source s = (if \<not> list_all (\<lambda>c. let n = nat_of_char c in

      n = 9 \<or> n = 10 \<or> n = 13 \<or> (32 \<le> n \<and> n < 127)) s

    ]:

        check(message in cli("assemble", "-", text=text, ok=False), message)

    check("16-bit range" in cli("assemble", "examples/overflow.span", ok=False), "overflow accepted")

    check("65536 instructions, 65536 bytes" in cli("assemble", "-", text="nop\n" * 65536), "maximum line count")

    check("invalid instruction at line 4097" in cli("assemble", "-", text="nop\n" * 4096 + "invalid\npad -1", ok=False), "first parse error changed")

    check("undefined label first" in cli("assemble", "-", text="pad 3\njmp first\njmp second", ok=False), "first resolution error changed")

    for padding, width in [(127, 2), (128, 3), (32767, 3)]:

        report = cli("assemble", "-", text=f"jmp end\npad {padding}\nlabel end\nhalt")

        check(f"{padding + width + 1} bytes" in report, "forward range boundary")