Merge branch 'ci/jh/r2l' into 'master'

Right-to-left evaluation order for heaplang

See merge request FP/iris-coq!178

tests/heap_lang.v

@@ -65,12 +65,12 @@ Section tests.
   Qed.
 
   Definition heap_e5 : expr :=
-    let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
+    let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
 
   Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, ⌜v = #13⌝ }]%I.
   Proof.
     rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
-    wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
+    wp_op. wp_load. wp_faa. do 2 wp_load. wp_op. done.
   Qed.
 
   Definition heap_e6 : val := λ: "v", "v" = "v".

theories/heap_lang/lang.v

@@ -271,14 +271,14 @@ Canonical Structure exprC := leibnizC expr.
 
 (** Evaluation contexts *)
 Inductive ectx_item :=
-  | AppLCtx (e2 : expr)
-  | AppRCtx (v1 : val)
+  | AppLCtx (v2 : val)
+  | AppRCtx (e1 : expr)
   | UnOpCtx (op : un_op)
-  | BinOpLCtx (op : bin_op) (e2 : expr)
-  | BinOpRCtx (op : bin_op) (v1 : val)
+  | BinOpLCtx (op : bin_op) (v2 : val)
+  | BinOpRCtx (op : bin_op) (e1 : expr)
   | IfCtx (e1 e2 : expr)
-  | PairLCtx (e2 : expr)
-  | PairRCtx (v1 : val)
+  | PairLCtx (v2 : val)
+  | PairRCtx (e1 : expr)
   | FstCtx
   | SndCtx
   | InjLCtx
@@ -286,24 +286,24 @@ Inductive ectx_item :=
   | CaseCtx (e1 : expr) (e2 : expr)
   | AllocCtx
   | LoadCtx
-  | StoreLCtx (e2 : expr)
-  | StoreRCtx (v1 : val)
-  | CasLCtx (e1 : expr) (e2 : expr)
-  | CasMCtx (v0 : val) (e2 : expr)
-  | CasRCtx (v0 : val) (v1 : val)
-  | FaaLCtx (e2 : expr)
-  | FaaRCtx (v1 : val).
+  | StoreLCtx (v2 : val)
+  | StoreRCtx (e1 : expr)
+  | CasLCtx (v1 : val) (v2 : val)
+  | CasMCtx (e0 : expr) (v2 : val)
+  | CasRCtx (e0 : expr) (e1 : expr)
+  | FaaLCtx (v2 : val)
+  | FaaRCtx (e1 : expr).
 
 Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
-  | AppLCtx e2 => App e e2
-  | AppRCtx v1 => App (of_val v1) e
+  | AppLCtx v2 => App e (of_val v2)
+  | AppRCtx e1 => App e1 e
   | UnOpCtx op => UnOp op e
-  | BinOpLCtx op e2 => BinOp op e e2
-  | BinOpRCtx op v1 => BinOp op (of_val v1) e
+  | BinOpLCtx op v2 => BinOp op e (of_val v2)
+  | BinOpRCtx op e1 => BinOp op e1 e
   | IfCtx e1 e2 => If e e1 e2
-  | PairLCtx e2 => Pair e e2
-  | PairRCtx v1 => Pair (of_val v1) e
+  | PairLCtx v2 => Pair e (of_val v2)
+  | PairRCtx e1 => Pair e1 e
   | FstCtx => Fst e
   | SndCtx => Snd e
   | InjLCtx => InjL e
@@ -311,13 +311,13 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2
-  | StoreRCtx v1 => Store (of_val v1) e
-  | CasLCtx e1 e2 => CAS e e1 e2
-  | CasMCtx v0 e2 => CAS (of_val v0) e e2
-  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
-  | FaaLCtx e2 => FAA e e2
-  | FaaRCtx v1 => FAA (of_val v1) e
+  | StoreLCtx v2 => Store e (of_val v2)
+  | StoreRCtx e1 => Store e1 e
+  | CasLCtx v1 v2 => CAS e (of_val v1) (of_val v2)
+  | CasMCtx e0 v2 => CAS e0 e (of_val v2)
+  | CasRCtx e0 e1 => CAS e0 e1 e
+  | FaaLCtx v2 => FAA e (of_val v2)
+  | FaaRCtx e1 => FAA e1 e
   end.
 
 (** Substitution *)

theories/heap_lang/lib/atomic_heap.v

@@ -27,7 +27,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
     <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    <<< ∀ v, mapsto l 1 v >>> store (#l, e) @ ⊤
+    <<< ∀ v, mapsto l 1 v >>> store #l e @ ⊤
     <<< mapsto l 1 w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
@@ -35,7 +35,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   spec is still good enough for all our applications. *)
   cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    <<< ∀ v, mapsto l 1 v >>> cas (#l, e1, e2) @ ⊤
+    <<< ∀ v, mapsto l 1 v >>> cas #l e1 e2 @ ⊤
     <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
         RET #(if decide (v = w1) then true else false) >>>;
 }.
@@ -53,9 +53,9 @@ Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 Notation "'ref' e" := (alloc e) : expr_scope.
 Notation "! e" := (load e) : expr_scope.
-Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
+Notation "e1 <- e2" := (store e1 e2) : expr_scope.
 
-Notation CAS e1 e2 e3 := (cas (e1, e2, e3)%E).
+Notation CAS e1 e2 e3 := (cas e1 e2 e3).
 
 End notation.
 
@@ -65,9 +65,9 @@ Definition primitive_alloc : val :=
 Definition primitive_load : val :=
   λ: "l", !"l".
 Definition primitive_store : val :=
-  λ: "p", (Fst "p") <- (Snd "p").
+  λ: "l" "x", "l" <- "x".
 Definition primitive_cas : val :=
-  λ: "p", CAS (Fst (Fst "p")) (Snd (Fst "p")) (Snd "p").
+  λ: "l" "e1" "e2", CAS "l" "e1" "e2".
 
 Section proof.
   Context `{!heapG Σ}.
@@ -89,10 +89,10 @@ Section proof.
 
   Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    <<< ∀ v, l ↦ v >>> primitive_store (#l, e) @ ⊤
+    <<< ∀ v, l ↦ v >>> primitive_store #l e @ ⊤
     <<< l ↦ w, RET #() >>>.
   Proof.
-    iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj.
+    iIntros (<- Q Φ) "? AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
@@ -100,11 +100,11 @@ Section proof.
   Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
     <<< ∀ (v : val), l ↦ v >>>
-      primitive_cas (#l, e1, e2) @ ⊤
+      primitive_cas #l e1 e2 @ ⊤
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET #(if decide (v = w1) then true else false) >>>.
   Proof.
-    iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
+    iIntros (<- <- ? Q Φ) "? AU". wp_lam. wp_let. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".

theories/heap_lang/lib/ticket_lock.v

@@ -74,7 +74,7 @@ Section proof.
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
-    wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
+    wp_seq. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
@@ -111,7 +111,7 @@ Section proof.
     iInv N as (o n) "[Hlo [Hln Ha]]".
     wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
-    wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
+    wp_let. wp_op. wp_proj. wp_bind (CAS _ _ _).
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - iMod (own_update with "Hauth") as "[Hauth Hofull]".
@@ -137,14 +137,14 @@ Section proof.
   Proof.
     iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iDestruct "Hγ" as (o) "Hγo".
-    wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
+    wp_let. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
     iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
-    wp_op.
+    wp_op. wp_proj.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
     iApply wp_fupd. wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as

theories/heap_lang/tactics.v

@@ -269,15 +269,15 @@ Ltac reshape_expr e tac :=
   let rec go K e :=
   match e with
   | _ => tac K e
-  | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
-  | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
+  | App ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (AppLCtx v2 :: K) e1)
+  | App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
   | UnOp ?op ?e => go (UnOpCtx op :: K) e
   | BinOp ?op ?e1 ?e2 =>
-     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
-  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
+     reshape_val e2 ltac:(fun v2 => go (BinOpLCtx op v2 :: K) e1)
+  | BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
   | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
-  | Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
-  | Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
+  | Pair ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (PairLCtx v2 :: K) e1)
+  | Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
   | Fst ?e => go (FstCtx :: K) e
   | Snd ?e => go (SndCtx :: K) e
   | InjL ?e => go (InjLCtx :: K) e
@@ -285,12 +285,12 @@ Ltac reshape_expr e tac :=
   | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
   | Alloc ?e => go (AllocCtx :: K) e
   | Load ?e => go (LoadCtx :: K) e
-  | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
-  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
-  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
-     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
-     | go (CasMCtx v0 e2 :: K) e1 ])
-  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
-  | FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2)
-  | FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1
+  | Store ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (StoreLCtx v2 :: K) e1)
+  | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
+  | CAS ?e0 ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => first
+     [ reshape_val e1 ltac:(fun v1 => go (CasLCtx v1 v2 :: K) e0)
+     | go (CasMCtx e0 v2 :: K) e1 ])
+  | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
+  | FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
+  | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
   end in go (@nil ectx_item) e.