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

liquid_fixpoint/
format.rs
