oxilean-parse 0.1.2

OxiLean parser - Concrete syntax to abstract syntax
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

//! # TacticParser - parsing Methods
//!
//! This module contains method implementations for `TacticParser`.
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use crate::{ParseError, TokenKind};

use super::types::{SimpArgs, TacticExpr};

use super::tacticparser_type::TacticParser;

impl<'a> TacticParser<'a> {
    /// Parse `simp`, `simp only [lem1, lem2]`, `simp [*]`, or `simp [lem1] {config}`
    pub(super) fn parse_simp(&mut self) -> Result<TacticExpr, ParseError> {
        self.advance();
        let only = if self.check_keyword("only") {
            self.advance();
            true
        } else {
            false
        };
        let lemmas = self.parse_simp_lemma_list()?;
        let config = self.parse_simp_config()?;
        Ok(TacticExpr::Simp(SimpArgs {
            only,
            lemmas,
            config,
        }))
    }
    pub(super) fn check_keyword(&self, kw: &str) -> bool {
        if let Some(token) = self.current() {
            matches!(& token.kind, TokenKind::Ident(s) if s == kw)
        } else {
            false
        }
    }
}