liquid_fixpoint/
format.rs

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

liquid_fixpoint/
format.rs
