veripb/rules/
scope.rs

1use std::{fmt::Display, rc::Rc};
2
3use veripb_formula::prelude::DBConstraint;
4
5use crate::prelude::*;
6
7#[derive(Debug, Clone, Copy, PartialEq)]
8#[repr(u8)]
9pub enum ScopeId {
10    LessEqual = 0,
11    GreaterEqual = 1,
12}
13
14impl Display for ScopeId {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        match self {
17            ScopeId::LessEqual => write!(f, "leq"),
18            ScopeId::GreaterEqual => write!(f, "geq"),
19        }
20    }
21}
22
23#[derive(Debug)]
24pub struct ScopeRule {
25    id: ScopeId,
26}
27
28impl ScopeRule {
29    pub fn new(id: ScopeId) -> Self {
30        Self { id }
31    }
32}
33
34impl Rule for ScopeRule {
35    #[inline]
36    fn compute(
37        &mut self,
38        context: &mut Context,
39        database: &mut Database,
40    ) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
41        if let Some(Subcontext::Subproof(subproof_context)) = context.subcontexts.last_mut() {
42            let premises = if let Some(active_order) = &mut context.active_order {
43                match self.id {
44                    ScopeId::LessEqual => active_order.get_specification_less_equal(),
45                    ScopeId::GreaterEqual => {
46                        active_order.get_specification_greater_equal(&subproof_context.witness)
47                    }
48                }
49            } else {
50                vec![]
51            };
52
53            if subproof_context.current_scope.is_some() {
54                return Err(CheckingError::StartScopeWhileOtherScopeOpen);
55            }
56            subproof_context.scope_start_id = database.len();
57            subproof_context.current_scope = Some(self.id);
58
59            Ok(premises)
60        } else {
61            Err(CheckingError::ScopeOutsideSubproof)
62        }
63    }
64
65    #[inline]
66    fn is_subproof_friendly(&self) -> bool {
67        true
68    }
69
70    #[inline]
71    fn elaborate(
72        &self,
73        context: &mut Context,
74        _database: &Database,
75    ) -> Result<(), ElaborationError> {
76        let elaborator = context.elaborator.as_mut().unwrap();
77        elaborator.write("\tscope ");
78        elaborator.writeln(&self.id.to_string());
79        Ok(())
80    }
81}
veripb/rules/scope.rs

veripb/rules/
scope.rs
