oxilean_parse/ast_impl/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5#[allow(unused_imports)]
6use crate::ast::{SimpleNodeKindExt, TreeNodeExt};
7use crate::tokens::{Span, StringPart};
8
9use super::functions::*;
10
11/// Binder kind.
12#[derive(Clone, Debug, PartialEq, Eq)]
13pub enum BinderKind {
14    /// Default (explicit argument)
15    Default,
16    /// Implicit argument: {x : alpha}
17    Implicit,
18    /// Instance argument: [x : alpha]
19    Instance,
20    /// Strict implicit: {{x : alpha}}
21    StrictImplicit,
22}
23/// A path in a tree, represented as a sequence of child indices.
24#[allow(dead_code)]
25#[allow(missing_docs)]
26#[derive(Debug, Clone, PartialEq, Eq)]
27pub struct TreePathExt(pub Vec<usize>);
28impl TreePathExt {
29    /// Create an empty (root) path.
30    #[allow(dead_code)]
31    pub fn root() -> Self {
32        TreePathExt(Vec::new())
33    }
34    /// Extend this path with a child index.
35    #[allow(dead_code)]
36    pub fn child(&self, idx: usize) -> Self {
37        let mut v = self.0.clone();
38        v.push(idx);
39        TreePathExt(v)
40    }
41    /// Returns the depth of this path.
42    #[allow(dead_code)]
43    pub fn depth(&self) -> usize {
44        self.0.len()
45    }
46}
47/// Computes tree statistics (depth, breadth, leaf count).
48#[allow(dead_code)]
49#[allow(missing_docs)]
50#[derive(Debug, Clone, Default)]
51pub struct TreeStatsExt2 {
52    /// Maximum depth of the tree
53    pub max_depth: usize,
54    /// Total number of nodes
55    pub node_count: usize,
56    /// Total number of leaves
57    pub leaf_count: usize,
58    /// Maximum branching factor seen
59    pub max_branching: usize,
60}
61/// Binder for lambda and Pi types.
62#[derive(Clone, Debug, PartialEq)]
63pub struct Binder {
64    /// Variable name (can be _ for unused)
65    pub name: String,
66    /// Type annotation (optional for lambda, required for Pi)
67    pub ty: Option<Box<Located<SurfaceExpr>>>,
68    /// Binder info (implicit, instance, etc.)
69    pub info: BinderKind,
70}
71/// A where clause for local definitions attached to a definition or theorem.
72///
73/// Example:
74/// ```text
75/// def foo (n : Nat) : Nat := bar n + baz n where
76///   bar (x : Nat) : Nat := x + 1
77///   baz (x : Nat) : Nat := x * 2
78/// ```
79#[derive(Clone, Debug, PartialEq)]
80pub struct WhereClause {
81    /// Name of the local definition.
82    pub name: String,
83    /// Parameters of the local definition.
84    pub params: Vec<Binder>,
85    /// Optional type annotation.
86    pub ty: Option<Located<SurfaceExpr>>,
87    /// Value (body) of the local definition.
88    pub val: Located<SurfaceExpr>,
89}
90impl WhereClause {
91    /// Create a new where clause.
92    #[allow(dead_code)]
93    pub fn new(
94        name: String,
95        params: Vec<Binder>,
96        ty: Option<Located<SurfaceExpr>>,
97        val: Located<SurfaceExpr>,
98    ) -> Self {
99        Self {
100            name,
101            params,
102            ty,
103            val,
104        }
105    }
106}
107/// A single step in a `calc` proof expression.
108///
109/// Example:
110/// ```text
111/// calc a = b := proof1
112///      _ < c := proof2
113/// ```
114#[derive(Clone, Debug, PartialEq)]
115pub struct CalcStep {
116    /// Left-hand side of the step.
117    pub lhs: Located<SurfaceExpr>,
118    /// Relation symbol (e.g., `=`, `<`, `<=`).
119    pub rel: String,
120    /// Right-hand side of the step.
121    pub rhs: Located<SurfaceExpr>,
122    /// Proof/justification for this step.
123    pub proof: Located<SurfaceExpr>,
124}
125impl CalcStep {
126    /// Create a new calc step.
127    #[allow(dead_code)]
128    pub fn new(
129        lhs: Located<SurfaceExpr>,
130        rel: String,
131        rhs: Located<SurfaceExpr>,
132        proof: Located<SurfaceExpr>,
133    ) -> Self {
134        Self {
135            lhs,
136            rel,
137            rhs,
138            proof,
139        }
140    }
141}
142/// Surface-level expression (before elaboration).
143#[derive(Clone, Debug, PartialEq)]
144pub enum SurfaceExpr {
145    /// Sort: Type, Prop, Type u, Sort u
146    Sort(SortKind),
147    /// Variable reference
148    Var(String),
149    /// Application: f a
150    App(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
151    /// Lambda: fun (x : alpha) => body  or  lambda (x : alpha), body
152    Lam(Vec<Binder>, Box<Located<SurfaceExpr>>),
153    /// Pi type: forall (x : alpha), beta  or  (x : alpha) -> beta
154    Pi(Vec<Binder>, Box<Located<SurfaceExpr>>),
155    /// Let binding: let x : alpha := v in body
156    Let(
157        String,
158        Option<Box<Located<SurfaceExpr>>>,
159        Box<Located<SurfaceExpr>>,
160        Box<Located<SurfaceExpr>>,
161    ),
162    /// Literal value
163    Lit(Literal),
164    /// Explicit type annotation: (e : tau)
165    Ann(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
166    /// Placeholder: _
167    Hole,
168    /// Projection: e.n
169    Proj(Box<Located<SurfaceExpr>>, String),
170    /// If-then-else: if c then t else e
171    If(
172        Box<Located<SurfaceExpr>>,
173        Box<Located<SurfaceExpr>>,
174        Box<Located<SurfaceExpr>>,
175    ),
176    /// Match expression: match e with | pat => rhs | ...
177    Match(Box<Located<SurfaceExpr>>, Vec<MatchArm>),
178    /// Do notation: do { ... }
179    Do(Vec<DoAction>),
180    /// Have expression: have h : T := proof; body
181    Have(
182        String,
183        Box<Located<SurfaceExpr>>,
184        Box<Located<SurfaceExpr>>,
185        Box<Located<SurfaceExpr>>,
186    ),
187    /// Suffices expression: suffices h : T by tactic; body
188    Suffices(String, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
189    /// Show expression: show T from expr
190    Show(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
191    /// Named argument application: f (x := e)
192    NamedArg(Box<Located<SurfaceExpr>>, String, Box<Located<SurfaceExpr>>),
193    /// Anonymous constructor: (langle) a, b, c (rangle)
194    AnonymousCtor(Vec<Located<SurfaceExpr>>),
195    /// List literal: [1, 2, 3]
196    ListLit(Vec<Located<SurfaceExpr>>),
197    /// Tuple: (a, b) or (a, b, c)
198    Tuple(Vec<Located<SurfaceExpr>>),
199    /// Return expression (used in `do` notation): `return e`
200    Return(Box<Located<SurfaceExpr>>),
201    /// String interpolation: `s!"hello {name}"`
202    StringInterp(Vec<StringPart>),
203    /// Range expression: `a..b`, `..b`, `a..`
204    Range(
205        Option<Box<Located<SurfaceExpr>>>,
206        Option<Box<Located<SurfaceExpr>>>,
207    ),
208    /// By-tactic expression: `by tactic1; tactic2; ...`
209    ByTactic(Vec<Located<TacticRef>>),
210    /// Calc expression: calculational proof
211    Calc(Vec<CalcStep>),
212}
213impl SurfaceExpr {
214    /// Create a variable expression.
215    #[allow(dead_code)]
216    pub fn var(name: &str) -> Self {
217        SurfaceExpr::Var(name.to_string())
218    }
219    /// Create a natural number literal expression.
220    #[allow(dead_code)]
221    pub fn nat(n: u64) -> Self {
222        SurfaceExpr::Lit(Literal::Nat(n))
223    }
224    /// Create a string literal expression.
225    #[allow(dead_code)]
226    pub fn string(s: &str) -> Self {
227        SurfaceExpr::Lit(Literal::String(s.to_string()))
228    }
229    /// Create a float literal expression.
230    #[allow(dead_code)]
231    pub fn float(v: f64) -> Self {
232        SurfaceExpr::Lit(Literal::Float(v))
233    }
234    /// Check if this expression is a hole/placeholder.
235    #[allow(dead_code)]
236    pub fn is_hole(&self) -> bool {
237        matches!(self, SurfaceExpr::Hole)
238    }
239    /// Check if this expression is a variable.
240    #[allow(dead_code)]
241    pub fn is_var(&self) -> bool {
242        matches!(self, SurfaceExpr::Var(_))
243    }
244    /// Get the variable name if this is a variable.
245    #[allow(dead_code)]
246    pub fn as_var(&self) -> Option<&str> {
247        match self {
248            SurfaceExpr::Var(s) => Some(s),
249            _ => None,
250        }
251    }
252}
253/// Match arm: pattern => expression
254#[derive(Clone, Debug, PartialEq)]
255pub struct MatchArm {
256    /// Pattern
257    pub pattern: Located<Pattern>,
258    /// Guard (optional): | when condition
259    pub guard: Option<Located<SurfaceExpr>>,
260    /// Right-hand side
261    pub rhs: Located<SurfaceExpr>,
262}
263/// A simple tree zipper for navigating trees.
264#[allow(dead_code)]
265#[allow(missing_docs)]
266#[derive(Debug, Clone)]
267pub struct TreeZipper {
268    /// Current focus node
269    pub focus: TreeNodeExt,
270    /// Context: (parent_label, left_siblings, right_siblings)
271    pub context: Vec<(String, Vec<TreeNodeExt>, Vec<TreeNodeExt>)>,
272}
273impl TreeZipper {
274    /// Create a zipper from a tree.
275    #[allow(dead_code)]
276    pub fn new(tree: TreeNodeExt) -> Self {
277        TreeZipper {
278            focus: tree,
279            context: Vec::new(),
280        }
281    }
282    /// Go down into the i-th child.
283    #[allow(dead_code)]
284    pub fn down(mut self, i: usize) -> Option<Self> {
285        if i >= self.focus.children.len() {
286            return None;
287        }
288        let mut children = self.focus.children.clone();
289        let child = children.remove(i);
290        let left = children[..i].to_vec();
291        let right = children[i..].to_vec();
292        self.context.push((self.focus.label.clone(), left, right));
293        Some(TreeZipper {
294            focus: child,
295            context: self.context,
296        })
297    }
298    /// Returns the depth (number of levels descended).
299    #[allow(dead_code)]
300    pub fn depth(&self) -> usize {
301        self.context.len()
302    }
303    /// Returns the label of the current focus node.
304    #[allow(dead_code)]
305    pub fn label(&self) -> &str {
306        &self.focus.label
307    }
308}
309/// Pattern for match expressions.
310#[derive(Clone, Debug, PartialEq)]
311pub enum Pattern {
312    /// Wildcard _
313    Wild,
314    /// Variable binding
315    Var(String),
316    /// Constructor application: C p1 p2 ...
317    Ctor(String, Vec<Located<Pattern>>),
318    /// Literal pattern
319    Lit(Literal),
320    /// Or pattern: p1 | p2
321    Or(Box<Located<Pattern>>, Box<Located<Pattern>>),
322}
323/// Top-level declaration.
324#[derive(Clone, Debug, PartialEq)]
325#[allow(clippy::large_enum_variant)]
326pub enum Decl {
327    /// Axiom declaration
328    Axiom {
329        /// Name
330        name: String,
331        /// Universe parameters
332        univ_params: Vec<String>,
333        /// Type
334        ty: Located<SurfaceExpr>,
335        /// Attributes
336        attrs: Vec<AttributeKind>,
337    },
338    /// Definition
339    Definition {
340        /// Name
341        name: String,
342        /// Universe parameters
343        univ_params: Vec<String>,
344        /// Type (optional, can be inferred)
345        ty: Option<Located<SurfaceExpr>>,
346        /// Value
347        val: Located<SurfaceExpr>,
348        /// Where clauses (local definitions)
349        where_clauses: Vec<WhereClause>,
350        /// Attributes
351        attrs: Vec<AttributeKind>,
352    },
353    /// Theorem
354    Theorem {
355        /// Name
356        name: String,
357        /// Universe parameters
358        univ_params: Vec<String>,
359        /// Type (statement)
360        ty: Located<SurfaceExpr>,
361        /// Proof
362        proof: Located<SurfaceExpr>,
363        /// Where clauses (local definitions)
364        where_clauses: Vec<WhereClause>,
365        /// Attributes
366        attrs: Vec<AttributeKind>,
367    },
368    /// Inductive type
369    Inductive {
370        /// Name
371        name: String,
372        /// Universe parameters
373        univ_params: Vec<String>,
374        /// Parameters (non-varying)
375        params: Vec<Binder>,
376        /// Indices (varying)
377        indices: Vec<Binder>,
378        /// Type
379        ty: Located<SurfaceExpr>,
380        /// Constructors
381        ctors: Vec<Constructor>,
382    },
383    /// Import declaration
384    Import {
385        /// Module path
386        path: Vec<String>,
387    },
388    /// Namespace declaration
389    Namespace {
390        /// Namespace name
391        name: String,
392        /// Declarations inside
393        decls: Vec<Located<Decl>>,
394    },
395    /// Structure declaration
396    Structure {
397        /// Structure name
398        name: String,
399        /// Universe parameters
400        univ_params: Vec<String>,
401        /// Parent structures (extends)
402        extends: Vec<String>,
403        /// Fields
404        fields: Vec<FieldDecl>,
405    },
406    /// Class declaration
407    ClassDecl {
408        /// Class name
409        name: String,
410        /// Universe parameters
411        univ_params: Vec<String>,
412        /// Parent classes (extends)
413        extends: Vec<String>,
414        /// Fields/methods
415        fields: Vec<FieldDecl>,
416    },
417    /// Instance declaration
418    InstanceDecl {
419        /// Optional instance name
420        name: Option<String>,
421        /// Class being instantiated
422        class_name: String,
423        /// The instance type
424        ty: Located<SurfaceExpr>,
425        /// Method definitions
426        defs: Vec<(String, Located<SurfaceExpr>)>,
427    },
428    /// Section declaration
429    SectionDecl {
430        /// Section name
431        name: String,
432        /// Declarations inside
433        decls: Vec<Located<Decl>>,
434    },
435    /// Variable declaration
436    Variable {
437        /// Binders
438        binders: Vec<Binder>,
439    },
440    /// Open declaration
441    Open {
442        /// Module path
443        path: Vec<String>,
444        /// Specific names to open (empty = open all)
445        names: Vec<String>,
446    },
447    /// Attribute declaration
448    Attribute {
449        /// Attribute names
450        attrs: Vec<String>,
451        /// Inner declaration
452        decl: Box<Located<Decl>>,
453    },
454    /// Hash command (#check, #eval, #print)
455    HashCmd {
456        /// Command name (e.g. "check", "eval", "print")
457        cmd: String,
458        /// Argument expression
459        arg: Located<SurfaceExpr>,
460    },
461    /// Mutual recursive definitions
462    Mutual {
463        /// The mutually recursive declarations
464        decls: Vec<Located<Decl>>,
465    },
466    /// Derive declaration: `deriving instance1, instance2 for TypeName`
467    Derive {
468        /// Instance strategies to derive
469        instances: Vec<String>,
470        /// Type name to derive for
471        type_name: String,
472    },
473    /// Notation declaration
474    NotationDecl {
475        /// Kind of notation
476        kind: AstNotationKind,
477        /// Precedence (optional)
478        prec: Option<u32>,
479        /// Name or symbol
480        name: String,
481        /// Notation body
482        notation: String,
483    },
484    /// Universe declaration: `universe u v w`
485    Universe {
486        /// Universe variable names
487        names: Vec<String>,
488    },
489}
490impl Decl {
491    /// Get the name of this declaration, if it has one.
492    #[allow(dead_code)]
493    pub fn name(&self) -> Option<&str> {
494        match self {
495            Decl::Axiom { name, .. }
496            | Decl::Definition { name, .. }
497            | Decl::Theorem { name, .. }
498            | Decl::Inductive { name, .. }
499            | Decl::Namespace { name, .. }
500            | Decl::Structure { name, .. }
501            | Decl::ClassDecl { name, .. }
502            | Decl::SectionDecl { name, .. } => Some(name),
503            Decl::InstanceDecl { name, .. } => name.as_deref(),
504            Decl::Derive { type_name, .. } => Some(type_name),
505            Decl::NotationDecl { name, .. } => Some(name),
506            _ => None,
507        }
508    }
509    /// Get the attributes if this declaration has typed attributes.
510    #[allow(dead_code)]
511    pub fn typed_attrs(&self) -> &[AttributeKind] {
512        match self {
513            Decl::Axiom { attrs, .. }
514            | Decl::Definition { attrs, .. }
515            | Decl::Theorem { attrs, .. } => attrs,
516            _ => &[],
517        }
518    }
519    /// Check if this declaration is a mutual block.
520    #[allow(dead_code)]
521    pub fn is_mutual(&self) -> bool {
522        matches!(self, Decl::Mutual { .. })
523    }
524}
525/// Kind of notation declaration in the AST.
526#[derive(Clone, Debug, PartialEq, Eq)]
527pub enum AstNotationKind {
528    /// Prefix operator (e.g., `-x`)
529    Prefix,
530    /// Postfix operator (e.g., `x!`)
531    Postfix,
532    /// Left-associative infix operator
533    Infixl,
534    /// Right-associative infix operator
535    Infixr,
536    /// General notation
537    Notation,
538}
539/// A located expression (expression with source span).
540#[derive(Clone, Debug, PartialEq)]
541pub struct Located<T> {
542    /// The value
543    pub value: T,
544    /// Source span
545    pub span: Span,
546}
547impl<T> Located<T> {
548    /// Create a new located value.
549    pub fn new(value: T, span: Span) -> Self {
550        Self { value, span }
551    }
552    /// Map the inner value while preserving the span.
553    #[allow(dead_code)]
554    pub fn map<U, F: FnOnce(T) -> U>(self, f: F) -> Located<U> {
555        Located {
556            value: f(self.value),
557            span: self.span,
558        }
559    }
560}
561/// Typed attribute kinds for declarations.
562///
563/// In Lean 4, attributes like `@[simp]`, `@[ext]`, `@[reducible]` control
564/// how the elaborator and tactics treat definitions.
565#[derive(Clone, Debug, PartialEq, Eq)]
566pub enum AttributeKind {
567    /// `@[simp]` - add to the simp set
568    Simp,
569    /// `@[ext]` - extensionality lemma
570    Ext,
571    /// `@[instance]` - typeclass instance
572    Instance,
573    /// `@[reducible]` - mark as reducible for definitional equality
574    Reducible,
575    /// `@[irreducible]` - mark as irreducible
576    Irreducible,
577    /// `@[inline]` - inline during compilation
578    Inline,
579    /// `@[noinline]` - do not inline
580    NoInline,
581    /// `@[specialize]` - specialization hint
582    SpecializeAttr,
583    /// Custom user attribute
584    Custom(String),
585}
586impl AttributeKind {
587    /// Check if this is a custom attribute.
588    #[allow(dead_code)]
589    pub fn is_custom(&self) -> bool {
590        matches!(self, AttributeKind::Custom(_))
591    }
592    /// Get the name of the attribute as a string.
593    #[allow(dead_code)]
594    pub fn name(&self) -> &str {
595        match self {
596            AttributeKind::Simp => "simp",
597            AttributeKind::Ext => "ext",
598            AttributeKind::Instance => "instance",
599            AttributeKind::Reducible => "reducible",
600            AttributeKind::Irreducible => "irreducible",
601            AttributeKind::Inline => "inline",
602            AttributeKind::NoInline => "noinline",
603            AttributeKind::SpecializeAttr => "specialize",
604            AttributeKind::Custom(s) => s,
605        }
606    }
607}
608/// Literal values.
609#[derive(Clone, Debug, PartialEq)]
610pub enum Literal {
611    /// Natural number
612    Nat(u64),
613    /// Float
614    Float(f64),
615    /// String
616    String(String),
617    /// Character
618    Char(char),
619}
620/// Do notation action.
621#[derive(Clone, Debug, PartialEq)]
622pub enum DoAction {
623    /// let x := e
624    Let(String, Located<SurfaceExpr>),
625    /// let x : tau := e
626    LetTyped(String, Located<SurfaceExpr>, Located<SurfaceExpr>),
627    /// x <- e
628    Bind(String, Located<SurfaceExpr>),
629    /// pure expression
630    Expr(Located<SurfaceExpr>),
631    /// return e
632    Return(Located<SurfaceExpr>),
633}
634/// Field declaration for structures and classes.
635#[derive(Clone, Debug, PartialEq)]
636pub struct FieldDecl {
637    /// Field name
638    pub name: String,
639    /// Field type
640    pub ty: Located<SurfaceExpr>,
641    /// Default value (optional)
642    pub default: Option<Located<SurfaceExpr>>,
643}
644/// An identity transform that returns the input unchanged.
645#[allow(dead_code)]
646#[allow(missing_docs)]
647pub struct IdentityTransformExt;
648/// Constructor for inductive types.
649#[derive(Clone, Debug, PartialEq)]
650pub struct Constructor {
651    /// Constructor name
652    pub name: String,
653    /// Constructor type
654    pub ty: Located<SurfaceExpr>,
655}
656/// A memo table for tree transformations (cache-aside pattern).
657#[allow(dead_code)]
658#[allow(missing_docs)]
659pub struct TransformMemo {
660    /// Cached results keyed by fingerprint
661    pub cache: std::collections::HashMap<u64, TreeNodeExt>,
662}
663impl TransformMemo {
664    /// Create a new empty memo table.
665    #[allow(dead_code)]
666    pub fn new() -> Self {
667        TransformMemo {
668            cache: std::collections::HashMap::new(),
669        }
670    }
671    /// Look up a cached result.
672    #[allow(dead_code)]
673    pub fn get(&self, key: u64) -> Option<&TreeNodeExt> {
674        self.cache.get(&key)
675    }
676    /// Store a result.
677    #[allow(dead_code)]
678    pub fn store(&mut self, key: u64, result: TreeNodeExt) {
679        self.cache.insert(key, result);
680    }
681    /// Returns the number of cached entries.
682    #[allow(dead_code)]
683    pub fn len(&self) -> usize {
684        self.cache.len()
685    }
686    /// Returns true if empty.
687    #[allow(dead_code)]
688    pub fn is_empty(&self) -> bool {
689        self.cache.is_empty()
690    }
691}
692/// A tree statistics collector.
693#[allow(dead_code)]
694#[allow(missing_docs)]
695#[derive(Debug, Default)]
696pub struct TreeStats {
697    /// Total node count
698    pub nodes: usize,
699    /// Leaf node count
700    pub leaves: usize,
701    /// Maximum depth
702    pub max_depth: usize,
703    /// Total tree size
704    pub total_size: usize,
705}
706impl TreeStats {
707    /// Create an empty stats record.
708    #[allow(dead_code)]
709    pub fn new() -> Self {
710        TreeStats::default()
711    }
712    /// Compute stats from a tree.
713    #[allow(dead_code)]
714    pub fn from_tree(root: &TreeNodeExt) -> Self {
715        let mut stats = TreeStats::new();
716        collect_stats(root, 0, &mut stats);
717        stats
718    }
719}
720/// A zipper-based tree cursor for incremental editing.
721#[allow(dead_code)]
722#[allow(missing_docs)]
723pub struct TreeCursor {
724    /// Current node
725    pub current: TreeNodeExt,
726    /// Path back to root
727    pub ancestors: Vec<TreeNodeExt>,
728}
729impl TreeCursor {
730    /// Create a cursor at the root.
731    #[allow(dead_code)]
732    pub fn new(root: TreeNodeExt) -> Self {
733        TreeCursor {
734            current: root,
735            ancestors: Vec::new(),
736        }
737    }
738    /// Returns the kind of the current node.
739    #[allow(dead_code)]
740    pub fn kind(&self) -> &SimpleNodeKindExt {
741        &self.current.kind
742    }
743    /// Returns the label of the current node.
744    #[allow(dead_code)]
745    pub fn label(&self) -> &str {
746        &self.current.label
747    }
748    /// Returns the child count.
749    #[allow(dead_code)]
750    pub fn child_count(&self) -> usize {
751        self.current.children.len()
752    }
753    /// Returns the depth.
754    #[allow(dead_code)]
755    pub fn depth(&self) -> usize {
756        self.ancestors.len()
757    }
758}
759/// A tree zipper for navigation.
760#[allow(dead_code)]
761#[allow(missing_docs)]
762pub struct TreeZipperExt {
763    /// The focused node
764    pub focus: TreeNodeExt,
765    /// The path to the focus
766    pub path: TreePathExt,
767    /// Ancestors (parent, sibling index, left siblings, right siblings)
768    pub ancestors: Vec<(
769        SimpleNodeKindExt,
770        String,
771        Vec<TreeNodeExt>,
772        Vec<TreeNodeExt>,
773    )>,
774}
775impl TreeZipperExt {
776    /// Create a zipper from a root.
777    #[allow(dead_code)]
778    pub fn new(root: TreeNodeExt) -> Self {
779        TreeZipperExt {
780            focus: root,
781            path: TreePathExt::root(),
782            ancestors: Vec::new(),
783        }
784    }
785    /// Move into the i-th child.
786    #[allow(dead_code)]
787    pub fn down(mut self, i: usize) -> Option<Self> {
788        if i >= self.focus.children.len() {
789            return None;
790        }
791        let mut children = self.focus.children;
792        let child = children.remove(i);
793        let left: Vec<TreeNodeExt> = children.drain(..i.min(children.len())).collect();
794        let right: Vec<TreeNodeExt> = children;
795        self.ancestors
796            .push((self.focus.kind, self.focus.label, left, right));
797        self.path = self.path.child(i);
798        Some(TreeZipperExt {
799            focus: child,
800            path: self.path,
801            ancestors: self.ancestors,
802        })
803    }
804    /// Move back up to the parent.
805    #[allow(dead_code)]
806    pub fn up(mut self) -> Option<(Self, TreeNodeExt)> {
807        let (kind, label, left, right) = self.ancestors.pop()?;
808        let child = self.focus;
809        let mut children = left;
810        children.push(child.clone());
811        children.extend(right);
812        let mut new_path = self.path;
813        new_path.0.pop();
814        Some((
815            TreeZipperExt {
816                focus: TreeNodeExt {
817                    kind,
818                    label,
819                    children,
820                },
821                path: new_path,
822                ancestors: self.ancestors,
823            },
824            child,
825        ))
826    }
827}
828/// A transform that renames all leaf nodes matching a pattern.
829#[allow(dead_code)]
830#[allow(missing_docs)]
831pub struct RenameTransformExt {
832    /// Name to rename from
833    pub from: String,
834    /// Name to rename to
835    pub to: String,
836    /// Counter of renames performed
837    pub count: usize,
838}
839impl RenameTransformExt {
840    /// Create a new rename transform.
841    #[allow(dead_code)]
842    pub fn new(from: &str, to: &str) -> Self {
843        RenameTransformExt {
844            from: from.to_string(),
845            to: to.to_string(),
846            count: 0,
847        }
848    }
849}
850/// A simple tree cache that memoises node computations.
851#[allow(dead_code)]
852#[allow(missing_docs)]
853pub struct NodeCache {
854    /// Cached values by label
855    pub values: std::collections::HashMap<String, u64>,
856}
857impl NodeCache {
858    /// Create a new cache.
859    #[allow(dead_code)]
860    pub fn new() -> Self {
861        NodeCache {
862            values: std::collections::HashMap::new(),
863        }
864    }
865    /// Store a value.
866    #[allow(dead_code)]
867    pub fn store(&mut self, key: &str, val: u64) {
868        self.values.insert(key.to_string(), val);
869    }
870    /// Retrieve a value.
871    #[allow(dead_code)]
872    pub fn get(&self, key: &str) -> Option<u64> {
873        self.values.get(key).copied()
874    }
875}
876/// A memoized computation table for tree transformations.
877#[allow(dead_code)]
878#[allow(missing_docs)]
879pub struct TransformMemoExt2 {
880    /// Cache from label to transformed label
881    pub cache: std::collections::HashMap<String, String>,
882}
883impl TransformMemoExt2 {
884    /// Create a new empty memo table.
885    #[allow(dead_code)]
886    pub fn new() -> Self {
887        TransformMemoExt2 {
888            cache: std::collections::HashMap::new(),
889        }
890    }
891    /// Check if a label is already memoized.
892    #[allow(dead_code)]
893    pub fn has(&self, label: &str) -> bool {
894        self.cache.contains_key(label)
895    }
896    /// Get the memoized result for a label.
897    #[allow(dead_code)]
898    pub fn get(&self, label: &str) -> Option<&str> {
899        self.cache.get(label).map(|s| s.as_str())
900    }
901    /// Insert a memoized result.
902    #[allow(dead_code)]
903    pub fn insert(&mut self, label: &str, result: &str) {
904        self.cache.insert(label.to_string(), result.to_string());
905    }
906    /// Returns the number of memoized entries.
907    #[allow(dead_code)]
908    pub fn len(&self) -> usize {
909        self.cache.len()
910    }
911    /// Returns true if empty.
912    #[allow(dead_code)]
913    pub fn is_empty(&self) -> bool {
914        self.cache.is_empty()
915    }
916}
917/// Sort kinds.
918#[derive(Clone, Debug, PartialEq, Eq)]
919pub enum SortKind {
920    /// Type (Type 0)
921    Type,
922    /// Prop (Sort 0)
923    Prop,
924    /// Type u (explicit universe)
925    TypeU(String),
926    /// Sort u (explicit universe)
927    SortU(String),
928}
oxilean_parse/ast_impl/types.rs

oxilean_parse/ast_impl/
types.rs
