lemma/
ast.rs

1//! AST infrastructure types
2//!
3//! This module contains metadata types used throughout the parser and compiler:
4//! - `Span` for tracking source code locations
5//! - `ExpressionId` for uniquely identifying AST nodes
6//! - `ExpressionIdGenerator` for generating unique IDs during parsing
7
8use std::fmt;
9
10/// Span representing a location in source code
11#[derive(Debug, Clone, PartialEq, Eq, Hash)]
12pub struct Span {
13    pub start: usize,
14    pub end: usize,
15    pub line: usize,
16    pub col: usize,
17}
18
19impl Span {
20    pub fn from_pest_span(span: pest::Span) -> Self {
21        let (line, col) = span.start_pos().line_col();
22        Self {
23            start: span.start(),
24            end: span.end(),
25            line,
26            col,
27        }
28    }
29}
30
31/// Unique identifier for each expression in the AST
32#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
33pub struct ExpressionId(u64);
34
35impl ExpressionId {
36    pub fn new(id: u64) -> Self {
37        Self(id)
38    }
39}
40
41impl fmt::Display for ExpressionId {
42    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
43        write!(f, "expr_{}", self.0)
44    }
45}
46
47/// Counter for generating unique expression IDs
48pub struct ExpressionIdGenerator {
49    next_id: u64,
50    depth: usize,
51    max_depth: usize,
52}
53
54impl ExpressionIdGenerator {
55    pub fn new() -> Self {
56        Self::default()
57    }
58
59    pub fn with_max_depth(max_depth: usize) -> Self {
60        Self {
61            next_id: 0,
62            depth: 0,
63            max_depth,
64        }
65    }
66
67    pub fn next_id(&mut self) -> ExpressionId {
68        let id = ExpressionId(self.next_id);
69        self.next_id += 1;
70        id
71    }
72
73    pub fn push_depth(&mut self) -> Result<(), String> {
74        self.depth += 1;
75        if self.depth > self.max_depth {
76            return Err(format!(
77                "Expression depth {} exceeds maximum of {}",
78                self.depth, self.max_depth
79            ));
80        }
81        Ok(())
82    }
83
84    pub fn pop_depth(&mut self) {
85        if self.depth > 0 {
86            self.depth -= 1;
87        }
88    }
89
90    pub fn max_depth(&self) -> usize {
91        self.max_depth
92    }
93}
94
95impl Default for ExpressionIdGenerator {
96    fn default() -> Self {
97        Self {
98            next_id: 0,
99            depth: 0,
100            max_depth: 100, // Default limit
101        }
102    }
103}
lemma/ast.rs

lemma/
ast.rs
