forked from leanprover/lean4
/
projection.cpp
136 lines (127 loc) · 6.43 KB
/
projection.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
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "runtime/sstream.h"
#include "kernel/kernel_exception.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "kernel/inductive.h"
#include "kernel/instantiate.h"
#include "library/reducible.h"
#include "library/projection.h"
#include "library/util.h"
#include "library/class.h"
#include "library/constructions/projection.h"
#include "library/constructions/util.h"
namespace lean {
[[ noreturn ]] static void throw_ill_formed(name const & n) {
throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype");
}
static bool is_prop(expr type) {
while (is_pi(type)) {
type = binding_body(type);
}
return is_sort(type) && is_zero(sort_level(type));
}
extern "C" object * lean_mk_outparam_args_implicit(object * n);
expr mk_outparam_args_implicit(expr const & type) { return expr(lean_mk_outparam_args_implicit(type.to_obj_arg())); }
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit) {
local_ctx lctx;
name_generator ngen = mk_constructions_name_generator();
constant_info ind_info = env.get(n);
if (!ind_info.is_inductive())
throw exception(sstream() << "projection generation, '" << n << "' is not an inductive datatype");
inductive_val ind_val = ind_info.to_inductive_val();
unsigned nparams = ind_val.get_nparams();
name rec_name = mk_rec_name(n);
if (ind_val.get_nindices() > 0)
throw exception(sstream() << "projection generation, '" << n << "' is an indexed inductive datatype family");
if (length(ind_val.get_cnstrs()) != 1)
throw exception(sstream() << "projection generation, '" << n << "' does not have a single constructor");
constant_info cnstr_info = env.get(head(ind_val.get_cnstrs()));
expr cnstr_type = cnstr_info.get_type();
expr cnstr_type_norm = mk_outparam_args_implicit(cnstr_type);
// The binder inference is quite messy since it is using `mk_outparam_args_implicit` and `infer_implicit_params`.
// TODO: cleanup
bool is_predicate = is_prop(ind_info.get_type());
names lvl_params = ind_info.get_lparams();
levels lvls = lparams_to_levels(lvl_params);
buffer<expr> params; // datatype parameters
expr cnstr_type_orig = cnstr_type; // we use the original type before `mk_outparam_args_implicit` to get the original binder info
for (unsigned i = 0; i < nparams; i++) {
if (!is_pi(cnstr_type_norm))
throw_ill_formed(n);
lean_assert(is_pi(cnstr_type_orig));
auto bi = binding_info(cnstr_type_norm);
auto bi_orig = binding_info(cnstr_type_orig);
auto type = binding_domain(cnstr_type_norm);
auto type_orig = binding_domain(cnstr_type_orig);
if (!is_inst_implicit(bi_orig) && !is_class_out_param(type_orig)) {
// We reset implicit binders in favor of having them inferred by `infer_implicit_params` later IF
// 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit.
// 2. It is not originally an outparam. Outparams must be implicit.
bi = mk_binder_info();
}
expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type_norm), type, bi);
cnstr_type_norm = instantiate(binding_body(cnstr_type_norm), param);
cnstr_type_orig = binding_body(cnstr_type_orig);
params.push_back(param);
}
expr C_A = mk_app(mk_constant(n, lvls), params);
binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info();
expr c = lctx.mk_local_decl(ngen, name("self"), C_A, c_bi);
buffer<expr> cnstr_type_args; // arguments that are not parameters
expr it = cnstr_type_norm;
while (is_pi(it)) {
expr local = lctx.mk_local_decl(ngen, binding_name(it), binding_domain(it), binding_info(it));
cnstr_type_args.push_back(local);
it = instantiate(binding_body(it), local);
}
unsigned i = 0;
environment new_env = env;
for (name const & proj_name : proj_names) {
if (!is_pi(cnstr_type_norm))
throw exception(sstream() << "generating projection '" << proj_name << "', '"
<< n << "' does not have sufficient data");
expr result_type = consume_type_annotations(binding_domain(cnstr_type_norm));
if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
<< "type is an inductive predicate, but field is not a proposition");
}
buffer<expr> proj_args;
proj_args.append(params);
proj_args.push_back(c);
expr proj_type = lctx.mk_pi(proj_args, result_type);
proj_type = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit);
expr proj_val = mk_proj(n, i, c);
proj_val = lctx.mk_lambda(proj_args, proj_val);
declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
reducibility_hints::mk_abbreviation());
new_env = new_env.add(new_d);
if (!inst_implicit)
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);
new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit);
expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
cnstr_type_norm = instantiate(binding_body(cnstr_type_norm), proj);
i++;
}
return new_env;
}
extern "C" LEAN_EXPORT object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) {
environment new_env(env);
name n(struct_name);
list_ref<name> ps(proj_infos);
buffer<name> proj_names;
for (auto p : ps) {
proj_names.push_back(p);
}
return catch_kernel_exceptions<environment>([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); });
}
void initialize_def_projection() {
}
void finalize_def_projection() {
}
}