From e722ea9ed99bd5ced6d3c4cc8293b4ddbd518e27 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Jul 2019 16:04:10 -0700 Subject: [PATCH] feat(library/init/lean): implement `findOLean` and `findLean` in Lean --- library/init/lean/environment.lean | 4 ++-- library/init/lean/modulename.lean | 23 +++++++++++++++++++ library/init/lean/path.lean | 36 +++++++++++++++++++++++++++--- library/init/system/io.lean | 12 +++++++--- 4 files changed, 67 insertions(+), 8 deletions(-) create mode 100644 library/init/lean/modulename.lean diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index f8a3cb94fe..02ba1aff8b 100644 --- a/library/init/lean/environment.lean +++ b/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; diff --git a/library/init/lean/modulename.lean b/library/init/lean/modulename.lean new file mode 100644 index 0000000000..6132b0d9fa --- /dev/null +++ b/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 diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean index ac3bcdbab2..52eba03bcc 100644 --- a/library/init/lean/path.lean +++ b/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 diff --git a/library/init/system/io.lean b/library/init/system/io.lean index fc1f087ab1..7dfa7ebd57 100644 --- a/library/init/system/io.lean +++ b/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