summaryrefslogtreecommitdiff
path: root/compiler/InterpreterBorrows.mli
blob: cf14e94b2c0f495fd6fc1047b0abeaf806bdd845 (plain)
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
open Types
open Values
open Contexts
open Cps

(** When copying values, we duplicate the shared borrows. This is tantamount to
    reborrowing the shared value. The [reborrow_shared original_id new_bid ctx]
    applies this change to an environment [ctx] by inserting a new borrow id in
    the set of borrows tracked by a shared value, referenced by the
    [original_bid] argument.  *)
val reborrow_shared :
  Meta.span -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx

(** End a borrow identified by its id, while preserving the invariants.

    If the borrow is inside another borrow/an abstraction or contains loans,
    [end_borrow] will end those borrows/abstractions/loans first.
  *)
val end_borrow : config -> Meta.span -> BorrowId.id -> cm_fun

(** End a set of borrows identified by their ids, while preserving the invariants. *)
val end_borrows : config -> Meta.span -> BorrowId.Set.t -> cm_fun

(** End an abstraction while preserving the invariants. *)
val end_abstraction : config -> Meta.span -> AbstractionId.id -> cm_fun

(** End a set of abstractions while preserving the invariants. *)
val end_abstractions : config -> Meta.span -> AbstractionId.Set.t -> cm_fun

(** End a borrow and return the resulting environment, ignoring synthesis *)
val end_borrow_no_synth :
  config -> Meta.span -> BorrowId.id -> eval_ctx -> eval_ctx

(** End a set of borrows and return the resulting environment, ignoring synthesis *)
val end_borrows_no_synth :
  config -> Meta.span -> BorrowId.Set.t -> eval_ctx -> eval_ctx

(** End an abstraction and return the resulting environment, ignoring synthesis *)
val end_abstraction_no_synth :
  config -> Meta.span -> AbstractionId.id -> eval_ctx -> eval_ctx

(** End a set of abstractions and return the resulting environment, ignoring synthesis *)
val end_abstractions_no_synth :
  config -> Meta.span -> AbstractionId.Set.t -> eval_ctx -> eval_ctx

(** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.

    Reserved borrows are special mutable borrows which are created as shared borrows
    then promoted to mutable borrows upon their first use.

    This function replaces the reserved borrow with a mutable borrow, then replaces
    the corresponding shared loan with a mutable loan (after having ended the
    other shared borrows which point to this loan).
 *)
val promote_reserved_mut_borrow : config -> Meta.span -> BorrowId.id -> cm_fun

(** Transform an abstraction to an abstraction where the values are not
    structured.

    For instance:
    {[
      abs {
        (mut_borrow l0, mut_borrow l1, _)
      }

          ~~>

      abs {
        mut_borrow l0
        mut_borrow l1
      }
    ]}

    Rem.: we do this to simplify the merging of abstractions. We can do this
    because for now we don't support nested borrows. In order to implement
    support for nested borrows, we will probably need to maintain the structure
    of the avalues.

    Paramters:
    - [abs_kind]
    - [can_end]
    - [destructure_shared_values]: if [true], explore shared values and whenever we find
      a shared loan, move it elsewhere by replacing it with the same value without
      the shared loan, and adding another ashared loan in the abstraction.
      For instance:
      {[
         ML {l0} (0, ML {l1} 1)

         ~~>

         ML {l0} (0, 1)
         ML {l1} 1
      ]}
    - [ctx]
    - [abs]
 *)
val destructure_abs :
  Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs

(** Return [true] if the values in an abstraction are destructured.

    We simply destructure it and check that it gives the identity.

    The input boolean is [destructure_shared_value]. See {!destructure_abs}.
 *)
val abs_is_destructured : Meta.span -> bool -> eval_ctx -> abs -> bool

(** Turn a value into a abstractions.

    We are conservative, and don't group borrows/loans into the same abstraction
    unless necessary.

    For instance:
    {[
      _ -> (mut_borrow l1 (mut_loan l2), mut_borrow l3)

      ~~>

      abs'0 { mut_borrow l1, mut_loan l2 }
      abs'1 { mut_borrow l3 }
    ]}

    Parameters:
    - [abs_kind]
    - [can_end]
    - [destructure_shared_values]: this is similar to [destructure_shared_values]
      for {!destructure_abs}.
    - [ctx]
    - [v]
 *)
val convert_value_to_abstractions :
  Meta.span -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list

(** See {!merge_into_abstraction}.

    Rem.: it may be more idiomatic to have a functor, but this seems a bit
    heavyweight, though.
  *)
type merge_duplicates_funcs = {
  merge_amut_borrows :
    borrow_id ->
    rty ->
    proj_marker ->
    typed_avalue ->
    rty ->
    proj_marker ->
    typed_avalue ->
    typed_avalue;
      (** Parameters:
          - [id]
          - [ty0]
          - [pm0]
          - [child0]
          - [ty1]
          - [pm1]
          - [child1]

          The children should be [AIgnored].
       *)
  merge_ashared_borrows :
    borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue;
      (** Parameters:
          - [id]
          - [ty0]
          - [pm0]
          - [ty1]
          - [pm1]
       *)
  merge_amut_loans :
    loan_id ->
    rty ->
    proj_marker ->
    typed_avalue ->
    rty ->
    proj_marker ->
    typed_avalue ->
    typed_avalue;
      (** Parameters:
          - [id]
          - [ty0]
          - [pm0]
          - [child0]
          - [ty1]
          - [pm1]
          - [child1]

          The children should be [AIgnored].
       *)
  merge_ashared_loans :
    loan_id_set ->
    rty ->
    proj_marker ->
    typed_value ->
    typed_avalue ->
    rty ->
    proj_marker ->
    typed_value ->
    typed_avalue ->
    typed_avalue;
      (** Parameters:
          - [ids]
          - [ty0]
          - [pm0]
          - [sv0]
          - [child0]
          - [ty1]
          - [pm1]
          - [sv1]
          - [child1]
       *)
}

(** Merge an abstraction into another abstraction.

    We insert the result of the merge in place of the first abstraction (and in
    particular, we don't simply push the merged abstraction at the end of the
    environment: this helps preserving the structure of the environment, when
    computing loop fixed points for instance).

    When we merge two abstractions together, we remove the loans which appear
    in the *left* abstraction and whose corresponding borrows appear in the
    **right** abstraction.
    For instance:
    {[
      abs'0 { mut_borrow l0, mut_loan l1 }   // Rem.: mut_loan l1
      abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1

          ~~>

      abs'2 { mut_borrow l0, mut_borrow l2 }
    ]}

    We also simplify the markers, when the same value appears in both abstractions
    but with different markers. For instance:
    {[
      abs'0 { |mut_borrow l0|, mut_loan l1 }
      abs'1 { ︙mut_borrow l0︙, mut_borrow l1 }

          ~~>

      abs'2 { mut_borrow l0 }
    ]}

    Finally, we merge all their regions together. For instance, if [abs'0] projects
    region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0]
    (the one with the smallest index in practice) and substitute [r1] with [r0]
    in the whole context.

    Parameters:
    - [kind]
    - [can_end]
    - [merge_funs]: those functions are used to merge borrows/loans with the
      *same ids* but different markers. This is necessary when doing a collapse
      (see the computation of joins).
      If [merge_funs] are not provided, we check that there are no markers.
    - [ctx]
    - [abs_id0]
    - [abs_id1]

    We return the updated context as well as the id of the new abstraction which
    results from the merge.
 *)
val merge_into_first_abstraction :
  Meta.span ->
  abs_kind ->
  bool ->
  merge_duplicates_funcs option ->
  eval_ctx ->
  AbstractionId.id ->
  AbstractionId.id ->
  eval_ctx * AbstractionId.id

(** Reorder the loans and borrows in the fresh abstractions.

    We do this in order to enforce some structure in the environments: this
    allows us to find fixed-points. Note that this function needs to be
    called typically after we merge abstractions together (see {!reduce_ctx}
    and {!collapse_ctx} for instance).

    Inputs:
    - [span]
    - [allow_markers]: disables some sanity checks (which check that projection
      markers don't appear).
    - [old_abs_ids]
    - [eval_ctx]
 *)
val reorder_loans_borrows_in_fresh_abs :
  Meta.span -> bool -> AbstractionId.Set.t -> eval_ctx -> eval_ctx