Use expr's and IntoVal as much as possible

theories/c_translation/derived.v

@@ -8,7 +8,6 @@ Section Derived.
 
   Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
 
-
   Lemma a_load_ret (l: loc) (w: val) R Φ:
     l ↦U w ∗ (l ↦U w -∗ Φ w) -∗
     awp (a_load (a_ret (#l)%E)) R Φ.
@@ -18,11 +17,12 @@ Section Derived.
     iExists l, w. by iFrame.
   Qed.
 
-  Lemma a_alloc_ret (w: val) R Φ:
-    (∀ (l: loc), (l ↦U w -∗ Φ #l)) -∗
-    awp (a_alloc (a_ret w)) R Φ.
+  Lemma a_alloc_ret (e: expr) (ev: val) R Φ:
+    IntoVal e ev →
+    (∀ (l: loc), (l ↦U ev -∗ Φ #l)) -∗
+    awp (a_alloc (a_ret e)) R Φ.
   Proof.
-    iIntros "H". iApply a_alloc_spec.
+    iIntros (<-%of_to_val) "H". iApply a_alloc_spec.
     iApply awp_ret. by wp_value_head.
   Qed.
 

theories/c_translation/monad.v

@@ -113,7 +113,6 @@ Section a_wp_rules.
     iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. iFrame.
   Qed.
 
-  (* Use [IntoVal] everywhere *)
   Lemma awp_bind (f e : expr) R Φ :
     AsVal f →
     awp e R (λ ev, awp (f ev) R Φ) -∗
@@ -127,7 +126,7 @@ Section a_wp_rules.
     iIntros (v) "H". by iApply ("H" with "[$]").
   Qed.
 
-  Lemma awp_atomic e (ev : val) R Φ :
+  Lemma awp_atomic (e : expr) (ev : val) R Φ :
     IntoVal e ev →
     (R -∗ ∃ R', R' ∗ awp (ev #()) R' (λ w, R' -∗ R ∗ Φ w)) -∗
     awp (a_atomic e) R Φ.
@@ -148,7 +147,7 @@ Section a_wp_rules.
     iIntros "Hunfl1". wp_seq. iFrame.
   Qed.
 
-  Lemma awp_atomic_env e (ev : val) R Φ :
+  Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
     IntoVal e ev →
     (∀ env, env_inv env -∗ R -∗
       WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
@@ -191,11 +190,12 @@ End a_wp_rules.
 Section a_wp_run.
   Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
 
-  Lemma awp_run (v : val) R Φ :
-    R -∗ (∀ `{locking_heapG Σ}, awp v R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗
-    WP a_run v {{ Φ }}.
+  Lemma awp_run (e : expr) R Φ :
+    AsVal e →
+    R -∗ (∀ `{locking_heapG Σ}, awp e R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗
+    WP a_run e {{ Φ }}.
   Proof.
-    iIntros "HR Hwp". rewrite /awp /a_run /=. wp_let.
+    iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
     wp_bind (mset_create #()). iApply mset_create_spec; first done.
     iNext. iIntros (env) "Henv". wp_let.
     iMod (locking_heap_init ∅) as (?) "Hσ".

theories/c_translation/translation.v

@@ -79,7 +79,7 @@ Section proofs.
     iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
   Qed.
 
-  Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
+  Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
      awp e1 R Φ -∗ awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
   Proof.
     iIntros "HΦ".
@@ -88,7 +88,7 @@ Section proofs.
     iLeft. iSplit; eauto. by awp_seq.
   Qed.
 
-  Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
+  Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
      awp e2 R Φ -∗ awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ.
   Proof.
     iIntros "HΦ".