-
Notifications
You must be signed in to change notification settings - Fork 335
/
inductive.h
145 lines (132 loc) · 6.67 KB
/
inductive.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
/*
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
#include "kernel/instantiate.h"
namespace lean {
/** \brief Return recursor name for the given inductive datatype name */
name mk_rec_name(name const & I);
bool is_inductive(environment const & env, name const & n);
bool is_constructor(environment const & env, name const & n);
bool is_recursor(environment const & env, name const & n);
/** \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 Return true if the given declaration is a structure */
bool is_structure_like(environment const & env, name const & decl_name);
/* Auxiliary function for to_cnstr_when_K */
optional<expr> mk_nullary_cnstr(environment const & env, expr const & type, unsigned num_params);
/* For datatypes that support K-axiom, given `e` an element of that type, we convert (if possible)
to the default constructor. For example, if `e : a = a`, then this method returns `eq.refl a` */
template<typename WHNF, typename INFER, typename IS_DEF_EQ>
inline expr to_cnstr_when_K(environment const & env, recursor_val const & rval, expr const & e,
WHNF const & whnf, INFER const & infer_type, IS_DEF_EQ const & is_def_eq) {
lean_assert(rval.is_k());
expr app_type = whnf(infer_type(e));
expr const & app_type_I = get_app_fn(app_type);
if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_induct()) return e; // type incorrect
if (has_expr_mvar(app_type)) {
buffer<expr> app_type_args;
get_app_args(app_type, app_type_args);
for (unsigned i = rval.get_nparams(); i < app_type_args.size(); i++) {
if (has_expr_metavar(app_type_args[i]))
return e;
}
}
optional<expr> new_cnstr_app = mk_nullary_cnstr(env, app_type, rval.get_nparams());
if (!new_cnstr_app) return e;
expr new_type = infer_type(*new_cnstr_app);
if (!is_def_eq(app_type, new_type)) return e;
return *new_cnstr_app;
}
optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major);
expr nat_lit_to_constructor(expr const & e);
expr string_lit_to_constructor(expr const & e);
/* Auxiliary method for \c to_cnstr_when_structure, convert `e` into `mk e.1 ... e.n` */
expr expand_eta_struct(environment const & env, expr const & e_type, expr const & e);
/* If `e` is not a constructor application and its type `C ...` is a structure, return `C.mk e.1 ... e.n`,
where `C.mk` is `C`s constructor. */
template<typename WHNF, typename INFER>
inline expr to_cnstr_when_structure(environment const & env, name const & induct_name, expr const & e,
WHNF const & whnf, INFER const & infer_type) {
if (!is_structure_like(env, induct_name) || is_constructor_app(env, e))
return e;
expr e_type = whnf(infer_type(e));
if (!is_constant(get_app_fn(e_type), induct_name))
return e;
if (whnf(infer_type(e_type)) == mk_Prop())
return e;
return expand_eta_struct(env, e_type, e);
}
template<typename WHNF, typename INFER, typename IS_DEF_EQ>
inline optional<expr> inductive_reduce_rec(environment const & env, expr const & e,
WHNF const & whnf, INFER const & infer_type, IS_DEF_EQ const & is_def_eq) {
expr const & rec_fn = get_app_fn(e);
if (!is_constant(rec_fn)) return none_expr();
optional<constant_info> rec_info = env.find(const_name(rec_fn));
if (!rec_info || !rec_info->is_recursor()) return none_expr();
buffer<expr> rec_args;
get_app_args(e, rec_args);
recursor_val const & rec_val = rec_info->to_recursor_val();
unsigned major_idx = rec_val.get_major_idx();
if (major_idx >= rec_args.size()) return none_expr(); // major premise is missing
expr major = rec_args[major_idx];
if (rec_val.is_k()) {
major = to_cnstr_when_K(env, rec_val, major, whnf, infer_type, is_def_eq);
}
major = whnf(major);
if (is_nat_lit(major))
major = nat_lit_to_constructor(major);
else if (is_string_lit(major))
major = string_lit_to_constructor(major);
else
major = to_cnstr_when_structure(env, rec_val.get_induct(), major, whnf, infer_type);
optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
if (!rule) return none_expr();
buffer<expr> major_args;
get_app_args(major, major_args);
if (rule->get_nfields() > major_args.size()) return none_expr();
if (length(const_levels(rec_fn)) != length(rec_info->get_lparams())) return none_expr();
expr rhs = instantiate_lparams(rule->get_rhs(), rec_info->get_lparams(), const_levels(rec_fn));
/* apply parameters, motives and minor premises from recursor application. */
rhs = mk_app(rhs, rec_val.get_nparams() + rec_val.get_nmotives() + rec_val.get_nminors(), rec_args.data());
/* The number of parameters in the constructor is not necessarily
equal to the number of parameters in the recursor when we have
nested inductive types. */
unsigned nparams = major_args.size() - rule->get_nfields();
/* apply fields from major premise */
rhs = mk_app(rhs, rule->get_nfields(), major_args.data() + nparams);
if (rec_args.size() > major_idx + 1) {
/* recursor application has more arguments after major premise */
unsigned nextra = rec_args.size() - major_idx - 1;
rhs = mk_app(rhs, nextra, rec_args.data() + major_idx + 1);
}
return some_expr(rhs);
}
template<typename WHNF, typename IS_STUCK>
optional<expr> inductive_is_stuck(environment const & env, expr const & e, WHNF const & whnf, IS_STUCK const & is_stuck) {
expr const & rec_fn = get_app_fn(e);
if (!is_constant(rec_fn)) return none_expr();
optional<constant_info> rec_info = env.find(const_name(rec_fn));
if (!rec_info || !rec_info->is_recursor()) return none_expr();
buffer<expr> rec_args;
get_app_args(e, rec_args);
recursor_val const & rec_val = rec_info->to_recursor_val();
unsigned major_idx = rec_val.get_major_idx();
if (rec_args.size() < major_idx + 1) return none_expr();
expr cnstr_app = whnf(rec_args[major_idx]);
if (rec_val.is_k()) {
/* TODO(Leo): make it more precise. Remark: this piece of
code does not affect the correctness of the kernel, but the
effectiveness of the elaborator. */
return none_expr();
} else {
return is_stuck(cnstr_app);
}
}
void initialize_inductive();
void finalize_inductive();
}