1use crate::prelude::*;
2
3impl Runtime {
4 pub fn define_parameter_by_binding_param_type(
6 &mut self,
7 name: &str,
8 param_type: &ParamType,
9 binding_kind: ParamObjType,
10 ) -> Result<InferResult, RuntimeError> {
11 match param_type {
12 ParamType::Obj(obj) => match obj {
13 Obj::FamilyObj(family_ty) => {
14 self.define_parameter_by_binding_family(name, family_ty, binding_kind)
15 }
16 Obj::FiniteSeqSet(fs) => {
17 let fn_set = self.finite_seq_set_to_fn_set(fs, default_line_file());
18 let type_fact = InFact::new(
19 param_binding_element_obj_for_store(name.to_string(), binding_kind),
20 fn_set.into(),
21 default_line_file(),
22 )
23 .into();
24 self.verify_well_defined_and_store_and_infer_with_default_verify_state(
25 type_fact,
26 )
27 }
28 Obj::SeqSet(ss) => {
29 let fn_set = self.seq_set_to_fn_set(ss, default_line_file());
30 let type_fact = InFact::new(
31 param_binding_element_obj_for_store(name.to_string(), binding_kind),
32 fn_set.into(),
33 default_line_file(),
34 )
35 .into();
36 self.verify_well_defined_and_store_and_infer_with_default_verify_state(
37 type_fact,
38 )
39 }
40 Obj::MatrixSet(ms) => {
41 let fn_set = self.matrix_set_to_fn_set(ms, default_line_file());
42 let type_fact = InFact::new(
43 param_binding_element_obj_for_store(name.to_string(), binding_kind),
44 fn_set.into(),
45 default_line_file(),
46 )
47 .into();
48 self.verify_well_defined_and_store_and_infer_with_default_verify_state(
49 type_fact,
50 )
51 }
52 _ => self.define_parameter_by_binding_obj(name, obj, binding_kind),
53 },
54 ParamType::Set(set) => self.define_parameter_by_binding_set(name, set, binding_kind),
55 ParamType::NonemptySet(nonempty_set) => {
56 self.define_parameter_by_binding_nonempty_set(name, nonempty_set, binding_kind)
57 }
58 ParamType::FiniteSet(finite_set) => {
59 self.define_parameter_by_binding_finite_set(name, finite_set, binding_kind)
60 }
61 }
62 }
63
64 fn define_parameter_by_binding_family(
65 &mut self,
66 name: &str,
67 family_ty: &FamilyObj,
68 binding_kind: ParamObjType,
69 ) -> Result<InferResult, RuntimeError> {
70 self.infer_membership_in_family_for_param_binding(name, family_ty, binding_kind)
71 }
72
73 fn define_parameter_by_binding_obj(
74 &mut self,
75 name: &str,
76 obj: &Obj,
77 binding_kind: ParamObjType,
78 ) -> Result<InferResult, RuntimeError> {
79 let type_fact = InFact::new(
80 param_binding_element_obj_for_store(name.to_string(), binding_kind),
81 obj.clone(),
82 default_line_file(),
83 )
84 .into();
85 self.verify_well_defined_and_store_and_infer_with_default_verify_state(type_fact)
86 }
87
88 fn define_parameter_by_binding_set(
89 &mut self,
90 name: &str,
91 _set: &Set,
92 binding_kind: ParamObjType,
93 ) -> Result<InferResult, RuntimeError> {
94 let type_fact = IsSetFact::new(
95 param_binding_element_obj_for_store(name.to_string(), binding_kind),
96 default_line_file(),
97 )
98 .into();
99 self.verify_well_defined_and_store_and_infer_with_default_verify_state(type_fact)
100 }
101
102 fn define_parameter_by_binding_nonempty_set(
103 &mut self,
104 name: &str,
105 _nonempty_set: &NonemptySet,
106 binding_kind: ParamObjType,
107 ) -> Result<InferResult, RuntimeError> {
108 let type_fact = IsNonemptySetFact::new(
109 param_binding_element_obj_for_store(name.to_string(), binding_kind),
110 default_line_file(),
111 )
112 .into();
113 self.verify_well_defined_and_store_and_infer_with_default_verify_state(type_fact)
114 }
115
116 fn define_parameter_by_binding_finite_set(
117 &mut self,
118 name: &str,
119 _finite_set: &FiniteSet,
120 binding_kind: ParamObjType,
121 ) -> Result<InferResult, RuntimeError> {
122 let type_fact = IsFiniteSetFact::new(
123 param_binding_element_obj_for_store(name.to_string(), binding_kind),
124 default_line_file(),
125 )
126 .into();
127 self.verify_well_defined_and_store_and_infer_with_default_verify_state(type_fact)
128 }
129
130 pub fn define_params_with_type(
131 &mut self,
132 param_defs: &ParamDefWithType,
133 check_type_nonempty: bool,
134 binding_kind: ParamObjType,
135 ) -> Result<InferResult, RuntimeError> {
136 let mut infer_result = InferResult::new();
137 for param_def in param_defs.groups.iter() {
138 self.verify_param_type_well_defined(¶m_def.param_type, &VerifyState::new(0, false))
139 .map_err(|well_defined_error| {
140 let param_names_text = param_def.params.join(", ");
141 let error_line_file = well_defined_error.line_file().clone();
142 RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new(
143 None,
144 format!(
145 "define params with type: failed to verify type well-defined for params [{}] with type {}",
146 param_names_text, param_def.param_type
147 ),
148 error_line_file,
149 Some(well_defined_error),
150 vec![],
151 )))
152 })?;
153 self.verify_param_type_nonempty_if_required(¶m_def.param_type, check_type_nonempty)
154 .map_err(|inner_exec_error| {
155 let param_names_text = param_def.params.join(", ");
156 RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
157 "define params with type: nonempty check failed for params [{}] with type {}",
158 param_names_text, param_def.param_type
159 ), inner_exec_error)))
160 })?;
161
162 for name in param_def.params.iter() {
163 self.store_free_param_or_identifier_name(name, binding_kind)
164 .map_err(|runtime_error| {
165 RuntimeError::from(DefineParamsRuntimeError(
166 RuntimeErrorStruct::new_with_msg_and_cause(
167 format!(
168 "define params with type: failed to declare parameter `{}`",
169 name
170 ),
171 runtime_error,
172 ),
173 ))
174 })?;
175 let fact_infer_result = self
176 .define_parameter_by_binding_param_type(
177 name,
178 ¶m_def.param_type,
179 binding_kind,
180 )
181 .map_err(|runtime_error| {
182 RuntimeError::from(DefineParamsRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
183 "define params with type: failed to apply param type for parameter `{}` with type {}",
184 name, param_def.param_type
185 ), runtime_error)))
186 })?;
187 infer_result.new_infer_result_inside(fact_infer_result);
188 }
189 }
190 Ok(infer_result)
191 }
192}