-
Notifications
You must be signed in to change notification settings - Fork 350
/
util.h
321 lines (243 loc) · 13.9 KB
/
util.h
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
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "kernel/environment.h"
#include "library/expr_pair.h"
namespace lean {
/* If \c n is not in \c env, then return \c. Otherwise, find the first j >= idx s.t.
n.append_after(j) is not in \c env. */
name mk_unused_name(environment const & env, name const & n, unsigned & idx);
/* If \c n is not in \c env, then return \c. Otherwise, find the first j >= 1 s.t.
n.append_after(j) is not in \c env. */
name mk_unused_name(environment const & env, name const & n);
/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
unsigned get_arity(expr type);
optional<expr> is_optional_param(expr const & e);
optional<expr_pair> is_auto_param(expr const & e);
/** \brief Return the universe level of the type of \c A.
Throws an exception if the (relaxed) whnf of the type
of A is not a sort. */
level get_level(abstract_type_context & ctx, expr const & A);
/** brief Return a name that does not appear in `lp_names`. */
name mk_fresh_lp_name(names const & lp_names);
/** \brief Return true iff \c n occurs in \c m */
bool occurs(expr const & n, expr const & m);
/** \brief Return true iff there is a constant named \c n in \c m. */
bool occurs(name const & n, expr const & m);
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
bool is_app_of(expr const & t, name const & f_name);
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
/** \brief If type is of the form (auto_param A p) or (opt_param A v), return A. Otherwise, return type. */
expr consume_auto_opt_param(expr const & type);
/** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
where \c f is a constant */
optional<expr> unfold_term(environment const & env, expr const & e);
/** \brief If \c e is of the form <tt>(f a_1 ... a_n)</tt>, where \c f is
a non-opaque definition, then unfold \c f, and beta reduce.
Otherwise, return none. */
optional<expr> unfold_app(environment const & env, expr const & e);
/** \brief Reduce (if possible) universe level by 1.
\pre is_not_zero(l) */
optional<level> dec_level(level const & l);
bool has_punit_decls(environment const & env);
bool has_pprod_decls(environment const & env);
bool has_eq_decls(environment const & env);
bool has_heq_decls(environment const & env);
bool has_and_decls(environment const & env);
inline bool is_inductive(environment const & env, name const & n) {
if (optional<constant_info> info = env.find(n))
return info->is_inductive();
return false;
}
inline bool is_constructor(environment const & env, name const & n) {
if (optional<constant_info> info = env.find(n))
return info->is_constructor();
return false;
}
inline bool is_recursor(environment const & env, name const & n) {
if (optional<constant_info> info = env.find(n))
return info->is_recursor();
return false;
}
/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
That is, it must be an inductive datatype AND contain a recursive constructor.
\remark Records are inductive datatypes, but they are not recursive.
\remark For mutually indutive datatypes, \c n is considered recursive
if there is a constructor taking \c n. */
bool is_recursive_datatype(environment const & env, name const & n);
/** \brief Return true iff \c n is an inductive predicate, i.e., an inductive datatype that is in Prop.
\remark If \c env does not have Prop (i.e., Type.{0} is not impredicative), then this method always return false. */
bool is_inductive_predicate(environment const & env, name const & n);
/** \brief Return true iff \c n is an inductive type with a recursor with an extra level parameter. */
bool can_elim_to_type(environment const & env, name const & n);
/** \brief Store in `result` the constructors of the given inductive datatype.
\remark this procedure does nothing if `n` is not an inductive datatype. */
void get_constructor_names(environment const & env, name const & n, buffer<name> & result);
/** \brief If \c e is a constructor application, then return the name of the constructor.
Otherwise, return none. */
optional<name> is_constructor_app(environment const & env, expr const & e);
/** \brief If \c e is a constructor application, or a definition that wraps a
constructor application, then return the name of the constructor.
Otherwise, return none. */
optional<name> is_constructor_app_ext(environment const & env, expr const & e);
/** \brief Store in \c result a bit-vector indicating which fields of the constructor \c n are
(computationally) relevant.
\pre inductive::is_intro_rule(env, n) */
void get_constructor_relevant_fields(environment const & env, name const & n, buffer<bool> & result);
/** Return the number of constructors of the given inductive datatype */
unsigned get_num_constructors(environment const & env, name const & n);
/** \brief Return the index (position) of the given constructor in the inductive datatype declaration.
\pre inductive::is_intro_rule(env, n) */
unsigned get_constructor_idx(environment const & env, name const & n);
/** \brief Given an expression \c e, return the number of arguments expected arguments.
\remark This function counts the number of nested Pi's in \c e. Weak-head-normal-forms are computed for the type of \c e.
\remark The type and whnf are computed using \c tc. */
unsigned get_expect_num_args(abstract_type_context & ctx, expr e);
/** \brief Return the universe where inductive datatype resides
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt> */
level get_datatype_level(expr const & ind_type);
/** \brief "Consume" Pi-type `type`. This procedure creates free variables based on the domain of `type` using `lctx`,
and store them in telescope and updates . If `binfo` is provided, then the free variables are annotated with
the given `binder_info`, otherwise the procedure uses the one attached in the domain.
The procedure returns the "body" of type. */
expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer<expr> & telescope, optional<binder_info> const & binfo = optional<binder_info>());
/** \brief Similar to previous procedure, but uses whnf to check whether `type` reduces to `Pi` or not. */
expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo = optional<binder_info>());
/** \brief Update the result sort of the given type */
expr update_result_sort(expr t, level const & l);
expr instantiate_lparam (expr const & e, name const & p, level const & l);
expr mk_true();
bool is_true(expr const & e);
expr mk_true_intro();
bool is_and(expr const & e, expr & arg1, expr & arg2);
bool is_and(expr const & e);
expr mk_and(expr const & a, expr const & b);
expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb);
expr mk_and_elim_left(abstract_type_context & ctx, expr const & H);
expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
expr mk_unit(level const & l);
expr mk_unit_mk(level const & l);
expr mk_unit();
expr mk_unit_mk();
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p);
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p);
expr mk_unit(level const & l, bool prop);
expr mk_unit_mk(level const & l, bool prop);
expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop);
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop);
expr mk_nat_type();
bool is_nat_type(expr const & e);
expr mk_nat_zero();
expr mk_nat_one();
expr mk_nat_bit0(expr const & e);
expr mk_nat_bit1(expr const & e);
expr mk_nat_add(expr const & e1, expr const & e2);
expr mk_int_type();
bool is_int_type(expr const & e);
expr mk_char_type();
bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f);
bool is_ite(expr const & e);
bool is_iff(expr const & e);
bool is_iff(expr const & e, expr & lhs, expr & rhs);
expr mk_iff(expr const & lhs, expr const & rhs);
expr mk_iff_refl(expr const & a);
expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr);
expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
expr mk_eq_refl(abstract_type_context & ctx, expr const & a);
expr mk_eq_symm(abstract_type_context & ctx, expr const & H);
expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2);
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
expr const & x, expr const & y, expr const & xeqy, expr const & h);
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h);
expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H);
/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) */
expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y);
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
bool is_eq_rec_core(expr const & e);
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
bool is_eq_rec(expr const & e);
/** \brief Return true iff \c e is a term of the form (eq.drec ....) */
bool is_eq_drec(expr const & e);
bool is_eq(expr const & e);
bool is_eq(expr const & e, expr & lhs, expr & rhs);
bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
/** \brief Return true iff \c e is of the form (eq A a a) */
bool is_eq_a_a(expr const & e);
/** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
bool is_eq_a_a(abstract_type_context & ctx, expr const & e);
expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
bool is_heq(expr const & e);
bool is_heq(expr const & e, expr & lhs, expr & rhs);
bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
expr mk_cast(abstract_type_context & ctx, expr const & H, expr const & e);
expr mk_false();
expr mk_empty();
bool is_false(expr const & e);
bool is_empty(expr const & e);
/** \brief Return an element of type t given an element \c f : false */
expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t);
bool is_or(expr const & e);
bool is_or(expr const & e, expr & A, expr & B);
/** \brief Return true if \c e is of the form <tt>(not arg)</tt> or <tt>arg -> false</tt>, and store \c arg in \c a.
Return false otherwise */
bool is_not(expr const & e, expr & a);
inline bool is_not(expr const & e) { expr a; return is_not(e, a); }
/** \brief Extends is_not to handle (lhs ≠ rhs). In the new case, it stores (lhs = rhs) in \c a. */
bool is_not_or_ne(expr const & e, expr & a);
expr mk_not(expr const & e);
/** \brief Create the term <tt>absurd e not_e : t</tt>. */
expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e);
/** \brief Returns none if \c e is not an application with at least two arguments.
Otherwise it returns <tt>app_fn(app_fn(e))</tt>. */
optional<expr> get_binary_op(expr const & e);
optional<expr> get_binary_op(expr const & e, expr & arg1, expr & arg2);
/** \brief Makes n-ary (right-associative) application. */
expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
expr mk_bool();
expr mk_bool_true();
expr mk_bool_false();
expr to_bool_expr(bool b);
/* Similar to is_head_beta, but ignores annotations around the function. */
bool is_annotated_head_beta(expr const & t);
/* Similar to head_beta_reduce, but also reduces annotations around the function. */
expr annotated_head_beta_reduce(expr const & t);
bool is_exists(expr const & e, expr & A, expr & p);
bool is_exists(expr const & e);
expr try_eta(expr const & e);
expr beta_reduce(expr t);
expr eta_reduce(expr t);
expr beta_eta_reduce(expr t);
enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
/** \brief Infer implicit parameter annotations for the first \c nparams using mode
specified by \c k. */
expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
/** Given an inductive datatype named \c n, return a recursor for \c n that supports dependent elimination
even if \c n is an inductive predicate. */
name get_dep_recursor(environment const & env, name const & n);
/** Given an inductive datatype named \c n, return a cases_on recursor \c n that supports dependent elimination
even if \c n is an inductive predicate. */
name get_dep_cases_on(environment const & env, name const & n);
/** We generate auxiliary unsafe definitions for regular recursive definitions.
The auxiliary unsafe definition has a clear runtime cost execution model, and
we use it in the VM and code generators. This function returns an auxiliary unsafe definition for the given name. */
name mk_unsafe_rec_name(name const & n);
/** Return some(n') if \c n is a name created using mk_unsafe_rec_name(n') */
optional<name> is_unsafe_rec_name(name const & n);
/** Convert an expression representing a `name` literal into a `name` object. */
optional<name> name_lit_to_name(expr const & name_lit);
std::string const & get_version_string();
expr const & extract_mdata(expr const &);
optional<expr> to_optional_expr(obj_arg o);
void initialize_library_util();
void finalize_library_util();
}