1use std::fmt::Write;
12
13use crate::ast::{
14 BinOp, DecisionBlock, DecisionImpact, Expr, FnDef, Literal, Module, Pattern, Spanned, Stmt,
15 StrPart, TopLevel, TypeDef, VerifyBlock, VerifyGiven, VerifyGivenDomain, VerifyKind,
16};
17
18#[derive(Debug, Clone, PartialEq)]
21pub enum UnparseError {
22 Unsupported(&'static str),
28 FmtError,
32}
33
34impl std::fmt::Display for UnparseError {
35 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
36 match self {
37 UnparseError::Unsupported(tag) => write!(f, "unsupported AST variant: {tag}"),
38 UnparseError::FmtError => write!(f, "internal fmt error"),
39 }
40 }
41}
42
43impl std::error::Error for UnparseError {}
44
45impl From<std::fmt::Error> for UnparseError {
46 fn from(_: std::fmt::Error) -> Self {
47 UnparseError::FmtError
48 }
49}
50
51type Result<T> = std::result::Result<T, UnparseError>;
52
53const INDENT: &str = " ";
54
55pub fn unparse(items: &[TopLevel]) -> Result<String> {
60 let mut out = String::with_capacity(items.len() * 64);
61 let mut first = true;
62 for item in items {
63 if !first {
64 out.push('\n');
65 }
66 first = false;
67 write_top_level(&mut out, item)?;
68 if !out.ends_with('\n') {
69 out.push('\n');
70 }
71 }
72 if out.is_empty() {
73 out.push('\n');
76 }
77 Ok(out)
78}
79
80fn write_top_level(out: &mut String, item: &TopLevel) -> Result<()> {
81 match item {
82 TopLevel::Module(m) => write_module(out, m),
83 TopLevel::TypeDef(td) => write_typedef(out, td),
84 TopLevel::FnDef(fd) => write_fndef(out, fd),
85 TopLevel::Verify(vb) => write_verify(out, vb),
86 TopLevel::Decision(db) => write_decision(out, db),
87 TopLevel::Stmt(stmt) => write_stmt(out, stmt, 0),
88 }
89}
90
91fn write_module(out: &mut String, m: &Module) -> Result<()> {
92 writeln!(out, "module {}", m.name)?;
93 if !m.intent.is_empty() {
94 writeln!(out, "{INDENT}intent =")?;
97 for line in m.intent.split('\n') {
98 let trimmed = line.trim();
99 if trimmed.is_empty() {
100 continue;
101 }
102 writeln!(out, "{INDENT}{INDENT}{}", quote_string(trimmed))?;
103 }
104 }
105 if !m.depends.is_empty() {
106 writeln!(out, "{INDENT}depends [{}]", m.depends.join(", "))?;
107 }
108 if !m.exposes.is_empty() || !m.exposes_opaque.is_empty() {
109 let names: Vec<String> = m
113 .exposes
114 .iter()
115 .cloned()
116 .chain(m.exposes_opaque.iter().map(|n| format!("opaque {n}")))
117 .collect();
118 writeln!(out, "{INDENT}exposes [{}]", names.join(", "))?;
119 }
120 if let Some(effects) = &m.effects {
121 writeln!(out, "{INDENT}effects [{}]", effects.join(", "))?;
122 }
123 Ok(())
124}
125
126fn write_typedef(out: &mut String, td: &TypeDef) -> Result<()> {
127 match td {
128 TypeDef::Sum { name, variants, .. } => {
129 writeln!(out, "type {name}")?;
130 for v in variants {
131 if v.fields.is_empty() {
132 writeln!(out, "{INDENT}{}", v.name)?;
133 } else {
134 writeln!(out, "{INDENT}{}({})", v.name, v.fields.join(", "))?;
135 }
136 }
137 }
138 TypeDef::Product { name, fields, .. } => {
139 writeln!(out, "record {name}")?;
140 for (fname, fty) in fields {
141 writeln!(out, "{INDENT}{fname}: {fty}")?;
142 }
143 }
144 }
145 Ok(())
146}
147
148fn write_fndef(out: &mut String, fd: &FnDef) -> Result<()> {
149 let params: Vec<String> = fd.params.iter().map(|(n, t)| format!("{n}: {t}")).collect();
150 writeln!(
157 out,
158 "fn {}({}) -> {}",
159 fd.name,
160 params.join(", "),
161 fd.return_type
162 )?;
163 if let Some(desc) = &fd.desc {
164 writeln!(out, "{INDENT}? {}", quote_string(desc))?;
165 }
166 if !fd.effects.is_empty() {
167 let names: Vec<String> = fd.effects.iter().map(|e| e.node.clone()).collect();
168 writeln!(out, "{INDENT}! [{}]", names.join(", "))?;
169 }
170 for stmt in fd.body.stmts() {
171 write_stmt(out, stmt, 1)?;
172 }
173 Ok(())
174}
175
176fn write_stmt(out: &mut String, stmt: &Stmt, indent: usize) -> Result<()> {
177 let pad = INDENT.repeat(indent);
178 match stmt {
179 Stmt::Binding(name, ty, expr) => {
180 let ty_part = ty.as_deref().map(|t| format!(": {t}")).unwrap_or_default();
181 write!(out, "{pad}{name}{ty_part} = ")?;
182 write_expr(out, expr, indent)?;
183 writeln!(out)?;
184 }
185 Stmt::Expr(expr) => {
186 write!(out, "{pad}")?;
187 write_expr(out, expr, indent)?;
188 writeln!(out)?;
189 }
190 }
191 Ok(())
192}
193
194fn write_verify(out: &mut String, vb: &VerifyBlock) -> Result<()> {
195 match &vb.kind {
196 VerifyKind::Cases => {
197 let header = if vb.trace {
198 "verify {} trace"
199 } else {
200 "verify {}"
201 };
202 let header = header.replace("{}", &vb.fn_name);
203 writeln!(out, "{header}")?;
204 for given in &vb.cases_givens {
205 write_given(out, given, 1)?;
206 }
207 for (lhs, rhs) in &vb.cases {
208 write!(out, "{INDENT}")?;
209 write_expr(out, lhs, 1)?;
210 write!(out, " => ")?;
211 write_expr(out, rhs, 1)?;
212 writeln!(out)?;
213 }
214 }
215 VerifyKind::Law(law) => {
216 let header = if vb.trace {
217 format!("verify {} law {} trace", vb.fn_name, law.name)
218 } else {
219 format!("verify {} law {}", vb.fn_name, law.name)
220 };
221 writeln!(out, "{header}")?;
222 for given in &law.givens {
223 write_given(out, given, 1)?;
224 }
225 if let Some(when_expr) = &law.when {
226 write!(out, "{INDENT}when ")?;
227 write_expr(out, when_expr, 1)?;
228 writeln!(out)?;
229 }
230 write!(out, "{INDENT}")?;
231 write_expr(out, &law.lhs, 1)?;
232 write!(out, " => ")?;
233 write_expr(out, &law.rhs, 1)?;
234 writeln!(out)?;
235 }
236 }
237 Ok(())
238}
239
240fn write_given(out: &mut String, given: &VerifyGiven, indent: usize) -> Result<()> {
241 let pad = INDENT.repeat(indent);
242 match &given.domain {
243 VerifyGivenDomain::IntRange { start, end } => {
244 writeln!(
245 out,
246 "{pad}given {}: {} = {}..{}",
247 given.name, given.type_name, start, end
248 )?;
249 }
250 VerifyGivenDomain::Explicit(values) => {
251 write!(out, "{pad}given {}: {} = [", given.name, given.type_name)?;
252 for (i, v) in values.iter().enumerate() {
253 if i > 0 {
254 write!(out, ", ")?;
255 }
256 write_expr(out, v, indent)?;
257 }
258 writeln!(out, "]")?;
259 }
260 }
261 Ok(())
262}
263
264fn write_decision(out: &mut String, db: &DecisionBlock) -> Result<()> {
265 writeln!(out, "decision {}", db.name)?;
266 if !db.date.is_empty() {
267 writeln!(out, "{INDENT}date = {}", quote_string(&db.date))?;
268 }
269 if !db.reason.is_empty() {
270 writeln!(out, "{INDENT}reason =")?;
280 for line in db.reason.split('\n') {
281 let trimmed = line.trim();
282 if trimmed.is_empty() {
283 continue;
284 }
285 writeln!(out, "{INDENT}{INDENT}{}", quote_string(trimmed))?;
286 }
287 }
288 let chosen_text = decision_impact_text(&db.chosen.node);
289 writeln!(out, "{INDENT}chosen = {}", quote_string(chosen_text))?;
290 if !db.rejected.is_empty() {
291 let parts: Vec<String> = db
292 .rejected
293 .iter()
294 .map(|r| quote_string(decision_impact_text(&r.node)))
295 .collect();
296 writeln!(out, "{INDENT}rejected = [{}]", parts.join(", "))?;
297 }
298 if !db.impacts.is_empty() {
299 let parts: Vec<String> = db
303 .impacts
304 .iter()
305 .map(|i| match &i.node {
306 DecisionImpact::Symbol(s) => s.clone(),
307 DecisionImpact::Semantic(s) => quote_string(s),
308 })
309 .collect();
310 writeln!(out, "{INDENT}impacts = [{}]", parts.join(", "))?;
311 }
312 if let Some(author) = &db.author {
313 writeln!(out, "{INDENT}author = {}", quote_string(author))?;
314 }
315 Ok(())
316}
317
318fn decision_impact_text(impact: &DecisionImpact) -> &str {
319 match impact {
320 DecisionImpact::Symbol(s) | DecisionImpact::Semantic(s) => s,
321 }
322}
323
324pub fn write_expr_public(out: &mut String, expr: &Spanned<Expr>, indent: usize) -> Result<()> {
332 write_expr(out, expr, indent)
333}
334
335fn write_expr(out: &mut String, expr: &Spanned<Expr>, indent: usize) -> Result<()> {
336 match &expr.node {
337 Expr::Literal(lit) => write_literal(out, lit),
338 Expr::Ident(name) => {
339 out.push_str(name);
340 Ok(())
341 }
342 Expr::Attr(inner, field) => {
343 out.push('(');
347 write_expr(out, inner, indent)?;
348 out.push(')');
349 out.push('.');
350 out.push_str(field);
351 Ok(())
352 }
353 Expr::FnCall(callee, args) => {
354 write_expr(out, callee, indent)?;
355 out.push('(');
356 for (i, arg) in args.iter().enumerate() {
357 if i > 0 {
358 out.push_str(", ");
359 }
360 write_expr(out, arg, indent)?;
361 }
362 out.push(')');
363 Ok(())
364 }
365 Expr::BinOp(op, lhs, rhs) => {
366 out.push('(');
367 write_expr(out, lhs, indent)?;
368 write!(out, " {} ", binop_str(*op))?;
369 write_expr(out, rhs, indent)?;
370 out.push(')');
371 Ok(())
372 }
373 Expr::Neg(inner) => {
374 out.push_str("(-");
375 write_expr(out, inner, indent)?;
376 out.push(')');
377 Ok(())
378 }
379 Expr::Match { subject, arms } => {
380 out.push_str("match ");
381 write_expr(out, subject, indent)?;
382 out.push('\n');
383 let pad = INDENT.repeat(indent + 1);
384 for arm in arms {
385 out.push_str(&pad);
386 write_pattern(out, &arm.pattern)?;
387 out.push_str(" -> ");
388 write_expr(out, &arm.body, indent + 1)?;
389 out.push('\n');
390 }
391 if out.ends_with('\n') {
395 out.pop();
396 }
397 Ok(())
398 }
399 Expr::Constructor(name, arg) => {
400 out.push_str(name);
401 if let Some(arg) = arg {
402 out.push('(');
403 write_expr(out, arg, indent)?;
404 out.push(')');
405 }
406 Ok(())
407 }
408 Expr::ErrorProp(inner) => {
409 out.push('(');
410 write_expr(out, inner, indent)?;
411 out.push_str(")?");
412 Ok(())
413 }
414 Expr::InterpolatedStr(parts) => {
415 out.push('"');
416 for part in parts {
417 match part {
418 StrPart::Literal(s) => out.push_str(&escape_string_inner(s)),
419 StrPart::Parsed(e) => {
420 out.push('{');
421 write_expr(out, e, indent)?;
422 out.push('}');
423 }
424 }
425 }
426 out.push('"');
427 Ok(())
428 }
429 Expr::List(items) => {
430 out.push('[');
431 for (i, item) in items.iter().enumerate() {
432 if i > 0 {
433 out.push_str(", ");
434 }
435 write_expr(out, item, indent)?;
436 }
437 out.push(']');
438 Ok(())
439 }
440 Expr::Tuple(items) => {
441 out.push('(');
442 for (i, item) in items.iter().enumerate() {
443 if i > 0 {
444 out.push_str(", ");
445 }
446 write_expr(out, item, indent)?;
447 }
448 out.push(')');
449 Ok(())
450 }
451 Expr::MapLiteral(entries) => {
452 out.push('{');
453 for (i, (k, v)) in entries.iter().enumerate() {
454 if i > 0 {
455 out.push_str(", ");
456 }
457 write_expr(out, k, indent)?;
458 out.push_str(" => ");
459 write_expr(out, v, indent)?;
460 }
461 out.push('}');
462 Ok(())
463 }
464 Expr::RecordCreate { type_name, fields } => {
465 out.push_str(type_name);
466 out.push('(');
467 for (i, (fname, val)) in fields.iter().enumerate() {
468 if i > 0 {
469 out.push_str(", ");
470 }
471 write!(out, "{fname} = ")?;
472 write_expr(out, val, indent)?;
473 }
474 out.push(')');
475 Ok(())
476 }
477 Expr::RecordUpdate {
478 type_name,
479 base,
480 updates,
481 } => {
482 write!(out, "{type_name}.update(")?;
483 write_expr(out, base, indent)?;
484 for (fname, val) in updates {
485 write!(out, ", {fname} = ")?;
486 write_expr(out, val, indent)?;
487 }
488 out.push(')');
489 Ok(())
490 }
491 Expr::IndependentProduct(items, unwrap) => {
492 out.push('(');
493 for (i, item) in items.iter().enumerate() {
494 if i > 0 {
495 out.push_str(", ");
496 }
497 write_expr(out, item, indent)?;
498 }
499 out.push(')');
500 out.push_str(if *unwrap { "?!" } else { "!" });
501 Ok(())
502 }
503 Expr::TailCall(_) => Err(UnparseError::Unsupported("Expr::TailCall")),
504 Expr::Resolved { .. } => Err(UnparseError::Unsupported("Expr::Resolved")),
505 }
506}
507
508fn binop_str(op: BinOp) -> &'static str {
509 match op {
510 BinOp::Add => "+",
511 BinOp::Sub => "-",
512 BinOp::Mul => "*",
513 BinOp::Div => "/",
514 BinOp::Eq => "==",
515 BinOp::Neq => "!=",
516 BinOp::Lt => "<",
517 BinOp::Gt => ">",
518 BinOp::Lte => "<=",
519 BinOp::Gte => ">=",
520 }
521}
522
523fn write_literal(out: &mut String, lit: &Literal) -> Result<()> {
524 match lit {
525 Literal::Int(i) => write!(out, "{i}")?,
526 Literal::BigInt(s) => write!(out, "{s}")?,
529 Literal::Float(f) => {
530 let s = format!("{f}");
535 if s.contains('.') || s.contains('e') || s.contains('E') {
536 write!(out, "{s}")?;
537 } else {
538 write!(out, "{s}.0")?;
539 }
540 }
541 Literal::Str(s) => {
542 out.push('"');
543 out.push_str(&escape_string_inner(s));
544 out.push('"');
545 }
546 Literal::Bool(b) => out.push_str(if *b { "true" } else { "false" }),
547 Literal::Unit => out.push_str("Unit"),
548 }
549 Ok(())
550}
551
552fn write_pattern(out: &mut String, pattern: &Pattern) -> Result<()> {
553 match pattern {
554 Pattern::Wildcard => {
555 out.push('_');
556 Ok(())
557 }
558 Pattern::Literal(lit) => write_literal(out, lit),
559 Pattern::Ident(name) => {
560 out.push_str(name);
561 Ok(())
562 }
563 Pattern::EmptyList => {
564 out.push_str("[]");
565 Ok(())
566 }
567 Pattern::Cons(head, tail) => {
568 write!(out, "[{head}, ..{tail}]")?;
569 Ok(())
570 }
571 Pattern::Tuple(items) => {
572 out.push('(');
573 for (i, item) in items.iter().enumerate() {
574 if i > 0 {
575 out.push_str(", ");
576 }
577 write_pattern(out, item)?;
578 }
579 out.push(')');
580 Ok(())
581 }
582 Pattern::Constructor(name, bindings) => {
583 out.push_str(name);
584 if !bindings.is_empty() {
585 out.push('(');
586 out.push_str(&bindings.join(", "));
587 out.push(')');
588 }
589 Ok(())
590 }
591 }
592}
593
594fn escape_string_inner(s: &str) -> String {
602 let mut out = String::with_capacity(s.len());
603 for c in s.chars() {
604 match c {
605 '"' => out.push_str("\\\""),
606 '\\' => out.push_str("\\\\"),
607 '\n' => out.push_str("\\n"),
608 '\r' => out.push_str("\\r"),
609 '\t' => out.push_str("\\t"),
610 '{' => out.push_str("\\{"),
614 '}' => out.push_str("\\}"),
615 c if (c as u32) < 0x20 => {
616 write!(out, "\\x{:02x}", c as u32).ok();
619 }
620 c => out.push(c),
621 }
622 }
623 out
624}
625
626fn quote_string(s: &str) -> String {
630 let mut out = String::with_capacity(s.len() + 2);
631 out.push('"');
632 out.push_str(&escape_string_inner(s));
633 out.push('"');
634 out
635}