From dbf38eb5e32ff2344d30fab8301ed905d078588e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2016 21:59:22 +0100
Subject: [PATCH] move functor def. to algebra/

---
 _CoqProject                          |  2 +-
 algebra/agree.v                      |  6 +++
 algebra/auth.v                       | 17 ++++++++
 algebra/excl.v                       |  7 ++++
 algebra/fin_maps.v                   | 16 ++++++++
 {program_logic => algebra}/functor.v | 61 +---------------------------
 algebra/option.v                     | 17 ++++++++
 program_logic/model.v                |  5 +++
 program_logic/resources.v            |  4 +-
 9 files changed, 72 insertions(+), 63 deletions(-)
 rename {program_logic => algebra}/functor.v (51%)

diff --git a/_CoqProject b/_CoqProject
index c8698f0db..81a1f9bb0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,6 +47,7 @@ algebra/dra.v
 algebra/cofe_solver.v
 algebra/agree.v
 algebra/excl.v
+algebra/functor.v
 program_logic/upred.v
 program_logic/model.v
 program_logic/adequacy.v
@@ -61,7 +62,6 @@ program_logic/pviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
-program_logic/functor.v
 program_logic/tests.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 62ec7ff26..bb07a72e9 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
@@ -174,3 +175,8 @@ Proof.
   intros f g Hfg x; split; simpl; intros; first done.
   by apply dist_le with n; try apply Hfg.
 Qed.
+
+Program Definition agreeF : iFunctor :=
+  {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
+Solve Obligations with done.
+
diff --git a/algebra/auth.v b/algebra/auth.v
index f5b396813..29760ee65 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,4 +1,5 @@
 Require Export algebra.excl.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 
 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 :=
   CofeMor (auth_map f).
 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.
+
+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.
+
diff --git a/algebra/excl.v b/algebra/excl.v
index d0a7df42a..f2acac84d 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -181,3 +182,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
   CofeMor (excl_map f).
 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.
+
+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.
+
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 9ca47881e..b2b65e30d 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra prelude.gmap algebra.option.
+Require Import algebra.functor.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
@@ -246,3 +247,18 @@ Proof.
   intros f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 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.
diff --git a/program_logic/functor.v b/algebra/functor.v
similarity index 51%
rename from program_logic/functor.v
rename to algebra/functor.v
index 1fe954763..819ca5b5f 100644
--- a/program_logic/functor.v
+++ b/algebra/functor.v
@@ -1,12 +1,7 @@
 Require Export algebra.cmra.
-Require Import algebra.agree algebra.excl algebra.auth.
-Require Import algebra.option algebra.fin_maps.
 
 (** * Functors from COFE to CMRA *)
-(* 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. *)
+(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
 Structure iFunctor := IFunctor {
   ifunctor_car :> cofeT → cmraT;
   ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
@@ -60,57 +55,3 @@ Next Obligation.
   intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
   apply iprod_map_ext=> y; apply ifunctor_map_compose.
 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.
diff --git a/algebra/option.v b/algebra/option.v
index 4c443e3a8..e6fb047af 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 
 (* COFE *)
 Section cofe.
@@ -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).
 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.
+
+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.
+
diff --git a/program_logic/model.v b/program_logic/model.v
index 022e7419e..d6d9721b0 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,6 +1,11 @@
 Require Export program_logic.upred program_logic.resources.
 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.
 Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
   uPredC (resRA Λ Σ (laterC A)).
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 44edf9de4..d4c2aebe6 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -1,5 +1,5 @@
-Require Export algebra.fin_maps algebra.agree algebra.excl.
-Require Export program_logic.language program_logic.functor.
+Require Export algebra.fin_maps algebra.agree algebra.excl algebra.functor.
+Require Export program_logic.language.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
-- 
GitLab