litex-lang 0.9.75-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation
use crate::prelude::*;

impl Runtime {
    pub fn parse_by_struct_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
        tb.skip_token(STRUCT)?;
        let mut struct_bindings = Vec::new();
        let mut value_bindings = Vec::new();

        while tb.current()? != COLON {
            let name = tb.advance()?;
            if tb.current_token_is_equal_to(FROM) {
                tb.skip_token(FROM)?;
                let tuple = self.parse_obj(tb)?;
                tb.skip_token(AS)?;
                let struct_ty = self.parse_struct_type_after_as(tb)?;
                struct_bindings.push(ByStructBinding::new(name, tuple, struct_ty));
            } else if tb.current_token_is_equal_to(EQUAL) {
                tb.skip_token(EQUAL)?;
                let value = self.parse_obj(tb)?;
                value_bindings.push(ByStructValueBinding::new(name, value));
            } else {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "by struct: expected `from` or `=` after parameter name".to_string(),
                        tb.line_file.clone(),
                    ),
                )));
            }

            if tb.current_token_is_equal_to(COMMA) {
                tb.skip_token(COMMA)?;
            } else if tb.current()? != COLON {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "by struct: expected `,` or `:` after binding".to_string(),
                        tb.line_file.clone(),
                    ),
                )));
            }
        }
        tb.skip_token(COLON)?;
        if !tb.exceed_end_of_head() {
            return Err(RuntimeError::from(ParseRuntimeError(
                RuntimeErrorStruct::new_with_msg_and_line_file(
                    "by struct: unexpected tokens after `:`".to_string(),
                    tb.line_file.clone(),
                ),
            )));
        }
        if struct_bindings.is_empty() {
            return Err(RuntimeError::from(ParseRuntimeError(
                RuntimeErrorStruct::new_with_msg_and_line_file(
                    "by struct: expected at least one struct binding".to_string(),
                    tb.line_file.clone(),
                ),
            )));
        }
        if tb.body.len() != 1 {
            return Err(RuntimeError::from(ParseRuntimeError(
                RuntimeErrorStruct::new_with_msg_and_line_file(
                    "by struct: expects exactly one forall fact in the body".to_string(),
                    tb.line_file.clone(),
                ),
            )));
        }

        let fact = self.parse_fact(&mut tb.body[0])?;
        let forall_fact = match fact {
            Fact::ForallFact(f) => f,
            Fact::ForallFactWithIff(_) => {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "by struct: forall with `<=>` is not allowed here".to_string(),
                        tb.line_file.clone(),
                    ),
                )));
            }
            _ => {
                return Err(RuntimeError::from(ParseRuntimeError(
                    RuntimeErrorStruct::new_with_msg_and_line_file(
                        "by struct: body must be a single forall fact".to_string(),
                        tb.line_file.clone(),
                    ),
                )));
            }
        };

        Ok(ByStructStmt::new(
            struct_bindings,
            value_bindings,
            forall_fact,
            tb.line_file.clone(),
        )
        .into())
    }

    fn parse_struct_type_after_as(
        &mut self,
        tb: &mut TokenBlock,
    ) -> Result<StructAsParamType, RuntimeError> {
        let name = if tb.token_at_add_index(1) == MOD_SIGN {
            let mod_name = tb.advance()?;
            tb.skip_token(MOD_SIGN)?;
            let name = tb.advance()?;
            NameOrNameWithMod::new_name_with_mod(mod_name, name)
        } else {
            NameOrNameWithMod::new_name(tb.advance()?)
        };
        let args = if !tb.exceed_end_of_head() && tb.current_token_is_equal_to(LEFT_BRACE) {
            self.parse_braced_objs(tb)?
        } else {
            vec![]
        };
        Ok(StructAsParamType::new(name, args))
    }
}