oxilean_parse/prettyprint/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use crate::ast_impl::*;
7use std::fmt::{self, Write};
8
9/// Parenthesization mode.
10#[derive(Clone, Debug, Default, PartialEq, Eq)]
11pub enum ParensMode {
12    /// Only add parentheses when needed based on precedence.
13    #[default]
14    Minimal,
15    /// Always add parentheses for compound expressions.
16    Full,
17}
18/// A simple column layout calculator.
19#[allow(dead_code)]
20#[allow(missing_docs)]
21pub struct ColumnLayout {
22    /// Column widths
23    pub widths: Vec<usize>,
24}
25impl ColumnLayout {
26    /// Create from a list of column widths.
27    #[allow(dead_code)]
28    pub fn new(widths: Vec<usize>) -> Self {
29        ColumnLayout { widths }
30    }
31    /// Total width including column separators.
32    #[allow(dead_code)]
33    pub fn total_width(&self, sep_width: usize) -> usize {
34        let sum: usize = self.widths.iter().sum();
35        sum + sep_width * self.widths.len().saturating_sub(1)
36    }
37    /// Number of columns.
38    #[allow(dead_code)]
39    pub fn num_cols(&self) -> usize {
40        self.widths.len()
41    }
42}
43/// Configuration for the pretty printer.
44#[derive(Clone, Debug)]
45pub struct PrettyConfig {
46    /// Maximum line width before breaking (default 100).
47    pub max_width: usize,
48    /// Number of spaces per indentation level (default 2).
49    pub indent_size: usize,
50    /// Whether to show implicit arguments.
51    pub show_implicit: bool,
52    /// Whether to show universe annotations.
53    pub show_universes: bool,
54    /// Whether to use unicode symbols (e.g. `->` vs `\u{2192}`).
55    pub use_unicode: bool,
56    /// Whether to try to use registered notations for App nodes.
57    pub use_notation: bool,
58    /// Parenthesization mode.
59    pub parens_mode: ParensMode,
60}
61impl PrettyConfig {
62    /// Create a new config with all defaults.
63    #[allow(dead_code)]
64    pub fn new() -> Self {
65        Self::default()
66    }
67    /// Set the maximum line width.
68    #[allow(dead_code)]
69    pub fn with_max_width(mut self, width: usize) -> Self {
70        self.max_width = width;
71        self
72    }
73    /// Set the indent size.
74    #[allow(dead_code)]
75    pub fn with_indent_size(mut self, size: usize) -> Self {
76        self.indent_size = size;
77        self
78    }
79    /// Enable or disable showing implicit arguments.
80    #[allow(dead_code)]
81    pub fn with_show_implicit(mut self, show: bool) -> Self {
82        self.show_implicit = show;
83        self
84    }
85    /// Enable or disable showing universe annotations.
86    #[allow(dead_code)]
87    pub fn with_show_universes(mut self, show: bool) -> Self {
88        self.show_universes = show;
89        self
90    }
91    /// Enable or disable unicode symbols.
92    #[allow(dead_code)]
93    pub fn with_unicode(mut self, unicode: bool) -> Self {
94        self.use_unicode = unicode;
95        self
96    }
97    /// Enable or disable notation-aware printing.
98    #[allow(dead_code)]
99    pub fn with_notation(mut self, notation: bool) -> Self {
100        self.use_notation = notation;
101        self
102    }
103    /// Set the parenthesization mode.
104    #[allow(dead_code)]
105    pub fn with_parens_mode(mut self, mode: ParensMode) -> Self {
106        self.parens_mode = mode;
107        self
108    }
109}
110/// A registered notation for notation-aware printing.
111#[derive(Clone, Debug)]
112#[allow(dead_code)]
113struct NotationEntry {
114    /// The function name this notation applies to (e.g. "HAdd.hAdd").
115    func_name: String,
116    /// The operator symbol to display (e.g. "+").
117    symbol: String,
118    /// Precedence of this operator.
119    precedence: u32,
120    /// Whether this is a binary infix operator.
121    is_infix: bool,
122}
123/// Pretty printer for surface expressions.
124pub struct PrettyPrinter {
125    /// Indentation level
126    indent: usize,
127    /// Output buffer
128    buffer: String,
129    /// Configuration
130    pub(super) config: PrettyConfig,
131    /// Registered notations for notation-aware printing
132    #[allow(dead_code)]
133    notations: Vec<NotationEntry>,
134}
135impl PrettyPrinter {
136    /// Create a new pretty printer with default configuration.
137    pub fn new() -> Self {
138        Self {
139            indent: 0,
140            buffer: String::new(),
141            config: PrettyConfig::default(),
142            notations: Vec::new(),
143        }
144    }
145    /// Create a pretty printer with the given configuration.
146    #[allow(dead_code)]
147    pub fn with_config(config: PrettyConfig) -> Self {
148        Self {
149            indent: 0,
150            buffer: String::new(),
151            config,
152            notations: Vec::new(),
153        }
154    }
155    /// Get the output buffer.
156    pub fn output(self) -> String {
157        self.buffer
158    }
159    /// Get the current length of the output buffer.
160    #[allow(dead_code)]
161    fn current_len(&self) -> usize {
162        self.buffer.len()
163    }
164    /// Get the column position on the current line.
165    #[allow(dead_code)]
166    fn current_column(&self) -> usize {
167        match self.buffer.rfind('\n') {
168            Some(idx) => self.buffer.len() - idx - 1,
169            None => self.buffer.len(),
170        }
171    }
172    /// Register a notation for notation-aware printing.
173    #[allow(dead_code)]
174    pub fn register_notation(
175        &mut self,
176        func_name: &str,
177        symbol: &str,
178        precedence: u32,
179        is_infix: bool,
180    ) {
181        self.notations.push(NotationEntry {
182            func_name: func_name.to_string(),
183            symbol: symbol.to_string(),
184            precedence,
185            is_infix,
186        });
187    }
188    /// Return the arrow symbol based on configuration.
189    fn arrow(&self) -> &str {
190        if self.config.use_unicode {
191            "\u{2192}"
192        } else {
193            "->"
194        }
195    }
196    /// Return the forall symbol based on configuration.
197    fn forall_sym(&self) -> &str {
198        if self.config.use_unicode {
199            "\u{2200}"
200        } else {
201            "forall"
202        }
203    }
204    /// Return the lambda symbol based on configuration.
205    fn lambda_sym(&self) -> &str {
206        if self.config.use_unicode {
207            "\u{03bb}"
208        } else {
209            "fun"
210        }
211    }
212    /// Return the product symbol based on configuration.
213    #[allow(dead_code)]
214    fn prod_sym(&self) -> &str {
215        if self.config.use_unicode {
216            "\u{00d7}"
217        } else {
218            "Prod"
219        }
220    }
221    /// Return the not symbol based on configuration.
222    #[allow(dead_code)]
223    fn not_sym(&self) -> &str {
224        if self.config.use_unicode {
225            "\u{00ac}"
226        } else {
227            "Not"
228        }
229    }
230    /// Write indentation at the current level.
231    fn write_indent(&mut self) {
232        for _ in 0..(self.indent * self.config.indent_size) {
233            self.buffer.push(' ');
234        }
235    }
236    /// Increase indentation.
237    fn increase_indent(&mut self) {
238        self.indent += 1;
239    }
240    /// Decrease indentation.
241    fn decrease_indent(&mut self) {
242        if self.indent > 0 {
243            self.indent -= 1;
244        }
245    }
246    /// Try to print an expression on a single line. Returns the string
247    /// if it fits within `max_width` from the current column, otherwise `None`.
248    #[allow(dead_code)]
249    pub fn try_single_line(&mut self, expr: &SurfaceExpr) -> Option<String> {
250        let mut sub = PrettyPrinter::with_config(self.config.clone());
251        sub.notations = self.notations.clone();
252        if sub.print_expr(expr).is_err() {
253            return None;
254        }
255        let result = sub.output();
256        let col = self.current_column();
257        if col + result.len() <= self.config.max_width {
258            Some(result)
259        } else {
260            None
261        }
262    }
263    /// Try to fit an expression on a single line; if not, use multi-line
264    /// formatting with the given indentation.
265    #[allow(dead_code)]
266    fn print_expr_auto(&mut self, expr: &SurfaceExpr) -> fmt::Result {
267        if let Some(s) = self.try_single_line(expr) {
268            write!(self.buffer, "{}", s)
269        } else {
270            self.print_expr_multiline(expr)
271        }
272    }
273    /// Print an expression using multi-line formatting.
274    #[allow(dead_code)]
275    fn print_expr_multiline(&mut self, expr: &SurfaceExpr) -> fmt::Result {
276        match expr {
277            SurfaceExpr::Lam(binders, body) => {
278                let sym = self.lambda_sym().to_string();
279                write!(self.buffer, "{}", sym)?;
280                for binder in binders {
281                    self.print_binder(binder)?;
282                }
283                writeln!(self.buffer, " =>")?;
284                self.increase_indent();
285                self.write_indent();
286                self.print_expr(&body.value)?;
287                self.decrease_indent();
288                Ok(())
289            }
290            SurfaceExpr::Let(name, ty, val, body) => {
291                write!(self.buffer, "let {}", name)?;
292                if let Some(ty) = ty {
293                    write!(self.buffer, " : ")?;
294                    self.print_expr(&ty.value)?;
295                }
296                write!(self.buffer, " := ")?;
297                self.print_expr(&val.value)?;
298                writeln!(self.buffer)?;
299                self.write_indent();
300                write!(self.buffer, "in ")?;
301                self.print_expr(&body.value)
302            }
303            SurfaceExpr::If(c, t, e) => {
304                write!(self.buffer, "if ")?;
305                self.print_expr(&c.value)?;
306                writeln!(self.buffer)?;
307                self.increase_indent();
308                self.write_indent();
309                write!(self.buffer, "then ")?;
310                self.print_expr(&t.value)?;
311                writeln!(self.buffer)?;
312                self.write_indent();
313                write!(self.buffer, "else ")?;
314                self.print_expr(&e.value)?;
315                self.decrease_indent();
316                Ok(())
317            }
318            _ => self.print_expr(expr),
319        }
320    }
321    /// Print a single binder.
322    pub(super) fn print_binder(&mut self, binder: &Binder) -> fmt::Result {
323        let (open, close) = match binder.info {
324            BinderKind::Default => ("(", ")"),
325            BinderKind::Implicit => {
326                if !self.config.show_implicit {
327                    return Ok(());
328                }
329                ("{", "}")
330            }
331            BinderKind::Instance => ("[", "]"),
332            BinderKind::StrictImplicit => ("{{", "}}"),
333        };
334        write!(self.buffer, " {}{}", open, binder.name)?;
335        if let Some(ty) = &binder.ty {
336            write!(self.buffer, " : ")?;
337            self.print_expr(&ty.value)?;
338        }
339        write!(self.buffer, "{}", close)
340    }
341    /// Print a binder always, regardless of implicit settings.
342    fn print_binder_always(&mut self, binder: &Binder) -> fmt::Result {
343        let (open, close) = match binder.info {
344            BinderKind::Default => ("(", ")"),
345            BinderKind::Implicit => ("{", "}"),
346            BinderKind::Instance => ("[", "]"),
347            BinderKind::StrictImplicit => ("{{", "}}"),
348        };
349        write!(self.buffer, " {}{}", open, binder.name)?;
350        if let Some(ty) = &binder.ty {
351            write!(self.buffer, " : ")?;
352            self.print_expr(&ty.value)?;
353        }
354        write!(self.buffer, "{}", close)
355    }
356    /// Get the precedence of an expression.
357    #[allow(dead_code)]
358    fn expr_prec(&self, expr: &SurfaceExpr) -> u32 {
359        match expr {
360            SurfaceExpr::Sort(_)
361            | SurfaceExpr::Var(_)
362            | SurfaceExpr::Lit(_)
363            | SurfaceExpr::Hole
364            | SurfaceExpr::ListLit(_)
365            | SurfaceExpr::Tuple(_)
366            | SurfaceExpr::AnonymousCtor(_) => prec::ATOM,
367            SurfaceExpr::Proj(_, _) => prec::ATOM,
368            SurfaceExpr::App(_, _) => prec::APP,
369            SurfaceExpr::Ann(_, _) => prec::ATOM,
370            SurfaceExpr::Pi(binders, _) => {
371                if binders.len() == 1 && binders[0].name == "_" {
372                    prec::ARROW
373                } else {
374                    prec::LAMBDA
375                }
376            }
377            SurfaceExpr::Lam(_, _) => prec::LAMBDA,
378            SurfaceExpr::Let(_, _, _, _) => prec::LET,
379            SurfaceExpr::If(_, _, _) => prec::IF,
380            SurfaceExpr::Match(_, _) => prec::LET,
381            SurfaceExpr::Do(_) => prec::LET,
382            SurfaceExpr::Have(_, _, _, _) => prec::LET,
383            SurfaceExpr::Suffices(_, _, _) => prec::LET,
384            SurfaceExpr::Show(_, _) => prec::LET,
385            SurfaceExpr::NamedArg(_, _, _) => prec::APP,
386            SurfaceExpr::Return(_) => prec::LET,
387            SurfaceExpr::StringInterp(_) => prec::ATOM,
388            SurfaceExpr::Range(_, _) => prec::LET,
389            SurfaceExpr::ByTactic(_) => prec::LET,
390            SurfaceExpr::Calc(_) => prec::LET,
391        }
392    }
393    /// Print an expression with precedence-aware parenthesization.
394    ///
395    /// If the expression's own precedence is less than `outer_prec`,
396    /// parentheses are added.
397    #[allow(dead_code)]
398    pub fn print_expr_prec(&mut self, expr: &SurfaceExpr, outer_prec: u32) -> fmt::Result {
399        let inner_prec = self.expr_prec(expr);
400        let needs_parens = match self.config.parens_mode {
401            ParensMode::Full => !matches!(
402                expr,
403                SurfaceExpr::Sort(_)
404                    | SurfaceExpr::Var(_)
405                    | SurfaceExpr::Lit(_)
406                    | SurfaceExpr::Hole
407            ),
408            ParensMode::Minimal => inner_prec < outer_prec,
409        };
410        if needs_parens {
411            write!(self.buffer, "(")?;
412            self.print_expr(expr)?;
413            write!(self.buffer, ")")
414        } else {
415            self.print_expr(expr)
416        }
417    }
418    /// Pretty print a pattern.
419    pub fn print_pattern(&mut self, pat: &Pattern) -> fmt::Result {
420        match pat {
421            Pattern::Wild => write!(self.buffer, "_"),
422            Pattern::Var(name) => write!(self.buffer, "{}", name),
423            Pattern::Ctor(name, args) => {
424                if args.is_empty() {
425                    write!(self.buffer, "{}", name)
426                } else {
427                    write!(self.buffer, "{}", name)?;
428                    for arg in args {
429                        write!(self.buffer, " ")?;
430                        self.print_pattern_atom(&arg.value)?;
431                    }
432                    Ok(())
433                }
434            }
435            Pattern::Lit(lit) => write!(self.buffer, "{}", lit),
436            Pattern::Or(left, right) => {
437                self.print_pattern(&left.value)?;
438                write!(self.buffer, " | ")?;
439                self.print_pattern(&right.value)
440            }
441        }
442    }
443    /// Print an atomic pattern (parenthesize compound patterns).
444    fn print_pattern_atom(&mut self, pat: &Pattern) -> fmt::Result {
445        match pat {
446            Pattern::Wild | Pattern::Var(_) | Pattern::Lit(_) => self.print_pattern(pat),
447            Pattern::Ctor(_, args) if args.is_empty() => self.print_pattern(pat),
448            _ => {
449                write!(self.buffer, "(")?;
450                self.print_pattern(pat)?;
451                write!(self.buffer, ")")
452            }
453        }
454    }
455    /// Pretty print a match expression with aligned arms.
456    #[allow(dead_code)]
457    pub fn print_match(&mut self, scrutinee: &SurfaceExpr, arms: &[MatchArm]) -> fmt::Result {
458        write!(self.buffer, "match ")?;
459        self.print_expr(scrutinee)?;
460        write!(self.buffer, " with")?;
461        for arm in arms {
462            writeln!(self.buffer)?;
463            self.write_indent();
464            write!(self.buffer, "| ")?;
465            self.print_pattern(&arm.pattern.value)?;
466            if let Some(guard) = &arm.guard {
467                write!(self.buffer, " when ")?;
468                self.print_expr(&guard.value)?;
469            }
470            write!(self.buffer, " => ")?;
471            self.print_expr(&arm.rhs.value)?;
472        }
473        Ok(())
474    }
475    /// Pretty print a do block with indented actions.
476    #[allow(dead_code)]
477    pub fn print_do(&mut self, actions: &[DoAction]) -> fmt::Result {
478        writeln!(self.buffer, "do")?;
479        self.increase_indent();
480        for action in actions {
481            self.write_indent();
482            match action {
483                DoAction::Let(name, expr) => {
484                    write!(self.buffer, "let {} := ", name)?;
485                    self.print_expr(&expr.value)?;
486                }
487                DoAction::LetTyped(name, ty, expr) => {
488                    write!(self.buffer, "let {} : ", name)?;
489                    self.print_expr(&ty.value)?;
490                    write!(self.buffer, " := ")?;
491                    self.print_expr(&expr.value)?;
492                }
493                DoAction::Bind(name, expr) => {
494                    let la = self.left_arrow().to_string();
495                    write!(self.buffer, "let {} {} ", name, la)?;
496                    self.print_expr(&expr.value)?;
497                }
498                DoAction::Expr(expr) => {
499                    self.print_expr(&expr.value)?;
500                }
501                DoAction::Return(expr) => {
502                    write!(self.buffer, "return ")?;
503                    self.print_expr(&expr.value)?;
504                }
505            }
506            writeln!(self.buffer)?;
507        }
508        self.decrease_indent();
509        Ok(())
510    }
511    /// Return the left arrow symbol based on configuration.
512    fn left_arrow(&self) -> &str {
513        if self.config.use_unicode {
514            "\u{2190}"
515        } else {
516            "<-"
517        }
518    }
519    /// Pretty print an inductive type declaration.
520    #[allow(dead_code)]
521    pub fn print_inductive(
522        &mut self,
523        name: &str,
524        univ_params: &[String],
525        params: &[Binder],
526        ty: &SurfaceExpr,
527        ctors: &[Constructor],
528    ) -> fmt::Result {
529        write!(self.buffer, "inductive {}", name)?;
530        if !univ_params.is_empty() {
531            write!(self.buffer, ".{{{}}}", univ_params.join(", "))?;
532        }
533        for param in params {
534            self.print_binder_always(param)?;
535        }
536        write!(self.buffer, " : ")?;
537        self.print_expr(ty)?;
538        write!(self.buffer, " where")?;
539        for ctor in ctors {
540            writeln!(self.buffer)?;
541            self.write_indent();
542            write!(self.buffer, "| {} : ", ctor.name)?;
543            self.print_expr(&ctor.ty.value)?;
544        }
545        Ok(())
546    }
547    /// Pretty print a surface expression.
548    pub fn print_expr(&mut self, expr: &SurfaceExpr) -> fmt::Result {
549        match expr {
550            SurfaceExpr::Sort(sort) => {
551                if !self.config.show_universes {
552                    match sort {
553                        SortKind::Type | SortKind::Prop => {
554                            write!(self.buffer, "{}", sort)
555                        }
556                        SortKind::TypeU(_) => write!(self.buffer, "Type"),
557                        SortKind::SortU(_) => write!(self.buffer, "Sort"),
558                    }
559                } else {
560                    write!(self.buffer, "{}", sort)
561                }
562            }
563            SurfaceExpr::Var(name) => write!(self.buffer, "{}", name),
564            SurfaceExpr::App(fun, arg) => {
565                self.print_expr(&fun.value)?;
566                write!(self.buffer, " ")?;
567                self.print_atom(&arg.value)
568            }
569            SurfaceExpr::Lam(binders, body) => {
570                let sym = self.lambda_sym().to_string();
571                write!(self.buffer, "{}", sym)?;
572                for binder in binders {
573                    self.print_binder_always(binder)?;
574                }
575                write!(self.buffer, " => ")?;
576                self.print_expr(&body.value)
577            }
578            SurfaceExpr::Pi(binders, body) => {
579                if binders.len() == 1 && binders[0].name == "_" {
580                    if let Some(ty) = &binders[0].ty {
581                        self.print_atom(&ty.value)?;
582                    }
583                    let arr = self.arrow().to_string();
584                    write!(self.buffer, " {} ", arr)?;
585                    self.print_expr(&body.value)
586                } else {
587                    let sym = self.forall_sym().to_string();
588                    write!(self.buffer, "{}", sym)?;
589                    for binder in binders {
590                        self.print_binder_always(binder)?;
591                    }
592                    write!(self.buffer, ", ")?;
593                    self.print_expr(&body.value)
594                }
595            }
596            SurfaceExpr::Let(name, ty, val, body) => {
597                write!(self.buffer, "let {} ", name)?;
598                if let Some(ty) = ty {
599                    write!(self.buffer, ": ")?;
600                    self.print_expr(&ty.value)?;
601                    write!(self.buffer, " ")?;
602                }
603                write!(self.buffer, ":= ")?;
604                self.print_expr(&val.value)?;
605                write!(self.buffer, " in ")?;
606                self.print_expr(&body.value)
607            }
608            SurfaceExpr::Lit(lit) => write!(self.buffer, "{}", lit),
609            SurfaceExpr::Ann(expr, ty) => {
610                write!(self.buffer, "(")?;
611                self.print_expr(&expr.value)?;
612                write!(self.buffer, " : ")?;
613                self.print_expr(&ty.value)?;
614                write!(self.buffer, ")")
615            }
616            SurfaceExpr::Hole => write!(self.buffer, "_"),
617            SurfaceExpr::Proj(expr, field) => {
618                self.print_atom(&expr.value)?;
619                write!(self.buffer, ".{}", field)
620            }
621            SurfaceExpr::If(c, t, e) => {
622                write!(self.buffer, "if ")?;
623                self.print_expr(&c.value)?;
624                write!(self.buffer, " then ")?;
625                self.print_expr(&t.value)?;
626                write!(self.buffer, " else ")?;
627                self.print_expr(&e.value)
628            }
629            SurfaceExpr::Match(scrutinee, arms) => self.print_match(&scrutinee.value, arms),
630            SurfaceExpr::Do(actions) => self.print_do(actions),
631            SurfaceExpr::Have(name, ty, proof, body) => {
632                write!(self.buffer, "have {} : ", name)?;
633                self.print_expr(&ty.value)?;
634                write!(self.buffer, " := ")?;
635                self.print_expr(&proof.value)?;
636                write!(self.buffer, "; ")?;
637                self.print_expr(&body.value)
638            }
639            SurfaceExpr::Suffices(name, ty, body) => {
640                write!(self.buffer, "suffices {} : ", name)?;
641                self.print_expr(&ty.value)?;
642                write!(self.buffer, " from ")?;
643                self.print_expr(&body.value)
644            }
645            SurfaceExpr::Show(ty, proof) => {
646                write!(self.buffer, "show ")?;
647                self.print_expr(&ty.value)?;
648                write!(self.buffer, " from ")?;
649                self.print_expr(&proof.value)
650            }
651            SurfaceExpr::NamedArg(func, name, arg) => {
652                self.print_expr(&func.value)?;
653                write!(self.buffer, " ({} := ", name)?;
654                self.print_expr(&arg.value)?;
655                write!(self.buffer, ")")
656            }
657            SurfaceExpr::AnonymousCtor(fields) => {
658                write!(self.buffer, "<")?;
659                for (i, f) in fields.iter().enumerate() {
660                    if i > 0 {
661                        write!(self.buffer, ", ")?;
662                    }
663                    self.print_expr(&f.value)?;
664                }
665                write!(self.buffer, ">")
666            }
667            SurfaceExpr::ListLit(elems) => {
668                write!(self.buffer, "[")?;
669                for (i, e) in elems.iter().enumerate() {
670                    if i > 0 {
671                        write!(self.buffer, ", ")?;
672                    }
673                    self.print_expr(&e.value)?;
674                }
675                write!(self.buffer, "]")
676            }
677            SurfaceExpr::Tuple(elems) => {
678                write!(self.buffer, "(")?;
679                for (i, e) in elems.iter().enumerate() {
680                    if i > 0 {
681                        write!(self.buffer, ", ")?;
682                    }
683                    self.print_expr(&e.value)?;
684                }
685                write!(self.buffer, ")")
686            }
687            SurfaceExpr::Return(expr) => {
688                write!(self.buffer, "return ")?;
689                self.print_expr(&expr.value)
690            }
691            SurfaceExpr::StringInterp(_parts) => write!(self.buffer, "s!\"...\""),
692            SurfaceExpr::Range(lo, hi) => {
693                if let Some(lo) = lo {
694                    self.print_expr(&lo.value)?;
695                }
696                write!(self.buffer, "..")?;
697                if let Some(hi) = hi {
698                    self.print_expr(&hi.value)?;
699                }
700                Ok(())
701            }
702            SurfaceExpr::ByTactic(tactics) => {
703                write!(self.buffer, "by")?;
704                for (i, t) in tactics.iter().enumerate() {
705                    if i > 0 {
706                        write!(self.buffer, ";")?;
707                    }
708                    write!(self.buffer, " {}", t.value)?;
709                }
710                Ok(())
711            }
712            SurfaceExpr::Calc(steps) => {
713                write!(self.buffer, "calc")?;
714                for step in steps {
715                    write!(self.buffer, "\n  ")?;
716                    self.print_expr(&step.lhs.value)?;
717                    write!(self.buffer, " {} ", step.rel)?;
718                    self.print_expr(&step.rhs.value)?;
719                    write!(self.buffer, " := ")?;
720                    self.print_expr(&step.proof.value)?;
721                }
722                Ok(())
723            }
724        }
725    }
726    /// Print an atomic expression (parenthesize if needed).
727    fn print_atom(&mut self, expr: &SurfaceExpr) -> fmt::Result {
728        match expr {
729            SurfaceExpr::Sort(_)
730            | SurfaceExpr::Var(_)
731            | SurfaceExpr::Lit(_)
732            | SurfaceExpr::Hole => self.print_expr(expr),
733            _ => {
734                write!(self.buffer, "(")?;
735                self.print_expr(expr)?;
736                write!(self.buffer, ")")
737            }
738        }
739    }
740    /// Pretty print a declaration.
741    pub fn print_decl(&mut self, decl: &Decl) -> fmt::Result {
742        match decl {
743            Decl::Axiom {
744                name,
745                univ_params,
746                ty,
747                ..
748            } => {
749                write!(self.buffer, "axiom {}", name)?;
750                if !univ_params.is_empty() {
751                    write!(self.buffer, " {{{}}}", univ_params.join(", "))?;
752                }
753                write!(self.buffer, " : ")?;
754                self.print_expr(&ty.value)
755            }
756            Decl::Definition {
757                name,
758                univ_params,
759                ty,
760                val,
761                ..
762            } => {
763                write!(self.buffer, "definition {}", name)?;
764                if !univ_params.is_empty() {
765                    write!(self.buffer, " {{{}}}", univ_params.join(", "))?;
766                }
767                if let Some(ty) = ty {
768                    write!(self.buffer, " : ")?;
769                    self.print_expr(&ty.value)?;
770                }
771                write!(self.buffer, " := ")?;
772                self.print_expr(&val.value)
773            }
774            Decl::Theorem {
775                name,
776                univ_params,
777                ty,
778                proof,
779                ..
780            } => {
781                write!(self.buffer, "theorem {}", name)?;
782                if !univ_params.is_empty() {
783                    write!(self.buffer, " {{{}}}", univ_params.join(", "))?;
784                }
785                write!(self.buffer, " : ")?;
786                self.print_expr(&ty.value)?;
787                write!(self.buffer, " := ")?;
788                self.print_expr(&proof.value)
789            }
790            Decl::Inductive {
791                name,
792                univ_params,
793                params,
794                ty,
795                ctors,
796                ..
797            } => self.print_inductive(name, univ_params, params, &ty.value, ctors),
798            Decl::Import { path } => write!(self.buffer, "import {}", path.join(".")),
799            Decl::Namespace { name, .. } => write!(self.buffer, "namespace {} ...", name),
800            Decl::Structure {
801                name,
802                univ_params,
803                extends,
804                fields,
805            } => self.print_structure(name, univ_params, extends, fields),
806            Decl::ClassDecl {
807                name,
808                univ_params,
809                extends,
810                fields,
811            } => self.print_class(name, univ_params, extends, fields),
812            Decl::InstanceDecl { class_name, .. } => {
813                write!(self.buffer, "instance {} ...", class_name)
814            }
815            Decl::SectionDecl { name, .. } => write!(self.buffer, "section {} ...", name),
816            Decl::Variable { binders } => {
817                write!(self.buffer, "variable")?;
818                for b in binders {
819                    self.print_binder_always(b)?;
820                }
821                Ok(())
822            }
823            Decl::Open { path, names } => {
824                write!(self.buffer, "open {}", path.join("."))?;
825                if !names.is_empty() {
826                    write!(self.buffer, " ({})", names.join(", "))?;
827                }
828                Ok(())
829            }
830            Decl::Attribute { attrs, decl } => {
831                write!(self.buffer, "@[{}] ", attrs.join(", "))?;
832                self.print_decl(&decl.value)
833            }
834            Decl::HashCmd { cmd, arg } => {
835                write!(self.buffer, "#{} ", cmd)?;
836                self.print_expr(&arg.value)
837            }
838            Decl::Mutual { decls } => {
839                write!(self.buffer, "mutual")?;
840                for d in decls {
841                    writeln!(self.buffer)?;
842                    self.print_decl(&d.value)?;
843                }
844                writeln!(self.buffer)?;
845                write!(self.buffer, "end")
846            }
847            Decl::Derive {
848                instances,
849                type_name,
850            } => {
851                write!(
852                    self.buffer,
853                    "deriving {} for {}",
854                    instances.join(", "),
855                    type_name
856                )
857            }
858            Decl::NotationDecl {
859                kind,
860                prec,
861                name,
862                notation,
863            } => {
864                write!(self.buffer, "{}", kind)?;
865                if let Some(p) = prec {
866                    write!(self.buffer, " {}", p)?;
867                }
868                write!(self.buffer, " {} := {}", name, notation)
869            }
870            Decl::Universe { names } => {
871                write!(self.buffer, "universe {}", names.join(" "))
872            }
873        }
874    }
875    /// Pretty print a structure declaration.
876    #[allow(dead_code)]
877    fn print_structure(
878        &mut self,
879        name: &str,
880        univ_params: &[String],
881        extends: &[String],
882        fields: &[FieldDecl],
883    ) -> fmt::Result {
884        write!(self.buffer, "structure {}", name)?;
885        if !univ_params.is_empty() {
886            write!(self.buffer, " {{{}}}", univ_params.join(", "))?;
887        }
888        if !extends.is_empty() {
889            write!(self.buffer, " extends {}", extends.join(", "))?;
890        }
891        write!(self.buffer, " where")?;
892        self.increase_indent();
893        for field in fields {
894            writeln!(self.buffer)?;
895            self.write_indent();
896            write!(self.buffer, "{} : ", field.name)?;
897            self.print_expr(&field.ty.value)?;
898            if let Some(default) = &field.default {
899                write!(self.buffer, " := ")?;
900                self.print_expr(&default.value)?;
901            }
902        }
903        self.decrease_indent();
904        Ok(())
905    }
906    /// Pretty print a class declaration.
907    #[allow(dead_code)]
908    fn print_class(
909        &mut self,
910        name: &str,
911        univ_params: &[String],
912        extends: &[String],
913        fields: &[FieldDecl],
914    ) -> fmt::Result {
915        write!(self.buffer, "class {}", name)?;
916        if !univ_params.is_empty() {
917            write!(self.buffer, " {{{}}}", univ_params.join(", "))?;
918        }
919        if !extends.is_empty() {
920            write!(self.buffer, " extends {}", extends.join(", "))?;
921        }
922        write!(self.buffer, " where")?;
923        self.increase_indent();
924        for field in fields {
925            writeln!(self.buffer)?;
926            self.write_indent();
927            write!(self.buffer, "{} : ", field.name)?;
928            self.print_expr(&field.ty.value)?;
929            if let Some(default) = &field.default {
930                write!(self.buffer, " := ")?;
931                self.print_expr(&default.value)?;
932            }
933        }
934        self.decrease_indent();
935        Ok(())
936    }
937}
938/// A simple indentation manager.
939#[allow(dead_code)]
940#[allow(missing_docs)]
941pub struct IndentManager {
942    /// Current indent level
943    pub level: usize,
944    /// Spaces per indent level
945    pub tab_width: usize,
946}
947impl IndentManager {
948    /// Create a new manager.
949    #[allow(dead_code)]
950    pub fn new(tab_width: usize) -> Self {
951        IndentManager {
952            level: 0,
953            tab_width,
954        }
955    }
956    /// Indent by one level.
957    #[allow(dead_code)]
958    pub fn indent(&mut self) {
959        self.level += 1;
960    }
961    /// Dedent by one level.
962    #[allow(dead_code)]
963    pub fn dedent(&mut self) {
964        if self.level > 0 {
965            self.level -= 1;
966        }
967    }
968    /// Returns the current indent string.
969    #[allow(dead_code)]
970    pub fn current(&self) -> String {
971        " ".repeat(self.level * self.tab_width)
972    }
973    /// Apply indentation to a multi-line string.
974    #[allow(dead_code)]
975    pub fn apply_to(&self, s: &str) -> String {
976        let prefix = self.current();
977        s.lines()
978            .map(|line| format!("{}{}", prefix, line))
979            .collect::<Vec<_>>()
980            .join("\n")
981    }
982}
983/// A breadcrumb trail for pretty-printing context.
984#[allow(dead_code)]
985#[allow(missing_docs)]
986pub struct BreadcrumbTrail {
987    /// Breadcrumb labels
988    pub crumbs: Vec<String>,
989}
990impl BreadcrumbTrail {
991    /// Create a new empty trail.
992    #[allow(dead_code)]
993    pub fn new() -> Self {
994        BreadcrumbTrail { crumbs: Vec::new() }
995    }
996    /// Push a crumb.
997    #[allow(dead_code)]
998    pub fn push(&mut self, label: &str) {
999        self.crumbs.push(label.to_string());
1000    }
1001    /// Pop the last crumb.
1002    #[allow(dead_code)]
1003    pub fn pop(&mut self) {
1004        self.crumbs.pop();
1005    }
1006    /// Format as a path string.
1007    #[allow(dead_code)]
1008    pub fn format(&self) -> String {
1009        self.crumbs.join(" > ")
1010    }
1011}
1012/// A ribbon formatter with line-break decisions.
1013#[allow(dead_code)]
1014#[allow(missing_docs)]
1015pub struct DocFormatter {
1016    /// Line width limit
1017    pub width: usize,
1018    /// Current column
1019    pub col: usize,
1020    /// Output buffer
1021    pub out: String,
1022}
1023impl DocFormatter {
1024    /// Create a new formatter.
1025    #[allow(dead_code)]
1026    pub fn new(width: usize) -> Self {
1027        DocFormatter {
1028            width,
1029            col: 0,
1030            out: String::new(),
1031        }
1032    }
1033    /// Write text.
1034    #[allow(dead_code)]
1035    pub fn write_text(&mut self, s: &str) {
1036        self.out.push_str(s);
1037        self.col += s.chars().count();
1038    }
1039    /// Write a newline with indent.
1040    #[allow(dead_code)]
1041    pub fn newline(&mut self, indent: usize) {
1042        self.out.push('\n');
1043        self.out.push_str(&" ".repeat(indent));
1044        self.col = indent;
1045    }
1046    /// Returns the current output.
1047    #[allow(dead_code)]
1048    pub fn finish(self) -> String {
1049        self.out
1050    }
1051}
1052/// A column-aligned table formatter.
1053#[allow(dead_code)]
1054#[allow(missing_docs)]
1055pub struct TableFormatter {
1056    /// Rows of the table
1057    pub rows: Vec<Vec<String>>,
1058    /// Column separator
1059    pub sep: String,
1060}
1061impl TableFormatter {
1062    /// Create a new table formatter.
1063    #[allow(dead_code)]
1064    pub fn new(sep: &str) -> Self {
1065        TableFormatter {
1066            rows: Vec::new(),
1067            sep: sep.to_string(),
1068        }
1069    }
1070    /// Add a row.
1071    #[allow(dead_code)]
1072    pub fn add_row(&mut self, row: Vec<&str>) {
1073        self.rows
1074            .push(row.into_iter().map(|s| s.to_string()).collect());
1075    }
1076    /// Compute column widths.
1077    #[allow(dead_code)]
1078    pub fn col_widths(&self) -> Vec<usize> {
1079        if self.rows.is_empty() {
1080            return Vec::new();
1081        }
1082        let ncols = self.rows.iter().map(|r| r.len()).max().unwrap_or(0);
1083        (0..ncols)
1084            .map(|c| {
1085                self.rows
1086                    .iter()
1087                    .filter_map(|r| r.get(c))
1088                    .map(|s| s.chars().count())
1089                    .max()
1090                    .unwrap_or(0)
1091            })
1092            .collect()
1093    }
1094    /// Render the table to a string.
1095    #[allow(dead_code)]
1096    pub fn render(&self) -> String {
1097        let widths = self.col_widths();
1098        let mut out = String::new();
1099        for row in &self.rows {
1100            let parts: Vec<String> = row
1101                .iter()
1102                .enumerate()
1103                .map(|(i, cell)| {
1104                    let w = widths.get(i).copied().unwrap_or(0);
1105                    format!("{:width$}", cell, width = w)
1106                })
1107                .collect();
1108            out.push_str(&parts.join(&self.sep));
1109            out.push('\n');
1110        }
1111        out
1112    }
1113}
1114/// A syntax highlighter that wraps tokens in ANSI escape codes.
1115#[allow(dead_code)]
1116#[allow(missing_docs)]
1117pub struct AnsiHighlighter;
1118impl AnsiHighlighter {
1119    const RESET: &'static str = "\x1b[0m";
1120    const BOLD: &'static str = "\x1b[1m";
1121    const RED: &'static str = "\x1b[31m";
1122    const GREEN: &'static str = "\x1b[32m";
1123    #[allow(dead_code)]
1124    const YELLOW: &'static str = "\x1b[33m";
1125    const BLUE: &'static str = "\x1b[34m";
1126    /// Highlight a keyword.
1127    #[allow(dead_code)]
1128    pub fn keyword(s: &str) -> String {
1129        format!("{}{}{}", Self::BOLD, s, Self::RESET)
1130    }
1131    /// Highlight an error.
1132    #[allow(dead_code)]
1133    pub fn error(s: &str) -> String {
1134        format!("{}{}{}", Self::RED, s, Self::RESET)
1135    }
1136    /// Highlight a literal.
1137    #[allow(dead_code)]
1138    pub fn literal(s: &str) -> String {
1139        format!("{}{}{}", Self::GREEN, s, Self::RESET)
1140    }
1141    /// Highlight a type.
1142    #[allow(dead_code)]
1143    pub fn type_name(s: &str) -> String {
1144        format!("{}{}{}", Self::BLUE, s, Self::RESET)
1145    }
1146    /// Strip ANSI escape codes from a string.
1147    #[allow(dead_code)]
1148    pub fn strip_ansi(s: &str) -> String {
1149        let mut result = String::new();
1150        let mut in_escape = false;
1151        for c in s.chars() {
1152            if c == '\x1b' {
1153                in_escape = true;
1154            } else if in_escape {
1155                if c == 'm' {
1156                    in_escape = false;
1157                }
1158            } else {
1159                result.push(c);
1160            }
1161        }
1162        result
1163    }
1164}
1165/// A box model for aligned output.
1166#[allow(dead_code)]
1167#[allow(missing_docs)]
1168#[derive(Debug, Clone)]
1169pub struct BoxModel {
1170    /// Width of this box
1171    pub width: usize,
1172    /// Lines of content
1173    pub lines: Vec<String>,
1174}
1175impl BoxModel {
1176    /// Create an empty box.
1177    #[allow(dead_code)]
1178    pub fn empty() -> Self {
1179        BoxModel {
1180            width: 0,
1181            lines: Vec::new(),
1182        }
1183    }
1184    /// Create a box from a single string.
1185    #[allow(dead_code)]
1186    pub fn of_str(s: &str) -> Self {
1187        let width = s.chars().count();
1188        BoxModel {
1189            width,
1190            lines: vec![s.to_string()],
1191        }
1192    }
1193    /// Stack two boxes vertically.
1194    #[allow(dead_code)]
1195    pub fn vstack(mut self, other: BoxModel) -> Self {
1196        self.width = self.width.max(other.width);
1197        self.lines.extend(other.lines);
1198        self
1199    }
1200    /// Place two boxes side by side.
1201    #[allow(dead_code)]
1202    pub fn hstack(self, other: BoxModel) -> Self {
1203        let h = self.lines.len().max(other.lines.len());
1204        let lw = self.width;
1205        let mut lines = Vec::new();
1206        for i in 0..h {
1207            let l = self.lines.get(i).cloned().unwrap_or_else(|| " ".repeat(lw));
1208            let r = other.lines.get(i).cloned().unwrap_or_default();
1209            let padded = format!("{:width$}{}", l, r, width = lw);
1210            lines.push(padded);
1211        }
1212        BoxModel {
1213            width: lw + other.width,
1214            lines,
1215        }
1216    }
1217    /// Render to a string.
1218    #[allow(dead_code)]
1219    pub fn render(&self) -> String {
1220        self.lines.join("\n")
1221    }
1222}
1223/// A document algebra node.
1224#[allow(dead_code)]
1225#[allow(missing_docs)]
1226#[derive(Debug, Clone)]
1227pub enum DocNode {
1228    /// Empty document
1229    Empty,
1230    /// A text string
1231    Text(String),
1232    /// A newline followed by indentation
1233    Line(usize),
1234    /// Horizontal concatenation
1235    Cat(Box<DocNode>, Box<DocNode>),
1236    /// Nested indentation
1237    Indent(usize, Box<DocNode>),
1238    /// A group that prefers to be on one line
1239    Group(Box<DocNode>),
1240}
1241impl DocNode {
1242    /// Create a text node.
1243    #[allow(dead_code)]
1244    pub fn text(s: &str) -> Self {
1245        DocNode::Text(s.to_string())
1246    }
1247    /// Create a line break with indent level.
1248    #[allow(dead_code)]
1249    pub fn line(indent: usize) -> Self {
1250        DocNode::Line(indent)
1251    }
1252    /// Concatenate two docs.
1253    #[allow(dead_code)]
1254    pub fn cat(a: DocNode, b: DocNode) -> Self {
1255        DocNode::Cat(Box::new(a), Box::new(b))
1256    }
1257    /// Indent a document.
1258    #[allow(dead_code)]
1259    pub fn indent(n: usize, doc: DocNode) -> Self {
1260        DocNode::Indent(n, Box::new(doc))
1261    }
1262    /// Group a document.
1263    #[allow(dead_code)]
1264    pub fn group(doc: DocNode) -> Self {
1265        DocNode::Group(Box::new(doc))
1266    }
1267    /// Render the document to a string (simplified: ignores group optimization).
1268    #[allow(dead_code)]
1269    pub fn render(&self, width: usize) -> String {
1270        let mut out = String::new();
1271        render_doc(self, 0, width, &mut out);
1272        out
1273    }
1274}
oxilean_parse/prettyprint/types.rs

oxilean_parse/prettyprint/
types.rs
