feat(library/init/lean): implement findOLean and findLean in Lean

library/init/lean/environment.lean

@@ -410,7 +410,7 @@ def writeModule (env : Environment) (fname : String) : IO Unit :=
 do modData ← mkModuleData env; saveModuleData fname modData
 
 @[extern 2 "lean_find_olean"]
-constant findOLean (modName : Name) : IO String := default _
+constant findOLeanOld (modName : Name) : IO String := default _
 
 partial def importModulesAux : List Name → (NameSet × Array ModuleData) → IO (NameSet × Array ModuleData)
 | []      r         := pure r
@@ -419,7 +419,7 @@ partial def importModulesAux : List Name → (NameSet × Array ModuleData) → I
     importModulesAux ms (s, mods)
   else do
     let s := s.insert m;
-    mFile ← findOLean m;
+    mFile ← findOLeanOld m;
     mod ← readModuleData mFile;
     (s, mods) ← importModulesAux mod.imports.toList (s, mods);
     let mods := mods.push mod;

library/init/lean/modulename.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.name
+
+namespace Lean
+
+inductive ModuleName
+| explicit (name : Name)
+| relative (rel : Nat) (name : Name)
+
+namespace ModuleName
+
+instance : Inhabited ModuleName := ⟨ModuleName.explicit Name.anonymous⟩
+
+instance : HasCoe Name ModuleName := ⟨explicit⟩
+
+end ModuleName
+
+end Lean

library/init/lean/path.lean

@@ -7,9 +7,11 @@ prelude
 import init.system.io
 import init.system.filepath
 import init.data.array
+import init.control.combinators
+import init.lean.modulename
 
 namespace Lean
-open System.FilePath (pathSeparator searchPathSeparator)
+open System.FilePath (pathSeparator searchPathSeparator extSeparator)
 private def pathSep : String := toString pathSeparator
 private def searchPathSep : String := toString searchPathSeparator
 
@@ -26,14 +28,12 @@ searchPathRef.set (s.split searchPathSep).toArray
 def getBuiltinSearchPath : IO String :=
 do appDir ← IO.appDir;
    let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "library";
-   IO.println libDir;
    libDirExists ← IO.isDir libDir;
    if libDirExists then
      IO.realPath libDir
    else do
      let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "library";
      installedLibDirExists ← IO.isDir installedLibDir;
-     IO.println installedLibDir;
      if installedLibDirExists then do
        IO.realPath installedLibDir
      else
@@ -62,7 +62,37 @@ def findFile (fname : String) : IO (Option String) :=
 do paths ← searchPathRef.get;
    paths.mfind $ fun path => do
      let curr := path ++ pathSep ++ fname;
+     IO.println ("trying " ++ curr);
      ex ← IO.fileExists curr;
      if ex then pure (some curr) else pure none
 
+def modNameToFileName : Name → String
+| (Name.mkString Name.anonymous h)  := h
+| (Name.mkString p h)               := modNameToFileName p ++ pathSep ++ h
+| Name.anonymous                    := ""
+| (Name.mkNumeral p _)              := modNameToFileName p
+
+def addRel : Nat → String
+| 0     := "."
+| (n+1) := addRel n ++ pathSep ++ ".."
+
+def findLeanFile (modName : ModuleName) (ext : String) : IO String :=
+match modName with
+| ModuleName.explicit modName => do
+  let fname := modNameToFileName modName ++ toString extSeparator ++ ext;
+  some fname ← findFile fname | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
+  IO.realPath fname
+| ModuleName.relative n modName => do
+  let fname := modNameToFileName modName ++ toString extSeparator ++ ext;
+  let fname := addRel n ++ pathSep ++ fname;
+  ex ← IO.fileExists fname;
+  unless ex $ throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
+  IO.realPath fname
+
+def findOLean (modName : ModuleName) : IO String :=
+findLeanFile modName "olean"
+
+def findLean (modName : Name) : IO String :=
+findLeanFile modName "lean"
+
 end Lean

library/init/system/io.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.control.estate init.data.string.basic
+import init.control.estate
+import init.data.string.basic
+import init.system.filepath
 
 /-- Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
     Makes sure we never reorder `IO` operations.
@@ -127,7 +129,7 @@ constant isDir (fname : @& String) : IO Bool := default _
 @[extern 2 "lean_io_file_exists"]
 constant fileExists (fname : @& String) : IO Bool := default _
 @[extern 1 "lean_io_app_dir"]
-constant appDir : IO String := default _
+constant appPath : IO String := default _
 
 @[inline] def liftIO {m : Type → Type} {α : Type} [monadIO m] (x : IO α) : m α :=
 monadLift x
@@ -146,7 +148,11 @@ def getEnv : String → m (Option String) := Prim.liftIO ∘ Prim.getEnv
 def realPath : String → m String := Prim.liftIO ∘ Prim.realPath
 def isDir : String → m Bool := Prim.liftIO ∘ Prim.isDir
 def fileExists : String → m Bool := Prim.liftIO ∘ Prim.fileExists
-def appDir : m String := Prim.liftIO Prim.appDir
+def appPath : m String := Prim.liftIO Prim.appPath
+
+def appDir : m String :=
+do p ← appPath;
+   realPath (System.FilePath.dirName p)
 
 end