src/rules/imports.bend
bolt@1.11.0.0 · 174 lines · 0 definitions
1# src/rules/imports: paths and relative imports, as the project rules see
2# them. A path is normalized (no `./`, `..` applied), an import resolves
3# against the importing file's directory, and a file's closure is every file
4# the linter read that it reaches by relative imports (`import ./m.bend as M`,
5# `import ../x/y.bend as Y`). Imports of files that were not read are dropped:
6# nothing is known of them.
7import Base
8import bolt@1.11.0.0/src/syntax/outline.bend as Outline
9import bolt@1.11.0.0/src/lazy/lazy.bend as Lazy
10
11# paths
12# -----
13
14# a segment onto the reversed path: `.` and empty are dropped, `..` pops
15def norm.put(+ss: String, acc: List<&2, String>) -> List<&2, String>:
16 match acc:
17 case Con{+h, +t}:
18 Bool.pick(List<&2, String>, String.eq(ss, ".."), t,
19 Bool.pick(List<&2, String>, Bool.or(String.eq(ss, "."), String.is_empty(ss)), h <> t, ss <> (h <> t)))
20 case Nil{}:
21 Bool.pick(List<&2, String>, Bool.or(String.eq(ss, ".."), Bool.or(String.eq(ss, "."), String.is_empty(ss))),
22 [], [ss])
23
24def norm.go(segs: List<&2, String>, acc: List<&2, String>) -> List<&2, String>:
25 match segs:
26 case Nil{}:
27 List.reverse(&2, String, acc)
28 case Con{+s, rest}:
29 norm.go(rest, norm.put(s, acc))
30
31# a path without `./`, `../` and doubled slashes, so two spellings compare
32def norm(path: String) -> String:
33 String.join(norm.go(String.split(path, '/'), []), "/")
34
35# the segments but the last
36def init(segs: List<&2, String>) -> List<&2, String>:
37 match segs:
38 case Nil{}:
39 Nil{}
40 case Con{h, Nil{}}:
41 Nil{}
42 case Con{h, t}:
43 h <> init(t)
44
45# a path's directory, with its slash (`src/lsp/`; `` at the root)
46def dir_of(path: String) -> String:
47 +segs = init(String.split(norm(path), '/'))
48 Bool.pick(String, Nat.is_eq(List.length(&2, String, segs), 0n), "", String.join(segs, "/") ++ "/")
49
50# a path imported from a file, normalized
51def resolve(+from: String, rel: String) -> String:
52 norm(dir_of(from) ++ rel)
53
54# the import graph
55# ----------------
56
57# a file (normalized) and the files it imports relatively (normalized)
58type Edge is Data:
59 Edge{path: String, deps: List<&2, String>}
60
61# the relative imports among a file's items, resolved against it
62def targets(items: List<&2, Outline.Item>, +from: String) -> List<&2, String>:
63 match items:
64 case Nil{}:
65 Nil{}
66 case Con{Outline.Item{Outline.IImport{}, name, line, sig, doc, +path}, rest}:
67 +more = targets(rest, from)
68 Lazy.stop(List<&2, String>, Bool.not(String.starts_with(path, ".")), more, _u => resolve(from, path) <> more)
69 case Con{other, rest}:
70 targets(rest, from)
71
72# is the path among them?
73def has(ps: List<&2, String>, +pp: String) -> Bool:
74 List.contains(~String, ~String.eq, ps, pp)
75
76# what the file at p imports (nothing when it was not read): the spec
77# deps.first is proven against (src/rules/PROOF.bend imp.deps)
78def deps.spec(es: List<&2, Edge>, +pp: String) -> List<&2, String>:
79 match es:
80 case Nil{}:
81 Nil{}
82 case Con{Edge{+ep, ds}, rest}:
83 +more = deps.spec(rest, pp)
84 Bool.pick(List<&2, String>, String.eq(ep, pp), ds, more)
85
86# the files of ds that were read and are not yet seen, each once: the spec
87# fresh.fast is proven against (imp.fresh)
88def fresh.spec(ds: List<&2, String>, +seen: List<&2, String>, +read: List<&2, String>) -> List<&2, String>:
89 match ds:
90 case Nil{}:
91 Nil{}
92 case Con{+d, rest}:
93 +more = fresh.spec(rest, seen, read)
94 Bool.pick(List<&2, String>, Bool.and(Bool.and(has(read, d), Bool.not(has(seen, d))), Bool.not(has(more, d))),
95 d <> more, more)
96
97# the paths of the files
98def paths(es: List<&2, Edge>) -> List<&2, String>:
99 match es:
100 case Nil{}:
101 Nil{}
102 case Con{Edge{p, ds}, rest}:
103 p <> paths(rest)
104
105# a worklist walk; each read file enters todo once, and a start that was
106# not read imports nothing, so fuel as many as the files never runs out
107# (src/rules/LAWS.bend unsafe_shut). The spec `walk` is proven against
108# (imp.walk), and what the laws' proofs reason over
109def walk.spec(
110 fuel: Nat,
111 todo: List<&2, String>,
112 +seen: List<&2, String>,
113 +es: List<&2, Edge>,
114 +read: List<&2, String>
115) -> List<&2, String>:
116 match fuel todo:
117 case 0n t:
118 seen
119 case 1n+f Nil{}:
120 seen
121 case 1n+f Con{p, rest}:
122 +found = fresh.spec(deps.spec(es, p), seen, read)
123 walk.spec(f, List.append(&2, String, found, rest), List.append(&2, String, List.reverse(&2, String, found), seen),
124 es, read)
125
126# `has`, stopping at the first hit
127def seek(ps: List<&2, String>, +pp: String) -> Bool:
128 match ps:
129 case Nil{}:
130 False{}
131 case Con{p, rest}:
132 Lazy.or_else(String.eq(p, pp), _u => seek(rest, pp))
133
134# `deps.spec`, stopping at the first file of that path
135def deps.first(es: List<&2, Edge>, +pp: String) -> List<&2, String>:
136 match es:
137 case Nil{}:
138 Nil{}
139 case Con{Edge{ep, ds}, rest}:
140 Lazy.stop(List<&2, String>, String.eq(ep, pp), ds, _u => deps.first(rest, pp))
141
142# `fresh.spec`, asking the short lists first and each only while the answer is
143# open: a target already found or seen is never looked for among every file
144def fresh.fast(ds: List<&2, String>, +seen: List<&2, String>, +read: List<&2, String>) -> List<&2, String>:
145 match ds:
146 case Nil{}:
147 Nil{}
148 case Con{+d, rest}:
149 +more = fresh.fast(rest, seen, read)
150 Bool.pick(List<&2, String>,
151 Lazy.and_then(Bool.not(seek(more, d)), _u => Lazy.and_then(Bool.not(seek(seen, d)), _v => seek(read, d))),
152 d <> more, more)
153
154# the walk: `walk.spec`, step for step, through the lookups above
155def walk(
156 fuel: Nat,
157 todo: List<&2, String>,
158 +seen: List<&2, String>,
159 +es: List<&2, Edge>,
160 +read: List<&2, String>
161) -> List<&2, String>:
162 match fuel todo:
163 case 0n t:
164 seen
165 case 1n+f Nil{}:
166 seen
167 case 1n+f Con{p, rest}:
168 +found = fresh.fast(deps.first(es, p), seen, read)
169 walk(f, List.append(&2, String, found, rest), List.append(&2, String, List.reverse(&2, String, found), seen), es,
170 read)
171
172# the closure of the file at from, a path normalized already, over the graph
173def closure.go(es: List<&2, Edge>, +read: List<&2, String>, +fuel: Nat, +from: String) -> List<&2, String>:
174 List.reverse(&2, String, walk(fuel, [from], [from], es, read))