a file for notations and testing file basics.v where all small examples can be written

_CoqProject

@@ -8,16 +8,15 @@ theories/lib/U.v
 theories/c_translation/monad.v
 theories/c_translation/proofmode.v
 theories/c_translation/translation.v
+theories/c_translation/notation.v
 theories/c_translation/derived.v
 theories/vcgen/dcexpr.v
 theories/vcgen/denv.v
 theories/vcgen/splitenv.v
 theories/vcgen/vcgen.v
+theories/vcgen/tests/basics.v
 theories/vcgen/tests/test.v
 theories/vcgen/tests/swap.v
-# theories/heap_lang_vcgen/dval.v
-# theories/heap_lang_vcgen/vcgen.v
-# theories/heap_lang_vcgen/test.v
 theories/tests/test1.v
 theories/tests/test2.v
 theories/tests/fact.v

theories/c_translation/notation.v

+From iris.program_logic Require Import language.
+From iris.heap_lang Require Export lang notation.
+From iris_c.c_translation Require Import monad translation.
+Set Default Proof Using "Type".
+
+Definition ret (v: val) : expr := a_ret v.
+
+Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
+Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
+
+Notation "! e" :=
+  (a_load e%E) (at level 9, right associativity) : expr_scope.
+
+Notation "e1 ⨟ e2" := (e1%E ;;;; e2%E)
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']'  ⨟  ']' '/' e2 ']'") : expr_scope.
+
+Notation "e1 ≕ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.

theories/vcgen/tests/basics.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.algebra Require Import frac.
+From iris.bi Require Import big_op.
+From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
+From iris_c.c_translation Require Import monad translation proofmode notation.
+From iris_c.lib Require Import locking_heap U.
+
+Section test.
+  Context `{amonadG Σ}.
+
+  Lemma test1 (l : loc) (v: val) :
+    l ↦C v -∗ awp (! ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
+  Proof.
+    iIntros "Hl1". vcg_solver.
+  Qed.
+
+  (* double dereferencing *)
+  Lemma test2 (l1 l2 : loc) (v: val) :
+    l1 ↦C #l2 -∗ l2 ↦C v -∗
+    awp (! ! ♯l1) True (λ v, ⌜v = #1⌝ ∗ l1 ↦C #l2 -∗ l2 ↦C v).
+  Proof.
+    iIntros "Hl1 Hl2". vcg_solver.
+  Qed.
+
+  Lemma test3 (l : loc) (v: val) :
+    l ↦C v -∗ awp (! ♯l ⨟ ! ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
+  Proof.
+    iIntros "Hl1". vcg_solver. iModIntro. eauto.
+  Qed.
+
+  Lemma test4 (l : loc) (v1 v2: val) :
+    l ↦C v1 -∗ awp ( ♯l ≕ ret v2) True (λ v, ⌜v = v2⌝ ∗ l ↦C[LLvl] v2).
+  Proof.
+    iIntros "Hl1". vcg_solver.
+  Qed.
+
+  (* double dereferencing & modification *)
+  Lemma test5 (l1 l2 r1 r2 : loc) (v1 v2: val) :
+    l1 ↦C #l2 -∗ l2 ↦C v1 -∗
+    r1 ↦C #r2 -∗ r2 ↦C v2 -∗
+    awp ( ♯l1 ≕ ♯r1 ⨟ ! ! ♯l1 ) True
+      (λ w, ⌜w = v2⌝ ∗ l1 ↦C #r2 ∗ l2 ↦C v1 ∗ r1 ↦C #r2 -∗ r2 ↦C v2).
+  Proof.
+    iIntros "Hl1 Hl2 Hr1 Hr2". vcg_solver. iModIntro. eauto.
+  Qed.
+
+End test.
\ No newline at end of file