From f00f21a8af7e319b25c92b6094726f66baec7f71 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Mar 2016 20:03:57 +0100
Subject: [PATCH] add some notation for writing cFunctors

---
 algebra/cofe.v             | 11 +++++++++++
 heap_lang/lang.v           |  2 +-
 program_logic/model.v      |  2 +-
 program_logic/saved_prop.v |  2 +-
 program_logic/tests.v      |  2 +-
 5 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 3fd8a65e4..ddf170fe7 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -347,6 +347,9 @@ Structure cFunctor := CFunctor {
 Existing Instance cFunctor_ne.
 Instance: Params (@cFunctor_map) 5.
 
+Delimit Scope cFunctor_scope with CF.
+Bind Scope cFunctor_scope with cFunctor.
+
 Class cFunctorContractive (F : cFunctor) :=
   cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
 
@@ -412,6 +415,7 @@ Proof.
   apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
 Qed.
 
+
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
@@ -518,3 +522,10 @@ Proof.
   intros A1 A2 B1 B2 n fg fg' Hfg.
   apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
 Qed.
+
+(** Notation for writing functors *)
+Notation "∙" := idCF : cFunctor_scope.
+Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
+Notation "( F1 , F2 , .. , Fn )" := (prodCF .. (prodCF F1%CF F2%CF) .. Fn%CF) : cFunctor_scope.
+Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
+Coercion constCF : cofeT >-> cFunctor.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index c127e0e94..bc135938a 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -20,7 +20,7 @@ Inductive binder := BAnon | BNamed : string → binder.
 Definition cons_binder (mx : binder) (X : list string) : list string :=
   match mx with BAnon => X | BNamed x => x :: X end.
 Infix ":b:" := cons_binder (at level 60, right associativity).
-Delimit Scope binder_scope with binder.
+Delimit Scope binder_scope with bind.
 Bind Scope binder_scope with binder.
 Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
 Proof. solve_decision. Defined.
diff --git a/program_logic/model.v b/program_logic/model.v
index d9ad12adb..fa422c026 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -34,7 +34,7 @@ End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
 Definition iProp_result (Λ : language) (Σ : iFunctor) :
-  solution (uPredCF (resRF Λ (laterCF idCF) Σ)) := solver.result _.
+  solution (uPredCF (resRF Λ (▶ ∙) Σ)) := solver.result _.
 
 Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ.
 Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 5298742ff..5e41b83a7 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,7 +5,7 @@ Import uPred.
 Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
   saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))).
 Definition savedPropGF (F : cFunctor) : gFunctor :=
-  GFunctor (agreeRF (laterCF F)).
+  GFunctor (agreeRF (â–¶ F)).
 Instance inGF_savedPropG  `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
 Proof. apply: inGF_inG. Qed.
 
diff --git a/program_logic/tests.v b/program_logic/tests.v
index ceb9e9dff..0a5ca9fdb 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -9,7 +9,7 @@ End ModelTest.
 Module SavedPropTest.
   (* Test if we can really go "crazy higher order" *)
   Section sec.
-    Definition F := (cofe_morCF idCF idCF).
+    Definition F : cFunctor := ( ∙ -n> ∙ ).
     Definition Σ : gFunctors := #[ savedPropGF F ].
     Context {Λ : language}.
     Notation iProp := (iPropG Λ Σ).
-- 
GitLab