max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): add new ^. notation

Browse source 
see #1403
This commit is contained in:
Leonardo de Moura 2017-03-05 20:02:03 -08:00
parent 7cae7a5b02
commit fa99861788
7 changed files with 52 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_exprs.cpp
View file

@ -967,7 +967,7 @@ parse_table init_nud_table() {
static name * g_field_notation_name = nullptr;
static std::string * g_field_notation_opcode = nullptr;
[[ noreturn ]] static void throw_pn_ex() { throw exception("unexpected occurrence of '~>' notation expression"); }
[[ noreturn ]] static void throw_pn_ex() { throw exception("unexpected occurrence of '^.' notation expression"); }
class field_notation_macro_cell : public macro_definition_cell {
name m_field;
@ -1023,7 +1023,7 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
throw parser_error("invalid projection, index must be greater than 0", num_pos);
return p.save_pos(mk_proj_notation(args[0], fidx), pos);
} else {
name field = p.check_id_next("invalid '~>' notation, identifier or numeral expected");
name field = p.check_id_next("invalid '^.' notation, identifier or numeral expected");
return p.save_pos(mk_proj_notation(args[0], field), pos);
}
} catch (break_at_pos_exception & ex) {

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

@ -908,6 +908,8 @@ expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref
if (is_placeholder(fn)) {
throw elaborator_exception(ref, "placeholders '_' cannot be used where a function is expected");
}
if (is_field_notation(fn))
throw elaborator_exception(ref, "invalid occurrence of '^.' notation");
expr r;
switch (fn.kind()) {
case expr_kind::Var:
@ -1795,6 +1797,37 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
}
validate_overloads(fns, ref);
return visit_overloaded_app(fns, args, expected_type, ref);
} else if (is_field_notation(fn) && amask == arg_mask::Default) {
expr s = visit(macro_arg(fn, 0), none_expr());
expr s_type = head_beta_reduce(instantiate_mvars(infer_type(s)));
name full_fname = find_field_fn(fn, s, s_type);
expr proj = copy_tag(fn, mk_constant(full_fname));
name struct_name = full_fname.get_prefix();
expr proj_type = m_env.get(full_fname).get_type();
buffer<expr> new_args;
unsigned i = 0;
while (is_pi(proj_type)) {
if (is_explicit(binding_info(proj_type))) {
if (is_app_of(binding_domain(proj_type), struct_name)) {
/* found s location */
new_args.push_back(copy_tag(fn, mk_as_is(s)));
for (; i < args.size(); i++)
new_args.push_back(args[i]);
expr new_proj = visit(proj, none_expr());
return visit_base_app(new_proj, amask, new_args, expected_type, ref);
} else {
if (i >= args.size()) {
throw elaborator_exception(ref, sstream() << "invalid '^.' notation, insufficient number of arguments for '"
<< full_fname << "'");
}
new_args.push_back(args[i]);
i++;
}
}
proj_type = binding_body(proj_type);
}
throw elaborator_exception(ref, sstream() << "invalid '^.' notation, function '" << full_fname << "' does not have explicit argument with type ("
<< struct_name << " ...)");
} else {
expr new_fn = visit_function(fn, has_args, ref);
/* Check if we should use a custom elaboration procedure for this application. */
@ -2379,7 +2412,7 @@ name elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_ty
expr I = get_app_fn(s_type);
if (!is_constant(I)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(e, format("invalid '~>' notation, type is not of the form (C ...) where C is a constant") +
throw elaborator_exception(e, format("invalid '^.' notation, type is not of the form (C ...) where C is a constant") +
pp_indent(pp_fn, s) +
line() + format("has type") +
pp_indent(pp_fn, s_type));
@ -2410,7 +2443,7 @@ name elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_ty
name full_fname = const_name(I) + fname;
if (!m_env.find(full_fname)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(e, format("invalid '~>' notation, '") + format(fname) + format("'") +
throw elaborator_exception(e, format("invalid '^.' notation, '") + format(fname) + format("'") +
format(" is not a valid \"field\" because environment does not contain ") +
format("'") + format(full_fname) + format("'") +
pp_indent(pp_fn, s) +

11
tests/lean/assertion1.lean.expected.out
View file

@ -1,11 +1,2 @@
assertion1.lean:37:21: error: type mismatch at application
MonoidalCategory.tensorObjects C
term
C
has type
MonoidalCategory
but is expected to have type
?m_1^.Obj
assertion1.lean:37:21: error: function expected at
sorry
assertion1.lean:37:21: error: invalid '^.' notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...)
assertion1.lean:35:11: warning: declaration 'tensor_on_left' uses sorry

4
tests/lean/field_access.lean.expected.out
View file

@ -9,11 +9,11 @@ field_access.lean:7:12: error: invalid projection, structure has only 2 field(s)
which has type
?m_1 × ?m_2
sorry : ?M_1
field_access.lean:10:1: error: invalid '~>' notation, 'forr' is not a valid "field" because environment does not contain 'list.forr'
field_access.lean:10:1: error: invalid '^.' notation, 'forr' is not a valid "field" because environment does not contain 'list.forr'
l
which has type
list ℕ
field_access.lean:13:1: error: invalid '~>' notation, type is not of the form (C ...) where C is a constant
field_access.lean:13:1: error: invalid '^.' notation, type is not of the form (C ...) where C is a constant
a
has type
A

8
tests/lean/interactive/complete_field.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '~>' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '~>' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '~>' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '~>' notation, identifier or numeral expected"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"},"response":"additional_message"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":408},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5}
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":408},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}

2
tests/lean/proj_notation.lean.expected.out
View file

@ -9,7 +9,7 @@ p^.snd : ℕ
f (p^.fst) : ℕ
p^.fst + p^.snd : ℕ
λ (c : car), (c^.pos)^.x : car → ℕ
proj_notation.lean:34:18: error: invalid '~>' notation, 'fst' is not a valid "field" because environment does not contain 'car.fst'
proj_notation.lean:34:18: error: invalid '^.' notation, 'fst' is not a valid "field" because environment does not contain 'car.fst'
c
which has type
car

7
tests/lean/run/new_proj_notation.lean Normal file
View file

@ -0,0 +1,7 @@
variable x : list nat
check x^.map (+1)
check x^.foldl (+) 0
vm_eval [1, 2, 3]^.map (+3)