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

liquid_fixpoint/
format.rs
