src/role.bend
bolt@1.22.0.0 · 179 lines · 0 definitions
1# src/role: what a file of the run is to the laws -- a law file, a proof
2# file, or neither. A LAWS.bend is a law file and a PROOF.bend a proof file,
3# by name, as Bend reads them. Any other file is on the laws' side when a
4# LAWS.bend or a PROOF.bend reaches it by relative imports and the code does
5# not: the code is every package's main.bend and every file the laws do not
6# reach, and all they import. On the laws' side, a file a LAWS.bend reaches is
7# a law file and any other a proof file, one only a PROOF.bend reaches, so a
8# proof may state laws of its own. So `LAWS.bend` can be nothing but
9# `import ./laws/x.bend as X` lines, the files it reaches are held to what a
10# law file is held to, and the code they state laws about, which main.bend
11# imports, is still code. Pure.
12import Base
13import bolt@1.22.0.0/src/paths.bend as Paths
14import bolt@1.22.0.0/src/src.bend as Src
15import bolt@1.22.0.0/src/lazy/lazy.bend as Lazy
16import bolt@1.22.0.0/src/rules/imports.bend as Imports
17import bolt@1.22.0.0/src/finding.bend as F
18
19# what a file is to the laws
20type Role is Data:
21 Plain{}
22 Laws{}
23 Proof{}
24
25# a file's role by its name alone: a LAWS.bend, a PROOF.bend, or neither
26def of_path(+path: String) -> Role:
27 Bool.pick(Role, Paths.is_laws(path), Laws{}, Bool.pick(Role, Paths.is_proof(path), Proof{}, Plain{}))
28
29# is it a law file?
30def is_laws(rr: Role) -> Bool:
31 match rr:
32 case Laws{}:
33 True{}
34 case other:
35 False{}
36
37# is it a proof file?
38def is_proof(rr: Role) -> Bool:
39 match rr:
40 case Proof{}:
41 True{}
42 case other:
43 False{}
44
45# is it a law file or a proof file?
46def is_law_file(rr: Role) -> Bool:
47 match rr:
48 case Plain{}:
49 False{}
50 case other:
51 True{}
52
53# a rule that has nothing to say of a law or proof file: its findings on a
54# file told its role, none on one of those
55def skip(+rr: Role, run: Unit -> List<&2, F.Finding>) -> List<&2, F.Finding>:
56 Lazy.stop(List<&2, F.Finding>, is_law_file(rr), [], run)
57
58# reading a file
59# --------------
60
61# what a file on the laws' side is: a law file when a LAWS.bend reaches it,
62# else a proof file
63def reached(laws: Bool) -> Role:
64 Bool.pick(Role, laws, Laws{}, Proof{})
65
66# one file as the walk reads it: its normalized path, what it imports, its
67# role by name, and whether it is a package's entry (a main.bend)
68type Fact is Data:
69 Fact{norm: String, deps: List<&2, String>, named: Role, entry: Bool}
70
71# a parsed file read down to its fact
72def fact(ss: Src.Src) -> Fact:
73 Src.Src{+path, _text, _toks, _tree, _bound, items} = ss
74 +nn = Imports.norm(path)
75 Fact{nn, Imports.targets(items, nn), of_path(path), String.eq(Paths.base(path), "main.bend")}
76
77# every file's fact, in order
78def facts(ss: List<&2, Src.Src>) -> List<&2, Fact>:
79 match ss:
80 case Nil{}:
81 Nil{}
82 case Con{s, rest}:
83 fact(s) <> facts(rest)
84
85# the walks
86# ---------
87
88# a file (normalized) and its role
89type Mark is Data:
90 Mark{norm: String, role: Role}
91
92# the import graph of the files
93def edges(fs: List<&2, Fact>) -> List<&2, Imports.Edge>:
94 match fs:
95 case Nil{}:
96 Nil{}
97 case Con{Fact{norm, deps, _named, _entry}, rest}:
98 Imports.Edge{norm, deps} <> edges(rest)
99
100# the paths of the files
101def paths(fs: List<&2, Fact>) -> List<&2, String>:
102 match fs:
103 case Nil{}:
104 Nil{}
105 case Con{Fact{norm, _deps, _named, _entry}, rest}:
106 norm <> paths(rest)
107
108# the roots of the laws: every LAWS.bend and PROOF.bend
109def roots(fs: List<&2, Fact>) -> List<&2, String>:
110 match fs:
111 case Nil{}:
112 Nil{}
113 case Con{Fact{norm, _deps, +named, _entry}, rest}:
114 +more = roots(rest)
115 Bool.pick(List<&2, String>, is_law_file(named), norm <> more, more)
116
117# the roots of the law files: every LAWS.bend
118def lawful(fs: List<&2, Fact>) -> List<&2, String>:
119 match fs:
120 case Nil{}:
121 Nil{}
122 case Con{Fact{norm, _deps, +named, _entry}, rest}:
123 +more = lawful(rest)
124 Bool.pick(List<&2, String>, is_laws(named), norm <> more, more)
125
126# what the walk from some files reaches, through every file of the run
127def reach(+fs: List<&2, Fact>, +from: List<&2, String>) -> List<&2, String>:
128 Imports.walk(List.length(&2, Fact, fs), from, from, edges(fs), paths(fs))
129
130# the roots of the code: every package's main.bend, and every file the laws
131# do not reach
132def code(fs: List<&2, Fact>, +laws: List<&2, String>) -> List<&2, String>:
133 match fs:
134 case Nil{}:
135 Nil{}
136 case Con{Fact{+norm, _deps, _named, entry}, rest}:
137 +more = code(rest, laws)
138 Bool.pick(List<&2, String>, Bool.or(entry, Bool.not(Imports.has(laws, norm))), norm <> more, more)
139
140# a file's role: its role by name, or else its role on the laws' side
141def role.of(+named: Role, reach: Role) -> Role:
142 Bool.pick(Role, is_law_file(named), named, reach)
143
144# the marks of the files the laws reach and the code does not, in the run's
145# order: a law file when a LAWS.bend reaches it
146def marks.of(
147 fs: List<&2, Fact>,
148 +laws: List<&2, String>,
149 +lawful: List<&2, String>,
150 +code: List<&2, String>
151) -> List<&2, Mark>:
152 match fs:
153 case Nil{}:
154 Nil{}
155 case Con{Fact{+norm, _deps, +named, _entry}, rest}:
156 +more = marks.of(rest, laws, lawful, code)
157 Bool.pick(List<&2, Mark>, Bool.and(Imports.has(laws, norm), Bool.not(Imports.has(code, norm))),
158 Mark{norm, role.of(named, reached(Imports.has(lawful, norm)))} <> more, more)
159
160# the role of every file on the laws' side. Both walks are the one every
161# project rule takes over imports (src/rules/imports.bend), each from all its
162# roots at once
163def marks(ss: List<&2, Src.Src>) -> List<&2, Mark>:
164 +fs = facts(ss)
165 +ls = reach(fs, roots(fs))
166 marks.of(fs, ls, reach(fs, lawful(fs)), reach(fs, code(fs, ls)))
167
168# a normalized path's role among the marks: neither when it is not marked
169def of.norm(ms: List<&2, Mark>, +nn: String) -> Role:
170 match ms:
171 case Nil{}:
172 Plain{}
173 case Con{Mark{+norm, role}, rest}:
174 Lazy.either(Role, String.eq(norm, nn), _u => role, _v => of.norm(rest, nn))
175
176# a file's role among the marks: a LAWS.bend or PROOF.bend by its name, any
177# other file as marked, and neither when it is not marked
178def of(ms: List<&2, Mark>, +path: String) -> Role:
179 role.of(of_path(path), of.norm(ms, Imports.norm(path)))