(* Requires Iris master e1764691 *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

Section swap.
  Context `{!heapG Σ}.
  Notation iProp := (iProp Σ).
  Implicit Types l : loc.

  Definition swap : val := λ: "x" "y",
    let: "tmp" := !"x" in
    "x" <- !"y";;
    "y" <- "tmp".
 
  Lemma swap_spec l1 l2 v1 v2 :
    {{ l1 ↦ v1 ∗ l2 ↦ v2 }} swap #l1 #l2 {{ w, ⌜w = #()⌝ ∗ l1 ↦ v2 ∗ l2 ↦ v1 }}.
  Proof.
    iIntros "!# [Hl1 Hl2]".
    do 2 wp_let.
    wp_load.
    wp_let.
    wp_load.
    wp_store.
    wp_store.
    iFrame.
    auto.
  Restart.
    Ltac solve := repeat (wp_let || wp_load || wp_store); iFrame; auto.
    iIntros "!# [Hl1 Hl2]".
    solve.
  Qed.
End swap.

Section list_reverse.
  Context `{!heapG Σ}.
  Notation iProp := (iProp Σ).
  Implicit Types l : loc.

  Fixpoint is_list (hd : val) (xs : list val) : iProp :=
    match xs with
    | [] => ⌜hd = NONEV⌝
    | x :: xs => ∃ l hd', ⌜hd = SOMEV #l⌝ ∗ l ↦ (x,hd') ∗ is_list hd' xs
    end%I.

  Definition rev : val :=
    rec: "rev" "hd" "acc" :=
      match: "hd" with
        NONE => "acc"
      | SOME "l" =>
         let: "tmp1" := Fst !"l" in
         let: "tmp2" := Snd !"l" in
         "l" <- ("tmp1", "acc");;
         "rev" "tmp2" "hd"
      end.

  Lemma rev_acc_ht hd acc xs ys :
    {{ is_list hd xs ∗ is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
  Proof.
    iIntros "!# [Hxs Hys]".
    iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
    destruct xs as [|x xs]; iSimplifyEq.
    - (* nil *) by wp_match.
    - (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
      wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
      rewrite reverse_cons -assoc.
      iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
      iExists l, acc; by iFrame.
  Qed.

  Lemma rev_ht hd xs :
    {{ is_list hd xs }} rev hd NONE {{ w, is_list w (reverse xs) }}.
  Proof.
    iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
    iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
  Qed.
End list_reverse.