oxilean_parse/command/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Binder, Decl, Span};
6
7/// Kind of notation declaration.
8#[derive(Debug, Clone, PartialEq, Eq)]
9pub enum NotationKind {
10    /// Prefix operator
11    Prefix,
12    /// Infix operator
13    Infix,
14    /// Postfix operator
15    Postfix,
16    /// General notation
17    Notation,
18}
19/// Items to selectively open from a namespace.
20#[derive(Debug, Clone, PartialEq)]
21pub enum OpenItem {
22    /// Open everything
23    All,
24    /// Open only these names
25    Only(Vec<String>),
26    /// Open everything except these
27    Hiding(Vec<String>),
28    /// Rename a single identifier (old, new)
29    Renaming(String, String),
30}
31/// A top-level command.
32#[derive(Debug, Clone)]
33pub enum Command {
34    /// Declaration command
35    Decl(Decl),
36    /// Import command
37    Import {
38        /// Module name
39        module: String,
40        /// Source span
41        span: Span,
42    },
43    /// Export command
44    Export {
45        /// Names to export
46        names: Vec<String>,
47        /// Source span
48        span: Span,
49    },
50    /// Namespace command
51    Namespace {
52        /// Namespace name
53        name: String,
54        /// Source span
55        span: Span,
56    },
57    /// End namespace/section command
58    End {
59        /// Source span
60        span: Span,
61    },
62    /// Set option command
63    SetOption {
64        /// Option name
65        name: String,
66        /// Option value
67        value: String,
68        /// Source span
69        span: Span,
70    },
71    /// Open namespace command
72    Open {
73        /// Dotted path to namespace
74        path: Vec<String>,
75        /// Items to selectively open
76        items: Vec<OpenItem>,
77        /// Source span
78        span: Span,
79    },
80    /// Section command
81    Section {
82        /// Section name
83        name: String,
84        /// Source span
85        span: Span,
86    },
87    /// Variable declaration
88    Variable {
89        /// Binders declared
90        binders: Vec<Binder>,
91        /// Source span
92        span: Span,
93    },
94    /// Attribute command
95    Attribute {
96        /// Attribute names
97        attrs: Vec<String>,
98        /// Target name
99        name: String,
100        /// Source span
101        span: Span,
102    },
103    /// Check command (#check)
104    Check {
105        /// Expression to check (as string)
106        expr_str: String,
107        /// Source span
108        span: Span,
109    },
110    /// Eval command (#eval)
111    Eval {
112        /// Expression to evaluate (as string)
113        expr_str: String,
114        /// Source span
115        span: Span,
116    },
117    /// Print command (#print)
118    Print {
119        /// Name to print
120        name: String,
121        /// Source span
122        span: Span,
123    },
124    /// Reduce command (#reduce)
125    Reduce {
126        /// Expression to reduce (as string)
127        expr_str: String,
128        /// Source span
129        span: Span,
130    },
131    /// Universe declaration
132    Universe {
133        /// Universe variable names
134        names: Vec<String>,
135        /// Source span
136        span: Span,
137    },
138    /// Notation declaration
139    Notation {
140        /// Notation kind
141        kind: NotationKind,
142        /// Operator or notation name
143        name: String,
144        /// Precedence level
145        prec: Option<u32>,
146        /// Body (definition) of the notation
147        body: String,
148        /// Source span
149        span: Span,
150    },
151    /// Derive command
152    Derive {
153        /// Strategies to derive (e.g. DecidableEq, Repr)
154        strategies: Vec<String>,
155        /// Type name to derive for
156        type_name: String,
157        /// Source span
158        span: Span,
159    },
160    /// Structure command with fields and optional extends
161    Structure {
162        /// Structure name
163        name: String,
164        /// Extends clause (parent structures)
165        extends: Vec<String>,
166        /// Field declarations
167        fields: Vec<StructureField>,
168        /// Derive strategies
169        derives: Vec<String>,
170        /// Source span
171        span: Span,
172    },
173    /// Class command
174    Class {
175        /// Class name
176        name: String,
177        /// Class parameters (binders)
178        params: Vec<Binder>,
179        /// Extends clause
180        extends: Vec<String>,
181        /// Methods/fields
182        fields: Vec<StructureField>,
183        /// Source span
184        span: Span,
185    },
186    /// Instance declaration with priority
187    Instance {
188        /// Instance name
189        name: String,
190        /// Instance type
191        ty: String,
192        /// Priority (optional)
193        priority: Option<u32>,
194        /// Implementation body
195        body: String,
196        /// Source span
197        span: Span,
198    },
199    /// Attribute declaration
200    AttributeDecl {
201        /// Attribute name
202        name: String,
203        /// Attribute kind
204        kind: AttributeDeclKind,
205        /// Source span
206        span: Span,
207    },
208    /// Attribute application
209    ApplyAttribute {
210        /// Attribute name
211        attr_name: String,
212        /// Target name
213        target: String,
214        /// Attribute parameters
215        params: Vec<String>,
216        /// Source span
217        span: Span,
218    },
219    /// Syntax command
220    Syntax {
221        /// Syntax name
222        name: String,
223        /// Precedence
224        prec: Option<u32>,
225        /// Pattern
226        pattern: String,
227        /// Source span
228        span: Span,
229    },
230    /// Precedence declaration
231    Precedence {
232        /// Operator name
233        name: String,
234        /// Precedence level
235        level: u32,
236        /// Source span
237        span: Span,
238    },
239}
240/// Attribute declaration kind
241#[derive(Debug, Clone, PartialEq, Eq)]
242pub enum AttributeDeclKind {
243    /// Simple attribute
244    Simple,
245    /// Attribute with macro expansion
246    Macro,
247    /// Attribute with builtin implementation
248    Builtin,
249}
250/// Field declaration for structures and classes
251#[derive(Debug, Clone, PartialEq)]
252pub struct StructureField {
253    /// Field name
254    pub name: String,
255    /// Field type
256    pub ty: String,
257    /// Whether field is explicit or implicit
258    pub is_explicit: bool,
259    /// Default value (if any)
260    pub default: Option<String>,
261}
oxilean_parse/command/types.rs

oxilean_parse/command/
types.rs
