Commit dbf38eb5 authored by Ralf Jung's avatar Ralf Jung

move functor def. to algebra/

parent 82511560
...@@ -47,6 +47,7 @@ algebra/dra.v ...@@ -47,6 +47,7 @@ algebra/dra.v
algebra/cofe_solver.v algebra/cofe_solver.v
algebra/agree.v algebra/agree.v
algebra/excl.v algebra/excl.v
algebra/functor.v
program_logic/upred.v program_logic/upred.v
program_logic/model.v program_logic/model.v
program_logic/adequacy.v program_logic/adequacy.v
...@@ -61,7 +62,6 @@ program_logic/pviewshifts.v ...@@ -61,7 +62,6 @@ program_logic/pviewshifts.v
program_logic/resources.v program_logic/resources.v
program_logic/hoare.v program_logic/hoare.v
program_logic/language.v program_logic/language.v
program_logic/functor.v
program_logic/tests.v program_logic/tests.v
heap_lang/heap_lang.v heap_lang/heap_lang.v
heap_lang/heap_lang_tactics.v heap_lang/heap_lang_tactics.v
......
Require Export algebra.cmra. Require Export algebra.cmra.
Require Import algebra.functor.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree { Record agree (A : Type) : Type := Agree {
...@@ -174,3 +175,8 @@ Proof. ...@@ -174,3 +175,8 @@ Proof.
intros f g Hfg x; split; simpl; intros; first done. intros f g Hfg x; split; simpl; intros; first done.
by apply dist_le with n; try apply Hfg. by apply dist_le with n; try apply Hfg.
Qed. Qed.
Program Definition agreeF : iFunctor :=
{| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
Solve Obligations with done.
Require Export algebra.excl. Require Export algebra.excl.
Require Import algebra.functor.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
...@@ -198,3 +199,19 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B := ...@@ -198,3 +199,19 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f). CofeMor (auth_map f).
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B). Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed. Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
Program Definition authF (Σ : iFunctor) : iFunctor := {|
ifunctor_car := authRA Σ; ifunctor_map A B := authC_map ifunctor_map Σ
|}.
Next Obligation.
by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros Σ A x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
intros Σ A B C f g x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply ifunctor_map_compose.
Qed.
Require Export algebra.cmra. Require Export algebra.cmra.
Require Import algebra.functor.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
...@@ -181,3 +182,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B := ...@@ -181,3 +182,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f). CofeMor (excl_map f).
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B). Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed. Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Program Definition exclF : iFunctor :=
{| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
Require Export algebra.cmra prelude.gmap algebra.option. Require Export algebra.cmra prelude.gmap algebra.option.
Require Import algebra.functor.
Section cofe. Section cofe.
Context `{Countable K} {A : cofeT}. Context `{Countable K} {A : cofeT}.
...@@ -246,3 +247,18 @@ Proof. ...@@ -246,3 +247,18 @@ Proof.
intros f g Hf m k; rewrite /= !lookup_fmap. intros f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf. destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed. Qed.
Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
ifunctor_car := mapRA K Σ; ifunctor_map A B := mapC_map ifunctor_map Σ
|}.
Next Obligation.
by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
Qed.
Next Obligation.
intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
Qed.
Require Export algebra.cmra. Require Export algebra.cmra.
Require Import algebra.agree algebra.excl algebra.auth.
Require Import algebra.option algebra.fin_maps.
(** * Functors from COFE to CMRA *) (** * Functors from COFE to CMRA *)
(* The Iris program logic is parametrized by a functor from the category of (* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
propositions using the agreement CMRA. *)
Structure iFunctor := IFunctor { Structure iFunctor := IFunctor {
ifunctor_car :> cofeT cmraT; ifunctor_car :> cofeT cmraT;
ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B; ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
...@@ -60,57 +55,3 @@ Next Obligation. ...@@ -60,57 +55,3 @@ Next Obligation.
intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose. intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
apply iprod_map_ext=> y; apply ifunctor_map_compose. apply iprod_map_ext=> y; apply ifunctor_map_compose.
Qed. Qed.
Program Definition agreeF : iFunctor :=
{| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
Solve Obligations with done.
Program Definition exclF : iFunctor :=
{| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
Program Definition authF (Σ : iFunctor) : iFunctor := {|
ifunctor_car := authRA Σ; ifunctor_map A B := authC_map ifunctor_map Σ
|}.
Next Obligation.
by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros Σ A x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
intros Σ A B C f g x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply ifunctor_map_compose.
Qed.
Program Definition optionF (Σ : iFunctor) : iFunctor := {|
ifunctor_car := optionRA Σ; ifunctor_map A B := optionC_map ifunctor_map Σ
|}.
Next Obligation.
by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros Σ A x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
intros Σ A B C f g x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
Qed.
Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
ifunctor_car := mapRA K Σ; ifunctor_map A B := mapC_map ifunctor_map Σ
|}.
Next Obligation.
by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
Qed.
Next Obligation.
intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
Qed.
Require Export algebra.cmra. Require Export algebra.cmra.
Require Import algebra.functor.
(* COFE *) (* COFE *)
Section cofe. Section cofe.
...@@ -173,3 +174,19 @@ Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B := ...@@ -173,3 +174,19 @@ Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A optionC B). CofeMor (fmap f : optionC A optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B). Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed. Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Program Definition optionF (Σ : iFunctor) : iFunctor := {|
ifunctor_car := optionRA Σ; ifunctor_map A B := optionC_map ifunctor_map Σ
|}.
Next Obligation.
by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
intros Σ A x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
intros Σ A B C f g x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
Qed.
Require Export program_logic.upred program_logic.resources. Require Export program_logic.upred program_logic.resources.
Require Import algebra.cofe_solver. Require Import algebra.cofe_solver.
(* The Iris program logic is parametrized by a functor from the category of
COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
propositions using the agreement CMRA. *)
Module iProp. Module iProp.
Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT := Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
uPredC (resRA Λ Σ (laterC A)). uPredC (resRA Λ Σ (laterC A)).
......
Require Export algebra.fin_maps algebra.agree algebra.excl. Require Export algebra.fin_maps algebra.agree algebra.excl algebra.functor.
Require Export program_logic.language program_logic.functor. Require Export program_logic.language.
Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res { Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
wld : mapRA positive (agreeRA A); wld : mapRA positive (agreeRA A);
......
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