1use crate::ast::{
6 Annotations, AuthorityExpr, Branch, CaseBranch, ChoiceGuard, Choreography, Condition,
7 MessageType, Protocol, Role, RoleParam,
8};
9use crate::compiler::parser::parse_choreography_str;
10
11#[derive(Debug, Clone)]
12pub struct PrettyConfig {
13 pub indent: usize,
14}
15
16impl Default for PrettyConfig {
17 fn default() -> Self {
18 Self { indent: 2 }
19 }
20}
21
22pub fn format_choreography(choreo: &Choreography) -> String {
23 format_choreography_with_config(choreo, &PrettyConfig::default())
24}
25
26pub fn format_choreography_with_config(choreo: &Choreography, config: &PrettyConfig) -> String {
27 let mut out = String::new();
28
29 if let Some(namespace) = &choreo.namespace {
30 out.push_str(&format!(
31 "module {} exposing ({})\n\n",
32 namespace, choreo.name
33 ));
34 }
35
36 out.push_str(&format!("protocol {} =\n", choreo.name));
37 write_line(
38 &mut out,
39 config.indent,
40 &format!("roles {}", format_role_list(&choreo.roles)),
41 );
42 format_protocol(&choreo.protocol, config.indent, config, &mut out);
43
44 out
45}
46
47pub fn format_choreography_str(input: &str) -> Result<String, crate::compiler::parser::ParseError> {
48 let choreo = parse_choreography_str(input)?;
49 Ok(format_choreography(&choreo))
50}
51
52fn format_protocol(protocol: &Protocol, indent: usize, config: &PrettyConfig, out: &mut String) {
54 match protocol {
55 Protocol::End => {}
56 Protocol::Begin {
57 operation,
58 args,
59 progress,
60 continuation,
61 } => {
62 let mut line = if args.is_empty() {
63 format!("begin {}", operation)
64 } else {
65 format!("begin {}({})", operation, args.join(", "))
66 };
67 if let Some(progress) = progress {
68 line.push_str(&format!(" {}", format_progress_attachment(progress)));
69 }
70 write_line(out, indent, &line);
71 format_protocol(continuation, indent, config, out);
72 }
73 Protocol::Await {
74 operation,
75 continuation,
76 } => {
77 write_line(out, indent, &format!("await {}", operation));
78 format_protocol(continuation, indent, config, out);
79 }
80 Protocol::Resolve {
81 operation,
82 outcome,
83 continuation,
84 } => {
85 write_line(
86 out,
87 indent,
88 &format!(
89 "resolve {} as {}",
90 operation,
91 format_commitment_outcome(outcome)
92 ),
93 );
94 format_protocol(continuation, indent, config, out);
95 }
96 Protocol::Invalidate {
97 operation,
98 continuation,
99 } => {
100 write_line(out, indent, &format!("invalidate {}", operation));
101 format_protocol(continuation, indent, config, out);
102 }
103 Protocol::Send {
104 from,
105 to,
106 message,
107 annotations,
108 from_annotations,
109 continuation,
110 ..
111 } => format_send_protocol(
112 from,
113 annotations,
114 from_annotations,
115 to,
116 message,
117 continuation,
118 indent,
119 config,
120 out,
121 ),
122 Protocol::Broadcast {
123 from,
124 message,
125 annotations,
126 from_annotations,
127 continuation,
128 ..
129 } => format_broadcast_protocol(
130 from,
131 annotations,
132 from_annotations,
133 message,
134 continuation,
135 indent,
136 config,
137 out,
138 ),
139 Protocol::Choice { role, branches, .. } => {
140 format_choice_protocol(role, branches, indent, config, out)
141 }
142 Protocol::Let {
143 name,
144 expr,
145 continuation,
146 ..
147 } => {
148 write_line(
149 out,
150 indent,
151 &format!("let {} = {}", name, format_authority_expr(expr)),
152 );
153 format_protocol(continuation, indent, config, out);
154 }
155 Protocol::Case { expr, branches } => {
156 write_line(
157 out,
158 indent,
159 &format!("case {} of", format_authority_expr(expr)),
160 );
161 for branch in branches {
162 format_case_branch(branch, indent + config.indent, config, out);
163 }
164 }
165 Protocol::Timeout {
166 role,
167 duration_ms,
168 body,
169 on_timeout,
170 on_cancel,
171 } => {
172 write_line(
173 out,
174 indent,
175 &format!("timeout {}ms {} at", duration_ms, format_role_ref(role)),
176 );
177 format_protocol(body, indent + config.indent, config, out);
178 write_line(out, indent, "on timeout =>");
179 format_protocol(on_timeout, indent + config.indent, config, out);
180 if let Some(on_cancel) = on_cancel.as_deref() {
181 write_line(out, indent, "on cancel =>");
182 format_protocol(on_cancel, indent + config.indent, config, out);
183 }
184 }
185 Protocol::Loop { condition, body } => {
186 format_loop_protocol(condition, body, indent, config, out)
187 }
188 Protocol::Parallel { protocols } => {
189 format_parallel_protocol(protocols, indent, config, out)
190 }
191 Protocol::Rec { label, body } => format_rec_protocol(label, body, indent, config, out),
192 Protocol::Var(label) => {
193 write_line(out, indent, &format!("continue {}", label));
194 }
195 Protocol::Publish {
196 event,
197 arg,
198 continuation,
199 } => {
200 if let Some(arg) = arg {
201 write_line(out, indent, &format!("publish {}{}", event, arg));
202 } else {
203 write_line(out, indent, &format!("publish {}", event));
204 }
205 format_protocol(continuation, indent, config, out);
206 }
207 Protocol::PublishAuthority {
208 witness,
209 publication_name,
210 continuation,
211 } => {
212 write_line(
213 out,
214 indent,
215 &format!("publish {} as {}", witness, publication_name),
216 );
217 format_protocol(continuation, indent, config, out);
218 }
219 Protocol::Materialize {
220 proof,
221 publication,
222 continuation,
223 } => {
224 write_line(
225 out,
226 indent,
227 &format!("materialize {} from {}", proof, publication),
228 );
229 format_protocol(continuation, indent, config, out);
230 }
231 Protocol::Handoff {
232 operation,
233 target,
234 receipt,
235 continuation,
236 } => {
237 write_line(
238 out,
239 indent,
240 &format!(
241 "handoff {} to {} using {}",
242 operation,
243 format_role_ref(target),
244 receipt
245 ),
246 );
247 format_protocol(continuation, indent, config, out);
248 }
249 Protocol::DependentWork {
250 name,
251 arg,
252 required_for,
253 continuation,
254 } => {
255 let work_head = match arg {
256 Some(arg) => format!(
257 "dependent work {}{} required for {}",
258 name, arg, required_for
259 ),
260 None => format!("dependent work {} required for {}", name, required_for),
261 };
262 write_line(out, indent, &work_head);
263 format_protocol(continuation, indent, config, out);
264 }
265 Protocol::Extension {
266 extension,
267 continuation,
268 ..
269 } => format_extension_protocol(extension.type_name(), continuation, indent, config, out),
270 }
271}
272
273fn format_progress_attachment(progress: &crate::ast::ProgressAttachment) -> String {
274 let mut parts = vec![format!("progress {}", progress.contract_name)];
275 if let Some(profile) = &progress.requires_profile {
276 parts.push(format!("requires {}", profile));
277 }
278 if let Some(window) = &progress.within_window {
279 parts.push(format!("within {}", window));
280 }
281 if let Some(timeout) = &progress.on_timeout {
282 parts.push(format!("on timeout => {}", timeout));
283 }
284 if let Some(stall) = &progress.on_stall {
285 parts.push(format!("on stall => {}", stall));
286 }
287 parts.join(" ")
288}
289
290fn format_commitment_outcome(outcome: &crate::ast::CommitmentOutcome) -> String {
291 match outcome {
292 crate::ast::CommitmentOutcome::Success(payload) => payload.as_ref().map_or_else(
293 || "Success".to_string(),
294 |payload| format!("Success({payload})"),
295 ),
296 crate::ast::CommitmentOutcome::Failure(payload) => payload.as_ref().map_or_else(
297 || "Failure".to_string(),
298 |payload| format!("Failure({payload})"),
299 ),
300 crate::ast::CommitmentOutcome::Timeout(payload) => payload.as_ref().map_or_else(
301 || "Timeout".to_string(),
302 |payload| format!("Timeout({payload})"),
303 ),
304 crate::ast::CommitmentOutcome::Cancelled => "Cancelled".to_string(),
305 }
306}
307
308fn format_send_protocol(
309 from: &Role,
310 annotations: &Annotations,
311 from_annotations: &Annotations,
312 to: &Role,
313 message: &MessageType,
314 continuation: &Protocol,
315 indent: usize,
316 config: &PrettyConfig,
317 out: &mut String,
318) {
319 let sender_annotations = merge_sender_annotations(from_annotations, annotations);
320 write_line(out, indent, &format_sender_term(from, &sender_annotations));
321 write_line(
322 out,
323 indent + config.indent,
324 &format!("-> {} : {}", format_role_ref(to), format_message(message)),
325 );
326 format_protocol(continuation, indent, config, out);
327}
328
329fn format_broadcast_protocol(
330 from: &Role,
331 annotations: &Annotations,
332 from_annotations: &Annotations,
333 message: &MessageType,
334 continuation: &Protocol,
335 indent: usize,
336 config: &PrettyConfig,
337 out: &mut String,
338) {
339 let sender_annotations = merge_sender_annotations(from_annotations, annotations);
340 write_line(out, indent, &format_sender_term(from, &sender_annotations));
341 write_line(
342 out,
343 indent + config.indent,
344 &format!("->* : {}", format_message(message)),
345 );
346 format_protocol(continuation, indent, config, out);
347}
348
349fn format_choice_protocol(
350 role: &Role,
351 branches: &[Branch],
352 indent: usize,
353 config: &PrettyConfig,
354 out: &mut String,
355) {
356 write_line(out, indent, &format!("choice {} at", format_role_ref(role)));
357 for branch in branches {
358 format_branch(branch, indent + config.indent, config, out);
359 }
360}
361
362fn format_loop_protocol(
363 condition: &Option<Condition>,
364 body: &Protocol,
365 indent: usize,
366 config: &PrettyConfig,
367 out: &mut String,
368) {
369 let header = format_loop_header(condition);
370 if is_end(body) {
371 write_line(out, indent, &format!("{} {{}}", header));
372 } else {
373 write_line(out, indent, &header);
374 format_protocol(body, indent + config.indent, config, out);
375 }
376}
377
378fn format_parallel_protocol(
379 protocols: &[Protocol],
380 indent: usize,
381 config: &PrettyConfig,
382 out: &mut String,
383) {
384 write_line(out, indent, "par");
385 for branch in protocols {
386 if is_end(branch) {
387 write_line(out, indent + config.indent, "| {}");
388 } else {
389 write_line(out, indent + config.indent, "|");
390 format_protocol(branch, indent + (2 * config.indent), config, out);
391 }
392 }
393}
394
395fn format_rec_protocol(
396 label: &proc_macro2::Ident,
397 body: &Protocol,
398 indent: usize,
399 config: &PrettyConfig,
400 out: &mut String,
401) {
402 if is_end(body) {
403 write_line(out, indent, &format!("rec {} {{}}", label));
404 } else {
405 write_line(out, indent, &format!("rec {}", label));
406 format_protocol(body, indent + config.indent, config, out);
407 }
408}
409
410fn format_extension_protocol(
411 extension_type_name: &str,
412 continuation: &Protocol,
413 indent: usize,
414 config: &PrettyConfig,
415 out: &mut String,
416) {
417 write_line(out, indent, &format!("// extension: {extension_type_name}"));
418 format_protocol(continuation, indent, config, out);
419}
420
421fn format_branch(branch: &Branch, indent: usize, config: &PrettyConfig, out: &mut String) {
422 let mut header = format!("| {}", branch.label);
423 if let Some(guard) = &branch.guard {
424 header.push_str(&format!(" {}", format_choice_guard(guard)));
425 }
426
427 if is_end(&branch.protocol) {
428 write_line(out, indent, &format!("{} => {{}}", header));
429 } else {
430 write_line(out, indent, &format!("{} =>", header));
431 format_protocol(&branch.protocol, indent + config.indent, config, out);
432 }
433}
434
435fn format_case_branch(branch: &CaseBranch, indent: usize, config: &PrettyConfig, out: &mut String) {
436 let binders = if branch.pattern.binders.is_empty() {
437 String::new()
438 } else {
439 format!("({})", branch.pattern.binders.join(", "))
440 };
441 let header = format!("| {}{} =>", branch.pattern.constructor, binders);
442 if is_end(&branch.protocol) {
443 write_line(out, indent, &format!("{header} {{}}"));
444 } else {
445 write_line(out, indent, &header);
446 format_protocol(&branch.protocol, indent + config.indent, config, out);
447 }
448}
449
450fn format_choice_guard(guard: &ChoiceGuard) -> String {
451 match guard {
452 ChoiceGuard::Predicate(tokens) => format!("when ({})", tokens),
453 ChoiceGuard::Evidence {
454 effect,
455 operation,
456 args,
457 binding,
458 } => {
459 let args = if args.is_empty() {
460 String::new()
461 } else {
462 args.join(", ")
463 };
464 format!(
465 "when check {}.{}({}) yields {}",
466 effect, operation, args, binding
467 )
468 }
469 }
470}
471
472fn format_authority_expr(expr: &AuthorityExpr) -> String {
473 match expr {
474 AuthorityExpr::Var(name) => name.clone(),
475 AuthorityExpr::Check {
476 effect,
477 operation,
478 args,
479 } => format!("check {}.{}({})", effect, operation, args.join(", ")),
480 AuthorityExpr::Observe {
481 effect,
482 operation,
483 args,
484 } => format!("observe {}.{}({})", effect, operation, args.join(", ")),
485 AuthorityExpr::Transfer { subject, from, to } => {
486 format!("transfer {} from {} to {}", subject, from, to)
487 }
488 AuthorityExpr::Constructor { name, arg } => match arg {
489 Some(arg) => format!("{name}({arg})"),
490 None => name.clone(),
491 },
492 AuthorityExpr::Call { name, args } => format!("{name}({})", args.join(", ")),
493 }
494}
495
496fn format_loop_header(condition: &Option<Condition>) -> String {
497 match condition {
498 Some(Condition::RoleDecides(role)) => {
499 format!("loop decide by {}", format_role_ref(role))
500 }
501 Some(Condition::Count(count)) => format!("loop repeat {}", count),
502 Some(Condition::Custom(tokens)) => format!("loop while {}", tokens),
503 Some(Condition::Fuel(count)) => format!("loop while \"fuel:{}\"", count),
504 Some(Condition::YieldAfter(count)) => format!("loop while \"yield_after:{}\"", count),
505 Some(Condition::YieldWhen(label)) => format!("loop while \"yield_when:{}\"", label),
506 None => "loop forever".to_string(),
507 }
508}
509
510fn format_role_list(roles: &[Role]) -> String {
511 roles
512 .iter()
513 .map(|role| {
514 let mut out = role.name().to_string();
515 if let Some(param) = role.param() {
516 out.push('[');
517 out.push_str(&format_role_param(param));
518 out.push(']');
519 }
520 out
521 })
522 .collect::<Vec<_>>()
523 .join(", ")
524}
525
526fn format_role_param(param: &RoleParam) -> String {
527 param.to_string()
528}
529
530fn format_role_ref(role: &Role) -> String {
531 let mut out = role.name().to_string();
532 if let Some(index) = role.index() {
533 out.push('[');
534 out.push_str(&index.to_string());
535 out.push(']');
536 }
537 out
538}
539
540fn format_sender_term(role: &Role, annotations: &Annotations) -> String {
541 let mut out = format_role_ref(role);
542 let entries = annotations.dsl_entries();
543 if !entries.is_empty() {
544 let formatted = entries
545 .into_iter()
546 .map(|entry| format!("{} : {}", entry.key, entry.value))
547 .collect::<Vec<_>>()
548 .join(", ");
549 out.push_str(" { ");
550 out.push_str(&formatted);
551 out.push_str(" }");
552 }
553 out
554}
555
556fn merge_sender_annotations(
557 sender_annotations: &Annotations,
558 statement_annotations: &Annotations,
559) -> Annotations {
560 let mut merged = sender_annotations.dsl_entries();
561 let mut existing_keys = merged
562 .iter()
563 .map(|entry| entry.key.clone())
564 .collect::<std::collections::BTreeSet<_>>();
565 for entry in statement_annotations.dsl_entries() {
566 if existing_keys.insert(entry.key.clone()) {
567 merged.push(entry);
568 }
569 }
570 Annotations::from_dsl_entries(&merged)
571}
572
573fn normalize_surface_type_string(s: &str) -> String {
574 s.replace(" :: ", ".").replace("::", ".")
575}
576
577fn format_message(message: &MessageType) -> String {
578 let mut out = message.name.to_string();
579 if let Some(payload) = &message.payload {
580 let payload_str = payload.to_string();
581 if payload_str.starts_with('(') {
582 out.push(' ');
583 out.push_str(&payload_str);
584 } else {
585 out.push_str(" of ");
586 out.push_str(&normalize_surface_type_string(&payload_str));
587 }
588 } else if let Some(type_annotation) = &message.type_annotation {
589 out.push_str(" of ");
590 out.push_str(&normalize_surface_type_string(&type_annotation.to_string()));
591 }
592 out
593}
594
595fn is_end(protocol: &Protocol) -> bool {
596 matches!(protocol, Protocol::End)
597}
598
599fn write_line(out: &mut String, indent: usize, text: &str) {
600 out.push_str(&" ".repeat(indent));
601 out.push_str(text);
602 out.push('\n');
603}
604
605#[cfg(test)]
606mod tests {
607 use super::*;
608
609 #[test]
610 fn pretty_roundtrip_basic() {
611 let input = "protocol PingPong =\n roles Alice, Bob\n Alice -> Bob : Ping\n Bob -> Alice : Pong\n";
612 let choreo = parse_choreography_str(input).expect("should parse");
613 let formatted = format_choreography(&choreo);
614 assert!(formatted.contains("Alice\n -> Bob : Ping"));
615 assert!(parse_choreography_str(&formatted).is_ok());
616 }
617
618 #[test]
619 fn pretty_roundtrip_choice_and_loop() {
620 let input = r#"
621protocol Demo =
622 roles Client, Server
623 choice Client at
624 | Buy =>
625 Client -> Server : Purchase
626 | Cancel =>
627 Client -> Server : Cancel
628 loop repeat 2
629 Client -> Server : Ping
630 Server -> Client : Pong
631"#;
632 let choreo = parse_choreography_str(input).expect("should parse");
633 let formatted = format_choreography(&choreo);
634 assert!(formatted.contains("choice Client at"));
635 assert!(formatted.contains("| Buy =>"));
636 assert!(parse_choreography_str(&formatted).is_ok());
637 }
638
639 #[test]
640 fn pretty_emits_aligned_arrows_and_sender_records() {
641 let input = r#"
642protocol Styled =
643 roles A, B, C, D
644 A { priority : high } -> B : Request of shop.Order
645 par
646 | C -> D : Left
647 | D -> C : Right
648"#;
649
650 let choreo = parse_choreography_str(input).expect("should parse");
651 let formatted = format_choreography(&choreo);
652 assert!(formatted.contains("A { priority : high }\n -> B : Request of shop.Order"));
653 assert!(formatted.contains("par\n |\n C\n -> D : Left"));
654 assert!(parse_choreography_str(&formatted).is_ok());
655 }
656
657 #[test]
658 fn pretty_is_stable_on_reformat() {
659 let input = r#"
660protocol Stable =
661 roles A, B
662 A { priority : high } -> B : Request of shop.Order
663"#;
664
665 let first = format_choreography_str(input).expect("first format should succeed");
666 let second = format_choreography_str(&first).expect("second format should succeed");
667 assert_eq!(first, second);
668 }
669}