From 43769f553c0f43f01a850840a4005dd02da4f8e1 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Fri, 13 May 2016 13:36:30 +0200
Subject: [PATCH] =?UTF-8?q?Remove=20the=20specification=20rules=20in=20F?=
 =?UTF-8?q?=CE=BC,ref,par?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These will be put in a separate file.
---
 F_mu_ref_par/rules.v | 60 ++++++++------------------------------------
 1 file changed, 11 insertions(+), 49 deletions(-)

diff --git a/F_mu_ref_par/rules.v b/F_mu_ref_par/rules.v
index 0039632..eccc311 100644
--- a/F_mu_ref_par/rules.v
+++ b/F_mu_ref_par/rules.v
@@ -2,7 +2,7 @@ Require Import iris.program_logic.lifting.
 Require Import iris.algebra.upred_big_op.
 Require Import F_mu_ref_par.lang.
 From iris.program_logic Require Export lifting.
-From iris.algebra Require Import upred_big_op frac dec_agree.
+From iris.algebra Require Import upred_big_op frac dec_agree list.
 From iris.program_logic Require Export invariants ghost_ownership.
 From iris.program_logic Require Import ownership auth.
 From iris.proofmode Require Import weakestpre.
@@ -12,7 +12,8 @@ Import uPred.
 Section lang_rules.
   Definition heapR : cmraT := gmapR loc (fracR (dec_agreeR val)).
 
-  (** The CMRA for the heap of the implementation. This is linked to the physical heap. *)
+  (** The CMRA for the heap of the implementation. This is linked to the
+      physical heap. *)
   Class heapIG Σ :=
     HeapIG {
         heapI_inG :> authG lang Σ heapR;
@@ -23,22 +24,6 @@ Section lang_rules.
   Definition of_heap : heapR → state :=
     omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
 
-  (** The CMRA for the heap of the specification. *)
-  Class heapSG Σ :=
-    HeapSG {
-        heapS_inG :> authG lang Σ heapR;
-        heapS_name : gname
-      }.
-
-  Definition tpoolR : cmraT := gmapR loc (fracR (dec_agreeR expr)).
-
-  (** The CMRA for the thread pool. *)
-  Class tpoolG Σ :=
-    TpoolSG {
-        tpool_inG :> authG lang Σ tpoolR;
-        tpool_name : gname
-      }.
-
   Section definitionsI.
     Context `{iI : heapIG Σ}.
 
@@ -60,31 +45,6 @@ Section lang_rules.
     (at level 20, q at level 50, format "l  ↦ᵢ{ q }  v") : uPred_scope.
   Notation "l ↦ᵢ v" := (heapI_mapsto l 1 v) (at level 20) : uPred_scope.
 
-  Section definitionsS.
-    Context `{iS : heapSG Σ}
-            `{iT : tpoolG Σ}.
-
-    Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iPropG lang Σ :=
-      auth_own heapS_name {[ l := Frac q (DecAgree v) ]}.
-
-    Definition tpool_mapsto (l : loc) (q : Qp) (e: expr) : iPropG lang Σ :=
-      auth_own tpool_name {[ l := Frac q (DecAgree e) ]}.
-
-    Definition Spec_ctx (S : namespace) : iPropG lang Σ :=
-      inv S (∃ h, ∃ T, (ghost_ownership.own heapS_name(● h))
-                                         ★ (ghost_ownership.own tpool_name (● T)))%I.
-  End definitionsS.
-  Typeclasses Opaque heapS_mapsto tpool_mapsto.
-
-  Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
-    (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : uPred_scope.
-  Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope.
-
-  Notation "j ⤇{ q } e" :=
-    (tpool_mapsto j q e)
-      (at level 20, q at level 50, format "j  ⤇{ q }  e") : uPred_scope.
-  Notation "j ⤇ e" := (tpool_mapsto j 1 e) (at level 20) : uPred_scope.
-
   Section heap.
     Context {Σ : gFunctors}.
     Implicit Types N : namespace.
@@ -93,9 +53,9 @@ Section lang_rules.
     Implicit Types σ : state.
     Implicit Types h g : heapR.
 
-
     Lemma wp_bind {E e} K Φ :
-      WP e @ E {{ (λ v, WP (fill K (of_val v)) @ E {{Φ}}) }} ⊢ WP (fill K e) @ E {{Φ}}.
+      WP e @ E {{ (λ v, WP (fill K (of_val v)) @ E {{Φ}}) }}
+         ⊢ WP (fill K e) @ E {{Φ}}.
     Proof. apply weakestpre.wp_bind. Qed.
 
     Lemma wp_bindi {E e} Ki Φ :
@@ -118,8 +78,8 @@ Section lang_rules.
           apply val_head_stuck, (fill_not_val K) in H;
             by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
         | H : head_step ?e _ _ _ _ |- _ =>
-          try (is_var e; fail 1); (* inversion yields many goals if e is a variable
-     and can thus better be avoided. *)
+          try (is_var e; fail 1); (* inversion yields many goals if e is a
+                                     variable and can thus better be avoided. *)
             inversion H; subst; clear H
         end.
 
@@ -128,7 +88,8 @@ Section lang_rules.
           match e with
           | of_val ?v => v
           | Pair ?e1 ?e2 =>
-            let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
+            let v1 := reshape_val e1 in
+            let v2 := reshape_val e2 in constr:(PairV v1 v2)
           | InjL ?e => let v := reshape_val e in constr:(InjLV v)
           | InjR ?e => let v := reshape_val e in constr:(InjRV v)
           | Loc ?l => constr:(LocV l)
@@ -149,7 +110,8 @@ Section lang_rules.
           | 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 => 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:
-- 
GitLab