fn fmt()

in smt2parser/src/concrete.rs [1189:1268]


    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        use Term::*;
        match self {
            Constant(c) => {
                // ⟨spec_constant⟩
                write!(f, "{}", c)
            }
            QualIdentifier(id) => {
                // ⟨qual_identifier⟩
                write!(f, "{}", id)
            }
            Application {
                qual_identifier,
                arguments,
            } => {
                // ( ⟨qual_identifier ⟩ ⟨term⟩+ )
                write!(f, "({} {})", qual_identifier, arguments.iter().format(" "))
            }
            Let { var_bindings, term } => {
                // ( let ( ⟨var_binding⟩+ ) ⟨term⟩ )
                write!(
                    f,
                    "(let ({}) {})",
                    var_bindings
                        .iter()
                        .format_with(" ", |(v, t), f| f(&format_args!("({} {})", v, t))),
                    term
                )
            }
            Forall { vars, term } => {
                // ( forall ( ⟨sorted_var⟩+ ) ⟨term⟩ )
                write!(
                    f,
                    "(forall ({}) {})",
                    vars.iter()
                        .format_with(" ", |(v, s), f| f(&format_args!("({} {})", v, s))),
                    term
                )
            }
            Exists { vars, term } => {
                // ( exists ( ⟨sorted_var⟩+ ) ⟨term⟩ )
                write!(
                    f,
                    "(exists ({}) {})",
                    vars.iter()
                        .format_with(" ", |(v, s), f| f(&format_args!("({} {})", v, s))),
                    term
                )
            }
            Match { term, cases } => {
                // ( match ⟨term⟩ ( ⟨match_case⟩+ ) )
                write!(
                    f,
                    "(match {} ({}))",
                    term,
                    cases.iter().format_with(" ", |(pattern, term), f| {
                        if pattern.len() == 1 {
                            f(&format_args!("({} {})", &pattern[0], term))
                        } else {
                            f(&format_args!("(({}) {})", pattern.iter().format(" "), term))
                        }
                    })
                )
            }
            Attributes { term, attributes } => {
                // ( ! ⟨term⟩ ⟨attribute⟩+ )
                write!(
                    f,
                    "(! {} {})",
                    term,
                    attributes
                        .iter()
                        .format_with(" ", |(key, value), f| match value {
                            AttributeValue::None => f(key),
                            _ => f(&format_args!("{} {}", key, value)),
                        })
                )
            }
        }
    }