Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387// Adapted from https://github.com/rust-lang/rust/blob/1.57.0/compiler/rustc_ast_pretty/src/pp.rs.// See "Algorithm notes" in the crate-level rustdoc.
use crate::ring::RingBuffer;use crate::{MARGIN, MIN_SPACE};use std::borrow::Cow;use std::cmp;use std::collections::VecDeque;use std::iter;
#[derive(Clone, Copy, PartialEq)]pub enum Breaks { Consistent, Inconsistent,}
#[derive(Clone, Copy, Default)]pub struct BreakToken { pub offset: isize, pub blank_space: usize, pub pre_break: Option<char>, pub post_break: &'static str, pub no_break: Option<char>, pub if_nonempty: bool, pub never_break: bool,}
#[derive(Clone, Copy)]pub struct BeginToken { pub offset: isize, pub breaks: Breaks,}
#[derive(Clone)]pub enum Token { String(Cow<'static, str>), Break(BreakToken), Begin(BeginToken), End,}
#[derive(Copy, Clone)]enum PrintFrame { Fits(Breaks), Broken(usize, Breaks),}
pub const SIZE_INFINITY: isize = 0xffff;
pub struct Printer { out: String, // Number of spaces left on line space: isize, // Ring-buffer of tokens and calculated sizes buf: RingBuffer<BufEntry>, // Total size of tokens already printed left_total: isize, // Total size of tokens enqueued, including printed and not yet printed right_total: isize, // Holds the ring-buffer index of the Begin that started the current block, // possibly with the most recent Break after that Begin (if there is any) on // top of it. Values are pushed and popped on the back of the queue using it // like stack, and elsewhere old values are popped from the front of the // queue as they become irrelevant due to the primary ring-buffer advancing. scan_stack: VecDeque<usize>, // Stack of blocks-in-progress being flushed by print print_stack: Vec<PrintFrame>, // Level of indentation of current line indent: usize, // Buffered indentation to avoid writing trailing whitespace pending_indentation: usize,}
#[derive(Clone)]struct BufEntry { token: Token, size: isize,}
impl Printer { pub fn new() -> Self { Printer { out: String::new(), space: MARGIN, buf: RingBuffer::new(), left_total: 0, right_total: 0, scan_stack: VecDeque::new(), print_stack: Vec::new(), indent: 0, pending_indentation: 0, } }
pub fn eof(mut self) -> String { if !self.scan_stack.is_empty() { self.check_stack(0); self.advance_left(); } self.out }
pub fn scan_begin(&mut self, token: BeginToken) { if self.scan_stack.is_empty() { self.left_total = 1; self.right_total = 1; self.buf.clear(); } let right = self.buf.push(BufEntry { token: Token::Begin(token), size: -self.right_total, }); self.scan_stack.push_back(right); }
pub fn scan_end(&mut self) { if self.scan_stack.is_empty() { self.print_end(); } else { if !self.buf.is_empty() { if let Token::Break(break_token) = self.buf.last().token { if self.buf.len() >= 2 { if let Token::Begin(_) = self.buf.second_last().token { self.buf.pop_last(); self.buf.pop_last(); self.scan_stack.pop_back(); self.scan_stack.pop_back(); self.right_total -= break_token.blank_space as isize; return; } } if break_token.if_nonempty { self.buf.pop_last(); self.scan_stack.pop_back(); self.right_total -= break_token.blank_space as isize; } } } let right = self.buf.push(BufEntry { token: Token::End, size: -1, }); self.scan_stack.push_back(right); } }
pub fn scan_break(&mut self, token: BreakToken) { if self.scan_stack.is_empty() { self.left_total = 1; self.right_total = 1; self.buf.clear(); } else { self.check_stack(0); } let right = self.buf.push(BufEntry { token: Token::Break(token), size: -self.right_total, }); self.scan_stack.push_back(right); self.right_total += token.blank_space as isize; }
pub fn scan_string(&mut self, string: Cow<'static, str>) { if self.scan_stack.is_empty() { self.print_string(string); } else { let len = string.len() as isize; self.buf.push(BufEntry { token: Token::String(string), size: len, }); self.right_total += len; self.check_stream(); } }
#[track_caller] pub fn offset(&mut self, offset: isize) { match &mut self.buf.last_mut().token { Token::Break(token) => token.offset += offset, Token::Begin(_) => {} Token::String(_) | Token::End => unreachable!(), } }
pub fn end_with_max_width(&mut self, max: isize) { let mut depth = 1; for &index in self.scan_stack.iter().rev() { let entry = &self.buf[index]; match entry.token { Token::Begin(_) => { depth -= 1; if depth == 0 { if entry.size < 0 { let actual_width = entry.size + self.right_total; if actual_width > max { self.buf.push(BufEntry { token: Token::String(Cow::Borrowed("")), size: SIZE_INFINITY, }); self.right_total += SIZE_INFINITY; } } break; } } Token::End => depth += 1, Token::Break(_) => {} Token::String(_) => unreachable!(), } } self.scan_end(); }
pub fn ends_with(&self, ch: char) -> bool { for i in self.buf.index_range().rev() { if let Token::String(token) = &self.buf[i].token { return token.ends_with(ch); } } self.out.ends_with(ch) }
fn check_stream(&mut self) { while self.right_total - self.left_total > self.space { if *self.scan_stack.front().unwrap() == self.buf.index_range().start { self.scan_stack.pop_front().unwrap(); self.buf.first_mut().size = SIZE_INFINITY; }
self.advance_left();
if self.buf.is_empty() { break; } } }
fn advance_left(&mut self) { while self.buf.first().size >= 0 { let left = self.buf.pop_first();
match left.token { Token::String(string) => { self.left_total += left.size; self.print_string(string); } Token::Break(token) => { self.left_total += token.blank_space as isize; self.print_break(token, left.size); } Token::Begin(token) => self.print_begin(token, left.size), Token::End => self.print_end(), }
if self.buf.is_empty() { break; } } }
fn check_stack(&mut self, mut depth: usize) { while let Some(&index) = self.scan_stack.back() { let entry = &mut self.buf[index]; match entry.token { Token::Begin(_) => { if depth == 0 { break; } self.scan_stack.pop_back().unwrap(); entry.size += self.right_total; depth -= 1; } Token::End => { self.scan_stack.pop_back().unwrap(); entry.size = 1; depth += 1; } Token::Break(_) => { self.scan_stack.pop_back().unwrap(); entry.size += self.right_total; if depth == 0 { break; } } Token::String(_) => unreachable!(), } } }
fn get_top(&self) -> PrintFrame { const OUTER: PrintFrame = PrintFrame::Broken(0, Breaks::Inconsistent); self.print_stack.last().map_or(OUTER, PrintFrame::clone) }
fn print_begin(&mut self, token: BeginToken, size: isize) { if cfg!(prettyplease_debug) { self.out.push(match token.breaks { Breaks::Consistent => '«', Breaks::Inconsistent => '‹', }); if cfg!(prettyplease_debug_indent) { self.out .extend(token.offset.to_string().chars().map(|ch| match ch { '0'..='9' => ['₀', '₁', '₂', '₃', '₄', '₅', '₆', '₇', '₈', '₉'] [(ch as u8 - b'0') as usize], '-' => '₋', _ => unreachable!(), })); } } if size > self.space { self.print_stack .push(PrintFrame::Broken(self.indent, token.breaks)); self.indent = usize::try_from(self.indent as isize + token.offset).unwrap(); } else { self.print_stack.push(PrintFrame::Fits(token.breaks)); } }
fn print_end(&mut self) { let breaks = match self.print_stack.pop().unwrap() { PrintFrame::Broken(indent, breaks) => { self.indent = indent; breaks } PrintFrame::Fits(breaks) => breaks, }; if cfg!(prettyplease_debug) { self.out.push(match breaks { Breaks::Consistent => '»', Breaks::Inconsistent => '›', }); } }
fn print_break(&mut self, token: BreakToken, size: isize) { let fits = token.never_break || match self.get_top() { PrintFrame::Fits(..) => true, PrintFrame::Broken(.., Breaks::Consistent) => false, PrintFrame::Broken(.., Breaks::Inconsistent) => size <= self.space, }; if fits { self.pending_indentation += token.blank_space; self.space -= token.blank_space as isize; if let Some(no_break) = token.no_break { self.out.push(no_break); self.space -= no_break.len_utf8() as isize; } if cfg!(prettyplease_debug) { self.out.push('·'); } } else { if let Some(pre_break) = token.pre_break { self.print_indent(); self.out.push(pre_break); } if cfg!(prettyplease_debug) { self.out.push('·'); } self.out.push('\n'); let indent = self.indent as isize + token.offset; self.pending_indentation = usize::try_from(indent).unwrap(); self.space = cmp::max(MARGIN - indent, MIN_SPACE); if !token.post_break.is_empty() { self.print_indent(); self.out.push_str(token.post_break); self.space -= token.post_break.len() as isize; } } }
fn print_string(&mut self, string: Cow<'static, str>) { self.print_indent(); self.out.push_str(&string); self.space -= string.len() as isize; }
fn print_indent(&mut self) { self.out.reserve(self.pending_indentation); self.out .extend(iter::repeat(' ').take(self.pending_indentation)); self.pending_indentation = 0; }}