From b5acbb222893264a6002dbd90e966f3fab92feb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Mar 2015 17:10:30 -0700 Subject: [PATCH] fix(frontends/lean/pp): missing parenthesis around abbreviations fixes #476 --- src/frontends/lean/pp.cpp | 12 ++++++------ src/frontends/lean/pp.h | 2 +- src/shell/CMakeLists.txt | 9 +++++++++ tests/lean/abbrev_paren.hlean | 5 +++++ tests/lean/abbrev_paren.hlean.expected.out | 7 +++++++ tests/lean/test_single.sh | 10 +++++++++- 6 files changed, 37 insertions(+), 8 deletions(-) create mode 100644 tests/lean/abbrev_paren.hlean create mode 100644 tests/lean/abbrev_paren.hlean.expected.out diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 4aad0d09c..b68c9cf8c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -364,11 +364,11 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result { if (auto it = is_abbreviated(e)) - return pp_abbreviation(e, *it, false, ignore_hide); + return pp_abbreviation(e, *it, false, bp, ignore_hide); if (is_app(e)) { expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { - return pp_abbreviation(e, *it, true, ignore_hide); + return pp_abbreviation(e, *it, true, bp, ignore_hide); } else if (is_implicit(f)) { return pp_child(f, bp, ignore_hide); } else if (!m_coercion && is_coercion(m_env, f)) { @@ -822,11 +822,11 @@ static unsigned get_some_precedence(token_table const & t, name const & tk) { auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result { if (auto it = is_abbreviated(e)) - return pp_abbreviation(e, *it, false); + return pp_abbreviation(e, *it, false, rbp); if (is_app(e)) { expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { - return pp_abbreviation(e, *it, true); + return pp_abbreviation(e, *it, true, rbp); } else if (is_implicit(f)) { return pp_notation_child(f, lbp, rbp); } else if (!m_coercion && is_coercion(m_env, f)) { @@ -1067,7 +1067,7 @@ auto pretty_fn::pp_notation(expr const & e) -> optional { return optional(); } -auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide) -> result { +auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, unsigned bp, bool ignore_hide) -> result { declaration const & d = m_env.get(abbrev); unsigned num_univs = d.get_num_univ_params(); buffer ls; @@ -1076,7 +1076,7 @@ auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, bo buffer args; if (fn) get_app_args(e, args); - return pp(mk_app(mk_constant(abbrev, to_list(ls)), args), ignore_hide); + return pp_child(mk_app(mk_constant(abbrev, to_list(ls)), args), bp, ignore_hide); } static bool is_pp_atomic(expr const & e) { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index e10f5ba3e..73a857372 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -108,7 +108,7 @@ private: result pp_let(expr e); result pp_num(mpz const & n); // If fn is true, then \c e is of the form (f a), and the abbreviation is \c f. - result pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide = false); + result pp_abbreviation(expr const & e, name const & abbrev, bool fn, unsigned bp = 0, bool ignore_hide = false); void set_options_core(options const & o); public: diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a5f782b42..b72b4abc8 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -53,6 +53,15 @@ FOREACH(T ${LEANTESTS}) COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) +# LEAN HoTT TESTS +file(GLOB LEANHTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.hlean") +FOREACH(T ${LEANHTESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanhtest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) +ENDFOREACH(T) + # LEAN RUN TESTS file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean") FOREACH(T ${LEANRUNTESTS}) diff --git a/tests/lean/abbrev_paren.hlean b/tests/lean/abbrev_paren.hlean new file mode 100644 index 000000000..289bb075a --- /dev/null +++ b/tests/lean/abbrev_paren.hlean @@ -0,0 +1,5 @@ +import algebra.precategory.basic + +open category + +example {C : Precategory} : C = Precategory.mk C C := _ diff --git a/tests/lean/abbrev_paren.hlean.expected.out b/tests/lean/abbrev_paren.hlean.expected.out new file mode 100644 index 000000000..6a9b69f12 --- /dev/null +++ b/tests/lean/abbrev_paren.hlean.expected.out @@ -0,0 +1,7 @@ +abbrev_paren.hlean:5:54: error: don't know how to synthesize placeholder +C : Precategory +⊢ C = Precategory.mk (carrier C) C +abbrev_paren.hlean:5:54: error: failed to add declaration '14.0' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + λ (C : Precategory), + ?M_1 diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index b2dce3ce8..aebfdd271 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -6,14 +6,22 @@ fi ulimit -s 8192 LEAN=$1 export LEAN_PATH=../../library:. +export HLEAN_PATH=../../hott:. if [ $# -ne 3 ]; then INTERACTIVE=no else INTERACTIVE=$3 fi f=$2 + +if [ ${f: -6} == ".hlean" ]; then + CONFIG="config.hlean" +else + CONFIG="config.lean" +fi + echo "-- testing $f" -$LEAN config.lean $f &> $f.produced.out.1 +$LEAN $CONFIG $f &> $f.produced.out.1 sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out rm -f $f.produced.out.1 if test -f $f.expected.out; then