litex-lang 0.9.88-beta

The Formal Way to Write Math as It Looks
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103

use crate::parse::parse_helpers::collect_forall_param_names_from_facts;
use crate::prelude::*;

impl Runtime {
    pub fn parse_claim_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
        tb.skip_token(CLAIM)?;
        if tb.current()? == COLON {
            Ok(self.parse_multiline_fact_claim(tb)?.into())
        } else {
            let fact = self.parse_header_fact_before_trailing_colon(
                tb,
                "claim",
                "claim => <fact>:",
                "claim <fact>:",
            )?;
            if matches!(&fact, Fact::ForallFactWithIff(_)) {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "claim multiline fact cannot be iff".to_string(),
                        tb.line_file.clone(),
                    ),
                )));
            }
            let names = collect_forall_param_names_from_facts(std::slice::from_ref(&fact));
            let lf = tb.line_file.clone();
            let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
                ParamObjType::Forall,
                &names,
                lf,
                |this| {
                    tb.body
                        .iter_mut()
                        .map(|b| this.parse_stmt(b))
                        .collect::<Result<_, _>>()
                },
            )?;
            Ok(ClaimStmt::new(fact, proof, tb.line_file.clone()).into())
        }
    }

    fn parse_multiline_fact_claim(
        &mut self,
        tb: &mut TokenBlock,
    ) -> Result<ClaimStmt, RuntimeError> {
        tb.skip_token(COLON)?;
        if tb.body.is_empty() {
            return Err(RuntimeError::from(ParseRuntimeError(
                RuntimeErrorStruct::new_with_msg_and_line_file(
                    "claim: expects a `prove:` block and optional proof body".to_string(),
                    tb.line_file.clone(),
                ),
            )));
        }
        let fact = {
            let first = tb.body.get_mut(0).ok_or_else(|| {
                RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "claim: expects a `prove:` block and optional proof body".to_string(),
                        tb.line_file.clone(),
                    ),
                ))
            })?;

            first.skip_token(PROVE)?;
            first.skip_token(COLON)?;

            let body_block = first.body.get_mut(0).ok_or_else(|| {
                RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "claim: `prove:` expects exactly one body block (the fact)".to_string(),
                        first.line_file.clone(),
                    ),
                ))
            })?;
            let f = self.parse_fact(body_block)?;
            if matches!(&f, Fact::ForallFactWithIff(_)) {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "claim multiline fact cannot be iff".to_string(),
                        first.line_file.clone(),
                    ),
                )));
            }
            Ok::<Fact, RuntimeError>(f)
        }?;

        let names = collect_forall_param_names_from_facts(std::slice::from_ref(&fact));
        let lf = tb.line_file.clone();
        let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
            ParamObjType::Forall,
            &names,
            lf,
            |this| {
                tb.body
                    .iter_mut()
                    .skip(1)
                    .map(|b| this.parse_stmt(b))
                    .collect::<Result<_, _>>()
            },
        )?;
        Ok(ClaimStmt::new(fact, proof, tb.line_file.clone()))
    }
}