michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): display type of binders, closes #238

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-08 22:54:10 -07:00
parent 25fd370c51
commit 8947bf4347
10 changed files with 149 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/elaborator.cpp
View file

@ -129,6 +129,15 @@ void elaborator::save_type_data(expr const & e, expr const & r) {
}
}
/** \brief Store the pair (pos(e), r) in the info_data if m_info_manager is available. */
void elaborator::save_binder_type(expr const & e, expr const & r) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e)) {
m_pre_info_data.add_type_info(p->first, p->second, r);
}
}
}
/** \brief Store type information at pos(e) for r if \c e is marked as "extra" in the info_manager */
void elaborator::save_extra_type_data(expr const & e, expr const & r) {
if (!m_no_info && infom() && pip()) {
@ -646,9 +655,14 @@ expr elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) {
buffer<expr> ds, ls, es;
while (e.kind() == k) {
es.push_back(e);
expr d = binding_domain(e);
expr const & d0 = binding_domain(e);
expr d = d0;
d = instantiate_rev_locals(d, ls.size(), ls.data());
d = ensure_type(visit_expecting_type(d, cs), cs);
if (is_placeholder(d0) && !is_explicit_placeholder(d0))
save_binder_type(d0, d);
ds.push_back(d);
expr l = mk_local(binding_name(e), d, binding_info(e));
if (binding_info(e).is_contextual())

1
src/frontends/lean/elaborator.h
View file

@ -76,6 +76,7 @@ class elaborator : public coercion_info_manager {
optional<expr> mvar_to_meta(expr const & mvar);
void save_type_data(expr const & e, expr const & r);
void save_binder_type(expr const & e, expr const & r);
void save_extra_type_data(expr const & e, expr const & r);
void save_identifier_info(expr const & f);
void save_synth_data(expr const & e, expr const & r);

2
src/frontends/lean/parser.cpp
View file

@ -749,6 +749,7 @@ expr parser::parse_binder_core(binder_info const & bi) {
} else {
type = save_pos(mk_expr_placeholder(), p);
}
save_identifier_info(p, id);
return save_pos(mk_local(id, type, bi), p);
}
@ -782,6 +783,7 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
}
for (auto p : names) {
expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
save_identifier_info(p.first, p.second);
expr local = save_pos(mk_local(p.second, arg_type, bi), p.first);
add_local(local);
r.push_back(local);

12
tests/lean/interactive/eq2.input.expected.out
View file

@ -11,6 +11,9 @@
-- SYMBOL|134|3
λ
-- ACK
-- IDENTIFIER|134|6
b₂
-- ACK
-- TYPE|134|11
A → Type
-- ACK
@ -23,6 +26,9 @@ A
-- IDENTIFIER|134|13
a₁
-- ACK
-- IDENTIFIER|134|18
H₂
-- ACK
-- TYPE|134|23
B a₁
-- ACK
@ -41,6 +47,9 @@ B a₁
-- IDENTIFIER|134|28
b₂
-- ACK
-- IDENTIFIER|134|33
c₂
-- ACK
-- TYPE|134|38
Π (a : A), B a → Type
-- ACK
@ -59,6 +68,9 @@ B a₁
-- IDENTIFIER|134|43
b₂
-- ACK
-- IDENTIFIER|134|48
H₃
-- ACK
-- TYPE|134|53
C a₁ b₂
-- ACK

60
tests/lean/interactive/in1.input.expected.out
View file

@ -1,15 +1,27 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|4|16
A
-- ACK
-- IDENTIFIER|4|18
B
-- ACK
-- SYMBOL|4|22
Type
-- ACK
-- IDENTIFIER|4|29
a
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- IDENTIFIER|4|37
b
-- ACK
-- TYPE|4|41
Type
-- ACK
@ -26,15 +38,27 @@ a
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|4|16
A
-- ACK
-- IDENTIFIER|4|18
B
-- ACK
-- SYMBOL|4|22
Type
-- ACK
-- IDENTIFIER|4|29
a
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- IDENTIFIER|4|37
b
-- ACK
-- TYPE|4|41
Type
-- ACK
@ -51,15 +75,27 @@ b
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|5|16
A
-- ACK
-- IDENTIFIER|5|18
B
-- ACK
-- SYMBOL|5|22
Type
-- ACK
-- IDENTIFIER|5|29
a
-- ACK
-- TYPE|5|33
Type
-- ACK
-- IDENTIFIER|5|33
A
-- ACK
-- IDENTIFIER|5|37
b
-- ACK
-- TYPE|5|41
Type
-- ACK
@ -76,15 +112,27 @@ b
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|4|16
A
-- ACK
-- IDENTIFIER|4|18
B
-- ACK
-- SYMBOL|4|22
Type
-- ACK
-- IDENTIFIER|4|29
a
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- IDENTIFIER|4|37
b
-- ACK
-- TYPE|4|41
Type
-- ACK
@ -103,15 +151,27 @@ b
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|4|16
A
-- ACK
-- IDENTIFIER|4|18
B
-- ACK
-- SYMBOL|4|22
Type
-- ACK
-- IDENTIFIER|4|29
a
-- ACK
-- TYPE|4|33
Type
-- ACK
-- IDENTIFIER|4|33
A
-- ACK
-- IDENTIFIER|4|37
b
-- ACK
-- TYPE|4|41
Type
-- ACK

3
tests/lean/interactive/missing.input.expected.out
View file

@ -7,6 +7,9 @@ have
-- SYMBOL|10|15
∀
-- ACK
-- IDENTIFIER|10|18
t
-- ACK
-- TYPE|10|22
Type → Type
-- ACK

9
tests/lean/interactive/sync.input.expected.out
View file

@ -5,9 +5,18 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- IDENTIFIER|3|16
A
-- ACK
-- SYMBOL|3|20
Type
-- ACK
-- IDENTIFIER|3|27
a
-- ACK
-- IDENTIFIER|3|29
b
-- ACK
-- TYPE|3|33
Type
-- ACK

3
tests/lean/interactive/t4.input.expected.out
View file

@ -13,6 +13,9 @@ epsilon
-- SYMBOL|6|15
λ
-- ACK
-- IDENTIFIER|6|17
x
-- ACK
-- TYPE|6|21
Type
-- ACK

7
tests/lean/interactive/var.input Normal file
View file

@ -0,0 +1,7 @@
VISIT foo.lean
SYNC 3
import data.prod
open prod
definition foo A := λB, A × B
WAIT
INFO 3

37
tests/lean/interactive/var.input.expected.out Normal file
View file

@ -0,0 +1,37 @@
-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- TYPE|3|15
Type
-- ACK
-- IDENTIFIER|3|15
A
-- ACK
-- SYMBOL|3|20
λ
-- ACK
-- TYPE|3|21
Type
-- ACK
-- IDENTIFIER|3|21
B
-- ACK
-- TYPE|3|24
Type
-- ACK
-- IDENTIFIER|3|24
A
-- ACK
-- TYPE|3|26
Type → Type → Type
-- ACK
-- SYMBOL|3|26
×
-- ACK
-- TYPE|3|28
Type
-- ACK
-- IDENTIFIER|3|28
B
-- ACK
-- ENDINFO