use crate::ast::{ Axiom, BinaryOp, BindX, Binder, Binders, Constant, Datatypes, Decl, DeclX, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, Query, QueryX, RoundingMode, Stmt, StmtX, Triggers, Typ, TypX, Typs, UnaryOp, }; use crate::context::{SmtEncoding, SmtSolver}; use crate::def::mk_skolem_id; use crate::util::vec_map; use sise::TreeNode as Node; use std::sync::Arc; pub fn str_to_node(s: &str) -> Node { Node::Atom(s.to_string()) } pub fn macro_push_node(nodes: &mut Vec, node: Node) { // turn a - b into a-b let len = nodes.len(); if len != 0 { if let Node::Atom(cur) = &node { if let Node::Atom(prev) = &nodes[len - 1] { if node == "-" || prev == ":" || (prev != "-" && prev.ends_with("-")) { nodes[len - 1] = Node::Atom(prev.to_owned() + cur); return; } } } } nodes.push(node); } /* examples: node!(my_atom) node!((atom1 atom2 atom-3)) node!((atom1 (10 20 30) atom-3)) let x = node!((10 20 30)); node!((atom1 {x} atom-3)) There's some limited support for atoms containing hyphens, at least for atoms inside a list. */ #[macro_export] macro_rules! node { ( - ) => { Node::Atom("-".to_string()) }; ( { $x:expr } ) => { $x }; ( [ $x:expr ] ) => { $x.clone() }; ( $x:literal ) => { Node::Atom($x.to_string()) }; ( ( $( $x:tt )* ) ) => { { #[allow(unused_mut)] let mut v = Vec::new(); $(macro_push_node(&mut v, node!($x));)* Node::List(v) } }; ( $x:tt ) => { Node::Atom(stringify!($x).to_string()) }; } #[macro_export] macro_rules! nodes { ( $( $x:tt )* ) => { { let mut v = Vec::new(); $(macro_push_node(&mut v, node!($x));)* Node::List(v) } }; } #[macro_export] macro_rules! nodes_vec { ( $( $x:tt )* ) => { { let mut v = Vec::new(); $(macro_push_node(&mut v, node!($x));)* v } }; } pub struct Printer { message_interface: Arc, // print as SMT, not as AIR print_as_smt: bool, smt_encoding: SmtEncoding, } impl Printer { pub fn new( message_interface: Arc, print_as_smt: bool, solver: SmtSolver, ) -> Self { Self::new_with_encoding(message_interface, print_as_smt, solver.default_encoding()) } pub fn new_with_encoding( message_interface: Arc, print_as_smt: bool, smt_encoding: SmtEncoding, ) -> Self { Printer { message_interface, print_as_smt, smt_encoding } } pub(crate) fn typ_to_node(&self, typ: &Typ) -> Node { match &**typ { TypX::Bool => str_to_node("Bool"), TypX::Int => str_to_node("Int"), TypX::Real => str_to_node("Real"), TypX::Fun if self.print_as_smt => str_to_node(crate::def::FUNCTION), TypX::Fun => str_to_node("Fun"), TypX::Named(name) => str_to_node(&name.clone()), TypX::BitVec(size) => Node::List(vec![ str_to_node("_"), str_to_node("BitVec"), str_to_node(&size.to_string()), ]), TypX::Float { exp_bits: 5, sig_bits: 11 } => str_to_node("Float16"), TypX::Float { exp_bits: 8, sig_bits: 24 } => str_to_node("Float32"), TypX::Float { exp_bits: 11, sig_bits: 53 } => str_to_node("Float64"), TypX::Float { exp_bits: 15, sig_bits: 113 } => str_to_node("Float128"), TypX::Float { exp_bits, sig_bits } => Node::List(vec![ str_to_node("_"), str_to_node("FloatingPoint"), str_to_node(&exp_bits.to_string()), str_to_node(&sig_bits.to_string()), ]), } } pub(crate) fn typs_to_node(&self, typs: &Typs) -> Node { Node::List(vec_map(typs, |t| self.typ_to_node(t))) } pub(crate) fn bv_const_expr_to_node(&self, n: &Arc, width: u32) -> Node { let bv_node = str_to_node(&format!("bv{}", n)); let width_node = str_to_node(&width.to_string()); node!((_ {bv_node} {width_node})) } pub(crate) fn filter_to_node(&self, filter: &Option) -> Node { if let Some(filter) = filter { nodes!({ str_to_node(filter) }) } else { Node::List(vec![]) } } fn rounding_mode_to_node(&self, r: &RoundingMode) -> Node { match r { RoundingMode::RNE => str_to_node("RNE"), RoundingMode::RNA => str_to_node("RNA"), RoundingMode::RTP => str_to_node("RTP"), RoundingMode::RTN => str_to_node("RTN"), RoundingMode::RTZ => str_to_node("RTZ"), } } pub fn expr_to_node(&self, expr: &Expr) -> Node { match &**expr { ExprX::Const(Constant::Bool(b)) => Node::Atom(b.to_string()), ExprX::Const(Constant::Nat(n)) => Node::Atom((**n).clone()), ExprX::Const(Constant::Real(n)) => Node::Atom((**n).clone()), ExprX::Const(Constant::BitVec(n, width)) => self.bv_const_expr_to_node(n, *width), ExprX::Var(x) => Node::Atom(x.to_string()), ExprX::Old(snap, x) => { nodes!(old {str_to_node(&snap.to_string())} {str_to_node(&x.to_string())}) } ExprX::Apply(x, exprs) => { let mut nodes: Vec = Vec::new(); nodes.push(str_to_node(x)); for expr in exprs.iter() { nodes.push(self.expr_to_node(expr)); } Node::List(nodes) } ExprX::ApplyFun(typ, expr0, exprs) => { let mut nodes: Vec = Vec::new(); nodes.push(str_to_node("apply")); nodes.push(self.typ_to_node(typ)); nodes.push(self.expr_to_node(expr0)); for expr in exprs.iter() { nodes.push(self.expr_to_node(expr)); } Node::List(nodes) } ExprX::Unary(UnaryOp::FloatRoundToInt(r), expr) => { let r = self.rounding_mode_to_node(r); Node::List(vec![str_to_node("fp.roundToIntegral"), r, self.expr_to_node(expr)]) } ExprX::Unary(op, expr) => { let sop = match op { UnaryOp::Not => "not", UnaryOp::BitNot => "bvnot", UnaryOp::BitNeg => "bvneg", UnaryOp::BitExtract(_, _) => "extract", UnaryOp::BitZeroExtend(_) => "zero_extend", UnaryOp::BitSignExtend(_) => "sign_extend", UnaryOp::FloatNeg => "fp.neg", UnaryOp::FloatRoundToInt(_) => unreachable!(), UnaryOp::FloatIsNormal => "fp.isNormal", UnaryOp::FloatIsSubnormal => "fp.isSubnormal", UnaryOp::FloatIsZero => "fp.isZero", UnaryOp::FloatIsInfinite => "fp.isInfinite", UnaryOp::FloatIsNaN => "fp.isNaN", UnaryOp::FloatIsNegative => "fp.isNegative", UnaryOp::FloatIsPositive => "fp.isPositive", UnaryOp::FloatFromIeeeBits { .. } => "to_fp", UnaryOp::FloatToIeeeBits => "fp.to_ieee_bv", UnaryOp::FloatFrom { signed: false, .. } => "to_fp_unsigned", UnaryOp::FloatFrom { signed: true, .. } => "to_fp", UnaryOp::FloatToBitVec { signed: false, .. } => "fp.to_ubv", UnaryOp::FloatToBitVec { signed: true, .. } => "fp.to_sbv", UnaryOp::FloatToReal => "fp.to_real", UnaryOp::ToReal => "to_real", UnaryOp::RealToInt => "to_int", }; // ( (_ extract numeral numeral) BitVec ) match op { UnaryOp::BitExtract(high, low) => { let nodes_in = vec![ str_to_node("_"), str_to_node(sop), str_to_node(&high.to_string()), str_to_node(&low.to_string()), ]; let nodes = vec![Node::List(nodes_in), self.expr_to_node(expr)]; Node::List(nodes) } UnaryOp::BitZeroExtend(w) | UnaryOp::BitSignExtend(w) => { let nodes_in = vec![str_to_node("_"), str_to_node(sop), str_to_node(&w.to_string())]; let nodes = vec![Node::List(nodes_in), self.expr_to_node(expr)]; Node::List(nodes) } UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits } => { let nodes_in = vec![ str_to_node("_"), str_to_node(sop), str_to_node(&exp_bits.to_string()), str_to_node(&sig_bits.to_string()), ]; let nodes = vec![Node::List(nodes_in), self.expr_to_node(expr)]; Node::List(nodes) } UnaryOp::FloatFrom { exp_bits, sig_bits, signed: _, round } => { let nodes_in = vec![ str_to_node("_"), str_to_node(sop), str_to_node(&exp_bits.to_string()), str_to_node(&sig_bits.to_string()), ]; let r = self.rounding_mode_to_node(round); let nodes = vec![Node::List(nodes_in), r, self.expr_to_node(expr)]; Node::List(nodes) } UnaryOp::FloatToBitVec { bits, signed: _, round } => { let nodes_in = vec![ str_to_node("_"), str_to_node(sop), str_to_node(&bits.to_string()), ]; let r = self.rounding_mode_to_node(round); let nodes = vec![Node::List(nodes_in), r, self.expr_to_node(expr)]; Node::List(nodes) } _ => Node::List(vec![str_to_node(sop), self.expr_to_node(expr)]), } } ExprX::Binary(BinaryOp::Relation(relation, n), lhs, rhs) => { use crate::ast::Relation; let s = match relation { Relation::PartialOrder => "partial-order", Relation::LinearOrder => "linear-order", Relation::TreeOrder => "tree-order", Relation::PiecewiseLinearOrder => "piecewise-linear-order", }; let op = Node::List(vec![str_to_node("_"), str_to_node(s), Node::Atom(n.to_string())]); Node::List(vec![op, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } ExprX::Binary(op, lhs, rhs) => { let sop = match op { BinaryOp::Implies => str_to_node("=>"), BinaryOp::Eq => str_to_node("="), BinaryOp::Le => str_to_node("<="), BinaryOp::Ge => str_to_node(">="), BinaryOp::Lt => str_to_node("<"), BinaryOp::Gt => str_to_node(">"), BinaryOp::EuclideanDiv => str_to_node("div"), BinaryOp::EuclideanMod => str_to_node("mod"), BinaryOp::RealDiv => str_to_node("/"), BinaryOp::Relation(..) => unreachable!(), BinaryOp::BitXor => str_to_node("bvxor"), BinaryOp::BitAnd => str_to_node("bvand"), BinaryOp::BitOr => str_to_node("bvor"), BinaryOp::BitAdd => str_to_node("bvadd"), BinaryOp::BitSub => str_to_node("bvsub"), BinaryOp::BitMul => str_to_node("bvmul"), BinaryOp::BitUDiv => str_to_node("bvudiv"), BinaryOp::BitURem => str_to_node("bvurem"), BinaryOp::BitSDiv => str_to_node("bvsdiv"), BinaryOp::BitSRem => str_to_node("bvsrem"), BinaryOp::BitULt => str_to_node("bvult"), BinaryOp::BitUGt => str_to_node("bvugt"), BinaryOp::BitULe => str_to_node("bvule"), BinaryOp::BitUGe => str_to_node("bvuge"), BinaryOp::BitSLt => str_to_node("bvslt"), BinaryOp::BitSGt => str_to_node("bvsgt"), BinaryOp::BitSLe => str_to_node("bvsle"), BinaryOp::BitSGe => str_to_node("bvsge"), BinaryOp::LShr => str_to_node("bvlshr"), BinaryOp::AShr => str_to_node("bvashr"), BinaryOp::Shl => str_to_node("bvshl"), BinaryOp::BitConcat => str_to_node("concat"), BinaryOp::FloatAdd(_) => str_to_node("fp.add"), BinaryOp::FloatSub(_) => str_to_node("fp.sub"), BinaryOp::FloatMul(_) => str_to_node("fp.mul"), BinaryOp::FloatDiv(_) => str_to_node("fp.div"), BinaryOp::FloatEq => str_to_node("fp.eq"), BinaryOp::FloatLt => str_to_node("fp.lt"), BinaryOp::FloatGt => str_to_node("fp.gt"), BinaryOp::FloatLe => str_to_node("fp.leq"), BinaryOp::FloatGe => str_to_node("fp.geq"), BinaryOp::FieldUpdate(field_ident) => Node::List(vec![ str_to_node("_"), str_to_node("update-field"), str_to_node(&**field_ident), ]), }; let round = match op { BinaryOp::FloatAdd(r) | BinaryOp::FloatSub(r) | BinaryOp::FloatMul(r) | BinaryOp::FloatDiv(r) => Some(self.rounding_mode_to_node(r)), _ => None, }; match round { None => Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]), Some(r) => { Node::List(vec![sop, r, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } } } ExprX::Multi(op, exprs) => { let sop = match op { MultiOp::And => "and", MultiOp::Or => "or", MultiOp::Xor => "xor", MultiOp::Add => "+", MultiOp::Sub => "-", MultiOp::Mul => "*", MultiOp::Distinct => "distinct", MultiOp::Float => "fp", }; let mut nodes: Vec = Vec::new(); nodes.push(str_to_node(sop)); for expr in exprs.iter() { nodes.push(self.expr_to_node(expr)); } match op { MultiOp::Distinct if exprs.len() <= 1 => { // Z3 doesn't like the expression "(distinct)" // cvc5 doesn't like the singleton expression "(distinct expr)" return Node::Atom("true".to_string()); } _ => {} } Node::List(nodes) } ExprX::IfElse(expr1, expr2, expr3) => { nodes!(ite {self.expr_to_node(expr1)} {self.expr_to_node(expr2)} {self.expr_to_node(expr3)}) } ExprX::Array(exprs) => { let mut nodes: Vec = Vec::new(); nodes.push(str_to_node("array")); for expr in exprs.iter() { nodes.push(self.expr_to_node(expr)); } Node::List(nodes) } ExprX::Bind(bind, expr) => { let with_triggers = |expr: &Expr, triggers: &Triggers, qid: &Qid| { if triggers.len() == 0 && qid.is_none() { self.expr_to_node(expr) } else { let mut nodes: Vec = Vec::new(); nodes.push(str_to_node("!")); nodes.push(self.expr_to_node(expr)); for trigger in triggers.iter() { nodes.push(str_to_node(":pattern")); nodes.push(self.exprs_to_node(trigger)); } if let Some(s) = qid { nodes.push(str_to_node(":qid")); nodes.push(str_to_node(s)); if matches!(self.smt_encoding, SmtEncoding::Z3) { nodes.push(str_to_node(":skolemid")); nodes.push(str_to_node(&mk_skolem_id(s))); } } Node::List(nodes) } }; match &**bind { BindX::Let(binders) => { let s_binders = self.binders_to_node(binders, &|e| self.expr_to_node(e)); nodes!(let {s_binders} {self.expr_to_node(expr)}) } BindX::Quant(quant, binders, triggers, qid) => { let s_quant = match quant { Quant::Forall => "forall", Quant::Exists => "exists", }; let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let body = with_triggers(expr, triggers, qid); nodes!({str_to_node(s_quant)} {s_binders} {body}) } BindX::Lambda(binders, triggers, qid, None, None) => { let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let body = with_triggers(expr, triggers, qid); nodes!(lambda {s_binders} {body}) } BindX::Lambda(binders, triggers, qid, None, Some(expr_cond)) => { let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let cond = self.expr_to_node(expr_cond); let body = with_triggers(expr, triggers, qid); nodes!(lambda {s_binders} {cond} {body}) } BindX::Lambda(binders, triggers, qid, Some(wrap), None) => { let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let w = Node::Atom(wrap.wrap.to_string()); let id = self.expr_to_node(&wrap.id); let body = with_triggers(expr, triggers, qid); nodes!(lambda {w} {id} {s_binders} {body}) } BindX::Lambda(binders, triggers, qid, Some(wrap), Some(expr_cond)) => { let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let w = Node::Atom(wrap.wrap.to_string()); let id = self.expr_to_node(&wrap.id); let cond = self.expr_to_node(expr_cond); let body = with_triggers(expr, triggers, qid); nodes!(lambda {w} {id} {s_binders} {cond} {body}) } BindX::Choose(binders, triggers, qid, expr_cond) => { let s_binders = self.binders_to_node(binders, &|t| self.typ_to_node(t)); let cond = with_triggers(expr_cond, triggers, qid); let body = self.expr_to_node(expr); nodes!(choose {s_binders} {cond} {body}) } } } ExprX::LabeledAxiom(labels, filter, expr) => { let spans = vec_map(labels, |s| { Node::Atom(format!("\"{}\"", self.message_interface.get_message_label_note(s))) }); if spans.len() == 0 && filter.is_none() { self.expr_to_node(expr) } else { let filter_nodes = self.filter_to_node(filter); nodes!(axiom_location {Node::List(spans)} {filter_nodes} {self.expr_to_node(expr)}) } } ExprX::LabeledAssertion(_, error, filter, expr) => { let spans = vec_map(&self.message_interface.all_msgs(error), |s| { Node::Atom(format!("\"{}\"", s)) }); if spans.len() == 0 && filter.is_none() { self.expr_to_node(expr) } else { let filter_nodes = self.filter_to_node(filter); nodes!(location {Node::List(spans)} {filter_nodes} {self.expr_to_node(expr)}) } } } } pub fn exprs_to_node(&self, exprs: &Exprs) -> Node { Node::List(vec_map(exprs, |e| self.expr_to_node(e))) } pub(crate) fn binder_to_node Node>( &self, binder: &Binder, f: &F, ) -> Node { Node::List([str_to_node(&binder.name), f(&binder.a)].to_vec()) } pub(crate) fn binders_to_node Node>( &self, binders: &Binders, f: &F, ) -> Node { Node::List(vec_map(binders, |b| self.binder_to_node(b, f))) } pub(crate) fn multibinder_to_node Node>( &self, binder: &Binder>>, f: &F, ) -> Node { let mut nodes: Vec = Vec::new(); nodes.push(str_to_node(&binder.name)); for a in binder.a.iter() { nodes.push(f(a)); } Node::List(nodes) } pub fn sort_decl_to_node(&self, x: &Ident) -> Node { node!((declare-sort {str_to_node(x)} 0)) } pub fn datatypes_decl_to_node(&self, datatypes: &Datatypes) -> Node { let decls = Node::List(vec_map(datatypes, |d| nodes!({str_to_node(&d.name)} 0))); let defns = Node::List(vec_map(datatypes, |d| { Node::List(vec_map(&d.a, |variant| { self.multibinder_to_node(&variant, &|field| { self.binder_to_node(&field, &|t| self.typ_to_node(t)) }) })) })); if self.print_as_smt && datatypes.len() == 0 { // cvc5 doesn't like empty declare-datatypes nodes!(assert true) } else { node!((declare-datatypes {decls} {defns})) } } pub fn const_decl_to_node(&self, x: &Ident, typ: &Typ) -> Node { nodes!(declare-const {str_to_node(x)} {self.typ_to_node(typ)}) } pub fn fun_decl_to_node(&self, x: &Ident, typs: &Typs, typ: &Typ) -> Node { nodes!(declare-fun {str_to_node(x)} {self.typs_to_node(typs)} {self.typ_to_node(typ)}) } pub fn var_decl_to_node(&self, x: &Ident, typ: &Typ) -> Node { nodes!(declare-var {str_to_node(x)} {self.typ_to_node(typ)}) } pub fn axiom_to_node(&self, axiom: &Axiom) -> Node { let Axiom { named, expr } = axiom; if let Some(named) = named { nodes!(axiom ({str_to_node("!")} {self.expr_to_node(expr)} {str_to_node(":named")} {str_to_node(named)})) } else { nodes!(axiom {self.expr_to_node(expr)}) } } pub fn decl_to_node(&self, decl: &Decl) -> Node { match &**decl { DeclX::Sort(x) => self.sort_decl_to_node(x), DeclX::Datatypes(datatypes) => self.datatypes_decl_to_node(datatypes), DeclX::Const(x, typ) => self.const_decl_to_node(x, typ), DeclX::Fun(x, typs, typ) => self.fun_decl_to_node(x, typs, typ), DeclX::Var(x, typ) => self.var_decl_to_node(x, typ), DeclX::Axiom(axiom) => self.axiom_to_node(axiom), } } pub fn stmt_to_node(&self, stmt: &Stmt) -> Node { match &**stmt { StmtX::Assume(expr) => nodes!(assume {self.expr_to_node(expr)}), StmtX::Assert(_, labels, filter, expr) => { let spans = vec_map(&self.message_interface.all_msgs(labels), |s| { Node::Atom(format!("\"{}\"", s)) }); if spans.len() == 0 && filter.is_none() { nodes!(assert {self.expr_to_node(expr)}) } else { let filter_nodes = self.filter_to_node(filter); nodes!(assert {Node::List(spans)} {filter_nodes} {self.expr_to_node(expr)}) } } StmtX::Havoc(x) => nodes!(havoc {str_to_node(x)}), StmtX::Assign(x, expr) => nodes!(assign {str_to_node(x)} {self.expr_to_node(expr)}), StmtX::Snapshot(snap) => nodes!(snapshot {str_to_node(snap)}), StmtX::DeadEnd(s) => nodes!(deadend {self.stmt_to_node(s)}), StmtX::Breakable(x, s) => nodes!(breakable {str_to_node(x)} {self.stmt_to_node(s)}), StmtX::Break(x) => nodes!(break { str_to_node(x) }), StmtX::Block(stmts) | StmtX::Switch(stmts) => { let mut nodes = Vec::new(); let s = match &**stmt { StmtX::Block(_) => "block", _ => "switch", }; nodes.push(str_to_node(s)); for stmt in stmts.iter() { nodes.push(self.stmt_to_node(stmt)); } Node::List(nodes) } } } pub fn query_to_node(&self, query: &Query) -> Node { let QueryX { local, assertion } = &**query; let mut nodes = Vec::new(); nodes.push(str_to_node("check-valid")); for decl in local.iter() { nodes.push(self.decl_to_node(decl)); } nodes.push(self.stmt_to_node(assertion)); Node::List(nodes) } } pub struct NodeWriter {} impl NodeWriter { pub fn new() -> Self { NodeWriter {} } pub fn write_node( &mut self, serializer: &mut sise::Serializer, node: &Node, break_len: usize, brk: bool, ) { let break_line_at = if brk { 0 } else { break_len }; match node { Node::Atom(a) => { serializer.put_atom(a, break_line_at); } Node::List(l) => { serializer.begin_list(break_line_at); let mut brk = false; let mut was_pattern = false; for n in l { self.write_node(serializer, n, break_len + 1, brk && !was_pattern); was_pattern = false; match n { Node::Atom(a) if a == "=>" || a == "and" || a == "or" || a == "ite" || a == "let" || a == "assume" || a == "assert" || a == "location" || a == "check-valid" || a == "!" || a == "switch" || a == "block" => { brk = true; } Node::Atom(a) if a == ":pattern" || a == ":qid" || a == ":skolemid" => { was_pattern = true; } _ => {} } } serializer.end_list(); } } } pub fn node_to_string_indent(&mut self, indent: &String, node: &Node) -> String { let indentation = " "; let style = sise::SerializerStyle { line_break: &("\n".to_string() + &indent), indentation }; let mut result = String::new(); let mut serializer = sise::Serializer::new(style, &mut result); self.write_node(&mut serializer, &node, 80, false); serializer.finish(false); // Clean up result: clean_up_lines(result, indentation) } } pub(crate) fn node_to_string(node: &Node) -> String { NodeWriter::new().node_to_string_indent(&"".to_string(), node) } pub fn clean_up_lines(input: String, indentation: &str) -> String { let lines: Vec<&str> = input.lines().collect(); let mut result: String = "".to_string(); let mut i = 0; while i < lines.len() { let mut line = lines[i].to_owned(); // Consolidate closing ) lines: if line.trim() == ")" { while i + 1 < lines.len() && lines[i + 1].trim() == ")" { line = lines[i + 1].to_string() + &indentation[1..] + line.trim(); i += 1; } } result.push_str(&line); i += 1; if i < lines.len() { result.push_str("\n"); } } result }