1	import Base
2	
3	# One declared or observed setting of the Mac: its nix-darwin option, how to write its value, and the value.
4	# KNix values are whole Nix expressions (lists, attribute sets, paths), written as they are.
5	# Values are kept exactly as nix-darwin would write them, so declared and observed compare directly.
6	type VKind is Data:
7	  KBool{}
8	  KInt{}
9	  KFloat{}
10	  KStr{}
11	  KNix{}
12	
13	type Setting is Data:
14	  Setting{option: String, kind: VKind, value: String}
15	
16	type Change is Data:
17	  Change{option: String, now: String, want: String}
18	
19	def cmp_eq(c: Cmp) -> Bool:
20	  match c:
21	    case EQ{}:
22	      True{}
23	    case _:
24	      False{}
25	
26	def snd_eq(r: (String & String) & Cmp) -> Bool:
27	  match r:
28	    case (_, c):
29	      cmp_eq(c)
30	
31	def str_eq(a: String, b: String) -> Bool:
32	  snd_eq(String.cmp(a, b))
33	
34	def option_of(s: Setting) -> String:
35	  match s:
36	    case Setting{o, _, _}:
37	      o
38	
39	def value_of(s: Setting) -> String:
40	  match s:
41	    case Setting{_, _, v}:
42	      v
43	
44	# The observed value of `option`, or "(unset)".
45	
46	def pick_value(hit: Bool, s: Setting, other: String) -> String:
47	  match hit:
48	    case True{}:
49	      value_of(s)
50	    case False{}:
51	      other
52	
53	
54	def lookup(+option: String, now: List<&2, Setting>) -> String:
55	  match now:
56	    case []:
57	      "(unset)"
58	    case +s <> rest:
59	      pick_value(str_eq(option, option_of(s)), s, lookup(option, rest))
60	
61	def change_if(same: Bool, option: String, now: String, want: String, rest: List<&2, Change>) -> List<&2, Change>:
62	  match same:
63	    case True{}:
64	      rest
65	    case False{}:
66	      Change{option, now, want} <> rest
67	
68	# Dry run: every declared setting whose observed value differs.
69	
70	def change_if_str(+observed: String, option: String, +value: String, rest: List<&2, Change>) -> List<&2, Change>:
71	  change_if(str_eq(observed, value), option, observed, value, rest)
72	
73	# The nix literal for a value.
74	
75	def diff_one(s: Setting, +now: List<&2, Setting>, rest: List<&2, Change>) -> List<&2, Change>:
76	  match s:
77	    case Setting{+option, _, +value}:
78	      change_if_str(lookup(option, now), option, value, rest)
79	
80	def diff(want: List<&2, Setting>, +now: List<&2, Setting>) -> List<&2, Change>:
81	  match want:
82	    case []:
83	      []
84	    case s <> rest:
85	      diff_one(s, now, diff(rest, now))
86	
87	def literal(k: VKind, v: String) -> String:
88	  match k:
89	    case KStr{}:
90	      "\"" ++ v ++ "\""
91	    case _:
92	      v
93	
94	def line(s: Setting) -> String:
95	  match s:
96	    case Setting{option, k, v}:
97	      "  " ++ option ++ " = " ++ literal(k, v) ++ ";\n"
98	
99	def lines(xs: List<&2, Setting>) -> String:
100	  match xs:
101	    case []:
102	      ""
103	    case s <> rest:
104	      line(s) ++ lines(rest)
105	
106	# A Homebrew entry: kind is "tap", "brew", "cask", "mas" (name is the Nix attribute `"App" = id`) or "other" (a raw Brewfile line).
107	type Brew is Data:
108	  Brew{kind: String, name: String}
109	
110	def brew_key(b: Brew) -> String:
111	  match b:
112	    case Brew{k, n}:
113	      k ++ " " ++ n
114	
115	def keys(xs: List<&2, Brew>) -> List<&2, String>:
116	  match xs:
117	    case []:
118	      []
119	    case b <> rest:
120	      brew_key(b) <> keys(rest)
121	
122	def has(+s: String, xs: List<&2, String>) -> Bool:
123	  match xs:
124	    case []:
125	      False{}
126	    case x <> rest:
127	      str_eq(s, x) || has(s, rest)
128	
129	def keep_if(missing: Bool, k: String, rest: List<&2, String>) -> List<&2, String>:
130	  match missing:
131	    case True{}:
132	      k <> rest
133	    case False{}:
134	      rest
135	
136	# Entries of `a` that are not in `b`.
137	def minus(a: List<&2, String>, +b: List<&2, String>) -> List<&2, String>:
138	  match a:
139	    case []:
140	      []
141	    case +k <> rest:
142	      keep_if(Bool.not(has(k, b)), k, minus(rest, b))
143	
144	# Nix for the Homebrew section: one list per kind; entries nix-darwin has no option for are raw Brewfile lines.
145	def kind_of(b: Brew) -> String:
146	  match b:
147	    case Brew{k, _}:
148	      k
149	
150	def name_of(b: Brew) -> String:
151	  match b:
152	    case Brew{_, n}:
153	      n
154	
155	def quoted_if(hit: Bool, n: String) -> String:
156	  match hit:
157	    case True{}:
158	      " \"" ++ n ++ "\""
159	    case False{}:
160	      ""
161	
162	def names(+k: String, xs: List<&2, Brew>) -> String:
163	  match xs:
164	    case []:
165	      ""
166	    case +b <> rest:
167	      quoted_if(str_eq(k, kind_of(b)), name_of(b)) ++ names(k, rest)
168	
169	def raw_if(hit: Bool, n: String) -> String:
170	  match hit:
171	    case True{}:
172	      "    " ++ n ++ "\n"
173	    case False{}:
174	      ""
175	
176	def raws(xs: List<&2, Brew>) -> String:
177	  match xs:
178	    case []:
179	      ""
180	    case +b <> rest:
181	      raw_if(str_eq("other", kind_of(b)), name_of(b)) ++ raws(rest)
182	
183	def mas_if(hit: Bool, n: String) -> String:
184	  match hit:
185	    case True{}:
186	      " " ++ n ++ ";"
187	    case False{}:
188	      ""
189	
190	def mas(xs: List<&2, Brew>) -> String:
191	  match xs:
192	    case []:
193	      ""
194	    case +b <> rest:
195	      mas_if(str_eq("mas", kind_of(b)), name_of(b)) ++ mas(rest)
196	
197	def brew_section(+xs: List<&2, Brew>) -> String:
198	  "  homebrew.taps = [" ++ names("tap", xs) ++ " ];\n" ++
199	  "  homebrew.masApps = {" ++ mas(xs) ++ " };\n" ++
200	  "  homebrew.brews = [" ++ names("brew", xs) ++ " ];\n" ++
201	  "  homebrew.casks = [" ++ names("cask", xs) ++ " ];\n" ++
202	  "  homebrew.extraConfig = ''\n" ++ raws(xs) ++ "  '';\n"
203	
204	# The macOS application firewall. Its options exist only while it is on: `socketfilterfw` turns the
205	# firewall on whenever one of them is set, so "off, with options" cannot be written.
206	type Firewall is Data:
207	  FirewallOff{}
208	  FirewallOn{allowSigned: Bool, allowSignedApp: Bool, blockAllIncoming: Bool, stealth: Bool}
209	
210	def nix_bool(b: Bool) -> String:
211	  match b:
212	    case True{}:
213	      "true"
214	    case False{}:
215	      "false"
216	
217	def firewall_nix(f: Firewall) -> String:
218	  match f:
219	    case FirewallOff{}:
220	      "  networking.applicationFirewall.enable = false;\n"
221	    case FirewallOn{a, b, c, d}:
222	      "  networking.applicationFirewall.enable = true;\n" ++
223	      "  networking.applicationFirewall.allowSigned = " ++ nix_bool(a) ++ ";\n" ++
224	      "  networking.applicationFirewall.allowSignedApp = " ++ nix_bool(b) ++ ";\n" ++
225	      "  networking.applicationFirewall.blockAllIncoming = " ++ nix_bool(c) ++ ";\n" ++
226	      "  networking.applicationFirewall.enableStealthMode = " ++ nix_bool(d) ++ ";\n"
227	
228	def firewall_show(f: Firewall) -> String:
229	  match f:
230	    case FirewallOff{}:
231	      "off"
232	    case FirewallOn{a, b, c, d}:
233	      "on (allowSigned " ++ nix_bool(a) ++ ", allowSignedApp " ++ nix_bool(b) ++ ", blockAllIncoming " ++ nix_bool(c) ++ ", stealth " ++ nix_bool(d) ++ ")"
234	
235	def firewall_change_if(same: Bool, now: String, want: String) -> String:
236	  match same:
237	    case True{}:
238	      ""
239	    case False{}:
240	      "change  networking.applicationFirewall: " ++ now ++ " -> " ++ want ++ "\n"
241	
242	def firewall_change_str(+want: String, +now: String) -> String:
243	  firewall_change_if(str_eq(want, now), now, want)
244	
245	# Dry run line for the firewall ("" when unchanged).
246	def firewall_change(want: Firewall, now: Firewall) -> String:
247	  firewall_change_str(firewall_show(want), firewall_show(now))
248	
249	# True when no setting's option starts with `p` (areas V types, like the firewall, stay out of the flat list).
250	def none_prefixed(+p: String, xs: List<&2, Setting>) -> Bool:
251	  match xs:
252	    case []:
253	      True{}
254	    case s <> rest:
255	      Bool.not(String.starts_with(option_of(s), p)) && none_prefixed(p, rest)