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