1use crate::prelude::*;
2
3use super::exec_have_fn_equal_shared::{
4 build_curried_function_obj_from_layers,
5 forall_binders_dom_and_curried_layers_from_fn_set_clause,
6};
7
8impl Runtime {
9 pub fn exec_have_fn_equal_stmt(
10 &mut self,
11 have_fn_equal_stmt: &HaveFnEqualStmt,
12 ) -> Result<StmtResult, RuntimeError> {
13 let fn_set_stored = self
14 .fn_set_from_fn_set_clause(&have_fn_equal_stmt.fn_set_clause)
15 .map_err(|e| {
16 short_exec_error(
17 have_fn_equal_stmt.clone().into(),
18 "have_fn_equal_stmt: build fn set for storage failed".to_string(),
19 Some(e),
20 vec![],
21 )
22 })?;
23
24 self.have_fn_equal_stmt_verify_well_defined(have_fn_equal_stmt, &fn_set_stored)
25 .map_err(|e| {
26 short_exec_error(
27 have_fn_equal_stmt.clone().into(),
28 "have_fn_equal_stmt: verify well-defined failed".to_string(),
29 Some(e),
30 vec![],
31 )
32 })?;
33
34 let infer_result =
35 self.store_have_fn_equal_stmt_facts(have_fn_equal_stmt, &fn_set_stored)?;
36
37 Ok(
38 (NonFactualStmtSuccess::new(have_fn_equal_stmt.clone().into(), infer_result, vec![]))
39 .into(),
40 )
41 }
42
43 fn have_fn_equal_stmt_forall_binders_dom_and_curried_layers(
44 &self,
45 clause: &FnSetClause,
46 ) -> Result<(ParamDefWithType, Vec<Fact>, Vec<Vec<String>>), RuntimeError> {
47 Ok(forall_binders_dom_and_curried_layers_from_fn_set_clause(
48 clause,
49 ))
50 }
51
52 fn store_have_fn_equal_stmt_facts(
53 &mut self,
54 have_fn_equal_stmt: &HaveFnEqualStmt,
55 fn_set_stored: &FnSet,
56 ) -> Result<InferResult, RuntimeError> {
57 self.store_free_param_or_identifier_name(
58 &have_fn_equal_stmt.name,
59 ParamObjType::Identifier,
60 )?;
61
62 let function_identifier_obj: Obj = Identifier::new(have_fn_equal_stmt.name.clone()).into();
63 let function_set_obj = fn_set_stored.clone().into();
64 let function_in_function_set_fact = InFact::new(
65 function_identifier_obj.clone(),
66 function_set_obj,
67 have_fn_equal_stmt.line_file.clone(),
68 )
69 .into();
70
71 let infer_result = self
72 .verify_well_defined_and_store_and_infer_with_default_verify_state(
73 function_in_function_set_fact,
74 )
75 .map_err(|store_fact_error| {
76 short_exec_error(
77 have_fn_equal_stmt.clone().into(),
78 "",
79 Some(store_fact_error),
80 vec![],
81 )
82 })?;
83
84 let stmt_lf = have_fn_equal_stmt.line_file.clone();
85 self.register_known_objs_in_fn_sets_for_element_body(
86 &function_identifier_obj,
87 fn_set_stored.body.clone(),
88 Some(have_fn_equal_stmt.equal_to.clone()),
89 stmt_lf.clone(),
90 stmt_lf,
91 );
92
93 let (param_defs_with_type, forall_dom_facts, curried_layers) = self
94 .have_fn_equal_stmt_forall_binders_dom_and_curried_layers(
95 &have_fn_equal_stmt.fn_set_clause,
96 )?;
97
98 let function_obj =
99 build_curried_function_obj_from_layers(&have_fn_equal_stmt.name, &curried_layers);
100
101 let function_equals_equal_to_fact: AtomicFact = EqualFact::new(
102 function_obj,
103 have_fn_equal_stmt.equal_to.clone(),
104 have_fn_equal_stmt.line_file.clone(),
105 )
106 .into();
107
108 let forall_fact = ForallFact::new(
109 param_defs_with_type,
110 forall_dom_facts,
111 vec![function_equals_equal_to_fact.into()],
112 have_fn_equal_stmt.line_file.clone(),
113 )?;
114
115 let to_store = self.inst_have_fn_forall_fact_for_store(forall_fact)?;
116
117 let _ = self
118 .verify_well_defined_and_store_and_infer_with_default_verify_state(to_store)
119 .map_err(|store_fact_error| {
120 short_exec_error(
121 have_fn_equal_stmt.clone().into(),
122 "",
123 Some(store_fact_error),
124 vec![],
125 )
126 })?;
127
128 Ok(infer_result)
129 }
130
131 fn have_fn_equal_stmt_verify_well_defined(
132 &mut self,
133 have_fn_equal_stmt: &HaveFnEqualStmt,
134 fn_set_stored: &FnSet,
135 ) -> Result<(), RuntimeError> {
136 self.run_in_local_env(|rt| {
137 rt.have_fn_equal_stmt_verify_well_defined_body(have_fn_equal_stmt, fn_set_stored)
138 })
139 }
140
141 fn have_fn_equal_stmt_verify_well_defined_body(
142 &mut self,
143 have_fn_equal_stmt: &HaveFnEqualStmt,
144 fn_set_stored: &FnSet,
145 ) -> Result<(), RuntimeError> {
146 let verify_state = VerifyState::new(0, false);
147
148 let function_set_obj = fn_set_stored.clone().into();
149 self.verify_obj_well_defined_and_store_cache(&function_set_obj, &verify_state)
150 .map_err(|well_defined_error| {
151 short_exec_error(
152 have_fn_equal_stmt.clone().into(),
153 "",
154 Some(well_defined_error),
155 vec![],
156 )
157 })?;
158
159 for param_def_with_set in have_fn_equal_stmt.fn_set_clause.params_def_with_set.iter() {
160 self.define_params_with_set(param_def_with_set)
161 .map_err(|define_params_error| {
162 short_exec_error(
163 have_fn_equal_stmt.clone().into(),
164 "",
165 Some(define_params_error),
166 vec![],
167 )
168 })?;
169 }
170
171 for dom_fact in have_fn_equal_stmt.fn_set_clause.dom_facts.iter() {
172 let _ = self
173 .store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
174 dom_fact.clone(),
175 )
176 .map_err(|store_fact_error| {
177 short_exec_error(
178 have_fn_equal_stmt.clone().into(),
179 "",
180 Some(store_fact_error),
181 vec![],
182 )
183 })?;
184 }
185
186 let mut ret_set = have_fn_equal_stmt.fn_set_clause.ret_set.clone();
187 let equal_to_for_in_fact = have_fn_equal_stmt.equal_to.clone();
188 while let Obj::FnSet(inner) = ret_set {
189 for param_def_with_set in inner.body.params_def_with_set.iter() {
190 self.define_params_with_set(param_def_with_set)
191 .map_err(|define_params_error| {
192 short_exec_error(
193 have_fn_equal_stmt.clone().into(),
194 "",
195 Some(define_params_error),
196 vec![],
197 )
198 })?;
199 }
200 for dom_fact in inner.body.dom_facts.iter() {
201 let _ = self
202 .store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
203 dom_fact.clone(),
204 )
205 .map_err(|store_fact_error| {
206 short_exec_error(
207 have_fn_equal_stmt.clone().into(),
208 "",
209 Some(store_fact_error),
210 vec![],
211 )
212 })?;
213 }
214 ret_set = (*inner.body.ret_set).clone();
215 }
216
217 let equal_to_in_ret_set_atomic_fact = InFact::new(
218 equal_to_for_in_fact.clone(),
219 ret_set.clone(),
220 have_fn_equal_stmt.line_file.clone(),
221 )
222 .into();
223 let verify_result = self
224 .verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
225 .map_err(|verify_error| {
226 short_exec_error(
227 have_fn_equal_stmt.clone().into(),
228 "",
229 Some(verify_error),
230 vec![],
231 )
232 })?;
233 if verify_result.is_unknown() {
234 let msg = format!(
235 "have_fn_equal_stmt: {} is not in return set {}",
236 equal_to_for_in_fact, ret_set
237 );
238 return Err(short_exec_error(
239 have_fn_equal_stmt.clone().into(),
240 msg,
241 None,
242 vec![],
243 ));
244 }
245
246 Ok(())
247 }
248}