break dependency of bi.weakestpre on program_logic.language

iris/bi/weakestpre.v

+(** 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

iris/program_logic/language.v

 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 Λ.

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).

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).