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

refactor(util/lua): propagate C++ Lean exceptions in Lua

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-27 12:19:54 -08:00
parent a6f6f49b5f
commit d87ad9eb7e
14 changed files with 288 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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:

35
src/frontends/lua/leanlua_state.cpp
View file

@ -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);

32
src/kernel/kernel_exception.h
View file

@ -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<expr> 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; }
};
}

2
src/library/elaborator/elaborator_exception.h
View file

@ -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; }
};
}

3
src/library/rewriter/rewriter.h
View file

@ -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,

2
src/util/debug.h
View file

@ -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<typename T> void display_var(char const * name, T const & value) {

59
src/util/exception.cpp
View file

@ -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<exception**>(luaL_checkudata(L, i, exception_mt)));
}
int push_exception(lua_State * L, exception const & e) {
exception ** mem = static_cast<exception**>(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<exception**>(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<exception_what>},
{"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");
}
}

11
src/util/exception.h
View file

@ -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 <exception>
#include <string>
@ -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);
}

33
src/util/lua.cpp
View file

@ -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

14
src/util/lua.h
View file

@ -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<lua_CFunction F> int safe_function(lua_State * L) {
return g_safe_function_wrapper(L, F);
return safe_function_wrapper(L, F);
}
template<lua_CFunction F> void set_global_function(lua_State * L, char const * name) {
lua_pushcfunction(L, safe_function<F>);
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<F>(L, N)
// Auxiliary macro for creating a Lua table that stores enumeration values

3
src/util/lua_exception.h
View file

@ -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; }
};
}

2
src/util/open_module.h
View file

@ -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);
}

8
tests/lean/lua15.lean
View file

@ -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()
**)

155
tests/lean/lua15.lean.expected.out
View file

@ -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