From 1e4c5f1761254492b5ceebe4caf9ab66f911b715 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 May 2014 14:12:15 -0700
Subject: [PATCH] feat(util/lua_named_param): add new functions for handling
 named parameters in Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/lua_named_param.cpp | 50 ++++++++++++++++++++++++++++++++++--
 src/util/lua_named_param.h   |  4 +++
 2 files changed, 52 insertions(+), 2 deletions(-)

diff --git a/src/util/lua_named_param.cpp b/src/util/lua_named_param.cpp
index 366645e77..2b0e34aa9 100644
--- a/src/util/lua_named_param.cpp
+++ b/src/util/lua_named_param.cpp
@@ -67,10 +67,56 @@ unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, uns
             return static_cast<unsigned>(result);
         } else if (lua_isnil(L, -1)) {
             lua_pop(L, 1);
-            return static_cast<unsigned>(def_value);
+            return def_value;
         } else {
             lua_pop(L, 1);
-            throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
+            throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
+
+optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name, optional<unsigned> const & def_value) {
+    if (lua_istable(L, idx)) {
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (lua_isnumber(L, -1)) {
+            long result = lua_tointeger(L, -1);
+            lua_pop(L, 1);
+            if (result < 0 || result > std::numeric_limits<unsigned>::max())
+                throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
+            return optional<unsigned>(static_cast<unsigned>(result));
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return def_value;
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
+
+name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value) {
+    if (lua_istable(L, idx)) {
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (is_name_set(L, -1)) {
+            name_set result = to_name_set(L, -1);
+            lua_pop(L, 1);
+            return result;
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return def_value;
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be a name_set in table at arg #" << idx);
         }
     } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
         throw exception(sstream() << "arg #" << idx << " must be a table");
diff --git a/src/util/lua_named_param.h b/src/util/lua_named_param.h
index 06799facf..411013521 100644
--- a/src/util/lua_named_param.h
+++ b/src/util/lua_named_param.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/lua.h"
 #include "util/optional.h"
+#include "util/name_set.h"
 
 namespace lean {
 // =======================================
@@ -15,4 +16,7 @@ namespace lean {
 bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value);
 int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value);
 unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value);
+optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name,
+                                            optional<unsigned> const & def_value = optional<unsigned>());
+name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value = name_set());
 }