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 ./finding.bend as F
18	
19	# what a file is to the laws
20	type 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
26	def 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?
30	def 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?
38	def 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?
46	def 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
55	def 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
63	def 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)
68	type 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
72	def 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
78	def 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
89	type Mark is Data:
90	  Mark{norm: String, role: Role}
91	
92	# the import graph of the files
93	def 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
101	def 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
109	def 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
118	def 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
127	def 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
132	def 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
141	def 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
146	def 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
163	def 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
169	def 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
178	def of(ms: List<&2, Mark>, +path: String) -> Role:
179	  role.of(of_path(path), of.norm(ms, Imports.norm(path)))