veripb/rules/
header.rs

1use std::rc::Rc;
2
3use logos::Lexer;
4use veripb_formula::prelude::DBConstraint;
5use veripb_parser::error::ParserError;
6
7use crate::prelude::*;
8
9#[derive(Debug)]
10pub struct HeaderRule;
11
12impl HeaderRule {
13    #[inline]
14    pub fn parse(lex: Lexer<RuleToken>, context: &mut Context) -> Result<Self, ParserError> {
15        let mut lex = lex.morph();
16        context.major_version = Some(IntegerToken::parse(&mut lex)? as u8);
17        // Skip the dot separating major and minor version.
18        lex.bump(1);
19        context.minor_version = Some(IntegerToken::parse(&mut lex)? as u8);
20
21        Ok(HeaderRule)
22    }
23}
24
25impl Rule for HeaderRule {
26    #[inline]
27    fn compute(
28        &mut self,
29        context: &mut Context,
30        _database: &mut Database,
31    ) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
32        if context.major_version.unwrap() < 2 {
33            return Err(CheckingError::UnsupportedProofVersion);
34        }
35        Ok(vec![])
36    }
37}
38
39#[cfg(test)]
40mod tests {
41    use logos::Logos;
42    use veripb_formula::prelude::VarNameManager;
43
44    use crate::{args::Args, context::Context, rules::RuleToken};
45
46    use super::HeaderRule;
47
48    #[test]
49    fn parse_version() {
50        let lex = RuleToken::lexer("2.1");
51        let mut context = Context::new(Args::default(), VarNameManager::default());
52
53        assert_eq!(context.major_version, None);
54        assert_eq!(context.minor_version, None);
55
56        HeaderRule::parse(lex, &mut context).unwrap();
57
58        assert_eq!(context.major_version, Some(2));
59        assert_eq!(context.minor_version, Some(1));
60    }
61}
veripb/rules/header.rs

veripb/rules/
header.rs
