oxilean_parse/ast/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6
7/// A combined source span holding both line-column positions and byte offsets.
8#[derive(Clone, Copy, Debug, PartialEq, Eq)]
9pub struct Span {
10    /// Start position (line/col).
11    pub start: Pos,
12    /// End position (line/col).
13    pub end: Pos,
14    /// Byte range.
15    pub bytes: ByteRange,
16}
17impl Span {
18    /// Construct a span from positions and byte offsets.
19    pub fn new(start: Pos, end: Pos, bytes: ByteRange) -> Self {
20        Self { start, end, bytes }
21    }
22    /// A dummy span at start-of-file.
23    pub fn dummy() -> Self {
24        Self {
25            start: Pos::start(),
26            end: Pos::start(),
27            bytes: ByteRange::empty(),
28        }
29    }
30    /// Merge two spans into the smallest enclosing span.
31    pub fn union(self, other: Span) -> Span {
32        Span {
33            start: if self.start.is_before(&other.start) {
34                self.start
35            } else {
36                other.start
37            },
38            end: if other.end.is_before(&self.end) {
39                self.end
40            } else {
41                other.end
42            },
43            bytes: self.bytes.union(other.bytes),
44        }
45    }
46    /// Whether the byte range is non-empty.
47    pub fn is_non_empty(&self) -> bool {
48        !self.bytes.is_empty()
49    }
50}
51/// A binder in a telescope (a sequence of bound variables).
52#[allow(dead_code)]
53#[allow(missing_docs)]
54#[derive(Debug, Clone)]
55pub struct BinderExtExt2 {
56    /// Variable name
57    pub name: String,
58    /// Type annotation (as string)
59    pub ty: Option<String>,
60    /// Whether the binder is implicit
61    pub implicit: bool,
62}
63impl BinderExtExt2 {
64    /// Create an explicit binder.
65    #[allow(dead_code)]
66    pub fn explicit(name: &str, ty: Option<&str>) -> Self {
67        BinderExtExt2 {
68            name: name.to_string(),
69            ty: ty.map(|s| s.to_string()),
70            implicit: false,
71        }
72    }
73    /// Create an implicit binder.
74    #[allow(dead_code)]
75    pub fn implicit(name: &str, ty: Option<&str>) -> Self {
76        BinderExtExt2 {
77            name: name.to_string(),
78            ty: ty.map(|s| s.to_string()),
79            implicit: true,
80        }
81    }
82    /// Format as "(name : ty)" or "(name)".
83    #[allow(dead_code)]
84    pub fn format(&self) -> String {
85        let brackets = if self.implicit {
86            ("{", "}")
87        } else {
88            ("(", ")")
89        };
90        match &self.ty {
91            Some(t) => format!("{}{} : {}{}", brackets.0, self.name, t, brackets.1),
92            None => format!("{}{}{}", brackets.0, self.name, brackets.1),
93        }
94    }
95}
96/// A record of a macro invocation and its expansion.
97#[derive(Clone, Debug)]
98pub struct MacroExpansion {
99    /// Name of the macro invoked.
100    pub macro_name: String,
101    /// Source span of the invocation.
102    pub span: ByteRange,
103    /// Number of expansion steps taken.
104    pub expansion_steps: u32,
105}
106impl MacroExpansion {
107    /// Create a macro expansion record.
108    pub fn new(macro_name: impl Into<String>, span: ByteRange) -> Self {
109        Self {
110            macro_name: macro_name.into(),
111            span,
112            expansion_steps: 0,
113        }
114    }
115    /// Increment expansion step count.
116    pub fn increment(&mut self) {
117        self.expansion_steps += 1;
118    }
119    /// Whether the expansion is considered deep (> 10 steps).
120    pub fn is_deep(&self) -> bool {
121        self.expansion_steps > 10
122    }
123}
124/// Fixity of an operator notation.
125#[derive(Clone, Copy, Debug, PartialEq, Eq)]
126pub enum Fixity {
127    /// Left-associative infix operator (e.g., `+`).
128    InfixLeft,
129    /// Right-associative infix operator (e.g., `^`).
130    InfixRight,
131    /// Non-associative infix operator.
132    Infix,
133    /// Prefix operator (e.g., `-`).
134    Prefix,
135    /// Postfix operator.
136    Postfix,
137}
138/// A line-column source position (1-based).
139#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
140pub struct Pos {
141    /// 1-based line number.
142    pub line: u32,
143    /// 1-based column number (in bytes from line start).
144    pub col: u32,
145}
146impl Pos {
147    /// Create a position.
148    pub fn new(line: u32, col: u32) -> Self {
149        Self { line, col }
150    }
151    /// The start-of-file position (line 1, col 1).
152    pub fn start() -> Self {
153        Self { line: 1, col: 1 }
154    }
155    /// Advance to the next column.
156    pub fn next_col(self) -> Self {
157        Self {
158            col: self.col + 1,
159            ..self
160        }
161    }
162    /// Advance to the next line (resets column to 1).
163    pub fn next_line(self) -> Self {
164        Self {
165            line: self.line + 1,
166            col: 1,
167        }
168    }
169    /// Whether this position comes before `other`.
170    pub fn is_before(&self, other: &Pos) -> bool {
171        (self.line, self.col) < (other.line, other.col)
172    }
173}
174/// A half-open byte range `[start, end)` in the source text.
175#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
176pub struct ByteRange {
177    /// Inclusive start byte offset.
178    pub start: usize,
179    /// Exclusive end byte offset.
180    pub end: usize,
181}
182impl ByteRange {
183    /// Create a byte range.
184    pub fn new(start: usize, end: usize) -> Self {
185        assert!(start <= end, "ByteRange: start > end");
186        Self { start, end }
187    }
188    /// The empty range at offset 0.
189    pub fn empty() -> Self {
190        Self { start: 0, end: 0 }
191    }
192    /// Length of the range in bytes.
193    pub fn len(&self) -> usize {
194        self.end - self.start
195    }
196    /// Whether the range is empty.
197    pub fn is_empty(&self) -> bool {
198        self.start == self.end
199    }
200    /// Merge two ranges into the smallest containing range.
201    pub fn union(self, other: ByteRange) -> ByteRange {
202        ByteRange {
203            start: self.start.min(other.start),
204            end: self.end.max(other.end),
205        }
206    }
207    /// Whether this range contains a byte offset.
208    pub fn contains(&self, offset: usize) -> bool {
209        offset >= self.start && offset < self.end
210    }
211    /// Extract the covered slice from a source string.
212    pub fn slice<'a>(&self, src: &'a str) -> &'a str {
213        &src[self.start..self.end]
214    }
215}
216/// A simple expression complexity metric.
217#[allow(dead_code)]
218#[allow(missing_docs)]
219pub struct ComplexityMetric {
220    /// Weight for each application
221    pub app_weight: u32,
222    /// Weight for each lambda
223    pub lam_weight: u32,
224    /// Weight for each leaf
225    pub leaf_weight: u32,
226}
227impl ComplexityMetric {
228    /// Create a default metric.
229    #[allow(dead_code)]
230    pub fn default_metric() -> Self {
231        ComplexityMetric {
232            app_weight: 2,
233            lam_weight: 3,
234            leaf_weight: 1,
235        }
236    }
237    /// Compute the complexity of a tree node.
238    #[allow(dead_code)]
239    pub fn compute(&self, node: &TreeNodeExt) -> u32 {
240        match node.kind {
241            SimpleNodeKindExt::Leaf => self.leaf_weight,
242            SimpleNodeKindExt::App => {
243                self.app_weight + node.children.iter().map(|c| self.compute(c)).sum::<u32>()
244            }
245            SimpleNodeKindExt::Lam => {
246                self.lam_weight + node.children.iter().map(|c| self.compute(c)).sum::<u32>()
247            }
248            _ => 1 + node.children.iter().map(|c| self.compute(c)).sum::<u32>(),
249        }
250    }
251}
252/// Metadata attached to an AST node during parsing or elaboration.
253#[derive(Clone, Debug, Default)]
254pub struct AstMetadata {
255    /// Source span of the node.
256    pub span: Option<ByteRange>,
257    /// Elaboration-time type annotation (stringified).
258    pub type_hint: Option<String>,
259    /// Whether this node was synthesized (not from real source).
260    pub synthetic: bool,
261    /// Arbitrary string tags for tooling.
262    pub tags: Vec<String>,
263}
264impl AstMetadata {
265    /// Create empty metadata.
266    pub fn empty() -> Self {
267        Self::default()
268    }
269    /// Create metadata with a span.
270    pub fn with_span(span: ByteRange) -> Self {
271        Self {
272            span: Some(span),
273            ..Default::default()
274        }
275    }
276    /// Mark as synthetic.
277    pub fn synthetic() -> Self {
278        Self {
279            synthetic: true,
280            ..Default::default()
281        }
282    }
283    /// Add a tag.
284    pub fn add_tag(&mut self, tag: impl Into<String>) {
285        self.tags.push(tag.into());
286    }
287    /// Whether a tag is present.
288    pub fn has_tag(&self, tag: &str) -> bool {
289        self.tags.iter().any(|t| t == tag)
290    }
291}
292/// An import declaration (`import Foo.Bar`).
293#[derive(Clone, Debug, PartialEq, Eq)]
294pub struct ImportDecl {
295    /// Dotted module path (e.g., `["Foo", "Bar"]`).
296    pub path: Vec<String>,
297    /// Source span.
298    pub span: ByteRange,
299}
300impl ImportDecl {
301    /// Create an import declaration.
302    pub fn new(path: Vec<String>, span: ByteRange) -> Self {
303        Self { path, span }
304    }
305    /// The module path as a dotted string (e.g., `"Foo.Bar"`).
306    pub fn dotted_path(&self) -> String {
307        self.path.join(".")
308    }
309    /// Whether the import is for a root module (single component).
310    pub fn is_root(&self) -> bool {
311        self.path.len() == 1
312    }
313}
314/// A registry of notation entries indexed by symbol.
315#[derive(Clone, Debug, Default)]
316pub struct OperatorTable {
317    /// All registered entries.
318    entries: Vec<NotationEntry>,
319}
320impl OperatorTable {
321    /// Create an empty table.
322    pub fn new() -> Self {
323        Self::default()
324    }
325    /// Register a notation entry.
326    pub fn register(&mut self, entry: NotationEntry) {
327        self.entries.push(entry);
328    }
329    /// Look up entries for a given symbol.
330    pub fn lookup(&self, symbol: &str) -> Vec<&NotationEntry> {
331        self.entries.iter().filter(|e| e.symbol == symbol).collect()
332    }
333    /// Number of registered entries.
334    pub fn len(&self) -> usize {
335        self.entries.len()
336    }
337    /// Whether the table is empty.
338    pub fn is_empty(&self) -> bool {
339        self.entries.is_empty()
340    }
341    /// Infix entries.
342    pub fn infix_entries(&self) -> Vec<&NotationEntry> {
343        self.entries.iter().filter(|e| e.is_infix()).collect()
344    }
345}
346/// A binder for a pi type or lambda.
347#[allow(dead_code)]
348#[allow(missing_docs)]
349#[derive(Debug, Clone)]
350pub struct BinderExt {
351    /// Variable name
352    pub name: String,
353    /// Type annotation (optional)
354    pub ty: Option<String>,
355    /// Whether this is implicit
356    pub implicit: bool,
357}
358impl BinderExt {
359    /// Create an explicit binder.
360    #[allow(dead_code)]
361    pub fn explicit(name: &str, ty: Option<&str>) -> Self {
362        BinderExt {
363            name: name.to_string(),
364            ty: ty.map(|s| s.to_string()),
365            implicit: false,
366        }
367    }
368    /// Create an implicit binder.
369    #[allow(dead_code)]
370    pub fn implicit(name: &str, ty: Option<&str>) -> Self {
371        BinderExt {
372            name: name.to_string(),
373            ty: ty.map(|s| s.to_string()),
374            implicit: true,
375        }
376    }
377    /// Format the binder.
378    #[allow(dead_code)]
379    pub fn format(&self) -> String {
380        let inner = if let Some(ref ty) = self.ty {
381            format!("{} : {}", self.name, ty)
382        } else {
383            self.name.clone()
384        };
385        if self.implicit {
386            format!("{{{}}}", inner)
387        } else {
388            format!("({})", inner)
389        }
390    }
391}
392/// A let binding in an expression.
393#[allow(dead_code)]
394#[allow(missing_docs)]
395#[derive(Debug, Clone)]
396pub struct LetBindingExtExt2 {
397    /// Name of the bound variable
398    pub name: String,
399    /// Optional type annotation
400    pub ty: Option<String>,
401    /// The value being bound
402    pub value: String,
403    /// The body of the let expression
404    pub body: String,
405}
406impl LetBindingExtExt2 {
407    /// Create a new let binding.
408    #[allow(dead_code)]
409    pub fn new(name: &str, ty: Option<&str>, value: &str, body: &str) -> Self {
410        LetBindingExtExt2 {
411            name: name.to_string(),
412            ty: ty.map(|s| s.to_string()),
413            value: value.to_string(),
414            body: body.to_string(),
415        }
416    }
417    /// Format as "let name := value; body".
418    #[allow(dead_code)]
419    pub fn format(&self) -> String {
420        match &self.ty {
421            Some(t) => {
422                format!("let {} : {} := {}; {}", self.name, t, self.value, self.body)
423            }
424            None => format!("let {} := {}; {}", self.name, self.value, self.body),
425        }
426    }
427}
428/// A type annotation node for the AST.
429#[allow(dead_code)]
430#[allow(missing_docs)]
431#[derive(Debug, Clone)]
432pub struct TypeAnnotation {
433    /// The expression being annotated
434    pub expr: String,
435    /// The type annotation
436    pub ty: String,
437}
438impl TypeAnnotation {
439    /// Create a new type annotation.
440    #[allow(dead_code)]
441    pub fn new(expr: &str, ty: &str) -> Self {
442        TypeAnnotation {
443            expr: expr.to_string(),
444            ty: ty.to_string(),
445        }
446    }
447    /// Format as "(expr : ty)".
448    #[allow(dead_code)]
449    pub fn format(&self) -> String {
450        format!("({} : {})", self.expr, self.ty)
451    }
452}
453/// A universe level expression (Lean 4 style).
454#[allow(dead_code)]
455#[allow(missing_docs)]
456#[derive(Debug, Clone, PartialEq, Eq)]
457pub enum UniverseLevel {
458    /// Universe 0 (Prop)
459    Zero,
460    /// Successor of a universe
461    Succ(Box<UniverseLevel>),
462    /// Maximum of two universes
463    Max(Box<UniverseLevel>, Box<UniverseLevel>),
464    /// A universe variable
465    Var(String),
466}
467impl UniverseLevel {
468    /// Returns the concrete level as a number, if possible.
469    #[allow(dead_code)]
470    pub fn concrete(&self) -> Option<usize> {
471        match self {
472            UniverseLevel::Zero => Some(0),
473            UniverseLevel::Succ(inner) => inner.concrete().map(|n| n + 1),
474            UniverseLevel::Max(a, b) => {
475                let ca = a.concrete()?;
476                let cb = b.concrete()?;
477                Some(ca.max(cb))
478            }
479            UniverseLevel::Var(_) => None,
480        }
481    }
482}
483/// An argument to an attribute annotation.
484#[derive(Clone, Debug, PartialEq)]
485pub enum AttrArg {
486    /// Identifier argument.
487    Ident(String),
488    /// Numeric argument.
489    Num(i64),
490    /// String argument.
491    Str(String),
492    /// List of arguments.
493    List(Vec<AttrArg>),
494}
495impl AttrArg {
496    /// Create an identifier attribute argument.
497    pub fn ident(s: &str) -> Self {
498        AttrArg::Ident(s.to_string())
499    }
500    /// Create a numeric attribute argument.
501    pub fn num(n: i64) -> Self {
502        AttrArg::Num(n)
503    }
504    /// Create a string attribute argument.
505    pub fn str_arg(s: &str) -> Self {
506        AttrArg::Str(s.to_string())
507    }
508    /// As an ident string, if this is an Ident.
509    pub fn as_ident(&self) -> Option<&str> {
510        match self {
511            AttrArg::Ident(s) => Some(s),
512            _ => None,
513        }
514    }
515    /// As a number, if this is a Num.
516    pub fn as_num(&self) -> Option<i64> {
517        match self {
518            AttrArg::Num(n) => Some(*n),
519            _ => None,
520        }
521    }
522}
523/// A registered notation (operator or mixfix).
524#[derive(Clone, Debug)]
525pub struct NotationEntry {
526    /// The notation symbol string (e.g., `+`).
527    pub symbol: String,
528    /// Associated declaration name.
529    pub decl_name: String,
530    /// Fixity and associativity.
531    pub fixity: Fixity,
532    /// Binding precedence.
533    pub prec: Prec,
534    /// Whether the notation is deprecated.
535    pub deprecated: bool,
536}
537impl NotationEntry {
538    /// Create a new notation entry.
539    pub fn new(symbol: &str, decl_name: &str, fixity: Fixity, prec: Prec) -> Self {
540        Self {
541            symbol: symbol.to_string(),
542            decl_name: decl_name.to_string(),
543            fixity,
544            prec,
545            deprecated: false,
546        }
547    }
548    /// Mark this notation as deprecated.
549    pub fn deprecated(mut self) -> Self {
550        self.deprecated = true;
551        self
552    }
553    /// Whether this is an infix notation.
554    pub fn is_infix(&self) -> bool {
555        matches!(
556            self.fixity,
557            Fixity::InfixLeft | Fixity::InfixRight | Fixity::Infix
558        )
559    }
560}
561/// A simple AST node kind for generic traversal.
562#[allow(dead_code)]
563#[allow(missing_docs)]
564#[derive(Debug, Clone, PartialEq, Eq, Hash)]
565pub enum SimpleNodeKindExt {
566    /// A leaf node (variable, literal)
567    Leaf,
568    /// An application node
569    App,
570    /// A lambda abstraction
571    Lam,
572    /// A pi-type / forall
573    Pi,
574    /// A let binding
575    Let,
576    /// A sort (Type/Prop)
577    Sort,
578    /// A match expression
579    Match,
580    /// A definition head
581    Def,
582    /// A theorem head
583    Theorem,
584    /// An annotation
585    Ann,
586    /// A projection
587    Proj,
588    /// A universe level
589    Level,
590}
591/// A let-binding surface expression.
592#[allow(dead_code)]
593#[allow(missing_docs)]
594#[derive(Debug, Clone)]
595pub struct LetBindingExt {
596    /// Variable name
597    pub name: String,
598    /// Optional type annotation
599    pub ty: Option<String>,
600    /// The value expression (as string)
601    pub value: String,
602    /// The body expression (as string)
603    pub body: String,
604}
605impl LetBindingExt {
606    /// Create a new let binding.
607    #[allow(dead_code)]
608    pub fn new(name: &str, value: &str, body: &str) -> Self {
609        LetBindingExt {
610            name: name.to_string(),
611            ty: None,
612            value: value.to_string(),
613            body: body.to_string(),
614        }
615    }
616    /// Add a type annotation.
617    #[allow(dead_code)]
618    pub fn with_ty(mut self, ty: &str) -> Self {
619        self.ty = Some(ty.to_string());
620        self
621    }
622    /// Format as "let name : ty := value; body" or "let name := value; body".
623    #[allow(dead_code)]
624    pub fn format(&self) -> String {
625        if let Some(ref ty) = self.ty {
626            format!(
627                "let {} : {} := {} in {}",
628                self.name, ty, self.value, self.body
629            )
630        } else {
631            format!("let {} := {} in {}", self.name, self.value, self.body)
632        }
633    }
634}
635/// A raw identifier as it appears in source, together with its span.
636#[derive(Clone, Debug, PartialEq, Eq, Hash)]
637pub struct SurfaceIdent {
638    /// The identifier string.
639    pub name: String,
640    /// Source span (byte offsets).
641    pub span: ByteRange,
642}
643impl SurfaceIdent {
644    /// Create a surface identifier.
645    pub fn new(name: &str, span: ByteRange) -> Self {
646        Self {
647            name: name.to_string(),
648            span,
649        }
650    }
651    /// Create a synthetic identifier with no real source span.
652    pub fn synthetic(name: &str) -> Self {
653        Self {
654            name: name.to_string(),
655            span: ByteRange::empty(),
656        }
657    }
658    /// Whether the identifier was synthesized (not from real source).
659    pub fn is_synthetic(&self) -> bool {
660        self.span.is_empty()
661    }
662    /// Whether the identifier starts with an underscore.
663    pub fn is_anonymous(&self) -> bool {
664        self.name.starts_with('_')
665    }
666    /// Whether the identifier contains a dot (qualified name).
667    pub fn is_qualified(&self) -> bool {
668        self.name.contains('.')
669    }
670    /// Split a qualified name at the last dot, if any.
671    pub fn split_last(&self) -> Option<(&str, &str)> {
672        let pos = self.name.rfind('.')?;
673        Some((&self.name[..pos], &self.name[pos + 1..]))
674    }
675}
676/// A telescope of binders.
677#[allow(dead_code)]
678#[allow(missing_docs)]
679pub struct Telescope {
680    /// The binders in order
681    pub binders: Vec<BinderExt>,
682}
683impl Telescope {
684    /// Create an empty telescope.
685    #[allow(dead_code)]
686    pub fn new() -> Self {
687        Telescope {
688            binders: Vec::new(),
689        }
690    }
691    /// Add a binder.
692    #[allow(dead_code)]
693    #[allow(clippy::should_implement_trait)]
694    pub fn add(mut self, b: BinderExt) -> Self {
695        self.binders.push(b);
696        self
697    }
698    /// Format the telescope.
699    #[allow(dead_code)]
700    pub fn format(&self) -> String {
701        self.binders
702            .iter()
703            .map(|b| b.format())
704            .collect::<Vec<_>>()
705            .join(" ")
706    }
707    /// Returns the number of binders.
708    #[allow(dead_code)]
709    pub fn len(&self) -> usize {
710        self.binders.len()
711    }
712    /// Returns true if empty.
713    #[allow(dead_code)]
714    pub fn is_empty(&self) -> bool {
715        self.binders.is_empty()
716    }
717}
718/// A declaration header.
719#[allow(dead_code)]
720#[allow(missing_docs)]
721#[derive(Debug, Clone)]
722pub struct DeclHeaderExt {
723    /// The declaration name
724    pub name: String,
725    /// The telescope of binders
726    pub params: Vec<BinderExt>,
727    /// The return type
728    pub return_type: Option<String>,
729}
730impl DeclHeaderExt {
731    /// Create a new declaration header.
732    #[allow(dead_code)]
733    pub fn new(name: &str) -> Self {
734        DeclHeaderExt {
735            name: name.to_string(),
736            params: Vec::new(),
737            return_type: None,
738        }
739    }
740    /// Add a parameter.
741    #[allow(dead_code)]
742    pub fn add_param(mut self, b: BinderExt) -> Self {
743        self.params.push(b);
744        self
745    }
746    /// Set the return type.
747    #[allow(dead_code)]
748    pub fn with_return_type(mut self, ty: &str) -> Self {
749        self.return_type = Some(ty.to_string());
750        self
751    }
752}
753/// A match expression surface form.
754#[allow(dead_code)]
755#[allow(missing_docs)]
756#[derive(Debug, Clone)]
757pub struct MatchExprExt {
758    /// The scrutinee
759    pub scrutinee: String,
760    /// The arms
761    pub arms: Vec<(String, String)>,
762}
763impl MatchExprExt {
764    /// Create a new match expression.
765    #[allow(dead_code)]
766    pub fn new(scrutinee: &str) -> Self {
767        MatchExprExt {
768            scrutinee: scrutinee.to_string(),
769            arms: Vec::new(),
770        }
771    }
772    /// Add an arm.
773    #[allow(dead_code)]
774    pub fn add_arm(mut self, pat: &str, body: &str) -> Self {
775        self.arms.push((pat.to_string(), body.to_string()));
776        self
777    }
778    /// Format the match expression.
779    #[allow(dead_code)]
780    pub fn format(&self) -> String {
781        let arms: Vec<String> = self
782            .arms
783            .iter()
784            .map(|(p, b)| format!("  | {} -> {}", p, b))
785            .collect();
786        format!("match {} with\n{}", self.scrutinee, arms.join("\n"))
787    }
788}
789/// A position-annotated wrapper for any value.
790#[allow(dead_code)]
791#[allow(missing_docs)]
792#[derive(Debug, Clone)]
793pub struct WithPosExt<T> {
794    /// The wrapped value
795    pub inner: T,
796    /// Byte start offset
797    pub start: usize,
798    /// Byte end offset
799    pub end: usize,
800}
801impl<T> WithPosExt<T> {
802    /// Create a new WithPosExt.
803    #[allow(dead_code)]
804    pub fn new(inner: T, start: usize, end: usize) -> Self {
805        WithPosExt { inner, start, end }
806    }
807    /// Map the inner value.
808    #[allow(dead_code)]
809    pub fn map<U, F: FnOnce(T) -> U>(self, f: F) -> WithPosExt<U> {
810        WithPosExt {
811            inner: f(self.inner),
812            start: self.start,
813            end: self.end,
814        }
815    }
816}
817/// A parse error with location information.
818#[derive(Clone, Debug, PartialEq, Eq)]
819pub struct ParseError {
820    /// Human-readable error message.
821    pub message: String,
822    /// Location in the source where the error occurred.
823    pub pos: Pos,
824    /// Optional hint for how to fix the error.
825    pub hint: Option<String>,
826}
827impl ParseError {
828    /// Create a parse error.
829    pub fn new(message: impl Into<String>, pos: Pos) -> Self {
830        Self {
831            message: message.into(),
832            pos,
833            hint: None,
834        }
835    }
836    /// Attach a hint to the error.
837    pub fn with_hint(mut self, hint: impl Into<String>) -> Self {
838        self.hint = Some(hint.into());
839        self
840    }
841    /// Format the error for display.
842    pub fn display(&self) -> String {
843        let mut s = format!("error at {}: {}", self.pos, self.message);
844        if let Some(h) = &self.hint {
845            s.push_str(&format!("\n  hint: {}", h));
846        }
847        s
848    }
849}
850/// A flat representation of an AST (pre-order traversal).
851#[allow(dead_code)]
852#[allow(missing_docs)]
853pub struct FlatAstExt {
854    /// Nodes in pre-order
855    pub nodes: Vec<(SimpleNodeKindExt, String, usize)>,
856}
857impl FlatAstExt {
858    /// Flatten a tree node into pre-order sequence.
859    #[allow(dead_code)]
860    pub fn from_tree(root: &TreeNodeExt) -> Self {
861        let mut nodes = Vec::new();
862        flatten_tree_ext(root, 0, &mut nodes);
863        FlatAstExt { nodes }
864    }
865    /// Returns the number of nodes.
866    #[allow(dead_code)]
867    pub fn len(&self) -> usize {
868        self.nodes.len()
869    }
870    /// Returns true if empty.
871    #[allow(dead_code)]
872    pub fn is_empty(&self) -> bool {
873        self.nodes.is_empty()
874    }
875}
876/// A telescope: a sequence of binders.
877#[allow(dead_code)]
878#[allow(missing_docs)]
879#[derive(Debug, Clone, Default)]
880pub struct TelescopeExt2 {
881    /// The binders in order
882    pub binders: Vec<BinderExtExt2>,
883}
884impl TelescopeExt2 {
885    /// Create an empty telescope.
886    #[allow(dead_code)]
887    pub fn new() -> Self {
888        TelescopeExt2 {
889            binders: Vec::new(),
890        }
891    }
892    /// Add a binder.
893    #[allow(dead_code)]
894    pub fn push(&mut self, b: BinderExtExt2) {
895        self.binders.push(b);
896    }
897    /// Returns the number of binders.
898    #[allow(dead_code)]
899    pub fn len(&self) -> usize {
900        self.binders.len()
901    }
902    /// Returns true if empty.
903    #[allow(dead_code)]
904    pub fn is_empty(&self) -> bool {
905        self.binders.is_empty()
906    }
907    /// Format as a space-separated list of binder strings.
908    #[allow(dead_code)]
909    pub fn format(&self) -> String {
910        self.binders
911            .iter()
912            .map(|b| b.format())
913            .collect::<Vec<_>>()
914            .join(" ")
915    }
916}
917/// A match expression in the AST.
918#[allow(dead_code)]
919#[allow(missing_docs)]
920#[derive(Debug, Clone)]
921pub struct MatchExprExtExt2 {
922    /// The discriminant expression
923    pub scrutinee: String,
924    /// The match arms as (pattern, body) pairs
925    pub arms: Vec<(String, String)>,
926}
927impl MatchExprExtExt2 {
928    /// Create a new match expression.
929    #[allow(dead_code)]
930    pub fn new(scrutinee: &str, arms: Vec<(&str, &str)>) -> Self {
931        MatchExprExtExt2 {
932            scrutinee: scrutinee.to_string(),
933            arms: arms
934                .into_iter()
935                .map(|(p, b)| (p.to_string(), b.to_string()))
936                .collect(),
937        }
938    }
939    /// Returns the number of arms.
940    #[allow(dead_code)]
941    pub fn arm_count(&self) -> usize {
942        self.arms.len()
943    }
944    /// Returns the patterns as a vector.
945    #[allow(dead_code)]
946    pub fn patterns(&self) -> Vec<&str> {
947        self.arms.iter().map(|(p, _)| p.as_str()).collect()
948    }
949}
950/// A generic tree node for testing AST operations.
951#[allow(dead_code)]
952#[allow(missing_docs)]
953#[derive(Debug, Clone)]
954pub struct TreeNodeExt {
955    /// Kind of this node
956    pub kind: SimpleNodeKindExt,
957    /// Label or identifier
958    pub label: String,
959    /// Children of this node
960    pub children: Vec<TreeNodeExt>,
961}
962impl TreeNodeExt {
963    /// Create a leaf node.
964    #[allow(dead_code)]
965    pub fn leaf(label: &str) -> Self {
966        TreeNodeExt {
967            kind: SimpleNodeKindExt::Leaf,
968            label: label.to_string(),
969            children: Vec::new(),
970        }
971    }
972    /// Create an app node with two children.
973    #[allow(dead_code)]
974    pub fn app(func: TreeNodeExt, arg: TreeNodeExt) -> Self {
975        TreeNodeExt {
976            kind: SimpleNodeKindExt::App,
977            label: "@".to_string(),
978            children: vec![func, arg],
979        }
980    }
981    /// Create a lam node.
982    #[allow(dead_code)]
983    pub fn lam(binder: &str, body: TreeNodeExt) -> Self {
984        TreeNodeExt {
985            kind: SimpleNodeKindExt::Lam,
986            label: binder.to_string(),
987            children: vec![body],
988        }
989    }
990    /// Returns the depth of this tree.
991    #[allow(dead_code)]
992    pub fn depth(&self) -> usize {
993        if self.children.is_empty() {
994            return 0;
995        }
996        1 + self.children.iter().map(|c| c.depth()).max().unwrap_or(0)
997    }
998    /// Returns the total number of nodes.
999    #[allow(dead_code)]
1000    pub fn size(&self) -> usize {
1001        1 + self.children.iter().map(|c| c.size()).sum::<usize>()
1002    }
1003    /// Visit all nodes with a visitor.
1004    #[allow(dead_code)]
1005    pub fn visit<V: AstNodeVisitorExt>(&self, visitor: &mut V, depth: usize) {
1006        let kind_str = format!("{:?}", self.kind);
1007        visitor.visit_node(&kind_str, depth);
1008        for child in &self.children {
1009            child.visit(visitor, depth + 1);
1010        }
1011    }
1012}
1013/// A type synonym definition.
1014#[allow(dead_code)]
1015#[allow(missing_docs)]
1016#[derive(Debug, Clone)]
1017pub struct TypeSynonym {
1018    /// Name of the synonym
1019    pub name: String,
1020    /// Type parameters
1021    pub params: Vec<String>,
1022    /// Definition
1023    pub def: String,
1024}
1025impl TypeSynonym {
1026    /// Create a new type synonym.
1027    #[allow(dead_code)]
1028    pub fn new(name: &str, params: Vec<&str>, def: &str) -> Self {
1029        TypeSynonym {
1030            name: name.to_string(),
1031            params: params.into_iter().map(|s| s.to_string()).collect(),
1032            def: def.to_string(),
1033        }
1034    }
1035    /// Format as "abbrev Name params := def".
1036    #[allow(dead_code)]
1037    pub fn format(&self) -> String {
1038        let params = self.params.join(" ");
1039        if params.is_empty() {
1040            format!("abbrev {} := {}", self.name, self.def)
1041        } else {
1042            format!("abbrev {} {} := {}", self.name, params, self.def)
1043        }
1044    }
1045}
1046/// A tag identifying the kind of an AST node.
1047#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
1048pub enum AstNodeKind {
1049    /// A variable or constant name.
1050    Var,
1051    /// A lambda expression.
1052    Lam,
1053    /// A Pi / forall type.
1054    Pi,
1055    /// An application.
1056    App,
1057    /// A let-expression.
1058    Let,
1059    /// A natural-number literal.
1060    NatLit,
1061    /// A string literal.
1062    StrLit,
1063    /// A sort (Prop/Type).
1064    Sort,
1065    /// A hole `_`.
1066    Hole,
1067    /// A `def` declaration.
1068    DefDecl,
1069    /// A `theorem` declaration.
1070    TheoremDecl,
1071    /// An `axiom` declaration.
1072    AxiomDecl,
1073}
1074/// A simple tag identifying broad categories of tokens.
1075#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
1076pub enum TokenKindTag {
1077    /// An identifier or keyword.
1078    Ident,
1079    /// A numeric literal.
1080    Num,
1081    /// A string literal.
1082    Str,
1083    /// An operator symbol.
1084    Op,
1085    /// A delimiter (paren, bracket, brace).
1086    Delim,
1087    /// End of file.
1088    Eof,
1089}
1090/// Numeric precedence for an operator.
1091#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
1092pub struct Prec(pub u32);
1093impl Prec {
1094    /// Default term precedence (Lean 4 uses 1024 for atoms).
1095    pub const ATOM: Prec = Prec(1024);
1096    /// Precedence for function application.
1097    pub const APP: Prec = Prec(1000);
1098    /// Precedence for `*` / `/`.
1099    pub const MUL: Prec = Prec(70);
1100    /// Precedence for `+` / `-`.
1101    pub const ADD: Prec = Prec(65);
1102    /// Precedence for comparison operators.
1103    pub const CMP: Prec = Prec(50);
1104    /// Minimum precedence (weakest binding).
1105    pub const MIN: Prec = Prec(0);
1106    /// Create a precedence value.
1107    pub fn new(p: u32) -> Self {
1108        Prec(p)
1109    }
1110    /// Raw numeric value.
1111    pub fn value(self) -> u32 {
1112        self.0
1113    }
1114    /// One level tighter binding.
1115    pub fn tighter(self) -> Self {
1116        Prec(self.0 + 1)
1117    }
1118}
1119/// An expression annotation kind.
1120#[allow(dead_code)]
1121#[allow(missing_docs)]
1122#[derive(Debug, Clone, PartialEq, Eq)]
1123pub enum AnnotationKind {
1124    /// Type annotation
1125    Type,
1126    /// Docstring
1127    Doc,
1128    /// Derivation hint
1129    Derive,
1130    /// Attribute
1131    Attr,
1132}
1133/// A counting visitor that counts each kind.
1134#[allow(dead_code)]
1135#[allow(missing_docs)]
1136pub struct CountingVisitorExt {
1137    /// Map from node kind to count
1138    pub counts: std::collections::HashMap<String, usize>,
1139    /// Current depth
1140    pub depth: usize,
1141}
1142impl CountingVisitorExt {
1143    /// Create a new counting visitor.
1144    #[allow(dead_code)]
1145    pub fn new() -> Self {
1146        CountingVisitorExt {
1147            counts: std::collections::HashMap::new(),
1148            depth: 0,
1149        }
1150    }
1151}
1152/// A stack of open namespaces, used during parsing.
1153#[derive(Clone, Debug, Default)]
1154pub struct NamespaceStack {
1155    stack: Vec<String>,
1156}
1157impl NamespaceStack {
1158    /// Create an empty stack.
1159    pub fn new() -> Self {
1160        Self::default()
1161    }
1162    /// Push a namespace.
1163    pub fn push(&mut self, ns: impl Into<String>) {
1164        self.stack.push(ns.into());
1165    }
1166    /// Pop the top namespace. Returns the popped name, or `None` if empty.
1167    pub fn pop(&mut self) -> Option<String> {
1168        self.stack.pop()
1169    }
1170    /// The current fully-qualified namespace path (dot-separated).
1171    pub fn current_path(&self) -> String {
1172        self.stack.join(".")
1173    }
1174    /// Qualify a name with the current namespace.
1175    pub fn qualify(&self, name: &str) -> String {
1176        if self.stack.is_empty() {
1177            name.to_string()
1178        } else {
1179            format!("{}.{}", self.current_path(), name)
1180        }
1181    }
1182    /// Depth of the stack.
1183    pub fn depth(&self) -> usize {
1184        self.stack.len()
1185    }
1186    /// Whether the stack is empty (top-level).
1187    pub fn is_top_level(&self) -> bool {
1188        self.stack.is_empty()
1189    }
1190}
1191/// A structure field.
1192#[allow(dead_code)]
1193#[allow(missing_docs)]
1194#[derive(Debug, Clone)]
1195pub struct StructField {
1196    /// Field name
1197    pub name: String,
1198    /// Field type
1199    pub ty: String,
1200    /// Optional default value
1201    pub default: Option<String>,
1202}
1203impl StructField {
1204    /// Create a new field.
1205    #[allow(dead_code)]
1206    pub fn new(name: &str, ty: &str) -> Self {
1207        StructField {
1208            name: name.to_string(),
1209            ty: ty.to_string(),
1210            default: None,
1211        }
1212    }
1213    /// Set the default value.
1214    #[allow(dead_code)]
1215    pub fn with_default(mut self, v: &str) -> Self {
1216        self.default = Some(v.to_string());
1217        self
1218    }
1219}
1220/// A documentation comment attached to a declaration.
1221#[derive(Clone, Debug, PartialEq, Eq)]
1222pub struct DocComment {
1223    /// The raw comment text (without the `/--` delimiters).
1224    pub text: String,
1225    /// Whether this is a module-level doc comment.
1226    pub is_module_doc: bool,
1227    /// Byte range of the comment in the source.
1228    pub span: ByteRange,
1229}
1230impl DocComment {
1231    /// Create a doc comment.
1232    pub fn new(text: &str, span: ByteRange) -> Self {
1233        Self {
1234            text: text.to_string(),
1235            is_module_doc: false,
1236            span,
1237        }
1238    }
1239    /// Create a module-level doc comment.
1240    pub fn module_doc(text: &str) -> Self {
1241        Self {
1242            text: text.to_string(),
1243            is_module_doc: true,
1244            span: ByteRange::empty(),
1245        }
1246    }
1247    /// The first line of the doc comment (for summaries).
1248    pub fn first_line(&self) -> &str {
1249        self.text.lines().next().unwrap_or("").trim()
1250    }
1251    /// Whether the doc comment is empty.
1252    pub fn is_empty(&self) -> bool {
1253        self.text.trim().is_empty()
1254    }
1255}
1256/// A scope-management declaration.
1257#[derive(Clone, Debug, PartialEq, Eq)]
1258pub enum ScopeDecl {
1259    /// `section Name`
1260    Section(String),
1261    /// `namespace Name`
1262    Namespace(String),
1263    /// `end Name`
1264    End(String),
1265    /// `open Name` (brings names into scope)
1266    Open(Vec<String>),
1267}
1268impl ScopeDecl {
1269    /// The name argument (for Section/Namespace/End).
1270    pub fn name(&self) -> Option<&str> {
1271        match self {
1272            ScopeDecl::Section(n) | ScopeDecl::Namespace(n) | ScopeDecl::End(n) => Some(n),
1273            ScopeDecl::Open(_) => None,
1274        }
1275    }
1276    /// Whether this opens new scope.
1277    pub fn opens_scope(&self) -> bool {
1278        matches!(self, ScopeDecl::Section(_) | ScopeDecl::Namespace(_))
1279    }
1280    /// Whether this closes scope.
1281    pub fn closes_scope(&self) -> bool {
1282        matches!(self, ScopeDecl::End(_))
1283    }
1284}
1285/// A substitution table for tree nodes.
1286#[allow(dead_code)]
1287#[allow(missing_docs)]
1288pub struct SubstTableExt {
1289    /// Mappings from variable name to replacement node
1290    pub mappings: Vec<(String, TreeNodeExt)>,
1291}
1292impl SubstTableExt {
1293    /// Create a new empty substitution table.
1294    #[allow(dead_code)]
1295    pub fn new() -> Self {
1296        SubstTableExt {
1297            mappings: Vec::new(),
1298        }
1299    }
1300    /// Add a mapping.
1301    #[allow(dead_code)]
1302    pub fn add(&mut self, var: &str, replacement: TreeNodeExt) {
1303        self.mappings.push((var.to_string(), replacement));
1304    }
1305    /// Apply the substitution to a tree node.
1306    #[allow(dead_code)]
1307    pub fn apply(&self, node: &TreeNodeExt) -> TreeNodeExt {
1308        match node.kind {
1309            SimpleNodeKindExt::Leaf => {
1310                if let Some((_, replacement)) = self.mappings.iter().find(|(v, _)| v == &node.label)
1311                {
1312                    replacement.clone()
1313                } else {
1314                    node.clone()
1315                }
1316            }
1317            _ => {
1318                let new_children: Vec<TreeNodeExt> =
1319                    node.children.iter().map(|c| self.apply(c)).collect();
1320                TreeNodeExt {
1321                    kind: node.kind.clone(),
1322                    label: node.label.clone(),
1323                    children: new_children,
1324                }
1325            }
1326        }
1327    }
1328}
1329/// Visibility of a declaration.
1330#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
1331pub enum Visibility {
1332    /// Visible everywhere (the default).
1333    #[default]
1334    Public,
1335    /// Visible only within the current file/module.
1336    Private,
1337    /// Visible within the current namespace and sub-namespaces.
1338    Protected,
1339}
1340impl Visibility {
1341    /// Whether this visibility allows access from outside the module.
1342    pub fn is_public(&self) -> bool {
1343        matches!(self, Visibility::Public)
1344    }
1345    /// Whether this visibility restricts access.
1346    pub fn is_restricted(&self) -> bool {
1347        !self.is_public()
1348    }
1349}
oxilean_parse/ast/types.rs

oxilean_parse/ast/
types.rs
