From cc9e16c3fcf2234356399d2b92a5f7c2cd4db63e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Dec 2013 18:45:13 -0800
Subject: [PATCH] feat(util/lean_path): add function for searching for a file
 in the LEAN_PATH

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

diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index 07cd6e1a68..d85d92fcc1 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -6,12 +6,17 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <cstdlib>
+#include <fstream>
+#include <vector>
 #include "util/exception.h"
+#include "util/sstream.h"
 
 namespace lean {
 #if defined(LEAN_WINDOWS)
 // Windows version
 #include <windows.h>
+static char g_path_sep = ';';
+static char g_sep      = '\\';
 static std::string get_exe_location() {
     HMODULE hModule = GetModuleHandleW(NULL);
     WCHAR path[MAX_PATH];
@@ -22,6 +27,8 @@ static std::string get_exe_location() {
 // OSX version
 #include <mach-o/dyld.h>
 #include <limits.h>
+static char g_path_sep = ':';
+static char g_sep      = '/';
 static std::string get_exe_location() {
     char buf[PATH_MAX];
     uint32_t bufsize = PATH_MAX;
@@ -36,6 +43,8 @@ static std::string get_exe_location() {
 #include <sys/stat.h>
 #include <limits.h> // NOLINT
 #include <stdio.h>
+static char g_path_sep = ':';
+static char g_sep      = '/';
 static std::string get_exe_location() {
     char path[PATH_MAX];
     char dest[PATH_MAX];
@@ -48,17 +57,42 @@ static std::string get_exe_location() {
     }
 }
 #endif
-static std::string g_lean_path;
+static std::string              g_lean_path;
+static std::vector<std::string> g_lean_path_vector;
 struct init_lean_path {
     init_lean_path() {
         char * r = getenv("LEAN_PATH");
-        if (r == nullptr)
-            g_lean_path = get_exe_location();
-        else
+        if (r == nullptr) {
+            g_lean_path  = ".";
+            g_lean_path += g_path_sep;
+            g_lean_path += get_exe_location();
+        } else {
             g_lean_path = r;
+        }
+        unsigned i  = 0;
+        unsigned j  = 0;
+        unsigned sz = g_lean_path.size();
+        for (; j < sz; j++) {
+            if (g_lean_path[j] == g_path_sep) {
+                if (j > i)
+                    g_lean_path_vector.push_back(g_lean_path.substr(i, j - i));
+                i = j + 1;
+            }
+        }
     }
 };
 static init_lean_path g_init_lean_path;
+
+std::string find_file(char const * fname) {
+    for (auto path : g_lean_path_vector) {
+        auto file = path + g_sep + fname;
+        std::ifstream ifile(file);
+        if (ifile)
+            return file;
+    }
+    throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH");
+}
+
 char const * get_lean_path() {
     return g_lean_path.c_str();
 }
diff --git a/src/util/lean_path.h b/src/util/lean_path.h
index 6bfb99418a..aec5745930 100644
--- a/src/util/lean_path.h
+++ b/src/util/lean_path.h
@@ -5,6 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 namespace lean {
+/**
+   \brief Return the LEAN_PATH string
+*/
 char const * get_lean_path();
+/**
+   \brief Search the file \c fname in the LEAN_PATH. Throw an
+   exception if the file was not found.
+*/
+std::string find_file(char const * fname);
 }