From ef069e39b01f931db3f6415763c9b8aff8c586db Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Dec 2013 12:53:49 -0800
Subject: [PATCH] chore(*): replace to_expr with to_nonnull_expr (when
 appropriate)

The goal is to make the Lua API more robust.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/fo_unify.cpp             | 2 +-
 src/library/substitution.cpp         | 4 ++--
 src/library/tactic/goal.cpp          | 6 +++---
 src/library/tactic/proof_builder.cpp | 4 ++--
 src/library/tactic/proof_state.cpp   | 2 +-
 src/library/tactic/tactic.cpp        | 4 ++--
 6 files changed, 11 insertions(+), 11 deletions(-)

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<substitution> fo_unify(expr e1, expr e2) {
 
 
 static int fo_unify(lua_State * L) {
-    optional<substitution> r = fo_unify(to_expr(L, 1), to_expr(L, 2));
+    optional<substitution> 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));
     }
 }