import Forth.Semantics

/-!
# Forth.Eval

A fuel-bounded executable interpreter for the Forth reference semantics, proved sound
against `Run`: if it returns a result, `Run` derives that result. It lets concrete facts about
the reference semantics (including recursive words) be established by evaluation.
-/

namespace WordDialect
namespace Forth

/-- Run `b` from `st` with at most `fuel` nested evaluation steps; `none` means out of fuel. -/
def eval {n : Nat} (defs : List Block) : Nat → Block → FState n → Option (Res n)
  | 0, _, _ => none
  | _ + 1, .nil, st => some (.ok st)
  | _ + 1, .exit _, st => some (.exit st)
  | _ + 1, .leave _, ⟨d, m, _ :: _ :: rs⟩ => some (.leave ⟨d, m, rs⟩)
  | _ + 1, .leave _, _ => some (.error .returnUnderflow)
  | f + 1, .op o rest, st =>
    match o.sem st with
    | .ok st' => eval defs f rest st'
    | .error t => some (.error t)
  | _ + 1, .ite _ _ _, ⟨[], _, _⟩ => some (.error .stackUnderflow)
  | f + 1, .ite t e rest, ⟨c :: d, m, rs⟩ =>
    match eval defs f (if Word.isTrue c then t else e) ⟨d, m, rs⟩ with
    | none => none
    | some (.error x) => some (.error x)
    | some (.exit st1) => some (.exit st1)
    | some (.leave st1) => some (.leave st1)
    | some (.ok st1) => eval defs f rest st1
  | f + 1, .untilL body rest, st =>
    match eval defs f body st with
    | none => none
    | some (.error x) => some (.error x)
    | some (.exit st1) => some (.exit st1)
    | some (.leave st1) => some (.leave st1)
    | some (.ok ⟨[], _, _⟩) => some (.error .stackUnderflow)
    | some (.ok ⟨c :: d, m, rs⟩) =>
      if Word.isTrue c then eval defs f rest ⟨d, m, rs⟩
      else eval defs f (.untilL body rest) ⟨d, m, rs⟩
  | f + 1, .whileL cond body rest, st =>
    match eval defs f cond st with
    | none => none
    | some (.error x) => some (.error x)
    | some (.exit st1) => some (.exit st1)
    | some (.leave st1) => some (.leave st1)
    | some (.ok ⟨[], _, _⟩) => some (.error .stackUnderflow)
    | some (.ok ⟨c :: d, m, rs⟩) =>
      if Word.isTrue c then
        match eval defs f body ⟨d, m, rs⟩ with
        | none => none
        | some (.error x) => some (.error x)
        | some (.exit st2) => some (.exit st2)
        | some (.leave st2) => some (.leave st2)
        | some (.ok st2) => eval defs f (.whileL cond body rest) st2
      else eval defs f rest ⟨d, m, rs⟩
  | f + 1, .call i rest, st =>
    match defs[i]? with
    | none => some (.error .badPc)
    | some body =>
      match eval defs f body st with
      | none => none
      | some (.error x) => some (.error x)
      | some (.exit st1) => eval defs f rest st1
      | some (.leave st1) => eval defs f rest st1
      | some (.ok st1) => eval defs f rest st1
  | f + 1, .doLoop body rest, ⟨i :: l :: d, m, rs⟩ =>
    match eval defs f body ⟨d, m, i :: l :: rs⟩ with
    | none => none
    | some (.error x) => some (.error x)
    | some (.exit st1) => some (.exit st1)
    | some (.leave st1) => eval defs f rest st1
    | some (.ok ⟨d1, m1, i1 :: l1 :: rs1⟩) =>
      if i1 + 1#n = l1 then eval defs f rest ⟨d1, m1, rs1⟩
      else eval defs f (.doLoop body rest) ⟨(i1 + 1#n) :: l1 :: d1, m1, rs1⟩
    | some (.ok _) => some (.error .returnUnderflow)
  | _ + 1, .doLoop _ _, _ => some (.error .stackUnderflow)
  | f + 1, .plusLoop body rest, ⟨i :: l :: d, m, rs⟩ =>
    match eval defs f body ⟨d, m, i :: l :: rs⟩ with
    | none => none
    | some (.error x) => some (.error x)
    | some (.exit st1) => some (.exit st1)
    | some (.leave st1) => eval defs f rest st1
    | some (.ok ⟨k :: d1, m1, i1 :: l1 :: rs1⟩) =>
      if loopCrossed i1 l1 k then eval defs f rest ⟨d1, m1, rs1⟩
      else eval defs f (.plusLoop body rest) ⟨(i1 + k) :: l1 :: d1, m1, rs1⟩
    | some (.ok ⟨[], _, _ :: _ :: _⟩) => some (.error .stackUnderflow)
    | some (.ok _) => some (.error .returnUnderflow)
  | _ + 1, .plusLoop _ _, _ => some (.error .stackUnderflow)

theorem eval_sound {n : Nat} {defs : List Block} :
    ∀ (fuel : Nat) (b : Block) (st : FState n) (r : Res n),
      eval defs fuel b st = some r → Run defs b st r := by
  intro fuel
  induction fuel with
  | zero => intro b st r h; simp [eval] at h
  | succ f ih =>
    intro b st r h
    cases b with
    | nil => simp only [eval, Option.some.injEq] at h; subst h; exact .nil
    | exit rest => simp only [eval, Option.some.injEq] at h; subst h; exact .exit
    | leave rest =>
      obtain ⟨d, m, rs⟩ := st
      rcases rs with _ | ⟨a, _ | ⟨b, rs⟩⟩
      · simp only [eval, Option.some.injEq] at h; subst h; exact .leaveUnder (by simp)
      · simp only [eval, Option.some.injEq] at h; subst h; exact .leaveUnder (by simp)
      · simp only [eval, Option.some.injEq] at h; subst h; exact .leaveOk
    | op o rest =>
      simp only [eval] at h
      split at h
      · exact .opOk ‹_› (ih _ _ _ h)
      · cases h; exact .opErr ‹_›
    | ite t e rest =>
      obtain ⟨d, m, rs⟩ := st
      cases d with
      | nil => simp only [eval, Option.some.injEq] at h; subst h; exact .iteUnder
      | cons c d =>
        simp only [eval] at h
        split at h
        · cases h
        · rename_i x hx
          cases h
          cases hc : Word.isTrue c
          · rw [hc] at hx; exact .iteFalseStop hc (ih _ _ _ hx) rfl
          · rw [hc] at hx; exact .iteTrueStop hc (ih _ _ _ hx) rfl
        · rename_i x hx
          cases h
          cases hc : Word.isTrue c
          · rw [hc] at hx; exact .iteFalseStop hc (ih _ _ _ hx) rfl
          · rw [hc] at hx; exact .iteTrueStop hc (ih _ _ _ hx) rfl
        · rename_i x hx
          cases h
          cases hc : Word.isTrue c
          · rw [hc] at hx; exact .iteFalseStop hc (ih _ _ _ hx) rfl
          · rw [hc] at hx; exact .iteTrueStop hc (ih _ _ _ hx) rfl
        · rename_i st1 hx
          cases hc : Word.isTrue c
          · rw [hc] at hx; exact .iteFalse hc (ih _ _ _ hx) (ih _ _ _ h)
          · rw [hc] at hx; exact .iteTrue hc (ih _ _ _ hx) (ih _ _ _ h)
    | untilL body rest =>
      simp only [eval] at h
      split at h
      · cases h
      · rename_i x hx; cases h; exact .untilBodyStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .untilBodyStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .untilBodyStop (ih _ _ _ hx) rfl
      · rename_i m rs hx; cases h; exact .untilUnder (ih _ _ _ hx)
      · rename_i c d m rs hx
        cases hc : Word.isTrue c
        · rw [hc] at h; exact .untilAgain (ih _ _ _ hx) hc (ih _ _ _ h)
        · rw [hc] at h; exact .untilDone (ih _ _ _ hx) hc (ih _ _ _ h)
    | whileL cond body rest =>
      simp only [eval] at h
      split at h
      · cases h
      · rename_i x hx; cases h; exact .whileCondStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .whileCondStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .whileCondStop (ih _ _ _ hx) rfl
      · rename_i m rs hx; cases h; exact .whileUnder (ih _ _ _ hx)
      · rename_i c d m rs hx
        split at h
        · rename_i hc
          split at h
          · cases h
          · rename_i x hb; cases h; exact .whileBodyStop (ih _ _ _ hx) hc (ih _ _ _ hb) rfl
          · rename_i x hb; cases h; exact .whileBodyStop (ih _ _ _ hx) hc (ih _ _ _ hb) rfl
          · rename_i x hb; cases h; exact .whileBodyStop (ih _ _ _ hx) hc (ih _ _ _ hb) rfl
          · rename_i st2 hb; exact .whileAgain (ih _ _ _ hx) hc (ih _ _ _ hb) (ih _ _ _ h)
        · rename_i hc
          exact .whileExit (ih _ _ _ hx) (by simpa using hc) (ih _ _ _ h)
    | call i rest =>
      simp only [eval] at h
      split at h
      · cases h; exact .callUndef ‹_›
      · rename_i body hi
        split at h
        · cases h
        · rename_i x hx; cases h; exact .callErr hi (ih _ _ _ hx)
        · rename_i st1 hx; exact .callOk hi (ih _ _ _ hx) rfl (ih _ _ _ h)
        · rename_i st1 hx; exact .callOk hi (ih _ _ _ hx) rfl (ih _ _ _ h)
        · rename_i st1 hx; exact .callOk hi (ih _ _ _ hx) rfl (ih _ _ _ h)
    | doLoop body rest =>
      obtain ⟨d, m, rs⟩ := st
      rcases d with _ | ⟨i, _ | ⟨l, d⟩⟩
      · simp only [eval, Option.some.injEq] at h; subst h; exact .doUnder (by simp)
      · simp only [eval, Option.some.injEq] at h; subst h; exact .doUnder (by simp)
      simp only [eval] at h
      split at h
      · cases h
      · rename_i x hx; cases h; exact .doBodyStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .doBodyStop (ih _ _ _ hx) rfl
      · rename_i st1 hx; exact .doLeave (ih _ _ _ hx) (ih _ _ _ h)
      · rename_i d1 m1 i1 l1 rs1 hx
        split at h
        · exact .doDone (ih _ _ _ hx) ‹_› (ih _ _ _ h)
        · exact .doAgain (ih _ _ _ hx) ‹_› (ih _ _ _ h)
      · rename_i st1 hne hx
        cases h
        obtain ⟨d1, m1, rs1⟩ := st1
        rcases rs1 with _ | ⟨a, _ | ⟨b, rs1⟩⟩
        · exact .doTestUnder (ih _ _ _ hx) (by simp)
        · exact .doTestUnder (ih _ _ _ hx) (by simp)
        · exact absurd rfl (hne d1 m1 a b rs1)
    | plusLoop body rest =>
      obtain ⟨d, m, rs⟩ := st
      rcases d with _ | ⟨i, _ | ⟨l, d⟩⟩
      · simp only [eval, Option.some.injEq] at h; subst h; exact .plusUnder (by simp)
      · simp only [eval, Option.some.injEq] at h; subst h; exact .plusUnder (by simp)
      simp only [eval] at h
      split at h
      · cases h
      · rename_i x hx; cases h; exact .plusBodyStop (ih _ _ _ hx) rfl
      · rename_i x hx; cases h; exact .plusBodyStop (ih _ _ _ hx) rfl
      · rename_i st1 hx; exact .plusLeave (ih _ _ _ hx) (ih _ _ _ h)
      · rename_i k d1 m1 i1 l1 rs1 hx
        split at h
        · exact .plusDone (ih _ _ _ hx) ‹_› (ih _ _ _ h)
        · rename_i hc; exact .plusAgain (ih _ _ _ hx) (by simpa using hc) (ih _ _ _ h)
      · rename_i m1 i1 l1 rs1 hx; cases h; exact .plusStepUnder (ih _ _ _ hx)
      · rename_i st1 hne1 hne2 hx
        cases h
        obtain ⟨d1, m1, rs1⟩ := st1
        rcases rs1 with _ | ⟨a, _ | ⟨b, rs1⟩⟩
        · exact .plusTestUnder (ih _ _ _ hx) (by simp)
        · exact .plusTestUnder (ih _ _ _ hx) (by simp)
        · cases d1 with
          | nil => exact absurd rfl (hne2 m1 a b rs1)
          | cons k d1 => exact absurd rfl (hne1 k d1 m1 a b rs1)

end Forth
end WordDialect