Repository navigation
Expand file tree
/
Copy pathcontext.cpp
More file actions
415 lines (374 loc) · 19.7 KB
/
Copy pathcontext.cpp
File metadata and controls
415 lines (374 loc) · 19.7 KB
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
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
#include "cppl/kernel/context.hpp"
#include "cppl/kernel/arithmetic.hpp"
#include "cppl/kernel/term.hpp"
#include "cppl/kernel/types.hpp"
#include <cstddef>
#include <cstdint>
#include <expected>
#include <span>
#include <string>
#include <type_traits>
#include <utility>
#include <variant>
#include <vector>
namespace cppl::kernel {
namespace {
std::unexpected<CoreError> fail(CoreErrorKind kind, std::string detail) {
return std::unexpected(CoreError{kind, std::move(detail)});
}
[[nodiscard]] std::expected<void, CoreError> validate_type(const Type& type) {
if (!is_supported(type)) {
return fail(CoreErrorKind::MalformedType, "unsupported or malformed core type");
}
return {};
}
[[nodiscard]] std::expected<Type, CoreError> type_of_impl(const Context& context, std::span<const Type> locals,
const Term& term, const CoreLimits& limits,
std::uint32_t depth) {
if (depth > limits.max_term_depth) {
return fail(CoreErrorKind::DepthLimitExceeded, "term nests deeper than the core allows");
}
return std::visit(
[&](const auto& node) -> std::expected<Type, CoreError> {
using Node = std::decay_t<decltype(node)>;
if constexpr (std::is_same_v<Node, Var>) {
if (node.index.value >= locals.size()) {
return fail(CoreErrorKind::VariableOutOfScope,
"variable #" + std::to_string(node.index.value) + " has no enclosing binder");
}
const Type& type = locals[locals.size() - 1 - node.index.value];
if (auto valid = validate_type(type); !valid) {
return std::unexpected(valid.error());
}
return type;
} else if constexpr (std::is_same_v<Node, Literal>) {
Type type{node.type};
if (auto valid = validate_type(type); !valid) {
return std::unexpected(valid.error());
}
if (!is_representable(node.type, node.value)) {
return fail(CoreErrorKind::MalformedLiteral,
"literal " + describe(node.value) + " is not representable in " + describe(node.type));
}
return std::move(type);
} else if constexpr (std::is_same_v<Node, Call>) {
const Definition* definition = context.lookup(node.callee);
if (definition == nullptr) {
return fail(CoreErrorKind::UnknownDefinition,
"def#" + std::to_string(node.callee.value) + " is not defined");
}
if (definition->parameters.size() != node.arguments.size()) {
return fail(CoreErrorKind::ArityMismatch, "def#" + std::to_string(node.callee.value) + " expects " +
std::to_string(definition->parameters.size()) +
" arguments but received " +
std::to_string(node.arguments.size()));
}
for (std::size_t index = 0; index < node.arguments.size(); ++index) {
auto argument = type_of_impl(context, locals, node.arguments[index], limits, depth + 1);
if (!argument) {
return argument;
}
if (!(*argument == definition->parameters[index])) {
return fail(CoreErrorKind::TypeMismatch,
"argument " + std::to_string(index) + " of def#" +
std::to_string(node.callee.value) + " has type " + describe(*argument) +
" but " + describe(definition->parameters[index]) + " is required");
}
}
return definition->result;
} else if constexpr (std::is_same_v<Node, Projection>) {
if (!is_supported(node.domain) || !node.domain.is_value())
return fail(CoreErrorKind::MalformedType, "projection requires a valid abstract domain");
const auto& signature = std::get<ValueType>(node.domain.node);
if (node.index >= signature.projections.size())
return fail(CoreErrorKind::MalformedPrimitive, "projection index is outside its signature");
if (node.arguments.size() != 1)
return fail(CoreErrorKind::ArityMismatch, "projection requires exactly one subject");
auto subject = type_of_impl(context, locals, node.arguments[0], limits, depth + 1);
if (!subject)
return subject;
if (*subject != node.domain)
return fail(CoreErrorKind::TypeMismatch, "projection subject does not match its domain signature");
return signature.projections[node.index];
} else if constexpr (std::is_same_v<Node, Element>) {
// FOUNDATIONS.md 45. The index is typed but unconstrained: the
// observation is total, and `index < extent` is a separate
// obligation this rule deliberately does not require.
if (!is_supported(node.domain) || !node.domain.is_indexed())
return fail(CoreErrorKind::MalformedType, "element requires a valid indexed domain");
if (node.arguments.size() != 2)
return fail(CoreErrorKind::ArityMismatch, "element requires exactly one subject and one index");
auto subject = type_of_impl(context, locals, node.arguments[0], limits, depth + 1);
if (!subject)
return subject;
if (*subject != node.domain)
return fail(CoreErrorKind::TypeMismatch, "element subject does not match its indexed domain");
auto index = type_of_impl(context, locals, node.arguments[1], limits, depth + 1);
if (!index)
return index;
if (!index->is_integer())
return fail(CoreErrorKind::TypeMismatch, "element index must be an integer");
return std::get<IndexedType>(node.domain.node).element[0];
} else {
const Type type{node.type};
if (auto valid = validate_type(type); !valid) {
return std::unexpected(valid.error());
}
if (!is_arithmetic(node.op) && !is_comparison(node.op) && !is_representability(node.op) &&
node.op != PrimOp::Not && node.op != PrimOp::Select && node.op != PrimOp::Quotient &&
node.op != PrimOp::Remainder && node.op != PrimOp::Convert) {
return fail(CoreErrorKind::MalformedPrimitive, "unrecognized primitive");
}
if (node.op == PrimOp::Not && !(node.type == kBoolean)) {
return fail(CoreErrorKind::TypeMismatch, "negation requires a boolean");
}
const std::size_t required_arity = arity(node.op);
if (node.arguments.size() != required_arity) {
return fail(CoreErrorKind::ArityMismatch,
describe(node.op) + " expects " + std::to_string(required_arity) +
" arguments but received " + std::to_string(node.arguments.size()));
}
// A conversion's argument is of whatever integer type it is
// converted from; that type is the argument's own, so it is
// derived here rather than stated, and anything but a
// supported integer is refused (RFC 0019).
if (node.op == PrimOp::Convert) {
auto argument_type = type_of_impl(context, locals, node.arguments[0], limits, depth + 1);
if (!argument_type) {
return argument_type;
}
if (!argument_type->is_integer()) {
return fail(CoreErrorKind::TypeMismatch,
"convert operates on an integer but received " + describe(*argument_type));
}
return Type{node.type};
}
for (std::size_t index = 0; index < node.arguments.size(); ++index) {
const auto& argument = node.arguments[index];
const Type expected = node.op == PrimOp::Select && index == 0 ? Type{kBoolean} : type;
auto argument_type = type_of_impl(context, locals, argument, limits, depth + 1);
if (!argument_type) {
return argument_type;
}
if (!(*argument_type == expected)) {
return fail(CoreErrorKind::TypeMismatch, describe(node.op) + " operates on " +
describe(expected) + " but received " +
describe(*argument_type));
}
}
return is_comparison(node.op) || is_representability(node.op) ? Type{kBoolean} : type;
}
},
term.node);
}
[[nodiscard]] std::expected<Term, CoreError> substitute(const Term& term, const std::vector<Term>& arguments,
const CoreLimits& limits, std::uint32_t depth) {
if (depth > limits.max_term_depth) {
return fail(CoreErrorKind::DepthLimitExceeded, "substitution nests deeper than the core allows");
}
return std::visit(
[&](const auto& node) -> std::expected<Term, CoreError> {
using Node = std::decay_t<decltype(node)>;
if constexpr (std::is_same_v<Node, Var>) {
if (node.index.value >= arguments.size()) {
return fail(CoreErrorKind::VariableOutOfScope, "definition body references variable #" +
std::to_string(node.index.value) +
" which is not one of its parameters");
}
return arguments[arguments.size() - 1 - node.index.value];
} else if constexpr (std::is_same_v<Node, Literal>) {
return Term{node};
} else {
Node replaced = node;
replaced.arguments.clear();
replaced.arguments.reserve(node.arguments.size());
for (const Term& argument : node.arguments) {
auto substituted = substitute(argument, arguments, limits, depth + 1);
if (!substituted) {
return substituted;
}
replaced.arguments.push_back(std::move(*substituted));
}
return Term{std::move(replaced)};
}
},
term.node);
}
[[nodiscard]] std::expected<Term, CoreError> normalize_impl(const Context& context, const Term& term,
const CoreLimits& limits, std::uint64_t& steps,
std::uint32_t depth) {
if (depth > limits.max_term_depth) {
return fail(CoreErrorKind::DepthLimitExceeded, "normalization nests deeper than the core allows");
}
if (steps > limits.max_normalization_steps) {
return fail(CoreErrorKind::NormalizationBudgetExhausted, "normalization exceeded its step budget");
}
return std::visit(
[&](const auto& node) -> std::expected<Term, CoreError> {
using Node = std::decay_t<decltype(node)>;
if constexpr (std::is_same_v<Node, Var> || std::is_same_v<Node, Literal>) {
return Term{node};
} else if constexpr (std::is_same_v<Node, Call>) {
const Definition* definition = context.lookup(node.callee);
if (definition == nullptr) {
return fail(CoreErrorKind::UnknownDefinition,
"def#" + std::to_string(node.callee.value) + " is not defined");
}
if (definition->parameters.size() != node.arguments.size()) {
return fail(CoreErrorKind::ArityMismatch, "def#" + std::to_string(node.callee.value) +
" applied with the wrong number of arguments");
}
std::vector<Term> arguments;
arguments.reserve(node.arguments.size());
for (const Term& argument : node.arguments) {
auto normalized = normalize_impl(context, argument, limits, steps, depth + 1);
if (!normalized) {
return normalized;
}
arguments.push_back(std::move(*normalized));
}
++steps;
auto unfolded = substitute(definition->body, arguments, limits, depth + 1);
if (!unfolded) {
return unfolded;
}
return normalize_impl(context, *unfolded, limits, steps, depth + 1);
} else {
std::vector<Term> arguments;
arguments.reserve(node.arguments.size());
for (const Term& argument : node.arguments) {
auto normalized = normalize_impl(context, argument, limits, steps, depth + 1);
if (!normalized) {
return normalized;
}
arguments.push_back(std::move(*normalized));
}
++steps;
if constexpr (std::is_same_v<Node, Projection>) {
if (!is_supported(node.domain) || !node.domain.is_value() || arguments.size() != 1 ||
node.index >= std::get<ValueType>(node.domain.node).projections.size())
return fail(CoreErrorKind::MalformedPrimitive, "malformed projection");
return Term{Projection{node.domain, node.index, std::move(arguments)}};
} else if constexpr (std::is_same_v<Node, Element>) {
// Normalizing the subject and index is all there is to do:
// the observation is uninterpreted, so it has no reduction
// rule and never selects a component of anything
// (FOUNDATIONS.md 45).
if (!is_supported(node.domain) || !node.domain.is_indexed() || arguments.size() != 2)
return fail(CoreErrorKind::MalformedPrimitive, "malformed element");
return Term{Element{node.domain, std::move(arguments)}};
} else {
return normalize_primitive(node.op, node.type, std::move(arguments), limits, steps);
}
}
},
term.node);
}
std::string describe_with_names(const Context& context, const Term& term) {
return std::visit(
[&](const auto& node) -> std::string {
using Node = std::decay_t<decltype(node)>;
if constexpr (std::is_same_v<Node, Var>) {
return "#" + std::to_string(node.index.value);
} else if constexpr (std::is_same_v<Node, Literal>) {
return describe(node.value);
} else {
std::string text;
if constexpr (std::is_same_v<Node, Call>) {
const Definition* definition = context.lookup(node.callee);
text = definition != nullptr ? definition->name : "def#" + std::to_string(node.callee.value);
} else if constexpr (std::is_same_v<Node, Projection>) {
text = "project[" + describe(node.domain) + "," + std::to_string(node.index) + "]";
} else if constexpr (std::is_same_v<Node, Element>) {
text = "element[" + describe(node.domain) + "]";
} else {
text = describe(node.op);
}
text += "(";
for (std::size_t index = 0; index < node.arguments.size(); ++index) {
if (index != 0) {
text += ", ";
}
text += describe_with_names(context, node.arguments[index]);
}
text += ")";
return text;
}
},
term.node);
}
} // namespace
std::string describe(CoreErrorKind kind) {
switch (kind) {
case CoreErrorKind::DuplicateDefinition:
return "duplicate definition";
case CoreErrorKind::UnknownDefinition:
return "unknown definition";
case CoreErrorKind::ArityMismatch:
return "arity mismatch";
case CoreErrorKind::TypeMismatch:
return "type mismatch";
case CoreErrorKind::VariableOutOfScope:
return "variable out of scope";
case CoreErrorKind::MalformedLiteral:
return "malformed literal";
case CoreErrorKind::MalformedPrimitive:
return "malformed primitive";
case CoreErrorKind::MalformedType:
return "malformed type";
case CoreErrorKind::DepthLimitExceeded:
return "depth limit exceeded";
case CoreErrorKind::NormalizationBudgetExhausted:
return "normalization budget exhausted";
}
return "unknown core error";
}
std::expected<void, CoreError> Context::define(Definition definition) {
if (lookup(definition.id) != nullptr) {
return fail(CoreErrorKind::DuplicateDefinition,
"def#" + std::to_string(definition.id.value) + " is already defined");
}
for (const Type& parameter : definition.parameters) {
if (auto valid = validate_type(parameter); !valid) {
return valid;
}
}
if (auto valid = validate_type(definition.result); !valid) {
return valid;
}
// The body is checked against the context as it stands, which excludes the
// definition being added. A definition therefore cannot call itself or any
// later definition, and the call graph stays acyclic.
const CoreLimits limits{};
auto body_type = type_of_impl(*this, definition.parameters, definition.body, limits, 0);
if (!body_type) {
return std::unexpected(body_type.error());
}
if (!(*body_type == definition.result)) {
return fail(CoreErrorKind::TypeMismatch, "definition '" + definition.name + "' returns " +
describe(*body_type) + " but declares " +
describe(definition.result));
}
definitions_.push_back(std::move(definition));
return {};
}
const Definition* Context::lookup(DefId id) const noexcept {
for (const Definition& definition : definitions_) {
if (definition.id == id) {
return &definition;
}
}
return nullptr;
}
std::expected<Type, CoreError> type_of(const Context& context, std::span<const Type> locals, const Term& term,
const CoreLimits& limits) {
return type_of_impl(context, locals, term, limits, 0);
}
std::expected<Term, CoreError> normalize(const Context& context, const Term& term, const CoreLimits& limits) {
std::uint64_t steps = 0;
return normalize_impl(context, term, limits, steps, 0);
}
std::string describe(const Context& context, const Term& term) {
return describe_with_names(context, term);
}
} // namespace cppl::kernel