Ton

1
/*
2
    This file is part of TON Blockchain Library.
3

4
    TON Blockchain Library is free software: you can redistribute it and/or modify
5
    it under the terms of the GNU Lesser General Public License as published by
6
    the Free Software Foundation, either version 2 of the License, or
7
    (at your option) any later version.
8

9
    TON Blockchain Library is distributed in the hope that it will be useful,
10
    but WITHOUT ANY WARRANTY; without even the implied warranty of
11
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
    GNU Lesser General Public License for more details.
13

14
    You should have received a copy of the GNU Lesser General Public License
15
    along with TON Blockchain Library.  If not, see <http://www.gnu.org/licenses/>.
16

17
    Copyright 2017-2020 Telegram Systems LLP
18
*/
19
#include "func.h"
20

21
namespace funC {
22

23
/*
24
 * 
25
 *   TYPE EXPRESSIONS
26
 * 
27
 */
28

29
int TypeExpr::holes = 0, TypeExpr::type_vars = 0;  // not thread safe, but it is ok for now
30

31
void TypeExpr::compute_width() {
32
  switch (constr) {
33
    case te_Atomic:
34
    case te_Map:
35
      minw = maxw = 1;
36
      break;
37
    case te_Tensor:
38
      minw = maxw = 0;
39
      for (TypeExpr* arg : args) {
40
        minw += arg->minw;
41
        maxw += arg->maxw;
42
      }
43
      if (minw > w_inf) {
44
        minw = w_inf;
45
      }
46
      if (maxw > w_inf) {
47
        maxw = w_inf;
48
      }
49
      break;
50
    case te_Tuple:
51
      minw = maxw = 1;
52
      for (TypeExpr* arg : args) {
53
        arg->compute_width();
54
      }
55
      break;
56
    case te_Indirect:
57
      minw = args[0]->minw;
58
      maxw = args[0]->maxw;
59
      break;
60
    default:
61
      minw = 0;
62
      maxw = w_inf;
63
      break;
64
  }
65
}
66

67
bool TypeExpr::recompute_width() {
68
  switch (constr) {
69
    case te_Tensor:
70
    case te_Indirect: {
71
      int min = 0, max = 0;
72
      for (TypeExpr* arg : args) {
73
        min += arg->minw;
74
        max += arg->maxw;
75
      }
76
      if (min > maxw || max < minw) {
77
        return false;
78
      }
79
      if (min > w_inf) {
80
        min = w_inf;
81
      }
82
      if (max > w_inf) {
83
        max = w_inf;
84
      }
85
      if (minw < min) {
86
        minw = min;
87
      }
88
      if (maxw > max) {
89
        maxw = max;
90
      }
91
      return true;
92
    }
93
    case te_Tuple: {
94
      for (TypeExpr* arg : args) {
95
        if (arg->minw > 1 || arg->maxw < 1 || arg->minw > arg->maxw) {
96
          return false;
97
        }
98
      }
99
      return true;
100
    }
101
    default:
102
      return false;
103
  }
104
}
105

106
int TypeExpr::extract_components(std::vector<TypeExpr*>& comp_list) {
107
  if (constr != te_Indirect && constr != te_Tensor) {
108
    comp_list.push_back(this);
109
    return 1;
110
  }
111
  int res = 0;
112
  for (TypeExpr* arg : args) {
113
    res += arg->extract_components(comp_list);
114
  }
115
  return res;
116
}
117

118
TypeExpr* TypeExpr::new_map(TypeExpr* from, TypeExpr* to) {
119
  return new TypeExpr{te_Map, std::vector<TypeExpr*>{from, to}};
120
}
121

122
void TypeExpr::replace_with(TypeExpr* te2) {
123
  if (te2 == this) {
124
    return;
125
  }
126
  constr = te_Indirect;
127
  value = 0;
128
  minw = te2->minw;
129
  maxw = te2->maxw;
130
  args.clear();
131
  args.push_back(te2);
132
}
133

134
bool TypeExpr::remove_indirect(TypeExpr*& te, TypeExpr* forbidden) {
135
  func_assert(te);
136
  while (te->constr == te_Indirect) {
137
    te = te->args[0];
138
  }
139
  if (te->constr == te_Unknown) {
140
    return te != forbidden;
141
  }
142
  bool res = true;
143
  for (auto& x : te->args) {
144
    res &= remove_indirect(x, forbidden);
145
  }
146
  return res;
147
}
148

149
std::vector<TypeExpr*> TypeExpr::remove_forall(TypeExpr*& te) {
150
  func_assert(te && te->constr == te_ForAll);
151
  func_assert(te->args.size() >= 1);
152
  std::vector<TypeExpr*> new_vars;
153
  for (std::size_t i = 1; i < te->args.size(); i++) {
154
    new_vars.push_back(new_hole(1));
155
  }
156
  TypeExpr* te2 = te;
157
  // std::cerr << "removing universal quantifier in " << te << std::endl;
158
  te = te->args[0];
159
  remove_forall_in(te, te2, new_vars);
160
  // std::cerr << "-> " << te << std::endl;
161
  return new_vars;
162
}
163

164
bool TypeExpr::remove_forall_in(TypeExpr*& te, TypeExpr* te2, const std::vector<TypeExpr*>& new_vars) {
165
  func_assert(te);
166
  func_assert(te2 && te2->constr == te_ForAll);
167
  if (te->constr == te_Var) {
168
    for (std::size_t i = 0; i < new_vars.size(); i++) {
169
      if (te == te2->args[i + 1]) {
170
        te = new_vars[i];
171
        return true;
172
      }
173
    }
174
    return false;
175
  }
176
  if (te->constr == te_ForAll) {
177
    return false;
178
  }
179
  if (te->args.empty()) {
180
    return false;
181
  }
182
  auto te1 = new TypeExpr(*te);
183
  bool res = false;
184
  for (auto& arg : te1->args) {
185
    res |= remove_forall_in(arg, te2, new_vars);
186
  }
187
  if (res) {
188
    te = te1;
189
  } else {
190
    delete te1;
191
  }
192
  return res;
193
}
194

195
void TypeExpr::show_width(std::ostream& os) {
196
  os << minw;
197
  if (maxw != minw) {
198
    os << "..";
199
    if (maxw < w_inf) {
200
      os << maxw;
201
    }
202
  }
203
}
204

205
std::ostream& operator<<(std::ostream& os, TypeExpr* type_expr) {
206
  if (!type_expr) {
207
    return os << "(null-type-ptr)";
208
  }
209
  return type_expr->print(os);
210
}
211

212
std::ostream& TypeExpr::print(std::ostream& os, int lex_level) {
213
  switch (constr) {
214
    case te_Unknown:
215
      return os << "??" << value;
216
    case te_Var:
217
      if (value >= -26 && value < 0) {
218
        return os << "_" << (char)(91 + value);
219
      } else if (value >= 0 && value < 26) {
220
        return os << (char)(65 + value);
221
      } else {
222
        return os << "TVAR" << value;
223
      }
224
    case te_Indirect:
225
      return os << args[0];
226
    case te_Atomic: {
227
      switch (value) {
228
        case _Int:
229
          return os << "int";
230
        case _Cell:
231
          return os << "cell";
232
        case _Slice:
233
          return os << "slice";
234
        case _Builder:
235
          return os << "builder";
236
        case _Cont:
237
          return os << "cont";
238
        case _Tuple:
239
          return os << "tuple";
240
        case _Type:
241
          return os << "type";
242
        default:
243
          return os << "atomic-type-" << value;
244
      }
245
    }
246
    case te_Tensor: {
247
      if (lex_level > -127) {
248
        os << "(";
249
      }
250
      auto c = args.size();
251
      if (c) {
252
        for (const auto& x : args) {
253
          x->print(os);
254
          if (--c) {
255
            os << ", ";
256
          }
257
        }
258
      }
259
      if (lex_level > -127) {
260
        os << ")";
261
      }
262
      return os;
263
    }
264
    case te_Tuple: {
265
      os << "[";
266
      auto c = args.size();
267
      if (c == 1 && args[0]->constr == te_Tensor) {
268
        args[0]->print(os, -127);
269
      } else if (c) {
270
        for (const auto& x : args) {
271
          x->print(os);
272
          if (--c) {
273
            os << ", ";
274
          }
275
        }
276
      }
277
      return os << "]";
278
    }
279
    case te_Map: {
280
      func_assert(args.size() == 2);
281
      if (lex_level > 0) {
282
        os << "(";
283
      }
284
      args[0]->print(os, 1);
285
      os << " -> ";
286
      args[1]->print(os);
287
      if (lex_level > 0) {
288
        os << ")";
289
      }
290
      return os;
291
    }
292
    case te_ForAll: {
293
      func_assert(args.size() >= 1);
294
      if (lex_level > 0) {
295
        os << '(';
296
      }
297
      os << "Forall ";
298
      for (std::size_t i = 1; i < args.size(); i++) {
299
        os << (i > 1 ? ' ' : '(');
300
        args[i]->print(os);
301
      }
302
      os << ") ";
303
      args[0]->print(os);
304
      if (lex_level > 0) {
305
        os << ')';
306
      }
307
      return os;
308
    }
309
    default:
310
      return os << "unknown-type-expr-" << constr;
311
  }
312
}
313

314
void UnifyError::print_message(std::ostream& os) const {
315
  os << "cannot unify type " << te1 << " with " << te2;
316
  if (!msg.empty()) {
317
    os << ": " << msg;
318
  }
319
}
320

321
std::ostream& operator<<(std::ostream& os, const UnifyError& ue) {
322
  ue.print_message(os);
323
  return os;
324
}
325

326
std::string UnifyError::message() const {
327
  std::ostringstream os;
328
  UnifyError::print_message(os);
329
  return os.str();
330
}
331

332
void check_width_compat(TypeExpr* te1, TypeExpr* te2) {
333
  if (te1->minw > te2->maxw || te2->minw > te1->maxw) {
334
    std::ostringstream os{"cannot unify types of widths ", std::ios_base::ate};
335
    te1->show_width(os);
336
    os << " and ";
337
    te2->show_width(os);
338
    throw UnifyError{te1, te2, os.str()};
339
  }
340
}
341

342
void check_update_widths(TypeExpr* te1, TypeExpr* te2) {
343
  check_width_compat(te1, te2);
344
  te1->minw = te2->minw = std::max(te1->minw, te2->minw);
345
  te1->maxw = te2->maxw = std::min(te1->maxw, te2->maxw);
346
  func_assert(te1->minw <= te1->maxw);
347
}
348

349
void unify(TypeExpr*& te1, TypeExpr*& te2) {
350
  func_assert(te1 && te2);
351
  // std::cerr << "unify( " << te1 << " , " << te2 << " )\n";
352
  while (te1->constr == TypeExpr::te_Indirect) {
353
    te1 = te1->args[0];
354
  }
355
  while (te2->constr == TypeExpr::te_Indirect) {
356
    te2 = te2->args[0];
357
  }
358
  if (te1 == te2) {
359
    return;
360
  }
361
  if (te1->constr == TypeExpr::te_ForAll) {
362
    TypeExpr* te = te1;
363
    std::vector<TypeExpr*> new_vars = TypeExpr::remove_forall(te);
364
    for (TypeExpr* t : new_vars) {
365
      t->was_forall_var = true;
366
    }
367
    unify(te, te2);
368
    for (TypeExpr* t : new_vars) {
369
      t->was_forall_var = false;
370
    }
371
    return;
372
  }
373
  if (te2->constr == TypeExpr::te_ForAll) {
374
    TypeExpr* te = te2;
375
    std::vector<TypeExpr*> new_vars = TypeExpr::remove_forall(te);
376
    for (TypeExpr* t : new_vars) {
377
      t->was_forall_var = true;
378
    }
379
    unify(te1, te);
380
    for (TypeExpr* t : new_vars) {
381
      t->was_forall_var = false;
382
    }
383
    return;
384
  }
385
  if (te1->was_forall_var && te2->constr == TypeExpr::te_Tensor) {
386
    throw UnifyError{te1, te2, "cannot unify generic type and tensor"};
387
  }
388
  if (te2->was_forall_var && te1->constr == TypeExpr::te_Tensor) {
389
    throw UnifyError{te2, te1, "cannot unify generic type and tensor"};
390
  }
391
  if (te1->constr == TypeExpr::te_Unknown) {
392
    if (te2->constr == TypeExpr::te_Unknown) {
393
      func_assert(te1->value != te2->value);
394
    }
395
    if (!TypeExpr::remove_indirect(te2, te1)) {
396
      throw UnifyError{te1, te2, "type unification results in an infinite cyclic type"};
397
    }
398
    check_update_widths(te1, te2);
399
    te1->replace_with(te2);
400
    te1 = te2;
401
    return;
402
  }
403
  if (te2->constr == TypeExpr::te_Unknown) {
404
    if (!TypeExpr::remove_indirect(te1, te2)) {
405
      throw UnifyError{te2, te1, "type unification results in an infinite cyclic type"};
406
    }
407
    check_update_widths(te2, te1);
408
    te2->replace_with(te1);
409
    te2 = te1;
410
    return;
411
  }
412
  if (te1->constr != te2->constr || te1->value != te2->value || te1->args.size() != te2->args.size()) {
413
    throw UnifyError{te1, te2};
414
  }
415
  for (std::size_t i = 0; i < te1->args.size(); i++) {
416
    unify(te1->args[i], te2->args[i]);
417
  }
418
  if (te1->constr == TypeExpr::te_Tensor) {
419
    if (!te1->recompute_width()) {
420
      throw UnifyError{te1, te2, "type unification incompatible with known width of first type"};
421
    }
422
    if (!te2->recompute_width()) {
423
      throw UnifyError{te2, te1, "type unification incompatible with known width of first type"};
424
    }
425
    check_update_widths(te1, te2);
426
  }
427
  te1->replace_with(te2);
428
  te1 = te2;
429
}
430

431
}  // namespace funC
432