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.
12	import Base
13	import ./paths.bend as Paths
14	import ./src.bend as Src
15	import ./lazy/lazy.bend as Lazy
16	import ./rules/imports.bend as Imports
17	import ./syntax/lex.bend as Lex
18	import ./syntax/outline.bend as Outline
19	import ./finding.bend as F
20	
21	# what a file is to the laws
22	type 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
28	def 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?
32	def 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?
40	def 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?
48	def 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
57	def 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
65	def 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)
70	type 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
74	def 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
81	def 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
87	def 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
98	type Mark is Data:
99	  Mark{norm: String, role: Role}
100	
101	# the import graph of the files
102	def 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
110	def 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
118	def 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
127	def 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
136	def 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
141	def 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
150	def 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
155	def 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
170	def 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
177	def 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
182	def 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
191	def of(ms: List<&2, Mark>, +path: String) -> Role:
192	  role.of(of_path(path), of.norm(ms, Imports.norm(path)))