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

liquid_fixpoint/
format.rs
