1 | | % (c) 2009-2017 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(units_interpreter, [ |
6 | | units_find_transition/5, |
7 | | units_compute_expression/4, |
8 | | units_compute_expressions/4, |
9 | | units_check_boolean_expression/3, |
10 | | units_check_list_of_boolean_expressions/3, |
11 | | units_execute_statement/5, |
12 | | units_execute_statement2/6, |
13 | | top_in_results/1, |
14 | | top_in_parameters/1 |
15 | | ]). |
16 | | |
17 | | :- use_module(library(lists)). |
18 | | :- use_module(library(samsort)). |
19 | | |
20 | | :- use_module(probsrc(bmachine)). |
21 | | :- use_module(probsrc(error_manager)). |
22 | | :- use_module(probsrc(bsyntaxtree)). |
23 | | :- use_module(probsrc(b_interpreter)). |
24 | | :- use_module(probsrc(state_space)). |
25 | | :- use_module(probsrc(translate)). |
26 | | :- use_module(probsrc(store)). |
27 | | :- use_module(probsrc(btypechecker)). |
28 | | |
29 | | :- use_module(units_domain). |
30 | | :- use_module(units_interpreter_helpers). |
31 | | :- use_module(units_tools). |
32 | | :- use_module(unit_parser, [unit_args_to_list/2]). |
33 | | :- use_module(units). |
34 | | |
35 | | :- use_module(probsrc(tools),[assert_once/1]). |
36 | | |
37 | | :- use_module(probsrc(module_information)). |
38 | | :- module_info(group,plugin_units). |
39 | | :- module_info(description,'Units Plugin: Abstract Interpreter'). |
40 | | |
41 | | :- dynamic top_in_parameters/1, top_in_results/1. |
42 | | |
43 | | units_find_transition(Operation, StateBegin, StateTrans, Paras, Results) :- |
44 | ? | units_execute_top_level_operation(Operation, _, StateBegin, StateTransInter, Paras, Results, Path), |
45 | | Path \= precond(false), |
46 | | StateTransInter = StateTrans. |
47 | | |
48 | | units_execute_top_level_operation(Name,FullOperation,InState,NewState,Parameters,Results,Path) :- |
49 | ? | b_interpreter:try_get_op_name(FullOperation, Name), |
50 | ? | units_execute_operation(Name,FullOperation,InState,NewState,Parameters,Results,true,Path). |
51 | | |
52 | | units_execute_operation_with_parameters(Name,InState,Parameters,OutState,ResultValues,Path) :- |
53 | ? | (b_get_machine_operation(Name,_,_,_) |
54 | ? | -> units_execute_operation(Name,_,InState,OutState,Parameters,ResultValues,false,Path) |
55 | | ; add_error_fail(units_interpreter,'Unknown operation, cannot call: ',Name) |
56 | | ). |
57 | | |
58 | | units_execute_operation(Name,Operation,InState,NewOutState,ParaValues,ResultValues,TopLevel,Path) :- |
59 | ? | b_interpreter:b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,TopLevel), |
60 | ? | units_execute_operation(Name,Operation,InState,NewOutState,Body,Parameters,ParaValues,Results,ResultValues,TopLevel,Path). |
61 | | |
62 | | units_execute_operation(Name,RealFullOperation,InState,SortedStateFinish,Body,Parameters,ParameterValues,Results,ResultValues,TopLevel,Path) :- |
63 | ? | units_set_up_localstate(Parameters,ParameterValues,LocalState), |
64 | ? | units_set_up_undefined_localstate(Results,InState,NewInState), |
65 | | ( |
66 | ? | TopLevel==true |
67 | ? | -> units_execute_top_level_statement(Body,LocalState,NewInState,OutState,Path) |
68 | ? | ; units_execute_statement(Body,LocalState,NewInState,OutState,Path) |
69 | | ), |
70 | | l_expand_and_normalise_values(ParameterValues,NormalisedParameterValues,Parameters), |
71 | | Operation =.. [Name|NormalisedParameterValues], |
72 | | ( |
73 | | Results == [] |
74 | | -> RealFullOperation = Operation |
75 | | ; RealFullOperation = '-->'(Operation,ResultValues) |
76 | | ), |
77 | | units_get_results(Results,OutState,ResultValues,StateFinish), |
78 | | units_get_results(Parameters,LocalState,ParameterValues,_StateFinish), |
79 | | samsort(StateFinish,SortedStateFinish), |
80 | | % check if either the parameters or the results contain top and add error |
81 | ? | (contains_top(ResultValues) |
82 | | -> %member(nodeid(Position),Info), |
83 | | current_state_id(ID), get_texpr_info(Body,Info), |
84 | | member(nodeid(Position),Info), |
85 | | %translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr), |
86 | | units:units_error_context(Context), |
87 | | store_state_error(ID,abort_error(well_definedness_error, |
88 | | 'Result value has multiple units',Name, |
89 | | span_context(Position,Context)),_), |
90 | | assert_once(top_in_results(Name)) |
91 | | ; true), |
92 | ? | (contains_top(ParameterValues) |
93 | | -> %member(nodeid(Position),Info), |
94 | | current_state_id(ID), get_texpr_info(Body,Info), |
95 | | member(nodeid(Position),Info), |
96 | | %translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr), |
97 | | units:units_error_context(Context), |
98 | | store_state_error(ID,abort_error(well_definedness_error, |
99 | | 'Parameter value has multiple units',Name, |
100 | | span_context(Position,Context)),_), |
101 | | assert_once(top_in_parameters(Name)) |
102 | | ; true). |
103 | | |
104 | | units_get_results([],OutState,[],OutState). |
105 | | units_get_results([R|Results],OutState,[NRV|ResultValues],NewOutState) :- |
106 | | def_get_texpr_id(R,ResultId), |
107 | | selectchk(bind(ResultId,NRV),OutState,OutState2), |
108 | | units_get_results(Results,OutState2,ResultValues,NewOutState). |
109 | | units_execute_top_level_statement(TExpr,LocalState,InState,OutState,Path) :- |
110 | ? | get_texpr_expr(TExpr,Stmt), |
111 | ? | units_execute_top_level_statement2(Stmt,TExpr,LocalState,InState,OutState,Path). |
112 | | units_execute_top_level_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :- |
113 | | !, units_check_boolean_expression(PreCond,LocalState,InState), |
114 | | units_execute_statement(Body,LocalState,InState,OutState,Path). |
115 | | units_execute_top_level_statement2(_,TExpr,LocalState,InState,OutState,Path) :- |
116 | ? | units_execute_statement(TExpr,LocalState,InState,OutState,Path). |
117 | | |
118 | | units_execute_statement(b(Stmt,_,Infos),LocalState,InState,OutState,Path) :- |
119 | ? | units_execute_statement2(Stmt, Infos, LocalState,InState, OutState, Path). |
120 | | units_execute_statement2(rlevent(_Name,_Section,_Status,_Params,_Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents), |
121 | | _Infos,LocalState,InState,OutState,eventb(Path)) :- !, |
122 | | execute_eventb_list(Actions,LocalState,InState,OutState,Path). |
123 | | units_execute_statement2(assign_single_id(IDE,Expr),_Infos,LocalState,InState,OutState,assign) :- |
124 | ? | get_texpr_id(IDE,ID),!, |
125 | ? | units_compute_expression(Expr,LocalState,InState,Value), |
126 | | state_store(bind(ID,Value),InState,OutState). |
127 | | units_execute_statement2(assign(VarExprs, ValExprs), _Infos,LocalState,InState,OutState,assign) :- |
128 | ? | !, units_compute_expressions(ValExprs, LocalState, InState, ValExprs2), |
129 | | assign_vars(VarExprs, ValExprs2, LocalState, InState, NewVars, NewVals), |
130 | | assign_vals_to_vars(NewVars, NewVals, StoreList), |
131 | | state_store_list(StoreList, InState, OutState). |
132 | | units_execute_statement2(parallel(Statements),_Infos,LocalState,InState,OutState,parallel(Paths)) :- |
133 | ? | !, execute_statements_in_parallel(Statements, LocalState, InState, OutState, Paths). |
134 | | units_execute_statement2(skip,_Infos,_LocalState,InState,InState,skip) :- !. |
135 | | units_execute_statement2(any(Parameters,PreCond,Body),_Infos,LocalState,InState,OutState,any(Bindings,Path)) :- |
136 | | !, units_set_up_localstate(Parameters,Bindings,ParameterState), |
137 | | append(ParameterState,LocalState,NewLocalState), |
138 | | units_check_boolean_expression(PreCond,NewLocalState,InState), |
139 | | units_execute_statement(Body,NewLocalState,InState,OutState,Path). |
140 | | units_execute_statement2(if(IfList),_Infos,LocalState,InState,OutState,if) :- |
141 | | !, execute_else_list(IfList,LocalState,InState,OutState). |
142 | | units_execute_statement2(select(SelectList),_Infos,LocalState,InState,OutState,select) :- |
143 | | !, execute_select_list(SelectList,LocalState,InState,OutState). |
144 | | units_execute_statement2(select(Whens,Else),Infos,LocalState,InState,OutState,select(PathWhens,PathElse)) :- !, |
145 | | units_execute_statement2(select(Whens),Infos,LocalState,InState,IntermediateState,PathWhens), |
146 | | findall(PC,(member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds), |
147 | | units_check_list_of_boolean_expressions(AllPreconds,LocalState,InState), |
148 | | units_execute_statement(Else,LocalState,IntermediateState,OutState,PathElse). |
149 | | units_execute_statement2(becomes_element_of(Element,Expression),_Infos,LocalState,InState,OutState,becomes_element_of) :- |
150 | | !, Element=[b(identifier(ID),_,_)], |
151 | | units_compute_expression(Expression,LocalState,InState,Value), |
152 | | Value = set(Inner), |
153 | | state_store(bind(ID,Inner),InState,OutState). |
154 | | units_execute_statement2(becomes_such(Vars,Condition),_,LocalState,InState,OutState,becomes_such) :- !, |
155 | | units_set_up_localstate(Vars,_Bindings,VarsState), |
156 | | state_store_list(VarsState, InState, OutState), |
157 | | insert_before_substitution_variables(Vars,LocalState,InState,OutState,TempLocalState), |
158 | | units_check_boolean_expression(Condition,TempLocalState,OutState). |
159 | | units_execute_statement2(operation_call(Operation,Results,Parameters),_,LocalState,InState,OutState, |
160 | ? | operation_call(OperationName,ParamValues,ResultValues,InnerPath)) :- !, |
161 | ? | def_get_texpr_id(Operation,op(OperationName)), |
162 | ? | units_compute_expressions(Parameters,LocalState,InState,ParamValues), |
163 | ? | units_execute_operation_with_parameters(OperationName,InState,ParamValues,OpOutState,ResultValues,InnerPath), |
164 | | b_interpreter:split_names_and_types(Results,ResultingIDs,_), |
165 | | assign_vals_to_vars(ResultingIDs, ResultValues, ResultsOutState), |
166 | | merge_non_overriding_states(ResultsOutState,OpOutState,OutState). |
167 | ? | units_execute_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :- !, |
168 | ? | units_check_boolean_expression(PreCond,LocalState,InState), |
169 | ? | Path=pre(IPath), |
170 | ? | units_execute_statement(Body,LocalState,InState,OutState,IPath). |
171 | | units_execute_statement2(case(Expression,Cases,Else),_,LocalState,InState,OutState,case) :- !, |
172 | | units_compute_expression(Expression,LocalState,InState,EValue), |
173 | | execute_cases_list(EValue,Cases,LocalState,InState,OutStateTmp), |
174 | | units_execute_statement(Else,LocalState,OutStateTmp,OutState,_Path). |
175 | ? | units_execute_statement2(var(Parameters,Body),_Infos,LocalState,InState,NewOutState,var(Path)) :- !, |
176 | ? | units_set_up_undefined_localstate(Parameters,InState,NewInState), |
177 | ? | b_interpreter:split_names_and_types(Parameters,Names,_), |
178 | ? | store:delete_variables_from_state(Names,LocalState,NewLocalState), |
179 | ? | units_execute_statement(Body,NewLocalState,NewInState,OutState,Path), |
180 | | units_get_results(Parameters,OutState,_ResultValues,NewOutState). |
181 | | units_execute_statement2(choice(ChoiceList),_,LocalState,InState,OutState,choice) :- !, |
182 | | execute_choice_list(ChoiceList,LocalState,InState,OutState). |
183 | | units_execute_statement2(let(Parameters,Defs,Body),_Infos,LocalState,InState,OutState,let(Path)) :- !, |
184 | | units_set_up_localstate(Parameters,_ParaValues,LetLocalState), |
185 | | append(LetLocalState,LocalState,ExtendedLocalState), |
186 | | units_check_boolean_expression(Defs,ExtendedLocalState,InState), |
187 | | units_execute_statement(Body,ExtendedLocalState,InState,OutState,Path). |
188 | ? | units_execute_statement2(sequence(Seq),_Infos,LocalState,InState,OutUpdates,Path) :- !, |
189 | ? | ( Seq = [First|Rest] -> |
190 | ? | (Rest == [] -> units_execute_statement(First,LocalState,InState,OutUpdates,Path) |
191 | ? | ; execute_sequence(First,sequence(Rest),LocalState,InState,OutUpdates,Path) |
192 | | ) |
193 | | ; Seq = [] -> OutUpdates = [], Path=[] |
194 | | ; add_error_fail(units_execute_statement2,'Illegal argument to sequence: ',Seq)). |
195 | | units_execute_statement2(while(Cond,Stmt,_Inv,_Variant),_,LocalState,InState,OutState,while) :- !, |
196 | | execute_while(Cond,Stmt,LocalState,InState,OutState). |
197 | | units_execute_statement2(Stmt,_Infos,LocalState,InState,_OutState,_Path) :- |
198 | | !, add_error_fail(units_execute_statement2, 'Statement not implemented: ', [Stmt,LocalState,InState]). |
199 | | |
200 | | % Computation of expressions |
201 | | |
202 | ? | units_compute_expression(b(Expr,Type,Info),LS,S,R) :- !, |
203 | ? | units_compute_expression2(Expr,Type,Info,LS,S,R), |
204 | ? | (contains_top(R) |
205 | ? | -> current_state_id(ID), |
206 | ? | member(nodeid(Position),Info), |
207 | | translate_bexpression(b(Expr,Type,Info), PPExpr), |
208 | | units:units_error_context(Context), |
209 | | store_state_error(ID,abort_error(well_definedness_error, |
210 | | 'Wrong usage of units in expression',PPExpr, |
211 | | span_context(Position,Context)),_) |
212 | | ; true). |
213 | | |
214 | | units_compute_expressions([], _, _, []). |
215 | | units_compute_expressions([EXPRsHd|EXPRsTl],LocalState,InState,[ValHd|ValTl]) :- |
216 | ? | units_compute_expression(EXPRsHd,LocalState,InState,ValHd), |
217 | ? | units_compute_expressions(EXPRsTl,LocalState,InState,ValTl). |
218 | | |
219 | | units_compute_expression2(boolean_true,_Type,_Info,_LocalState,_State,boolean(_)) :- !. |
220 | | units_compute_expression2(boolean_false,_Type,_Info,_LocalState,_State,boolean(_)) :- !. |
221 | | units_compute_expression2(min_int,_Type,_Info,_LocalState,_State,integer(_)) :- !. |
222 | | units_compute_expression2(max_int,_Type,_Info,_LocalState,_State,integer(_)) :- !. |
223 | | units_compute_expression2(empty_set,Type,Info,_LocalState,_State,Result) :- |
224 | | !, b_type_to_internal_type(Type,Info,Result). |
225 | | units_compute_expression2(bool_set,_Type,_Info,_LocalState,_State,set(boolean(_))) :- !. |
226 | | units_compute_expression2(string_set,_Type,_Info,_LocalState,_State,set(string(_))) :- !. |
227 | | units_compute_expression2(convert_bool(Arg1),_Type,_Info,LocalState,State,boolean(_)) :- |
228 | | !, units_check_boolean_expression(Arg1,LocalState,State). |
229 | | units_compute_expression2(add(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :- |
230 | ? | !, units_compute_expression(Arg1,LocalState,State,integer(SV1)), |
231 | ? | units_compute_expression(Arg2,LocalState,State,integer(SV2)), |
232 | ? | units_compute_expression(Arg2,LocalState,State,integer(SV2)), |
233 | | ( |
234 | ? | member(conversion,Info) |
235 | | -> ( |
236 | ? | (var(SV1) |
237 | | -> units_domain_addition_conversion(Arg1,SV2,Value), ! |
238 | ? | ; units_domain_addition_conversion(Arg2,SV1,Value), ! |
239 | | ) |
240 | ? | ; !, member(nodeid(Position),Info), |
241 | | current_state_id(ID), |
242 | | translate_bexpression(b(add(Arg1,Arg2),integer,Info), PPExpr), |
243 | | units:units_error_context(Context), |
244 | | store_state_error(ID,abort_error(well_definedness_error, |
245 | | 'Wrong usage of conversion',PPExpr, |
246 | | span_context(Position,Context)),_) |
247 | | ) |
248 | | ; lub(SV1,SV2,Value) |
249 | | ). |
250 | | units_compute_expression2(minus(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :- |
251 | ? | !, units_compute_expression(Arg1,LocalState,State,integer(SV1)), |
252 | ? | units_compute_expression(Arg2,LocalState,State,integer(SV2)), |
253 | | ( |
254 | ? | member(conversion,Info) |
255 | | -> ( |
256 | | (var(SV1) |
257 | | -> units_domain_subtraction_conversion(Arg1,SV2,Value), ! |
258 | ? | ; units_domain_subtraction_conversion(Arg2,SV1,Value), ! |
259 | | ) |
260 | | ; !, member(nodeid(Position),Info), |
261 | | current_state_id(ID), |
262 | | translate_bexpression(b(minus(Arg1,Arg2),integer,Info), PPExpr), |
263 | | units:units_error_context(Context), |
264 | | store_state_error(ID,abort_error(well_definedness_error, |
265 | | 'Wrong usage of conversion',PPExpr, |
266 | | span_context(Position,Context)),_) |
267 | | ) |
268 | | ; lub(SV1,SV2,Value) |
269 | | ). |
270 | | units_compute_expression2(unary_minus(Arg1),integer,_Info,LocalState,State,Arg2) :- |
271 | ? | !, units_compute_expression(Arg1,LocalState,State,Arg2). |
272 | | units_compute_expression2(multiplication(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :- |
273 | ? | !, |
274 | ? | units_compute_expression(Arg1,LocalState,State,integer(SV1)), |
275 | ? | units_compute_expression(Arg2,LocalState,State,integer(SV2)), |
276 | | ( |
277 | ? | member(conversion,Info) |
278 | | -> ( |
279 | ? | (var(SV1) |
280 | ? | -> units_domain_multiplication_conversion(Arg1,SV2,Value), ! |
281 | ? | ; units_domain_multiplication_conversion(Arg2,SV1,Value), ! |
282 | | ) |
283 | ? | ; !, member(nodeid(Position),Info), |
284 | | current_state_id(ID), |
285 | | translate_bexpression(b(multiplication(Arg1,Arg2),integer,Info), PPExpr), |
286 | | units:units_error_context(Context), |
287 | | store_state_error(ID,abort_error(well_definedness_error, |
288 | | 'Wrong usage of conversion',PPExpr, |
289 | | span_context(Position,Context)),_) |
290 | | ) |
291 | | ; units_domain_multiplication(SV1,SV2,Value) |
292 | | ). |
293 | | units_compute_expression2(cartesian_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
294 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
295 | | units_compute_expression(Arg2,LocalState,State,SV2), |
296 | | SV1 = set(C1), SV2 = set(C2), Value = set(couple(C1,C2)). |
297 | | units_compute_expression2(div(Arg1,Arg2),integer,Info,LocalState,State,integer(Value)) :- |
298 | ? | !, |
299 | ? | units_compute_expression(Arg1,LocalState,State,integer(SV1)), |
300 | ? | units_compute_expression(Arg2,LocalState,State,integer(SV2)), |
301 | | ( |
302 | ? | member(conversion,Info) |
303 | | -> ( |
304 | | (var(SV1) |
305 | | -> units_domain_division_conversion(Arg1,SV2,Value), ! |
306 | ? | ; units_domain_division_conversion(Arg2,SV1,Value), ! |
307 | | ) |
308 | | ; !, member(nodeid(Position),Info), |
309 | | current_state_id(ID), |
310 | | translate_bexpression(b(div(Arg1,Arg2),integer,Info), PPExpr), |
311 | | units:units_error_context(Context), |
312 | | store_state_error(ID,abort_error(well_definedness_error, |
313 | | 'Wrong usage of conversion',PPExpr, |
314 | | span_context(Position,Context)),_) |
315 | | ) |
316 | | ; units_domain_division(SV1,SV2,Value) |
317 | | ). |
318 | | units_compute_expression2(modulo(Arg1,_Arg2),integer,_Info,LocalState,State,SV1) :- |
319 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1). |
320 | | units_compute_expression2(power_of(Arg1,Arg2),integer,_Info,LocalState,State,integer(Value)) :- |
321 | ? | !, units_compute_expression(Arg1,LocalState,State,integer(SV1)), |
322 | | units_domain_power_of(SV1,Arg2,Value). |
323 | | units_compute_expression2(min(Arg1),_Type,_Info,LocalState,State,Value) :- |
324 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1), |
325 | | SV1 = set(Value). |
326 | | units_compute_expression2(max(Arg1),_Type,_Info,LocalState,State,Value) :- |
327 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1), |
328 | | SV1 = set(Value). |
329 | | units_compute_expression2(card(_Arg1),integer,_Info,_LocalState,_State,integer([])) :- !. |
330 | | units_compute_expression2(couple(Arg1,Arg2),_Type,_Info,LocalState,State,couple(SV1,SV2)) :- |
331 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
332 | | units_compute_expression(Arg2,LocalState,State,SV2). |
333 | | units_compute_expression2(pow_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :- |
334 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
335 | | units_compute_expression2(pow1_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :- |
336 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
337 | | units_compute_expression2(fin_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :- |
338 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
339 | | units_compute_expression2(fin1_subset(Arg1),_X,_Info,LocalState,State,set(SV1)) :- |
340 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
341 | | units_compute_expression2(interval(Arg1,Arg2),set(integer),_Info,LocalState,State,set(Value)) :- |
342 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1), |
343 | ? | units_compute_expression(Arg2,LocalState,State,SV2), |
344 | | lub(SV1,SV2,Value). |
345 | | units_compute_expression2(union(Arg1,Arg2),set(_X),_Info,LocalState,State,set(Value)) :- |
346 | | !, units_compute_expression(Arg1,LocalState,State,set(SV1)), |
347 | | units_compute_expression(Arg2,LocalState,State,set(SV2)), |
348 | | lub(SV1,SV2,Value). |
349 | | units_compute_expression2(intersection(Arg1,Arg2),set(_X),_Info,LocalState,State,set(Value)) :- |
350 | | !, units_compute_expression(Arg1,LocalState,State,set(SV1)), |
351 | | units_compute_expression(Arg2,LocalState,State,set(SV2)), |
352 | | lub(SV1,SV2,Value). |
353 | | units_compute_expression2(set_subtraction(Arg1,Arg2),_X,_Info,LocalState,State,Value) :- |
354 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
355 | | units_compute_expression(Arg2,LocalState,State,SV2), |
356 | | lub(SV1,SV2,Value). |
357 | | units_compute_expression2(general_union(Arg1),_X,_Info,LocalState,State,Value) :- |
358 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
359 | | SV1 = set(set(A)), Value = set(A). |
360 | | units_compute_expression2(general_intersection(Arg1),_X,_Info,LocalState,State,Value) :- |
361 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
362 | | SV1 = set(set(A)), Value = set(A). |
363 | | units_compute_expression2(relations(Arg1,Arg2),_X,_Info,LocalState,State,Value) :- |
364 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
365 | | units_compute_expression(Arg2,LocalState,State,SV2), |
366 | | units_domain_relation(SV1,SV2,Value). |
367 | | units_compute_expression2(reverse(Arg1),_X,_Info,LocalState,State,Value) :- |
368 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
369 | | SV1 = set(couple(A,B)), |
370 | | Value = set(couple(B,A)). |
371 | | units_compute_expression2(concat(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
372 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
373 | | units_compute_expression(Arg2,LocalState,State,SV2), |
374 | | lub(SV1,SV2,Value). |
375 | | units_compute_expression2(insert_front(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
376 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
377 | | units_compute_expression(Arg2,LocalState,State,SV2), |
378 | | lub(set(couple(integer(_),SV1)),SV2,Value). |
379 | | units_compute_expression2(insert_tail(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
380 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
381 | | units_compute_expression(Arg2,LocalState,State,SV2), |
382 | | lub(SV1,set(couple(integer(_),SV2)),Value). |
383 | | units_compute_expression2(general_concat(Arg1),_X,_Info,LocalState,State,Value) :- |
384 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
385 | | SV1 = set(couple(integer(_),set(couple(integer(_),A)))), Value = set(couple(integer(_),A)). |
386 | | units_compute_expression2(composition(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
387 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
388 | | units_compute_expression(Arg2,LocalState,State,SV2), |
389 | | SV1 = set(couple(A,B1)), SV2 = set(couple(B2,C)), |
390 | | same_units(B1,B2), Value = set(couple(A,C)). |
391 | | units_compute_expression2(direct_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
392 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
393 | | units_compute_expression(Arg2,LocalState,State,SV2), |
394 | | SV1 = set(couple(A1,B)), SV2 = set(couple(A2,C)), |
395 | | lub(A1,A2,A3), |
396 | | Value = set(couple(A3,couple(B,C))). |
397 | | units_compute_expression2(parallel_product(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
398 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
399 | | units_compute_expression(Arg2,LocalState,State,SV2), |
400 | | SV1 = set(couple(A,B)), SV2 = set(couple(C,D)), |
401 | | Value = set(couple(couple(A,C),couple(B,D))). |
402 | | units_compute_expression2(domain(Arg1),_Type,_Info,LocalState,State,set(Value)) :- |
403 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
404 | | SV1 = set(couple(Value,_X)). |
405 | | units_compute_expression2(range(Arg1),_Type,_Info,LocalState,State,set(Value)) :- |
406 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
407 | | SV1 = set(couple(_X,Value)). |
408 | | units_compute_expression2(image(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
409 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
410 | | units_compute_expression(Arg2,LocalState,State,SV2), |
411 | | SV1 = set(couple(A1,Image)), SV2 = set(A2), |
412 | | same_units(A1,A2), Value=set(Image). |
413 | | units_compute_expression2(domain_restriction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
414 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
415 | | units_compute_expression(Arg2,LocalState,State,SV2), |
416 | | SV1 = set(A1), SV2 = set(couple(A2,B)), |
417 | | lub(A1,A2,A3), Value=set(couple(A3,B)). |
418 | | units_compute_expression2(domain_subtraction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
419 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
420 | | units_compute_expression(Arg2,LocalState,State,SV2), |
421 | | SV1 = set(A1), SV2 = set(couple(A2,B)), |
422 | | lub(A1,A2,A3), Value=set(couple(A3,B)). |
423 | | units_compute_expression2(range_restriction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
424 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
425 | | units_compute_expression(Arg2,LocalState,State,SV2), |
426 | | SV1 = set(couple(A,B1)), SV2 = set(B2), |
427 | | lub(B1,B2,B3), Value=set(couple(A,B3)). |
428 | | units_compute_expression2(range_subtraction(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
429 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
430 | | units_compute_expression(Arg2,LocalState,State,SV2), |
431 | | SV1 = set(couple(A,B1)), SV2 = set(B2), |
432 | | lub(B1,B2,B3), Value=set(couple(A,B3)). |
433 | | units_compute_expression2(overwrite(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
434 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
435 | | units_compute_expression(Arg2,LocalState,State,SV2), |
436 | | lub(SV1,SV2,Value). |
437 | | units_compute_expression2(partial_function(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
438 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
439 | | units_compute_expression(Arg2,LocalState,State,SV2), |
440 | | units_domain_relation(SV1,SV2,Value). |
441 | | units_compute_expression2(total_function(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
442 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
443 | | units_compute_expression(Arg2,LocalState,State,SV2), |
444 | | units_domain_relation(SV1,SV2,Value). |
445 | | units_compute_expression2(partial_injection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
446 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
447 | | units_compute_expression(Arg2,LocalState,State,SV2), |
448 | | units_domain_relation(SV1,SV2,Value). |
449 | | units_compute_expression2(total_injection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
450 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
451 | | units_compute_expression(Arg2,LocalState,State,SV2), |
452 | | units_domain_relation(SV1,SV2,Value). |
453 | | units_compute_expression2(partial_surjection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
454 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
455 | | units_compute_expression(Arg2,LocalState,State,SV2), |
456 | | units_domain_relation(SV1,SV2,Value). |
457 | | units_compute_expression2(total_surjection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
458 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
459 | | units_compute_expression(Arg2,LocalState,State,SV2), |
460 | | units_domain_relation(SV1,SV2,Value). |
461 | | units_compute_expression2(total_bijection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
462 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
463 | | units_compute_expression(Arg2,LocalState,State,SV2), |
464 | | units_domain_relation(SV1,SV2,Value). |
465 | | units_compute_expression2(partial_bijection(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
466 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
467 | | units_compute_expression(Arg2,LocalState,State,SV2), |
468 | | units_domain_relation(SV1,SV2,Value). |
469 | | units_compute_expression2(total_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
470 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
471 | | units_compute_expression(Arg2,LocalState,State,SV2), |
472 | | units_domain_relation(SV1,SV2,Value). |
473 | | units_compute_expression2(surjection_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
474 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
475 | | units_compute_expression(Arg2,LocalState,State,SV2), |
476 | | units_domain_relation(SV1,SV2,Value). |
477 | | units_compute_expression2(total_surjection_relation(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
478 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
479 | | units_compute_expression(Arg2,LocalState,State,SV2), |
480 | | units_domain_relation(SV1,SV2,Value). |
481 | | units_compute_expression2(seq(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
482 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
483 | | SV1 = set(V). |
484 | | units_compute_expression2(seq1(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
485 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
486 | | SV1 = set(V). |
487 | | units_compute_expression2(iset(couple(integer(_),Arg1)),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
488 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
489 | | SV1 = set(V). |
490 | | units_compute_expression2(iseq(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
491 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
492 | | SV1 = set(V). |
493 | | units_compute_expression2(iseq1(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
494 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
495 | | SV1 = set(V). |
496 | | units_compute_expression2(perm(Arg1),_Type,_Info,LocalState,State,set(set(couple(integer(_),V)))) :- |
497 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
498 | | SV1 = set(V). |
499 | | units_compute_expression2(empty_sequence,Type,Info,_LocalState,_State,Result) :- |
500 | | !, b_type_to_internal_type(Type,Info,Result). |
501 | | units_compute_expression2(size(_Arg1),_Type,_Info,_LocalState,_State,integer([])) :- !. |
502 | | units_compute_expression2(first(Arg1),_Type,_Info,LocalState,State,V) :- |
503 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
504 | | SV1 = set(couple(integer(_),V)). |
505 | | units_compute_expression2(last(Arg1),_Type,_Info,LocalState,State,V) :- |
506 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
507 | | SV1 = set(couple(integer(_),V)). |
508 | | units_compute_expression2(front(Arg1),_Type,_Info,LocalState,State,SV1) :- |
509 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
510 | | units_compute_expression2(tail(Arg1),_Type,_Info,LocalState,State,SV1) :- |
511 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
512 | | units_compute_expression2(rev(Arg1),_Type,_Info,LocalState,State,SV1) :- |
513 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
514 | | units_compute_expression2(concat(Arg1,Arg2),_Type,_Info,LocalState,State,Value) :- |
515 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
516 | | units_compute_expression(Arg2,LocalState,State,SV2), |
517 | | lub(SV1,SV2,Value). |
518 | | units_compute_expression2(function(Function,Arg),_Type,_Info,LocalState,State,Value) :- |
519 | | !, units_compute_expression(Function,LocalState,State,FValue), |
520 | | units_compute_expression(Arg,LocalState,State,ArgValue), |
521 | | FValue = set(couple(ArgValue,Value)). |
522 | | units_compute_expression2(set_extension(Ex),set(_X),_Info,LocalState,State,set(Merged)) :- |
523 | ? | !, units_compute_expressions(Ex,LocalState,State,ExValue), |
524 | ? | merge_expression_list(ExValue,Merged). |
525 | | units_compute_expression2(sequence_extension(Ex),_X,_Info,LocalState,State,set(couple(integer(_),Merged))) :- |
526 | ? | !, units_compute_expressions(Ex,LocalState,State,ExValue), |
527 | ? | merge_expression_list(ExValue,Merged). |
528 | | units_compute_expression2(comprehension_set(ListOfIDs,Pred),_Type,_Info,LocalState,State,set(Merged)) :- |
529 | | !, |
530 | | units_set_up_localstate(ListOfIDs,_Bindings,ParameterState), |
531 | | append(ParameterState,LocalState,NewLocalState), |
532 | | units_check_boolean_expression(Pred,NewLocalState,State), |
533 | | units_compute_expressions(ListOfIDs,NewLocalState,State,ExValues), |
534 | | %format('#### ExValues in Comprehension Set: ~w~n', [ExValues]), |
535 | | couplise_list(ExValues, Merged). |
536 | | units_compute_expression2(general_sum(ListOfIDs,Pred,Stmt),_Type,_Info,LocalState,State,Value) :- |
537 | | !, |
538 | | units_set_up_localstate(ListOfIDs,_Bindings,ParameterState), |
539 | | append(ParameterState,LocalState,NewLocalState), |
540 | | units_check_boolean_expression(Pred,NewLocalState,State), |
541 | | units_compute_expression(Stmt,NewLocalState,State,Value). |
542 | | units_compute_expression2(general_product(ListOfIDs,Pred,Stmt),_Type,_Info,LocalState,State,Value) :- |
543 | | !, |
544 | | units_set_up_localstate(ListOfIDs,_Bindings,ParameterState), |
545 | | append(ParameterState,LocalState,NewLocalState), |
546 | | units_check_boolean_expression(Pred,NewLocalState,State), |
547 | | units_compute_expression(Stmt,NewLocalState,State,Value). |
548 | | % Expressions not listed in the typechecker |
549 | | units_compute_expression2(closure(Arg1),_X,_Info,LocalState,State,SV1) :- |
550 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
551 | | units_compute_expression2(closure1(Arg1),_X,_Info,LocalState,State,SV1) :- |
552 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
553 | | units_compute_expression2(reflexive_closure(Arg1),_X,_Info,LocalState,State,SV1) :- |
554 | | !, units_compute_expression(Arg1,LocalState,State,SV1). |
555 | | units_compute_expression2(integer(_Int),_T,Info,_LS,_S,Res) :- !, |
556 | | (member(unit(Unit),Info) -> unit_args_to_list(Unit, V), Res=integer(V); Res=integer(_)). |
557 | | units_compute_expression2(identifier(Id),_Type,_Info,LocalState,State,Value) :- |
558 | | !, units_lookup_value(Id,LocalState,State,Value). |
559 | | units_compute_expression2(first_of_pair(Pair),_Type,_Info,LocalState,State,Value) :- |
560 | | !, units_compute_expression(Pair,LocalState,State,SV1), |
561 | | SV1 = couple(Value,_Second). |
562 | | units_compute_expression2(second_of_pair(Pair),_Type,_Info,LocalState,State,Value) :- |
563 | | !, units_compute_expression(Pair,LocalState,State,SV1), |
564 | | SV1 = couple(_First,Value). |
565 | | units_compute_expression2(iteration(Arg1,_Arg2),_Type,_Info,LocalState,State,Value) :- |
566 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
567 | | Value = SV1. |
568 | | units_compute_expression2(integer_set(_),Type,Info,_LocalState,_State,Result) :- |
569 | | !, b_type_to_internal_type(Type,Info,Result). |
570 | | units_compute_expression2(string(_),_Type,_Info,_LocalState,_State,string(_)) :- !. |
571 | | units_compute_expression2(external_function_call(_FunName,Arguments),Type,Info,LocalState,State,Result) :- |
572 | | %format('Function: ~w~nArguments: ~w~nType: ~w~nInfo:~w~n', [FunName,Arguments,Type,Info]), |
573 | | !, units_compute_expressions(Arguments,LocalState,State,_EvaluatedArgs), |
574 | | b_type_to_internal_type(Type,Info,Result). |
575 | | units_compute_expression2(identity(X),_Type,_Info,LocalState,State,Result) :- |
576 | | !, units_compute_expression(X,LocalState,State,set(XExpr)), |
577 | | Result = set(couple(XExpr,XExpr)). |
578 | | units_compute_expression2(value(_),Type,Info,_LocalState,_State,Result) :- |
579 | | !, b_type_to_internal_type(Type,Info,Result). |
580 | | units_compute_expression2(let_expression(Ids,Assignments,Expr),_Type,_Infos,LocalState,State,Result) :- |
581 | | !, units_compute_expressions(Assignments,LocalState,State,Assignments2), |
582 | | assign_vars(Ids,Assignments2,LocalState,State,NewVars,NewVals), |
583 | | assign_vals_to_vars(NewVars,NewVals,StoreList), |
584 | | append(StoreList,LocalState,LetState), |
585 | | units_compute_expression(Expr,LetState,State,Result). |
586 | | units_compute_expression2(rec(Fields),_Type,_Infos,LocalState,State,rec(Result)) :- |
587 | | !, units_compute_record_fields(Fields,LocalState,State,Result). |
588 | | units_compute_expression2(record_field(Record,Field),_Type,_Infos,LocalState,State,Result) :- |
589 | ? | !, units_compute_expression(Record,LocalState,State,rec(Fields)), |
590 | ? | member(field(Field,Result),Fields). |
591 | | units_compute_expression2(struct(Rec),_Type,_Infos,LocalState,State,set(Result)) :- |
592 | | !, units_compute_expression(Rec,LocalState,State,Result). |
593 | | units_compute_expression2(X,T,I,LS,S,_V) :- |
594 | | !, add_error_fail(units_compute_expression2, 'Expression not implemented: ', [X,T,I,LS,S]). |
595 | | |
596 | | units_compute_record_fields([],_,_,[]). |
597 | | units_compute_record_fields([field(Name,Val)|Fields],LocalState,State,[field(Name,UVal)|UFields]) :- |
598 | | units_compute_expression(Val,LocalState,State,UVal), |
599 | | units_compute_record_fields(Fields,LocalState,State,UFields). |
600 | | |
601 | | % Checking of boolean expressions |
602 | | units_check_list_of_boolean_expressions([],_LocalState,_InState). |
603 | | units_check_list_of_boolean_expressions([Expr|T],LocalState,InState) :- |
604 | | units_check_boolean_expression(Expr,LocalState,InState), |
605 | | units_check_list_of_boolean_expressions(T,LocalState,InState). |
606 | | |
607 | | |
608 | | units_check_boolean_expression(b(Expr,Type,Infos),LS,S) :- !, |
609 | | % if units_check_boolean_expression2 fails, there was a wrong usage of units |
610 | | %statistics(walltime,[Start,_]), |
611 | | %format('Start checking ~w~n', [Expr]), |
612 | ? | (units_check_boolean_expression2(Expr,Infos,LS,S,NoInnerError) |
613 | | -> ( NoInnerError = false |
614 | | -> %trace, units_check_boolean_expression2(Expr,Infos,LS,S,NoInnerError), notrace, |
615 | | current_state_id(ID), |
616 | | member(nodeid(Position),Infos), |
617 | | translate_bexpression(b(Expr,Type,Infos), PPExpr), |
618 | | units:units_error_context(Context), |
619 | | store_state_error(ID,abort_error(well_definedness_error, |
620 | | 'Wrong usage of units in expression',PPExpr, |
621 | | span_context(Position,Context)),_) |
622 | | ; true%, format('Boolean Expression computed: ~w~n', [Expr]) |
623 | | ) |
624 | | ; % computational error, not unit error! |
625 | | add_error_fail(units_check_boolean_expression, 'Boolean Expression Check Failed: ', [Expr,Infos,LS,S])). |
626 | | %statistics(walltime,[End,_]), |
627 | | %Duration is End - Start, |
628 | | %format('Checking ~w took ~w ms~n', [Expr, Duration]). |
629 | | units_check_boolean_expression2(truth,_Infos,_LocalState,_InState,true) :- !. |
630 | | units_check_boolean_expression2(falsity,_Infos,_LocalState,_InState,true) :- !. |
631 | | units_check_boolean_expression2(partition(Arg1,Arg2),_Infos,LocalState,State,Result) :- |
632 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
633 | | units_compute_expressions(Arg2,LocalState,State,SV2), |
634 | | (same_units([SV1|SV2]) -> Result = true ; Result = false). |
635 | | units_check_boolean_expression2(conjunct(LHS,RHS),_Infos,LocalState,State,true) :- |
636 | | !,units_check_boolean_expression(LHS,LocalState,State), |
637 | | units_check_boolean_expression(RHS,LocalState,State). |
638 | | units_check_boolean_expression2(negation(Val),_Infos,LocalState,State,true) :- |
639 | | !,units_check_boolean_expression(Val,LocalState,State). |
640 | | units_check_boolean_expression2(disjunct(LHS,RHS),_Infos,LocalState,State,true) :- |
641 | | !,units_check_boolean_expression(LHS,LocalState,State), |
642 | | units_check_boolean_expression(RHS,LocalState,State). |
643 | | units_check_boolean_expression2(implication(LHS,RHS),_Infos,LocalState,State,true) :- |
644 | | !,units_check_boolean_expression(LHS,LocalState,State), |
645 | | units_check_boolean_expression(RHS,LocalState,State). |
646 | | units_check_boolean_expression2(equivalence(LHS,RHS),_Infos,LocalState,State,true) :- |
647 | | !,units_check_boolean_expression(LHS,LocalState,State), |
648 | | units_check_boolean_expression(RHS,LocalState,State). |
649 | | units_check_boolean_expression2(equal(Arg1,Arg2),_Info,LocalState,State,Result) :- |
650 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1), |
651 | | units_compute_expression(Arg2,LocalState,State,SV2), |
652 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
653 | | units_check_boolean_expression2(not_equal(Arg1,Arg2),_Info,LocalState,State,Result) :- |
654 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
655 | | units_compute_expression(Arg2,LocalState,State,SV2), |
656 | | (same_units(SV1,SV2) -> Result = true ; Result = false). |
657 | | units_check_boolean_expression2(member(Arg1,Arg2),_Info,LocalState,State,Result) :- |
658 | ? | !, units_compute_expression(Arg1,LocalState,State,SV1), |
659 | ? | units_compute_expression(Arg2,LocalState,State,SV2), |
660 | | (units_domain_member(SV1,SV2) -> Result = true ; Result = false). |
661 | | units_check_boolean_expression2(not_member(Arg1,Arg2),_Info,LocalState,State,Result) :- |
662 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
663 | | units_compute_expression(Arg2,LocalState,State,SV2), |
664 | | (units_domain_member(SV1,SV2) -> Result = true ; Result = false). |
665 | | units_check_boolean_expression2(subset(Arg1,Arg2),_Info,LocalState,State,Result) :- |
666 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
667 | | units_compute_expression(Arg2,LocalState,State,SV2), |
668 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
669 | | units_check_boolean_expression2(subset_strict(Arg1,Arg2),_Info,LocalState,State,Result) :- |
670 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
671 | | units_compute_expression(Arg2,LocalState,State,SV2), |
672 | | (same_units(SV1,SV2) -> Result = true ; Result = false). |
673 | | units_check_boolean_expression2(not_subset(Arg1,Arg2),_Info,LocalState,State,Result) :- |
674 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
675 | | units_compute_expression(Arg2,LocalState,State,SV2), |
676 | | (same_units(SV1,SV2) -> Result = true ; Result = false). |
677 | | units_check_boolean_expression2(not_subset_strict(Arg1,Arg2),_Info,LocalState,State,Result) :- |
678 | | !, units_compute_expression(Arg1,LocalState,State,SV1), |
679 | | units_compute_expression(Arg2,LocalState,State,SV2), |
680 | | (same_units(SV1,SV2) -> Result = true ; Result = false). |
681 | | units_check_boolean_expression2(less_equal(Arg1,Arg2),_Infos,LocalState,InState,Result) :- |
682 | ? | !, units_compute_expression(Arg1,LocalState,InState,SV1), |
683 | ? | units_compute_expression(Arg2,LocalState,InState,SV2), |
684 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
685 | | units_check_boolean_expression2(less(Arg1,Arg2),_Infos,LocalState,InState,Result) :- |
686 | | !, units_compute_expression(Arg1,LocalState,InState,SV1), |
687 | | units_compute_expression(Arg2,LocalState,InState,SV2), |
688 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
689 | | units_check_boolean_expression2(greater_equal(Arg1,Arg2),_Infos,LocalState,InState,Result) :- |
690 | | !, units_compute_expression(Arg1,LocalState,InState,SV1), |
691 | | units_compute_expression(Arg2,LocalState,InState,SV2), |
692 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
693 | | units_check_boolean_expression2(greater(Arg1,Arg2),_Infos,LocalState,InState,Result) :- |
694 | ? | !, units_compute_expression(Arg1,LocalState,InState,SV1), |
695 | | units_compute_expression(Arg2,LocalState,InState,SV2), |
696 | ? | (same_units(SV1,SV2) -> Result = true ; Result = false). |
697 | | units_check_boolean_expression2(exists(Parameters,RHS),_Infos,LocalState,InState,true) :- |
698 | | !, units_set_up_localstate(Parameters,_ParaValues,InnerLocalState), |
699 | | append(InnerLocalState,LocalState,CompleteLocalState), |
700 | | units_check_boolean_expression(RHS,CompleteLocalState,InState). |
701 | | units_check_boolean_expression2(forall(Parameters,LHS,RHS),_Infos,LocalState,InState,true) :- |
702 | | !, units_set_up_localstate(Parameters,_ParaValues,InnerLocalState), |
703 | | append(InnerLocalState,LocalState,CompleteLocalState), |
704 | | units_check_boolean_expression(LHS,CompleteLocalState,InState), |
705 | | units_check_boolean_expression(RHS,CompleteLocalState,InState). |
706 | | units_check_boolean_expression2(let_predicate(Ids,Assignments,Expr),_Infos,LocalState,State,true) :- |
707 | | !, units_compute_expressions(Assignments,LocalState,State,Assignments2), |
708 | | assign_vars(Ids,Assignments2,LocalState,State, NewVars, NewVals), |
709 | | assign_vals_to_vars(NewVars, NewVals, StoreList), |
710 | | append(StoreList,LocalState,LetState), |
711 | | units_check_boolean_expression(Expr,LetState,State). |
712 | | units_check_boolean_expression2(Test,_Infos,LocalState,InState,_Res) :- |
713 | | !, add_error_fail(units_check_boolean_expression, 'Boolean Expression not implemented: ', [Test,LocalState,InState]). |