From fa99861788b4eebbd0e368533869a3a8326e0827 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Mar 2017 20:02:03 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): add new ^. notation see #1403 --- src/frontends/lean/builtin_exprs.cpp | 4 +- src/frontends/lean/elaborator.cpp | 37 ++++++++++++++++++- tests/lean/assertion1.lean.expected.out | 11 +----- tests/lean/field_access.lean.expected.out | 4 +- .../complete_field.lean.expected.out | 8 ++-- tests/lean/proj_notation.lean.expected.out | 2 +- tests/lean/run/new_proj_notation.lean | 7 ++++ 7 files changed, 52 insertions(+), 21 deletions(-) create mode 100644 tests/lean/run/new_proj_notation.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9a8886ef59..c47ed6097f 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7a6a80e1ba..453dd5877d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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 const & args, optional 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) + diff --git a/tests/lean/assertion1.lean.expected.out b/tests/lean/assertion1.lean.expected.out index 0dc7cb9d78..5cb4980b95 100644 --- a/tests/lean/assertion1.lean.expected.out +++ b/tests/lean/assertion1.lean.expected.out @@ -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 diff --git a/tests/lean/field_access.lean.expected.out b/tests/lean/field_access.lean.expected.out index 8364f3997d..68e5968a5e 100644 --- a/tests/lean/field_access.lean.expected.out +++ b/tests/lean/field_access.lean.expected.out @@ -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 diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out index e2cde9123b..ec19306aa5 100644 --- a/tests/lean/interactive/complete_field.lean.expected.out +++ b/tests/lean/interactive/complete_field.lean.expected.out @@ -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} diff --git a/tests/lean/proj_notation.lean.expected.out b/tests/lean/proj_notation.lean.expected.out index 2f70187e93..4a871698f8 100644 --- a/tests/lean/proj_notation.lean.expected.out +++ b/tests/lean/proj_notation.lean.expected.out @@ -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 diff --git a/tests/lean/run/new_proj_notation.lean b/tests/lean/run/new_proj_notation.lean new file mode 100644 index 0000000000..6bafe578e0 --- /dev/null +++ b/tests/lean/run/new_proj_notation.lean @@ -0,0 +1,7 @@ +variable x : list nat + +check x^.map (+1) + +check x^.foldl (+) 0 + +vm_eval [1, 2, 3]^.map (+3)