liquid_fixpoint/
format.rs

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

liquid_fixpoint/
format.rs
