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. 7 import Base 8 import ../syntax/outline.bend as Outline 9 import ../lazy/lazy.bend as Lazy 10 11 # paths 12 # ----- 13 14 # a segment onto the reversed path: `.` and empty are dropped, `..` pops 15 def 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 24 def 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 32 def norm(path: String) -> String: 33 String.join(norm.go(String.split(path, '/'), []), "/") 34 35 # the segments but the last 36 def 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) 46 def 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 51 def 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) 58 type Edge is Data: 59 Edge{path: String, deps: List<&2, String>} 60 61 # the relative imports among a file's items, resolved against it 62 def 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? 73 def 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) 78 def 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) # noqa: C003 the spec deps.first is proven against; only walk.spec runs it 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) 88 def 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 +known = Bool.and(has(read, d), Bool.not(has(seen, d))) 95 Bool.pick(List<&2, String>, Bool.and(known, Bool.not(has(more, d))), d <> more, more) 96 97 # the paths of the files 98 def 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 109 def 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 127 def 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 135 def 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 144 def 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 155 def 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 173 def 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)) 175 176 # a file the trail's walk has queued, and the files it was reached through, 177 # itself first and the start last 178 type Step is Data: 179 Step{at: String, back: List<&2, String>} 180 181 # each file queued, reached through back 182 def steps(ds: List<&2, String>, +back: List<&2, String>) -> List<&2, Step>: 183 match ds: 184 case Nil{}: 185 Nil{} 186 case Con{+d, rest}: 187 Step{d, d <> back} <> steps(rest, back) 188 189 # the walk `walk` takes, breadth first, each queued file carrying how it was 190 # reached, until it takes the file at to: the files from the start to it, in 191 # order; none when the walk never takes it 192 def trail.go( 193 fuel: Nat, 194 todo: List<&2, Step>, 195 +seen: List<&2, String>, 196 +es: List<&2, Edge>, 197 +read: List<&2, String>, 198 +to: String 199 ) -> List<&2, String>: 200 match fuel todo: 201 case 0n t: 202 Nil{} 203 case 1n+f Nil{}: 204 Nil{} 205 case 1n+f Con{Step{+at, +back}, rest}: 206 +found = fresh.fast(deps.first(es, at), seen, read) 207 Lazy.stop(List<&2, String>, String.eq(at, to), List.reverse(&2, String, back), 208 _u => trail.go(f, List.append(&2, Step, rest, steps(found, back)), 209 List.append(&2, String, List.reverse(&2, String, found), seen), es, read, to)) 210 211 # a shortest chain of relative imports from the file at from to the file at 212 # to, both normalized: the files in order, from first and to last 213 def trail(es: List<&2, Edge>, +read: List<&2, String>, +fuel: Nat, +from: String, +to: String) -> List<&2, String>: 214 trail.go(fuel, [Step{from, [from]}], [from], es, read, to)