liquid_fixpoint/
format.rs

1use std::{
2    fmt::{self, Write},
3    iter,
4};
5
6use itertools::Itertools;
7
8use crate::{
9    BinOp, BinRel, ConstDecl, Constant, Constraint, DataCtor, DataDecl, DataField, Expr,
10    FixpointFmt, FunDef, FunSort, Identifier, KVarDecl, Pred, Qualifier, Sort, SortCtor, Task,
11    Types, constraint::Quantifier,
12};
13
14pub(crate) fn fmt_constraint<T: Types>(
15    cstr: &Constraint<T>,
16    f: &mut fmt::Formatter<'_>,
17    pretty: bool,
18) -> fmt::Result {
19    let mut cx = ConstraintFormatter::new(pretty);
20    write!(f, "(constraint")?;
21    cx.incr();
22    cx.newline(f)?;
23    cx.fmt_constraint(f, cstr)?;
24    cx.decr();
25    if pretty { writeln!(f, ")") } else { write!(f, ")") }
26}
27
28impl<T: Types> fmt::Display for Constraint<T> {
29    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
30        fmt_constraint(self, f, true)
31    }
32}
33
34pub(crate) fn fmt_task<T: Types>(
35    task: &Task<T>,
36    f: &mut fmt::Formatter<'_>,
37    pretty: bool,
38) -> fmt::Result {
39    if task.scrape_quals {
40        writeln!(f, "(fixpoint \"--scrape=both\")")?;
41    }
42    if pretty {
43        for line in &task.comments {
44            writeln!(f, ";; {line}")?;
45        }
46        writeln!(f)?;
47    }
48
49    for data_decl in &task.data_decls {
50        writeln!(f, "{data_decl}")?;
51    }
52
53    for qualif in &task.qualifiers {
54        writeln!(f, "{qualif}")?;
55    }
56
57    for cinfo in &task.constants {
58        writeln!(f, "{cinfo}")?;
59    }
60
61    for fun_decl in &task.define_funs {
62        writeln!(f, "{fun_decl}")?;
63    }
64
65    for kvar in &task.kvars {
66        writeln!(f, "{kvar}")?;
67    }
68
69    if pretty {
70        writeln!(f)?;
71    }
72    fmt_constraint(&task.constraint, f, pretty)
73}
74
75impl<T: Types> fmt::Display for Task<T> {
76    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
77        fmt_task(self, f, true)
78    }
79}
80
81pub(crate) struct CompactTask<'a, T: Types>(pub &'a Task<T>);
82
83impl<T: Types> fmt::Display for CompactTask<'_, T> {
84    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
85        fmt_task(self.0, f, false)
86    }
87}
88
89impl<T: Types> fmt::Display for KVarDecl<T> {
90    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
91        write!(
92            f,
93            "(var ${} ({})) ;; {}",
94            self.kvid.display(),
95            self.sorts.iter().format(" "),
96            self.comment
97        )
98    }
99}
100
101impl<T: Types> fmt::Display for ConstDecl<T> {
102    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
103        write!(f, "(constant {} {})", self.name.display(), self.sort)?;
104        if let Some(comment) = &self.comment {
105            write!(f, "  ;; {comment}")?;
106        }
107        Ok(())
108    }
109}
110
111impl<T: Types> fmt::Debug for Task<T> {
112    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
113        fmt::Display::fmt(self, f)
114    }
115}
116
117struct ConstraintFormatter {
118    level: u32,
119    pretty: bool,
120}
121
122impl ConstraintFormatter {
123    fn new(pretty: bool) -> Self {
124        Self { level: 0, pretty }
125    }
126    fn fmt_constraint<T: Types>(
127        &mut self,
128        f: &mut fmt::Formatter<'_>,
129        cstr: &Constraint<T>,
130    ) -> fmt::Result {
131        match cstr {
132            Constraint::Pred(pred, tag) => self.fmt_pred_in_head_position(pred, tag.as_ref(), f),
133            Constraint::Conj(cstrs) => {
134                match &cstrs[..] {
135                    [] => write!(f, "((true))"),
136                    [cstr] => self.fmt_constraint(f, cstr),
137                    cstrs => {
138                        write!(f, "(and")?;
139                        for cstr in cstrs {
140                            self.incr();
141                            self.newline(f)?;
142                            self.fmt_constraint(f, cstr)?;
143                            self.decr();
144                        }
145                        f.write_char(')')
146                    }
147                }
148            }
149            Constraint::ForAll(bind, head) => {
150                write!(f, "(forall (({} {}) {})", bind.name.display(), bind.sort, bind.pred)?;
151
152                self.incr();
153                self.newline(f)?;
154                self.fmt_constraint(f, head)?;
155                self.decr();
156
157                f.write_str(")")
158            }
159        }
160    }
161
162    fn fmt_pred_in_head_position<T: Types>(
163        &mut self,
164        pred: &Pred<T>,
165        tag: Option<&T::Tag>,
166        f: &mut fmt::Formatter<'_>,
167    ) -> fmt::Result {
168        match pred {
169            Pred::And(preds) => {
170                match &preds[..] {
171                    [] => write!(f, "((true))"),
172                    [pred] => self.fmt_pred_in_head_position(pred, tag, f),
173                    _ => {
174                        write!(f, "(and")?;
175                        for pred in preds {
176                            self.incr();
177                            self.newline(f)?;
178                            self.fmt_pred_in_head_position(pred, tag, f)?;
179                            self.decr();
180                        }
181                        write!(f, ")")
182                    }
183                }
184            }
185            Pred::Expr(_) | Pred::KVar(..) => {
186                if let Some(tag) = tag {
187                    write!(f, "(tag {pred} \"{tag}\")")
188                } else {
189                    write!(f, "{pred}")
190                }
191            }
192        }
193    }
194
195    fn incr(&mut self) {
196        self.level += 1;
197    }
198
199    fn decr(&mut self) {
200        self.level -= 1;
201    }
202
203    fn newline(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
204        if self.pretty {
205            f.write_char('\n')?;
206            self.padding(f)
207        } else {
208            f.write_char(' ')
209        }
210    }
211
212    fn padding(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
213        if self.pretty {
214            for _ in 0..self.level {
215                f.write_str(" ")?;
216            }
217        }
218        Ok(())
219    }
220}
221
222impl<T: Types> fmt::Display for DataDecl<T> {
223    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
224        write!(
225            f,
226            "(datatype ({} {}) ({}))",
227            self.name.display(),
228            self.vars,
229            self.ctors.iter().format(" ")
230        )
231    }
232}
233
234impl<T: Types> fmt::Display for DataCtor<T> {
235    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
236        write!(f, "({} ({}))", self.name.display(), self.fields.iter().format(" "))
237    }
238}
239
240impl<T: Types> fmt::Display for DataField<T> {
241    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
242        write!(f, "({} {})", self.name.display(), self.sort)
243    }
244}
245
246impl<T: Types> fmt::Display for SortCtor<T> {
247    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
248        match self {
249            SortCtor::Set => write!(f, "Set_Set"),
250            SortCtor::Map => write!(f, "Map_t"),
251            SortCtor::Data(name) => write!(f, "{}", name.display()),
252        }
253    }
254}
255
256impl<T: Types> fmt::Display for Sort<T> {
257    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
258        match self {
259            Sort::Int => write!(f, "int"),
260            Sort::Bool => write!(f, "bool"),
261            Sort::Real => write!(f, "real"),
262            Sort::Str => write!(f, "Str"),
263            Sort::Var(i) => write!(f, "@({i})"),
264            Sort::BitVec(size) => write!(f, "(BitVec {size})"),
265            Sort::BvSize(size) => write!(f, "Size{size}"),
266            Sort::Abs(..) => {
267                let (params, sort) = self.peel_out_abs();
268                fmt_func(params, sort, f)
269            }
270            Sort::Func(..) => fmt_func(0, self, f),
271            Sort::App(ctor, args) => {
272                write!(f, "({ctor}")?;
273                for arg in args {
274                    write!(f, " {arg}")?;
275                }
276                write!(f, ")")
277            }
278        }
279    }
280}
281
282fn fmt_func<T: Types>(params: usize, sort: &Sort<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
283    write!(f, "(func {params} (")?;
284    let mut curr = sort;
285    while let Sort::Func(input_and_output) = curr {
286        let [input, output] = &**input_and_output;
287        write!(f, "{input} ")?;
288        curr = output;
289    }
290    write!(f, ") {curr})")
291}
292
293impl<T: Types> fmt::Display for Pred<T> {
294    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
295        match self {
296            Pred::And(preds) => {
297                match &preds[..] {
298                    [] => write!(f, "((true))"),
299                    [pred] => write!(f, "{pred}"),
300                    preds => write!(f, "(and {})", preds.iter().join(" ")),
301                }
302            }
303            Pred::KVar(kvid, args) => {
304                write!(f, "(${} {})", kvid.display(), args.iter().join(" "),)
305            }
306            Pred::Expr(expr) => write!(f, "({expr})"),
307        }
308    }
309}
310
311impl fmt::Display for Quantifier {
312    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
313        match self {
314            Quantifier::Exists => write!(f, "exists"),
315            Quantifier::Forall => write!(f, "forall"),
316        }
317    }
318}
319
320impl<T: Types> fmt::Display for Expr<T> {
321    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
322        match self {
323            Expr::Constant(c) => write!(f, "{c}"),
324            Expr::Var(x) => write!(f, "{}", x.display()),
325            Expr::App(func, _sort_args, args, _out_sort) => {
326                write!(f, "({func} {})", args.iter().format(" "))
327            }
328            Expr::Neg(e) => {
329                write!(f, "(- {e})")
330            }
331            Expr::BinaryOp(op, exprs) => {
332                let [e1, e2] = &**exprs;
333                write!(f, "({op} {e1} {e2})")
334            }
335            Expr::IfThenElse(exprs) => {
336                let [p, e1, e2] = &**exprs;
337                write!(f, "(if {p} {e1} {e2})")
338            }
339            Expr::And(exprs) => {
340                write!(f, "(and {})", exprs.iter().format(" "))
341            }
342            Expr::Or(exprs) => {
343                write!(f, "(or {})", exprs.iter().format(" "))
344            }
345            Expr::Not(e) => {
346                write!(f, "(not {e})")
347            }
348            Expr::Imp(exprs) => {
349                let [e1, e2] = &**exprs;
350                write!(f, "(=> {e1} {e2})")
351            }
352            Expr::Iff(exprs) => {
353                let [e1, e2] = &**exprs;
354                write!(f, "(<=> {e1} {e2})")
355            }
356            Expr::Atom(rel, exprs) => {
357                let [e1, e2] = &**exprs;
358                write!(f, "({rel} {e1} {e2})")
359            }
360            Expr::Let(name, exprs) => {
361                // Fixpoint only support one binder per let expressions, but it parses a singleton
362                // list of binders to be forward-compatible
363                let [e1, e2] = &**exprs;
364                write!(f, "(let (({} {e1})) {e2})", name.display())
365            }
366            Expr::ThyFunc(thy_func) => write!(f, "{}", thy_func),
367            Expr::IsCtor(ctor, e) => {
368                write!(f, "(is${} {})", ctor.display(), e)
369            }
370            Expr::Quantifier(q, sorts, body) => {
371                write!(
372                    f,
373                    "({} ({}) {})",
374                    q,
375                    sorts.iter().format_with(" ", |(name, sort), f| {
376                        f(&format_args!("({} {sort})", name.display()))
377                    }),
378                    body
379                )
380            }
381        }
382    }
383}
384
385impl<T: Types> fmt::Display for Constant<T> {
386    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
387        match self {
388            Constant::Numeral(n) => write!(f, "{n}"),
389            Constant::Real(n) => write!(f, "{}", n.display()),
390            Constant::Boolean(b) => write!(f, "{b}"),
391            Constant::String(s) => write!(f, "{}", s.display()),
392            Constant::BitVec(i, sz) => {
393                if sz.is_multiple_of(4) {
394                    write!(f, "(lit \"#x{i:00$x}\" (BitVec Size{sz}))", (sz / 4) as usize)
395                } else {
396                    write!(f, "(lit \"#b{i:00$x}\" (BitVec Size{sz}))", *sz as usize)
397                }
398            }
399        }
400    }
401}
402
403impl<T: Types> fmt::Display for Qualifier<T> {
404    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
405        write!(
406            f,
407            "(qualif {} ({}) ({}))",
408            self.name,
409            self.args.iter().format_with(" ", |(name, sort), f| {
410                f(&format_args!("({} {sort})", name.display()))
411            }),
412            self.body
413        )
414    }
415}
416
417impl<T: Types> fmt::Display for FunDef<T> {
418    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
419        if let Some(body) = &self.body {
420            write!(
421                f,
422                "(define_fun {} ({}) {} ({}))",
423                self.name.display(),
424                iter::zip(&body.args, &self.sort.inputs).format_with(" ", |(name, sort), f| {
425                    f(&format_args!("({} {sort})", name.display()))
426                }),
427                self.sort.output,
428                body.expr
429            )?;
430        } else {
431            write!(f, "(constant {} {})", self.name.display(), self.sort)?;
432        }
433        if let Some(comment) = &self.comment {
434            write!(f, "  ;; {comment}")?;
435        }
436        Ok(())
437    }
438}
439
440impl<T: Types> fmt::Display for FunSort<T> {
441    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
442        write!(f, "(func {} ({}) {})", self.params, self.inputs.iter().format(" "), self.output)
443    }
444}
445
446impl fmt::Display for BinOp {
447    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
448        match self {
449            BinOp::Add => write!(f, "+"),
450            BinOp::Sub => write!(f, "-"),
451            BinOp::Mul => write!(f, "*"),
452            BinOp::Div => write!(f, "/"),
453            BinOp::Mod => write!(f, "mod"),
454        }
455    }
456}
457
458impl fmt::Display for BinRel {
459    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
460        match self {
461            BinRel::Eq => write!(f, "="),
462            BinRel::Ne => write!(f, "!="),
463            BinRel::Gt => write!(f, ">"),
464            BinRel::Ge => write!(f, ">="),
465            BinRel::Lt => write!(f, "<"),
466            BinRel::Le => write!(f, "<="),
467        }
468    }
469}
470
471impl fmt::Debug for BinOp {
472    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
473        fmt::Display::fmt(self, f)
474    }
475}
liquid_fixpoint/format.rs

liquid_fixpoint/
format.rs
