Commit e578423a authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (C→O rename + lazy_tc).

parent 8aacd098
Pipeline #18891 failed with stage
in 11 minutes and 36 seconds
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") } "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
] ]
...@@ -35,14 +35,14 @@ Section ofe. ...@@ -35,14 +35,14 @@ Section ofe.
Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP). Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP).
Proof. Proof.
refine (iso_ofe_mixin (λ P : fracPred PROP, P : _ -c> _) _ _); refine (iso_ofe_mixin (λ P : fracPred PROP, P : _ -d> _) _ _);
(split; [by destruct 1|by constructor]). (split; [by destruct 1|by constructor]).
Qed. Qed.
Canonical Structure fracPredC : ofeT := OfeT (fracPred PROP) fracPred_ofe_mixin. Canonical Structure fracPredO : ofeT := OfeT (fracPred PROP) fracPred_ofe_mixin.
Global Instance fracPred_cofe `{Cofe PROP} : Cofe fracPredC. Global Instance fracPred_cofe `{Cofe PROP} : Cofe fracPredO.
Proof. Proof.
refine (iso_cofe (λ P : _ -c> _, @FracPred PROP P) id _ _). refine (iso_cofe (λ P : _ -d> _, @FracPred PROP P) id _ _).
- split; [by destruct 1|by constructor]. - split; [by destruct 1|by constructor].
- done. - done.
Qed. Qed.
...@@ -504,7 +504,7 @@ Section sbi_facts. ...@@ -504,7 +504,7 @@ Section sbi_facts.
- apply bi.forall_intro=>?. apply (bi.f_equiv (flip fracPred_at _)). - apply bi.forall_intro=>?. apply (bi.f_equiv (flip fracPred_at _)).
- rewrite {2}(_ : P = FracPred P); last by destruct P. - rewrite {2}(_ : P = FracPred P); last by destruct P.
rewrite {2}(_ : Q = FracPred Q); last by destruct Q. rewrite {2}(_ : Q = FracPred Q); last by destruct Q.
by rewrite -(@bi.f_equiv _ _ _ (@FracPred PROP : (_ -c> _) fracPred) by rewrite -(@bi.f_equiv _ _ _ (@FracPred PROP : (_ -d> _) fracPred)
ltac:(by constructor)) -bi.fun_ext. ltac:(by constructor)) -bi.fun_ext.
Qed. Qed.
......
...@@ -13,13 +13,13 @@ Set Default Proof Using "Type". ...@@ -13,13 +13,13 @@ Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG { Class heapPreG Σ := HeapPreG {
heap_preG_iris :> ironInvPreG Σ; heap_preG_iris :> ironInvPreG Σ;
heap_preG_inG :> inG Σ (ufrac_authR heapUR); heap_preG_inG :> inG Σ (ufrac_authR heapUR);
heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC)))); heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionO ufracO))));
}. }.
Definition heapΣ : gFunctors := #[ Definition heapΣ : gFunctors := #[
ironInvΣ; ironInvΣ;
GFunctor (ufrac_authR heapUR); GFunctor (ufrac_authR heapUR);
GFunctor (authR (gmapUR positive (exclR (optionC ufracC))))]. GFunctor (authR (gmapUR positive (exclR (optionO ufracO))))].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ. Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
......
...@@ -10,7 +10,7 @@ From iron.heap_lang Require Export lang. ...@@ -10,7 +10,7 @@ From iron.heap_lang Require Export lang.
From iron.iron_logic Require Export weakestpre. From iron.iron_logic Require Export weakestpre.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valC)). Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valO)).
Definition to_heap : gmap loc val heapUR := Definition to_heap : gmap loc val heapUR :=
fmap (λ v, (1%Qp, to_agree v)). fmap (λ v, (1%Qp, to_agree v)).
...@@ -22,7 +22,7 @@ Class heapG Σ := HeapG { ...@@ -22,7 +22,7 @@ Class heapG Σ := HeapG {
heapG_fcinv_cinvG : cinvG Σ; heapG_fcinv_cinvG : cinvG Σ;
heapG_fcinv_inG : inG Σ (frac_authR ufracR); heapG_fcinv_inG : inG Σ (frac_authR ufracR);
heapG_fork_post_name : gname; heapG_fork_post_name : gname;
heapG_fork_postG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC)))); heapG_fork_postG :> inG Σ (authR (gmapUR positive (exclR (optionO ufracO))));
}. }.
Arguments heapG_name {_} _ : assert. Arguments heapG_name {_} _ : assert.
Arguments heapG_fork_post_name {_} _ : assert. Arguments heapG_fork_post_name {_} _ : assert.
...@@ -98,7 +98,7 @@ Section to_heap. ...@@ -98,7 +98,7 @@ Section to_heap.
Lemma to_heap_empty : to_heap = . Lemma to_heap_empty : to_heap = .
Proof. by rewrite /to_heap fmap_empty. Qed. Proof. by rewrite /to_heap fmap_empty. Qed.
Lemma to_heap_insert l v σ : Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC val))]> (to_heap σ). to_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO val))]> (to_heap σ).
Proof. by rewrite /to_heap fmap_insert. Qed. Proof. by rewrite /to_heap fmap_insert. Qed.
Lemma to_heap_delete l σ : Lemma to_heap_delete l σ :
to_heap (delete l σ) = delete l (to_heap σ). to_heap (delete l σ) = delete l (to_heap σ).
...@@ -296,7 +296,7 @@ Section heap. ...@@ -296,7 +296,7 @@ Section heap.
iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hp". iDestruct 1 as (πfs Hsize) "[Hπfs Hσ]"; iIntros "Hp".
iMod (own_update_2 with "Hσ Hp") as "[Hσ Hl]". iMod (own_update_2 with "Hσ Hp") as "[Hσ Hl]".
{ eapply ufrac_auth_update, { eapply ufrac_auth_update,
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _))) => //. (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizO _))) => //.
by apply lookup_to_heap_None. } by apply lookup_to_heap_None. }
iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame. iModIntro. iFrame "Hl". iExists πfs. rewrite to_heap_insert. by iFrame.
Qed. Qed.
......
...@@ -16,7 +16,7 @@ Open Scope Z_scope. ...@@ -16,7 +16,7 @@ Open Scope Z_scope.
(** Expressions and vals. *) (** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *) Definition loc := positive. (* Really, any countable type. *)
Canonical Structure locC := leibnizC loc. (* Really, any countable type. *) Canonical Structure locO := leibnizO loc. (* Really, any countable type. *)
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc). | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
...@@ -218,12 +218,12 @@ Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed. ...@@ -218,12 +218,12 @@ Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit). Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit). Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Canonical Structure valC := leibnizC val. Canonical Structure valO := leibnizO val.
Canonical Structure exprC := leibnizC expr. Canonical Structure exprO := leibnizO expr.
(** The state: heaps of vals. *) (** The state: heaps of vals. *)
Definition state := gmap loc val. Definition state := gmap loc val.
Canonical Structure stateC := leibnizC state. Canonical Structure stateO := leibnizO state.
(** Evaluation contexts *) (** Evaluation contexts *)
Inductive ectx_item := Inductive ectx_item :=
......
...@@ -45,7 +45,7 @@ Section spec. ...@@ -45,7 +45,7 @@ Section spec.
Context `{!heapG Σ, !lockG Σ, !cinvG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ, !cinvG Σ} (N : namespace).
Local Notation iProp := (iProp Σ). Local Notation iProp := (iProp Σ).
Definition isBag_pre (Ψ : val iProp) (Φ : Qp -c> loc -c> iProp): Qp -c> loc -c> iProp := λ π , Definition isBag_pre (Ψ : val iProp) (Φ : Qp -d> loc -d> iProp): Qp -d> loc -d> iProp := λ π ,
( [π] NONEV ( [π] NONEV
x (' : loc) (πℓ πb : Qp), (πℓ + πb = π)%Qp [πℓ] SOMEV (x, #') Ψ x (Φ πb%Qp '))%I. x (' : loc) (πℓ πb : Qp), (πℓ + πb = π)%Qp [πℓ] SOMEV (x, #') Ψ x (Φ πb%Qp '))%I.
......
...@@ -48,7 +48,7 @@ Definition receive : val := λ: "p", ...@@ -48,7 +48,7 @@ Definition receive : val := λ: "p",
Definition close : val := λ: "p", Definition close : val := λ: "p",
let: "flag" := Snd "p" in "flag" <- #false. let: "flag" := Snd "p" in "flag" <- #false.
Definition binary_choiceR := csumR (exclR unitC) (agreeR boolC). Definition binary_choiceR := csumR (exclR unitO) (agreeR boolO).
Definition no_choice : binary_choiceR := Cinl (Excl ()). Definition no_choice : binary_choiceR := Cinl (Excl ()).
Definition chose (n : bool) : binary_choiceR := Cinr (to_agree n). Definition chose (n : bool) : binary_choiceR := Cinr (to_agree n).
......
...@@ -62,9 +62,9 @@ Definition delete_all : val := ...@@ -62,9 +62,9 @@ Definition delete_all : val :=
end. end.
Class queueG Σ := { Class queueG Σ := {
queueG_inG :> inG Σ (prodR fracR (agreeR (listC valC))); queueG_inG :> inG Σ (prodR fracR (agreeR (listO valO)));
queueG_dequeue_inG :> inG Σ (exclR unitC); queueG_dequeue_inG :> inG Σ (exclR unitO);
queueG_enqueue_inG :> inG Σ (authR (optionUR (exclR locC))) queueG_enqueue_inG :> inG Σ (authR (optionUR (exclR locO)))
}. }.
Record queue_name := QueueName { Record queue_name := QueueName {
...@@ -75,7 +75,7 @@ Record queue_name := QueueName { ...@@ -75,7 +75,7 @@ Record queue_name := QueueName {
}. }.
(* (*
Definition queueΣ : gFunctors := #[GFunctor queueCmra; GFunctor fracR; GFunctor (exclR unitC); fcinvΣ]. Definition queueΣ : gFunctors := #[GFunctor queueCmra; GFunctor fracR; GFunctor (exclR unitO); fcinvΣ].
Instance subG_queueΣ {Σ} : subG queueΣ Σ → queueG Σ. Instance subG_queueΣ {Σ} : subG queueΣ Σ → queueG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
......
...@@ -10,12 +10,12 @@ From iris.algebra Require Import excl. ...@@ -10,12 +10,12 @@ From iris.algebra Require Import excl.
Record transfer_name := { transfer_name : gname; transfer_name : gname; }. Record transfer_name := { transfer_name : gname; transfer_name : gname; }.
Class transferG Σ := TransferG { Class transferG Σ := TransferG {
transfer_tokG : inG Σ (exclR unitC); transfer_tokG : inG Σ (exclR unitO);
transfer_fracG : inG Σ fracR transfer_fracG : inG Σ fracR
}. }.
Local Existing Instances transfer_tokG transfer_fracG. Local Existing Instances transfer_tokG transfer_fracG.
Definition transferΣ : gFunctors := Definition transferΣ : gFunctors :=
#[GFunctor (exclR unitC); GFunctor fracR]. #[GFunctor (exclR unitO); GFunctor fracR].
Instance subG_transferΣ {Σ} : subG transferΣ Σ transferG Σ. Instance subG_transferΣ {Σ} : subG transferΣ Σ transferG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
......
...@@ -22,8 +22,8 @@ Definition free : val := ...@@ -22,8 +22,8 @@ Definition free : val :=
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }. Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)]. Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ. Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
......
...@@ -26,8 +26,8 @@ Definition free : val := ...@@ -26,8 +26,8 @@ Definition free : val :=
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (authR (optionUR (exclR fracC))) }. Class lockG Σ := LockG { lock_tokG :> inG Σ (authR (optionUR (exclR fracO))) }.
Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracC))) ]. Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracO))) ].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ. Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
......
...@@ -212,7 +212,7 @@ Tactic Notation "wp_apply" open_constr(lem) := ...@@ -212,7 +212,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch iTypeOf H with lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P | Some (_,?P) => fail "wp_apply: cannot apply" P
end in end in
iPoseProofCore lem as false true (fun H => iPoseProofCore lem as false (fun H =>
lazymatch goal with lazymatch goal with
| |- envs_entails_wp ?e => | |- envs_entails_wp ?e =>
reshape_expr e ltac:(fun K e' => reshape_expr e ltac:(fun K e' =>
......
...@@ -42,7 +42,7 @@ Class ironInvG (Σ : gFunctors) := IronInvG { ...@@ -42,7 +42,7 @@ Class ironInvG (Σ : gFunctors) := IronInvG {
fcinv_inG :> inG Σ (frac_authR ufracR); fcinv_inG :> inG Σ (frac_authR ufracR);
}. }.
Notation ironProp Σ := (fracPred (iProp Σ)). Notation ironProp Σ := (fracPred (iProp Σ)).
Notation ironPropC Σ := (fracPredC (iProp Σ)). Notation ironPropC Σ := (fracPredO (iProp Σ)).
Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))). Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))).
Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))). Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))).
......
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