/
environment.cpp
272 lines (238 loc) · 9.92 KB
/
environment.cpp
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
/*
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <vector>
#include <limits>
#include <lean/sstream.h>
#include <lean/thread.h>
#include "util/map_foreach.h"
#include "util/io.h"
#include "kernel/environment.h"
#include "kernel/kernel_exception.h"
#include "kernel/type_checker.h"
#include "kernel/quot.h"
namespace lean {
extern "C" object* lean_environment_add(object*, object*);
extern "C" object* lean_mk_empty_environment(uint32, object*);
extern "C" object* lean_environment_find(object*, object*);
extern "C" uint32 lean_environment_trust_level(object*);
extern "C" object* lean_environment_mark_quot_init(object*);
extern "C" uint8 lean_environment_quot_init(object*);
extern "C" object* lean_register_extension(object*);
extern "C" object* lean_get_extension(object*, object*);
extern "C" object* lean_set_extension(object*, object*, object*);
extern "C" object* lean_environment_set_main_module(object*, object*);
extern "C" object* lean_environment_main_module(object*);
environment mk_empty_environment(uint32 trust_lvl) {
return get_io_result<environment>(lean_mk_empty_environment(trust_lvl, io_mk_world()));
}
environment::environment(unsigned trust_lvl):
object_ref(mk_empty_environment(trust_lvl)) {
}
void environment::set_main_module(name const & n) {
m_obj = lean_environment_set_main_module(m_obj, n.to_obj_arg());
}
name environment::get_main_module() const {
return name(lean_environment_main_module(to_obj_arg()));
}
unsigned environment::trust_lvl() const {
return lean_environment_trust_level(to_obj_arg());
}
bool environment::is_quot_initialized() const {
return lean_environment_quot_init(to_obj_arg()) != 0;
}
void environment::mark_quot_initialized() {
m_obj = lean_environment_mark_quot_init(m_obj);
}
optional<constant_info> environment::find(name const & n) const {
return to_optional<constant_info>(lean_environment_find(to_obj_arg(), n.to_obj_arg()));
}
constant_info environment::get(name const & n) const {
object * o = lean_environment_find(to_obj_arg(), n.to_obj_arg());
if (is_scalar(o))
throw unknown_constant_exception(*this, n);
constant_info r(cnstr_get(o, 0), true);
dec(o);
return r;
}
static void check_no_metavar(environment const & env, name const & n, expr const & e) {
if (has_metavar(e))
throw declaration_has_metavars_exception(env, n, e);
}
static void check_no_fvar(environment const & env, name const & n, expr const & e) {
if (has_fvar(e))
throw declaration_has_free_vars_exception(env, n, e);
}
void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e) {
check_no_metavar(env, n, e);
check_no_fvar(env, n, e);
}
static void check_name(environment const & env, name const & n) {
if (env.find(n))
throw already_declared_exception(env, n);
}
void environment::check_name(name const & n) const {
::lean::check_name(*this, n);
}
static void check_duplicated_univ_params(environment const & env, names ls) {
while (!is_nil(ls)) {
auto const & p = head(ls);
ls = tail(ls);
if (std::find(ls.begin(), ls.end(), p) != ls.end()) {
throw kernel_exception(env, sstream() << "failed to add declaration to environment, "
<< "duplicate universe level parameter: '"
<< p << "'");
}
}
}
void environment::check_duplicated_univ_params(names ls) const {
::lean::check_duplicated_univ_params(*this, ls);
}
static void check_constant_val(environment const & env, constant_val const & v, type_checker & checker) {
check_name(env, v.get_name());
check_duplicated_univ_params(env, v.get_lparams());
check_no_metavar_no_fvar(env, v.get_name(), v.get_type());
expr sort = checker.check(v.get_type(), v.get_lparams());
checker.ensure_sort(sort, v.get_type());
}
static void check_constant_val(environment const & env, constant_val const & v, bool safe_only) {
type_checker checker(env, safe_only);
check_constant_val(env, v, checker);
}
void environment::add_core(constant_info const & info) {
m_obj = lean_environment_add(m_obj, info.to_obj_arg());
}
environment environment::add(constant_info const & info) const {
return environment(lean_environment_add(to_obj_arg(), info.to_obj_arg()));
}
environment environment::add_axiom(declaration const & d, bool check) const {
axiom_val const & v = d.to_axiom_val();
if (check)
check_constant_val(*this, v.to_constant_val(), !d.is_unsafe());
return add(constant_info(d));
}
environment environment::add_definition(declaration const & d, bool check) const {
definition_val const & v = d.to_definition_val();
if (v.is_unsafe()) {
/* Meta definition can be recursive.
So, we check the header, add, and then type check the body. */
if (check) {
bool safe_only = false;
type_checker checker(*this, safe_only);
check_constant_val(*this, v.to_constant_val(), checker);
}
environment new_env = add(constant_info(d));
if (check) {
bool safe_only = false;
type_checker checker(new_env, safe_only);
check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(new_env, d, val_type);
}
return new_env;
} else {
if (check) {
type_checker checker(*this);
check_constant_val(*this, v.to_constant_val(), checker);
check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return add(constant_info(d));
}
}
environment environment::add_theorem(declaration const & d, bool check) const {
theorem_val const & v = d.to_theorem_val();
if (check) {
// TODO(Leo): we must add support for handling tasks here
type_checker checker(*this);
check_constant_val(*this, v.to_constant_val(), checker);
check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return add(constant_info(d));
}
environment environment::add_opaque(declaration const & d, bool check) const {
opaque_val const & v = d.to_opaque_val();
if (check) {
type_checker checker(*this);
check_constant_val(*this, v.to_constant_val(), checker);
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(*this, d, val_type);
}
return add(constant_info(d));
}
environment environment::add_mutual(declaration const & d, bool check) const {
definition_vals const & vs = d.to_definition_vals();
if (empty(vs))
throw kernel_exception(*this, "invalid empty mutual definition");
definition_safety safety = head(vs).get_safety();
if (safety == definition_safety::safe)
throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as unsafe/partial");
bool safe_only = safety == definition_safety::partial;
/* Check declarations header */
if (check) {
type_checker checker(*this, safe_only);
for (definition_val const & v : vs) {
if (v.get_safety() != safety)
throw kernel_exception(*this, "invalid mutual definition, declarations must have the same safety annotation");
check_constant_val(*this, v.to_constant_val(), checker);
}
}
/* Add declarations */
environment new_env = *this;
for (definition_val const & v : vs) {
new_env.add_core(constant_info(v));
}
/* Check actual definitions */
if (check) {
type_checker checker(new_env, safe_only);
for (definition_val const & v : vs) {
check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(new_env, d, val_type);
}
}
return new_env;
}
environment environment::add(declaration const & d, bool check) const {
switch (d.kind()) {
case declaration_kind::Axiom: return add_axiom(d, check);
case declaration_kind::Definition: return add_definition(d, check);
case declaration_kind::Theorem: return add_theorem(d, check);
case declaration_kind::Opaque: return add_opaque(d, check);
case declaration_kind::MutualDefinition: return add_mutual(d, check);
case declaration_kind::Quot: return add_quot();
case declaration_kind::Inductive: return add_inductive(d);
}
lean_unreachable();
}
extern "C" object * lean_add_decl(object * env, object * decl) {
return catch_kernel_exceptions<environment>([&]() {
return environment(env).add(declaration(decl, true));
});
}
void environment::for_each_constant(std::function<void(constant_info const & d)> const & f) const {
smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) {
constant_info cinfo(v, true);
f(cinfo);
});
}
extern "C" obj_res lean_display_stats(obj_arg env, obj_arg w);
void environment::display_stats() const {
dec_ref(lean_display_stats(to_obj_arg(), io_mk_world()));
}
void initialize_environment() {
}
void finalize_environment() {
}
}