Commit 2d9c59ac authored by Ralf Jung's avatar Ralf Jung

Revert accidentally pushed "WIP: move the later from the resources to the model"

This reverts commit 5161e463.
parent 36289cf3
...@@ -2,14 +2,14 @@ Require Export modures.logic iris.resources. ...@@ -2,14 +2,14 @@ Require Export modures.logic iris.resources.
Require Import modures.cofe_solver. Require Import modures.cofe_solver.
Module iProp. Module iProp.
Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)). Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ A).
Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT} Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
(f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 := (f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
uPredC_map (resRA_map (laterC_map (f.1))). uPredC_map (resRA_map (f.1)).
Definition result Σ : solution (F Σ). Definition result Σ : solution (F Σ).
Proof. Proof.
apply (solver.result _ (@map Σ)). apply (solver.result _ (@map Σ)).
* intros A B r n ?; rewrite /uPred_holds /= /laterC_map /=. later_map_id res_map_id. * by intros A B r n ?; rewrite /uPred_holds /= res_map_id.
* by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?; * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?;
rewrite /= /uPred_holds /= res_map_compose. rewrite /= /uPred_holds /= res_map_compose.
* by intros A1 A2 B1 B2 n f f' [??] r; * by intros A1 A2 B1 B2 n f f' [??] r;
......
Require Export modures.fin_maps modures.agree modures.excl iris.parameter. Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
Record res (Σ : iParam) (A : cofeT) := Res { Record res (Σ : iParam) (A : cofeT) := Res {
wld : mapRA positive (agreeRA A); wld : mapRA positive (agreeRA (laterC A));
pst : exclRA (istateC Σ); pst : exclRA (istateC Σ);
gst : icmra Σ A; gst : icmra Σ (laterC A);
}. }.
Add Printing Constructor res. Add Printing Constructor res.
Arguments Res {_ _} _ _ _. Arguments Res {_ _} _ _ _.
...@@ -137,7 +137,7 @@ Canonical Structure resRA : cmraT := ...@@ -137,7 +137,7 @@ Canonical Structure resRA : cmraT :=
Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A := Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
Res (wld r) (Excl σ) (gst r). Res (wld r) (Excl σ) (gst r).
Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A := Definition update_gst (m : icmra Σ (laterC A)) (r : res Σ A) : res Σ A :=
Res (wld r) (pst r) m. Res (wld r) (pst r) m.
Lemma wld_validN n r : {n} r {n} (wld r). Lemma wld_validN n r : {n} r {n} (wld r).
...@@ -167,9 +167,9 @@ End res. ...@@ -167,9 +167,9 @@ End res.
Arguments resRA : clear implicits. Arguments resRA : clear implicits.
Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B := Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
Res (agree_map f <$> (wld r)) Res (agree_map (later_map f) <$> (wld r))
(pst r) (pst r)
(icmra_map Σ f (gst r)). (icmra_map Σ (laterC_map f) (gst r)).
Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) : Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) :
( n, Proper (dist n ==> dist n) f) ( n, Proper (dist n ==> dist n) f)
n, Proper (dist n ==> dist n) (@res_map Σ _ _ f). n, Proper (dist n ==> dist n) (@res_map Σ _ _ f).
...@@ -178,16 +178,20 @@ Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r. ...@@ -178,16 +178,20 @@ Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r.
Proof. Proof.
constructor; simpl; [|done|]. constructor; simpl; [|done|].
* rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=. * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=; done. rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
* rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=; done. by rewrite later_map_id.
* rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
by rewrite later_map_id.
Qed. Qed.
Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) : Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) :
res_map (g f) r res_map g (res_map f r). res_map (g f) r res_map g (res_map f r).
Proof. Proof.
constructor; simpl; [|done|]. constructor; simpl; [|done|].
* rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=. * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
rewrite -agree_map_compose; apply agree_map_ext=> y' /=; done. rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
* rewrite -icmra_map_compose; apply icmra_map_ext=> m /=; done. by rewrite later_map_compose.
* rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
by rewrite later_map_compose.
Qed. Qed.
Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B := Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
CofeMor (res_map f : resRA Σ A resRA Σ B). CofeMor (res_map f : resRA Σ A resRA Σ B).
...@@ -199,3 +203,10 @@ Proof. ...@@ -199,3 +203,10 @@ Proof.
intros (?&?&?); split_ands'; simpl; try apply includedN_preserving. intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
* by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving. * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed. Qed.
Instance resRA_map_contractive {Σ A B} : Contractive (@resRA_map Σ A B).
Proof.
intros n f g ? r; constructor; simpl; [|done|].
* by apply (mapRA_map_ne _ (agreeRA_map (laterC_map f))
(agreeRA_map (laterC_map g))), agreeRA_map_ne, laterC_map_contractive.
* by apply icmra_map_ne, laterC_map_contractive.
Qed.
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