c-notations with superscript wip

theories/c_translation/notation.v

@@ -8,11 +8,11 @@ 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" :=
+Notation "∗ᶜ e" :=
   (a_load e%E) (at level 9, right associativity) : expr_scope.
 
-Notation "e1 ⨟ e2" := (e1%E ;;;; e2%E)
+Notation "e1 ;ᶜ e2" := (e1%E ;;;; e2%E)
   (at level 100, e2 at level 200,
-   format "'[' '[hv' '[' e1 ']'  ⨟  ']' '/' e2 ']'") : expr_scope.
+   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
 
-Notation "e1 ≕ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.

theories/vcgen/tests/basics.v

@@ -9,27 +9,27 @@ Section test.
   Context `{amonadG Σ}.
 
   Lemma test1 (l : loc) (v: val) :
-    l ↦C v -∗ awp (! ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
+    l ↦C v -∗ awp (∗ᶜ ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
   Proof.
     iIntros "Hl1". vcg_solver.
-  Qed.
+   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).
+    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).
+    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).
+    l ↦C v1 -∗ awp ( ♯l =ᶜ ret v2) True (λ v, ⌜v = v2⌝ ∗ l ↦C[LLvl] v2).
   Proof.
     iIntros "Hl1". vcg_solver.
   Qed.
@@ -38,7 +38,7 @@ Section test.
   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
+    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.