1	import Base
2	import ./geom.bend as G
3	import ./protein.bend as P
4	
5	# --- PDB reader v0: ATOM records -> Complex. ---
6	# Fixed columns; ATOM lines before the first ENDMDL (HETATM and the rest are
7	# dropped); consecutive records with equal (chain, resSeq) merge into one
8	# Residue, consecutive same-chain residues into one Chain. Insertion codes
9	# are ignored, so insertion variants of one residue merge.
10	# Element symbols map to Z (unknown -> 0); a blank element field falls back
11	# to the atom name's first letter (so CA-the-carbon needs its element field;
12	# without one it reads as calcium).
13	# Coordinates need digits on both sides of the point ("12." and ".5" fail);
14	# mantissas must fit U32 (about 9 digits). A line that fails any field is
15	# skipped and counted: parse_pdb answers the skip count beside the Complex.
16	#
17	# Structure note: Bend checks top-to-bottom with no forward references, and
18	# branching on a computed Bool needs a callee, so every helper below only
19	# calls defs above it. Grouping is branchless: both next-states are built
20	# as data and picked (Bool.pick), with a single self-call on the tail.
21	
22	# Fixed-column slice: 0-based start, length.
23	def pdb_slice(s: String, start: Nat, len: Nat) -> String:
24	  String.take(String.drop(s, start), len)
25	
26	def is_atom_line(line: String) -> Bool:
27	  String.starts_with(line, "ATOM  ")
28	
29	# Tail-recursive lines(): single self-call in tail position, so long files
30	# do not grow the machine stack (String.split recurses per character).
31	def tlines_go(s: String, cur: String, acc: List<&2, String>) -> List<&2, String>:
32	  match s:
33	    case SNil{}:
34	      List.reverse(&2, String, String.reverse(cur) <> acc)
35	    case SCon{'\n', t}:
36	      tlines_go(t, SNil{}, String.reverse(cur) <> acc)
37	    case SCon{h, t}:
38	      tlines_go(t, SCon{h, cur}, acc)
39	
40	def tlines(s: String) -> List<&2, String>:
41	  tlines_go(s, SNil{}, Nil{})
42	
43	# ATOM lines up to (excluding) the first ENDMDL. Decided by matching the
44	# first six characters literally, so no computed Bool is ever matched.
45	# Tail-recursive over lines for the same stack reason as tlines.
46	def atom_lines_go(lines: List<&2, String>, acc: List<&2, String>) -> List<&2, String>:
47	  match lines:
48	    case Nil{}:
49	      List.reverse(&2, String, acc)
50	    case h <> t:
51	      match h:
52	        case SCon{'E', SCon{'N', SCon{'D', SCon{'M', SCon{'D', SCon{'L', _}}}}}}:
53	          List.reverse(&2, String, acc)
54	        case SCon{'A', SCon{'T', SCon{'O', SCon{'M', SCon{' ', SCon{' ', _}}}}}}:
55	          atom_lines_go(t, h <> acc)
56	        case _:
57	          atom_lines_go(t, acc)
58	
59	def atom_lines(lines: List<&2, String>) -> List<&2, String>:
60	  atom_lines_go(lines, Nil{})
61	
62	def is_conect_line(line: String) -> Bool:
63	  String.starts_with(line, "CONECT")
64	
65	# CONECT lines anywhere in the file (they follow ENDMDL in practice).
66	def conect_lines(lines: List<&2, String>) -> List<&2, String>:
67	  match lines:
68	    case Nil{}:
69	      Nil{}
70	    case h <> t:
71	      match h:
72	        case SCon{'C', SCon{'O', SCon{'N', SCon{'E', SCon{'C', SCon{'T', _}}}}}}:
73	          h <> conect_lines(t)
74	        case _:
75	          conect_lines(t)
76	
77	# Powers of ten for the fractional scale.
78	def pow10(n: Nat) -> U32:
79	  match n:
80	    case 0n:
81	      1
82	    case 1n+p:
83	      U32.mul(10, pow10(p))
84	
85	def f32_apply_sign(neg: Bool, v: F32) -> F32:
86	  match neg:
87	    case True{}:
88	      (0.0 - v : F32)
89	    case False{}:
90	      v
91	
92	def f32_combine(neg: Bool, iv: U32, fv: U32, sc: U32) -> F32:
93	  f32_apply_sign(neg, (U32.to_f32(iv) + (U32.to_f32(fv) / U32.to_f32(sc) : F32) : F32))
94	
95	def parse_f32_frac(neg: Bool, iv: U32, f: Maybe<&2, U32>, sc: U32) -> Maybe<&2, F32>:
96	  match f:
97	    case None{}:
98	      None{}
99	    case Some{fv}:
100	      Some{f32_combine(neg, iv, fv, sc)}
101	
102	def parse_f32_num(neg: Bool, i: Maybe<&2, U32>, fp: String, flen: Nat) -> Maybe<&2, F32>:
103	  match i:
104	    case None{}:
105	      None{}
106	    case Some{iv}:
107	      parse_f32_frac(neg, iv, U32.read(fp), pow10(flen))
108	
109	def parse_f32_int(neg: Bool, ip: String, +fp: String) -> Maybe<&2, F32>:
110	  parse_f32_num(neg, U32.read(ip), fp, String.length(fp))
111	
112	def parse_f32_split(neg: Bool, parts: List<&2, String>) -> Maybe<&2, F32>:
113	  match parts:
114	    case Nil{}:
115	      None{}
116	    case ip <> Nil{}:
117	      parse_f32_int(neg, ip, "0")
118	    case ip <> fp <> Nil{}:
119	      parse_f32_int(neg, ip, fp)
120	    case ip <> fp <> rest:
121	      None{}
122	
123	def parse_f32_stripped(p: Bool & String) -> Maybe<&2, F32>:
124	  match p:
125	    case (neg, rest):
126	      parse_f32_split(neg, String.split(rest, '.'))
127	
128	def strip_sign_kept(plus: Bool, h: Char, t: String) -> Bool & String:
129	  match plus:
130	    case True{}:
131	      (False{}, t)
132	    case False{}:
133	      (False{}, SCon{h, t})
134	
135	def strip_sign_plus(+h: Char, t: String) -> Bool & String:
136	  strip_sign_kept(Char.is_eq(h, '+'), h, t)
137	
138	def strip_sign_if(dash: Bool, h: Char, t: String) -> Bool & String:
139	  match dash:
140	    case True{}:
141	      (True{}, t)
142	    case False{}:
143	      strip_sign_plus(h, t)
144	
145	def strip_sign_go(+h: Char, t: String) -> Bool & String:
146	  strip_sign_if(Char.is_eq(h, '-'), h, t)
147	
148	def strip_sign(s: String) -> Bool & String:
149	  match s:
150	    case SNil{}:
151	      (False{}, SNil{})
152	    case SCon{h, t}:
153	      strip_sign_go(h, t)
154	
155	# Decimal floats: optional sign, digits, optional '.', digits.
156	def parse_f32(s: String) -> Maybe<&2, F32>:
157	  parse_f32_stripped(strip_sign(String.trim(s)))
158	
159	# Element symbol -> atomic number; unknown -> 0.
160	def elem_1(h: Char) -> U32:
161	  match h:
162	    case 'H':
163	      1
164	    case 'B':
165	      5
166	    case 'C':
167	      6
168	    case 'N':
169	      7
170	    case 'O':
171	      8
172	    case 'F':
173	      9
174	    case 'P':
175	      15
176	    case 'S':
177	      16
178	    case 'K':
179	      19
180	    case 'V':
181	      23
182	    case 'I':
183	      53
184	    case _:
185	      0
186	
187	def elem_2(h: Char, h2: Char) -> U32:
188	  match h h2:
189	    case 'F' 'E':
190	      26
191	    case 'Z' 'N':
192	      30
193	    case 'C' 'A':
194	      20
195	    case 'M' 'G':
196	      12
197	    case 'M' 'N':
198	      25
199	    case 'N' 'A':
200	      11
201	    case 'C' 'L':
202	      17
203	    case 'C' 'U':
204	      29
205	    case _ _:
206	      0
207	
208	def elem_no_1(h: Char, t: String) -> U32:
209	  match t:
210	    case SNil{}:
211	      elem_1(h)
212	    case SCon{h2, t2}:
213	      elem_2(h, h2)
214	
215	def elem_no(s: String) -> U32:
216	  match s:
217	    case SNil{}:
218	      0
219	    case SCon{h, t}:
220	      elem_no_1(h, t)
221	
222	def elem_from_name(n: String) -> U32:
223	  match n:
224	    case SNil{}:
225	      0
226	    case SCon{h, t}:
227	      elem_1(Char.to_upper(h))
228	
229	def elem_of_go(e: String, n: String) -> U32:
230	  match e:
231	    case SNil{}:
232	      elem_from_name(n)
233	    case SCon{h, t}:
234	      elem_no(String.to_upper(e))
235	
236	def elem_of(raw_elem: String, raw_name: String) -> U32:
237	  elem_of_go(String.trim(raw_elem), String.trim(raw_name))
238	
239	def chain_u32(s: String) -> U32:
240	  match s:
241	    case SNil{}:
242	      32
243	    case SCon{h, t}:
244	      Char.to_u32(h)
245	
246	# One ATOM line -> (chain, seq, atom). None{} when any field fails.
247	# Threaded bottom-up: each helper matches one Maybe and passes the rest on.
248	def parse_atom_z(serial: U32, ch: U32, seq: Nat, x: F32, y: F32, mz: Maybe<&2, F32>, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
249	  match mz:
250	    case None{}:
251	      None{}
252	    case Some{z}:
253	      Some{(ch, seq, P.Atom{serial, elem_of(elem_s, name_s), G.V3{x, y, z}})}
254	
255	def parse_atom_y(serial: U32, ch: U32, seq: Nat, x: F32, my: Maybe<&2, F32>, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
256	  match my:
257	    case None{}:
258	      None{}
259	    case Some{y}:
260	      parse_atom_z(serial, ch, seq, x, y, parse_f32(String.trim(zs)), elem_s, name_s)
261	
262	def parse_atom_x(serial: U32, ch: U32, seq: Nat, mx: Maybe<&2, F32>, ys: String, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
263	  match mx:
264	    case None{}:
265	      None{}
266	    case Some{x}:
267	      parse_atom_y(serial, ch, seq, x, parse_f32(String.trim(ys)), zs, elem_s, name_s)
268	
269	def parse_atom_seq(serial: U32, ch: U32, ms: Maybe<&2, Nat>, xs: String, ys: String, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
270	  match ms:
271	    case None{}:
272	      None{}
273	    case Some{seq}:
274	      parse_atom_x(serial, ch, seq, parse_f32(String.trim(xs)), ys, zs, elem_s, name_s)
275	
276	def parse_atom_chain(serial: U32, chain_s: String, seq_s: String, xs: String, ys: String, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
277	  parse_atom_seq(serial, chain_u32(chain_s), Nat.read(String.trim(seq_s)), xs, ys, zs, elem_s, name_s)
278	
279	def parse_atom_serial(ms: Maybe<&2, U32>, chain_s: String, seq_s: String, xs: String, ys: String, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
280	  match ms:
281	    case None{}:
282	      None{}
283	    case Some{serial}:
284	      parse_atom_chain(serial, chain_s, seq_s, xs, ys, zs, elem_s, name_s)
285	
286	def parse_atom_fields(serial_s: String, chain_s: String, seq_s: String, xs: String, ys: String, zs: String, elem_s: String, name_s: String) -> Maybe<&1, U32 & Nat & P.Atom>:
287	  parse_atom_serial(U32.read(String.trim(serial_s)), chain_s, seq_s, xs, ys, zs, elem_s, name_s)
288	
289	def parse_atom_line(+line: String) -> Maybe<&1, U32 & Nat & P.Atom>:
290	  parse_atom_fields(pdb_slice(line, 6n, 5n), pdb_slice(line, 21n, 1n), pdb_slice(line, 22n, 4n), pdb_slice(line, 30n, 8n), pdb_slice(line, 38n, 8n), pdb_slice(line, 46n, 8n), pdb_slice(line, 76n, 2n), pdb_slice(line, 12n, 4n))
291	
292	# One CONECT line -> [(s0, si)] bonds for each partner present.
293	def conect_p4(s0: U32, m4: Maybe<&2, U32>) -> List<&1, U32 & U32>:
294	  match m4:
295	    case None{}:
296	      Nil{}
297	    case Some{s4}:
298	      [(s0, s4)]
299	
300	def conect_p3(+s0: U32, m3: Maybe<&2, U32>, m4: Maybe<&2, U32>) -> List<&1, U32 & U32>:
301	  match m3:
302	    case None{}:
303	      conect_p4(s0, m4)
304	    case Some{s3}:
305	      (s0, s3) <> conect_p4(s0, m4)
306	
307	def conect_p2(+s0: U32, m2: Maybe<&2, U32>, m3: Maybe<&2, U32>, m4: Maybe<&2, U32>) -> List<&1, U32 & U32>:
308	  match m2:
309	    case None{}:
310	      conect_p3(s0, m3, m4)
311	    case Some{s2}:
312	      (s0, s2) <> conect_p3(s0, m3, m4)
313	
314	def conect_p1(+s0: U32, m1: Maybe<&2, U32>, m2: Maybe<&2, U32>, m3: Maybe<&2, U32>, m4: Maybe<&2, U32>) -> List<&1, U32 & U32>:
315	  match m1:
316	    case None{}:
317	      conect_p2(s0, m2, m3, m4)
318	    case Some{s1}:
319	      (s0, s1) <> conect_p2(s0, m2, m3, m4)
320	
321	def conect_assemble(m0: Maybe<&2, U32>, m1: Maybe<&2, U32>, m2: Maybe<&2, U32>, m3: Maybe<&2, U32>, m4: Maybe<&2, U32>) -> List<&1, U32 & U32>:
322	  match m0:
323	    case None{}:
324	      Nil{}
325	    case Some{s0}:
326	      conect_p1(s0, m1, m2, m3, m4)
327	
328	def parse_conect_line(+line: String) -> List<&1, U32 & U32>:
329	  conect_assemble(U32.read(String.trim(pdb_slice(line, 6n, 5n))), U32.read(String.trim(pdb_slice(line, 11n, 5n))), U32.read(String.trim(pdb_slice(line, 16n, 5n))), U32.read(String.trim(pdb_slice(line, 21n, 5n))), U32.read(String.trim(pdb_slice(line, 26n, 5n))))
330	
331	# Collect parsed atoms plus the skipped-line count. Tail-recursive: the
332	# extend step builds both outcomes as data (no match, no cycle) and the
333	# single self-call runs on the tail.
334	def collect_extend(m: Maybe<&1, U32 & Nat & P.Atom>, st: List<&1, U32 & Nat & P.Atom> & Nat) -> List<&1, U32 & Nat & P.Atom> & Nat:
335	  match m:
336	    case None{}:
337	      match st:
338	        case (as, n):
339	          (as, 1n+n)
340	    case Some{x}:
341	      match st:
342	        case (as, n):
343	          (x <> as, n)
344	
345	def collect_finish(st: List<&1, U32 & Nat & P.Atom> & Nat) -> List<&1, U32 & Nat & P.Atom> & Nat:
346	  match st:
347	    case (as, n):
348	      (List.reverse(&1, U32 & Nat & P.Atom, as), n)
349	
350	def collect_go(lines: List<&2, String>, st: List<&1, U32 & Nat & P.Atom> & Nat) -> List<&1, U32 & Nat & P.Atom> & Nat:
351	  match lines:
352	    case Nil{}:
353	      collect_finish(st)
354	    case h <> t:
355	      collect_go(t, collect_extend(parse_atom_line(h), st))
356	
357	def collect_atoms(lines: List<&2, String>) -> List<&1, U32 & Nat & P.Atom> & Nat:
358	  collect_go(lines, (Nil{}, 0n))
359	
360	def append_conect(a: List<&1, U32 & U32>, b: List<&1, U32 & U32>) -> List<&1, U32 & U32>:
361	  match a:
362	    case Nil{}:
363	      b
364	    case h <> t:
365	      h <> append_conect(t, b)
366	
367	def conect_pairs(lines: List<&2, String>) -> List<&1, U32 & U32>:
368	  match lines:
369	    case Nil{}:
370	      Nil{}
371	    case h <> t:
372	      append_conect(parse_conect_line(h), conect_pairs(t))
373	
374	# Pass 1: consecutive equal (chain, seq) merge. Chains and residues run in
375	# parallel Data lists: a pair accumulator would not be reusable (+ needs
376	# Data), so the two stay aligned and are zipped after (zip_chains).
377	# Branchless: both next-states are built as data and picked, with one
378	# self-call on the tail, so no helper cycle is needed.
379	def group_res_go(items: List<&1, U32 & Nat & P.Atom>, +cur_c: U32, +cur_s: Nat, +cur_as: List<&2, P.Atom>, +acc_c: List<&2, U32>, +acc_r: List<&2, P.Residue>) -> List<&2, U32> & List<&2, P.Residue>:
380	  match items:
381	    case Nil{}:
382	      (List.reverse(&2, U32, cur_c <> acc_c), List.reverse(&2, P.Residue, P.Residue{cur_s, List.reverse(&2, P.Atom, cur_as)} <> acc_r))
383	    case (c, s, a) <> t:
384	      +c2 = c
385	      +s2 = s
386	      +same = Bool.and(U32.is_eq(c2, cur_c), Nat.is_eq(s2, cur_s))
387	      group_res_go(t, Bool.pick(U32, same, cur_c, c2), Bool.pick(Nat, same, cur_s, s2), a <> Bool.pick(List<&2, P.Atom>, same, cur_as, Nil{}), Bool.pick(List<&2, U32>, same, acc_c, cur_c <> acc_c), Bool.pick(List<&2, P.Residue>, same, acc_r, P.Residue{cur_s, List.reverse(&2, P.Atom, cur_as)} <> acc_r))
388	
389	def group_residues(items: List<&1, U32 & Nat & P.Atom>) -> List<&2, U32> & List<&2, P.Residue>:
390	  match items:
391	    case Nil{}:
392	      (Nil{}, Nil{})
393	    case (c, s, a) <> t:
394	      group_res_go(t, c, s, [a], Nil{}, Nil{})
395	
396	# Zip the parallel chain/residue lists back into pairs (aligned by
397	# construction; extra elements on either side are dropped).
398	def zip_chains(cs: List<&2, U32>, rs: List<&2, P.Residue>) -> List<&1, U32 & P.Residue>:
399	  match cs rs:
400	    case Nil{} Nil{}:
401	      Nil{}
402	    case Nil{} _ <> _:
403	      Nil{}
404	    case _ <> _ Nil{}:
405	      Nil{}
406	    case c <> ct r <> rt:
407	      (c, r) <> zip_chains(ct, rt)
408	
409	# Pass 2: consecutive equal chains merge into Chain.
410	def group_chain_go(items: List<&1, U32 & P.Residue>, +cur_c: U32, +cur_rs: List<&2, P.Residue>, +acc: List<&2, P.Chain>) -> List<&2, P.Chain>:
411	  match items:
412	    case Nil{}:
413	      List.reverse(&2, P.Chain, P.Chain{cur_c, List.reverse(&2, P.Residue, cur_rs)} <> acc)
414	    case (c, r) <> t:
415	      +c2 = c
416	      +same = U32.is_eq(c2, cur_c)
417	      group_chain_go(t, Bool.pick(U32, same, cur_c, c2), r <> Bool.pick(List<&2, P.Residue>, same, cur_rs, Nil{}), Bool.pick(List<&2, P.Chain>, same, acc, P.Chain{cur_c, List.reverse(&2, P.Residue, cur_rs)} <> acc))
418	
419	def group_chains_zip(items: List<&1, U32 & P.Residue>) -> List<&2, P.Chain>:
420	  match items:
421	    case Nil{}:
422	      Nil{}
423	    case (c, r) <> t:
424	      group_chain_go(t, c, [r], Nil{})
425	
426	def group_chains(cs: List<&2, U32>, rs: List<&2, P.Residue>) -> List<&2, P.Chain>:
427	  group_chains_zip(zip_chains(cs, rs))
428	
429	# Whole file -> (Complex, skipped lines).
430	def parse_pdb_group(g: List<&2, U32> & List<&2, P.Residue>, n: Nat) -> P.Complex & Nat:
431	  match g:
432	    case (cs, rs):
433	      (P.Complex{group_chains(cs, rs)}, n)
434	
435	def parse_pdb_collect(p: List<&1, U32 & Nat & P.Atom> & Nat) -> P.Complex & Nat:
436	  match p:
437	    case (items, n):
438	      parse_pdb_group(group_residues(items), n)
439	
440	def parse_pdb(text: String) -> P.Complex & Nat:
441	  parse_pdb_collect(collect_atoms(atom_lines(tlines(text))))
442	
443	def complex_of(p: P.Complex & Nat) -> P.Complex:
444	  match p:
445	    case (cx, n):
446	      cx
447	
448	def skipped_of(p: P.Complex & Nat) -> Nat:
449	  match p:
450	    case (cx, n):
451	      n
452	
453	def first_elem_go(xs: List<&2, P.Atom>) -> Maybe<&2, U32>:
454	  match xs:
455	    case Nil{}:
456	      None{}
457	    case h <> t:
458	      Some{P.Atom.elem(h)}
459	
460	def first_elem(cx: P.Complex) -> Maybe<&2, U32>:
461	  first_elem_go(P.Complex.flatten(cx))
462	
463	# Two-line ALA snippet for laws and smoke tests.
464	def demo_text() -> String:
465	  "ATOM      1  N   ALA A   1      11.104  13.207   2.100  1.00 13.79           N  \nATOM      2  CA  ALA A   1      12.104  13.207   2.100  1.00 10.80           C  "
466	
467	# A bad serial ("X") so the second line skips.
468	def demo_bad_text() -> String:
469	  "ATOM      1  N   ALA A   1      11.104  13.207   2.100  1.00 13.79           N  \nATOM      X  CA  ALA A   1      12.104  13.207   2.100  1.00 10.80           C  "
470	
471	def finish_read(fr: File & Result<&1, &1, U32 & String, String>) -> IO(P.Complex & Nat):
472	  match fr:
473	    case (fh2, res):
474	      do IO<P.Complex & Nat>:
475	        text : String <- IO.pass(String, res)
476	        File.close(fh2)
477	        return parse_pdb(text)
478	
479	# Whole file from disk -> (Complex, skipped lines). Reads at most 1 MiB.
480	def load_pdb_file(path: String) -> IO(P.Complex & Nat):
481	  do IO<P.Complex & Nat>:
482	    fh : File <- IO.try(File, File.open(path, "r"))
483	    fr : File & Result<&1, &1, U32 & String, String> <- File.read(fh, 1048576)
484	    finish_read(fr)
485	
486	# --- PDB writer v0: normalizing export (not round-trip). ---
487	# Atom names canonicalize to the element symbol, residues to UNK, chain to
488	# the cid character, occupancy 1.00, tempFactor 0.00. Coordinates print as
489	# near-%8.3f. Validates by reparse: write then parse gives equal counts.
490	
491	def pad_left(+s: String, w: Nat) -> String:
492	  String.append(String.repeat(" ", Nat.sub(w, String.length(s))), s)
493	
494	def pad_right(+s: String, w: Nat) -> String:
495	  String.append(s, String.repeat(" ", Nat.sub(w, String.length(s))))
496	
497	def pad_zero(+s: String, w: Nat) -> String:
498	  String.append(String.repeat("0", Nat.sub(w, String.length(s))), s)
499	
500	def fmt_u32(w: Nat, x: U32) -> String:
501	  pad_left(U32.show(x), w)
502	
503	def fmt_nat(w: Nat, n: Nat) -> String:
504	  pad_left(Nat.show(n), w)
505	
506	def fmt_frac3(f: F32) -> String:
507	  pad_zero(Nat.show(F32.to_nat(F32.floor(((f * 1000.0 : F32) + 0.5 : F32)))), 3n)
508	
509	def fmt_abs(+x: F32) -> F32:
510	  Bool.pick(F32, F32.is_lt(x, 0.0), (0.0 - x : F32), x)
511	
512	def fmt_f83_sign(sgn: String, +ax: F32) -> String:
513	  pad_left(String.append(sgn, String.append(Nat.show(F32.to_nat(F32.floor(ax))), String.append(".", fmt_frac3((ax - U32.to_f32(F32.to_u32(F32.floor(ax))) : F32))))), 8n)
514	
515	def fmt_f83(+x: F32) -> String:
516	  fmt_f83_sign(Bool.pick(String, F32.is_lt(x, 0.0), "-", SNil{}), fmt_abs(x))
517	
518	def elem_sym(e: U32) -> String:
519	  match e:
520	    case 1:
521	      "H"
522	    case 5:
523	      "B"
524	    case 6:
525	      "C"
526	    case 7:
527	      "N"
528	    case 8:
529	      "O"
530	    case 9:
531	      "F"
532	    case 11:
533	      "NA"
534	    case 12:
535	      "MG"
536	    case 15:
537	      "P"
538	    case 16:
539	      "S"
540	    case 17:
541	      "CL"
542	    case 19:
543	      "K"
544	    case 20:
545	      "CA"
546	    case 23:
547	      "V"
548	    case 25:
549	      "MN"
550	    case 26:
551	      "FE"
552	    case 29:
553	      "CU"
554	    case 30:
555	      "ZN"
556	    case 53:
557	      "I"
558	    case _:
559	      "X"
560	
561	def write_atom_line(serial: U32, name4: String, chain1: String, seq: Nat, x: F32, y: F32, z: F32, elem2: String) -> String:
562	  String.append("ATOM  ", String.append(fmt_u32(5n, serial), String.append(" ", String.append(pad_right(name4, 4n), String.append(" UNK ", String.append(chain1, String.append(fmt_nat(4n, seq), String.append("    ", String.append(fmt_f83(x), String.append(fmt_f83(y), String.append(fmt_f83(z), String.append("  1.00  0.00          ", elem2))))))))))))
563	
564	def write_atom_pos(serial: U32, +elem: U32, pos: G.Vec3, chain1: String, seq: Nat) -> String:
565	  match pos:
566	    case G.V3{x, y, z}:
567	      write_atom_line(serial, String.append(" ", String.append(elem_sym(elem), " ")), chain1, seq, x, y, z, pad_left(elem_sym(elem), 2n))
568	
569	def write_atom(h: P.Atom, chain1: String, seq: Nat) -> String:
570	  match h:
571	    case P.Atom{serial, elem, pos}:
572	      write_atom_pos(serial, elem, pos, chain1, seq)
573	
574	def write_atoms(xs: List<&2, P.Atom>, +chain1: String, +seq: Nat) -> List<&2, String>:
575	  match xs:
576	    case Nil{}:
577	      Nil{}
578	    case h <> t:
579	      write_atom(h, chain1, seq) <> write_atoms(t, chain1, seq)
580	
581	def append_lines(a: List<&2, String>, b: List<&2, String>) -> List<&2, String>:
582	  match a:
583	    case Nil{}:
584	      b
585	    case h <> t:
586	      h <> append_lines(t, b)
587	
588	def write_residue(r: P.Residue, chain1: String) -> List<&2, String>:
589	  match r:
590	    case P.Residue{seq, atoms}:
591	      write_atoms(atoms, chain1, seq)
592	
593	def write_residues(rs: List<&2, P.Residue>, +chain1: String) -> List<&2, String>:
594	  match rs:
595	    case Nil{}:
596	      Nil{}
597	    case h <> t:
598	      append_lines(write_residue(h, chain1), write_residues(t, chain1))
599	
600	def write_chain(c: P.Chain) -> List<&2, String>:
601	  match c:
602	    case P.Chain{cid, residues}:
603	      write_residues(residues, SCon{Char.from_u32(cid), SNil{}})
604	
605	def write_chains(cs: List<&2, P.Chain>) -> List<&2, String>:
606	  match cs:
607	    case Nil{}:
608	      Nil{}
609	    case h <> t:
610	      append_lines(write_chain(h), write_chains(t))
611	
612	def complex_chains(k: P.Complex) -> List<&2, P.Chain>:
613	  match k:
614	    case P.Complex{chains}:
615	      chains
616	
617	def write_complex(k: P.Complex) -> String:
618	  String.join(write_chains(complex_chains(k)), "\n")
619	
620	def finish_write(fr: File & Result<&1, &1, U32 & String, Unit>) -> IO(Unit):
621	  match fr:
622	    case (fh2, res):
623	      do IO<Unit>:
624	        done : Unit <- IO.pass(Unit, res)
625	        File.close(fh2)
626	        return done
627	
628	def write_text_file(path: String, text: String) -> IO(Unit):
629	  do IO<Unit>:
630	    fh : File <- IO.try(File, File.open(path, "w"))
631	    fr : File & Result<&1, &1, U32 & String, Unit> <- File.write(fh, text)
632	    finish_write(fr)
633	
634	def save_pdb_file(path: String, cx: P.Complex) -> IO(Unit):
635	  write_text_file(path, write_complex(cx))
636	
637	def finish_bonds(fr: File & Result<&1, &1, U32 & String, String>) -> IO(List<&1, U32 & U32>):
638	  match fr:
639	    case (fh2, res):
640	      do IO<List<&1, U32 & U32>>:
641	        text : String <- IO.pass(String, res)
642	        File.close(fh2)
643	        return conect_pairs(conect_lines(tlines(text)))
644	
645	# CONECT bonds from disk. A second full read; callers flatten once.
646	def load_pdb_bonds(path: String) -> IO(List<&1, U32 & U32>):
647	  do IO<List<&1, U32 & U32>>:
648	    fh : File <- IO.try(File, File.open(path, "r"))
649	    fr : File & Result<&1, &1, U32 & String, String> <- File.read(fh, 1048576)
650	    finish_bonds(fr)
651	
652	def finish_text(fr: File & Result<&1, &1, U32 & String, String>) -> IO(String):
653	  match fr:
654	    case (fh2, res):
655	      do IO<String>:
656	        text : String <- IO.pass(String, res)
657	        File.close(fh2)
658	        return text
659	
660	# Raw file text (for template atom collection).
661	def load_text_file(path: String) -> IO(String):
662	  do IO<String>:
663	    fh : File <- IO.try(File, File.open(path, "r"))
664	    fr : File & Result<&1, &1, U32 & String, String> <- File.read(fh, 1048576)
665	    finish_text(fr)