Commit 55cd1cc9 authored by Ralf Jung's avatar Ralf Jung
Browse files

more consistent names for some class projections

parent e252ca6e
......@@ -219,7 +219,7 @@ Qed.
(** This simpler form of adequacy requires the [irisGS] instance that you use
everywhere to syntactically be of the form
{|
iris_invG := ...;
iris_invGS := ...;
state_interp σ _ κs _ := ...;
fork_post v := ...;
num_laters_per_step _ := 0;
......
......@@ -21,13 +21,13 @@ Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
}.
Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
iris_invG := ownP_invG;
iris_invGS := ownP_invG;
state_interp σ _ κs _ := own ownP_name (E σ)%I;
fork_post _ := True%I;
num_laters_per_step _ := 0;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
Global Opaque iris_invG.
Global Opaque iris_invGS.
Definition ownPΣ (Λ : language) : gFunctors :=
#[invΣ;
......
......@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
Import uPred.
Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
iris_invG :> invGS Σ;
iris_invGS :> invGS Σ;
(** The state interpretation is an invariant that should hold in
between each step of reduction. Here [Λstate] is the global state,
......@@ -45,7 +45,7 @@ Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
state_interp_mono σ ns κs nt:
state_interp σ ns κs nt ={}= state_interp σ (S ns) κs nt
}.
Global Opaque iris_invG.
Global Opaque iris_invGS.
Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
(wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
......
......@@ -11,14 +11,14 @@ From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
Class heapGS Σ := HeapGS {
heapG_invG : invGS Σ;
heapG_gen_heapG :> gen_heapGS loc (option val) Σ;
heapG_inv_heapG :> inv_heapGS loc (option val) Σ;
heapG_proph_mapG :> proph_mapGS proph_id (val * val) Σ;
heapGS_invGS : invGS Σ;
heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
}.
Global Instance heapG_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
iris_invG := heapG_invG;
Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
iris_invGS := heapGS_invGS;
state_interp σ _ κs _ :=
(gen_heap_interp σ.(heap) proph_map_interp κs σ.(used_proph_id))%I;
fork_post _ := True%I;
......
Markdown is supported
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