Commit 6828183c authored by Ralf Jung's avatar Ralf Jung
Browse files

experiment: don't tie bi.weakestpre to program_logic.language

parent d55f8339
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.
(** We define a canonical structure tying together the two types that are
relevant for us: expressions and values. This helps [Wp] typeclass inference.
*)
Structure pre_language := PreLanguage {
expr : Type;
val : Type;
}.
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.
(** We have some specialized notaton related to stuckness, so we need to define
that type here. *)
Inductive stuckness := NotStuck | MaybeStuck.
Definition stuckness_leb (s1 s2 : stuckness) : bool :=
......@@ -14,9 +31,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,12 +42,12 @@ 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) :=
Class Wp (Λ : pre_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) :=
Class Twp (Λ : pre_language) (PROP A : Type) :=
twp : A coPset expr Λ (val Λ PROP) PROP.
Global Arguments twp {_ _ _ _} _ _ _%E _%I.
Global Instance: Params (@twp) 7 := {}.
......
......@@ -116,6 +116,8 @@ Proof.
Qed.
End adequacy.
Implicit Types Λ : language.
(** Iris's generic adequacy result *)
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
(num_laters_per_step : nat nat) :
......
......@@ -141,7 +141,9 @@ Section ectx_language.
apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
Qed.
Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
Canonical Structure ectx_lang : language :=
Language (pre:=PreLanguage (expr Λ) (val Λ)) ectx_lang_mixin.
Canonical Structure ectxi_pre_lang := PreOfLanguage ectx_lang.
Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
σ κ e' σ' efs,
......@@ -322,5 +324,5 @@ Note that this trick no longer works when we switch to canonical projections
because then the pattern match [let '...] will be desugared into projections. *)
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
@Language E V St K of_val to_val _
@Language (PreLanguage E V) St K of_val to_val _
(@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
......@@ -139,6 +139,7 @@ Section ectxi_language.
Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.
Canonical Structure ectxi_pre_lang := PreOfLanguage ectxi_lang.
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
......
From iris.algebra Require Export ofe.
From iris.bi Require Export weakestpre.
From iris.prelude Require Import options.
(** TAKE CARE: When you define a [language] canonical structure for your
language, you need to also define a corresponding [pre_language] canonical
structure. Use the coercion [PreOfLanguage] as defined in the bottom of this
file for doing that. *)
Section language_mixin.
Context {expr val state observation : Type}.
Context (of_val : val expr).
......@@ -18,32 +24,23 @@ Section language_mixin.
End language_mixin.
Structure language := Language {
expr : Type;
val : Type;
pre :> pre_language; (* Avoid having two [val] and [expr] projections. *)
state : Type;
observation : Type;
of_val : val expr;
to_val : expr option val;
prim_step : expr state list observation expr state list expr Prop;
of_val : val pre expr pre;
to_val : expr pre option (val pre);
prim_step : expr pre state list observation expr pre state list (expr pre) Prop;
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 {_ _ _ _ _ _ _} _.
Global Arguments Language {_ _ _ _ _ _} _.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments prim_step {_} _ _ _ _ _ _.
Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
Canonical Structure exprO Λ := leibnizO (expr Λ).
Canonical Structure stateO (Λ : language) := leibnizO (state Λ).
Canonical Structure valO (Λ : language) := leibnizO (val Λ).
Canonical Structure exprO (Λ : language) := leibnizO (expr Λ).
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
......@@ -58,11 +55,14 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
e2', e2 = K e2' prim_step e1' σ1 κ e2' σ2 efs
}.
Global Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Global Instance language_ctx_id (Λ : language) : LanguageCtx (@id (expr Λ)).
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 Λ.
......@@ -331,3 +331,14 @@ End language.
Global Arguments step_atomic {Λ ρ1 κ ρ2}.
Notation pure_steps_tp := (Forall2 (rtc pure_step)).
(* This definition makes sure that the fields of the [pre_language] record do not
refer to the projections of the [language] record but to the actual fields
of the [language] record. This is crucial for canonical structure search to
work.
Note that this trick no longer works when we switch to canonical projections
because then the pattern match [let '...] will be desugared into projections. *)
Definition PreOfLanguage (Λ : language) : pre_language :=
let '@Language (PreLanguage E V) St K of_val to_val prim mix := Λ in
PreLanguage E V.
......@@ -748,6 +748,7 @@ End heap_lang.
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
Canonical Structure heap_pre_lang := PreOfLanguage heap_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
......
......@@ -32,7 +32,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
......@@ -43,7 +43,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
......@@ -64,7 +64,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
......@@ -75,7 +75,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
......@@ -95,7 +95,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
......@@ -106,7 +106,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
......@@ -127,7 +127,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
......@@ -138,7 +138,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
......@@ -162,7 +162,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
......@@ -183,7 +183,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
......@@ -205,7 +205,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
......@@ -228,7 +228,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Φ #() >>
......@@ -251,7 +251,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
......@@ -274,7 +274,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Φ #() >>
......@@ -297,7 +297,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
......@@ -321,7 +321,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
......@@ -336,7 +336,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
Φ : weakestpre.val heap_ectx_lang → iProp Σ
============================
"AU" : ∃ x : val,
P x
......
......@@ -292,7 +292,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
Σ : gFunctors
heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
Φ : weakestpre.val heap_pre_lang → iPropI Σ
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
......@@ -305,7 +305,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
Σ : gFunctors
heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
Φ : weakestpre.val heap_pre_lang → iPropI Σ
E : coPset
============================
--------------------------------------∗
......
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