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,
12};
13
14pub(crate) fn fmt_constraint<T: Types>(
15    cstr: &Constraint<T>,
16    f: &mut fmt::Formatter<'_>,
17) -> fmt::Result {
18    let mut cx = ConstraintFormatter::default();
19    write!(f, "(constraint")?;
20    cx.incr();
21    cx.newline(f)?;
22    cx.fmt_constraint(f, cstr)?;
23    cx.decr();
24    writeln!(f, ")")
25}
26
27impl<T: Types> fmt::Display for Constraint<T> {
28    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
29        fmt_constraint(self, f)
30    }
31}
32
33impl<T: Types> fmt::Display for Task<T> {
34    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
35        if self.scrape_quals {
36            writeln!(f, "(fixpoint \"--scrape=both\")")?;
37        }
38        for line in &self.comments {
39            writeln!(f, ";; {line}")?;
40        }
41        writeln!(f)?;
42
43        for data_decl in &self.data_decls {
44            writeln!(f, "{data_decl}")?;
45        }
46
47        for qualif in &self.qualifiers {
48            writeln!(f, "{qualif}")?;
49        }
50
51        for cinfo in &self.constants {
52            writeln!(f, "{cinfo}")?;
53        }
54
55        for fun_decl in &self.define_funs {
56            writeln!(f, "{fun_decl}")?;
57        }
58
59        for kvar in &self.kvars {
60            writeln!(f, "{kvar}")?;
61        }
62
63        writeln!(f)?;
64        fmt_constraint(&self.constraint, f)
65    }
66}
67
68impl<T: Types> fmt::Display for KVarDecl<T> {
69    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
70        write!(
71            f,
72            "(var ${} ({})) ;; {}",
73            self.kvid.display(),
74            self.sorts.iter().format(" "),
75            self.comment
76        )
77    }
78}
79
80impl<T: Types> fmt::Display for ConstDecl<T> {
81    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
82        write!(f, "(constant {} {})", self.name.display(), self.sort)?;
83        if let Some(comment) = &self.comment {
84            write!(f, "  ;; {comment}")?;
85        }
86        Ok(())
87    }
88}
89
90impl<T: Types> fmt::Debug for Task<T> {
91    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
92        fmt::Display::fmt(self, f)
93    }
94}
95
96#[derive(Default)]
97struct ConstraintFormatter {
98    level: u32,
99}
100
101impl ConstraintFormatter {
102    fn fmt_constraint<T: Types>(
103        &mut self,
104        f: &mut fmt::Formatter<'_>,
105        cstr: &Constraint<T>,
106    ) -> fmt::Result {
107        match cstr {
108            Constraint::Pred(pred, tag) => self.fmt_pred_in_head_position(pred, tag.as_ref(), f),
109            Constraint::Conj(cstrs) => {
110                match &cstrs[..] {
111                    [] => write!(f, "((true))"),
112                    [cstr] => self.fmt_constraint(f, cstr),
113                    cstrs => {
114                        write!(f, "(and")?;
115                        for cstr in cstrs {
116                            self.incr();
117                            self.newline(f)?;
118                            self.fmt_constraint(f, cstr)?;
119                            self.decr();
120                        }
121                        f.write_char(')')
122                    }
123                }
124            }
125            Constraint::ForAll(bind, head) => {
126                write!(f, "(forall (({} {}) {})", bind.name.display(), bind.sort, bind.pred)?;
127
128                self.incr();
129                self.newline(f)?;
130                self.fmt_constraint(f, head)?;
131                self.decr();
132
133                f.write_str(")")
134            }
135        }
136    }
137
138    fn fmt_pred_in_head_position<T: Types>(
139        &mut self,
140        pred: &Pred<T>,
141        tag: Option<&T::Tag>,
142        f: &mut fmt::Formatter<'_>,
143    ) -> fmt::Result {
144        match pred {
145            Pred::And(preds) => {
146                match &preds[..] {
147                    [] => write!(f, "((true))"),
148                    [pred] => self.fmt_pred_in_head_position(pred, tag, f),
149                    _ => {
150                        write!(f, "(and")?;
151                        for pred in preds {
152                            self.incr();
153                            self.newline(f)?;
154                            self.fmt_pred_in_head_position(pred, tag, f)?;
155                            self.decr();
156                        }
157                        write!(f, ")")
158                    }
159                }
160            }
161            Pred::Expr(_) | Pred::KVar(..) => {
162                if let Some(tag) = tag {
163                    write!(f, "(tag {pred} \"{tag}\")")
164                } else {
165                    write!(f, "{pred}")
166                }
167            }
168        }
169    }
170
171    fn incr(&mut self) {
172        self.level += 1;
173    }
174
175    fn decr(&mut self) {
176        self.level -= 1;
177    }
178
179    fn newline(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
180        f.write_char('\n')?;
181        self.padding(f)
182    }
183
184    fn padding(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
185        for _ in 0..self.level {
186            f.write_str(" ")?;
187        }
188        Ok(())
189    }
190}
191
192impl<T: Types> fmt::Display for DataDecl<T> {
193    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
194        write!(
195            f,
196            "(datatype ({} {}) ({}))",
197            self.name.display(),
198            self.vars,
199            self.ctors.iter().format(" ")
200        )
201    }
202}
203
204impl<T: Types> fmt::Display for DataCtor<T> {
205    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
206        write!(f, "({} ({}))", self.name.display(), self.fields.iter().format(" "))
207    }
208}
209
210impl<T: Types> fmt::Display for DataField<T> {
211    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
212        write!(f, "({} {})", self.name.display(), self.sort)
213    }
214}
215
216impl<T: Types> fmt::Display for SortCtor<T> {
217    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
218        match self {
219            SortCtor::Set => write!(f, "Set_Set"),
220            SortCtor::Map => write!(f, "Map_t"),
221            SortCtor::Data(name) => write!(f, "{}", name.display()),
222        }
223    }
224}
225
226impl<T: Types> fmt::Display for Sort<T> {
227    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
228        match self {
229            Sort::Int => write!(f, "int"),
230            Sort::Bool => write!(f, "bool"),
231            Sort::Real => write!(f, "real"),
232            Sort::Str => write!(f, "Str"),
233            Sort::Var(i) => write!(f, "@({i})"),
234            Sort::BitVec(size) => write!(f, "(BitVec {size})"),
235            Sort::BvSize(size) => write!(f, "Size{size}"),
236            Sort::Abs(..) => {
237                let (params, sort) = self.peel_out_abs();
238                fmt_func(params, sort, f)
239            }
240            Sort::Func(..) => fmt_func(0, self, f),
241            Sort::App(ctor, args) => {
242                write!(f, "({ctor}")?;
243                for arg in args {
244                    write!(f, " {arg}")?;
245                }
246                write!(f, ")")
247            }
248        }
249    }
250}
251
252fn fmt_func<T: Types>(params: usize, sort: &Sort<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
253    write!(f, "(func {params} (")?;
254    let mut curr = sort;
255    while let Sort::Func(input_and_output) = curr {
256        let [input, output] = &**input_and_output;
257        write!(f, "{input} ")?;
258        curr = output;
259    }
260    write!(f, ") {curr})")
261}
262
263impl<T: Types> fmt::Display for Pred<T> {
264    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
265        match self {
266            Pred::And(preds) => {
267                match &preds[..] {
268                    [] => write!(f, "((true))"),
269                    [pred] => write!(f, "{pred}"),
270                    preds => write!(f, "(and {})", preds.iter().join(" ")),
271                }
272            }
273            Pred::KVar(kvid, args) => {
274                write!(f, "(${} {})", kvid.display(), args.iter().join(" "),)
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, _sort_args, args, _out_sort) => {
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            Expr::ThyFunc(thy_func) => write!(f, "{}", thy_func),
328            Expr::IsCtor(ctor, e) => {
329                write!(f, "(is${} {})", ctor.display(), e)
330            }
331            Expr::Exists(sorts, body) => {
332                write!(
333                    f,
334                    "(exists ({}) {})",
335                    sorts.iter().map(|binder| &binder.1).format(" "),
336                    body
337                )
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        if let Some(body) = &self.body {
378            write!(
379                f,
380                "(define_fun {} ({}) {} ({}))",
381                self.name.display(),
382                iter::zip(&body.args, &self.sort.inputs).format_with(" ", |(name, sort), f| {
383                    f(&format_args!("({} {sort})", name.display()))
384                }),
385                self.sort.output,
386                body.expr
387            )?;
388        } else {
389            write!(f, "(constant {} {})", self.name.display(), self.sort)?;
390        }
391        if let Some(comment) = &self.comment {
392            write!(f, "  ;; {comment}")?;
393        }
394        Ok(())
395    }
396}
397
398impl<T: Types> fmt::Display for FunSort<T> {
399    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
400        write!(f, "(func {} ({}) {})", self.params, self.inputs.iter().format(" "), self.output)
401    }
402}
403
404impl fmt::Display for BinOp {
405    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
406        match self {
407            BinOp::Add => write!(f, "+"),
408            BinOp::Sub => write!(f, "-"),
409            BinOp::Mul => write!(f, "*"),
410            BinOp::Div => write!(f, "/"),
411            BinOp::Mod => write!(f, "mod"),
412        }
413    }
414}
415
416impl fmt::Display for BinRel {
417    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
418        match self {
419            BinRel::Eq => write!(f, "="),
420            BinRel::Ne => write!(f, "!="),
421            BinRel::Gt => write!(f, ">"),
422            BinRel::Ge => write!(f, ">="),
423            BinRel::Lt => write!(f, "<"),
424            BinRel::Le => write!(f, "<="),
425        }
426    }
427}
428
429impl fmt::Debug for BinOp {
430    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
431        fmt::Display::fmt(self, f)
432    }
433}
liquid_fixpoint/format.rs

liquid_fixpoint/
format.rs
