From 20c6789d1c616651036b4a31c8102d302fed7eb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Nov 2013 15:56:44 -0800
Subject: [PATCH] feat(extra): add extension that demonstrates how to parse
 'templates'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/frontend_lean.cpp |  4 +--
 src/bindings/lua/util.cpp          | 25 ++++++++++----
 src/bindings/lua/util.h            |  1 +
 src/extra/README.md                |  5 +++
 src/extra/parse_lean_tpl.lua       | 54 ++++++++++++++++++++++++++++++
 5 files changed, 81 insertions(+), 8 deletions(-)
 create mode 100644 src/extra/README.md
 create mode 100644 src/extra/parse_lean_tpl.lua

diff --git a/src/bindings/lua/frontend_lean.cpp b/src/bindings/lua/frontend_lean.cpp
index 5deaf05ac..cd590e388 100644
--- a/src/bindings/lua/frontend_lean.cpp
+++ b/src/bindings/lua/frontend_lean.cpp
@@ -56,7 +56,7 @@ static int parse_lean_expr(lua_State * L) {
       3. (string, env, options, formatter?) : Everything is explicitly provided in this
          version. We also support a variation where the formmater is omitted.
     */
-    int nargs = lua_gettop(L);
+    int nargs = get_nonnil_top(L);
     if (nargs == 1) {
         ro_environment env(L); // get global environment
         return parse_lean_expr_core(L, env);
@@ -100,7 +100,7 @@ static int parse_lean_cmds(lua_State * L) {
       The main difference is the function result. When calling with explicit options
       the function returns an updated set of options. Otherwise it does not return anything.
     */
-    int nargs = lua_gettop(L);
+    int nargs = get_nonnil_top(L);
     if (nargs == 1) {
         rw_environment env(L); // get global environment
         parse_lean_cmds_core(L, env);
diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp
index 5ea042303..02fd0d568 100644
--- a/src/bindings/lua/util.cpp
+++ b/src/bindings/lua/util.cpp
@@ -81,28 +81,41 @@ int equal(lua_State * L, int idx1, int idx2) {
     #endif
 }
 
+int get_nonnil_top(lua_State * L) {
+    int top = lua_gettop(L);
+    while (top > 0 && lua_isnil(L, top))
+        top--;
+    return top;
+}
+
 static void exec(lua_State * L) {
     pcall(L, 0, LUA_MULTRET, 0);
 }
 
+static 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));
+    }
+}
+
 void dofile(lua_State * L, char const * fname) {
     int result = luaL_loadfile(L, fname);
-    if (result)
-        throw lua_exception(lua_tostring(L, -1));
+    check_result(L, result);
     exec(L);
 }
 
 void dostring(lua_State * L, char const * str) {
     int result = luaL_loadstring(L, str);
-    if (result)
-        throw lua_exception(lua_tostring(L, -1));
+    check_result(L, result);
     exec(L);
 }
 
 void pcall(lua_State * L, int nargs, int nresults, int errorfun) {
     int result = lua_pcall(L, nargs, nresults, errorfun);
-    if (result)
-        throw lua_exception(lua_tostring(L, -1));
+    check_result(L, result);
 }
 
 int safe_function_wrapper(lua_State * L, lua_CFunction f){
diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h
index 39b2537c8..29aa5fde7 100644
--- a/src/bindings/lua/util.h
+++ b/src/bindings/lua/util.h
@@ -17,6 +17,7 @@ void dostring(lua_State * L, char const * str);
 void pcall(lua_State * L, int nargs, int nresults, int errorfun);
 int lessthan(lua_State * L, int idx1, int idx2);
 int equal(lua_State * L, int idx1, int idx2);
+int get_nonnil_top(lua_State * L);
 /**
    \brief Wrapper for invoking function f, and catching Lean exceptions.
 */
diff --git a/src/extra/README.md b/src/extra/README.md
new file mode 100644
index 000000000..bdc72073e
--- /dev/null
+++ b/src/extra/README.md
@@ -0,0 +1,5 @@
+Extra functionality
+-------------------
+
+This directory contains several Lua scripts that provide additional
+functionality to Lean.
diff --git a/src/extra/parse_lean_tpl.lua b/src/extra/parse_lean_tpl.lua
new file mode 100644
index 000000000..1f7e740d4
--- /dev/null
+++ b/src/extra/parse_lean_tpl.lua
@@ -0,0 +1,54 @@
+-- Parse a template expression string 'str'.
+-- The string 'str' contains placeholders of the form 'a::i', where 'i' is a numeral.
+-- The placeholders are replaced with values from the array 'args'.
+-- See 'test' function for an example.
+function parse_lean_tpl(str, args, env, opts, fmt)
+   assert(type(str) == "string")
+   assert(type(args) == "table")
+   assert(env == nil or is_environment(env))
+   if #args == 0 then
+      return parse_lean(str, env, opts, fmt)
+   else
+      -- Create the string "fun (a::1 : type-of-args[1]) ... (a::n : type-of-args[n]), $str",
+      -- where n is the size of args
+      local inferer = type_inferer(env)
+      local tbl = {"fun"}
+      for i = 1, #args do
+         table.insert(tbl, " (a::")
+         table.insert(tbl, i)
+         table.insert(tbl, " : ")
+         table.insert(tbl, tostring(inferer(args[i])))
+         table.insert(tbl, ")")
+      end
+      table.insert(tbl, ", ")
+      table.insert(tbl, str)
+      local new_str = table.concat(tbl)
+      local r = parse_lean(new_str, env, opts, fmt)
+      for i = 1, #args do
+         assert(r:is_lambda())
+         local n, d, body = r:fields()
+         r = body:instantiate(args[i])
+      end
+      return r
+   end
+end
+
+local test = function()
+   local env  = environment()
+   -- Load environment with some definitions
+   parse_lean_cmds([[
+        Variables a b : Real
+        Variable  f : Real -> Real
+        Variable  g : Real -> Real -> Real
+]], env)
+   local a, b, g = Consts("a, b, g")
+   local t1      = parse_lean_tpl("a::1 + (f a::2) - 10 + a::2", {a, g(b, a)}, env)
+   print(t1)
+   local t2      = parse_lean_tpl("f (a::1 + 1)", {g(b, b)}, env)
+   print(t2)
+end
+
+if not pcall(debug.getlocal, 4, 1) then
+   -- Main file
+   test()
+end