src/role.bend

bolt@1.27.0.0 · 192 lines · 24 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.27.0.0/src/paths.bend as Paths
14import bolt@1.27.0.0/src/src.bend as Src
15import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
16import bolt@1.27.0.0/src/rules/imports.bend as Imports
17import bolt@1.27.0.0/src/syntax/lex.bend as Lex
18import bolt@1.27.0.0/src/syntax/outline.bend as Outline
19import bolt@1.27.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)))