1use std::{io::Write, vec};
4
5use crate::ast::*;
6
7pub fn print<W: Write>(defs: &[Def], width: usize, out: &mut W) -> std::io::Result<()> {
9 for (i, def) in defs.iter().enumerate() {
10 if i > 0 {
11 writeln!(out)?;
12 }
13 print_node(def, width, out)?;
14 writeln!(out)?;
15 }
16 Ok(())
17}
18
19pub fn dump<N: ToSExpr>(node: &N) -> std::io::Result<()> {
21 print_node(node, 120, &mut std::io::stdout())
22}
23
24pub fn print_node<N: ToSExpr, W: Write>(
26 node: &N,
27 width: usize,
28 out: &mut W,
29) -> std::io::Result<()> {
30 let mut printer = Printer::new(out, width);
31 let sexpr = node.to_sexpr();
32 printer.print(&sexpr)
33}
34
35#[derive(Debug, Clone, PartialEq, Eq)]
37pub enum SExpr {
38 Atom(String),
40 Binding(String, Box<SExpr>),
42 List(Vec<SExpr>),
44}
45
46pub trait ToSExpr {
48 fn to_sexpr(&self) -> SExpr;
50}
51
52impl SExpr {
53 fn atom<S: ToString>(atom: S) -> Self {
54 SExpr::Atom(atom.to_string())
55 }
56
57 fn list(items: &[impl ToSExpr]) -> Self {
58 SExpr::List(items.into_iter().map(|i| i.to_sexpr()).collect())
59 }
60
61 fn tagged(tag: &str, items: &[impl ToSExpr]) -> Self {
62 let mut parts = vec![SExpr::atom(tag)];
63 parts.extend(items.iter().map(ToSExpr::to_sexpr));
64 SExpr::List(parts)
65 }
66}
67
68struct Printer<'a, W: Write> {
69 out: &'a mut W,
70 col: usize,
71 indent: usize,
72 width: usize,
73}
74
75#[derive(Clone, Copy, PartialEq, Eq)]
76enum Wrapping {
77 Wrap,
78 SingleLine,
79}
80
81impl<'a, W: Write> Printer<'a, W> {
82 fn new(out: &'a mut W, width: usize) -> Self {
83 Self {
84 out,
85 col: 0,
86 indent: 0,
87 width,
88 }
89 }
90
91 fn print(&mut self, sexpr: &SExpr) -> std::io::Result<()> {
92 self.print_wrapped(sexpr, Wrapping::Wrap)
93 }
94
95 fn print_wrapped(&mut self, sexpr: &SExpr, wrapping: Wrapping) -> std::io::Result<()> {
96 match sexpr {
97 SExpr::Atom(atom) => self.put(atom),
98 SExpr::Binding(name, sexpr) => {
99 self.put(name)?;
100 self.put(" @ ")?;
101 self.print_wrapped(sexpr, wrapping)
102 }
103 SExpr::List(items) => {
104 if wrapping == Wrapping::SingleLine || self.fits(sexpr) {
105 self.put("(")?;
106 for (i, item) in items.iter().enumerate() {
107 if i > 0 {
108 self.put(" ")?;
109 }
110 self.print_wrapped(item, Wrapping::SingleLine)?;
111 }
112 self.put(")")
113 } else {
114 let (first, rest) = items.split_first().expect("non-empty list");
115 self.put("(")?;
116 self.print_wrapped(first, wrapping)?;
117 self.indent += 1;
118 for item in rest {
119 self.nl()?;
120 self.print_wrapped(item, wrapping)?;
121 }
122 self.indent -= 1;
123 self.nl()?;
124 self.put(")")?;
125 Ok(())
126 }
127 }
128 }
129 }
130
131 fn fits(&self, sexpr: &SExpr) -> bool {
133 let Some(mut remaining) = self.width.checked_sub(self.col) else {
134 return false;
135 };
136 let mut stack = vec![sexpr];
137 while let Some(sexpr) = stack.pop() {
138 let consume = match sexpr {
139 SExpr::Atom(atom) => atom.len(),
140 SExpr::Binding(name, inner) => {
141 stack.push(inner);
142 name.len() + 3 }
144 SExpr::List(items) => {
145 stack.extend(items.iter().rev());
146 2 + items.len() - 1 }
148 };
149 if consume > remaining {
150 return false;
151 }
152 remaining -= consume;
153 }
154 true
155 }
156
157 fn put(&mut self, s: &str) -> std::io::Result<()> {
158 write!(self.out, "{s}")?;
159 self.col += s.len();
160 Ok(())
161 }
162
163 fn nl(&mut self) -> std::io::Result<()> {
164 writeln!(self.out)?;
165 self.col = 0;
166 for _ in 0..self.indent {
167 write!(self.out, " ")?;
168 }
169 Ok(())
170 }
171}
172
173impl ToSExpr for Def {
174 fn to_sexpr(&self) -> SExpr {
175 match self {
176 Def::Pragma(_) => unimplemented!("pragmas not supported"),
177 Def::Type(ty) => ty.to_sexpr(),
178 Def::Rule(rule) => rule.to_sexpr(),
179 Def::Extractor(extractor) => extractor.to_sexpr(),
180 Def::Decl(decl) => decl.to_sexpr(),
181 Def::Spec(spec) => spec.to_sexpr(),
182 Def::Model(model) => model.to_sexpr(),
183 Def::Form(form) => form.to_sexpr(),
184 Def::Instantiation(instantiation) => instantiation.to_sexpr(),
185 Def::Extern(ext) => ext.to_sexpr(),
186 Def::Converter(converter) => converter.to_sexpr(),
187 Def::Attr(attr) => attr.to_sexpr(),
188 Def::SpecMacro(spec_macro) => spec_macro.to_sexpr(),
189 Def::State(state) => state.to_sexpr(),
190 }
191 }
192}
193
194impl ToSExpr for Type {
195 fn to_sexpr(&self) -> SExpr {
196 let Type {
197 name,
198 ty,
199 is_extern,
200 is_nodebug,
201 pos: _,
202 } = self;
203 let mut parts = vec![SExpr::atom("type"), name.to_sexpr()];
204 if *is_extern {
205 parts.push(SExpr::atom("extern"));
206 }
207 if *is_nodebug {
208 parts.push(SExpr::Atom("nodebug".to_string()));
209 }
210 parts.push(ty.to_sexpr());
211 SExpr::List(parts)
212 }
213}
214
215impl ToSExpr for Rule {
216 fn to_sexpr(&self) -> SExpr {
217 let Rule {
218 name,
219 prio,
220 pattern,
221 iflets,
222 expr,
223 pos: _,
224 } = self;
225 let mut parts = vec![SExpr::atom("rule")];
226 if let Some(name) = name {
227 parts.push(name.to_sexpr());
228 }
229 if let Some(prio) = prio {
230 parts.push(SExpr::atom(prio.to_string()));
231 }
232 parts.push(pattern.to_sexpr());
233 parts.extend(iflets.iter().map(ToSExpr::to_sexpr));
234 parts.push(expr.to_sexpr());
235 SExpr::List(parts)
236 }
237}
238
239impl ToSExpr for Extractor {
240 fn to_sexpr(&self) -> SExpr {
241 let Extractor {
242 term,
243 args,
244 template,
245 pos: _,
246 } = self;
247 let mut sig = vec![term.to_sexpr()];
248 sig.extend(args.iter().map(ToSExpr::to_sexpr));
249
250 let mut parts = vec![SExpr::atom("extractor")];
251 parts.push(SExpr::List(sig));
252 parts.push(template.to_sexpr());
253 SExpr::List(parts)
254 }
255}
256
257impl ToSExpr for Decl {
258 fn to_sexpr(&self) -> SExpr {
259 let Decl {
260 term,
261 arg_tys,
262 ret_ty,
263 pure,
264 multi,
265 partial,
266 rec,
267 pos: _,
268 } = self;
269 let mut parts = vec![SExpr::atom("decl")];
270 if *pure {
271 parts.push(SExpr::atom("pure"));
272 }
273 if *multi {
274 parts.push(SExpr::atom("multi"));
275 }
276 if *partial {
277 parts.push(SExpr::atom("partial"));
278 }
279 if *rec {
280 parts.push(SExpr::atom("rec"));
281 }
282 parts.push(term.to_sexpr());
283 parts.push(SExpr::list(arg_tys));
284 parts.push(ret_ty.to_sexpr());
285 SExpr::List(parts)
286 }
287}
288
289impl ToSExpr for Spec {
290 fn to_sexpr(&self) -> SExpr {
291 let Spec {
292 term,
293 args,
294 provides,
295 requires,
296 matches,
297 modifies,
298 pos: _,
299 } = self;
300 let mut sig = vec![term.to_sexpr()];
301 sig.extend(args.iter().map(ToSExpr::to_sexpr));
302
303 let mut parts = vec![SExpr::atom("spec")];
304 parts.push(SExpr::List(sig));
305 if !provides.is_empty() {
306 parts.push(SExpr::tagged("provide", provides));
307 }
308 if !requires.is_empty() {
309 parts.push(SExpr::tagged("require", requires));
310 }
311 if !matches.is_empty() {
312 parts.push(SExpr::tagged("match", matches));
313 }
314 for modifies in modifies {
315 parts.push(modifies.to_sexpr());
316 }
317 SExpr::List(parts)
318 }
319}
320
321impl ToSExpr for Modifies {
322 fn to_sexpr(&self) -> SExpr {
323 let Modifies { state, cond } = self;
324 let mut parts = vec![SExpr::atom("modifies"), state.to_sexpr()];
325 if let Some(cond) = cond {
326 parts.push(cond.to_sexpr());
327 }
328 SExpr::List(parts)
329 }
330}
331
332impl ToSExpr for Model {
333 fn to_sexpr(&self) -> SExpr {
334 let Model { name, val } = self;
335 SExpr::List(vec![SExpr::atom("model"), name.to_sexpr(), val.to_sexpr()])
336 }
337}
338
339impl ToSExpr for Form {
340 fn to_sexpr(&self) -> SExpr {
341 let Form {
342 name,
343 signatures,
344 pos: _,
345 } = self;
346 let mut parts = vec![SExpr::atom("form"), name.to_sexpr()];
347 parts.extend(signatures.iter().map(ToSExpr::to_sexpr));
348 SExpr::List(parts)
349 }
350}
351
352impl ToSExpr for Instantiation {
353 fn to_sexpr(&self) -> SExpr {
354 let Instantiation {
355 term,
356 form,
357 signatures,
358 tags,
359 pos: _,
360 } = self;
361 let mut parts = vec![SExpr::atom("instantiate"), term.to_sexpr()];
362 if let Some(form) = form {
363 parts.push(form.to_sexpr());
364 } else {
365 parts.extend(signatures.iter().map(ToSExpr::to_sexpr));
366 }
367 parts.extend(
368 tags.iter()
369 .map(|tag| SExpr::List(vec![SExpr::atom("tag"), tag.to_sexpr()])),
370 );
371 SExpr::List(parts)
372 }
373}
374
375impl ToSExpr for Extern {
376 fn to_sexpr(&self) -> SExpr {
377 match self {
378 Extern::Extractor {
379 term,
380 func,
381 infallible,
382 pos: _,
383 } => {
384 let mut parts = vec![SExpr::atom("extern"), SExpr::atom("extractor")];
385 if *infallible {
386 parts.push(SExpr::atom("infallible"));
387 }
388 parts.push(term.to_sexpr());
389 parts.push(func.to_sexpr());
390 SExpr::List(parts)
391 }
392 Extern::Constructor { term, func, pos: _ } => SExpr::List(vec![
393 SExpr::atom("extern"),
394 SExpr::atom("constructor"),
395 term.to_sexpr(),
396 func.to_sexpr(),
397 ]),
398 Extern::Const { name, ty, pos: _ } => SExpr::List(vec![
399 SExpr::atom("extern"),
400 SExpr::atom("const"),
401 SExpr::atom(format!("${}", name.0)),
402 ty.to_sexpr(),
403 ]),
404 }
405 }
406}
407
408impl ToSExpr for Converter {
409 fn to_sexpr(&self) -> SExpr {
410 let Converter {
411 inner_ty,
412 outer_ty,
413 term,
414 pos: _,
415 } = self;
416 SExpr::List(vec![
417 SExpr::atom("convert"),
418 inner_ty.to_sexpr(),
419 outer_ty.to_sexpr(),
420 term.to_sexpr(),
421 ])
422 }
423}
424
425impl ToSExpr for TypeValue {
426 fn to_sexpr(&self) -> SExpr {
427 match self {
428 TypeValue::Primitive(name, _) => {
429 SExpr::List(vec![SExpr::atom("primitive"), name.to_sexpr()])
430 }
431 TypeValue::Enum(variants, _) => {
432 let mut parts = vec![SExpr::atom("enum")];
433 parts.extend(variants.iter().map(ToSExpr::to_sexpr));
434 SExpr::List(parts)
435 }
436 TypeValue::Struct(fields, _) => {
437 let mut parts = vec![SExpr::atom("struct")];
438 parts.extend(fields.to_sexpr_iter());
439 SExpr::List(parts)
440 }
441 }
442 }
443}
444
445impl ToSExpr for Variant {
446 fn to_sexpr(&self) -> SExpr {
447 let Variant {
448 name,
449 fields,
450 pos: _,
451 } = self;
452 let mut parts = vec![name.to_sexpr()];
453 parts.extend(fields.to_sexpr_iter());
454 SExpr::List(parts)
455 }
456}
457
458impl Fields {
459 fn to_sexpr_iter(&self) -> Vec<SExpr> {
460 match self {
461 Fields::Unit => Vec::new(),
462 Fields::Struct(f) => f.to_sexpr_iter(),
463 Fields::Tuple(f) => f.to_sexpr_iter(),
464 }
465 }
466}
467
468impl StructFields {
469 fn to_sexpr_iter(&self) -> Vec<SExpr> {
470 self.fields.iter().map(ToSExpr::to_sexpr).collect()
471 }
472}
473
474impl ToSExpr for StructField {
475 fn to_sexpr(&self) -> SExpr {
476 let StructField { name, ty, pos: _ } = self;
477 SExpr::List(vec![name.to_sexpr(), ty.to_sexpr()])
478 }
479}
480
481impl TupleFields {
482 fn to_sexpr_iter(&self) -> Vec<SExpr> {
483 self.fields.iter().map(ToSExpr::to_sexpr).collect()
484 }
485}
486
487impl ToSExpr for TupleField {
488 fn to_sexpr(&self) -> SExpr {
489 self.ty.to_sexpr()
490 }
491}
492
493impl ToSExpr for ModelValue {
494 fn to_sexpr(&self) -> SExpr {
495 match self {
496 ModelValue::TypeValue(mt) => SExpr::List(vec![SExpr::atom("type"), mt.to_sexpr()]),
497 ModelValue::ConstValue(e) => SExpr::List(vec![SExpr::atom("const"), e.to_sexpr()]),
498 }
499 }
500}
501
502impl ToSExpr for ModelType {
503 fn to_sexpr(&self) -> SExpr {
504 match self {
505 ModelType::Unit => SExpr::atom("Unit"),
506 ModelType::Int => SExpr::atom("Int"),
507 ModelType::Bool => SExpr::atom("Bool"),
508 ModelType::BitVec(Some(size)) => {
509 SExpr::List(vec![SExpr::atom("bv"), SExpr::atom(size)])
510 }
511 ModelType::BitVec(None) => SExpr::List(vec![SExpr::atom("bv")]),
512 ModelType::Struct(fields) => {
513 let mut parts = vec![SExpr::atom("struct")];
514 parts.extend(fields.iter().map(ToSExpr::to_sexpr));
515 SExpr::List(parts)
516 }
517 ModelType::Named(id) => SExpr::List(vec![SExpr::atom("named"), id.to_sexpr()]),
518 ModelType::Unspecified => SExpr::atom("!"),
519 ModelType::Auto => SExpr::atom("_"),
520 }
521 }
522}
523
524impl ToSExpr for Signature {
525 fn to_sexpr(&self) -> SExpr {
526 let Signature { args, ret, pos: _ } = self;
527 SExpr::List(vec![
528 SExpr::tagged("args", args),
529 SExpr::tagged("ret", std::slice::from_ref(ret)),
530 ])
531 }
532}
533
534impl ToSExpr for SpecExpr {
535 fn to_sexpr(&self) -> SExpr {
536 match self {
537 SpecExpr::ConstInt { val, pos: _ } => SExpr::atom(val),
538 SpecExpr::ConstBitVec { val, width, pos: _ } => SExpr::atom(if *width % 4 == 0 {
539 format!("#x{val:0width$x}", width = *width / 4)
540 } else {
541 format!("#b{val:0width$b}", width = *width)
542 }),
543 SpecExpr::ConstBool { val, pos: _ } => SExpr::atom(if *val { "true" } else { "false" }),
544 SpecExpr::Var { var, pos: _ } => var.to_sexpr(),
545 SpecExpr::Op { op, args, pos: _ } => {
546 let mut parts = vec![op.to_sexpr()];
547 parts.extend(args.iter().map(ToSExpr::to_sexpr));
548 SExpr::List(parts)
549 }
550 SpecExpr::As { x, ty, pos: _ } => {
551 SExpr::List(vec![SExpr::atom("as"), x.to_sexpr(), ty.to_sexpr()])
552 }
553 SpecExpr::Field { field, x, pos: _ } => {
554 SExpr::List(vec![SExpr::atom(format!(":{}", field.0)), x.to_sexpr()])
555 }
556 SpecExpr::Discriminator { variant, x, pos: _ } => {
557 SExpr::List(vec![SExpr::atom(format!("{}?", variant.0)), x.to_sexpr()])
558 }
559 SpecExpr::Match { x, arms, pos: _ } => {
560 let mut parts = vec![SExpr::atom("match"), x.to_sexpr()];
561 parts.extend(arms.iter().map(ToSExpr::to_sexpr));
562 SExpr::List(parts)
563 }
564 SpecExpr::Let { defs, body, pos: _ } => {
565 let defs = defs
566 .iter()
567 .map(|(name, expr)| SExpr::List(vec![name.to_sexpr(), expr.to_sexpr()]))
568 .collect::<Vec<_>>();
569
570 SExpr::List(vec![SExpr::atom("let"), SExpr::List(defs), body.to_sexpr()])
571 }
572 SpecExpr::With {
573 decls,
574 body,
575 pos: _,
576 } => {
577 let decls = decls.iter().map(ToSExpr::to_sexpr).collect::<Vec<_>>();
578 SExpr::List(vec![
579 SExpr::atom("with"),
580 SExpr::List(decls),
581 body.to_sexpr(),
582 ])
583 }
584 SpecExpr::Macro {
585 params,
586 body,
587 pos: _,
588 } => {
589 let params = params.iter().map(ToSExpr::to_sexpr).collect::<Vec<_>>();
590 SExpr::List(vec![
591 SExpr::atom("macro"),
592 SExpr::List(params),
593 body.to_sexpr(),
594 ])
595 }
596 SpecExpr::Expand { name, args, pos: _ } => {
597 let mut parts = vec![SExpr::atom(format!("{}!", name.0))];
598 parts.extend(args.iter().map(ToSExpr::to_sexpr));
599 SExpr::List(parts)
600 }
601 SpecExpr::Pair { l, r, pos: _ } => SExpr::List(vec![l.to_sexpr(), r.to_sexpr()]),
602 SpecExpr::Enum {
603 name,
604 variant,
605 args,
606 pos: _,
607 } => {
608 let mut parts = vec![SExpr::atom(format!("{}.{}", name.0, variant.0))];
609 parts.extend(args.iter().map(ToSExpr::to_sexpr));
610 SExpr::List(parts)
611 }
612 SpecExpr::Struct { fields, pos: _ } => {
613 let mut parts = vec![SExpr::atom("struct")];
614 parts.extend(fields.iter().map(ToSExpr::to_sexpr));
615 SExpr::List(parts)
616 }
617 }
618 }
619}
620
621impl ToSExpr for SpecOp {
622 fn to_sexpr(&self) -> SExpr {
623 SExpr::atom(match self {
624 SpecOp::Eq => "=",
625 SpecOp::And => "and",
626 SpecOp::Not => "not",
627 SpecOp::Imp => "=>",
628 SpecOp::Or => "or",
629 SpecOp::Add => "+",
630 SpecOp::Sub => "-",
631 SpecOp::Mul => "*",
632 SpecOp::Lte => "<=",
633 SpecOp::Lt => "<",
634 SpecOp::Gte => ">=",
635 SpecOp::Gt => ">",
636 SpecOp::BVNot => "bvnot",
637 SpecOp::BVAnd => "bvand",
638 SpecOp::BVOr => "bvor",
639 SpecOp::BVXor => "bvxor",
640 SpecOp::BVNeg => "bvneg",
641 SpecOp::BVAdd => "bvadd",
642 SpecOp::BVSub => "bvsub",
643 SpecOp::BVMul => "bvmul",
644 SpecOp::BVUdiv => "bvudiv",
645 SpecOp::BVUrem => "bvurem",
646 SpecOp::BVSdiv => "bvsdiv",
647 SpecOp::BVSrem => "bvsrem",
648 SpecOp::BVShl => "bvshl",
649 SpecOp::BVLshr => "bvlshr",
650 SpecOp::BVAshr => "bvashr",
651 SpecOp::BVSaddo => "bvsaddo",
652 SpecOp::BVUle => "bvule",
653 SpecOp::BVUlt => "bvult",
654 SpecOp::BVUgt => "bvugt",
655 SpecOp::BVUge => "bvuge",
656 SpecOp::BVSlt => "bvslt",
657 SpecOp::BVSle => "bvsle",
658 SpecOp::BVSgt => "bvsgt",
659 SpecOp::BVSge => "bvsge",
660 SpecOp::Rotr => "rotr",
661 SpecOp::Rotl => "rotl",
662 SpecOp::Extract => "extract",
663 SpecOp::ZeroExt => "zero_ext",
664 SpecOp::SignExt => "sign_ext",
665 SpecOp::Concat => "concat",
666 SpecOp::Replicate => "replicate",
667 SpecOp::ConvTo => "conv_to",
668 SpecOp::Int2BV => "int2bv",
669 SpecOp::BV2Nat => "bv2nat",
670 SpecOp::ToFP => "to_fp",
671 SpecOp::FPToUBV => "fp.to_ubv",
672 SpecOp::FPToSBV => "fp.to_sbv",
673 SpecOp::ToFPUnsigned => "to_fp_unsigned",
674 SpecOp::ToFPFromFP => "to_fp_from_fp",
675 SpecOp::WidthOf => "widthof",
676 SpecOp::If => "if",
677 SpecOp::Switch => "switch",
678 SpecOp::Popcnt => "popcnt",
679 SpecOp::Rev => "rev",
680 SpecOp::Cls => "cls",
681 SpecOp::Clz => "clz",
682 SpecOp::FPPositiveInfinity => "fp.+oo",
683 SpecOp::FPNegativeInfinity => "fp.-oo",
684 SpecOp::FPPositiveZero => "fp.+zero",
685 SpecOp::FPNegativeZero => "fp.-zero",
686 SpecOp::FPNaN => "fp.NaN",
687 SpecOp::FPEq => "fp.eq",
688 SpecOp::FPNe => "fp.ne",
689 SpecOp::FPLt => "fp.lt",
690 SpecOp::FPGt => "fp.gt",
691 SpecOp::FPLe => "fp.le",
692 SpecOp::FPGe => "fp.ge",
693 SpecOp::FPAdd => "fp.add",
694 SpecOp::FPSub => "fp.sub",
695 SpecOp::FPMul => "fp.mul",
696 SpecOp::FPDiv => "fp.div",
697 SpecOp::FPMin => "fp.min",
698 SpecOp::FPMax => "fp.max",
699 SpecOp::FPNeg => "fp.neg",
700 SpecOp::FPCeil => "fp.ceil",
701 SpecOp::FPFloor => "fp.floor",
702 SpecOp::FPSqrt => "fp.sqrt",
703 SpecOp::FPTrunc => "fp.trunc",
704 SpecOp::FPNearest => "fp.nearest",
705 SpecOp::FPIsZero => "fp.isZero",
706 SpecOp::FPIsInfinite => "fp.isInfinite",
707 SpecOp::FPIsNaN => "fp.isNaN",
708 SpecOp::FPIsNegative => "fp.isNegative",
709 SpecOp::FPIsPositive => "fp.isPositive",
710 })
711 }
712}
713
714impl ToSExpr for Pattern {
715 fn to_sexpr(&self) -> SExpr {
716 match self {
717 Pattern::Var {
718 var: Ident(var, _),
719 pos: _,
720 } => SExpr::atom(var.clone()),
721 Pattern::BindPattern {
722 var: Ident(var, _),
723 subpat,
724 pos: _,
725 } => SExpr::Binding(var.clone(), Box::new(subpat.to_sexpr())),
726 Pattern::ConstInt { val, pos: _ } => SExpr::atom(val),
727 Pattern::ConstBool { val, pos: _ } => SExpr::atom(if *val { "true" } else { "false" }),
728 Pattern::ConstPrim { val, pos: _ } => SExpr::atom(format!("${}", val.0)),
729 Pattern::Wildcard { pos: _ } => SExpr::atom("_"),
730 Pattern::Term { sym, args, pos: _ } => {
731 let mut parts = vec![sym.to_sexpr()];
732 parts.extend(args.iter().map(ToSExpr::to_sexpr));
733 SExpr::List(parts)
734 }
735 Pattern::And { subpats, pos: _ } => {
736 let mut parts = vec![SExpr::atom("and")];
737 parts.extend(subpats.iter().map(ToSExpr::to_sexpr));
738 SExpr::List(parts)
739 }
740 Pattern::MacroArg { .. } => unimplemented!("macro arguments are for internal use only"),
741 }
742 }
743}
744
745impl ToSExpr for IfLet {
746 fn to_sexpr(&self) -> SExpr {
747 let IfLet {
748 pattern,
749 expr,
750 pos: _,
751 } = self;
752 SExpr::List(vec![
753 SExpr::atom("if-let"),
754 pattern.to_sexpr(),
755 expr.to_sexpr(),
756 ])
757 }
758}
759
760impl ToSExpr for Expr {
761 fn to_sexpr(&self) -> SExpr {
762 match self {
763 Expr::Term { sym, args, pos: _ } => {
764 let mut parts = vec![sym.to_sexpr()];
765 parts.extend(args.iter().map(ToSExpr::to_sexpr));
766 SExpr::List(parts)
767 }
768 Expr::Var { name, pos: _ } => name.to_sexpr(),
769 Expr::ConstInt { val, pos: _ } => SExpr::atom(val),
770 Expr::ConstBool { val, pos: _ } => SExpr::atom(if *val { "true" } else { "false" }),
771 Expr::ConstPrim { val, pos: _ } => SExpr::atom(format!("${}", val.0)),
772 Expr::Let { defs, body, pos: _ } => {
773 let mut parts = vec![SExpr::atom("let")];
774 parts.push(SExpr::list(&defs));
775 parts.push(body.to_sexpr());
776 SExpr::List(parts)
777 }
778 }
779 }
780}
781
782impl ToSExpr for LetDef {
783 fn to_sexpr(&self) -> SExpr {
784 let LetDef {
785 var,
786 ty,
787 val,
788 pos: _,
789 } = self;
790 SExpr::List(vec![var.to_sexpr(), ty.to_sexpr(), val.to_sexpr()])
791 }
792}
793
794impl ToSExpr for Ident {
795 fn to_sexpr(&self) -> SExpr {
796 let Ident(name, _) = self;
797 SExpr::atom(name.clone())
798 }
799}
800
801impl ToSExpr for AttrKind {
802 fn to_sexpr(&self) -> SExpr {
803 match self {
804 AttrKind::Chain => SExpr::List(vec![SExpr::atom("veri"), SExpr::atom("chain")]),
805 AttrKind::Priority => SExpr::List(vec![SExpr::atom("veri"), SExpr::atom("priority")]),
806 AttrKind::Tag(tag) => SExpr::List(vec![SExpr::atom("tag"), tag.to_sexpr()]),
807 }
808 }
809}
810
811impl ToSExpr for Attr {
812 fn to_sexpr(&self) -> SExpr {
813 let mut parts = vec![SExpr::atom("attr")];
814 match &self.target {
815 AttrTarget::Rule(name) => {
816 parts.push(SExpr::atom("rule"));
817 parts.push(name.to_sexpr());
818 }
819 AttrTarget::Term(name) => {
820 parts.push(name.to_sexpr());
821 }
822 }
823 parts.extend(self.kinds.iter().map(ToSExpr::to_sexpr));
824 SExpr::List(parts)
825 }
826}
827
828impl ToSExpr for SpecMacro {
829 fn to_sexpr(&self) -> SExpr {
830 let mut sig = vec![self.name.to_sexpr()];
831 sig.extend(self.params.iter().map(ToSExpr::to_sexpr));
832
833 SExpr::List(vec![
834 SExpr::atom("macro"),
835 SExpr::List(sig),
836 self.body.to_sexpr(),
837 ])
838 }
839}
840
841impl ToSExpr for State {
842 fn to_sexpr(&self) -> SExpr {
843 SExpr::List(vec![
844 SExpr::atom("state"),
845 self.name.to_sexpr(),
846 SExpr::List(vec![SExpr::atom("type"), self.ty.to_sexpr()]),
847 SExpr::List(vec![SExpr::atom("default"), self.default.to_sexpr()]),
848 ])
849 }
850}
851
852impl ToSExpr for ModelField {
853 fn to_sexpr(&self) -> SExpr {
854 SExpr::List(vec![self.name.to_sexpr(), self.ty.to_sexpr()])
855 }
856}
857
858impl ToSExpr for FieldInit {
859 fn to_sexpr(&self) -> SExpr {
860 SExpr::List(vec![self.name.to_sexpr(), self.value.to_sexpr()])
861 }
862}
863
864impl ToSExpr for Arm {
865 fn to_sexpr(&self) -> SExpr {
866 let mut head = vec![self.variant.to_sexpr()];
867 head.extend(self.args.iter().map(ToSExpr::to_sexpr));
868
869 SExpr::List(vec![SExpr::List(head), self.body.to_sexpr()])
870 }
871}