liquid_fixpoint/
format.rs

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

liquid_fixpoint/
format.rs
