oxilean_parse/command/
commandparser_parsing.rs

1//! # CommandParser - parsing Methods
2//!
3//! This module contains method implementations for `CommandParser`.
4//!
5//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
6
7use crate::{
8    dummy_span, parser_impl::Parser as DeclParser, Binder, BinderKind, Decl, Located, ParseError,
9    ParseErrorKind, Span, Token, TokenKind,
10};
11
12use super::types::{AttributeDeclKind, Command, NotationKind, OpenItem, StructureField};
13
14use super::commandparser_type::CommandParser;
15
16impl CommandParser {
17    /// Create a new command parser.
18    pub fn new() -> Self {
19        Self {
20            pos: 0,
21            tokens: Vec::new(),
22        }
23    }
24    /// Expect a specific token kind; error if not matched.
25    pub(super) fn expect(&mut self, kind: &TokenKind) -> Result<Span, ParseError> {
26        if let Some(token) = self.current() {
27            if &token.kind == kind {
28                let span = token.span.clone();
29                self.advance();
30                return Ok(span);
31            }
32            return Err(ParseError::new(
33                ParseErrorKind::InvalidSyntax(format!("expected {:?}, got {:?}", kind, token.kind)),
34                token.span.clone(),
35            ));
36        }
37        Err(ParseError::new(
38            ParseErrorKind::UnexpectedEof {
39                expected: vec![format!("{:?}", kind)],
40            },
41            self.eof_span(),
42        ))
43    }
44    /// Parse an identifier token and return the string.
45    pub(super) fn parse_ident(&mut self) -> Result<String, ParseError> {
46        if let Some(token) = self.current() {
47            if let TokenKind::Ident(s) = &token.kind {
48                let result = s.clone();
49                self.advance();
50                return Ok(result);
51            }
52            return Err(ParseError::new(
53                ParseErrorKind::InvalidSyntax(format!("expected identifier, got {:?}", token.kind)),
54                token.span.clone(),
55            ));
56        }
57        Err(ParseError::new(
58            ParseErrorKind::UnexpectedEof {
59                expected: vec!["identifier".to_string()],
60            },
61            self.eof_span(),
62        ))
63    }
64    /// Span for unexpected eof.
65    pub(super) fn eof_span(&self) -> Span {
66        if let Some(last) = self.tokens.last() {
67            Span::new(
68                last.span.end,
69                last.span.end,
70                last.span.line,
71                last.span.column + 1,
72            )
73        } else {
74            dummy_span()
75        }
76    }
77    /// Collect text from current position until eof.
78    /// Returns the collected tokens joined by spaces.
79    pub(super) fn collect_rest_as_string(&mut self) -> String {
80        let mut parts = Vec::new();
81        while let Some(token) = self.current() {
82            match &token.kind {
83                TokenKind::Eof => break,
84                TokenKind::Ident(s) => parts.push(s.clone()),
85                TokenKind::Nat(n) => parts.push(n.to_string()),
86                TokenKind::String(s) => parts.push(format!("\"{}\"", s)),
87                TokenKind::LParen => parts.push("(".to_string()),
88                TokenKind::RParen => parts.push(")".to_string()),
89                TokenKind::LBrace => parts.push("{".to_string()),
90                TokenKind::RBrace => parts.push("}".to_string()),
91                TokenKind::LBracket => parts.push("[".to_string()),
92                TokenKind::RBracket => parts.push("]".to_string()),
93                TokenKind::Arrow => parts.push("->".to_string()),
94                TokenKind::Colon => parts.push(":".to_string()),
95                TokenKind::Comma => parts.push(",".to_string()),
96                TokenKind::Dot => parts.push(".".to_string()),
97                TokenKind::Eq => parts.push("=".to_string()),
98                TokenKind::Plus => parts.push("+".to_string()),
99                TokenKind::Minus => parts.push("-".to_string()),
100                TokenKind::Star => parts.push("*".to_string()),
101                TokenKind::Slash => parts.push("/".to_string()),
102                TokenKind::Assign => parts.push(":=".to_string()),
103                TokenKind::Underscore => parts.push("_".to_string()),
104                TokenKind::Bar => parts.push("|".to_string()),
105                TokenKind::Semicolon => parts.push(";".to_string()),
106                _ => parts.push(format!("{}", token.kind)),
107            }
108            self.advance();
109        }
110        parts.join(" ")
111    }
112    /// Parse binders: `(x : T)`, `{x : T}`, `[x : T]`, or bare `x`.
113    pub(super) fn parse_binders(&mut self) -> Result<Vec<Binder>, ParseError> {
114        let mut binders = Vec::new();
115        loop {
116            if self.check(&TokenKind::LParen) {
117                self.advance();
118                let names = self.parse_binder_names()?;
119                let ty = if self.consume(&TokenKind::Colon) {
120                    Some(self.collect_type_expr()?)
121                } else {
122                    None
123                };
124                self.expect(&TokenKind::RParen)?;
125                for name in names {
126                    binders.push(Binder {
127                        name,
128                        ty: ty.clone(),
129                        info: BinderKind::Default,
130                    });
131                }
132            } else if self.check(&TokenKind::LBrace) {
133                self.advance();
134                if self.check(&TokenKind::LBrace) {
135                    self.advance();
136                    let names = self.parse_binder_names()?;
137                    let ty = if self.consume(&TokenKind::Colon) {
138                        Some(self.collect_type_expr()?)
139                    } else {
140                        None
141                    };
142                    self.expect(&TokenKind::RBrace)?;
143                    self.expect(&TokenKind::RBrace)?;
144                    for name in names {
145                        binders.push(Binder {
146                            name,
147                            ty: ty.clone(),
148                            info: BinderKind::StrictImplicit,
149                        });
150                    }
151                } else {
152                    let names = self.parse_binder_names()?;
153                    let ty = if self.consume(&TokenKind::Colon) {
154                        Some(self.collect_type_expr()?)
155                    } else {
156                        None
157                    };
158                    self.expect(&TokenKind::RBrace)?;
159                    for name in names {
160                        binders.push(Binder {
161                            name,
162                            ty: ty.clone(),
163                            info: BinderKind::Implicit,
164                        });
165                    }
166                }
167            } else if self.check(&TokenKind::LBracket) {
168                self.advance();
169                let names = self.parse_binder_names()?;
170                let ty = if self.consume(&TokenKind::Colon) {
171                    Some(self.collect_type_expr()?)
172                } else {
173                    None
174                };
175                self.expect(&TokenKind::RBracket)?;
176                for name in names {
177                    binders.push(Binder {
178                        name,
179                        ty: ty.clone(),
180                        info: BinderKind::Instance,
181                    });
182                }
183            } else if let Some(token) = self.current() {
184                if let TokenKind::Ident(s) = &token.kind {
185                    if Self::is_command_keyword(&token.kind)
186                        || self.check(&TokenKind::Colon)
187                        || matches!(s.as_str(), "extends" | "where" | "deriving" | "priority")
188                    {
189                        break;
190                    }
191                    let name = self.parse_ident()?;
192                    binders.push(Binder {
193                        name,
194                        ty: None,
195                        info: BinderKind::Default,
196                    });
197                } else {
198                    break;
199                }
200            } else {
201                break;
202            }
203        }
204        Ok(binders)
205    }
206    /// Parse one or more binder names (identifiers or _).
207    pub(super) fn parse_binder_names(&mut self) -> Result<Vec<String>, ParseError> {
208        let mut names = Vec::new();
209        loop {
210            if self.check(&TokenKind::Underscore) {
211                self.advance();
212                names.push("_".to_string());
213            } else if let Some(token) = self.current() {
214                if let TokenKind::Ident(_) = &token.kind {
215                    names.push(self.parse_ident()?);
216                } else {
217                    break;
218                }
219            } else {
220                break;
221            }
222            if self.check(&TokenKind::Colon)
223                || self.check(&TokenKind::RParen)
224                || self.check(&TokenKind::RBrace)
225                || self.check(&TokenKind::RBracket)
226            {
227                break;
228            }
229        }
230        if names.is_empty() {
231            return Err(ParseError::new(
232                ParseErrorKind::InvalidBinder("expected binder name".to_string()),
233                self.current_span(),
234            ));
235        }
236        Ok(names)
237    }
238    /// Collect a type expression until we see `)`, `}`, `]`, `,`, or eof.
239    /// Returns it as a Located<SurfaceExpr>::Var (simplified).
240    pub(super) fn collect_type_expr(
241        &mut self,
242    ) -> Result<Box<crate::Located<crate::SurfaceExpr>>, ParseError> {
243        let span_start = self.current_span();
244        let mut parts = Vec::new();
245        let mut depth = 0i32;
246        while let Some(token) = self.current() {
247            match &token.kind {
248                TokenKind::RParen | TokenKind::RBrace | TokenKind::RBracket if depth <= 0 => break,
249                TokenKind::Comma if depth <= 0 => break,
250                TokenKind::Assign if depth <= 0 => break,
251                TokenKind::Eof => break,
252                TokenKind::LParen | TokenKind::LBrace | TokenKind::LBracket => {
253                    depth += 1;
254                    parts.push(format!("{}", token.kind));
255                    self.advance();
256                }
257                TokenKind::RParen | TokenKind::RBrace | TokenKind::RBracket => {
258                    depth -= 1;
259                    parts.push(format!("{}", token.kind));
260                    self.advance();
261                }
262                _ => {
263                    parts.push(format!("{}", token.kind));
264                    self.advance();
265                }
266            }
267        }
268        let text = parts.join(" ");
269        let span_end = self.current_span();
270        let merged = span_start.merge(&span_end);
271        Ok(Box::new(crate::Located::new(
272            crate::SurfaceExpr::Var(text),
273            merged,
274        )))
275    }
276    /// Parse a command from a token stream.
277    pub fn parse_command(&mut self, tokens: &[Token]) -> Result<Command, ParseError> {
278        self.tokens = tokens.to_vec();
279        self.pos = 0;
280        if tokens.is_empty() {
281            return Err(ParseError::new(
282                ParseErrorKind::UnexpectedEof {
283                    expected: vec!["command".to_string()],
284                },
285                dummy_span(),
286            ));
287        }
288        let token = &self.tokens[self.pos];
289        match &token.kind {
290            TokenKind::Import => self.parse_import(),
291            TokenKind::Export => self.parse_export(),
292            TokenKind::Namespace => self.parse_namespace(),
293            TokenKind::End => self.parse_end(),
294            TokenKind::Open => self.parse_open(),
295            TokenKind::Section => self.parse_section(),
296            TokenKind::Variable | TokenKind::Variables => self.parse_variable(),
297            TokenKind::Attribute => self.parse_attribute(),
298            TokenKind::Structure => self.parse_structure(),
299            TokenKind::Class => self.parse_class(),
300            TokenKind::Instance => self.parse_instance(),
301            TokenKind::Axiom
302            | TokenKind::Definition
303            | TokenKind::Theorem
304            | TokenKind::Lemma
305            | TokenKind::Inductive
306            | TokenKind::Opaque
307            | TokenKind::Constant
308            | TokenKind::Constants => {
309                let remaining: Vec<Token> = self.tokens[self.pos..].to_vec();
310                let mut decl_parser = DeclParser::new(remaining);
311                let located_decl: Located<Decl> = decl_parser.parse_decl()?;
312                Ok(Command::Decl(located_decl.value))
313            }
314            TokenKind::Hash => self.parse_hash_command(),
315            TokenKind::Ident(s) => {
316                let s = s.clone();
317                match s.as_str() {
318                    "set_option" => self.parse_set_option(),
319                    "universe" | "universes" => self.parse_universe(),
320                    "notation" => self.parse_notation(NotationKind::Notation),
321                    "prefix" => self.parse_notation(NotationKind::Prefix),
322                    "infix" | "infixl" | "infixr" => self.parse_notation(NotationKind::Infix),
323                    "postfix" => self.parse_notation(NotationKind::Postfix),
324                    "derive" | "deriving" => self.parse_derive(),
325                    "syntax" => self.parse_syntax(),
326                    _ => Err(ParseError::new(
327                        ParseErrorKind::InvalidSyntax(format!("unknown command: {}", s)),
328                        token.span.clone(),
329                    )),
330                }
331            }
332            _ => Err(ParseError::new(
333                ParseErrorKind::InvalidSyntax(format!("expected command, got {:?}", token.kind)),
334                token.span.clone(),
335            )),
336        }
337    }
338    /// Parse `export <name1> <name2> ...`.
339    pub(super) fn parse_export(&mut self) -> Result<Command, ParseError> {
340        let start_span = self.current_span();
341        self.advance();
342        let mut names = Vec::new();
343        while let Some(token) = self.current() {
344            if let TokenKind::Ident(_) = &token.kind {
345                names.push(self.parse_ident()?);
346            } else {
347                break;
348            }
349        }
350        if names.is_empty() {
351            return Err(ParseError::new(
352                ParseErrorKind::InvalidSyntax("expected at least one name to export".to_string()),
353                self.current_span(),
354            ));
355        }
356        let span = start_span.merge(&self.current_span());
357        Ok(Command::Export { names, span })
358    }
359    /// Parse `open <path> [( only | hiding | renaming )]`.
360    pub(super) fn parse_open(&mut self) -> Result<Command, ParseError> {
361        let start_span = self.current_span();
362        self.advance();
363        let path = self.parse_dotted_path()?;
364        let mut items = Vec::new();
365        if self.check_ident("only") {
366            self.advance();
367            self.expect(&TokenKind::LBracket)?;
368            let names = self.parse_comma_separated_idents()?;
369            self.expect(&TokenKind::RBracket)?;
370            items.push(OpenItem::Only(names));
371        } else if self.check_ident("hiding") {
372            self.advance();
373            self.expect(&TokenKind::LBracket)?;
374            let names = self.parse_comma_separated_idents()?;
375            self.expect(&TokenKind::RBracket)?;
376            items.push(OpenItem::Hiding(names));
377        } else if self.check_ident("renaming") {
378            self.advance();
379            let old_name = self.parse_ident()?;
380            self.expect(&TokenKind::Arrow)?;
381            let new_name = self.parse_ident()?;
382            items.push(OpenItem::Renaming(old_name, new_name));
383        } else {
384            items.push(OpenItem::All);
385        }
386        let span = start_span.merge(&self.current_span());
387        Ok(Command::Open { path, items, span })
388    }
389    /// Parse `variable (x : T) ...` or `variables (x : T) ...`.
390    pub(super) fn parse_variable(&mut self) -> Result<Command, ParseError> {
391        let start_span = self.current_span();
392        self.advance();
393        let binders = self.parse_binders()?;
394        if binders.is_empty() {
395            return Err(ParseError::new(
396                ParseErrorKind::InvalidBinder("expected at least one binder".to_string()),
397                self.current_span(),
398            ));
399        }
400        let span = start_span.merge(&self.current_span());
401        Ok(Command::Variable { binders, span })
402    }
403    /// Parse attribute commands:
404    /// - `attribute [attr1, attr2] <name>` -> Command::Attribute
405    /// - `attribute [attr_name] <target>` -> Command::ApplyAttribute
406    /// - `attribute [attr_name]` -> Command::AttributeDecl
407    pub(super) fn parse_attribute(&mut self) -> Result<Command, ParseError> {
408        let start_span = self.current_span();
409        self.advance();
410        self.expect(&TokenKind::LBracket)?;
411        let first_name = self.parse_ident()?;
412        if self.check(&TokenKind::Comma) {
413            let mut attrs = vec![first_name];
414            while self.consume(&TokenKind::Comma) {
415                attrs.push(self.parse_ident()?);
416            }
417            self.expect(&TokenKind::RBracket)?;
418            let name = self.parse_ident()?;
419            let span = start_span.merge(&self.current_span());
420            return Ok(Command::Attribute { attrs, name, span });
421        }
422        let mut params = Vec::new();
423        while !self.check(&TokenKind::RBracket) && !self.at_end() {
424            if let Some(token) = self.current() {
425                if let TokenKind::Ident(_) = &token.kind {
426                    params.push(self.parse_ident()?);
427                } else {
428                    break;
429                }
430            } else {
431                break;
432            }
433        }
434        self.expect(&TokenKind::RBracket)?;
435        let kind = if first_name.contains("macro") {
436            AttributeDeclKind::Macro
437        } else if first_name.contains("builtin") {
438            AttributeDeclKind::Builtin
439        } else {
440            AttributeDeclKind::Simple
441        };
442        let span = start_span.merge(&self.current_span());
443        if let Some(token) = self.current() {
444            if let TokenKind::Ident(_) = &token.kind {
445                let target = self.parse_ident()?;
446                let span = start_span.merge(&self.current_span());
447                return Ok(Command::ApplyAttribute {
448                    attr_name: first_name,
449                    target,
450                    params,
451                    span,
452                });
453            }
454        }
455        Ok(Command::AttributeDecl {
456            name: first_name,
457            kind,
458            span,
459        })
460    }
461    /// Parse `#check <expr>` or `#eval <expr>` or `#print <name>`.
462    pub(super) fn parse_hash_command(&mut self) -> Result<Command, ParseError> {
463        let start_span = self.current_span();
464        self.advance();
465        let cmd_name = self.parse_ident()?;
466        match cmd_name.as_str() {
467            "check" => {
468                let expr_str = self.collect_rest_as_string();
469                let span = start_span.merge(&self.current_span());
470                Ok(Command::Check { expr_str, span })
471            }
472            "eval" => {
473                let expr_str = self.collect_rest_as_string();
474                let span = start_span.merge(&self.current_span());
475                Ok(Command::Eval { expr_str, span })
476            }
477            "print" => {
478                let name = if let Ok(n) = self.parse_ident() {
479                    n
480                } else {
481                    self.collect_rest_as_string()
482                };
483                let span = start_span.merge(&self.current_span());
484                Ok(Command::Print { name, span })
485            }
486            "reduce" => {
487                let expr_str = self.collect_rest_as_string();
488                let span = start_span.merge(&self.current_span());
489                Ok(Command::Reduce { expr_str, span })
490            }
491            _ => Err(ParseError::new(
492                ParseErrorKind::InvalidSyntax(format!("unknown # command: #{}", cmd_name)),
493                start_span,
494            )),
495        }
496    }
497    /// Parse `universe <name1> <name2> ...` or `universes <name1> ...`.
498    pub(super) fn parse_universe(&mut self) -> Result<Command, ParseError> {
499        let start_span = self.current_span();
500        self.advance();
501        let mut names = Vec::new();
502        while let Some(token) = self.current() {
503            if let TokenKind::Ident(_) = &token.kind {
504                names.push(self.parse_ident()?);
505            } else {
506                break;
507            }
508        }
509        if names.is_empty() {
510            return Err(ParseError::new(
511                ParseErrorKind::InvalidSyntax("expected at least one universe name".to_string()),
512                self.current_span(),
513            ));
514        }
515        let span = start_span.merge(&self.current_span());
516        Ok(Command::Universe { names, span })
517    }
518    /// Parse `notation <prec>? <name> := <body>` or prefix/infix/postfix variant.
519    pub(super) fn parse_notation(&mut self, kind: NotationKind) -> Result<Command, ParseError> {
520        let start_span = self.current_span();
521        self.advance();
522        let prec = if let Some(token) = self.current() {
523            if let TokenKind::Nat(n) = &token.kind {
524                let p = *n as u32;
525                self.advance();
526                Some(p)
527            } else {
528                None
529            }
530        } else {
531            None
532        };
533        let name = if let Some(token) = self.current() {
534            match &token.kind {
535                TokenKind::String(s) => {
536                    let n = s.clone();
537                    self.advance();
538                    n
539                }
540                TokenKind::Ident(_) => self.parse_ident()?,
541                _ => {
542                    return Err(ParseError::new(
543                        ParseErrorKind::InvalidSyntax(
544                            "expected notation name or symbol".to_string(),
545                        ),
546                        token.span.clone(),
547                    ));
548                }
549            }
550        } else {
551            return Err(ParseError::new(
552                ParseErrorKind::UnexpectedEof {
553                    expected: vec!["notation name".to_string()],
554                },
555                self.eof_span(),
556            ));
557        };
558        let _ = self.consume(&TokenKind::Assign);
559        let body = self.collect_rest_as_string();
560        let span = start_span.merge(&self.current_span());
561        Ok(Command::Notation {
562            kind,
563            name,
564            prec,
565            body,
566            span,
567        })
568    }
569    /// Parse `derive <strategy1>, <strategy2> for <type_name>` or
570    /// `deriving <strategy> for <type_name>`.
571    pub(super) fn parse_derive(&mut self) -> Result<Command, ParseError> {
572        let start_span = self.current_span();
573        self.advance();
574        let mut strategies = Vec::new();
575        loop {
576            let strat = self.parse_ident()?;
577            if strat == "for" {
578                if strategies.is_empty() {
579                    return Err(ParseError::new(
580                        ParseErrorKind::InvalidSyntax(
581                            "expected strategy name before 'for'".to_string(),
582                        ),
583                        self.current_span(),
584                    ));
585                }
586                break;
587            }
588            strategies.push(strat);
589            if self.consume(&TokenKind::Comma) {
590                continue;
591            }
592            if self.check_ident("for") {
593                self.advance();
594                break;
595            }
596            break;
597        }
598        let type_name = self.parse_ident()?;
599        let span = start_span.merge(&self.current_span());
600        Ok(Command::Derive {
601            strategies,
602            type_name,
603            span,
604        })
605    }
606    /// Parse comma-separated identifiers (used inside `[...]`).
607    pub(super) fn parse_comma_separated_idents(&mut self) -> Result<Vec<String>, ParseError> {
608        let mut names = Vec::new();
609        if let Some(token) = self.current() {
610            if matches!(token.kind, TokenKind::RBracket) {
611                return Ok(names);
612            }
613        }
614        names.push(self.parse_ident()?);
615        while self.consume(&TokenKind::Comma) {
616            names.push(self.parse_ident()?);
617        }
618        Ok(names)
619    }
620    /// Parse `structure <name> [extends <base1>, <base2>] where [field decls] [deriving ...]`.
621    pub(super) fn parse_structure(&mut self) -> Result<Command, ParseError> {
622        let start_span = self.current_span();
623        self.advance();
624        let name = self.parse_ident()?;
625        let mut extends = Vec::new();
626        if self.check_ident("extends") {
627            self.advance();
628            extends.push(self.parse_ident()?);
629            while self.consume(&TokenKind::Comma) {
630                extends.push(self.parse_ident()?);
631            }
632        }
633        let mut fields = Vec::new();
634        let mut derives = Vec::new();
635        if self.check_keyword("where") {
636            self.advance();
637            fields = self.parse_structure_fields()?;
638        }
639        if self.check_ident("deriving") {
640            self.advance();
641            derives.push(self.parse_ident()?);
642            while self.consume(&TokenKind::Comma) {
643                derives.push(self.parse_ident()?);
644            }
645        }
646        let span = start_span.merge(&self.current_span());
647        Ok(Command::Structure {
648            name,
649            extends,
650            fields,
651            derives,
652            span,
653        })
654    }
655    /// Parse structure field declarations
656    pub(super) fn parse_structure_fields(&mut self) -> Result<Vec<StructureField>, ParseError> {
657        let mut fields = Vec::new();
658        while let Some(token) = self.current() {
659            if let TokenKind::Ident(_) = &token.kind {
660                if self.check_ident("deriving") {
661                    break;
662                }
663                let field_name = self.parse_ident()?;
664                self.expect(&TokenKind::Colon)?;
665                let ty = self.collect_type_expr()?;
666                let ty_str = match *ty {
667                    crate::Located {
668                        value: crate::SurfaceExpr::Var(ref s),
669                        ..
670                    } => s.clone(),
671                    _ => "unknown".to_string(),
672                };
673                let default = if self.consume(&TokenKind::Assign) {
674                    Some(self.collect_rest_as_string())
675                } else {
676                    None
677                };
678                fields.push(StructureField {
679                    name: field_name,
680                    ty: ty_str,
681                    is_explicit: true,
682                    default,
683                });
684                if !self.consume(&TokenKind::Comma) {
685                    break;
686                }
687            } else {
688                break;
689            }
690        }
691        Ok(fields)
692    }
693    /// Parse `class <name> [(<params>)] [extends <base>] where [methods]`.
694    pub(super) fn parse_class(&mut self) -> Result<Command, ParseError> {
695        let start_span = self.current_span();
696        self.advance();
697        let name = self.parse_ident()?;
698        let params = self.parse_binders()?;
699        let mut extends = Vec::new();
700        if self.check_ident("extends") {
701            self.advance();
702            extends.push(self.parse_ident()?);
703            while self.consume(&TokenKind::Comma) {
704                extends.push(self.parse_ident()?);
705            }
706        }
707        let mut fields = Vec::new();
708        if self.check_keyword("where") {
709            self.advance();
710            fields = self.parse_structure_fields()?;
711        }
712        let span = start_span.merge(&self.current_span());
713        Ok(Command::Class {
714            name,
715            params,
716            extends,
717            fields,
718            span,
719        })
720    }
721    /// Parse `instance [<name> :] <type> [priority <n>] := <body>` or `by <tactic>`.
722    pub(super) fn parse_instance(&mut self) -> Result<Command, ParseError> {
723        let start_span = self.current_span();
724        self.advance();
725        let name = if self.check_ident("_") {
726            self.advance();
727            "_".to_string()
728        } else {
729            self.parse_ident()?
730        };
731        self.expect(&TokenKind::Colon)?;
732        let mut ty_parts = Vec::new();
733        while let Some(token) = self.current() {
734            match &token.kind {
735                TokenKind::Assign | TokenKind::Eof => break,
736                TokenKind::Ident(s) if s == "priority" => break,
737                _ => {
738                    ty_parts.push(format!("{}", token.kind));
739                    self.advance();
740                }
741            }
742        }
743        let ty_str = ty_parts.join(" ");
744        let mut priority = None;
745        if self.check_ident("priority") {
746            self.advance();
747            if let Some(token) = self.current() {
748                if let TokenKind::Nat(n) = &token.kind {
749                    priority = Some(*n as u32);
750                    self.advance();
751                }
752            }
753        }
754        self.expect(&TokenKind::Assign)?;
755        let body = self.collect_rest_as_string();
756        let span = start_span.merge(&self.current_span());
757        Ok(Command::Instance {
758            name,
759            ty: ty_str,
760            priority,
761            body,
762            span,
763        })
764    }
765    /// Parse `attribute [<attr_name> <params>]` or `attribute [<attr>] <target>`.
766    #[allow(dead_code)]
767    pub(super) fn parse_attribute_decl(&mut self) -> Result<Command, ParseError> {
768        let start_span = self.current_span();
769        self.advance();
770        if !self.check(&TokenKind::LBracket) {
771            return Err(ParseError::new(
772                ParseErrorKind::InvalidSyntax("expected '[' after 'attribute'".to_string()),
773                self.current_span(),
774            ));
775        }
776        self.advance();
777        let attr_name = self.parse_ident()?;
778        let mut params = Vec::new();
779        while !self.check(&TokenKind::RBracket) && !self.at_end() {
780            if let Some(token) = self.current() {
781                if let TokenKind::Ident(_) = &token.kind {
782                    params.push(self.parse_ident()?);
783                } else {
784                    break;
785                }
786            } else {
787                break;
788            }
789        }
790        self.expect(&TokenKind::RBracket)?;
791        let kind = if attr_name.contains("macro") {
792            AttributeDeclKind::Macro
793        } else if attr_name.contains("builtin") {
794            AttributeDeclKind::Builtin
795        } else {
796            AttributeDeclKind::Simple
797        };
798        let span = start_span.merge(&self.current_span());
799        if let Some(token) = self.current() {
800            if let TokenKind::Ident(_) = &token.kind {
801                let target = self.parse_ident()?;
802                return Ok(Command::ApplyAttribute {
803                    attr_name,
804                    target,
805                    params,
806                    span,
807                });
808            }
809        }
810        Ok(Command::AttributeDecl {
811            name: attr_name,
812            kind,
813            span,
814        })
815    }
816}
oxilean_parse/command/commandparser_parsing.rs

oxilean_parse/command/
commandparser_parsing.rs
