(** Testing function calls and CWP resources *)
From iris_c.vcgen Require Import proofmode.

Section tests_vcg.
  Context `{cmonadG Σ}.

  Definition c_id : val := λ: "v", c_ret "v".

  Lemma test_invoke_1 (l: cloc)  R :
    l ↦C #42 -∗
    CWP callᶜ (c_ret c_id) (∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #42 }}%I.
  Proof.
    iIntros "Hl". vcg. iIntros "Hl !> $ !>".
    cwp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
  Qed.

  Definition plus_pair : val := λ: "vv",
    "v1" ←ᶜ c_ret (Fst "vv");ᶜ
    "v2" ←ᶜ c_ret (Snd "vv");ᶜ
    (c_ret "v1") +ᶜ (c_ret "v2").

  Lemma test_invoke_2 R :
    CWP callᶜ (c_ret plus_pair) (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
  Proof.
    iIntros. vcg. iIntros "!> $ !>". cwp_lam. vcg. by vcg_continue.
  Qed.

  Lemma test_invoke_3 (l : cloc) R :
    l ↦C #21 -∗
    CWP callᶜ (c_ret plus_pair) (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl) @ R
      {{ v, ⌜v = #42⌝ ∗  l ↦C #21 }}%I.
  Proof.
    iIntros. vcg. iIntros "Hl !> $ !>". cwp_lam. vcg.
    iIntros "Hl". vcg_continue; eauto.
  Qed.
End tests_vcg.