litex/parse/by_stmt/
contra_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    /// `by contra:` then `prove:` block with exactly one atomic fact, optional proof statements, then `impossible` atomic fact.
5    ///
6    /// Shorthand: `by contra => atomic_goal:` embeds the goal on the header line; body is optional proof
7    /// statement blocks followed by `impossible ...` as the last block.
8    pub fn parse_by_contra_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
9        tb.skip_token(CONTRA)?;
10        let (to_prove, inline_arrow): (AtomicFact, bool) = if tb.current()? == RIGHT_ARROW {
11            tb.skip_token(RIGHT_ARROW)?;
12            let header = &tb.header;
13            if header.len() < tb.parse_index + 2 || header.last().map(|t| t.as_str()) != Some(COLON)
14            {
15                return Err(RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
16                    "by contra => ... : expected one atomic goal and a trailing `:` on the same line".to_string(),
17                    tb.line_file.clone(),
18                ))));
19            }
20            let colon_pos = header.len() - 1;
21            let fact_tokens = header[tb.parse_index..colon_pos].to_vec();
22            if fact_tokens.is_empty() {
23                return Err(RuntimeError::from(ParseRuntimeError(
24                    RuntimeErrorStruct::new_with_msg_and_line_file(
25                        "by contra => ... : expected a non-empty goal after `=>`".to_string(),
26                        tb.line_file.clone(),
27                    ),
28                )));
29            }
30            let mut fact_tb = TokenBlock::new(fact_tokens, vec![], tb.line_file.clone());
31            let atom = self.parse_atomic_fact(&mut fact_tb, true)?;
32            if !fact_tb.exceed_end_of_head() {
33                return Err(RuntimeError::from(ParseRuntimeError(
34                    RuntimeErrorStruct::new_with_msg_and_line_file(
35                        "by contra => ... : unfinished tokens in goal".to_string(),
36                        tb.line_file.clone(),
37                    ),
38                )));
39            }
40            tb.parse_index = colon_pos + 1;
41            if !tb.exceed_end_of_head() {
42                return Err(RuntimeError::from(ParseRuntimeError(
43                    RuntimeErrorStruct::new_with_msg_and_line_file(
44                        "by contra => ... : unexpected tokens after `:`".to_string(),
45                        tb.line_file.clone(),
46                    ),
47                )));
48            }
49            (atom, true)
50        } else {
51            tb.skip_token(COLON)?;
52            if !tb.exceed_end_of_head() {
53                return Err(RuntimeError::from(ParseRuntimeError(
54                    RuntimeErrorStruct::new_with_msg_and_line_file(
55                        "by contra: expected end of head after by contra:".to_string(),
56                        tb.line_file.clone(),
57                    ),
58                )));
59            }
60            if tb.body.len() < 2 {
61                return Err(RuntimeError::from(ParseRuntimeError(
62                    RuntimeErrorStruct::new_with_msg_and_line_file(
63                        "by contra: expects prove: block and impossible ... tail".to_string(),
64                        tb.line_file.clone(),
65                    ),
66                )));
67            }
68            let to_prove = {
69                let prove_block = tb.body.get_mut(0).ok_or_else(|| {
70                    RuntimeError::from(ParseRuntimeError(
71                        RuntimeErrorStruct::new_with_msg_and_line_file(
72                            "Expected body".to_string(),
73                            tb.line_file.clone(),
74                        ),
75                    ))
76                })?;
77                prove_block.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
78                if prove_block.body.len() != 1 {
79                    return Err(RuntimeError::from(ParseRuntimeError(
80                        RuntimeErrorStruct::new_with_msg_and_line_file(
81                            "by contra: prove: expects exactly one atomic fact block".to_string(),
82                            prove_block.line_file.clone(),
83                        ),
84                    )));
85                }
86                let atomic_fact_block = prove_block.body.get_mut(0).ok_or_else(|| {
87                    RuntimeError::from(ParseRuntimeError(
88                        RuntimeErrorStruct::new_with_msg_and_line_file(
89                            "Expected body".to_string(),
90                            prove_block.line_file.clone(),
91                        ),
92                    ))
93                })?;
94                self.parse_atomic_fact(atomic_fact_block, true)?
95            };
96            (to_prove, false)
97        };
98
99        let n = tb.body.len();
100        if inline_arrow {
101            if n < 1 {
102                return Err(RuntimeError::from(ParseRuntimeError(
103                    RuntimeErrorStruct::new_with_msg_and_line_file(
104                        "by contra => ... : expects a final `impossible ...` block in the body"
105                            .to_string(),
106                        tb.line_file.clone(),
107                    ),
108                )));
109            }
110        } else if n < 2 {
111            return Err(RuntimeError::from(ParseRuntimeError(
112                RuntimeErrorStruct::new_with_msg_and_line_file(
113                    "by contra: expects prove: block and impossible ... tail".to_string(),
114                    tb.line_file.clone(),
115                ),
116            )));
117        }
118
119        let proof_hi = n.saturating_sub(1);
120        let proof_lo = if inline_arrow { 0 } else { 1 };
121        let mut proof = Vec::new();
122        if proof_lo < proof_hi {
123            for block in tb.body[proof_lo..proof_hi].iter_mut() {
124                proof.push(self.parse_stmt(block)?);
125            }
126        }
127        let mut last_block = tb.body.last_mut().ok_or_else(|| {
128            RuntimeError::from(ParseRuntimeError(
129                RuntimeErrorStruct::new_with_msg_and_line_file(
130                    "Expected body".to_string(),
131                    tb.line_file.clone(),
132                ),
133            ))
134        })?;
135        last_block.skip_token(IMPOSSIBLE)?;
136        let impossible_fact = self.parse_atomic_fact(&mut last_block, true)?;
137        Ok(ByContraStmt::new(to_prove, proof, impossible_fact, tb.line_file.clone()).into())
138    }
139}
litex/parse/by_stmt/contra_by_stmt.rs

litex/parse/by_stmt/
contra_by_stmt.rs
