summaryrefslogtreecommitdiff
path: root/src/Substitute.ml
blob: 9db58812886d73ee6589e075271d50884191a18f (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
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
(** This file implements various substitution utilities to instantiate types,
    function bodies, etc.
 *)

module T = Types
module TU = TypesUtils
module V = Values
module E = Expressions
module A = CfimAst
module C = Contexts

(** Substitute types variables and regions in a type *)
let rec ty_substitute (rsubst : 'r1 -> 'r2)
    (tsubst : T.TypeVarId.id -> 'r2 T.ty) (ty : 'r1 T.ty) : 'r2 T.ty =
  let open T in
  let subst = ty_substitute rsubst tsubst in
  (* helper *)
  match ty with
  | Adt (def_id, regions, tys) ->
      Adt (def_id, List.map rsubst regions, List.map subst tys)
  | Array aty -> Array (subst aty)
  | Slice sty -> Slice (subst sty)
  | Ref (r, ref_ty, ref_kind) -> Ref (rsubst r, subst ref_ty, ref_kind)
  (* Below variants: we technically return the same value, but because
     one has type ['r1 ty] and the other has type ['r2 ty], we need to
     deconstruct then reconstruct *)
  | Bool -> Bool
  | Char -> Char
  | Never -> Never
  | Integer int_ty -> Integer int_ty
  | Str -> Str
  | TypeVar vid -> tsubst vid

(** Convert an [rty] to an [ety] by erasing the region variables *)
let erase_regions (ty : T.rty) : T.ety =
  ty_substitute (fun _ -> T.Erased) (fun vid -> T.TypeVar vid) ty

(** Generate fresh regions for region variables.

    Return the list of new regions and appropriate substitutions from the
    original region variables to the fresh regions.
    
    TODO: simplify? we only need the subst `T.RegionVarId.id -> T.RegionId.id`
  *)
let fresh_regions_with_substs (region_vars : T.region_var list) :
    T.RegionId.id list
    * (T.RegionVarId.id -> T.RegionId.id)
    * (T.RegionVarId.id T.region -> T.RegionId.id T.region) =
  (* Generate fresh regions *)
  let fresh_region_ids = List.map (fun _ -> C.fresh_region_id ()) region_vars in
  (* Generate the map from region var ids to regions *)
  let ls = List.combine region_vars fresh_region_ids in
  let rid_map =
    List.fold_left
      (fun mp (k, v) -> T.RegionVarId.Map.add k.T.index v mp)
      T.RegionVarId.Map.empty ls
  in
  (* Generate the substitution from region var id to region *)
  let rid_subst id = T.RegionVarId.Map.find id rid_map in
  (* Generate the substitution from region to region *)
  let rsubst r =
    match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
  in
  (* Return *)
  (fresh_region_ids, rid_subst, rsubst)

(** Erase the regions in a type and substitute the type variables *)
let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
    (ty : 'r T.region T.ty) : T.ety =
  let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
  ty_substitute rsubst tsubst ty

(** Create a region substitution from a list of region variable ids and a list of
    regions (with which to substitute the region variable ids *)
let make_region_subst (var_ids : T.RegionVarId.id list)
    (regions : 'r T.region list) : T.RegionVarId.id T.region -> 'r T.region =
  let ls = List.combine var_ids regions in
  let mp =
    List.fold_left
      (fun mp (k, v) -> T.RegionVarId.Map.add k v mp)
      T.RegionVarId.Map.empty ls
  in
  fun r ->
    match r with
    | T.Static -> T.Static
    | T.Var id -> T.RegionVarId.Map.find id mp

(** Create a type substitution from a list of type variable ids and a list of
    types (with which to substitute the type variable ids) *)
let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
    T.TypeVarId.id -> 'r T.ty =
  let ls = List.combine var_ids tys in
  let mp =
    List.fold_left
      (fun mp (k, v) -> T.TypeVarId.Map.add k v mp)
      T.TypeVarId.Map.empty ls
  in
  fun id -> T.TypeVarId.Map.find id mp

(** Instantiate the type variables in an ADT definition, and return, for
    every variant, the list of the types of its fields *)
let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def)
    (regions : T.RegionId.id T.region list) (types : T.rty list) :
    (T.VariantId.id option * T.rty list) list =
  let r_subst =
    make_region_subst
      (List.map (fun x -> x.T.index) def.T.region_params)
      regions
  in
  let ty_subst =
    make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
  in
  let (variants_fields : (T.VariantId.id option * T.field list) list) =
    match def.T.kind with
    | T.Enum variants ->
        List.mapi
          (fun i v -> (Some (T.VariantId.of_int i), v.T.fields))
          variants
    | T.Struct fields -> [ (None, fields) ]
  in
  List.map
    (fun (id, fields) ->
      ( id,
        List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields
      ))
    variants_fields

(** Instantiate the type variables in an ADT definition, and return the list
    of types of the fields for the chosen variant *)
let type_def_get_instantiated_field_rtypes (def : T.type_def)
    (opt_variant_id : T.VariantId.id option)
    (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
  let r_subst =
    make_region_subst
      (List.map (fun x -> x.T.index) def.T.region_params)
      regions
  in
  let ty_subst =
    make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
  in
  let fields = TU.type_def_get_fields def opt_variant_id in
  List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields

(** Return the types of the properly instantiated ADT's variant, provided a
    context *)
let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
    (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
  let def = C.ctx_lookup_type_def ctx def_id in
  type_def_get_instantiated_field_rtypes def opt_variant_id regions types

(** Return the types of the properly instantiated ADT value (note that
    here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *)
let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
    (adt : V.adt_value) (id : T.type_id)
    (region_params : T.RegionId.id T.region list) (type_params : T.rty list) :
    T.rty list =
  match id with
  | T.AdtId id ->
      (* Retrieve the types of the fields *)
      ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id
        region_params type_params
  | T.Tuple ->
      assert (List.length region_params = 0);
      type_params
  | T.Assumed aty -> (
      match aty with
      | T.Box ->
          assert (List.length region_params = 0);
          assert (List.length type_params = 1);
          type_params)

(** Instantiate the type variables in an ADT definition, and return the list
    of types of the fields for the chosen variant *)
let type_def_get_instantiated_field_etypes (def : T.type_def)
    (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
  let ty_subst =
    make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
  in
  let fields = TU.type_def_get_fields def opt_variant_id in
  List.map
    (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
    fields

(** Return the types of the properly instantiated ADT's variant, provided a
    context *)
let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
    (types : T.ety list) : T.ety list =
  let def = C.ctx_lookup_type_def ctx def_id in
  type_def_get_instantiated_field_etypes def opt_variant_id types

(** Apply a type substitution to a place *)
let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place
    =
  (* There is nothing to do *)
  p

(** Apply a type substitution to an operand constant value *)
let operand_constant_value_substitute (_tsubst : T.TypeVarId.id -> T.ety)
    (op : E.operand_constant_value) : E.operand_constant_value =
  (* There is nothing to do *)
  op

(** Apply a type substitution to an operand *)
let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
    E.operand =
  let p_subst = place_substitute tsubst in
  match op with
  | E.Copy p -> E.Copy (p_subst p)
  | E.Move p -> E.Move (p_subst p)
  | E.Constant (ety, cv) ->
      let rsubst x = x in
      E.Constant
        ( ty_substitute rsubst tsubst ety,
          operand_constant_value_substitute tsubst cv )

(** Apply a type substitution to an rvalue *)
let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
    E.rvalue =
  let op_subst = operand_substitute tsubst in
  let p_subst = place_substitute tsubst in
  match rv with
  | E.Use op -> E.Use (op_subst op)
  | E.Ref (p, bkind) -> E.Ref (p_subst p, bkind)
  | E.UnaryOp (unop, op) -> E.UnaryOp (unop, op_subst op)
  | E.BinaryOp (binop, op1, op2) ->
      E.BinaryOp (binop, op_subst op1, op_subst op2)
  | E.Discriminant p -> E.Discriminant (p_subst p)
  | E.Aggregate (kind, ops) ->
      let ops = List.map op_subst ops in
      let kind =
        match kind with
        | E.AggregatedTuple -> E.AggregatedTuple
        | E.AggregatedAdt (def_id, variant_id, regions, tys) ->
            let rsubst x = x in
            E.AggregatedAdt
              ( def_id,
                variant_id,
                regions,
                List.map (ty_substitute rsubst tsubst) tys )
      in
      E.Aggregate (kind, ops)

(** Apply a type substitution to an assertion *)
let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety) (a : A.assertion) :
    A.assertion =
  { A.cond = operand_substitute tsubst a.A.cond; A.expected = a.A.expected }

(** Apply a type substitution to a call *)
let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call
    =
  let rsubst x = x in
  let type_params = List.map (ty_substitute rsubst tsubst) call.A.type_params in
  let args = List.map (operand_substitute tsubst) call.A.args in
  let dest = place_substitute tsubst call.A.dest in
  (* Putting all the paramters on purpose: we want to get a compiler error if
     something moves - we may add a field on which we need to apply a substitution *)
  {
    func = call.A.func;
    region_params = call.A.region_params;
    A.type_params;
    args;
    dest;
  }

(** Apply a type substitution to a statement *)
let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
    (st : A.statement) : A.statement =
  match st with
  | A.Assign (p, rvalue) ->
      let p = place_substitute tsubst p in
      let rvalue = rvalue_substitute tsubst rvalue in
      A.Assign (p, rvalue)
  | A.FakeRead p ->
      let p = place_substitute tsubst p in
      A.FakeRead p
  | A.SetDiscriminant (p, vid) ->
      let p = place_substitute tsubst p in
      A.SetDiscriminant (p, vid)
  | A.Drop p ->
      let p = place_substitute tsubst p in
      A.Drop p
  | A.Assert assertion ->
      let assertion = assertion_substitute tsubst assertion in
      A.Assert assertion
  | A.Call call ->
      let call = call_substitute tsubst call in
      A.Call call
  | A.Panic | A.Return | A.Break _ | A.Continue _ | A.Nop -> st
  | A.Sequence (st1, st2) ->
      A.Sequence
        (statement_substitute tsubst st1, statement_substitute tsubst st2)
  | A.Switch (op, tgts) ->
      A.Switch
        (operand_substitute tsubst op, switch_targets_substitute tsubst tgts)
  | A.Loop le -> A.Loop (statement_substitute tsubst le)

(** Apply a type substitution to switch targets *)
and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety)
    (tgts : A.switch_targets) : A.switch_targets =
  match tgts with
  | A.If (st1, st2) ->
      A.If (statement_substitute tsubst st1, statement_substitute tsubst st2)
  | A.SwitchInt (int_ty, tgts, otherwise) ->
      let tgts =
        List.map (fun (sv, st) -> (sv, statement_substitute tsubst st)) tgts
      in
      let otherwise = statement_substitute tsubst otherwise in
      A.SwitchInt (int_ty, tgts, otherwise)

(** Apply a type substitution to a function body. Return the local variables
    and the body. *)
let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
    (def : A.fun_def) : A.var list * A.statement =
  let rsubst r = r in
  let locals =
    List.map
      (fun v -> { v with A.var_ty = ty_substitute rsubst tsubst v.A.var_ty })
      def.A.locals
  in
  let body = statement_substitute tsubst def.body in
  (locals, body)

(** Substitute a function signature *)
let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
    (rsubst : T.RegionVarId.id -> T.RegionId.id)
    (tsubst : T.TypeVarId.id -> T.rty) (sg : A.fun_sig) : A.inst_fun_sig =
  let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
  in
  let inputs = List.map (ty_substitute rsubst' tsubst) sg.A.inputs in
  let output = ty_substitute rsubst' tsubst sg.A.output in
  let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
    let id = asubst rg.id in
    let regions = List.map rsubst rg.regions in
    let parents = List.map asubst rg.parents in
    { id; regions; parents }
  in
  let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
  { A.regions_hierarchy; inputs; output }