litex/verify/
verify_arg_satisfy_param_def.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_obj_satisfies_param_type(
5        &mut self,
6        obj: Obj,
7        param_type: &ParamType,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        match param_type {
11            ParamType::Obj(set_obj) => {
12                let fact = InFact::new(obj, set_obj.clone(), default_line_file()).into();
13                self.verify_atomic_fact(&fact, verify_state)
14            }
15            ParamType::Set(_) => {
16                let fact = IsSetFact::new(obj, default_line_file()).into();
17                self.verify_atomic_fact(&fact, verify_state)
18            }
19            ParamType::NonemptySet(_) => {
20                let fact = IsNonemptySetFact::new(obj, default_line_file()).into();
21                self.verify_atomic_fact(&fact, verify_state)
22            }
23            ParamType::FiniteSet(_) => {
24                let fact = IsFiniteSetFact::new(obj, default_line_file()).into();
25                self.verify_atomic_fact(&fact, verify_state)
26            }
27        }
28    }
29
30    pub fn verify_args_satisfy_param_def_flat_types(
31        &mut self,
32        param_defs: &ParamDefWithType,
33        args: &Vec<Obj>,
34        verify_state: &VerifyState,
35        to_inst_param_type: ParamObjType,
36    ) -> Result<StmtResult, RuntimeError> {
37        let instantiated_types =
38            self.inst_param_def_with_type_one_by_one(param_defs, args, to_inst_param_type)?;
39        let flat_types = param_defs.flat_instantiated_types_for_args(&instantiated_types);
40        let mut infer_result = InferResult::new();
41        for (arg, param_type) in args.iter().zip(flat_types.iter()) {
42            let verify_result =
43                self.verify_obj_satisfies_param_type(arg.clone(), param_type, verify_state)?;
44            if verify_result.is_unknown() {
45                return Ok(verify_result);
46            }
47            match verify_result {
48                StmtResult::NonFactualStmtSuccess(x) => {
49                    infer_result.new_infer_result_inside(x.infers);
50                }
51                StmtResult::FactualStmtSuccess(x) => {
52                    infer_result.new_infer_result_inside(x.infers);
53                }
54                StmtResult::StmtUnknown(_) => unreachable!(),
55            }
56        }
57        Ok(NonFactualStmtSuccess::new(
58            DoNothingStmt::new(default_line_file()).into(),
59            infer_result,
60            Vec::new(),
61        )
62        .into())
63    }
64}
litex/verify/verify_arg_satisfy_param_def.rs

litex/verify/
verify_arg_satisfy_param_def.rs
