From d87ad9eb7e1d33aedb43e3d106b1a7bbd8c8fd20 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Nov 2013 12:19:54 -0800 Subject: [PATCH] refactor(util/lua): propagate C++ Lean exceptions in Lua The following call sequence is possible: C++ -> Lua -> C++ -> Lua -> C++ The first block of C++ is the Lean main function. The main function invokes the Lua interpreter. The Lua interpreter invokes a C++ Lean API. Then the Lean API invokes a callback implemented in Lua. The Lua callback invokes another Lean API. Now, suppose the Lean API throws an exception. We want the C++ exception to propagate over the mixed C++/Lua call stack. We use the clone/rethrow exception idiom to achieve this goal. Before this commit, the C++ exceptions were converted into strings using the method what(), and then they were propagated over the Lua stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++. This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 6 +- src/frontends/lua/leanlua_state.cpp | 35 ---- src/kernel/kernel_exception.h | 32 ++++ src/library/elaborator/elaborator_exception.h | 2 + src/library/rewriter/rewriter.h | 3 + src/util/debug.h | 2 + src/util/exception.cpp | 59 +++++++ src/util/exception.h | 11 ++ src/util/lua.cpp | 33 +--- src/util/lua.h | 14 +- src/util/lua_exception.h | 3 + src/util/open_module.h | 2 + tests/lean/lua15.lean | 8 +- tests/lean/lua15.lean.expected.out | 155 ++++++++++++++++++ 14 files changed, 288 insertions(+), 77 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index cdaa57a17..385d247ff 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -141,6 +141,8 @@ class parser::imp { pos_info m_pos; parser_error(char const * msg, pos_info const & p):exception(msg), m_pos(p) {} parser_error(sstream const & msg, pos_info const & p):exception(msg), m_pos(p) {} + virtual exception * clone() const { return new parser_error(m_msg.c_str(), m_pos); } + virtual void rethrow() const { throw *this; } }; /** @@ -1573,7 +1575,6 @@ class parser::imp { regular(m_frontend) << " executing script, but could not decode position information, " << ex.what() << endl; break; } - next(); } void updt_options() { @@ -1592,8 +1593,9 @@ class parser::imp { m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos()); if (!m_script_evaluator) throw exception("failed to execute Lua script, parser does not have a Lua interpreter"); - m_script_evaluator->dostring(m_scanner.get_str_val().c_str(), m_frontend.get_environment(), m_frontend.get_state()); + std::string script_code = m_scanner.get_str_val(); next(); + m_script_evaluator->dostring(script_code.c_str(), m_frontend.get_environment(), m_frontend.get_state()); } public: diff --git a/src/frontends/lua/leanlua_state.cpp b/src/frontends/lua/leanlua_state.cpp index 1a8e998a1..5ca722cd2 100644 --- a/src/frontends/lua/leanlua_state.cpp +++ b/src/frontends/lua/leanlua_state.cpp @@ -566,46 +566,11 @@ static void open_interrupt(lua_State * L) { SET_GLOBAL_FUN(channel_write, "write"); } -void _check_result(lua_State * L, int result) { - if (result) { - if (is_justification(L, -1)) - throw elaborator_exception(to_justification(L, -1)); - else - throw lua_exception(lua_tostring(L, -1)); - } -} - -static set_check_result set_check(_check_result); - -static int _safe_function_wrapper(lua_State * L, lua_CFunction f) { - try { - return f(L); - } catch (kernel_exception & e) { - std::ostringstream out; - options o = get_global_options(L); - out << mk_pair(e.pp(get_global_formatter(L), o), o); - lua_pushstring(L, out.str().c_str()); - } catch (elaborator_exception & e) { - push_justification(L, e.get_justification()); - } catch (exception & e) { - lua_pushstring(L, e.what()); - } catch (std::bad_alloc &) { - lua_pushstring(L, "out of memory"); - } catch (std::exception & e) { - lua_pushstring(L, e.what()); - } catch(...) { - lua_pushstring(L, "unknown error"); - } - return lua_error(L); -} - static int mk_environment(lua_State * L) { frontend f; return push_environment(L, f.get_environment()); } -static set_safe_function_wrapper set_wrapper(_safe_function_wrapper); - void open_extra(lua_State * L) { open_state(L); open_thread(L); diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 1b2e8fa49..7bb0b5349 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -30,16 +30,21 @@ public: */ virtual expr const & get_main_expr() const { return expr::null(); } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new kernel_exception(m_env, m_msg.c_str()); } + virtual void rethrow() const { throw *this; } }; /** \brief Base class for unknown universe or object exceptions. */ class unknown_name_exception : public kernel_exception { +protected: name m_name; public: unknown_name_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {} virtual ~unknown_name_exception() {} name const & get_name() const { return m_name; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new unknown_name_exception(m_env, m_name); } + virtual void rethrow() const { throw *this; } }; /** \brief Exception used to report that a universe variable is not known in a given environment. */ @@ -47,6 +52,8 @@ class unknown_universe_variable_exception : public unknown_name_exception { public: unknown_universe_variable_exception(environment const & env, name const & n):unknown_name_exception(env, n) {} virtual char const * what() const noexcept { return "unknown universe variable"; } + virtual exception * clone() const { return new unknown_universe_variable_exception(m_env, m_name); } + virtual void rethrow() const { throw *this; } }; /** \brief Exception used to report that an object is not known in a given environment. */ @@ -54,10 +61,13 @@ class unknown_object_exception : public unknown_name_exception { public: unknown_object_exception(environment const & env, name const & n):unknown_name_exception(env, n) {} virtual char const * what() const noexcept { return "unknown object"; } + virtual exception * clone() const { return new unknown_object_exception(m_env, m_name); } + virtual void rethrow() const { throw *this; } }; /** \brief Base class for already declared object. */ class already_declared_exception : public kernel_exception { +protected: name m_name; public: already_declared_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {} @@ -65,6 +75,8 @@ public: name const & get_name() const { return m_name; } virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new already_declared_exception(m_env, m_name); } + virtual void rethrow() const { throw *this; } }; /** @@ -77,12 +89,16 @@ class read_only_environment_exception : public kernel_exception { public: read_only_environment_exception(environment const & env):kernel_exception(env) {} virtual char const * what() const noexcept { return "environment cannot be updated because it has children environments"; } + virtual exception * clone() const { return new read_only_environment_exception(m_env); } + virtual void rethrow() const { throw *this; } }; /** \brief Base class for type checking related exceptions. */ class type_checker_exception : public kernel_exception { public: type_checker_exception(environment const & env):kernel_exception(env) {} + virtual exception * clone() const { return new type_checker_exception(m_env); } + virtual void rethrow() const { throw *this; } }; /** \brief Exception for objects that do not have types associated with them */ @@ -94,6 +110,8 @@ public: virtual expr const & get_main_expr() const { return m_const; } virtual char const * what() const noexcept { return "object does not have a type associated with it"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new has_no_type_exception(m_env, m_const); } + virtual void rethrow() const { throw *this; } }; /** @@ -120,6 +138,8 @@ public: std::vector const & get_arg_types() const { return m_arg_types; } virtual char const * what() const noexcept { return "application argument type mismatch"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new app_type_mismatch_exception(m_env, m_context, m_app, m_arg_types.size(), m_arg_types.data()); } + virtual void rethrow() const { throw *this; } }; /** @@ -142,6 +162,8 @@ public: virtual expr const & get_main_expr() const { return get_expr(); } virtual char const * what() const noexcept { return "function expected"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new function_expected_exception(m_env, m_context, m_expr); } + virtual void rethrow() const { throw *this; } }; /** @@ -164,6 +186,8 @@ public: virtual expr const & get_main_expr() const { return get_expr(); } virtual char const * what() const noexcept { return "type expected"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new type_expected_exception(m_env, m_context, m_expr); } + virtual void rethrow() const { throw *this; } }; /** @@ -198,6 +222,8 @@ public: virtual expr const & get_main_expr() const { return m_value; } virtual char const * what() const noexcept { return "definition type mismatch"; } virtual format pp(formatter const & fmt, options const & opts) const; + virtual exception * clone() const { return new def_type_mismatch_exception(m_env, m_context, m_name, m_type, m_value, m_value_type); } + virtual void rethrow() const { throw *this; } }; /** @@ -210,6 +236,8 @@ public: virtual ~invalid_builtin_value_declaration() {} virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; } virtual expr const & get_main_expr() const { return m_expr; } + virtual exception * clone() const { return new invalid_builtin_value_declaration(m_env, m_expr); } + virtual void rethrow() const { throw *this; } }; /** @@ -223,6 +251,8 @@ public: virtual ~invalid_builtin_value_reference() {} virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; } virtual expr const & get_main_expr() const { return m_expr; } + virtual exception * clone() const { return new invalid_builtin_value_reference(m_env, m_expr); } + virtual void rethrow() const { throw *this; } }; /** @@ -235,5 +265,7 @@ public: virtual ~unexpected_metavar_occurrence() {} virtual char const * what() const noexcept { return "unexpected metavariable occurrence"; } virtual expr const & get_main_expr() const { return m_expr; } + virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); } + virtual void rethrow() const { throw *this; } }; } diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h index 1a8f244a4..7f847eee5 100644 --- a/src/library/elaborator/elaborator_exception.h +++ b/src/library/elaborator/elaborator_exception.h @@ -20,5 +20,7 @@ public: virtual ~elaborator_exception() {} virtual char const * what() const noexcept { return "elaborator exception"; } justification const & get_justification() const { return m_justification; } + virtual exception * clone() const { return new elaborator_exception(m_justification); } + virtual void rethrow() const { throw *this; } }; } diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index afa89c1f7..42a753d96 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -24,6 +24,9 @@ Author: Soonho Kong namespace lean { class rewriter_exception : public exception { +public: + virtual exception * clone() const { return new rewriter_exception(); } + virtual void rethrow() const { throw *this; } }; enum class rewriter_kind { Theorem, OrElse, Then, Try, App, diff --git a/src/util/debug.h b/src/util/debug.h index d8eeff670..70a6dc1e7 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -106,6 +106,8 @@ public: unreachable_reached() {} virtual ~unreachable_reached() noexcept {} virtual char const * what() const noexcept { return "'unreachable' code was reached"; } + virtual exception * clone() const { return new unreachable_reached(); } + virtual void rethrow() const { throw *this; } }; namespace debug { template void display_var(char const * name, T const & value) { diff --git a/src/util/exception.cpp b/src/util/exception.cpp index b3246351e..a5976a354 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -32,4 +32,63 @@ char const * parser_exception::what() const noexcept { return m_msg.c_str(); } } + +constexpr char const * exception_mt = "exception_mt"; +exception const & to_exception(lua_State * L, int i) { + return *(*static_cast(luaL_checkudata(L, i, exception_mt))); +} + +int push_exception(lua_State * L, exception const & e) { + exception ** mem = static_cast(lua_newuserdata(L, sizeof(exception*))); // NOLINT + *mem = e.clone(); + luaL_getmetatable(L, exception_mt); + lua_setmetatable(L, -2); + return 1; +} + +static int exception_gc(lua_State * L) { + exception ** mem = static_cast(lua_touserdata(L, 1)); + delete (*mem); + return 0; +} + +bool is_exception(lua_State * L, int i) { + return testudata(L, i, exception_mt); +} + +static int exception_what(lua_State * L) { + lua_pushstring(L, to_exception(L, 1).what()); + return 1; +} + +static int exception_rethrow(lua_State * L) { + lua_pushvalue(L, 1); + return lua_error(L); +} + +static int exception_pred(lua_State * L) { + lua_pushboolean(L, is_exception(L, 1)); + return 1; +} + +static const struct luaL_Reg exception_m[] = { + {"__gc", exception_gc}, // never throws + {"what", safe_function}, + {"rethrow", exception_rethrow}, // generates a lua_error + {0, 0} +}; + +static void exception_migrate(lua_State * src, int i, lua_State * tgt) { + push_exception(tgt, to_exception(src, i)); +} + +void open_exception(lua_State * L) { + luaL_newmetatable(L, exception_mt); + set_migrate_fn_field(L, -1, exception_migrate); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, exception_m, 0); + + SET_GLOBAL_FUN(exception_pred, "is_exception"); +} } diff --git a/src/util/exception.h b/src/util/exception.h index 684546019..20dab89a2 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include #include @@ -21,6 +22,8 @@ public: exception(sstream const & strm); virtual ~exception() noexcept; virtual char const * what() const noexcept; + virtual exception * clone() const { return new exception(m_msg); } + virtual void rethrow() const { throw *this; } }; /** \brief Exception produced by a Lean parser. */ class parser_exception : public exception { @@ -35,6 +38,8 @@ public: virtual char const * what() const noexcept; unsigned get_line() const { return m_line; } unsigned get_pos() const { return m_pos; } + virtual exception * clone() const { return new parser_exception(m_msg, m_line, m_pos); } + virtual void rethrow() const { throw *this; } }; /** \brief Exception used to sign that a computation was interrupted */ class interrupted : public exception { @@ -42,10 +47,16 @@ public: interrupted() {} virtual ~interrupted() noexcept {} virtual char const * what() const noexcept { return "interrupted"; } + virtual exception * clone() const { return new interrupted(); } + virtual void rethrow() const { throw *this; } }; /** \brief Throw interrupted exception iff flag is true. */ inline void check_interrupted(bool flag) { if (flag) throw interrupted(); } +int push_exception(lua_State * L, exception const & e); +exception const & to_exception(lua_State * L, int i); +bool is_exception(lua_State * L, int i); +void open_exception(lua_State * L); } diff --git a/src/util/lua.cpp b/src/util/lua.cpp index fe13b3192..e68c25959 100644 --- a/src/util/lua.cpp +++ b/src/util/lua.cpp @@ -89,26 +89,15 @@ static void exec(lua_State * L) { pcall(L, 0, LUA_MULTRET, 0); } -/** - \brief check_result for "customers" that are only using a subset - of Lean libraries. -*/ -void simple_check_result(lua_State * L, int result) { +void check_result(lua_State * L, int result) { if (result) { - throw lua_exception(lua_tostring(L, -1)); + if (is_exception(L, -1)) + to_exception(L, -1).rethrow(); + else + throw lua_exception(lua_tostring(L, -1)); } } -static void (*g_check_result)(lua_State *, int) = simple_check_result; - -static void check_result(lua_State * L, int result) { - g_check_result(L, result); -} - -set_check_result::set_check_result(void (*f)(lua_State *, int)) { - g_check_result = f; -} - void dofile(lua_State * L, char const * fname) { int result = luaL_loadfile(L, fname); check_result(L, result); @@ -130,11 +119,13 @@ void pcall(lua_State * L, int nargs, int nresults, int errorfun) { \brief Wrapper for "customers" that are only using a subset of Lean libraries. */ -int simple_safe_function_wrapper(lua_State * L, lua_CFunction f){ +int safe_function_wrapper(lua_State * L, lua_CFunction f) { try { return f(L); - } catch (exception & e) { + } catch (lua_exception & e) { lua_pushstring(L, e.what()); + } catch (exception & e) { + push_exception(L, e); } catch (std::bad_alloc &) { lua_pushstring(L, "out of memory"); } catch (std::exception & e) { @@ -145,12 +136,6 @@ int simple_safe_function_wrapper(lua_State * L, lua_CFunction f){ return lua_error(L); } -int (*g_safe_function_wrapper)(lua_State * L, lua_CFunction f) = simple_safe_function_wrapper; - -set_safe_function_wrapper::set_safe_function_wrapper(int (*f)(lua_State *, lua_CFunction)) { - g_safe_function_wrapper = f; -} - void set_migrate_fn_field(lua_State * L, int i, lua_migrate_fn fn) { lean_assert(lua_istable(L, i)); lua_pushvalue(L, i); // copy table to the top of the stack diff --git a/src/util/lua.h b/src/util/lua.h index 23c40eb0d..43eefc2f8 100644 --- a/src/util/lua.h +++ b/src/util/lua.h @@ -31,24 +31,14 @@ int get_nonnil_top(lua_State * L); /** \brief Wrapper for invoking function f, and catching Lean exceptions. */ -extern int (*g_safe_function_wrapper)(lua_State * L, lua_CFunction f); +int safe_function_wrapper(lua_State * L, lua_CFunction f); template int safe_function(lua_State * L) { - return g_safe_function_wrapper(L, F); + return safe_function_wrapper(L, F); } template void set_global_function(lua_State * L, char const * name) { lua_pushcfunction(L, safe_function); lua_setglobal(L, name); } -/** - \brief Helper object for setting g_safe_function_wrapper. -*/ -struct set_safe_function_wrapper { set_safe_function_wrapper(int (*f)(lua_State *, lua_CFunction)); }; - -/** - \brief Helper object for setting a different check_result function. -*/ -struct set_check_result { set_check_result(void (*f)(lua_State *, int)); }; - #define SET_GLOBAL_FUN(F, N) set_global_function(L, N) // Auxiliary macro for creating a Lua table that stores enumeration values diff --git a/src/util/lua_exception.h b/src/util/lua_exception.h index b35dd6195..6877bc54e 100644 --- a/src/util/lua_exception.h +++ b/src/util/lua_exception.h @@ -18,6 +18,7 @@ private: source m_source; std::string m_file; // if source == File, then this field contains the filename that triggered the error. unsigned m_line; // line number + lua_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {} public: lua_exception(char const * lua_error); virtual ~lua_exception(); @@ -26,5 +27,7 @@ public: virtual unsigned get_line() const; /** \brief Return error message without position information */ virtual char const * get_msg() const noexcept; + virtual exception * clone() const { return new lua_exception(m_source, m_file, m_line); } + virtual void rethrow() const { throw *this; } }; } diff --git a/src/util/open_module.h b/src/util/open_module.h index da7332332..bf416845d 100644 --- a/src/util/open_module.h +++ b/src/util/open_module.h @@ -5,11 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/exception.h" #include "util/name.h" #include "util/splay_map.h" namespace lean { inline void open_util_module(lua_State * L) { + open_exception(L); open_name(L); open_splay_map(L); } diff --git a/tests/lean/lua15.lean b/tests/lean/lua15.lean index 92f7b5d12..528e57ac3 100644 --- a/tests/lean/lua15.lean +++ b/tests/lean/lua15.lean @@ -3,12 +3,12 @@ Variable p : Bool (** local env = get_environment() - ok, jst = pcall( + ok, ex = pcall( function() print(parse_lean("i + p")) end) assert(not ok) - assert(is_justification(jst)) - assert(not jst:is_null()) - print(jst:pp{display_children = false}) + assert(is_exception(ex)) + print(ex:what()) + ex:rethrow() **) diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out index 3b5aff40d..94a771a32 100644 --- a/tests/lean/lua15.lean.expected.out +++ b/tests/lean/lua15.lean.expected.out @@ -3,5 +3,160 @@ Assumed: i Assumed: j Assumed: p +elaborator exception Failed to solve ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add) + Overloading at + (Real::add | Int::add | Nat::add) i p + Failed to solve + ⊢ (?M::1 ≈ λ x : ℤ, x) ⊕ (?M::1 ≈ int_to_real) + Coercion for + i + Failed to solve + ⊢ ℤ ≺ ℕ + Substitution + ⊢ ℤ ≺ ?M::6 + Substitution + ⊢ (?M::5[inst:0 i]) i ≺ ?M::6 + Type of argument 1 must be convertible to the expected type in the application of + ?M::0 + with arguments: + ?M::1 i + p + Assignment + x : ℤ ⊢ λ x : ℤ, ℤ ≈ ?M::5 + Destruct/Decompose + x : ℤ ⊢ ℤ ≈ ?M::5 x + Destruct/Decompose + ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 x + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x + Function expected at + ?M::1 i + Assignment + ⊢ ℤ → ℤ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ λ x : ℤ, x + Assumption 1 + Assignment + ⊢ ℕ ≈ ?M::6 + Destruct/Decompose + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℕ → ℕ → ℕ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Nat::add + Assumption 0 + Failed to solve + ⊢ ℝ ≺ ℕ + Substitution + ⊢ ℝ ≺ ?M::6 + Substitution + ⊢ (?M::5[inst:0 i]) i ≺ ?M::6 + Type of argument 1 must be convertible to the expected type in the application of + ?M::0 + with arguments: + ?M::1 i + p + Assignment + _ : ℤ ⊢ λ x : ℤ, ℝ ≈ ?M::5 + Destruct/Decompose + _ : ℤ ⊢ ℝ ≈ ?M::5 _ + Destruct/Decompose + ⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5 x + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x + Function expected at + ?M::1 i + Assignment + ⊢ ℤ → ℝ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ int_to_real + Assumption 2 + Assignment + ⊢ ℕ ≈ ?M::6 + Destruct/Decompose + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℕ → ℕ → ℕ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Nat::add + Assumption 0 + Failed to solve + ⊢ Bool ≺ ℤ + Substitution + ⊢ Bool ≺ ?M::8 + Type of argument 2 must be convertible to the expected type in the application of + ?M::0 + with arguments: + ?M::1 i + p + Assignment + ⊢ ℤ ≈ ?M::8 + Destruct/Decompose + ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x + Substitution + ⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7 + Destruct/Decompose + _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _ + Destruct/Decompose + ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℤ → ℤ → ℤ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Int::add + Assumption 3 + Failed to solve + ⊢ Bool ≺ ℝ + Substitution + ⊢ Bool ≺ ?M::8 + Type of argument 2 must be convertible to the expected type in the application of + ?M::0 + with arguments: + ?M::1 i + p + Assignment + ⊢ ℝ ≈ ?M::8 + Destruct/Decompose + ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x + Substitution + ⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7 + Destruct/Decompose + _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _ + Destruct/Decompose + ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℝ → ℝ → ℝ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Real::add + Assumption 5