(* iris_unstable/heap_lang/interpreter.v *)
Fixpoint interpret (fuel:nat) (e: expr) {struct fuel} : InterpretM val
:=
    match fuel with
    | 0 => λ s, (inr OutOfFuel, s)
    | S fuel' => let interp := interpret fuel' in
    match e with

      (* lambda calculus *)
    | Val v => mret v
    | Var x => error $ "free var: " + x
    | Rec f x e => mret (RecV f x e)
    | App f e =>
      v2 ← interp e;
      f ← interp f;
      match f with
      | RecV f x e1 =>
        interp (subst' x v2 (subst' f (RecV f x e1) e1))
      | _ => error $ "attempt to call non-function " +:+ pretty f
      end

    (* mostly boring pure operations (sums, products, unary/binary ops) *)
    | Pair e1 e2 =>
      v2 ← interp e2;
      v1 ← interp e1;
      mret (PairV v1 v2)
    | InjL e => InjLV <$> interp e
    | InjR e => InjRV <$> interp e
    | UnOp op e =>
      v ← interp e;
      match un_op_eval op v with
      | Some v => mret v
      | None => error $ "un-op failed: " + match explain_un_op_fail op v with
                                           | Some msg => msg
                                           | None => "" (* impossible *)
                                           end
      end
    | BinOp op e1 e2 =>
      v2 ← interp e2;
      v1 ← interp e1;
      match bin_op_eval op v1 v2 with
      | Some v => mret v
      | None => error $ "bin-op failed: " + match explain_bin_op_fail op v1 v2 with
                                            | Some msg => msg
                                            | None => "" (* impossible *)
                                            end
      end
    | If e e1 e2 =>
      cond ← interp e;
      match cond with
      | LitV (LitBool b) => interp (if b then e1 else e2)
      | _ => error $ "if: non-bool condition " + cond
      end
    | Fst e =>
      v ← interp e;
      match v with
      | PairV v1 _ => mret v1
      | _ => error $ "fst: called on non-pair " + v
      end
    | Snd e =>
      v ← interp e;
      match v with
      | PairV _ v2 => mret v2
      | _ => error $ "snd: called on non-pair " + v
      end
    | Case e e1 e2 =>
      v ← interp e;
      match v with
      | InjLV v => interp (App e1 (Val v))
      | InjRV v => interp (App e2 (Val v))
      | _ => error $ "case: called on non-sum " + v
      end

    | Fork e =>
      _ ← interp_modify (add_forked_thread e);
      mret (LitV LitUnit)

    (* heap manipulation *)
    | AllocN ne e =>
      v ← interp e;
      nv ← interp ne;
      match nv with
      | LitV (LitInt n) =>
        if decide (0 < n)%Z then
          l ← interp_alloc n;
          _ ← interp_modify_state (state_init_heap l n v);
          mret (LitV (LitLoc l))
        else (error $ if decide (n = 0)
                      then "alloc: cannot allocate 0 elements"
                      else "alloc: negative number of elements (first argument) " + n)
      | _ => error $ "alloc: number of elements (first argument) " + nv
      end
    | Load e =>
      vl ← interp e;
      l_v0 ← read_loc "load" vl;
      let '(_, v0) := l_v0 in
      mret v0
    | Free e =>
      vl ← interp e;
      l_v0 ← read_loc "free" vl;
      let '(l, _) := l_v0 in
      _ ← interp_modify_state (state_upd_heap <[l:=None]>);
      mret (LitV LitUnit)
    | Store el e =>
      w ← interp e;
      vl ← interp el;
      l_v0 ← read_loc "store" vl;
      let '(l, _) := l_v0 in
      _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
      mret (LitV LitUnit)
    | Xchg el e =>
      w ← interp e;
      vl ← interp el;
      l_v0 ← read_loc "xchg" vl;
      let '(l, v0) := l_v0 in
      _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
      mret v0
    | CmpXchg e e1 e2 =>
      v2 ← interp e2;
      v1 ← interp e1;
      vl ← interp e;
      l_v0 ← read_loc "cmpxchg" vl;
      let '(l, vl) := l_v0 in
      let b := bool_decide (vl = v1) in
      if decide (vals_compare_safe vl v1) then
        _ ← interp_modify_state (λ σ, if b
                                      then state_upd_heap <[l:=Some v2]> σ
                                      else σ);
        mret (PairV vl (LitV (LitBool b)))
      else
        error $ "cmpxchg: failed comparison: " + default "" (explain_vals_compare_safe_fail vl v1)
    | FAA el e =>
      v ← interp e;
      vl ← interp el;
      l_v0 ← read_loc "faa" vl;
      let '(l, v0) := l_v0 in
      match v0, v with
      | LitV (LitInt i1), LitV (LitInt i2) =>
        _ ← interp_modify_state (state_upd_heap <[l:=Some (LitV (LitInt (i1 + i2)))]>);
        mret (LitV (LitInt i1))
      (* check constant passed to FAA only if heap value is an integer *)
      | LitV (LitInt _), _ => error $ "faa: increment " + v + " is not an integer"
      | _, _ => error $ "faa: called on non-integer heap value: " + v0
      end

    (* unsupported prophecy variable operations *)
    | NewProph => λ s, (inr (Unsupported "NewProph"), s)
    | Resolve _ _ _ => λ s, (inr (Unsupported "Resolve"), s)
    end
    end.