litex-lang 0.9.68-beta

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

impl Runtime {
    pub fn define_params_with_set(
        &mut self,
        param_def: &ParamGroupWithSet,
    ) -> Result<InferResult, RuntimeError> {
        self.verify_obj_well_defined_and_store_cache(&param_def.set, &VerifyState::new(0, false))
            .map_err(|well_defined_error| {
                let param_names_text = param_def.params.join(", ");
                let error_line_file = well_defined_error.line_file().clone();
                RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new(
                    None,
                    format!(
                        "define params with set: failed to verify set well-defined for params [{}] with set {}",
                        param_names_text, param_def.set
                    ),
                    error_line_file,
                    Some(well_defined_error),
                    vec![],
                )))
            })?;
        let mut infer_result = InferResult::new();
        let facts = param_def.facts();
        for (name, fact) in param_def.params.iter().zip(facts.iter()) {
            self.store_free_param_or_identifier_name(name, ParamObjType::FnSet)
                .map_err(|runtime_error| {
                    RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new(
                        None,
                        format!(
                            "define params with set: failed to declare parameter `{}`",
                            name
                        ),
                        default_line_file(),
                        Some(runtime_error),
                        vec![],
                    )))
                })?;
            let fact_infer_result = self
                .verify_well_defined_and_store_and_infer_with_default_verify_state(fact.clone())
                .map_err(|store_fact_error| {
                    RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new(
                        None,
                        format!(
                            "define params with set: failed to store in-set fact for parameter `{}`",
                            name
                        ),
                        default_line_file(),
                        Some(store_fact_error),
                        vec![],
                    )))
                })?;
            infer_result.new_infer_result_inside(fact_infer_result);
        }
        Ok(infer_result)
    }
}