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

litex/parse/by_stmt/
contra_by_stmt.rs
