arc.bend
near-architecture@0.8.0.0 · 762 lines · 0 definitions
1import Base
2
3# Arc: a system's architecture as types, in two hierarchies over the same containers.
4# Where it runs: node -> container -> part.
5# What it is: system -> container -> part.
6# Keys work like foreign keys: a container names its host node (`on`), a part its container (`in`)
7# and execution node (`on`), and a link two keys. A project states its laws with the predicates
8# below; the compiler proves them.
9
10# ---- vocabulary ----
11# UserDevice: a user's own device. Server: a machine the project runs. Overlay: the private
12# (overlay) network between them. Outside: someone else's servers.
13type NodeRole is Data:
14 UserDevice{}
15 Server{}
16 Overlay{}
17 Outside{}
18
19type PhysicalDevice is Data:
20 PhysicalDevice{key: String, name: String, platform: String}
21
22type Vendor is Data:
23 Vendor{name: String, cloud: String}
24
25type Org is Data:
26 Org{name: String, vendor: Vendor, devices: List<&2, PhysicalDevice>}
27
28type Host is Data:
29 Owned{device: String}
30 Cloud{provider: String}
31 Other{}
32
33type Node is Data:
34 Node{key: String, name: String, role: NodeRole, host: Host}
35
36# What a container is. The list is closed: something that is none of these is not a container.
37# Client: the app, on the user's device. The private overlay is a node, not a container.
38# DataApi: answers queries on records and changes them.
39# Harness: an agent harness, the loop around a model (tools, context, threads), driven over its remote-control API.
40# Proxy: forwards connections to another container, adding what it lacks, such as TLS or authentication.
41# ModelApi: answers model calls. Cli: a command a person runs. Worker: has no API of its own; it
42# only moves data between data APIs, so it is the first thing to fold into a data API's own actions.
43type ContainerKind is Data:
44 Client{}
45 DataApi{}
46 Harness{}
47 Proxy{}
48 ModelApi{}
49 Cli{}
50 Worker{}
51
52# Whether the project builds and runs it, or uses it as it is.
53type Owner is Data:
54 Ours{}
55 Theirs{}
56
57# Who can reach it: its own machine (127.0.0.1), the local network, the overlay, the device it is on, anyone.
58type Exposure is Data:
59 Local{}
60 Lan{}
61 Tailnet{}
62 Device{}
63 Public{}
64
65# What a container provides. Hosting is serving the app itself (its HTML and scripts); a data API
66# may also host the app only while it is private (shared_hosting_ok). Observability is receiving
67# a running container's errors, traces and structured logs.
68type Cap is Data:
69 Hosting{}
70 PrivateHosting{}
71 Realtime{}
72 BlobStore{}
73 Observability{}
74
75type Lang is Data:
76 Bend{}
77 C{}
78 Rust{}
79 TypeScript{}
80 JavaScript{}
81 Python{}
82 Opaque{}
83
84type Container is Data:
85 Container{key: String, name: String, kind: ContainerKind, owner: Owner, on: String, exposure: Exposure, caps: List<&2, Cap>, source: String, vendors: List<&2, String>, frameworks: List<&2, String>, libraries: List<&2, String>, languages: List<&2, String>}
86
87type Part is Data:
88 Part{key: String, name: String, lang: Lang, in: String, on: String}
89
90# A talks-to edge between two containers or parts, by key.
91type Link is Data:
92 Link{src: String, dst: String, label: String, live: Bool}
93
94type System is Data:
95 System{org: Org, nodes: List<&2, Node>, containers: List<&2, Container>, parts: List<&2, Part>, links: List<&2, Link>}
96
97# ---- access ----
98def org(s: System) -> Org:
99 match s:
100 case System{o, _, _, _, _}:
101 o
102
103def nodes(s: System) -> List<&2, Node>:
104 match s:
105 case System{_, n, _, _, _}:
106 n
107
108def containers(s: System) -> List<&2, Container>:
109 match s:
110 case System{_, _, c, _, _}:
111 c
112
113def parts(s: System) -> List<&2, Part>:
114 match s:
115 case System{_, _, _, p, _}:
116 p
117
118def links(s: System) -> List<&2, Link>:
119 match s:
120 case System{_, _, _, _, l}:
121 l
122
123def nkey(n: Node) -> String:
124 match n:
125 case Node{k, _, _, _}:
126 k
127
128def ckey(c: Container) -> String:
129 match c:
130 case Container{k, _, _, _, _, _, _, _, _, _, _, _}:
131 k
132
133def con(c: Container) -> String:
134 match c:
135 case Container{_, _, _, _, o, _, _, _, _, _, _, _}:
136 o
137
138def caps(c: Container) -> List<&2, Cap>:
139 match c:
140 case Container{_, _, _, _, _, _, cs, _, _, _, _, _}:
141 cs
142
143def pkey(p: Part) -> String:
144 match p:
145 case Part{k, _, _, _, _}:
146 k
147
148def pin(p: Part) -> String:
149 match p:
150 case Part{_, _, _, i, _}:
151 i
152
153def pon(p: Part) -> String:
154 match p:
155 case Part{_, _, _, _, on}:
156 on
157
158def nkeys(xs: List<&2, Node>) -> List<&2, String>:
159 match xs:
160 case []:
161 []
162 case n <> rest:
163 nkey(n) <> nkeys(rest)
164
165def ckeys(xs: List<&2, Container>) -> List<&2, String>:
166 match xs:
167 case []:
168 []
169 case c <> rest:
170 ckey(c) <> ckeys(rest)
171
172def pkeys(xs: List<&2, Part>) -> List<&2, String>:
173 match xs:
174 case []:
175 []
176 case p <> rest:
177 pkey(p) <> pkeys(rest)
178
179# Keys links may name: containers and parts.
180def keys(+s: System) -> List<&2, String>:
181 List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
182
183# ---- predicates on the vocabulary ----
184def is_server(r: NodeRole) -> Bool:
185 match r:
186 case Server{}:
187 True{}
188 case _:
189 False{}
190
191def is_outside(r: NodeRole) -> Bool:
192 match r:
193 case Outside{}:
194 True{}
195 case _:
196 False{}
197
198def is_device(r: NodeRole) -> Bool:
199 match r:
200 case UserDevice{}:
201 True{}
202 case _:
203 False{}
204
205def is_overlay(r: NodeRole) -> Bool:
206 match r:
207 case Overlay{}:
208 True{}
209 case _:
210 False{}
211
212def one_if(b: Bool) -> Nat:
213 match b:
214 case True{}:
215 1n
216 case False{}:
217 0n
218
219def overlay_nodes.go(xs: List<&2, Node>) -> Nat:
220 match xs:
221 case []:
222 0n
223 case n <> rest:
224 match n:
225 case Node{_, _, role, _}:
226 Nat.add(one_if(is_overlay(role)), overlay_nodes.go(rest))
227
228# Private access is represented by exactly one Overlay node.
229def overlay_nodes(+s: System) -> Nat:
230 overlay_nodes.go(nodes(s))
231
232def is_client(k: ContainerKind) -> Bool:
233 match k:
234 case Client{}:
235 True{}
236 case _:
237 False{}
238
239def is_data_api(k: ContainerKind) -> Bool:
240 match k:
241 case DataApi{}:
242 True{}
243 case _:
244 False{}
245
246def is_ours(o: Owner) -> Bool:
247 match o:
248 case Ours{}:
249 True{}
250 case Theirs{}:
251 False{}
252
253def is_local(e: Exposure) -> Bool:
254 match e:
255 case Local{}:
256 True{}
257 case _:
258 False{}
259
260def is_tailnet(e: Exposure) -> Bool:
261 match e:
262 case Tailnet{}:
263 True{}
264 case _:
265 False{}
266
267def is_rust(l: Lang) -> Bool:
268 match l:
269 case Rust{}:
270 True{}
271 case _:
272 False{}
273
274# ---- keys, like foreign keys ----
275def str_eq(a: String, b: String) -> Bool:
276 String.eq(a, b)
277
278def has(+s: String, xs: List<&2, String>) -> Bool:
279 match xs:
280 case []:
281 False{}
282 case x <> rest:
283 str_eq(s, x) || has(s, rest)
284
285def owned_device(+key: String, +name: String, xs: List<&2, PhysicalDevice>) -> Bool:
286 match xs:
287 case []:
288 False{}
289 case PhysicalDevice{k, n, _} <> rest:
290 (str_eq(key, k) && str_eq(name, n)) || owned_device(key, name, rest)
291
292def host_in_inventory(h: Host, name: String, o: Org) -> Bool:
293 match h o:
294 case Owned{key} Org{_, _, devices}:
295 owned_device(key, name, devices)
296 case Cloud{provider} Org{_, Vendor{_, cloud}, _}:
297 str_eq(provider, cloud)
298 case Other{} _:
299 False{}
300
301def node_owned(n: Node, +o: Org) -> Bool:
302 match n:
303 case Node{_, name, +role, host}:
304 Bool.not(is_server(role) || is_device(role)) || host_in_inventory(host, name, o)
305
306def owned_nodes.go(xs: List<&2, Node>, +o: Org) -> Bool:
307 match xs:
308 case []:
309 True{}
310 case n <> rest:
311 node_owned(n, o) && owned_nodes.go(rest, o)
312
313# Every server and user device is in the owner's inventory or on its vendor's cloud.
314def owned_nodes(+s: System) -> Bool:
315 owned_nodes.go(nodes(s), org(s))
316
317def pick_str(c: Bool, a: String, b: String) -> String:
318 match c:
319 case True{}:
320 a
321 case False{}:
322 b
323
324# No key names two things.
325def distinct_keys(xs: List<&2, String>) -> Bool:
326 match xs:
327 case []:
328 True{}
329 case +k <> +rest:
330 Bool.not(has(k, rest)) && distinct_keys(rest)
331
332# Every key in `xs` names something in `ks`.
333def all_in(xs: List<&2, String>, +ks: List<&2, String>) -> Bool:
334 match xs:
335 case []:
336 True{}
337 case x <> rest:
338 has(x, ks) && all_in(rest, ks)
339
340def part_ins(xs: List<&2, Part>) -> List<&2, String>:
341 match xs:
342 case []:
343 []
344 case p <> rest:
345 pin(p) <> part_ins(rest)
346
347def part_ons(xs: List<&2, Part>) -> List<&2, String>:
348 match xs:
349 case []:
350 []
351 case p <> rest:
352 pon(p) <> part_ons(rest)
353
354def container_ons(xs: List<&2, Container>) -> List<&2, String>:
355 match xs:
356 case []:
357 []
358 case c <> rest:
359 con(c) <> container_ons(rest)
360
361def link_ends(xs: List<&2, Link>) -> List<&2, String>:
362 match xs:
363 case []:
364 []
365 case l <> rest:
366 match l:
367 case Link{a, b, _, _}:
368 a <> b <> link_ends(rest)
369
370# The system is well formed: node keys and container/part keys are unique, every container is on
371# a node, every part in a container, and every link joins two things that exist.
372def well_formed(+s: System) -> Bool:
373 distinct_keys(nkeys(nodes(s))) && distinct_keys(keys(s)) &&
374 all_in(container_ons(containers(s)), nkeys(nodes(s))) &&
375 all_in(part_ins(parts(s)), ckeys(containers(s))) &&
376 all_in(part_ons(parts(s)), nkeys(nodes(s))) &&
377 all_in(link_ends(links(s)), keys(s))
378
379# ---- looking things up ----
380def part_home(+k: String, xs: List<&2, Part>) -> String:
381 match xs:
382 case []:
383 ""
384 case +p <> rest:
385 pick_str(str_eq(k, pkey(p)), pin(p), part_home(k, rest))
386
387# The container a key belongs to: itself, or the one its part sits in.
388def home(+k: String, +s: System) -> String:
389 pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
390
391def none() -> Container:
392 Container{"", "", Worker{}, Theirs{}, "", Public{}, [], "", [], [], [], []}
393
394def pick_c(hit: Bool, c: Container, other: Container) -> Container:
395 match hit:
396 case True{}:
397 c
398 case False{}:
399 other
400
401# The container with key `k` (an empty one when `k` is unknown; well_formed rules that out).
402def container(+k: String, xs: List<&2, Container>) -> Container:
403 match xs:
404 case []:
405 none()
406 case +c <> rest:
407 pick_c(str_eq(k, ckey(c)), c, container(k, rest))
408
409def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
410 match hit:
411 case True{}:
412 r
413 case False{}:
414 other
415
416def node_role(+k: String, xs: List<&2, Node>) -> NodeRole:
417 match xs:
418 case []:
419 Outside{}
420 case n <> rest:
421 match n:
422 case Node{nk, _, r, _}:
423 pick_r(str_eq(k, nk), r, node_role(k, rest))
424
425def part_node(+k: String, xs: List<&2, Part>) -> String:
426 match xs:
427 case []:
428 ""
429 case +p <> rest:
430 pick_str(str_eq(k, pkey(p)), pon(p), part_node(k, rest))
431
432# The node a container or part runs on, and its role.
433def node_of(+k: String, +s: System) -> String:
434 pick_str(has(k, pkeys(parts(s))), part_node(k, parts(s)), con(container(home(k, s), containers(s))))
435
436def role_of(+k: String, +s: System) -> NodeRole:
437 node_role(node_of(k, s), nodes(s))
438
439def container_exposure(c: Container) -> Exposure:
440 match c:
441 case Container{_, _, _, _, _, exposure, _, _, _, _, _, _}:
442 exposure
443
444def exposure_of(+k: String, +s: System) -> Exposure:
445 container_exposure(container(home(k, s), containers(s)))
446
447# ---- where it runs ----
448# On a server, everything is reachable only from the server itself or over the overlay.
449def private_ok(c: Container, +ns: List<&2, Node>) -> Bool:
450 match c:
451 case Container{_, _, _, _, on, +exposure, _, _, _, _, _, _}:
452 Bool.not(is_server(node_role(on, ns))) || is_tailnet(exposure) || is_local(exposure)
453
454def all_private(xs: List<&2, Container>, +ns: List<&2, Node>) -> Bool:
455 match xs:
456 case []:
457 True{}
458 case c <> rest:
459 private_ok(c, ns) && all_private(rest, ns)
460
461def servers_private(+s: System) -> Bool:
462 all_private(containers(s), nodes(s))
463
464# A device reaches a server over the overlay only when the destination is exposed to the tailnet.
465def devices_via_network.go(xs: List<&2, Link>, +s: System) -> Bool:
466 match xs:
467 case []:
468 True{}
469 case l <> rest:
470 match l:
471 case Link{src, +dst, _, _}:
472 (Bool.not(is_device(role_of(src, s)) && is_server(role_of(dst, s))) ||
473 is_tailnet(exposure_of(dst, s))) && devices_via_network.go(rest, s)
474
475def devices_via_network(+s: System) -> Bool:
476 devices_via_network.go(links(s), s)
477
478# A server container needs overlay exposure exactly when a device-origin link reaches it.
479def device_reaches(+key: String, xs: List<&2, Link>, +s: System) -> Bool:
480 match xs:
481 case []:
482 False{}
483 case Link{src, dst, _, _} <> rest:
484 (is_device(role_of(src, s)) && str_eq(home(dst, s), key)) || device_reaches(key, rest, s)
485
486def exposure_for_reach(c: Container, reached: Bool) -> Bool:
487 match reached:
488 case True{}: is_tailnet(container_exposure(c))
489 case False{}: is_local(container_exposure(c))
490
491def exposure_follows_reach.go(xs: List<&2, Container>, +s: System) -> Bool:
492 match xs:
493 case []:
494 True{}
495 case +c <> rest:
496 (Bool.not(is_server(role_of(ckey(c), s))) ||
497 exposure_for_reach(c, device_reaches(ckey(c), links(s), s))) &&
498 exposure_follows_reach.go(rest, s)
499
500def exposure_follows_reach(+s: System) -> Bool:
501 exposure_follows_reach.go(containers(s), s)
502
503# ---- what it is: minimality, every capability provided exactly once ----
504def is_cap(want: Cap, c: Cap) -> Bool:
505 match want c:
506 case Hosting{} Hosting{}:
507 True{}
508 case PrivateHosting{} PrivateHosting{}:
509 True{}
510 case Realtime{} Realtime{}:
511 True{}
512 case BlobStore{} BlobStore{}:
513 True{}
514 case Observability{} Observability{}:
515 True{}
516 case _ _:
517 False{}
518
519def count_in(+want: Cap, cs: List<&2, Cap>) -> Nat:
520 match cs:
521 case []:
522 0n
523 case c <> rest:
524 Nat.add(one_if(is_cap(want, c)), count_in(want, rest))
525
526def direct(+want: Cap, xs: List<&2, Container>) -> Nat:
527 match xs:
528 case []:
529 0n
530 case c <> rest:
531 Nat.add(count_in(want, caps(c)), direct(want, rest))
532
533def tailnet_hosting.go(xs: List<&2, Container>) -> Nat:
534 match xs:
535 case []:
536 0n
537 case c <> rest:
538 match c:
539 case Container{_, _, _, _, _, exposure, cs, _, _, _, _, _}:
540 Nat.add(one_if(is_tailnet(exposure) && Nat.is_gt(count_in(Hosting{}, cs), 0n)), tailnet_hosting.go(rest))
541
542# How many containers host the app at Tailnet exposure.
543def tailnet_hosting(+s: System) -> Nat:
544 tailnet_hosting.go(containers(s))
545
546# How many containers provide `want`. One tailnet host plus one overlay composes private hosting.
547def provided(want: Cap, +s: System) -> Nat:
548 match want:
549 case PrivateHosting{}:
550 Nat.add(direct(PrivateHosting{}, containers(s)), one_if(Nat.is_eq(tailnet_hosting(s), 1n) && Nat.is_eq(overlay_nodes(s), 1n)))
551 case _:
552 direct(want, containers(s))
553
554# ---- observability: everything we run reports to the observability provider ----
555def cons_if(b: Bool, k: String, xs: List<&2, String>) -> List<&2, String>:
556 match b:
557 case True{}:
558 k <> xs
559 case False{}:
560 xs
561
562# Keys of the containers that provide `want`.
563def providers(+want: Cap, xs: List<&2, Container>) -> List<&2, String>:
564 match xs:
565 case []:
566 []
567 case +c <> rest:
568 cons_if(Nat.is_gt(count_in(want, caps(c)), 0n), ckey(c), providers(want, rest))
569
570# The container a link end belongs to: a part's container, else the key itself.
571def part_container(ps: List<&2, Part>, +k: String) -> String:
572 match ps:
573 case []:
574 k
575 case +p <> rest:
576 pick_str(str_eq(k, pkey(p)), pin(p), part_container(rest, k))
577
578# Some link from container `k` (or one of its parts) reaches one of `obs`.
579def reports_to(ls: List<&2, Link>, +k: String, +ps: List<&2, Part>, +obs: List<&2, String>) -> Bool:
580 match ls:
581 case []:
582 False{}
583 case Link{src, dst, _, _} <> rest:
584 (str_eq(k, part_container(ps, src)) && has(dst, obs)) || reports_to(rest, k, ps, obs)
585
586def observed.go(xs: List<&2, Container>, +s: System, +obs: List<&2, String>) -> Bool:
587 match xs:
588 case []:
589 True{}
590 case c <> rest:
591 match c:
592 case Container{+k, _, _, owner, _, _, _, source, _, _, _, _}:
593 (Bool.not(is_ours(owner) && Bool.not(str_eq(source, ""))) || reports_to(links(s), k, parts(s), obs)) && observed.go(rest, s, obs)
594
595# Every container we build (ours, with source) links to a container providing Observability.
596def observed(+s: System) -> Bool:
597 observed.go(containers(s), s, providers(Observability{}, containers(s)))
598
599def tailnet_data_apis.go(xs: List<&2, Container>) -> Nat:
600 match xs:
601 case []:
602 0n
603 case c <> rest:
604 match c:
605 case Container{_, _, kind, _, _, exposure, _, _, _, _, _, _}:
606 Nat.add(one_if(is_data_api(kind) && is_tailnet(exposure)), tailnet_data_apis.go(rest))
607
608# The data APIs the overlay reaches: the client's data API. Local and outside ones are its sources.
609def tailnet_data_apis(+s: System) -> Nat:
610 tailnet_data_apis.go(containers(s))
611
612def own_data_apis.go(xs: List<&2, Container>, +ns: List<&2, Node>) -> Nat:
613 match xs:
614 case []:
615 0n
616 case c <> rest:
617 match c:
618 case Container{_, _, kind, _, on, _, _, _, _, _, _, _}:
619 Nat.add(one_if(is_data_api(kind) && Bool.not(is_outside(node_role(on, ns)))), own_data_apis.go(rest, ns))
620
621# The system's own data APIs: those not on someone else's servers. "Exactly one" means one store.
622def own_data_apis(+s: System) -> Nat:
623 own_data_apis.go(containers(s), nodes(s))
624
625# A data API may also host the app only while it is private.
626def shared_hosting_ok(c: Container) -> Bool:
627 match c:
628 case Container{_, _, kind, _, _, +exposure, +cs, _, _, _, _, _}:
629 Bool.not(Nat.is_gt(count_in(Hosting{}, cs), 0n) && is_data_api(kind)) || is_tailnet(exposure) || is_local(exposure)
630
631def shared_hosting_private.go(xs: List<&2, Container>) -> Bool:
632 match xs:
633 case []:
634 True{}
635 case c <> rest:
636 shared_hosting_ok(c) && shared_hosting_private.go(rest)
637
638def shared_hosting_private(+s: System) -> Bool:
639 shared_hosting_private.go(containers(s))
640
641# ---- a goal: every part of our own non-client containers is Rust ----
642def backend(c: Container) -> Bool:
643 match c:
644 case Container{_, _, kind, owner, _, _, _, _, _, _, _, _}:
645 is_ours(owner) && Bool.not(is_client(kind))
646
647def rust_ok(p: Part, +s: System) -> Bool:
648 match p:
649 case Part{_, _, lang, i, _}:
650 Bool.not(backend(container(i, containers(s)))) || is_rust(lang)
651
652def all_rust.go(xs: List<&2, Part>, +s: System) -> Bool:
653 match xs:
654 case []:
655 True{}
656 case p <> rest:
657 rust_ok(p, s) && all_rust.go(rest, s)
658
659def all_rust(+s: System) -> Bool:
660 all_rust.go(parts(s), s)
661
662# Every modeled part belongs to a container we build; someone else's program is a black box.
663def container_ours(c: Container) -> Bool:
664 match c:
665 case Container{_, _, _, owner, _, _, _, _, _, _, _, _}:
666 is_ours(owner)
667
668def parts_ours.go(xs: List<&2, Part>, +s: System) -> Bool:
669 match xs:
670 case []:
671 True{}
672 case p <> rest:
673 container_ours(container(pin(p), containers(s))) && parts_ours.go(rest, s)
674
675def parts_ours(+s: System) -> Bool:
676 parts_ours.go(parts(s), s)
677
678# ---- the diagram (D2): nodes as boxes, containers inside their node, parts inside their container ----
679def path(+k: String, +s: System) -> String:
680 node_of(k, s) ++ "." ++ pick_str(String.eq(home(k, s), k), k, home(k, s) ++ "." ++ k)
681
682def node_box(n: Node) -> String:
683 match n:
684 case Node{k, name, role, _}:
685 match role:
686 case Outside{}:
687 k ++ ": \"" ++ name ++ "\" {class: node; style.stroke-dash: 4; style.fill: \"#FFFFFF\"}\n"
688 case _:
689 k ++ ": \"" ++ name ++ "\" {class: node}\n"
690
691def node_boxes(xs: List<&2, Node>) -> String:
692 match xs:
693 case []:
694 ""
695 case n <> rest:
696 node_box(n) ++ node_boxes(rest)
697
698def stack_label(frameworks: List<&2, String>, libraries: List<&2, String>) -> String:
699 match frameworks:
700 case []:
701 match libraries:
702 case []:
703 ""
704 case _:
705 "\\n[" ++ String.join(libraries, ", ") ++ "]"
706 case _:
707 match libraries:
708 case []:
709 "\\n[" ++ String.join(frameworks, ", ") ++ "]"
710 case _:
711 "\\n[" ++ String.join(frameworks, ", ") ++ " · " ++ String.join(libraries, ", ") ++ "]"
712
713def container_box(c: Container) -> String:
714 match c:
715 case Container{k, name, _, _, on, _, _, _, _, frameworks, libraries, _}:
716 on ++ "." ++ k ++ ": \"" ++ name ++ stack_label(frameworks, libraries) ++ "\" {class: container}\n"
717
718def container_boxes(xs: List<&2, Container>) -> String:
719 match xs:
720 case []:
721 ""
722 case c <> rest:
723 container_box(c) ++ container_boxes(rest)
724
725def part_box(p: Part, +s: System) -> String:
726 match p:
727 case Part{+k, name, _, _, _}:
728 path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
729
730def part_boxes(xs: List<&2, Part>, +s: System) -> String:
731 match xs:
732 case []:
733 ""
734 case p <> rest:
735 part_box(p, s) ++ part_boxes(rest, s)
736
737def style(live: Bool) -> String:
738 match live:
739 case True{}:
740 "live"
741 case False{}:
742 "plain"
743
744def edges(xs: List<&2, Link>, +s: System) -> String:
745 match xs:
746 case []:
747 ""
748 case l <> rest:
749 match l:
750 case Link{src, dst, label, live}:
751 path(src, s) ++ " -> " ++ path(dst, s) ++ ": \"" ++ label ++ "\" {class: " ++ style(live) ++ "}\n" ++ edges(rest, s)
752
753def d2(+s: System) -> String:
754 "direction: right\n" ++
755 "classes: {\n" ++
756 " node: {style: {fill: \"#F2F2F2\"; stroke: \"#D9D9D9\"; border-radius: 14; font-size: 26; bold: true}}\n" ++
757 " container: {style: {fill: \"#FFFFFF\"; stroke: \"#8C8C8C\"; border-radius: 10; font-size: 22}}\n" ++
758 " part: {style: {fill: \"#FAFAFA\"; stroke: \"#BFBFBF\"; border-radius: 8; font-size: 18}}\n" ++
759 " live: {style: {stroke: \"#3E8A62\"; stroke-width: 3; font-color: \"#3E8A62\"; font-size: 18; bold: true}}\n" ++
760 " plain: {style: {stroke: \"#8C8C8C\"; stroke-width: 2; font-color: \"#8C8C8C\"; font-size: 16}}\n" ++
761 "}\n" ++
762 node_boxes(nodes(s)) ++ container_boxes(containers(s)) ++ part_boxes(parts(s), s) ++ edges(links(s), s)