1	# layout/case: a name whose case does not follow the kind of what it names.
2	# Fix: renames the declaration, with its uses.
3	# Heuristics: the kind comes from the syntax and the written types, not from the checker:
4	#
5	# | Kind                                              | Case              | Examples                     |
6	# | ------------------------------------------------- | ----------------- | ---------------------------- |
7	# | type, constructor, import alias                   | PascalCase        | `Maybe`, `Some{}`, `M`       |
8	# | def whose written return type ends in a sort      | PascalCase        | `IO`, `Pair`, `Set()`        |
9	# | parameter or field whose written type ends in one | PascalCase        | `-A: Type`, `F: U32 -> Type` |
10	# | law, other def, parameter or field                | snake_case        | `add_comm`, `from_list`, `n` |
11	# | variable, lambda, forall, def without a return    | either            | `Big`, `small`               |
12	# | namespace segment                                 | its parent's case | `IO.print`, `Set.from_list`  |
13	#
14	# A sort is `Type`, `Data` or `Kind(..)`; a type ends in one when it is one, or a function type whose
15	# result does. A binder written bare (`<a>`, `(x)`) is a quantity, so snake_case. PascalCase is a
16	# capital, then letters and digits: `IO`, `OP` and `U32` pass. snake_case has no capital. A dotted
17	# name is checked by its last segment; the segments before it name its parent, checked where the parent
18	# is declared. `import Base`, and a def that fills a law of another file, are skipped: their names are
19	# not this file's to choose.
20	import Base
21	import bend-lint-api@0.2.1.0/linter/lint.bend as Lint
22	import bend-lint-api@0.2.1.0/shared/lists.bend as Lists
23	import bend-lint-api@0.2.1.0/shared/strings.bend as Strings
24	
25	# Types
26	# =====
27	type Case is Data:
28	  Pascal{}
29	  Snake{}
30	  Either{}
31	
32	# Case
33	# ====
34	def has_no_underscore(s: String) -> Bool:
35	  match s:
36	    case SNil{}:
37	      True{}
38	    case SCon{'_', rest}:
39	      False{}
40	    case SCon{c, rest}:
41	      has_no_underscore(rest)
42	
43	def has_no_capital(s: String, ok: Bool) -> Bool:
44	  match s ok:
45	    case _ False{}:
46	      False{}
47	    case SNil{} True{}:
48	      True{}
49	    case SCon{c, rest} True{}:
50	      has_no_capital(rest, Bool.not(Char.is_upper(c)))
51	
52	def is_pascal.rest(upper: Bool, rest: String) -> Bool:
53	  match upper:
54	    case True{}:
55	      has_no_underscore(rest)
56	    case False{}:
57	      False{}
58	
59	def is_pascal(s: String) -> Bool:
60	  match s:
61	    case SCon{c, rest}:
62	      is_pascal.rest(Char.is_upper(c), rest)
63	    case SNil{}:
64	      False{}
65	
66	def is_snake.of(empty: Bool, s: String) -> Bool:
67	  match empty:
68	    case True{}:
69	      False{}
70	    case False{}:
71	      has_no_capital(s, True{})
72	
73	def is_snake(+s: String) -> Bool:
74	  is_snake.of(String.is_empty(s), s)
75	
76	def fits(want: Case, +s: String) -> Bool:
77	  match want:
78	    case Pascal{}:
79	      is_pascal(s)
80	    case Snake{}:
81	      is_snake(s)
82	    case Either{}:
83	      Bool.or(is_pascal(s), is_snake(s))
84	
85	def has_small_head(s: String) -> Bool:
86	  match s:
87	    case SCon{c, rest}:
88	      Char.is_lower(c)
89	    case SNil{}:
90	      False{}
91	
92	def has_capital_head(s: String) -> Bool:
93	  match s:
94	    case SCon{c, rest}:
95	      Char.is_upper(c)
96	    case SNil{}:
97	      False{}
98	
99	def snake_cap(cut: Bool, c: Char, acc: String) -> String:
100	  match cut:
101	    case True{}:
102	      SCon{Char.to_lower(c), SCon{'_', acc}}
103	    case False{}:
104	      SCon{Char.to_lower(c), acc}
105	
106	# `s` in snake_case: a word starts at a capital after a small letter or digit, or at the last capital of a run before a
107	# small letter. `capital`: whether `s` starts with a capital. `prev`: the character before is none or `_` (0), a small
108	# letter or digit (1), or a capital (2). `acc`: the result so far, last character first.
109	def snake(s: String, capital: Bool, +prev: U32, acc: String) -> String:
110	  match s capital:
111	    case SNil{} _:
112	      String.reverse(acc)
113	    case SCon{c, +rest} True{}:
114	      snake(
115	        rest,
116	        has_capital_head(rest),
117	        2,
118	        snake_cap(
119	          Bool.or(U32.is_eq(prev, 1), Bool.and(U32.is_eq(prev, 2), has_small_head(rest))),
120	          c,
121	          acc
122	        )
123	      )
124	    case SCon{+c, +rest} False{}:
125	      snake(rest, has_capital_head(rest), Bool.pick(U32, Char.is_eq(c, '_'), 0, 1), SCon{c, acc})
126	
127	# `s` in PascalCase: `_` goes, and the character after it becomes a capital.
128	def pascal(s: String, up: Bool, acc: String) -> String:
129	  match s up:
130	    case SNil{} _:
131	      String.reverse(acc)
132	    case SCon{'_', rest} _:
133	      pascal(rest, True{}, acc)
134	    case SCon{c, rest} True{}:
135	      pascal(rest, False{}, SCon{Char.to_upper(c), acc})
136	    case SCon{c, rest} False{}:
137	      pascal(rest, False{}, SCon{c, acc})
138	
139	def recased(want: Case, +s: String) -> String:
140	  match want:
141	    case Pascal{}:
142	      pascal(s, True{}, "")
143	    case _:
144	      snake(s, has_capital_head(s), 0, "")
145	
146	# Written types
147	# =============
148	
149	# Whether the type the last of `nodes` writes ends in a sort: it is one, or a function type whose result does.
150	def ends(nodes: List<&2, Lint.Node>) -> Bool:
151	  match nodes:
152	    case Con{Lint.Node{Lint.Sort{}, n, s, k, f}, Nil{}}:
153	      True{}
154	    case Con{Lint.Node{Lint.Forall{b, q}, n, s, kids, f}, Nil{}}:
155	      ends(kids)
156	    case Con{x, Nil{}}:
157	      False{}
158	    case Con{x, rest}:
159	      ends(rest)
160	    case Nil{}:
161	      False{}
162	
163	# The case of a name whose written type is the last of `nodes`: none written, either.
164	def typed(+nodes: List<&2, Lint.Node>) -> Case:
165	  match nodes:
166	    case Nil{}:
167	      Either{}
168	    case _:
169	      Bool.pick(Case, ends(nodes), Pascal{}, Snake{})
170	
171	# The case of a def's name, by its written return type, among its nodes.
172	def returns(nodes: List<&2, Lint.Node>) -> Case:
173	  match nodes:
174	    case Nil{}:
175	      Either{}
176	    case Con{Lint.Node{Lint.Returns{}, n, s, kids, f}, rest}:
177	      typed(kids)
178	    case Con{x, rest}:
179	      returns(rest)
180	
181	# Rule
182	# ====
183	
184	# The case a declaration's name takes, if the file chooses it.
185	def wanted(+node: Lint.Node, namespace: String) -> Maybe<&2, Case>:
186	  match node:
187	    case Lint.Node{Lint.Import{t}, name, s, k, f}:
188	      Lists.when(Case, Bool.not(String.eq(name, "Base")), Pascal{})
189	    case Lint.Node{Lint.Datatype{t}, name, s, k, f}:
190	      Some{Pascal{}}
191	    case Lint.Node{Lint.Constructor{t}, name, s, k, f}:
192	      Some{Pascal{}}
193	    case Lint.Node{Lint.Law{t}, name, s, k, f}:
194	      Some{Snake{}}
195	    case Lint.Node{Lint.Definition{t, u}, name, s, kids, f}:
196	      Lists.when(Case, String.eq(Lint.Name.namespace(t), namespace), returns(kids))
197	    case Lint.Node{Lint.Parameter{b, q}, name, s, kids, f}:
198	      Some{typed(kids)}
199	    case Lint.Node{Lint.Field{b, q}, name, s, kids, f}:
200	      Some{typed(kids)}
201	    case _:
202	      Some{Either{}}
203	
204	# A name of `syntax`, in a message. `sort`: whether it is a type.
205	def noun(syntax: Lint.Syntax, sort: Bool) -> String:
206	  match syntax sort:
207	    case Lint.Import{t} _:
208	      "an import alias"
209	    case Lint.Datatype{t} _:
210	      "a type"
211	    case Lint.Constructor{t} _:
212	      "a constructor"
213	    case Lint.Law{t} _:
214	      "a law"
215	    case Lint.Definition{t, u} True{}:
216	      "a def that returns a type"
217	    case Lint.Definition{t, u} False{}:
218	      "a def that does not return a type"
219	    case Lint.Parameter{b, q} True{}:
220	      "a parameter that is a type"
221	    case Lint.Parameter{b, q} False{}:
222	      "a parameter that is not a type"
223	    case Lint.Field{b, q} True{}:
224	      "a field that is a type"
225	    case Lint.Field{b, q} False{}:
226	      "a field that is not a type"
227	    case _ _:
228	      "a variable"
229	
230	def what(syntax: Lint.Syntax, want: Case) -> String:
231	  match want:
232	    case Pascal{}:
233	      noun(syntax, True{}) ++ " is PascalCase"
234	    case Snake{}:
235	      noun(syntax, False{}) ++ " is snake_case"
236	    case Either{}:
237	      "this name is snake_case, or PascalCase if it is a type"
238	
239	# Whether a name is a binder's: only its own declaration names it, so a rename touches no other file.
240	def is_local.of(declares: Maybe<&2, Bool>) -> Bool:
241	  match declares:
242	    case Some{False{}}:
243	      True{}
244	    case _:
245	      False{}
246	
247	def is_local(syntax: Lint.Syntax) -> Bool:
248	  is_local.of(Lint.Syntax.declares(syntax))
249	
250	# The fix that renames a local name to `to`, if recasing made one that fits.
251	def renames(ok: Bool, at: Lint.Span, full: String, to: String) -> List<&2, Lint.Fix>:
252	  match ok:
253	    case True{}:
254	      [Lint.Fix{"Rename to " ++ full, [Lint.Rename{at, to}]}]
255	    case False{}:
256	      []
257	
258	# The finding for a name that does not fit: it says the new name when recasing makes one that fits, and, for a local
259	# name, offers the rename.
260	def misfit(
261	  +syntax: Lint.Syntax,
262	  +want: Case,
263	  +name: String,
264	  +span: Lint.Span
265	) -> List<&2, Lint.Finding>:
266	  +seg = Strings.after_last(name, '.')
267	  +to = String.take(name, Nat.sub(String.length(name), String.length(seg))) ++ recased(want, seg)
268	  +ok = fits(want, recased(want, seg))
269	  rename = Bool.pick(String, ok, "Rename " ++ name ++ " to " ++ to, "Rename " ++ name)
270	  [
271	    Lint.Finding{
272	      Lint.Warning{},
273	      span,
274	      rename ++ ": " ++ what(syntax, want) ++ ".",
275	      renames(Bool.and(ok, is_local(syntax)), span, to, recased(want, seg))
276	    }
277	  ]
278	
279	def verdict(
280	  fit: Bool,
281	  syntax: Lint.Syntax,
282	  want: Case,
283	  name: String,
284	  span: Lint.Span
285	) -> List<&2, Lint.Finding>:
286	  match fit:
287	    case True{}:
288	      []
289	    case False{}:
290	      misfit(syntax, want, name, span)
291	
292	def judged(
293	  want: Maybe<&2, Case>,
294	  syntax: Lint.Syntax,
295	  +name: String,
296	  span: Lint.Span
297	) -> List<&2, Lint.Finding>:
298	  match want:
299	    case Some{+w}:
300	      verdict(fits(w, Strings.after_last(name, '.')), syntax, w, name, span)
301	    case None{}:
302	      []
303	
304	def judge(
305	  +namespace: String,
306	  declarations: List<&2, Lint.Declaration>,
307	  out: List<&2, Lint.Finding>
308	) -> List<&2, Lint.Finding>:
309	  match declarations:
310	    case Nil{}:
311	      List.reverse(&2, Lint.Finding, out)
312	    case Con{Lint.Declaration{Lint.Node{+syntax, +name, Some{+span}, kids, facts}, uses}, rest}:
313	      judge(
314	        namespace,
315	        rest,
316	        Lists.onto(
317	          &2,
318	          Lint.Finding,
319	          judged(
320	            wanted(Lint.Node{syntax, name, Some{span}, kids, facts}, namespace),
321	            syntax,
322	            name,
323	            span
324	          ),
325	          out
326	        )
327	      )
328	    case Con{d, rest}:
329	      judge(namespace, rest, out)
330	
331	def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
332	  Lint.done(judge(Lint.Here.namespace(here), Lint.Here.declarations(here), []))
333	
334	def rule() -> Lint.Rule:
335	  Lint.Rule{Lint.Needs{False{}, True{}}, [], Lint.OnFile{run}}