1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
(** The [MakeX] classes are "smart constructors" for the logical connectives
and modalities that perform some trivial logical simplifications to give "clean"
results.
For example, when framing below logical connectives/modalities, framing should
remove connectives/modalities if the result of framing is [emp]. For example,
when framing [P] (using [iFrame]) in goal [P ∗ Q], the result should be [Q]. The
result should not be [emp ∗ Q], where [emp] would be the result of (recursively)
framing [P] in [P]. Hence, in the recursive calls, the framing machinery uses
the class [MakeSep P Q PQ]. If either [P] or [Q] is [emp] (or [True] in case of
appropriate assumptions w.r.t. affinity), the result [PQ] is [Q] or [P],
respectively. In other cases, the result is [PQ] is simply [P ∗ Q].
The [MakeX] classes are used in each recursive step of the framing machinery.
Hence, they should be "constant time", which means that the number of steps in
the inference search for [MakeX] should not depend on the size of the inputs.
This implies that [MakeX] instances should not be recursive, and [MakeX]
instances should not have premises of other classes with recursive instances. In
particular, [MakeX] instances should not have [Affine] or [Absorbing] premises
(because these could invoke a recursive search). Instances for [MakeX] instances
typically look only at the top-level symbol of the input, or check if the whole
BI is affine (via the [BiAffine] class) -- the latter can be linear in
the size of [PROP] itself, but is still independent of the size of the term.
One could imagine a smarter way of "cleaning up", as implemented in
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
but that makes framing less predictable and might have some performance impact
(i.e., not be constant time). Hence, we only perform such cleanup for [True]
and [emp].
For each of the [MakeX] class, there is a [KnownMakeX] variant, which only
succeeds if the parameter(s) is not an evar. In the case the parameter(s) is an
evar, then [MakeX] will not instantiate it arbitrarily.
The reason for this is that if given an evar, these classes would typically
try to instantiate this evar with some arbitrary logical constructs such as
[emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances
that would have this behavior.
In practice this means that usually only the default instance should use [MakeX],
and most specialized instances should use [KnownMakeX]. *)
From iris.bi Require Export bi.
From iris.prelude Require Import options.
(** Aliases for [Affine] and [Absorbing], but the instances are severely
restricted. They only inspect the top-level symbol or check if the whole BI
is affine. *)
Class QuickAffine {PROP : bi} (P : PROP) := quick_affine : Affine P.
Global Hint Mode QuickAffine + ! : typeclass_instances.
Class QuickAbsorbing {PROP : bi} (P : PROP) := quick_absorbing : Absorbing P.
Global Hint Mode QuickAbsorbing + ! : typeclass_instances.
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
Global Arguments MakeEmbed {_ _ _} _%_I _%_I.
Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
#[global] known_make_embed :: MakeEmbed P Q.
Global Arguments KnownMakeEmbed {_ _ _} _%_I _%_I.
Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
Global Arguments MakeSep {_} _%_I _%_I _%_I.
Global Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
#[global] knownl_make_sep :: MakeSep P Q PQ.
Global Arguments KnownLMakeSep {_} _%_I _%_I _%_I.
Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
#[global] knownr_make_sep :: MakeSep P Q PQ.
Global Arguments KnownRMakeSep {_} _%_I _%_I _%_I.
Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
Class MakeAnd {PROP : bi} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
Global Arguments MakeAnd {_} _%_I _%_I _%_I.
Global Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
#[global] knownl_make_and :: MakeAnd P Q PQ.
Global Arguments KnownLMakeAnd {_} _%_I _%_I _%_I.
Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
#[global] knownr_make_and :: MakeAnd P Q PQ.
Global Arguments KnownRMakeAnd {_} _%_I _%_I _%_I.
Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
Global Arguments MakeOr {_} _%_I _%_I _%_I.
Global Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
#[global] knownl_make_or :: MakeOr P Q PQ.
Global Arguments KnownLMakeOr {_} _%_I _%_I _%_I.
Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := #[global] knownr_make_or :: MakeOr P Q PQ.
Global Arguments KnownRMakeOr {_} _%_I _%_I _%_I.
Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
Global Arguments MakeAffinely {_} _%_I _%_I.
Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
#[global] known_make_affinely :: MakeAffinely P Q.
Global Arguments KnownMakeAffinely {_} _%_I _%_I.
Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
Global Arguments MakeIntuitionistically {_} _%_I _%_I.
Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
#[global] known_make_intuitionistically :: MakeIntuitionistically P Q.
Global Arguments KnownMakeIntuitionistically {_} _%_I _%_I.
Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
Global Arguments MakeAbsorbingly {_} _%_I _%_I.
Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
#[global] known_make_absorbingly :: MakeAbsorbingly P Q.
Global Arguments KnownMakeAbsorbingly {_} _%_I _%_I.
Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
Global Arguments MakePersistently {_} _%_I _%_I.
Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
#[global] known_make_persistently :: MakePersistently P Q.
Global Arguments KnownMakePersistently {_} _%_I _%_I.
Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Global Arguments MakeLaterN {_} _%_nat _%_I _%_I.
Global Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
#[global] known_make_laterN :: MakeLaterN n P lP.
Global Arguments KnownMakeLaterN {_} _%_nat _%_I _%_I.
Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
Global Arguments MakeExcept0 {_} _%_I _%_I.
Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
#[global] known_make_except_0 :: MakeExcept0 P Q.
Global Arguments KnownMakeExcept0 {_} _%_I _%_I.
Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
|
