You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
def Handler.lookup (hdl : Handler) (name : Name) :=
  hdl.ops.find? (·.op == name)

def instantiate2 (arg cont : Value) (body : Computation) : Computation :=
  instantiateComputationLvl arg 1 (instantiateComputationLvl cont 0 body)

def strAppend : String → String → String
| "", s => s
| s, "" => s
| s₁, s₂ => s₁ ++ " " ++ s₂

@[grind cases]
inductive Step : Computation → Computation → Prop
 
| beta v body : Step (.app (.lam body) v) (instantiateComp v body)
 
| recBeta v body : Step (.app (.recfun body) v) (instantiate2 (.recfun body) v body)
 
| iteTrue c₁ c₂ : Step (.ite (.bool true) c₁ c₂) c₁
 
| iteFalse c₁ c₂ : Step (.ite (.bool false) c₁ c₂) c₂
 
| bindStep c₁ c₁' c₂ (h : Step c₁ c₁') : Step (.bind c₁ c₂) (.bind c₁' c₂)
 
| bindReturn v c : Step (.bind (.ret v) c) (instantiateComp v c)
 
| bindOp op v body c : Step (.bind (.opCall op v body) c) (.opCall op v (.bind body c))
 
| handleInner h c₁ c₂ (h₁ : Step c₁ c₂) : Step (.handle (.hdl h) c₁) (.handle (.hdl h) c₂)
 
| handleReturn h v :
  Step (.handle (.hdl h) (.ret v)) (instantiateComp v h.ret)
 
| handleOpHit h op v body c (hop : h.lookup op = some ⟨op, c⟩) :
  Step (.handle (.hdl h) (.opCall op v body))
    (instantiate2 v (.lam (.handle (.hdl h) body)) c)
 
| handleOpMiss h op v body (hop : h.lookup op = none) :
  Step (.handle (.hdl h) (.opCall op v body)) (.opCall op v (.handle (.hdl h) body))
 
| join s₁ s₂ : Step (.join (.string s₁) (.string s₂)) (.ret (.string (strAppend s₁ s₂)))
 
| fstStep v₁ v₂ : Step (.fst (.pair v₁ v₂)) (.ret v₁)
 
| sndStep v₁ v₂ : Step (.snd (.pair v₁ v₂)) (.ret v₂)
| add v₁ v₂ : Step (.add (.num v₁) (.num v₂)) (.ret (.num (v₁ + v₂)))
| sub v₁ v₂ : Step (.sub (.num v₁) (.num v₂)) (.ret (.num (v₁ - v₂)))
| max v₁ v₂ : Step (.max (.num v₁) (.num v₂)) (.ret (.num (Max.max v₁ v₂)))
| lt v₁ v₂ : Step (.lt (.num v₁) (.num v₂)) (.ret (.bool (v₁ < v₂)))
| mul v₁ v₂ : Step (.mul (.num v₁) (.num v₂)) (.ret (.num (v₁ * v₂)))
| eq v₁ v₂ : Step (.eq v₁ v₂) (.ret (.bool (v₁ == v₂)))

@[grind cases]
inductive StepStar : Computation → Computation → Prop
| refl (c) : StepStar c c
| trans : Step c₁ c₂ → StepStar c₂ c₃ → StepStar c₁ c₃

inductive ValueTy' where
| bool | string | num | unit | void
| pair : ValueTy' → ValueTy' → ValueTy'
| function : ValueTy' → ComputationTy' → ValueTy'
| handler : ComputationTy' → ComputationTy' → ValueTy'
| mvar : Nat → ValueTy'
deriving DecidableEq, Inhabited

structure ComputationTy' where
  returnTy : ValueTy'
deriving DecidableEq

def mvarInVal (n : Nat) : ValueTy' → Bool
| .mvar n' => n == n'
| .function input output => mvarInVal n input || mvarInComp n output
| .handler c1 c2 => mvarInComp n c1 || mvarInComp n c2
| .pair v1 v2 => mvarInVal n v1 || mvarInVal n v2
| .bool => false
| .unit => false
| .string => false
| .num => false
| .void => false

def mvarInComp (n : Nat) : ComputationTy' → Bool
| ⟨returnTy⟩ => mvarInVal n returnTy

inductive Constraint where
| valEq (τ τ' : ValueTy') 
deriving Inhabited

inductive Ty' where
| val : ValueTy' → Ty'
| comp : ComputationTy' → Ty'

def ValueTy'.format (prec : Nat) : ValueTy' → Format
| .mvar n => .group <| s!"?α{n}"
| .bool => .group <| "bool"
| .handler c1 c2 => .group <| c1.format prec ++ " ⇒ " ++ c2.format prec
| .function v c => .group <| v.format prec ++ " → " ++ c.format prec
| .pair v1 v2 => .group <| "(" ++ v1.format prec ++ ", " ++ v2.format prec ++ ")"
| .void => .group <| "void"
| .unit => .group <| "unit"
| .num => .group <| "int"
| .string => .group <| "str"

def ComputationTy'.format (prec : Nat) : ComputationTy' → Format
| ⟨returnTy⟩ => .group <| "{" ++ returnTy.format prec ++ "}"

def Constraint.format (prec : Nat) : Constraint → Format
| .valEq v1 v2 => .group <| v1.format prec ++ " ≡ " ++ v2.format prec

instance : Repr ComputationTy' where
  reprPrec comp n := comp.format n

instance : Repr ValueTy' where
  reprPrec value n := value.format n

instance : Repr Ty' where
  reprPrec e := match e with
    | .val v => reprPrec v
    | .comp c => reprPrec c

instance : Repr Constraint where
  reprPrec c n := c.format n

instance : ToString ComputationTy' where
  toString := toString ∘ repr

instance : ToString ValueTy' where
  toString := toString ∘ repr

instance : ToString Ty' where
  toString := toString ∘ repr

instance : ToString Constraint where
  toString := toString ∘ repr

def Except.exceptFormat : Except String Ty' → String
| .ok t => toString t
| .error s => s

abbrev Ctx' := List ValueTy'

abbrev OpSignatureList := List (String × (ValueTy × ValueTy))

abbrev Constraints := List Constraint

def valueTyToPrime : ValueTy → ValueTy'
| .bool => .bool | .unit => .unit | .num => .num | .string => .string | .void => .void
| .pair v1 v2 => .pair (valueTyToPrime v1) (valueTyToPrime v2)
| .handler c1 c2 => .handler (compTyToPrime c1) (compTyToPrime c2)
| .function v c => .function (valueTyToPrime v) (compTyToPrime c)

def compTyToPrime : ComputationTy → ComputationTy'
| ⟨returnTy, _⟩ => ⟨valueTyToPrime returnTy⟩

def mvarInConstraint (n : Nat) : Constraint → Bool
| .valEq v1 v2 => mvarInVal n v1 || mvarInVal n v2

def mvarInConstraints (n : Nat) (cs : Constraints) := cs.any (mvarInConstraint n ·)

instance : Coe ValueTy ValueTy' where
  coe := valueTyToPrime

structure MVarState where
  next : Nat := 0
deriving Repr

abbrev MetaM := ExceptT String (StateM MVarState)

def freshValueMVar : MetaM ValueTy' := do
  let n ← get <&> (·.next)
  modify (fun s => {next := s.next + 1})
  return (.mvar n)

def freshCompMVar : MetaM ComputationTy' := do
  return ({returnTy := ←freshValueMVar})

def collectValConstraints (σ : OpSignature) (Γ : Ctx') :
    Value → MetaM (ValueTy' × Constraints)
| .var (.bvar i) =>
  match Γ[i]? with
  | some τ => pure (τ, [])
  | none => Except.error s!"Unbound de Bruijn index {i}"
| .bool _ => pure (.bool, [])
| .hdl h => collectHandlerConstraints σ Γ h
| .lam body => do
  
  let α ← freshValueMVar
  let (k, C) ← collectCompConstraints σ (α :: Γ) body
  return (.function α k, C)
| .recfun body => do
  
  let α ← freshValueMVar
  let β ← freshValueMVar
  let (k, C) ← collectCompConstraints σ (α :: β :: Γ) body
  let newConstraints : Constraints := [.valEq β (.function α k)]
  return (.function α k, newConstraints ++ C)
| .pair v1 v2 => do
  let (τ1, C1) ← collectValConstraints σ Γ v1
  let (τ2, C2) ← collectValConstraints σ Γ v2
  return (.pair τ1 τ2, C1 ++ C2)
| .string _ => pure (.string, [])
| .num _ => pure (.num, [])
| .unit => pure (.unit, [])
| .var (.fvar n) => Except.error s!"Free variable {n}"

def collectCompConstraints (σ : OpSignature) (Γ : Ctx') :
    Computation → MetaM (ComputationTy' × Constraints)
| .ret v => do
  let (τ, C) ← collectValConstraints σ Γ v
  return (.mk τ, C)
| .opCall name v cont => do
  let some (Aop, Bop) := (σ.get? name) | Except.error s!"Unknown op {name}"
  let (τ_v, C_v) ← collectValConstraints σ Γ v

  
  let y ← freshValueMVar
  let (τ_cont, C_cont) ← collectCompConstraints σ (y :: Γ) cont

  let newConstraints : Constraints := [
    .valEq τ_v Aop, 
    .valEq y Bop, 
  ]
  return ({returnTy := τ_cont.returnTy}, newConstraints ++ C_v ++ C_cont)
| .bind c1 c2 => do
  let (τ_c1, C_c1) ← collectCompConstraints σ Γ c1

  
  let α ← freshValueMVar
  let (τ_c2, C_c2) ← collectCompConstraints σ (α :: Γ) c2

  let newConstraints : Constraints := [.valEq α τ_c1.returnTy]

  return ({returnTy := τ_c2.returnTy}, newConstraints ++ C_c1 ++ C_c2)
| .app v1 v2 => do
  let (τ1, C1) ← collectValConstraints σ Γ v1
  let (τ2, C2) ← collectValConstraints σ Γ v2
  let α ← freshCompMVar
  let newConstraint : Constraints := [.valEq τ1 (.function τ2 α)]
  return (α, newConstraint ++ C1 ++ C2)
| .ite b c1 c2 => do
  let (τb, Cb) ← collectValConstraints σ Γ b
  let (τ1, C1) ← collectCompConstraints σ Γ c1
  let (τ2, C2) ← collectCompConstraints σ Γ c2
  let newConstraints : Constraints := [
    .valEq τb .bool,
    .valEq τ1.returnTy τ2.returnTy
  ]
  return ({returnTy := τ1.returnTy},
    newConstraints ++ C1 ++ C2 ++ Cb)
| .handle h c => do
  let (.handler startType endType, Ch) ← collectValConstraints σ Γ h
    | Except.error s!"Expected a handler but was given {h}"
  let (τc, Cc) ← collectCompConstraints σ Γ c
  let newConstraints : Constraints := [.valEq startType.returnTy τc.returnTy]
  return (endType, newConstraints ++ Ch ++ Cc)
| .join v1 v2 => do
  let (τ1, C1) ← collectValConstraints σ Γ v1
  let (τ2, C2) ← collectValConstraints σ Γ v2
  let newConstraints : Constraints := [
    .valEq τ1 .string,
    .valEq τ2 .string,
  ]
  return ({returnTy := .string}, newConstraints ++ C1 ++ C2)
| .fst v => do
  
  let α ← freshValueMVar
  let β ← freshValueMVar
  let (τ, C) ← collectValConstraints σ Γ v
  let newConstraints : Constraints := [.valEq τ (.pair α β)]
  return ({returnTy := α}, newConstraints ++ C)
| .snd v => do
  
  let α ← freshValueMVar
  let β ← freshValueMVar
  let (τ, C) ← collectValConstraints σ Γ v
  let newConstraints : Constraints := [.valEq τ (.pair α β)]
  return ({returnTy := β}, newConstraints ++ C)
| .add v1 v2 | .sub v1 v2 | .mul v1 v2 | .max v1 v2 => do
  let (τ1, C1) ← collectValConstraints σ Γ v1
  let (τ2, C2) ← collectValConstraints σ Γ v2
  let newConstraints : Constraints := [
    .valEq τ1 .num,
    .valEq τ2 .num
  ]
  return ({returnTy := .num}, newConstraints ++ C1 ++ C2)
| .lt v1 v2 => do
  let (τ1, C1) ← collectValConstraints σ Γ v1
  let (τ2, C2) ← collectValConstraints σ Γ v2
  let newConstraints : Constraints := [
    .valEq τ1 .num,
    .valEq τ2 .num
  ]
  return ({returnTy := .bool}, newConstraints ++ C1 ++ C2)
| .eq v1 v2 => do
  let (_, C1) ← collectValConstraints σ Γ v1
  let (_, C2) ← collectValConstraints σ Γ v2
  return ({returnTy := .bool}, C1 ++ C2)

def collectOpClauseConstraints (σ : OpSignature) (Γ : Ctx') :
    OpClause → MetaM (ComputationTy' × Constraints)
| ⟨op, body⟩ => do
  let some (Aop, Bop) := (σ.get? op) | Except.error s!"Unknown op {op}"

  
  let α ← freshValueMVar
  let (τ_body, C_body) ← collectCompConstraints σ (α :: Aop :: Γ) body

  
  
  if Aop = .void then
    Except.error s!"Operation {op} has input type void."
  if Bop = .void then
    match α with
    | .mvar n =>
      if mvarInComp n τ_body || mvarInConstraints n C_body then
        Except.error s!"Operation {op} has return type void but uses its continuation."
    | _ => Except.error "Created mvar is not an mvar??"

  let newConstraints : Constraints := [.valEq α (.function Bop τ_body)]
  return (τ_body, newConstraints ++ C_body)

def collectHandlerConstraints (σ : OpSignature) (Γ : Ctx') :
    Handler → MetaM (ValueTy' × Constraints)
| ⟨ret, ops⟩ => do
  
  let α ← freshValueMVar
  let (τret, Cret) ← collectCompConstraints σ (α :: Γ) ret
  let opsTypes ← ops.mapM (collectOpClauseConstraints σ Γ ·)
  let newConstraints : Constraints := opsTypes.map (.valEq ·.1.returnTy τret.returnTy)
  return (.handler ⟨α⟩ τret, Cret ++ newConstraints ++ (opsTypes.map (·.2)).flatten)

def collectConstraints (σ : OpSignature) (e : Computation) :
    Except String (ComputationTy' × Constraints) :=
  collectCompConstraints σ [] e |>.run' {} |>.run

def substMVarComp (n : Nat) (new : ValueTy') : ComputationTy' → ComputationTy'
| ⟨returnTy⟩ => ⟨substMVarVal n new returnTy⟩

def substMVarVal (n : Nat) (new : ValueTy') : ValueTy' → ValueTy'
| .mvar n' => if n = n' then new else .mvar n'
| .function input output => .function (substMVarVal n new input) (substMVarComp n new output)
| .handler c1 c2 => .handler (substMVarComp n new c1) (substMVarComp n new c2)
| .pair v1 v2 => .pair (substMVarVal n new v1) (substMVarVal n new v2)
| .bool => .bool
| .unit => .unit
| .string => .string
| .num => .num
| .void => .void

def Constraint.applySubst (f : ValueTy' → ValueTy') : Constraint → Constraint
| .valEq τ τ' => .valEq (f τ) (f τ')

def List.applySubst (f : ValueTy' → ValueTy') (c : Constraints) : Constraints :=
  c.map (·.applySubst f)

partial def unify : Constraints → Except String (ComputationTy' → ComputationTy')
| [] => Except.ok id
| .valEq τ τ' :: cs => do
  if τ = τ' ∨ τ = .void ∨ τ' = .void then
    return ←unify cs
  else if let .mvar n := τ then
    if ¬mvarInVal n τ' then
      let compSub := substMVarComp n τ'
      let valSub := substMVarVal n τ'
      let unifySubCs ← unify (cs.applySubst valSub)
      return unifySubCs ∘ compSub
  else if let .mvar n := τ' then
    if ¬mvarInVal n τ then
      let compSub := substMVarComp n τ
      let valSub := substMVarVal n τ
      let unifySubCs ← unify (cs.applySubst valSub)
      return unifySubCs ∘ compSub
  else if let .function τ₀ τ₁ := τ then
    if let .function τ₀' τ₁' := τ' then
      return ← unify (.valEq τ₀ τ₀' :: .valEq (τ₁.returnTy) (τ₁'.returnTy) :: cs)
  else if let .pair τ₀ τ₁ := τ then
    if let .pair τ₀' τ₁' := τ' then
      return ← unify (.valEq τ₀ τ₀' :: .valEq τ₁ τ₁' :: cs)
  Except.error s!"Failed to solve constraint {repr (Constraint.valEq τ τ')}"

def inferCompType (σ : OpSignatureList) (c : Computation) :
    Except String ComputationTy' := do
  let (type, constraints) ← collectConstraints (Std.TreeMap.ofList σ) c
  let substitution ← unify constraints
  return substitution type

def inferValType (σ : OpSignatureList) (v : Value) :
    Except String ValueTy' := do
  let (type, constraints) ← collectConstraints (Std.TreeMap.ofList σ) (Computation.ret v)
  let substitution ← unify constraints
  return (substitution type).returnTy

def inferType (σ : List (String × (ValueTy × ValueTy))) : Expr → Except String Ty'
| .val v => (.val ·) <$> inferValType σ v
| .comp c => (.comp ·) <$> inferCompType σ c

macro "#inferType " σ:term ", " e:term : command =>
  `(#eval (inferType $σ $e).exceptFormat)

def abstractValueLvl (me : Name) (level : Nat) : Value → Value
| .var (.fvar you) => if you = me then .var (.bvar level) else .var (.fvar you)
| .lam comp => .lam <| abstractComputationLvl me (level+1) comp
| .hdl h => .hdl <| abstractHandlerLvl me level h
| .pair v₁ v₂ => .pair (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .recfun body => .recfun <| abstractComputationLvl me (level+2) body
| .string s => .string s
| .bool b => .bool b
| .unit => .unit
| .var (.bvar b) => .var (.bvar b)
| .num n => .num n
termination_by v => sizeOf v
decreasing_by
  all_goals simp
  all_goals grind

def abstractComputationLvl (me : Name) (level : Nat) : Computation → Computation
| .ret v => .ret (abstractValueLvl me level v)
| .opCall op v c => .opCall op (abstractValueLvl me level v) (abstractComputationLvl me (level+1) c)
| .bind c₁ c₂ => .bind (abstractComputationLvl me level c₁) (abstractComputationLvl me (level+1) c₂)
| .ite v c₁ c₂ => .ite (abstractValueLvl me level v) (abstractComputationLvl me level c₁) (abstractComputationLvl me level c₂)
| .app v₁ v₂ => .app (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .handle v c => .handle (abstractValueLvl me level v) (abstractComputationLvl me level c)
| .join v₁ v₂ => .join (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .fst v => .fst (abstractValueLvl me level v)
| .snd v => .snd (abstractValueLvl me level v)
| .add v₁ v₂ => .add (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .sub v₁ v₂ => .sub (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .max v₁ v₂ => .max (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .lt v₁ v₂ => .lt (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .mul v₁ v₂ => .mul (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
| .eq v₁ v₂ => .eq (abstractValueLvl me level v₁) (abstractValueLvl me level v₂)
termination_by c => sizeOf c
decreasing_by
  all_goals simp
  all_goals grind

def abstractOps (me : Name) (level : Nat) : List OpClause → List OpClause
| [] => []
| ⟨op, body⟩ :: ls =>
  ⟨op, abstractComputationLvl me (level+2) body⟩ :: abstractOps  me level ls
termination_by l => sizeOf l

def abstractHandlerLvl (me : Name) (level : Nat) : Handler → Handler
| ⟨ret, ops'⟩ =>
    ⟨abstractComputationLvl me (level+1) ret, abstractOps me level ops'⟩
termination_by h => sizeOf h
decreasing_by
  all_goals simp
  all_goals grind

def instantiateValueLvl (what : Value) (level : Nat) : Value → Value
| var@(.var (.bvar bvarLevel)) => if bvarLevel = level then what else var
| .lam c => .lam <| instantiateComputationLvl what (level + 1) c
| .hdl h => .hdl <| instantiateHandlerLvl what level h
| .pair v₁ v₂ => .pair (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .recfun c => .recfun <| instantiateComputationLvl what (level + 2) c
| .string s => .string s
| .bool b => .bool b
| .unit => .unit
| .var v => .var v
| .num n => .num n
termination_by v => sizeOf v
decreasing_by
  all_goals simp
  all_goals grind

def instantiateComputationLvl (what : Value) (level : Nat) : Computation → Computation
| .ret v => .ret <| instantiateValueLvl what level v
| .opCall op v c => .opCall op (instantiateValueLvl what level v) (instantiateComputationLvl what (level+1) c)
| .bind c₁ c₂ => .bind (instantiateComputationLvl what level c₁) (instantiateComputationLvl what (level+1) c₂)
| .ite v c₁ c₂ => .ite (instantiateValueLvl what level v) (instantiateComputationLvl what level c₁) (instantiateComputationLvl what level c₂)
| .app v₁ v₂ => .app (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .handle v c => .handle (instantiateValueLvl what level v) (instantiateComputationLvl what level c)
| .join v₁ v₂ => .join (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .fst v => .fst (instantiateValueLvl what level v)
| .snd v => .snd (instantiateValueLvl what level v)
| .add v₁ v₂ => .add (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .sub v₁ v₂ => .sub (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .max v₁ v₂ => .max (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .lt v₁ v₂ => .lt (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .mul v₁ v₂ => .mul (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
| .eq v₁ v₂ => .eq (instantiateValueLvl what level v₁) (instantiateValueLvl what level v₂)
termination_by c => sizeOf c
decreasing_by
  all_goals simp
  all_goals grind

def instantiateOps (what : Value) (level : Nat) : List OpClause → List OpClause
| [] => []
| ⟨op, body⟩ :: ls =>
  ⟨op, instantiateComputationLvl what (level+2) body⟩ :: instantiateOps what level ls
termination_by l => sizeOf l

def instantiateHandlerLvl (what : Value) (level : Nat) : Handler → Handler
| ⟨ret, ops'⟩ =>
    ⟨instantiateComputationLvl what (level+1) ret, instantiateOps what level ops'⟩
termination_by h => sizeOf h
decreasing_by
  all_goals simp
  all_goals grind

def instantiateComp (what : Value) (comp : Computation) : Computation :=
  instantiateComputationLvl what 0 comp

def printFullName := {{{
  ← print⟨str "What is your forename?"⟩;
  do forename ← read⟨()⟩ in
  ← print⟨str "What is your surname?"⟩;
  do surname ← read⟨()⟩ in
  join(forename, surname)
}}}

def alwaysRead := {{{
  fun s ↦ (return handler {ops := ["read"(x,k) ↦ k s, "print"(x,k) ↦ k ()]})
}}}

def abc := {{{
  ← print⟨str "A"⟩;
  ← print⟨str "B"⟩;
  print⟨str "C"⟩
}}}

def collect := {{{
  handler {
    return x ↦ return pair(x, str ""),
    ops := [
      "print"(s, k) ↦
        do (x, acc) ← k () in
        do joined ← join(s, acc) in
        return pair(x, joined)
    ]
  }
}}}

def reverse := {{{
  handler {
    ops := ["print"(s,k) ↦ ← k (); print⟨s⟩]
  }
}}}

def collect' := {{{
  handler {
    return x ↦ return (fun acc ↦ (return pair(x, acc))),
    ops := [
      "print"(s, k) ↦
        return (fun acc ↦
          (do res ← k () in
          do joined ← join(acc, s) in
          res joined))
    ]
  }
}}}

def choose := {{{
  fun xy ↦
    do b ← decide⟨()⟩ in
    if b then fst xy else snd xy
}}}

def pickTrue := {{{
  handler {ops := ["decide"(_x, k) ↦ k True]}
}}}

def chooseDiff := {{{
  do x₁ ← ~choose pair(15,30) in
  do x₂ ← ~choose pair(5,10) in
  x₁ - x₂
}}}

def pickMax := {{{
  handler {ops := ["decide"(_x, k) ↦
    do xt ← k True in
    do xf ← k False in
    max(xt, xf)
  ]}
}}}

def chooseInt := {{{
  recfun chooseInt mn ↦
    do m ← fst mn in
    do n ← snd mn in
    do isNLtM ← n < m in
    if isNLtM then
      fail⟨()⟩
    else
      do b ← decide⟨()⟩ in
      if b then (return m) else
      do mPlusOne ← m + 1 in
      chooseInt pair(mPlusOne, n)
}}}

def isSquare := {{{
  fun n ↦
  (recfun isSquareAux nAcc ↦
    do n ← fst nAcc in
    do acc ← snd nAcc in
    do accSquared ← acc * acc in
    do isNLtAccSquared ← n < accSquared in
    if isNLtAccSquared then
      return pair(False, 0)
    else
      do isNEqAccSquared ← n == accSquared in
      if isNEqAccSquared then
        return pair(True, acc)
      else
        do accPlusOne ← acc + 1 in
        isSquareAux pair(n, accPlusOne)) pair(n, 0)
}}}

def pythagorean := {{{
  fun mn ↦
    do m ← fst mn in
    do n ← snd mn in
    do nMinusOne ← n - 1 in
    do a ← ~chooseInt pair(m, nMinusOne) in
    do aPlusOne ← a + 1 in
    do b ← ~chooseInt pair(aPlusOne, n) in
    do aSquared ← a * a in
    do bSquared ← b * b in
    do a2Plusb2 ← aSquared + bSquared in
    do (isSquare, sqrt) ← ~isSquare a2Plusb2 in
    if isSquare then
      return pair(a, pair(b, sqrt))
    else
      fail⟨()⟩
}}}

def backtrack := {{{
  handler {ops := ["decide"(_x, k) ↦
    with
      handler {ops := ["fail"(_x,_k) ↦ k False]}
    handle
      k True
  ]}
}}}

def main : IO Unit :=
  let hello_world := evalLang {{{
    do (_a, out) ←
      with ~collect handle
        ← print⟨str "Hello,"⟩;
        print⟨str "world!"⟩
      in
    return out
  }}}

  IO.println hello_world

def evalSingleStep : Computation → Option Computation
 
| .app (.lam body) v => some <| instantiateComp v body
 
| .app (.recfun body) v => some <| instantiate2 (.recfun body) v body
| .ite (.bool true) c₁ _ => some c₁
| .ite (.bool false) _ c₂ => some c₂
 
| .bind (.ret v) c => some <| instantiateComp v c
 
| .bind (.opCall op v body) c => some <| .opCall op v (.bind body c)
| .bind c₁ c₂ => (evalSingleStep c₁).map (fun c₁' => .bind c₁' c₂)
   
| .handle (.hdl h) (.ret v) => some <| instantiateComp v h.ret
| .handle (.hdl h) (.opCall op v body) =>
  match h.lookup op with
   
  | some ⟨_, c⟩ =>
    let cont := .lam (.handle (.hdl h) body)
    some <| instantiate2 v cont c
   
  | none => some <| .opCall op v (.handle (.hdl h) body)
| .handle (.hdl h) c =>
  (evalSingleStep c).map (fun c' => .handle (.hdl h) c')
| .join (.string s₁) (.string s₂) => some <| .ret (.string (strAppend s₁ s₂))
| .fst (.pair v₁ _) => some <| .ret v₁
| .snd (.pair _ v₂) => some <| .ret v₂
| .add (.num v₁) (.num v₂) => some <| .ret (.num (v₁ + v₂))
| .sub (.num v₁) (.num v₂) => some <| .ret (.num (v₁ - v₂))
| .max (.num v₁) (.num v₂) => some <| .ret (.num (Max.max v₁ v₂))
| .lt (.num v₁) (.num v₂) => some <| .ret (.bool (v₁ < v₂))
| .mul (.num v₁) (.num v₂) => some <| .ret (.num (v₁ * v₂))
| .eq v₁ v₂ => some <| .ret (.bool (v₁ == v₂))
| _ => none

def evalFuel : Nat → Computation → Option Computation
| 0, _ => none
| _+1, .ret v => some <| .ret v
| _+1, .opCall n v c => some <| .opCall n v c
| n+1, c =>
  match evalSingleStep c with
  | some c' => evalFuel n c'
  | none => none

def eval : Computation → Option Computation
| .ret v => some <| .ret v
| .opCall n v c => some <| .opCall n v c
| c =>
  match evalSingleStep c with
  | some c' => eval c'
  | none => none
partial_fixpoint

def evalLang (c : Computation) : Computation := (eval c).getD (.ret (.var (.fvar "Error")))

macro "#evalLang " e:term : command =>
  `(#eval (evalLang $e))

def simplify : Computation → Option Computation
| .ret v => some (.ret v)
| c =>
  match evalSingleStep c with
  | some c' => simplify c'
  | none => some c
partial_fixpoint

macro "#simplifyLang " e:term : command =>
  `(#eval (simplify $e).getD (.ret (.var (.fvar "Error"))))

def evalTrace' : Computation → List Computation → List Computation
| .ret v, xs => .ret v :: xs
| c, xs =>
  match evalSingleStep c with
  | some c' => evalTrace' c' (c :: xs)
  | none => c :: xs
partial_fixpoint

def evalTrace (c : Computation) : List Computation := evalTrace' c [] |>.reverse

macro "#evalLangTrace " e:term : command =>
  `(#eval (evalTrace $e).foldl (fun acc s => acc ++ repr s ++ "\n\n") "")

inductive ValueTy where
| bool | string | num | void | unit
| pair : ValueTy → ValueTy → ValueTy
| function : ValueTy → ComputationTy → ValueTy
| handler : ComputationTy → ComputationTy → ValueTy
deriving DecidableEq, Repr

structure ComputationTy where
  returnTy : ValueTy
  Δ : List String
deriving DecidableEq, Repr

inductive Ty where
| val : ValueTy → Ty
| comp : ComputationTy → Ty

instance : Coe ValueTy Ty where
  coe := .val

instance : Coe ComputationTy Ty where
  coe := .comp

inductive Expr where
| val : Value → Expr
| comp : Computation → Expr

instance : Coe Value Expr where
  coe := .val

instance : Coe Computation Expr where
  coe := .comp

abbrev OpSignature := Std.TreeMap String (ValueTy × ValueTy)

abbrev Ctx := List ValueTy

def OpSignature.inputType (σ : OpSignature) (s : String)
  (h : s ∈ σ := by admit /- proof elided -/
  ) := σ.get s h |>.1

def OpSignature.outputType (σ : OpSignature) (s : String)
  (h : s ∈ σ := by admit /- proof elided -/
  ) := σ.get s h |>.2

def lookup : Ctx → Nat → Option ValueTy
| [], _ => none
| τ::_, 0 => some τ
| _::Γ, n+1 => lookup Γ n

inductive HasType (σ : OpSignature) : Ctx → Expr → Ty → Prop where
 
| var x A : ((x : A) ∈ Γ) → HasType σ Γ (Value.var (.bvar x)) A
 
| bool b : HasType σ Γ (Value.bool b) ValueTy.bool
 
| lam A (c : Computation) (C : ComputationTy) :
  HasType σ (A :: Γ) c C → HasType σ Γ (Value.lam c) (ValueTy.function A C)
 
| handler (cr : Computation) :
  HasType σ (A :: Γ) cr (B ! Δ') → 
  (h: ∀opClause ∈ ops, opClause.op ∈ σ) → 
  (∀mem : opClause ∈ ops,
    let Aᵢ := σ.inputType opClause.op
    let Bᵢ := σ.outputType opClause.op
    let k := ValueTy.function Bᵢ (B ! Δ')
    HasType σ (k :: Aᵢ :: Γ) opClause.body (B ! Δ')
  ) → 
  (Δ.removeAll (ops.map (·.op)) ⊆ Δ') → 
  HasType σ Γ (Value.hdl (Handler.mk cr ops))
    (ValueTy.handler (A ! Δ) (B ! Δ'))
| ret (v : Value) Δ (A : ValueTy) : HasType σ Γ v A →
  HasType σ Γ (Computation.ret v) (A ! Δ)
 
| op (v : Value) (c : Computation) :
  (h : name ∈ σ) → 
  HasType σ Γ v (σ.inputType name) → 
  HasType σ (σ.outputType name :: Γ) c (A ! Δ) → 
  (name ∈ Δ) → 
  HasType σ Γ (Computation.opCall name v c) (A ! Δ)
 
| bind (c₁ c₂ : Computation):
  HasType σ Γ c₁ (A ! Δ) → HasType σ (A :: Γ) c₂ (B ! Δ) →
  HasType σ Γ (Computation.bind c₁ c₂) (B ! Δ)
 
| app (v₁ v₂ : Value) :
  HasType σ Γ v₁ (ValueTy.function A C) → HasType σ Γ v₂ A →
  HasType σ Γ (Computation.app v₁ v₂) C
 
| ite (v : Value) (c₁ c₂ : Computation) :
  HasType σ Γ v ValueTy.bool → HasType σ Γ c₁ C → HasType σ Γ c₂ C →
  HasType σ Γ (Computation.ite v c₁ c₂) C
 
| handle (v : Value) (c : Computation) :
  HasType σ Γ v (ValueTy.handler C D) → HasType σ Γ c C →
  HasType σ Γ (Computation.handle v c) D

macro "[σ| " elems:sigma,* "]" : term => do
  let elems := elems.getElems
  let transformed ← elems.mapM fun stx =>
    match stx with
    | `(sigma| ( $s, $e1 ⟶ $e2 )) =>

def checkValType (op : OpSignatureList) (t : ValueTy) (v : Value) : Bool := (do
  let type ← inferValType op v
  let constraint : Constraints := [.valEq type t]
  unify constraint).toBool

def checkCompType (op : OpSignatureList) (t : ComputationTy) (c : Computation) : Bool := (do
  let type ← inferCompType op c
  let constraint : Constraints := [.valEq type.returnTy t.returnTy]
  unify constraint).toBool

def checkType (op : OpSignatureList) : Ty → Expr →  Bool
| .val vt, .val v => checkValType op vt v
| .comp ct, .comp c => checkCompType op ct c
| _, _ => false

abbrev Name := String

inductive Var where
| fvar : Name → Var
| bvar : Nat → Var
deriving Repr, DecidableEq

inductive Value where
| var : Var → Value
| bool : Bool → Value
| string : String → Value
| num : Int → Value
| unit : Value
| pair : Value → Value → Value
 
| lam : Computation → Value
 
| recfun : Computation → Value
| hdl : Handler → Value
deriving BEq

inductive Computation where
| ret : Value → Computation
 
| opCall : Name → Value → Computation → Computation
 
| bind : Computation → Computation → Computation
| ite (val : Value) (trueBranch falseBranch : Computation)
| app : Value → Value → Computation
 
| handle : Value → Computation → Computation
| join : Value → Value → Computation
| fst : Value → Computation
| snd : Value → Computation
| add : Value → Value → Computation
| sub : Value → Value → Computation
| mul : Value → Value → Computation
| max : Value → Value → Computation
| lt : Value → Value → Computation
| eq : Value → Value → Computation
deriving BEq

structure OpClause where
  op : Name
   
  body : Computation
deriving Repr, BEq

structure Handler where
   
  ret : Computation
  ops : List OpClause
deriving Repr, BEq

structure BoundCtx where
  bound : List String

def BoundCtx.addBvar (ctx : BoundCtx) (name : String) : BoundCtx := ⟨name :: ctx.bound⟩

def BoundCtx.lookup (ctx : BoundCtx) (bvar : Nat) : String :=
  ctx.bound[bvar]?.getD (toString bvar)

def BoundCtx.getNewName (ctx : BoundCtx) : String := "x" ++ toString ctx.bound.length

def Value.format (prec : Nat) (ctx : BoundCtx): Value → Format
| .var (.bvar n) => .group <| ctx.lookup n
| .var (.fvar n) => n
| .bool true => "True"
| .bool false => "False"
| .string s => "\"" ++ s ++ "\""
| .pair v₁ v₂ => .group <| "(" ++  v₁.format prec ctx ++ ", " ++ v₂.format prec ctx ++ ")"
| .unit => "()"
| .num n => repr n
| .lam c =>
  let name := ctx.getNewName
  .group <| "fun " ++ name ++ " ↦ " ++ .nest 2 (.line ++ c.format prec (ctx.addBvar name))
| .recfun c =>
  let name1 := ctx.getNewName
  let name2 := (ctx.addBvar name1).getNewName
  let newCtx := (ctx.addBvar name1).addBvar name2
  .group <| "recfun " ++ name1 ++ " " ++ name2 ++ " ↦ " ++ .nest 2 (.line ++ c.format prec newCtx)
| .hdl h => h.format prec ctx

def Computation.format (prec : Nat) (ctx : BoundCtx) : Computation → Format
| .ret v => .group <| "return " ++ v.format prec ctx
| .handle h c => .group <| "with " ++ h.format prec ctx ++ " handle" ++ .line ++ .nest 2 (c.format prec ctx)
| .app v₁ v₂ => .group <| v₁.format prec ctx ++ " " ++ v₂.format prec ctx
| .ite v c₁ c₂ => .group <| "if " ++ v.format prec ctx ++ .line ++ " then " ++
  c₁.format prec ctx ++ .line ++ " else " ++ c₂.format prec ctx
| .bind c₁ c₂ =>
  let name := ctx.getNewName
  .group <| "do " ++ name ++ " ← " ++ c₁.format prec ctx ++ " in " ++ .line ++ c₂.format prec (ctx.addBvar name)
| .opCall name v c =>
  let newName := ctx.getNewName
  .group <| name ++ "⟨" ++ v.format prec ctx ++ "; fun " ++ newName ++ " ↦ " ++ c.format prec (ctx.addBvar newName) ++ "⟩"
| .join v₁ v₂ => .group <| "join(" ++ v₁.format prec ctx ++ ", " ++ v₂.format prec ctx ++ ")"
| .fst v => .group <| "fst " ++ v.format prec ctx
| .snd v => .group <| "snd " ++ v.format prec ctx
| .add v₁ v₂ => .group <| v₁.format prec ctx ++ " + " ++ v₂.format prec ctx
| .sub v₁ v₂ => .group <| v₁.format prec ctx ++ " - " ++ v₂.format prec ctx
| .max v₁ v₂ => .group <| "max(" ++ v₁.format prec ctx ++ ", " ++ v₂.format prec ctx ++ ")"
| .lt v₁ v₂ => .group <| v₁.format prec ctx ++ " < " ++ v₂.format prec ctx
| .mul v₁ v₂ => .group <| v₁.format prec ctx ++ " * " ++ v₂.format prec ctx
| .eq v₁ v₂ => .group <| v₁.format prec ctx ++ " == " ++ v₂.format prec ctx

def OpClause.format (prec : Nat) (ctx : BoundCtx) : OpClause → Format
| ⟨op, body⟩ =>
  let name1 := ctx.getNewName
  let name2 := (ctx.addBvar name1).getNewName
  let opsCtx := (ctx.addBvar name1).addBvar name2
  .group <| "{" ++ op ++ "(" ++ name1 ++ ", " ++ name2 ++ ") ↦ " ++ .line ++ body.format prec opsCtx ++ "}"

def Handler.format (prec : Nat) (ctx : BoundCtx) : Handler → Format
| ⟨ret, ops⟩ =>
  let name := ctx.getNewName
  let retStr := "return " ++ name ++ " ↦ " ++ ret.format prec (ctx.addBvar name)
  .group <| "{" ++ retStr ++ ", " ++ .line ++ "ops := [" ++
    .joinSep (ops.map (·.format prec ctx)) (", " ++ .line) ++ "]}"
where
  repr : Option Computation → Format
  | none => "none"
  | some c => c.format prec (ctx.addBvar ctx.getNewName)

instance : Repr Computation where
  reprPrec comp n := comp.format n ⟨[]⟩

instance : Repr Value where
  reprPrec value n := value.format n ⟨[]⟩

instance : ToString Computation where
  toString := toString ∘ repr

instance : ToString Value where
  toString := toString ∘ repr

structure Ctx where
  bound : List Lean.Name

abbrev ElabM := StateT Ctx TermElabM

def lookup (x : Lean.Name) : Ctx → Option Nat
| ⟨bs⟩ => bs.idxOf? x

def extractLambdaBody : TSyntax `term → TSyntax `term
| `(term| Value.lam $body) => body
| _ => TSyntax.mk Syntax.missing

def withBoundIdentifier (id : Lean.Name) (cont : ElabM (TSyntax `term)) : ElabM (TSyntax `term) := do
  modify (fun ⟨bs⟩ => ⟨id :: bs⟩)
  let res ← cont
  modify (fun | ⟨_::bs⟩ => ⟨bs⟩ | ⟨[]⟩ => ⟨[]⟩)
  return res

partial def toTermSyntax : Syntax → ElabM (TSyntax `term)
 
| `(embedded| $x:ident) => do
  let ctx ← get
  match lookup x.getId ctx with
  | some k => `(Value.var (Var.bvar $(Lean.quote k)))
  | none => `(Value.var (Var.fvar $(Lean.quote x.getId.toString)))
| `(embedded| True) => `(Value.bool true)
| `(embedded| False) => `(Value.bool false)
| `(embedded| ( $e )) => toTermSyntax e

| `(embedded| fun $x:ident ↦ $body) => do
  let bodyTerm ← withBoundIdentifier x.getId (toTermSyntax body)
  `(Value.lam $bodyTerm)
| `(embedded| recfun $f:ident $x:ident ↦ $body) => do
    let bodyTerm ← withBoundIdentifier f.getId (withBoundIdentifier x.getId (toTermSyntax body))
    `(Value.recfun $bodyTerm)
| `(embedded| $f $arg) => do
  let fTerm ← toTermSyntax f
  let argTerm ← toTermSyntax arg
  `(Computation.app $fTerm $argTerm)
| `(embedded| return $e) => do
  let t ← toTermSyntax e
  `(Computation.ret $t)
| `(embedded| $op:ident ⟨ $v ; $k ⟩) => do
  let vTerm ← toTermSyntax v
   
  let kTerm := extractLambdaBody (←toTermSyntax k)
  `(Computation.opCall $(Lean.quote op.getId.toString) $vTerm $kTerm)

| `(embedded| $op:ident ⟨$v⟩) => do
  let newSyntax : TSyntax `embedded ← `(embedded| $op:ident ⟨$v; fun y ↦ (return y)⟩)
  toTermSyntax newSyntax.raw
| `(embedded| do $x:ident ← $c₁ in $c₂) => do
  let c₁Term ← toTermSyntax c₁
  let c₂Term ← withBoundIdentifier x.getId (toTermSyntax c₂)
  `(Computation.bind $c₁Term $c₂Term)
| `(embedded| ← $c₁; $c₂) => do
  let c₁Term ← toTermSyntax c₁
  let c₂Term ← withBoundIdentifier (←mkFreshUserName `x) (toTermSyntax c₂)
  `(Computation.bind $c₁Term $c₂Term)

| `(embedded| if $v then $c₁ else $c₂) => do
  let vTerm ← toTermSyntax v
  let c₁Term ← toTermSyntax c₁
  let c₂Term ← toTermSyntax c₂
  `(Computation.ite $vTerm $c₁Term $c₂Term)

| `(embedded| with $h handle $c) => do
  let hTerm ← toTermSyntax h
  let cTerm ← toTermSyntax c
  `(Computation.handle $hTerm $cTerm)
| `(embedded| ~$e) => pure e

| `(embedded| $t:str ($x, $k) ↦ $e) => do
  let eTerm ← withBoundIdentifier x.getId (withBoundIdentifier k.getId (toTermSyntax e))
  `(OpClause.mk $t $eTerm)
| `(embedded| handler {return $x ↦ $e, ops := [$xs,*] }) => do
  
  let eTerm ← withBoundIdentifier x.getId (toTermSyntax e)
  
  let opsTerms ← xs.getElems.mapM (toTermSyntax ·)
  `(Value.hdl (Handler.mk $eTerm [$opsTerms,*]))
| `(embedded| handler {ops := [$xs,*] }) => do
    let opsTerms ← xs.getElems.mapM (toTermSyntax ·)
    `(Value.hdl (Handler.mk (Computation.ret (Value.var (Var.bvar 0))) [$opsTerms,*]))

| `(embedded| str $s:str) => `(Value.string $s)

| `(embedded| join($e1, $e2)) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Computation.join $e1Term $e2Term)

| `(embedded| ()) => `(Value.unit)

| `(embedded| pair($e1, $e2)) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Value.pair $e1Term $e2Term)

| `(embedded| fst $e) => do
  let eTerm ← toTermSyntax e
  `(Computation.fst $eTerm)

| `(embedded| snd $e) => do
  let eTerm ← toTermSyntax e
  `(Computation.snd $eTerm)

| `(embedded| do ($x, $y) ← $c₁ in $c₂) => do
  let newSyntax : TSyntax `embedded ← `(embedded|
    do c ← $c₁ in
    do $x ← fst c in
    do $y ← snd c in
    $c₂)
  toTermSyntax newSyntax.raw

| `(embedded| $n:num) => `(Value.num $n)
| `(embedded| -$e) => do
  let eTerm ← toTermSyntax e
  match eTerm with
  | `(term| Value.num $n) => `(Value.num (-$n))
  | _ => pure <| TSyntax.mk Syntax.missing
| `(embedded| $e₁ + $e₂) => do
  let e1Term ← toTermSyntax e₁
  let e2Term ← toTermSyntax e₂
  `(Computation.add $e1Term $e2Term)
| `(embedded| $e₁ - $e₂) => do
  let e1Term ← toTermSyntax e₁
  let e2Term ← toTermSyntax e₂
  `(Computation.sub $e1Term $e2Term)
| `(embedded| max($e1, $e2)) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Computation.max $e1Term $e2Term)
| `(embedded| $e1 < $e2) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Computation.lt $e1Term $e2Term)
| `(embedded| $e1 * $e2) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Computation.mul $e1Term $e2Term)
| `(embedded| $e1 == $e2) => do
  let e1Term ← toTermSyntax e1
  let e2Term ← toTermSyntax e2
  `(Computation.eq $e1Term $e2Term)
| _ => pure <| TSyntax.mk Syntax.missing

@[term_elab embeddedTerm] def elabEmbedded : TermElab := fun stx _ => do
  let body := stx[1]
  let termStx ← (toTermSyntax body).run ⟨[]⟩
  elabTerm termStx.1 none

IO in Init.System.IO

Unit in Init.Prelude

IO.println in Init.System.IO

DecidableEq in Init.Prelude

Inhabited in Init.Prelude

Nat in Init.Prelude

bool in Init.Control.Basic

Bool in Init.Prelude

Std.Format in Init.Data.Format.Basic

Lean.Parser.group in Lean.Parser.Extra

Repr in Init.Data.Repr

ToString in Init.Data.ToString.Basic

repr in Init.Data.Repr

Except in Init.Prelude

String in Init.Prelude

Except.ok in Init.Prelude

Lean.Parser.error in Lean.Parser.Basic

List in Init.Prelude

Coe in Init.Coe

ExceptT in Init.Control.Except

StateM in Init.Control.State

modify in Init.Prelude

Except.error in Init.Prelude

Computation in Mathlib.Data.Seq.Computation

ite in Init.Prelude

id in Init.Prelude

Std.TreeMap in Std.Data.TreeMap.Basic

Std.TreeMap.ofList in Std.Data.TreeMap.Basic

Max in Init.Prelude

Max.max in Init.Prelude

Option in Init.Prelude

Lean.Name in Init.Prelude

StateT in Init.Control.State

Lean.TSyntax in Init.Prelude

Lean.Syntax.missing in Init.Prelude

Lean.TSyntax.mk in Init.Prelude

Lean.Syntax in Init.Prelude

BEq in Init.Prelude

Int in Init.Data.Int.Basic
</all_available_defs>

<all_available_lemmas>
theorem step_determinism (c c₁ c₂ : Computation) (c_step_c₁ : c ⤳ c₁)
    (c_step_c₂ : c ⤳ c₂) : c₁ = c₂
</all_available_lemmas>

<local_ctx>
import IntroEffects.SmallStep

def evalSingleStep : Computation → Option Computation
 
| .app (.lam body) v => some <| instantiateComp v body
 
| .app (.recfun body) v => some <| instantiate2 (.recfun body) v body
| .ite (.bool true) c₁ _ => some c₁
| .ite (.bool false) _ c₂ => some c₂
 
| .bind (.ret v) c => some <| instantiateComp v c
 
| .bind (.opCall op v body) c => some <| .opCall op v (.bind body c)
| .bind c₁ c₂ => (evalSingleStep c₁).map (fun c₁' => .bind c₁' c₂)
   
| .handle (.hdl h) (.ret v) => some <| instantiateComp v h.ret
| .handle (.hdl h) (.opCall op v body) =>
  match h.lookup op with
   
  | some ⟨_, c⟩ =>
    let cont := .lam (.handle (.hdl h) body)
    some <| instantiate2 v cont c
   
  | none => some <| .opCall op v (.handle (.hdl h) body)
| .handle (.hdl h) c =>
  (evalSingleStep c).map (fun c' => .handle (.hdl h) c')
| .join (.string s₁) (.string s₂) => some <| .ret (.string (strAppend s₁ s₂))
| .fst (.pair v₁ _) => some <| .ret v₁
| .snd (.pair _ v₂) => some <| .ret v₂
| .add (.num v₁) (.num v₂) => some <| .ret (.num (v₁ + v₂))
| .sub (.num v₁) (.num v₂) => some <| .ret (.num (v₁ - v₂))
| .max (.num v₁) (.num v₂) => some <| .ret (.num (Max.max v₁ v₂))
| .lt (.num v₁) (.num v₂) => some <| .ret (.bool (v₁ < v₂))
| .mul (.num v₁) (.num v₂) => some <| .ret (.num (v₁ * v₂))
| .eq v₁ v₂ => some <| .ret (.bool (v₁ == v₂))
| _ => none

def evalFuel : Nat → Computation → Option Computation
| 0, _ => none
| _+1, .ret v => some <| .ret v
| _+1, .opCall n v c => some <| .opCall n v c
| n+1, c =>
  match evalSingleStep c with
  | some c' => evalFuel n c'
  | none => none
</local_ctx>

<target_theorem>
theorem evalFuel_sound  : evalFuel n c = some v → c ⤳⋆ v :=
</target_theorem>

