Skip to main content

cranelift_isle/
printer.rs

1//! Printer for ISLE language.
2
3use std::{io::Write, vec};
4
5use crate::ast::*;
6
7/// Print ISLE definitions.
8pub 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
19/// Dump a single ISLE node to standard output.
20pub fn dump<N: ToSExpr>(node: &N) -> std::io::Result<()> {
21    print_node(node, 120, &mut std::io::stdout())
22}
23
24/// Print a single ISLE node.
25pub 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/// S-expression representation of ISLE source code prior to printing.
36#[derive(Debug, Clone, PartialEq, Eq)]
37pub enum SExpr {
38    /// Atom is a plain string to be printed.
39    Atom(String),
40    /// A binding for an ISLE structure, e.g. `x @ (...)`.
41    Binding(String, Box<SExpr>),
42    /// A parenthesized list of S-expressions, e.g. `(x y z)`.
43    List(Vec<SExpr>),
44}
45
46/// Trait for converting ISLE definitions to S-expressions.
47pub trait ToSExpr {
48    /// Convert the given value to an S-expression.
49    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    // Would the expressions fit in the current line?
132    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 // " @ "
143                }
144                SExpr::List(items) => {
145                    stack.extend(items.iter().rev());
146                    2 + items.len() - 1 // "(" + ")" + spaces
147                }
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}