From 21ab62fdc0266fa4144b4a2e1d130dbea88dd718 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Mar 2021 13:59:02 +0100
Subject: [PATCH] break dependency of bi.weakestpre on program_logic.language

---
 iris/bi/weakestpre.v                  | 30 +++++++++++++++------------
 iris/program_logic/language.v         |  9 ++++----
 iris/program_logic/total_weakestpre.v |  2 +-
 iris/program_logic/weakestpre.v       |  2 +-
 4 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index 3bcc9cfe9..b2c248e6b 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -1,8 +1,15 @@
+(** Shared notation file for WP connectives. *)
+
 From stdpp Require Export coPset.
 From iris.bi Require Import interface derived_connectives.
-From iris.program_logic Require Import language.
 From iris.prelude Require Import options.
 
+Declare Scope expr_scope.
+Delimit Scope expr_scope with E.
+
+Declare Scope val_scope.
+Delimit Scope val_scope with V.
+
 Inductive stuckness := NotStuck | MaybeStuck.
 
 Definition stuckness_leb (s1 s2 : stuckness) : bool :=
@@ -14,9 +21,6 @@ Global Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
 Global Instance stuckness_le_po : PreOrder stuckness_le.
 Proof. split; by repeat intros []. Qed.
 
-Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
-  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
-
 (** Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
 of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
 class. This argument can be used for e.g. the stuckness bit (as in Iris) or
@@ -28,15 +32,15 @@ and [s] to be [NotStuck] or [MaybeStuck].  This will fail to typecheck if [A] is
 not [stuckness].  If we ever want to use the notation [WP e @ E {{ Φ }}] with a
 different [A], the plan is to generalize the notation to use [Inhabited] instead
 to pick a default value depending on [A]. *)
-Class Wp (Λ : language) (PROP A : Type) :=
-  wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Global Arguments wp {_ _ _ _} _ _ _%E _%I.
-Global Instance: Params (@wp) 7 := {}.
-
-Class Twp (Λ : language) (PROP A : Type) :=
-  twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Global Arguments twp {_ _ _ _} _ _ _%E _%I.
-Global Instance: Params (@twp) 7 := {}.
+Class Wp (PROP EXPR VAL A : Type) :=
+  wp : A → coPset → EXPR → (VAL → PROP) → PROP.
+Global Arguments wp {_ _ _ _ _} _ _ _%E _%I.
+Global Instance: Params (@wp) 8 := {}.
+
+Class Twp (PROP EXPR VAL A : Type) :=
+  twp : A → coPset → EXPR → (VAL → PROP) → PROP.
+Global Arguments twp {_ _ _ _ _} _ _ _%E _%I.
+Global Instance: Params (@twp) 8 := {}.
 
 (** Notations for partial weakest preconditions *)
 (** Notations without binder -- only parsing because they overlap with the
diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 547c9c53a..bcce4c75f 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export ofe.
+From iris.bi Require Export weakestpre.
 From iris.prelude Require Import options.
 
 Section language_mixin.
@@ -28,12 +29,7 @@ Structure language := Language {
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 
-Declare Scope expr_scope.
-Delimit Scope expr_scope with E.
 Bind Scope expr_scope with expr.
-
-Declare Scope val_scope.
-Delimit Scope val_scope with V.
 Bind Scope val_scope with val.
 
 Global Arguments Language {_ _ _ _ _ _ _} _.
@@ -63,6 +59,9 @@ Proof. constructor; naive_solver. Qed.
 
 Inductive atomicity := StronglyAtomic | WeaklyAtomic.
 
+Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 7ef86fa5b..ad4f754bf 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -57,7 +57,7 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{!irisGS Λ Σ} : Twp Λ (iProp Σ) stuckness
+Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index bb54d9962..72064fadc 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -73,7 +73,7 @@ Proof.
   - by rewrite -IH.
 Qed.
 
-Definition wp_def `{!irisGS Λ Σ} : Wp Λ (iProp Σ) stuckness :=
+Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
-- 
GitLab