Commit 59d18188 authored by Ralf Jung's avatar Ralf Jung
Browse files

break dependency of bi.weakestpre on program_logic.language

parent e14e1fed
(** 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
......
From iris.algebra Require Export ofe.
From iris.bi Require Import 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 Λ.
......
......@@ -57,7 +57,7 @@ Proof.
rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
Qed.
Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
Definition twp_def `{!irisG Λ Σ} : 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).
......
......@@ -73,7 +73,7 @@ Proof.
- by rewrite -IH.
Qed.
Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
Definition wp_def `{!irisG Λ Σ} : 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).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment