src/rules/imports.bend checks

raw source on the hub · import 0xde9bb08f7de298b03207fb5797ede9a5/src/rules/imports.bend as Imports

src/rules/imports: paths and relative imports, as the project rules see them. A path is normalized (no ./, .. applied), an import resolves against the importing file's directory, and a file's closure is every file the linter read that it reaches by relative imports (import ./m.bend as M, import ../x/y.bend as Y). Imports of files that were not read are dropped: nothing is known of them.

3 imports

import Base
import ../syntax/outline.bend as Outline
import ../lazy/lazy.bend as Lazy

Types

type Edge source · line 58 · raw

Data

a file (normalized) and the files it imports relatively (normalized)

Edge

@path:String -> @deps:List<&2, String> -> Edge

Definitions

def norm.put source · line 15 · raw

@+ss:String -> @acc:List<&2, String> -> List<&2, String>

a segment onto the reversed path: . and empty are dropped, .. pops

def norm.go source · line 24 · raw

@segs:List<&2, String> -> @acc:List<&2, String> -> List<&2, String>

def norm source · line 32 · raw

@path:String -> String

a path without ./, ../ and doubled slashes, so two spellings compare

def init source · line 36 · raw

@segs:List<&2, String> -> List<&2, String>

the segments but the last

def dir_of source · line 46 · raw

@path:String -> String

a path's directory, with its slash (src/lsp/; `` at the root)

def resolve source · line 51 · raw

@+from:String -> @rel:String -> String

a path imported from a file, normalized

def targets source · line 62 · raw

@items:List<&2, 0xde9bb08f7de298b03207fb5797ede9a5/src/syntax/outline.Item> -> @+from:String -> List<&2, String>

the relative imports among a file's items, resolved against it

def has source · line 73 · raw

@ps:List<&2, String> -> @+pp:String -> Bool

is the path among them?

def deps.spec source · line 78 · raw

@es:List<&2, Edge> -> @+pp:String -> List<&2, String>

what the file at p imports (nothing when it was not read): the spec deps.first is proven against (src/rules/PROOF.bend imp.deps)

def fresh.spec source · line 88 · raw

@ds:List<&2, String> -> @+seen:List<&2, String> -> @+read:List<&2, String> -> List<&2, String>

the files of ds that were read and are not yet seen, each once: the spec fresh.fast is proven against (imp.fresh)

def paths source · line 98 · raw

@es:List<&2, Edge> -> List<&2, String>

the paths of the files

def walk.spec source · line 109 · raw

@fuel:Nat -> @todo:List<&2, String> -> @+seen:List<&2, String> -> @+es:List<&2, Edge> -> @+read:List<&2, String> -> List<&2, String>

a worklist walk; each read file enters todo once, and a start that was not read imports nothing, so fuel as many as the files never runs out (src/rules/LAWS.bend unsafe_shut). The spec walk is proven against (imp.walk), and what the laws' proofs reason over

def seek source · line 127 · raw

@ps:List<&2, String> -> @+pp:String -> Bool

has, stopping at the first hit

def deps.first source · line 135 · raw

@es:List<&2, Edge> -> @+pp:String -> List<&2, String>

deps.spec, stopping at the first file of that path

def fresh.fast source · line 144 · raw

@ds:List<&2, String> -> @+seen:List<&2, String> -> @+read:List<&2, String> -> List<&2, String>

fresh.spec, asking the short lists first and each only while the answer is open: a target already found or seen is never looked for among every file

def walk source · line 155 · raw

@fuel:Nat -> @todo:List<&2, String> -> @+seen:List<&2, String> -> @+es:List<&2, Edge> -> @+read:List<&2, String> -> List<&2, String>

the walk: walk.spec, step for step, through the lookups above

def closure.go source · line 173 · raw

@es:List<&2, Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> @+from:String -> List<&2, String>

the closure of the file at from, a path normalized already, over the graph