global_functor.v 3.14 KB
Newer Older
1
2
From program_logic Require Export ghost_ownership.

3
4
5
6
7
Module rFunctors.
  Inductive rFunctors :=
    | nil  : rFunctors
    | cons : rFunctor  rFunctors  rFunctors.
  Coercion singleton (F : rFunctor) : rFunctors := cons F nil.
8
9
10
11
12
13

  Fixpoint fold_right {A} (f : rFunctor  A  A) (a : A) (Fs : rFunctors) : A :=
    match Fs with
    | nil => a
    | cons F Fs => f F (fold_right f a Fs)
    end.
14
15
16
17
18
19
20
21
22
End rFunctors.
Notation rFunctors := rFunctors.rFunctors.

Delimit Scope rFunctors_scope with rFunctors.
Bind Scope rFunctors_scope with rFunctors.
Arguments rFunctors.cons _ _%rFunctors.

Notation "[ ]" := rFunctors.nil (format "[ ]") : rFunctors_scope.
Notation "[ F ]" := (rFunctors.cons F rFunctors.nil) : rFunctors_scope.
23
Notation "[ F ; .. ; F' ]" :=
24
  (rFunctors.cons F .. (rFunctors.cons F' rFunctors.nil) ..) : rFunctors_scope.
25

26
27
Module rFunctorG.
  Definition nil : rFunctorG := const (constRF unitR).
28

29
  Definition cons (F : rFunctor) (Σ : rFunctorG) : rFunctorG :=
30
31
    λ n, match n with O => F | S n => Σ n end.

32
  Fixpoint app (Fs : rFunctors) (Σ : rFunctorG) : rFunctorG :=
33
    match Fs with
34
35
    | rFunctors.nil => Σ
    | rFunctors.cons F Fs => cons F (app Fs Σ)
36
    end.
37
End rFunctorG.
38

39
(** Cannot bind this scope with the [rFunctorG] since [rFunctorG] is a
40
notation hiding a more complex type. *)
41
42
Notation "#[ ]" := rFunctorG.nil (format "#[ ]").
Notation "#[ Fs ]" := (rFunctorG.app Fs rFunctorG.nil).
43
Notation "#[ Fs ; .. ; Fs' ]" :=
44
  (rFunctorG.app Fs .. (rFunctorG.app Fs' rFunctorG.nil) ..).
45
46
47
48

(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
   the functor breaks badly because Coq is unable to infer the correct
   typeclasses, it does not unfold the functor. *)
49
Class inGF (Λ : language) (Σ : rFunctorG) (F : rFunctor) := InGF {
50
51
52
53
54
55
56
57
58
59
60
61
  inGF_id : gid;
  inGF_prf : F = Σ inGF_id;
}.
(* Avoid eager type class search: this line ensures that type class search
is only triggered if the first two arguments of inGF do not contain evars. Since
instance search for [inGF] is restrained, instances should always have [inGF] as
their first argument to avoid loops. For example, the instances [authGF_inGF]
and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode inGF + + - : typeclass_instances.

Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
62
Instance inGF_here {Λ Σ} (F: rFunctor) : inGF Λ (rFunctorG.cons F Σ) F.
63
Proof. by exists 0. Qed.
64
65
Instance inGF_further {Λ Σ} (F F': rFunctor) :
  inGF Λ Σ F  inGF Λ (rFunctorG.cons F' Σ) F.
66
Proof. intros [i ?]. by exists (S i). Qed.
67
68
69
70
71
72
73
74
75
76
77
78
79

(** For modules that need more than one functor, we offer a typeclass
    [inGFs] to demand a list of rFunctor to be available. We do
    *not* register any instances that go from there to [inGF], to
    avoid cycles. *)
Class inGFs (Λ : language) (Σ : rFunctorG) (Fs : rFunctors) :=
  InGFs : (rFunctors.fold_right (λ F T, inGF Λ Σ F * T) () Fs)%type.

Instance inGFs_nil {Λ Σ} : inGFs Λ Σ [].
Proof. exact tt. Qed.
Instance inGFs_cons {Λ Σ} F Fs :
  inGF Λ Σ F  inGFs Λ Σ Fs  inGFs Λ Σ (rFunctors.cons F Fs).
Proof. split; done. Qed.