diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index 528492036..32aec3ac3 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -78,7 +78,7 @@ optional fo_unify(expr e1, expr e2) { static int fo_unify(lua_State * L) { - optional r = fo_unify(to_expr(L, 1), to_expr(L, 2)); + optional r = fo_unify(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2)); if (!r) { lua_pushnil(L); return 1; diff --git a/src/library/substitution.cpp b/src/library/substitution.cpp index 21402682d..e913fb073 100644 --- a/src/library/substitution.cpp +++ b/src/library/substitution.cpp @@ -59,7 +59,7 @@ static int substitution_find(lua_State * L) { substitution & s = to_substitution(L, 1); expr * it; if (is_expr(L, 2)) { - expr const & e = to_expr(L, 2); + expr const & e = to_nonnull_expr(L, 2); if (is_metavar(e)) it = s.splay_find(metavar_name(e)); else @@ -75,7 +75,7 @@ static int substitution_find(lua_State * L) { } static int substitution_apply(lua_State * L) { - return push_expr(L, apply(to_substitution(L, 1), to_expr(L, 2))); + return push_expr(L, apply(to_substitution(L, 1), to_nonnull_expr(L, 2))); } static const struct luaL_Reg substitution_m[] = { diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 941dfe51f..40fedea8f 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -159,9 +159,9 @@ static int mk_hypotheses(lua_State * L) { if (nargs == 0) { return push_hypotheses(L, hypotheses()); } else if (nargs == 2) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses())); + return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_nonnull_expr(L, 2)), hypotheses())); } else if (nargs == 3) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3))); + return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_nonnull_expr(L, 2)), to_hypotheses(L, 3))); } else { throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments"); } @@ -230,7 +230,7 @@ static const struct luaL_Reg hypotheses_m[] = { DECL_UDATA(goal) static int mk_goal(lua_State * L) { - return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); + return push_goal(L, goal(to_hypotheses(L, 1), to_nonnull_expr(L, 2))); } static int goal_is_null(lua_State * L) { diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index 2d15fb426..1f7fbae3e 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/src/library/tactic/proof_builder.cpp @@ -50,7 +50,7 @@ static int proof_map_find(lua_State * L) { } static int proof_map_insert(lua_State * L) { - to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3)); + to_proof_map(L, 1).insert(to_name_ext(L, 2), to_nonnull_expr(L, 3)); return 0; } @@ -104,7 +104,7 @@ static int mk_proof_builder(lua_State * L) { push_proof_map(L, m); push_assignment(L, a); pcall(L, 2, 1, 0); - r = to_expr(L, -1); + r = to_nonnull_expr(L, -1); lua_pop(L, 1); }); return r; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 7a58dda42..917a81004 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -194,7 +194,7 @@ static int mk_proof_state(lua_State * L) { } static int to_proof_state(lua_State * L) { - return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3))); + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_nonnull_expr(L, 3))); } static int proof_state_tostring(lua_State * L) { diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 5785fd4fd..d80bb8569 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -663,10 +663,10 @@ static int tactic_solve(lua_State * L) { } else { io_state * ios = get_io_state(L); check_ios(ios); - return tactic_solve_core(L, t, env, *ios, to_context(L, 3), to_expr(L, 4)); + return tactic_solve_core(L, t, env, *ios, to_context(L, 3), to_nonnull_expr(L, 4)); } } else { - return tactic_solve_core(L, t, env, to_io_state(L, 3), to_context(L, 4), to_expr(L, 5)); + return tactic_solve_core(L, t, env, to_io_state(L, 3), to_context(L, 4), to_nonnull_expr(L, 5)); } }