Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit f99c4b4

Browse files
committed
feat: add module file path helpers
1 parent a9dcdab commit f99c4b4

File tree

1 file changed

+19
-7
lines changed

1 file changed

+19
-7
lines changed

Diff for: Lake/Config/Module.lean

+19-7
Original file line numberDiff line numberDiff line change
@@ -46,26 +46,38 @@ abbrev pkg (self : Module) : Package :=
4646
@[inline] def rootDir (self : Module) : FilePath :=
4747
self.lib.rootDir
4848

49+
@[inline] def filePath (dir : FilePath) (ext : String) (self : Module) : FilePath :=
50+
Lean.modToFilePath dir self.name ext
51+
52+
@[inline] def srcPath (ext : String) (self : Module) : FilePath :=
53+
self.filePath self.lib.srcDir ext
54+
4955
@[inline] def leanFile (self : Module) : FilePath :=
50-
Lean.modToFilePath self.lib.srcDir self.name "lean"
56+
self.srcPath "lean"
57+
58+
@[inline] def leanLibPath (ext : String) (self : Module) : FilePath :=
59+
self.filePath self.pkg.oleanDir ext
5160

5261
@[inline] def oleanFile (self : Module) : FilePath :=
53-
Lean.modToFilePath self.pkg.oleanDir self.name "olean"
62+
self.leanLibPath "olean"
5463

5564
@[inline] def ileanFile (self : Module) : FilePath :=
56-
Lean.modToFilePath self.pkg.oleanDir self.name "ilean"
65+
self.leanLibPath "ilean"
5766

5867
@[inline] def traceFile (self : Module) : FilePath :=
59-
Lean.modToFilePath self.pkg.oleanDir self.name "trace"
68+
self.leanLibPath "trace"
69+
70+
@[inline] def irPath (ext : String) (self : Module) : FilePath :=
71+
self.filePath self.pkg.irDir ext
6072

6173
@[inline] def cFile (self : Module) : FilePath :=
62-
Lean.modToFilePath self.pkg.irDir self.name "c"
74+
self.irPath "c"
6375

6476
@[inline] def cTraceFile (self : Module) : FilePath :=
65-
Lean.modToFilePath self.pkg.irDir self.name "c.trace"
77+
self.irPath "c.trace"
6678

6779
@[inline] def oFile (self : Module) : FilePath :=
68-
Lean.modToFilePath self.pkg.irDir self.name "o"
80+
self.irPath "o"
6981

7082
@[inline] def dynlibName (self : Module) : String :=
7183
-- NOTE: file name MUST be unique on Windows

0 commit comments

Comments
 (0)