Skip to content

Commit 7aee7c9

Browse files
RussoulRussoul
authored
[ new ] --install-with-src; refactoring around FCs (#1450)
Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
1 parent baa6051 commit 7aee7c9

File tree

143 files changed

+918
-619
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

143 files changed

+918
-619
lines changed

‎Makefile

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -149,6 +149,9 @@ install: install-idris2 install-support install-libs
149149
install-api: src/IdrisPaths.idr
150150
${IDRIS2_BOOT} --install ${IDRIS2_LIB_IPKG}
151151

152+
install-with-src-api: src/IdrisPaths.idr
153+
${IDRIS2_BOOT} --install-with-src ${IDRIS2_LIB_IPKG}
154+
152155
install-idris2:
153156
mkdir -p ${PREFIX}/bin/
154157
install ${TARGET} ${PREFIX}/bin
@@ -180,6 +183,12 @@ install-libs:
180183
${MAKE} -C libs/network install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
181184
${MAKE} -C libs/test install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
182185

186+
install-with-src-libs:
187+
${MAKE} -C libs/prelude install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
188+
${MAKE} -C libs/base install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
189+
${MAKE} -C libs/contrib install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
190+
${MAKE} -C libs/network install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
191+
${MAKE} -C libs/test install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
183192

184193
.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean
185194

‎libs/base/Language/Reflection/TT.idr

Lines changed: 40 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -4,20 +4,54 @@ import public Data.List
44

55
%default total
66

7+
public export
8+
data Namespace = MkNS (List String) -- namespace, stored in reverse order
9+
10+
public export
11+
data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order
12+
13+
export
14+
showSep : String -> List String -> String
15+
showSep sep [] = ""
16+
showSep sep [x] = x
17+
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
18+
19+
export
20+
Show Namespace where
21+
show (MkNS ns) = showSep "." (reverse ns)
22+
723
-- 'FilePos' represents the position of
824
-- the source information in the file (or REPL).
925
-- in the form of '(line-no, column-no)'.
1026
public export
1127
FilePos : Type
1228
FilePos = (Int, Int)
1329

14-
-- 'FC' represents the source location of the term.
15-
-- The first 'FilePos' indicates the starting position.
16-
-- the second 'FilePos' indicates the start of the next term.
1730
public export
18-
data FC : Type where
19-
MkFC : String -> FilePos -> FilePos -> FC
20-
EmptyFC : FC
31+
data VirtualIdent : Type where
32+
Interactive : VirtualIdent
33+
34+
public export
35+
data OriginDesc : Type where
36+
||| Anything that originates in physical Idris source files is assigned a
37+
||| `PhysicalIdrSrc modIdent`,
38+
||| where `modIdent` is the top-level module identifier of that file.
39+
PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
40+
||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
41+
||| where `fname` is path to the package file.
42+
PhysicalPkgSrc : (fname : String) -> OriginDesc
43+
Virtual : (ident : VirtualIdent) -> OriginDesc
44+
45+
||| A file context is a filename together with starting and ending positions.
46+
||| It's often carried by AST nodes that might have been created from a source
47+
||| file or by the compiler. That makes it useful to have the notion of
48+
||| `EmptyFC` as part of the type.
49+
public export
50+
data FC = MkFC OriginDesc FilePos FilePos
51+
| ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
52+
||| errors, but we shouldn't attach semantic highlighting metadata to them.
53+
MkVirtualFC OriginDesc FilePos FilePos
54+
| EmptyFC
2155

2256
public export
2357
emptyFC : FC
@@ -54,19 +88,6 @@ data Constant
5488
| DoubleType
5589
| WorldType
5690

57-
public export
58-
data Namespace = MkNS (List String) -- namespace, stored in reverse order
59-
60-
export
61-
showSep : String -> List String -> String
62-
showSep sep [] = ""
63-
showSep sep [x] = x
64-
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
65-
66-
export
67-
Show Namespace where
68-
show (MkNS ns) = showSep "." (reverse ns)
69-
7091
public export
7192
data Name = UN String -- user defined name
7293
| MN String Int -- machine generated name

‎libs/base/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ all:
44
install:
55
${IDRIS2} --install base.ipkg
66

7+
install-with-src:
8+
${IDRIS2} --install-with-src base.ipkg
9+
710
docs:
811
${IDRIS2} --mkdoc base.ipkg
912

‎libs/contrib/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ all:
44
install:
55
${IDRIS2} --install contrib.ipkg
66

7+
install-with-src:
8+
${IDRIS2} --install-with-src contrib.ipkg
9+
710
docs:
811
${IDRIS2} --mkdoc contrib.ipkg
912

‎libs/network/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ all:
44
install:
55
${IDRIS2} --install network.ipkg
66

7+
install-with-src:
8+
${IDRIS2} --install-with-src network.ipkg
9+
710
docs:
811
${IDRIS2} --mkdoc network.ipkg
912

‎libs/prelude/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ all:
44
install:
55
${IDRIS2} --install prelude.ipkg
66

7+
install-with-src:
8+
${IDRIS2} --install-with-src prelude.ipkg
9+
710
docs:
811
${IDRIS2} --mkdoc prelude.ipkg
912

‎libs/test/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ all:
44
install:
55
${IDRIS2} --install test.ipkg
66

7+
install-with-src:
8+
${IDRIS2} --install-with-src test.ipkg
9+
710
docs:
811
${IDRIS2} --mkdoc test.ipkg
912

‎src/Core/Directory.idr

Lines changed: 54 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,33 @@ import System.Info
1818

1919
%default total
2020

21+
public export
22+
data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md
23+
24+
public export
25+
Eq IdrSrcExt where
26+
E_idr == E_idr = True
27+
E_lidr == E_lidr = True
28+
E_yaff == E_yaff = True
29+
E_org == E_org = True
30+
E_md == E_md = True
31+
_ == _ = False
32+
33+
public export
34+
Show IdrSrcExt where
35+
show E_idr = "idr"
36+
show E_lidr = "lidr"
37+
show E_yaff = "yaff"
38+
show E_org = "org"
39+
show E_md = "md"
40+
41+
public export
42+
listOfExtensions : List IdrSrcExt
43+
listOfExtensions = [E_idr, E_lidr, E_yaff, E_org, E_md]
44+
2145
-- Return the name of the first file available in the list
46+
-- Used in LSP.
47+
export
2248
firstAvailable : {auto c : Ref Ctxt Defs} ->
2349
List String -> Core (Maybe String)
2450
firstAvailable [] = pure Nothing
@@ -73,7 +99,7 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
7399
FC -> ModuleIdent -> Core (Either Error String)
74100
nsToPath loc ns
75101
= do d <- getDirs
76-
let fnameBase = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
102+
let fnameBase = ModuleIdent.toPath ns
77103
let fs = map (\p => p </> fnameBase <.> "ttc")
78104
((build_dir d </> "ttc") :: extra_dirs d)
79105
Just f <- firstAvailable fs
@@ -87,31 +113,42 @@ nsToSource : {auto c : Ref Ctxt Defs} ->
87113
FC -> ModuleIdent -> Core String
88114
nsToSource loc ns
89115
= do d <- getDirs
90-
let fnameOrig = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
116+
let fnameOrig = ModuleIdent.toPath ns
91117
let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
92-
let fs = map (\ext => fnameBase <.> ext)
93-
[".idr", ".lidr", ".yaff", ".org", ".md"]
118+
let fs = map ((fnameBase <.>) . show) listOfExtensions
94119
Just f <- firstAvailable fs
95120
| Nothing => throw (ModuleNotFound loc ns)
96121
pure f
97122

98123
-- Given a filename in the working directory + source directory, return the correct
99124
-- namespace for it
100125
export
101-
pathToNS : String -> Maybe String -> String -> Core ModuleIdent
102-
pathToNS wdir sdir fname =
126+
mbPathToNS : String -> Maybe String -> String -> Maybe ModuleIdent
127+
mbPathToNS wdir sdir fname =
103128
let
104129
sdir = fromMaybe "" sdir
105130
base = if isAbsolute fname then wdir </> sdir else sdir
106131
in
107-
case Path.dropBase base fname of
108-
Nothing => throw (UserError (
132+
unsafeFoldModuleIdent . reverse . splitPath . Path.dropExtension
133+
<$> Path.dropBase base fname
134+
135+
export
136+
corePathToNS : String -> Maybe String -> String -> Core ModuleIdent
137+
corePathToNS wdir sdir fname = do
138+
let err = UserError $
109139
"Source file "
110-
++ show fname
111-
++ " is not in the source directory "
112-
++ show (wdir </> sdir)))
113-
Just relPath =>
114-
pure $ unsafeFoldModuleIdent $ reverse $ splitPath $ Path.dropExtension relPath
140+
++ show fname
141+
++ " is not in the source directory "
142+
++ show (wdir </> fromMaybe "" sdir)
143+
maybe (throw err) pure (mbPathToNS wdir sdir fname)
144+
145+
export
146+
ctxtPathToNS : {auto c : Ref Ctxt Defs} -> String -> Core ModuleIdent
147+
ctxtPathToNS fname = do
148+
defs <- get Ctxt
149+
let wdir = defs.options.dirs.working_dir
150+
let sdir = defs.options.dirs.source_dir
151+
corePathToNS wdir sdir fname
115152

116153
dirExists : String -> IO Bool
117154
dirExists dir = do Right d <- openDir dir
@@ -162,12 +199,11 @@ export
162199
getTTCFileName : {auto c : Ref Ctxt Defs} ->
163200
String -> String -> Core String
164201
getTTCFileName inp ext
165-
= do ns <- getNS
166-
d <- getDirs
167-
-- Get its namespace from the file relative to the working directory
202+
= do -- Get its namespace from the file relative to the working directory
168203
-- and generate the ttc file from that
169-
ns <- pathToNS (working_dir d) (source_dir d) inp
170-
let fname = joinPath (reverse $ unsafeUnfoldModuleIdent ns) <.> ext
204+
ns <- ctxtPathToNS inp
205+
let fname = ModuleIdent.toPath ns <.> ext
206+
d <- getDirs
171207
let bdir = build_dir d
172208
pure $ bdir </> "ttc" </> fname
173209

0 commit comments

Comments
 (0)