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

liquid_fixpoint/
format.rs
