feat(util/script_state): add 'import' command to Lua, it import files from the LEAN_PATH

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/macros.lean

@@ -1,80 +1,6 @@
 (**
- -- This example demonstrates how to create Macros for automating proof
+-- import macros for, assume, mp, ...
- -- construction using Lua.
+import("macros.lua")
-
- -- This macro creates the syntax-sugar
- --     name bindings ',' expr
- -- For a function f with signature
- --    f : ... (A : Type) ... (Pi x : A, ...)
- --
- -- farity is the arity of f
- -- typepos is the position of (A : Type) argument
- -- lambdapos is the position of the (Pi x : A, ...) argument
- --
- -- Example: suppose we invoke
- --
- --    binder_macro("for", Const("ForallIntro"), 3, 1, 3)
- --
- -- Then, the macro expression
- --
- --     for x y : Int, H x y
- --
- -- produces the expression
- --
- --     ForallIntro Int _ (fun x : Int, ForallIntro Int _ (fun y : Int, H x y))
- --
- -- The _ are placeholders (aka) holes that will be filled by the Lean
- -- elaborator.
- function binder_macro(name, f, farity, typepos, lambdapos)
-    macro(name, { macro_arg.Bindings, macro_arg.Comma, macro_arg.Expr },
-          function (bindings, body)
-             local r = body
-             for i = #bindings, 1, -1 do
-                local bname = bindings[i][1]
-                local btype = bindings[i][2]
-                local args  = {}
-                args[#args + 1] = f
-                for j = 1, farity, 1 do
-                   if j == typepos then
-                      args[#args + 1] = btype
-                   elseif j == lambdapos then
-                      args[#args + 1] = fun(bname, btype, r)
-                   else
-                      args[#args + 1] = mk_placeholder()
-                   end
-                end
-                r = mk_app(unpack(args))
-             end
-             return r
-    end)
- end
-
- function nary_macro(name, f, farity)
-    local bin_app = function(e1, e2)
-       local args = {}
-       args[#args + 1] = f
-       for i = 1, farity - 2, 1 do
-          args[#args + 1] = mk_placeholder()
-       end
-       args[#args + 1] = e1
-       args[#args + 1] = e2
-       return mk_app(unpack(args))
-    end
-
-    macro(name, { macro_arg.Expr, macro_arg.Expr, macro_arg.Exprs },
-          function (e1, e2, rest)
-             local r = bin_app(e1, e2)
-             for i = 1, #rest do
-                r = bin_app(r, rest[i])
-             end
-             return r
-    end)
- end
-
- binder_macro("for", Const("ForallIntro"), 3, 1, 3)
- binder_macro("assume", Const("Discharge"), 3, 1, 3)
- nary_macro("instantiate", Const("ForallElim"), 4)
- nary_macro("mp", Const("MP"), 4)
 **)
 
 Definition Set (A : Type) : Type := A → Bool

src/extra/macros.lua

@@ -0,0 +1,87 @@
+-- Extra macros for automating proof construction using Lua.
+
+-- This macro creates the syntax-sugar
+--     name bindings ',' expr
+-- For a function f with signature
+--    f : ... (A : Type) ... (Pi x : A, ...)
+--
+-- farity is the arity of f
+-- typepos is the position of (A : Type) argument
+-- lambdapos is the position of the (Pi x : A, ...) argument
+--
+-- Example: suppose we invoke
+--
+--    binder_macro("for", Const("ForallIntro"), 3, 1, 3)
+--
+-- Then, the macro expression
+--
+--     for x y : Int, H x y
+--
+-- produces the expression
+--
+--     ForallIntro Int _ (fun x : Int, ForallIntro Int _ (fun y : Int, H x y))
+--
+-- The _ are placeholders (aka) holes that will be filled by the Lean
+-- elaborator.
+function binder_macro(name, f, farity, typepos, lambdapos)
+   macro(name, { macro_arg.Bindings, macro_arg.Comma, macro_arg.Expr },
+         function (bindings, body)
+            local r = body
+            for i = #bindings, 1, -1 do
+               local bname = bindings[i][1]
+               local btype = bindings[i][2]
+               local args  = {}
+               args[#args + 1] = f
+               for j = 1, farity, 1 do
+                  if j == typepos then
+                     args[#args + 1] = btype
+                  elseif j == lambdapos then
+                     args[#args + 1] = fun(bname, btype, r)
+                  else
+                     args[#args + 1] = mk_placeholder()
+                  end
+               end
+               r = mk_app(unpack(args))
+            end
+            return r
+   end)
+end
+
+-- The following macro is used to create nary versions of operators such as MP and ForallElim.
+-- Example: suppose we invoke
+--
+--    nary_macro("mp", Const("MP"), 4)
+--
+-- Then, the macro expression
+--
+--     mp Foo H1 H2 H3
+--
+-- produces the expression
+--
+--     (MP (MP (MP Foo H1) H2) H3)
+function nary_macro(name, f, farity)
+   local bin_app = function(e1, e2)
+      local args = {}
+      args[#args + 1] = f
+      for i = 1, farity - 2, 1 do
+         args[#args + 1] = mk_placeholder()
+      end
+      args[#args + 1] = e1
+      args[#args + 1] = e2
+      return mk_app(unpack(args))
+   end
+
+   macro(name, { macro_arg.Expr, macro_arg.Expr, macro_arg.Exprs },
+         function (e1, e2, rest)
+            local r = bin_app(e1, e2)
+            for i = 1, #rest do
+               r = bin_app(r, rest[i])
+            end
+            return r
+   end)
+end
+
+binder_macro("for", Const("ForallIntro"), 3, 1, 3)
+binder_macro("assume", Const("Discharge"), 3, 1, 3)
+nary_macro("instantiate", Const("ForallElim"), 4)
+nary_macro("mp", Const("MP"), 4)

src/util/lean_path.cpp

@@ -23,16 +23,7 @@ static std::string get_exe_location() {
     WCHAR path[MAX_PATH];
     GetModuleFileNameW(hModule, path, MAX_PATH);
     std::wstring pathstr(path);
-    std::string r(pathstr.begin(), pathstr.end());
+    return std::string(pathstr.begin(), pathstr.end());
-    while (true) {
-        if (r.empty())
-            throw exception("failed to locate Lean executable location");
-        if (r.back() == g_sep) {
-            r.pop_back();
-            return r;
-        }
-        r.pop_back();
-    }
 }
 #elif defined(__APPLE__)
 // OSX version
@@ -79,6 +70,18 @@ std::string normalize_path(std::string f) {
     return f;
 }
 
+std::string get_path(std::string f) {
+    while (true) {
+        if (f.empty())
+            throw exception("failed to locate Lean executable location");
+        if (f.back() == g_sep) {
+            f.pop_back();
+            return f;
+        }
+        f.pop_back();
+    }
+}
+
 static std::string              g_lean_path;
 static std::vector<std::string> g_lean_path_vector;
 struct init_lean_path {
@@ -87,7 +90,7 @@ struct init_lean_path {
         if (r == nullptr) {
             g_lean_path  = ".";
             g_lean_path += g_path_sep;
-            g_lean_path += get_exe_location();
+            g_lean_path += get_path(get_exe_location());
         } else {
             g_lean_path = r;
         }

src/util/script_state.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <string>
 #include <vector>
+#include <unordered_set>
 #include "util/thread.h"
 #include "util/lua.h"
 #include "util/debug.h"
@@ -18,6 +19,7 @@ Author: Leonardo de Moura
 #include "util/script_exception.h"
 #include "util/name.h"
 #include "util/splay_map.h"
+#include "util/lean_path.h"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
@@ -46,6 +48,7 @@ static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and sa
 struct script_state::imp {
     lua_State * m_state;
     mutex       m_mutex;
+    std::unordered_set<std::string> m_imported_modules;
 
     static std::weak_ptr<imp> * get_weak_ptr(lua_State * L) {
         lua_pushlightuserdata(L, static_cast<void *>(&g_weak_ptr_key));
@@ -115,6 +118,14 @@ struct script_state::imp {
         lock_guard<mutex> lock(m_mutex);
         ::lean::dostring(m_state, str);
     }
+
+    void import(char const * fname) {
+        std::string fname_str(find_file(fname));
+        if (m_imported_modules.find(fname_str) == m_imported_modules.end()) {
+            dofile(fname_str.c_str());
+            m_imported_modules.insert(fname_str);
+        }
+    }
 };
 
 script_state to_script_state(lua_State * L) {
@@ -143,6 +154,10 @@ void script_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
 
+void script_state::import(char const * str) {
+    m_ptr->import(str);
+}
+
 mutex & script_state::get_mutex() {
     return m_ptr->m_mutex;
 }
@@ -581,6 +596,13 @@ static int yield(lua_State * L) {
     }
 }
 
+static int import(lua_State * L) {
+    std::string fname = luaL_checkstring(L, 1);
+    script_state s = to_script_state(L);
+    s.exec_unprotected([&]() { s.import(fname.c_str()); });
+    return 0;
+}
+
 static void open_interrupt(lua_State * L) {
     SET_GLOBAL_FUN(check_interrupted, "check_interrupted");
     SET_GLOBAL_FUN(sleep,             "sleep");
@@ -597,5 +619,7 @@ void open_extra(lua_State * L) {
     open_thread(L);
 #endif
     open_interrupt(L);
+
+    SET_GLOBAL_FUN(import, "import");
 }
 }

src/util/script_state.h

@@ -44,6 +44,11 @@ public:
        This method throws an exception if an error occurs.
     */
     void dostring(char const * str);
+    /**
+       \brief Import file \c fname from the LEAN_PATH.
+       If the file was already included, then it nothing happens.
+    */
+    void import(char const * fname);
 
     /**
        \brief Execute \c f in the using the internal Lua State.