proof_engine/symbolic/
typeset.rs

1//! Mathematical typesetting — render equations as positioned glyphs with proper notation.
2
3use super::expr::Expr;
4use glam::{Vec2, Vec4};
5
6/// A positioned glyph for mathematical typesetting.
7#[derive(Debug, Clone)]
8pub struct MathGlyph {
9    pub character: char,
10    pub position: Vec2,
11    pub scale: f32,
12    pub color: Vec4,
13}
14
15/// A typeset expression ready for rendering.
16#[derive(Debug, Clone)]
17pub struct TypesetExpr {
18    pub glyphs: Vec<MathGlyph>,
19    pub width: f32,
20    pub height: f32,
21    pub baseline: f32,
22}
23
24impl TypesetExpr {
25    /// Typeset an expression starting at the given position.
26    pub fn layout(expr: &Expr, start: Vec2, base_scale: f32, color: Vec4) -> Self {
27        let mut glyphs = Vec::new();
28        let mut cursor = start;
29        let bounds = layout_expr(expr, &mut cursor, base_scale, color, &mut glyphs, 0);
30        Self {
31            glyphs,
32            width: bounds.0,
33            height: bounds.1,
34            baseline: start.y,
35        }
36    }
37}
38
39fn layout_expr(
40    expr: &Expr, cursor: &mut Vec2, scale: f32, color: Vec4,
41    glyphs: &mut Vec<MathGlyph>, depth: u32,
42) -> (f32, f32) {
43    let start_x = cursor.x;
44    let char_w = scale * 0.6;
45    let char_h = scale;
46
47    match expr {
48        Expr::Const(v) => {
49            let s = if v.fract() == 0.0 && v.abs() < 1e12 { format!("{}", *v as i64) } else { format!("{v:.2}") };
50            for ch in s.chars() {
51                glyphs.push(MathGlyph { character: ch, position: *cursor, scale, color });
52                cursor.x += char_w;
53            }
54        }
55        Expr::Var(name) => {
56            for ch in name.chars() {
57                glyphs.push(MathGlyph { character: ch, position: *cursor, scale, color });
58                cursor.x += char_w;
59            }
60        }
61        Expr::Add(a, b) => {
62            layout_expr(a, cursor, scale, color, glyphs, depth);
63            push_char('+', cursor, char_w, scale, color, glyphs);
64            layout_expr(b, cursor, scale, color, glyphs, depth);
65        }
66        Expr::Sub(a, b) => {
67            layout_expr(a, cursor, scale, color, glyphs, depth);
68            push_char('-', cursor, char_w, scale, color, glyphs);
69            layout_expr(b, cursor, scale, color, glyphs, depth);
70        }
71        Expr::Mul(a, b) => {
72            let needs_parens_a = matches!(**a, Expr::Add(_, _) | Expr::Sub(_, _));
73            let needs_parens_b = matches!(**b, Expr::Add(_, _) | Expr::Sub(_, _));
74            if needs_parens_a { push_char('(', cursor, char_w, scale, color, glyphs); }
75            layout_expr(a, cursor, scale, color, glyphs, depth);
76            if needs_parens_a { push_char(')', cursor, char_w, scale, color, glyphs); }
77            push_char('·', cursor, char_w, scale, color, glyphs);
78            if needs_parens_b { push_char('(', cursor, char_w, scale, color, glyphs); }
79            layout_expr(b, cursor, scale, color, glyphs, depth);
80            if needs_parens_b { push_char(')', cursor, char_w, scale, color, glyphs); }
81        }
82        Expr::Div(a, b) => {
83            // Fraction: numerator above, line, denominator below
84            let frac_scale = scale * 0.8;
85            let num_y = cursor.y + char_h * 0.5;
86            let den_y = cursor.y - char_h * 0.5;
87            let save_x = cursor.x;
88
89            let mut num_cursor = Vec2::new(cursor.x, num_y);
90            layout_expr(a, &mut num_cursor, frac_scale, color, glyphs, depth + 1);
91            let num_width = num_cursor.x - save_x;
92
93            let mut den_cursor = Vec2::new(cursor.x, den_y);
94            layout_expr(b, &mut den_cursor, frac_scale, color, glyphs, depth + 1);
95            let den_width = den_cursor.x - save_x;
96
97            // Fraction line
98            let line_width = num_width.max(den_width);
99            let line_y = cursor.y;
100            for i in 0..(line_width / (char_w * 0.5)).ceil() as usize {
101                glyphs.push(MathGlyph {
102                    character: '─',
103                    position: Vec2::new(save_x + i as f32 * char_w * 0.5, line_y),
104                    scale: frac_scale,
105                    color,
106                });
107            }
108            cursor.x = save_x + line_width + char_w * 0.3;
109        }
110        Expr::Pow(base, exp) => {
111            layout_expr(base, cursor, scale, color, glyphs, depth);
112            // Superscript
113            let exp_scale = scale * 0.6;
114            let exp_y = cursor.y + char_h * 0.5;
115            let mut exp_cursor = Vec2::new(cursor.x, exp_y);
116            layout_expr(exp, &mut exp_cursor, exp_scale, color, glyphs, depth + 1);
117            cursor.x = exp_cursor.x;
118        }
119        Expr::Sqrt(a) => {
120            push_char('√', cursor, char_w, scale, color, glyphs);
121            push_char('(', cursor, char_w, scale, color, glyphs);
122            layout_expr(a, cursor, scale, color, glyphs, depth);
123            push_char(')', cursor, char_w, scale, color, glyphs);
124        }
125        Expr::Sin(a) => { push_str("sin", cursor, char_w, scale, color, glyphs); push_char('(', cursor, char_w, scale, color, glyphs); layout_expr(a, cursor, scale, color, glyphs, depth); push_char(')', cursor, char_w, scale, color, glyphs); }
126        Expr::Cos(a) => { push_str("cos", cursor, char_w, scale, color, glyphs); push_char('(', cursor, char_w, scale, color, glyphs); layout_expr(a, cursor, scale, color, glyphs, depth); push_char(')', cursor, char_w, scale, color, glyphs); }
127        Expr::Tan(a) => { push_str("tan", cursor, char_w, scale, color, glyphs); push_char('(', cursor, char_w, scale, color, glyphs); layout_expr(a, cursor, scale, color, glyphs, depth); push_char(')', cursor, char_w, scale, color, glyphs); }
128        Expr::Ln(a) => { push_str("ln", cursor, char_w, scale, color, glyphs); push_char('(', cursor, char_w, scale, color, glyphs); layout_expr(a, cursor, scale, color, glyphs, depth); push_char(')', cursor, char_w, scale, color, glyphs); }
129        Expr::Exp(a) => { push_char('e', cursor, char_w, scale, color, glyphs); let mut sc = Vec2::new(cursor.x, cursor.y + char_h * 0.5); layout_expr(a, &mut sc, scale * 0.6, color, glyphs, depth + 1); cursor.x = sc.x; }
130        Expr::Neg(a) => { push_char('-', cursor, char_w, scale, color, glyphs); layout_expr(a, cursor, scale, color, glyphs, depth); }
131        Expr::Sum { body, var, from, to } => {
132            push_char('Σ', cursor, char_w * 1.5, scale * 1.3, color, glyphs);
133            layout_expr(body, cursor, scale, color, glyphs, depth);
134        }
135        Expr::Integral { body, var } => {
136            push_char('∫', cursor, char_w * 1.2, scale * 1.3, color, glyphs);
137            layout_expr(body, cursor, scale, color, glyphs, depth);
138            push_str(&format!("d{var}"), cursor, char_w, scale * 0.8, color, glyphs);
139        }
140        _ => {
141            let s = format!("{expr}");
142            push_str(&s, cursor, char_w, scale, color, glyphs);
143        }
144    }
145
146    let width = cursor.x - start_x;
147    (width, char_h)
148}
149
150fn push_char(ch: char, cursor: &mut Vec2, char_w: f32, scale: f32, color: Vec4, glyphs: &mut Vec<MathGlyph>) {
151    glyphs.push(MathGlyph { character: ch, position: *cursor, scale, color });
152    cursor.x += char_w;
153}
154
155fn push_str(s: &str, cursor: &mut Vec2, char_w: f32, scale: f32, color: Vec4, glyphs: &mut Vec<MathGlyph>) {
156    for ch in s.chars() {
157        push_char(ch, cursor, char_w, scale, color, glyphs);
158    }
159}
160
161#[cfg(test)]
162mod tests {
163    use super::*;
164
165    #[test]
166    fn typeset_simple_expr() {
167        let expr = Expr::var("x").pow(Expr::c(2.0)).add(Expr::c(1.0));
168        let ts = TypesetExpr::layout(&expr, Vec2::ZERO, 1.0, Vec4::ONE);
169        assert!(!ts.glyphs.is_empty());
170        assert!(ts.width > 0.0);
171    }
172
173    #[test]
174    fn typeset_fraction() {
175        let expr = Expr::var("x").div(Expr::var("y"));
176        let ts = TypesetExpr::layout(&expr, Vec2::ZERO, 1.0, Vec4::ONE);
177        assert!(ts.glyphs.len() >= 2); // at least x, y, and fraction line
178    }
179
180    #[test]
181    fn typeset_trig() {
182        let expr = Expr::var("x").sin();
183        let ts = TypesetExpr::layout(&expr, Vec2::ZERO, 1.0, Vec4::ONE);
184        let chars: Vec<char> = ts.glyphs.iter().map(|g| g.character).collect();
185        assert!(chars.contains(&'s'));
186    }
187}
proof_engine/symbolic/typeset.rs

proof_engine/symbolic/
typeset.rs
