1 | | % (c) 2009-2024 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(haskell_csp,[%clear_cspm_spec/0, % triggerred by clear specification event |
6 | | parse_and_load_cspm_file/1, load_cspm_pl_file/1, |
7 | | |
8 | | cspm_trans_enum/3, |
9 | | animatable_process/1, animatable_process_cli/1,animatable_process_without_arguments/1, |
10 | | channel/2, %cspPrintCompiled/2, |
11 | | evaluate_argument/2, force_evaluate_argument/2, evaluate_int_argument/2, |
12 | | force_evaluate_argument_for_member_check/2, |
13 | | check_boolean_expression/1, |
14 | | |
15 | | enumerate_channel_input_value/4, |
16 | | enumerate_datatype_el/5, |
17 | | |
18 | | is_a_datatype/2, csp_constructor/3, |
19 | | %% csp_full_type_constructor/3,csp_full_type_constant/2, % exported by haskell_csp_analyzer.pl |
20 | | dataTypeDef/2, |
21 | | channel_type_list/2, |
22 | | agent_compiled/3, % called in slicer_csp.pl ??? |
23 | | is_not_infinite_type/1, |
24 | | channel_type_is_finite/2, |
25 | | get_symbol_span/2, |
26 | | extract_span_from_event/4, extract_span_info/2, |
27 | | get_internal_csp_representation/1, |
28 | | get_csp_assertions_as_string/2,get_csp_assertions/1, get_csp_processes/1, |
29 | | translate_csp_assertion/2, %translate_csp_assertions/2, %get_csp_assertions_enum/2, |
30 | | parse_and_load_cspm_file_into_specific_pl_file/2, |
31 | | evaluate_type_list/2, |
32 | | %% get_formula_from_cspm_file/2, |
33 | | filter_formulas_from_pragmas/3, |
34 | | add_error_with_span/4,add_internal_error_with_span/4, |
35 | | evaluate_csp_expression/2,evaluate_csp_expression/3, parse_single_csp_expression/3, |
36 | | evaluate_parsed_csp_expression_with_timing/2, |
37 | | parse_single_csp_declaration/3, |
38 | | add_symbol_error/4, |
39 | | bindval/3, agent/3, agent_curry/3, subTypeDef/2, nameType/2, |
40 | | symbol/4, cspTransparent/1, cspPrint/1, valid_constant/1, |
41 | | parse_single_csp_expression_file/3, |
42 | | %% perform_csp_self_check/0, |
43 | | normalise_cspm_state/2, |
44 | | check_compiled_term/1, |
45 | | get_cspm_identifier/2, |
46 | | ignore_infinite_datatypes/0 % TODO: get rid of this ugly hack |
47 | | ]). |
48 | | |
49 | | |
50 | | :- meta_predicate read_compiled_prolog_file(-,-,1). |
51 | | |
52 | | :- use_module(probsrc(module_information)). |
53 | | :- module_info(group,csp). |
54 | | :- module_info(description,'Interpreter for CSP.'). |
55 | | |
56 | | :- use_module(library(lists)). |
57 | | :- use_module(library(file_systems)). |
58 | | %% :- use_module(library(process)). |
59 | | %% :- use_module(library(system)). |
60 | | |
61 | | /* the new CSP interpreter using the format produced by |
62 | | Marc's Haskell compiler fecsp/cspcomp */ |
63 | | |
64 | | /********* PROB modules *********/ |
65 | | :- use_module(probsrc(error_manager)). |
66 | | :- use_module(probsrc(self_check)). |
67 | | :- use_module(probsrc(debug)). |
68 | | :- use_module(probsrc(typechecker)). |
69 | | :- use_module(probsrc(kernel_objects),[top_level_dif/2,enumerate_basic_type/3]). |
70 | | :- use_module(probsrc(tools),[string_concatenate/3,flatten/2,split_atom/3, get_set_optional_prolog_flag/3]). |
71 | | :- use_module(probsrc(preferences),[preference/2, set_preference/2, get_preference/2,init_preferences/0]). |
72 | | :- use_module(probsrc(system_call),[system_call/4,system_call/5, get_writable_compiled_filename/3]). |
73 | | :- use_module(probsrc(kernel_waitflags)). |
74 | | :- use_module(probsrc(translate),[translate_cspm_state/2,translate_cspm_expression/2]). |
75 | | :- use_module(probsrc(specfile),[process_algebra_mode/0,csp_with_bz_mode/0,currently_opened_file/1]). |
76 | | /******** ------------ *********/ |
77 | | |
78 | | :- set_prolog_flag(double_quotes, codes). |
79 | | |
80 | | /* Predicate for performing self check for all CSP modules */ |
81 | | |
82 | | :- public perform_general_csp_self_check/0. |
83 | | perform_general_csp_self_check :- |
84 | | perform_csp_self_check, |
85 | | get_preference(use_clpfd_solver,Value), |
86 | | (Value=false -> |
87 | | NewValue = true |
88 | | ; NewValue = false), |
89 | | set_preference(use_clpfd_solver,NewValue), |
90 | | perform_csp_self_check, |
91 | | % reverting to the old use_clpfd_solver preference |
92 | | set_preference(use_clpfd_solver,Value). |
93 | | |
94 | | perform_csp_self_check :- |
95 | | init_preferences, |
96 | | perform_self_check(csp_basic), |
97 | | perform_self_check(csp_tuples), |
98 | | perform_self_check(csp_sequences), |
99 | | perform_self_check(csp_sets), |
100 | | perform_self_check(haskell_csp), |
101 | | perform_self_check(haskell_csp_analyzer). |
102 | | |
103 | | /* ------------------------------------- */ |
104 | | |
105 | | |
106 | | :- dynamic channel/2, bindval/3, agent/3, agent_curry/3, dataTypeDef/2, subTypeDef/2. |
107 | | :- dynamic nameType/2, symbol/4, cspTransparent/1, cspPrint/1, assertRef/5. |
108 | | :- dynamic assertModelCheck/3, assertModelCheckExt/4, pragma/1. |
109 | | %:- dynamic assertLtl/4, assertCtl/4. % dynamic declarations still generated by parser it seems, but not used |
110 | | |
111 | | :- discontiguous channel/2, agent/3, bindval/3, assertModelCheck/3. |
112 | | |
113 | | :- use_module(probcspsrc(haskell_csp_analyzer)). |
114 | | :- use_module(probcspsrc(csp_tuples)). |
115 | | :- use_module(probcspsrc(csp_sets)). |
116 | | :- use_module(probcspsrc(csp_basic)). |
117 | | |
118 | | /* ------------------------------------- */ |
119 | | /* Sample .pl Translation of a CSP file */ |
120 | | |
121 | | dataTypeDef('FRUIT',[constructor(apples),constructor(oranges),constructor(pears)]). |
122 | | channel(left,type(dotTupleType(['FRUIT']))). |
123 | | bindval('SEND',prefix(span,[in(_x)],left,prefix(span,[out(_x)],mid,prefix(span,[],ack,val_of('SEND',no_loc_info_available))),span2),span). |
124 | | symbol('SEND','SEND',src,'Process'). |
125 | | |
126 | | |
127 | | :- use_module(probsrc(eventhandling),[register_event_listener/3]). |
128 | | :- register_event_listener(start_unit_tests,reset_for_selfcheck,'Setup CSP dataTypeDef, channel,..'). |
129 | | %:- register_event_listener(stop_unit_tests, set_silent(false), 'Printing wf warnings again'). |
130 | | |
131 | | reset_for_selfcheck :- % TO DO: reset all facts and link with event_handling |
132 | | clear_cspm_spec, |
133 | | retractall(dataTypeDef(_,_)), |
134 | | assertz( dataTypeDef('FRUIT',[constructor(apples),constructor(oranges),constructor(pears)])), |
135 | | /* for testing is_not_infinite_type predicate */ |
136 | | assertz( dataTypeDef('Msg',[constructor('A'),constructor('B'),constructorC('con',dotTupleType(['SubMsg']))]) ), |
137 | | assertz( dataTypeDef('Msg1',[constructor('A'),constructor('B')]) ), |
138 | | assertz( dataTypeDef('SubMsg',[constructor('KA'), |
139 | | constructorC(conc,dotTupleType(['Msg'])),constructorC(ste,dotTupleType([builtin_call('Seq'('Msg'))]))]) ), |
140 | | assertz( dataTypeDef('Inf',[constructorC(ste,dotTupleType([builtin_call('Seq'('FRUIT'))]))]) ), |
141 | | retractall( channel(_,_)), |
142 | | assertz( channel(left,type(dotTupleType(['FRUIT']))) ), |
143 | | assertz( channel(right,type(dotTupleType(['FRUIT']))) ), |
144 | | assertz( channel(mid,type(dotTupleType(['FRUIT']))) ), |
145 | | assertz( channel(receive,type(dotTupleType(['Msg']))) ), |
146 | | assertz( channel(infinite,type(dotTupleType(['Inf']))) ), |
147 | | retractall( bindval(_,_,_) ), |
148 | | assertz( bindval('SEND', |
149 | | prefix(no_loc_info_available,[in(_x)],left, |
150 | | prefix(no_loc_info_available,[out(_x)],mid, |
151 | | prefix(no_loc_info_available,[],ack,val_of('SEND',no_loc_info_available),no_loc_info_available), |
152 | | no_loc_info_available), |
153 | | no_loc_info_available),no_loc_info_available) ), |
154 | | assertz( bindval('REC',prefix(no_loc_info_available,[in(_x)],mid, |
155 | | prefix(no_loc_info_available,[out(_x)],right, |
156 | | prefix(no_loc_info_available,[],ack,val_of('REC',no_loc_info_available),no_loc_info_available), |
157 | | no_loc_info_available),no_loc_info_available),no_loc_info_available) ), |
158 | | assertz( bindval('SYSTEM',sharing(closure([mid,ack]),val_of('SEND',no_loc_info_available), |
159 | | val_of('REC',no_loc_info_available),no_loc_info_available),no_loc_info_available) ), |
160 | | assertz( bindval('GEN1', |
161 | | prefix(no_loc_info_available,[out(oranges)], |
162 | | left, |
163 | | prefix(no_loc_info_available,[out(oranges)],right,val_of('GEN2',no_loc_info_available),no_loc_info_available), |
164 | | no_loc_info_available),no_loc_info_available) ), |
165 | | assertz( bindval('GEN2', |
166 | | prefix(no_loc_info_available,[out(pears)],left, |
167 | | prefix(no_loc_info_available,[out(pears)], |
168 | | right,val_of('GEN1',no_loc_info_available),no_loc_info_available),no_loc_info_available),no_loc_info_available) ), |
169 | | assertz( bindval('MAIN',sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available),val_of('GEN1',no_loc_info_available),no_loc_info_available),no_loc_info_available) ), |
170 | | assertz( bindval('P1',agent_call(no_loc_info_available,'Q',[int(10)]),no_loc_info_available) ), |
171 | | retractall(agent(_,_,_)), |
172 | | assertz( agent('P'(_),'prefix'('src_span'(8,8,8,9,87,1),['in'(_i2)],'c', |
173 | | 'prefix'('src_span'(8,15,8,16,94,1),['out'(_i2)],'c', |
174 | | 'stop'('src_span'(8,22,8,26,101,4)),'src_span'(8,19,8,21,97,10)), |
175 | | 'src_span'(8,12,8,14,90,17)),'src_span'(8,8,8,26,87,18)) ), |
176 | | %assertz( agent('P2'(_n),agent_call(no_loc_info_available,'Q',['-'(_n, int(10))]),no_loc_info_available) ), |
177 | | %assertz( agent('P1',agent_call(no_loc_info_available,'Q',[int(10)]),no_loc_info_available) ), |
178 | | assertz( agent('Q'(_n),ifte('=='(_n,int(0)),stop(no_loc_info_available), |
179 | | prefix(no_loc_info_available,[],'a', |
180 | | agent_call(no_loc_info_available,'Q',['-'(_n,'int'(1))]),no_loc_info_available), |
181 | | no_loc_info_available,no_loc_info_available,no_loc_info_available),no_loc_info_available) ), |
182 | | retractall(symbol(_,_,_,_)), |
183 | | assertz( symbol('SEND','SEND',src,'Process') ), |
184 | | assertz( symbol('REC','REC',src(8,1,8,4,4,3),'Procsess') ), |
185 | | assertz( symbol('SYSTEM','SYSTEM',src,'Process') ), |
186 | | assertz( symbol('GEN1','GEN1',src,'Process') ), |
187 | | assertz( symbol('GEN2','GEN2',src,'Process') ), |
188 | | assertz( symbol('MAIN','MAIN',src(3,1,3,5,20,4),'Process') ), |
189 | | retractall(assertRef(_,_,_,_,_)), |
190 | | assertz( assertRef('False','val_of'('MAIN',no_loc_info_available),'Trace', |
191 | | 'val_of'('PROB_TEST_TRACE',no_loc_info_available),no_loc_info_available) ), |
192 | | assertz( assertRef('True', 'val_of'('PROB_TEST_TRACE',no_loc_info_available), |
193 | | 'Trace', 'val_of'('MAIN',no_loc_info_available),no_loc_info_available) ), |
194 | | retractall(assertModelCheckExt(_,_,_,_)), |
195 | | assertz( assertModelCheckExt('False', |
196 | | sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available), |
197 | | val_of('GEN1',no_loc_info_available),no_loc_info_available), 'Deterministic','F') ), |
198 | | assertz( assertModelCheckExt('True', |
199 | | sharing(closure([left,right]),val_of('SYSTEM',no_loc_info_available), |
200 | | val_of('GEN1',no_loc_info_available),no_loc_info_available), 'DeadlockFree','FD') ), |
201 | | retractall(assertModelCheck(_,_,_)), |
202 | | assertz( assertModelCheck('False', |
203 | | 'prefix'(no_loc_info_available,[],'dotTuple'(['a','int'(1)]), |
204 | | 'val_of'('P',no_loc_info_available),no_loc_info_available),'LivelockFree')), |
205 | | retractall(pragma(_)), |
206 | | assertz(pragma('assert_ltl "GF(a)"')), |
207 | | assertz(pragma('ASSERT_LTL "GF(b)"')), |
208 | | assertz(pragma('ASSERT_LTL_TRUE "true"')), |
209 | | haskell_csp_analyzer:analyze. |
210 | | |
211 | | |
212 | | % these predicates are generated by the csp analyzer, there are not the standard generated predicates from the translation |
213 | | % process csp -> pl |
214 | | |
215 | | /* ------------------------------------- */ |
216 | | |
217 | | /* ------------------------------------- */ |
218 | | |
219 | | animatable_process_without_arguments(X) :- |
220 | ? | symbol(RenamedX,X,_,_), |
221 | ? | (is_csp_process(RenamedX);is_possible_csp_process(RenamedX)). |
222 | | |
223 | | animatable_process(X) :- |
224 | | (symbol(RenamedX,X,_,_),(is_csp_process(RenamedX);is_possible_csp_process(RenamedX))) ; |
225 | | (nonvar(X), X=agent_call(_Src,_F,_Args)) ; |
226 | | (nonvar(X), X=agent_call_curry(_F,_Args)) ; |
227 | | (agent(F,_,_),is_csp_process(F),animatable_process_with_arguments(F,proc(FName,N)),proc_with_arguments_to_string(FName,N,X)). |
228 | | |
229 | | animatable_process_cli(X) :- |
230 | | symbol(RenamedX,X,_,_), |
231 | | (is_csp_process(RenamedX) ; is_possible_csp_process(RenamedX)). |
232 | | |
233 | | animatable_process_with_arguments(X,proc(F,N)) :- |
234 | | functor(X,F,N),N>0. |
235 | | |
236 | | check_compiled_term(Term) :- |
237 | | nonvar(Term),!, |
238 | | Term=agent_call(_Src,F,Args), |
239 | | length(Args,N), |
240 | | ( (symbol(RenamedF,F,_,_),functor(P,RenamedF,N),is_csp_process(P)) -> |
241 | | true |
242 | | ; translate_cspm_state(Term,Proc), |
243 | | add_error_fail(check_compiled_term, 'There is no such process in file: ',Proc) |
244 | | ). |
245 | | |
246 | | /* ------------------------------------- */ |
247 | | |
248 | | /* Predicates for calling the CSPM Parser and loading the corresponding to the Csp File Prolog File */ |
249 | | |
250 | | parse_and_load_cspm_file(CSPFile) :- |
251 | | \+ file_exists(CSPFile), |
252 | | !, |
253 | | add_error_fail(parse_and_load_cspm_file,'CSP file does not exist:',CSPFile). |
254 | | parse_and_load_cspm_file(CSPFile) :- |
255 | | get_writable_compiled_filename(CSPFile,'.pl',PrologFile), |
256 | | parse_and_load_cspm_file_into_specific_pl_file(CSPFile,PrologFile). |
257 | | |
258 | | %% parse_and_load_cspm_file(CSPFile) :- |
259 | | %% (parsercall: call_cspmj_parser(CSPFile,PrologFile) |
260 | | %% -> load_cspm_pl_file(PrologFile,CSPFile) |
261 | | %% ; add_error(parse_and_load_cspm_file,'Error while parsing CSP file: ',CSPFile), |
262 | | %% add_error_fail(parse_and_load_cspm_file,'Std error: ','to be added') |
263 | | %% ). |
264 | | |
265 | | /* Specific predicate for parsing and re-writting the Parse-Output into already existing prolog file.*/ |
266 | | % It will be needed by parsing a temporary files when the Csp Assertion Viewer is used. |
267 | | parse_and_load_cspm_file_into_specific_pl_file(CSPFile, PrologFile) :- |
268 | | debug_println(15,reading_cspm_file(CSPFile)), |
269 | | get_cspm_parser_command(AbsParseCmd), |
270 | | debug_println(5,parsecmd(AbsParseCmd)), |
271 | | string_concatenate('--prologOut=', PrologFile, PrologFileOutArg), |
272 | | debug_stats(parsing(AbsParseCmd,'translate',PrologFileOutArg, CSPFile)), |
273 | | system_call(AbsParseCmd, ['translate',PrologFileOutArg, CSPFile], Text,JExit), |
274 | | debug_stats(done_parsing), |
275 | | debug_println(15,parse_exit(JExit)), |
276 | | (JExit=exit(0) |
277 | | -> load_cspm_pl_file(PrologFile,CSPFile) |
278 | | ; add_internal_error('Error while parsing CSP file: ',CSPFile), |
279 | | atom_codes(T,Text), |
280 | | add_error_fail(parse_and_load_cspm_file,'Std error: ',T) |
281 | | ). |
282 | | |
283 | | parse_single_csp_declaration(Decl,CSPFile,Result) :- |
284 | | get_cspm_parser_command(Cmd), |
285 | | string_concatenate('--declarationToPrologTerm=', Decl, DeclarationArgument), |
286 | | system_call(Cmd, ['translate', DeclarationArgument, CSPFile],Text,ErrText,JExit), |
287 | | (JExit=exit(0) |
288 | | -> read_from_codes(Text,Result) |
289 | | ; atom_codes(ErrT,ErrText), |
290 | | add_error_fail(parsing_csp_declaration,'Std error: ',ErrT) |
291 | | ). |
292 | | |
293 | | :- use_module(probsrc(xtl_interface),[last_opened_cspm_file/1]). |
294 | | parse_single_csp_expression(Context,Expr,Res) :- |
295 | | ( Context==eval -> Filename='no-file' |
296 | | ; Context==ltl -> |
297 | | (csp_with_bz_mode |
298 | | -> last_opened_cspm_file(Filename) |
299 | | ; currently_opened_file(Filename) |
300 | | ) |
301 | | ; add_internal_error('Internal Error: Unknown context argument: ', Context),fail |
302 | | ), |
303 | | parse_single_csp_expression_file(Expr,Filename,Res). |
304 | | |
305 | | :- use_module(library(codesio)). |
306 | | parse_single_csp_expression_file(Expr,CSPFile,Res) :- |
307 | | get_cspm_parser_command(Cmd), |
308 | | string_concatenate('--expressionToPrologTerm=', Expr, ExpressionArgument), |
309 | | system_call(Cmd, ['translate', ExpressionArgument, CSPFile],Text,ErrText,JExit), |
310 | | (JExit=exit(0) |
311 | | -> read_from_codes(Text,Result), |
312 | | translate_expression(Result,Res) |
313 | | ; atom_codes(ErrT,ErrText), |
314 | | add_error_fail(parsing_csp_expression,'Std error: ',ErrT) |
315 | | ). |
316 | | |
317 | | evaluate_csp_expression(Expr,Result) :- |
318 | | ( parse_single_csp_expression(eval,Expr,ParsedExpr) -> |
319 | | evaluate_parsed_csp_expression(ParsedExpr,Expr,Result) |
320 | | ; add_error_fail(parsing_csp_expression, 'Error while parsing expression: ', Expr) |
321 | | ). |
322 | | |
323 | | evaluate_parsed_csp_expression(ParsedExpr,Expr,Result) :- |
324 | | debug_println(9,parsed_csp_expression(ParsedExpr)), |
325 | ? | haskell_csp_analyzer:compile_body(ParsedExpr,'evaluate',[],[],CompiledExpr), |
326 | | ( evaluate_parsed_csp_expression_with_timing(CompiledExpr,Res) -> |
327 | | ( translate_cspm_expression(Res, R) -> R=Result |
328 | | ; add_error_fail(pretty_printing_evaluated_expression, 'Error while pretty-printing result: ', Res) |
329 | | ) |
330 | | ; add_error_fail(evaluating_expression, 'Error while evaluating expression: ',Expr) |
331 | | ). |
332 | | |
333 | | evaluate_csp_expression(Expr,CSPFile,Result) :- |
334 | | ( parse_single_csp_expression_file(Expr, CSPFile,ParsedExpr) -> |
335 | ? | evaluate_parsed_csp_expression(ParsedExpr,Expr,Result) |
336 | | ; add_error_fail(parsing_csp_expression, 'Error while parsing typed expression: ', Expr) |
337 | | ). |
338 | | |
339 | | :- use_module(probsrc(tools),[cputime/1]). |
340 | | evaluate_parsed_csp_expression_with_timing(ParsedExpr,Res) :- |
341 | | cputime(T1), |
342 | | evaluate_expression(ParsedExpr,Res), |
343 | | cputime(T2), |
344 | | D is T2-T1, |
345 | | print('% Time to evaluate expression: '),print(D), print(' ms.%'),nl. |
346 | | |
347 | | % TODO: Which are the expressions allowed to be written in events |
348 | | translate_expression(listExp(rangeEnum(List)),Res) :- !, Res=list(List). |
349 | | translate_expression(setExp(rangeEnum(List)),Res) :- !, Res=setValue(List). |
350 | | translate_expression(dotTuple(List),dotTuple(Res)) :- !, |
351 | | maplist(translate_expression,List,Res). |
352 | | translate_expression(X,X). |
353 | | |
354 | | /* Predicates for reading a Prolog file (usually generated after translating the appropriate Csp file with the CSPM-Tool) |
355 | | and filtering the asssertion declarations from it. Needed for the 'Check Csp Assertions' window in Tcl_Tk. */ |
356 | | read_compiled_prolog_file(CSPFile,Result,PredName) :- |
357 | | get_writable_compiled_filename(CSPFile,'.pl', PrologFile), |
358 | | debug_print(9,'opening Prolog file: '), debug_println(9,PrologFile), |
359 | | my_see(PrologFile), |
360 | | call(PredName,Result), |
361 | | !,seen,debug_println(9,done). |
362 | | |
363 | | my_see(File) :- |
364 | | catch(see(File), |
365 | | error(existence_error(_,_),_), |
366 | | add_error_fail(my_see,'File does not exist: ',File)). |
367 | | |
368 | | filter_assertion_declarations(Assertions) :- |
369 | | read(Term), !, |
370 | | ((Term = end_of_file) -> (Assertions = []) |
371 | | ; (is_assertion(Term) |
372 | | -> (Assertions = [Term|T]) |
373 | | ; (Assertions = T) |
374 | | ), filter_assertion_declarations(T) |
375 | | ). |
376 | | |
377 | | :- assert_must_succeed((is_assertion(assertRef(_,_,_,_,_)),is_assertion(assertModelCheck(_,_,_)), is_assertion(assertModelCheckExt(_,_,_,_)))). |
378 | | |
379 | | is_assertion(assertRef(_,_,_,_,_)). |
380 | | is_assertion(assertModelCheck(_,_,_)). |
381 | | is_assertion(assertModelCheckExt(_,_,_,_)). |
382 | | is_assertion(assertLtl(_,_,_,_)). |
383 | | is_assertion(assertCtl(_,_,_,_)). |
384 | | |
385 | | filter_formulas_from_pragmas(Type,FlNList,FlFList) :- |
386 | | findall(Formulas,(pragma(S),get_formulas_from_pragma(Type,pragma(S),_Names,Formulas)),FList), |
387 | | findall(Names,(pragma(S),get_formulas_from_pragma(Type,pragma(S),Names,_Formulas)),NList), |
388 | | flatten(NList,FlNList), |
389 | | flatten(FList,FlFList). |
390 | | |
391 | | get_formula_from_cspm_file(Type,Formula) :- |
392 | | filter_formulas_from_pragmas(Type,_Ns,[String|_]), |
393 | | (var(String) -> |
394 | | Formula = '' |
395 | | ; Formula=String |
396 | | ). |
397 | | |
398 | | get_formulas_from_cspm_file(Type,String) :- |
399 | | filter_formulas_from_pragmas(Type,_Ns,Formulas), |
400 | | convert_string_list_to_string(Formulas,String). |
401 | | |
402 | | string_concatenate_sep(Sep,Atom,R) :- |
403 | | string_concatenate(Atom,Sep,R). |
404 | | |
405 | | convert_string_list_to_string(L,Res) :- |
406 | | maplist(string_concatenate_sep(';'),L,LRes), |
407 | | concatenate_string_list(LRes,Res). |
408 | | |
409 | | get_formulas_from_pragma(Type,pragma(Str),Names,Formulas) :- |
410 | | atom_codes(Str,CodeList), |
411 | | (Type = ltl -> |
412 | ? | ltl_equations(Names,Formulas,CodeList,[]) |
413 | | ;Type = ctl -> |
414 | | ctl_equations(Names,Formulas,CodeList,[]) |
415 | | ; |
416 | | Names=[], Formulas=[] |
417 | | ). |
418 | | |
419 | | %%%%%%%%%%%%%%%%%% Tests for the ASSERT_LTL Equations Parser below %%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
420 | | |
421 | | :- assert_must_succeed((haskell_csp:reset_for_selfcheck)). |
422 | | :- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL_123=="F(e(a))" "Checking simple LTL property."'), |
423 | | Names,Formulas),Names==[123],Formulas==['F(e(a))'])). |
424 | | :- assert_must_fail((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL_0123=="F(e(a))" "First digit in number must be nonzero."'), |
425 | | _Names,_Formulas))). |
426 | | :- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('ASSERT_LTL=="F(e(a))"'), |
427 | | Names,Formulas),Names==[[95]],Formulas==['F(e(a))'])). |
428 | | :- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('assert_ltl "F(e(a))" "Checking simple LTL property."'), |
429 | | Names,Formulas),Names==[[95]],Formulas==['F(e(a))'])). |
430 | | :- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ctl,pragma('assert_ctl "true" "Checking simple CTL property."'), |
431 | | Names,Formulas),Names==[[95]],Formulas==['true'])). |
432 | | :- assert_must_succeed((haskell_csp: get_formulas_from_pragma(ltl,pragma('assert_ltl "F(e(a))" "Parsing multiple LTL equations."; ASSERT_LTL_TRUE "F(e(b))"; ASSERT_LTL_2=="F(e(c))"; ASSERT_LTL "F(e(d))"'), |
433 | | Names,Formulas),Names==[[95],[84,82,85,69],2,[95]],Formulas==['F(e(a))','F(e(b))','F(e(c))','F(e(d))'])). |
434 | | :- assert_must_succeed(( |
435 | | haskell_csp: get_formulas_from_cspm_file(ltl,S), S == 'GF(a);GF(b);true;')). |
436 | | :- assert_must_succeed(( |
437 | | haskell_csp: get_formula_from_cspm_file(ltl,S), S == 'GF(a)')). |
438 | | |
439 | | %%%%%%%%%%%%%%%%%% Simple Parser for Parsing ASSERT_LTL Equations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
440 | | |
441 | | %%%%%%%%%%%%% CTL assertions %%%%%%%%%%%%%%% |
442 | | ctl_equations([N|Ns],[F|Fs]) --> ctl_equation(N,F),ctl_equations2(Ns,Fs). |
443 | | ctl_equations2(Ns,Fs) --> ows,sep,ows,ctl_equations(Ns,Fs),{Fs\=[],Ns\=[]}. |
444 | | ctl_equations2([],[]) --> ows. |
445 | | |
446 | | ctl_equation(N,F) --> ows,assert_id_ctl(N), ows, eq,!, ows, string(F), ows, optional_string. |
447 | | |
448 | | assert_id_ctl(N) --> ass_ctl,!,ass_name(N). |
449 | | assert_id_ctl(N) --> "assert_ctl",{N="_"},!. |
450 | | assert_id_ctl(N) --> "ASSERT_CTL",{N="_"},!. |
451 | | |
452 | | ass_ctl --> "ASSERT_CTL_". |
453 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
454 | | |
455 | ? | ltl_equations([N|Ns],[F|Fs]) --> ltl_equation(N,F),ltl_equations2(Ns,Fs). |
456 | ? | ltl_equations2(Ns,Fs) --> ows,sep,ows,ltl_equations(Ns,Fs),{Fs\=[],Ns\=[]}. |
457 | | ltl_equations2([],[]) --> ows. |
458 | | |
459 | | ltl_equation(N,F) --> ows,assert_id_ltl(N), ows, eq,!, ows, string(F), ows, optional_string. |
460 | | |
461 | | string(Atom) --> [34], stringcontent(String), [34], {atom_codes(Atom,String)}. %34 is Ascii Code of " |
462 | | |
463 | | optional_string --> [34], stringcontent(_String), [34],!. |
464 | | optional_string --> "",!. |
465 | | |
466 | | stringcontent([C|Rest]) --> [C], {C \= 34}, !, stringcontent(Rest). |
467 | | stringcontent([]) --> []. |
468 | | |
469 | | assert_id_ltl(N) --> ass,!,ass_name(N). |
470 | | assert_id_ltl(N) --> "assert_ltl",{N="_"},!. |
471 | | assert_id_ltl(N) --> "ASSERT_LTL",{N="_"},!. |
472 | | |
473 | ? | ass_name(N) --> num(N),{number(N)},!. |
474 | | ass_name(N) --> name_tail(N),!. |
475 | | |
476 | | name_tail([C|Cs]) --> [C],{is_digit(C) ; |
477 | | (0'A =< C,C =< 0'Z) ; |
478 | | (0'a =< C,C =< 0'z) ; |
479 | | C=0'_}, |
480 | | name_tail(Cs),!. |
481 | | name_tail([]) --> [],!. |
482 | | |
483 | | num(Number) --> nonzerodigit(D), num2(Rest),{number_codes(Number,[D|Rest])}. |
484 | | num(Number) --> digit(D),{number_codes(Number,[D])}. |
485 | | num2([D|Rest]) --> digit(D),!,num2(Rest). |
486 | | num2([]) --> []. |
487 | | |
488 | | digit(D) --> [D], {is_digit(D)},!. |
489 | | nonzerodigit(ND) --> [ND], {is_nz_digit(ND)},!. |
490 | | |
491 | | is_digit(D) :- 0'0 =< D, D =< 0'9. |
492 | | is_nz_digit(D) :- 0'0 < D, D =< 0'9. |
493 | | |
494 | ? | sep --> [C],{member(C,";,")}. |
495 | | |
496 | ? | ows --> [C], {member(C," \t\n\r")}, !, ows. |
497 | | ows --> "". |
498 | | |
499 | | eq --> "==",!. |
500 | | eq --> [32],!. |
501 | | eq --> "",!. |
502 | | |
503 | | ass --> "ASSERT_LTL_",!. |
504 | | |
505 | | /* ------------------------------------------------------------------------------------------------------------- */ |
506 | | |
507 | | /* Predicates for getting the CSPM-Tool command from the library and loading cspm Prolog files.*/ |
508 | | get_cspm_parser_command(AbsParseCmd) :- |
509 | | debug_println(9,getting_parser_cmd), |
510 | | catch( |
511 | | absolute_file_name(prob_lib(cspmf),AbsParseCmd,[access(exist),extensions(['.exe',''])]), |
512 | | error(E,_), |
513 | | add_error_fail(haskell_csp,'Could not find CSP-M Parser. Be sure to install cspmf in your ProB lib directory. ',E)), |
514 | | debug_println(9,parser(AbsParseCmd)). |
515 | | |
516 | | |
517 | | :- dynamic parseResult/5. |
518 | | load_cspm_pl_file(PFile) :- load_cspm_pl_file(PFile,PFile). |
519 | | load_cspm_pl_file(PrologFile,CSPFile) :- clear_cspm_spec, |
520 | | \+ file_exists(PrologFile),!, |
521 | | add_error(haskell_csp,'Could not generate Prolog encoding of CSP file: ',CSPFile),fail. |
522 | | load_cspm_pl_file(PrologFile,CSPFile) :- |
523 | | debug_println(15,consulting(PrologFile)), |
524 | | cia_consult_without_redefine_warning(PrologFile), debug_stats(done_loading_pl_file), |
525 | | /* TO DO: replace by safer load which checks that |
526 | | only correct facts are loaded !!!! */ |
527 | | parseResult(ParseResult,ErrorMsg,StartLine,SC,Off), |
528 | | (ParseResult='ok' -> analyze ; |
529 | | add_error(haskell_csp,'Error while parsing CSP-M: ',ParseResult:CSPFile), |
530 | | add_error(haskell_csp,'CSP-M Parse error message: ',ErrorMsg,src_position(StartLine,SC,Off,1)) |
531 | | ). |
532 | | |
533 | | /* ------------------------------------------------------------------------------------------------------------ */ |
534 | | |
535 | | % A small pretty-printer for printing assert declarations |
536 | | refinement_operator('Trace',' [T= ') :- !. |
537 | | refinement_operator('Failure', ' [F= ') :- !. |
538 | | refinement_operator('FailureDivergence',' [FD= ') :- !. |
539 | | refinement_operator('RefusalTesting',' [R= ') :- !. |
540 | | refinement_operator('RefusalTestingDiv',' [RD= ') :- !. |
541 | | refinement_operator('RevivalTesting',' [V= ') :- !. |
542 | | refinement_operator('RevivalTestingDiv',' [VD= ') :- !. |
543 | | /* the clauses below will be called if we check the particular assertion direct from the command line and not from the .pl file */ |
544 | | refinement_operator('[T=',' [T= ') :- !. |
545 | | refinement_operator('[F=', ' [F= ') :- !. |
546 | | refinement_operator('[FD=',' [FD= ') :- !. |
547 | | refinement_operator('[R=',' [R= ') :- !. |
548 | | refinement_operator('[RD=',' [RD= ') :- !. |
549 | | refinement_operator('[V=',' [V= ') :- !. |
550 | | refinement_operator('[VD=',' [VD= ') :- !. |
551 | | refinement_operator(A, _) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported refinement operator: ', A). |
552 | | |
553 | | adding_not('True', 'not ') :- !. |
554 | | adding_not('False', '') :- !. |
555 | | adding_not(A,_) :- add_error_fail(haskell_csp,'Error while pretty-printing assert declaration. Unexpected argument infront the assertion declaration: ',A). |
556 | | |
557 | | fdr_model('Deterministic', ' :[ deterministic ') :- !. |
558 | | fdr_model('DeadlockFree', ' :[ deadlock free ') :- !. |
559 | | fdr_model('LivelockFree', ' :[ livelock free ') :- !. |
560 | | fdr_model(A,_) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported model inside of process assertion: ', A). |
561 | | |
562 | | fdr_single_model('Deterministic', ' :[ deterministic [FD] ]') :- !. |
563 | | fdr_single_model('DeadlockFree', ' :[ deadlock free [FD] ]') :- !. |
564 | | fdr_single_model('LivelockFree', ' :[ livelock free ]') :- !. |
565 | | fdr_single_model(A,_) :- add_error_fail(haskell_csp, 'Error while pretty-printing assert declaration. Invalid or unsupported model inside of process assertion: ', A). |
566 | | |
567 | | fdr_ext('F', '[F] ]') :- !. |
568 | | fdr_ext('FD', '[FD] ]') :- !. |
569 | | fdr_ext(Ext, _) :- add_error_fail(haskell_csp, 'Not supported assertion type model: ',Ext). |
570 | | |
571 | | :- assert_must_fail(proc_with_arguments_to_string('P',0,_)). |
572 | | :- assert_must_fail(proc_with_arguments_to_string('P',-10,_)). |
573 | | :- assert_must_succeed((proc_with_arguments_to_string('P',1,String), String=='P(-)')). |
574 | | :- assert_must_succeed((proc_with_arguments_to_string('P',3,String), String=='P(-,-,-)')). |
575 | | |
576 | | proc_with_arguments_to_string(Fun,N,FunRes) :- |
577 | | ( N>1 -> |
578 | | count_proc_arguments(N,R), |
579 | | concatenate_string_list([Fun,'('|R],FunRes) |
580 | | ; N =:= 1 -> |
581 | | string_concatenate(Fun,'(-)',FunRes) |
582 | | ). |
583 | | |
584 | | count_proc_arguments(N,Res) :- |
585 | | count_proc_arguments(N,['-',')'],Res). |
586 | | |
587 | | count_proc_arguments(N,L,Res) :- |
588 | | (N =:= 1 -> |
589 | | Res=L |
590 | | ; N>1 -> |
591 | | N1 is N-1, |
592 | | count_proc_arguments(N1,['-',','|L],Res) |
593 | | ). |
594 | | |
595 | | :- assert_must_succeed((string_to_proc_term('P(-,-,-)',Term), Term = 'P'(_A,_B,_C))). |
596 | | :- assert_must_succeed((string_to_proc_term('P(-)',Term), Term = 'P'(_X))). |
597 | | :- assert_must_succeed((string_to_proc_term('P',Term), Term = 'P')). |
598 | | :- assert_must_succeed((string_to_proc_term(p(1,2),Term), Term == p(1,2))). |
599 | | |
600 | | string_to_proc_term(Proc,Term) :- |
601 | | atom(Proc),!, |
602 | | split_atom(Proc,['(',',',')'],[Fun|A]), |
603 | | length(A,N), |
604 | | gen_vars(N,Args), |
605 | | Term =.. [Fun|Args]. |
606 | | string_to_proc_term(X,X). |
607 | | |
608 | | :- assert_must_succeed((string_to_proc_term('P(-,-,-)',Term), functor(Term,F,N), proc_with_arguments_to_string(F,N,Str), Str == 'P(-,-,-)')). |
609 | | |
610 | | gen_vars(N,Vars) :- |
611 | | ( N>0 -> N1 is N-1, gen_vars(N1,T),Vars=[_X|T] |
612 | | ; N =:= 0 -> Vars = []). |
613 | | |
614 | | :- assert_must_succeed(string_term_with_args('Fun(1,2,-)')). |
615 | | :- assert_must_fail(string_term_with_args('Fun(1,2,3)')). |
616 | | :- assert_must_fail(string_term_with_args('Fun(X,_,_Y)')). |
617 | | :- assert_must_fail(string_term_with_args(_Fun)). |
618 | | |
619 | | string_term_with_args(StrTerm) :- |
620 | | atom(StrTerm),!, |
621 | | split_atom(StrTerm,['(',',',')'],[_Fun|A]), |
622 | | A\=[],member(-,A). |
623 | | |
624 | | :- assert_must_succeed((haskell_csp:concatenate_string_list(['A','B','C'],'ABC'))). |
625 | | :- assert_must_succeed((haskell_csp:concatenate_string_list([],''))). |
626 | | |
627 | | concatenate_string_list(L,Res) :- |
628 | | concatenate_string_list(L,'',Res). |
629 | | |
630 | | concatenate_string_list([],Res,Res). |
631 | | concatenate_string_list([H|T],Str,Res) :- |
632 | | string_concatenate(Str,H,StrRes), |
633 | | concatenate_string_list(T,StrRes,Res). |
634 | | |
635 | | translate_csp_assertions(L,Res) :- |
636 | | maplist(translate_csp_assertion_with_sep,L,LRes), |
637 | | concatenate_string_list(LRes,Res). |
638 | | |
639 | | translate_csp_assertion_with_sep(Ass,AssStrWithSep) :- |
640 | | translate_with_sep(translate_csp_assertion,Ass,'$',AssStrWithSep). |
641 | | |
642 | | % Sep must be an atom |
643 | | translate_with_sep(TranslationPredicate,Arg,Sep,ArgStrSep) :- |
644 | | functor(Fun,TranslationPredicate,2),arg(1,Fun,Arg),arg(2,Fun,ArgStr), |
645 | | %Fun =.. [TranslationPredicate,Arg,ArgStr], |
646 | | call(Fun), |
647 | | string_concatenate(ArgStr,Sep,ArgStrSep). |
648 | | |
649 | | translate_csp_assertion(AssertionExpr,ConcRes) :- |
650 | | /* assert not? P [Op= Q */ |
651 | | (AssertionExpr = assertRef(N,P,Op,Q,_) -> |
652 | | refinement_operator(Op,Operator), |
653 | | translate_cspm_state(Q,Proc_2), |
654 | | L=[Operator,Proc_2] |
655 | | /* assert P |= LTL: "ltl-formula" */ |
656 | | ;AssertionExpr = assertLtl(N,P,Formula,_) -> |
657 | | L = [' |= ', 'LTL: ', '\"', Formula, '\"'] |
658 | | /* assert P |= CTL: "ctl-formula" */ |
659 | | ;AssertionExpr = assertCtl(N,P,Formula,_) -> |
660 | | L = [' |= ', 'CTL: ', '\"', Formula, '\"'] |
661 | | /* assert not? P :[Mod [E]] */ |
662 | | ;AssertionExpr = assertModelCheckExt(N,P,Mod,E) -> |
663 | | fdr_model(Mod,Model), |
664 | | fdr_ext(E,Ext), |
665 | | L=[Model,Ext] |
666 | | /* assert not? P :[Mod] */ |
667 | | ;AssertionExpr = assertModelCheck(N,P,Mod) -> |
668 | | fdr_single_model(Mod,Model), |
669 | | L=[Model] |
670 | | ; |
671 | | add_internal_error('Internal Error (CSP-M Parser): Unexpected assertion predicate: ', |
672 | | translate_csp_assertion(AssertionExpr,ConcRes)) |
673 | | ), |
674 | | adding_not(N,Not), |
675 | | translate_cspm_state(P,Proc), |
676 | | concatenate_string_list([Not, Proc|L], ConcRes). |
677 | | |
678 | | %%%%%%%%%%%%%%%%%%%%%%%%%%% Testing get_csp_processes/1, get_csp_process/2 and translate_csp_assertions/2 predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%% |
679 | | find_and_assert_all_csp_processes_from_arity_zero :- |
680 | | findall(P,(bindval(P,Body,_),definite_cspm_process_expression(Body),assertz(is_csp_process(P))),_L). |
681 | | |
682 | | clear_all_is_csp_process_facts :- retractall(is_csp_process(_)). |
683 | | |
684 | | :- assert_must_succeed((find_and_assert_all_csp_processes_from_arity_zero, |
685 | | get_csp_processes(Res), %print(Res),nl, |
686 | | clear_all_is_csp_process_facts, |
687 | | Res==list(['P(-)','Q(-)','SEND','REC','SYSTEM','GEN1','GEN2','MAIN']))). |
688 | | :- assert_must_succeed((findall(assertRef(A,B,C,D,S), |
689 | | haskell_csp: assertRef(A,B,C,D,S),L),haskell_csp: translate_csp_assertions(L,String), |
690 | | String == 'CSP: MAIN [T= CSP: PROB_TEST_TRACE$not CSP: PROB_TEST_TRACE [T= CSP: MAIN$')). |
691 | | :- assert_must_succeed((findall(assertModelCheckExt(A,B,C,D), |
692 | | haskell_csp: assertModelCheckExt(A,B,C,D),L), |
693 | | findall(assertModelCheck(A,B,C),haskell_csp:assertModelCheck(A,B,C),L1,L), |
694 | | haskell_csp: translate_csp_assertions(L1,String), |
695 | | String == 'CSP: a.1->P :[ livelock free ]$CSP: SYSTEM [|{|left,right|}|] GEN1 :[ deterministic [F] ]$not CSP: SYSTEM [|{|left,right|}|] GEN1 :[ deadlock free [FD] ]$')). |
696 | | |
697 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
698 | | |
699 | | /* Tcl_Tk cannot handle complicated prolog strings, that's why we have to convert the from the Csp prolog file filtered assertions |
700 | | into simple string. Assertions will be separated with the '$' symbol. */ |
701 | | get_csp_assertions_as_string(CSPFile,R) :- |
702 | | read_compiled_prolog_file(CSPFile,A,filter_assertion_declarations), |
703 | | translate_csp_assertions(A,R),debug_print(9,'string_for_tcl: '),debug_println(9,R). |
704 | | |
705 | | /* The same as above for the processes, these will be separate by '$' as well. Needed for the process comboboxes in the |
706 | | 'Check Csp Assertions' window in Tcl_Tk. */ |
707 | | get_csp_processes(list(R1)) :- |
708 | | debug_nl(9), debug_println(9,getting_csp_processes), |
709 | | findall(bindval(P,_,_),bindval(P,_,_),L), |
710 | | findall(agent(F,Body,_),agent(F,Body,_),L1,L), |
711 | | get_processes(L1,R1), |
712 | | debug_println(9,R1), debug_nl(9). |
713 | | |
714 | | get_processes([],[]). |
715 | | get_processes([bindval(A,_,_)|T],R) :- !, |
716 | | ( animatable_process(A) -> R=[A|Res] ; R=Res), |
717 | | get_processes(T,Res). |
718 | | get_processes([agent(Fun,Body,_)|T],R) :- !, |
719 | | ( (definite_cspm_process_expression(Body),animatable_process_with_arguments(Fun,proc(F,N))) |
720 | | -> proc_with_arguments_to_string(F,N,FunRes),R = [FunRes|Res] |
721 | | ; R=Res |
722 | | ), |
723 | | get_processes(T,Res). |
724 | | |
725 | | /* ------------------------------------------------------------------------------------------------------------------------- */ |
726 | | |
727 | | clear_cspm_spec :- % nl,print('RESET CSPM'),nl,nl, |
728 | | retractall(parseResult(_,_,_,_,_)), |
729 | | retractall(channel(_,_)), |
730 | | retractall(bindval(_,_,_)), |
731 | | retractall(cspTransparent(_)), |
732 | | retractall(agent(_,_,_)), |
733 | | retractall(dataTypeDef(_,_)), |
734 | | retractall(subTypeDef(_,_)), |
735 | | retractall(nameType(_,_)), |
736 | | retractall(assertRef(_,_,_,_,_)), |
737 | | % retractall(assertTauTrio(_,_,_,_,_,_)), |
738 | | retractall(assertModelCheckExt(_,_,_,_)), |
739 | | retractall(assertModelCheck(_,_,_)), |
740 | | retractall(channel_type_list(_,_)), |
741 | | retractall(csp_full_type_constructor(_,_,_)), |
742 | | retractall(pragma(_)), |
743 | | retractall(enum_warning_occured(_,_,_)). |
744 | | %retractall(csp_full_expanded_type(_,_)), |
745 | | %retractall(expanded_setFromTo(_,_,_)). |
746 | | |
747 | | %:- use_module(probsrc(eventhandling),[register_event_listener/3]). |
748 | | :- register_event_listener(clear_specification,clear_cspm_spec, |
749 | | 'Clearing any CSPM Specification.'). |
750 | | |
751 | | is_a_datatype(DT,L) :- |
752 | ? | (dataTypeDef(DT,L) ; subTypeDef(DT,L)). |
753 | | |
754 | | /* Tests for the is_not_infinite_type/1 predicate (see .pl translation sample on lines 68-106 ) */ |
755 | | |
756 | | :- assert_must_fail((assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])), |
757 | | assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])), |
758 | | haskell_csp:is_not_infinite_type(closure([tuple([receive])])))). |
759 | | :- assert_must_succeed((assertz(csp_full_type_constructor(_,'FRUIT', |
760 | | [constructor(apples),construcor(oranges),constructor(pears)])), |
761 | | haskell_csp:is_not_infinite_type(closure([tuple([left])])))). |
762 | | :- assert_must_fail((assertz(csp_full_type_constructor(_,'FRUIT', |
763 | | [constructor(apples),construcor(oranges),constructor(pears)])), |
764 | | assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])), |
765 | | assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])), |
766 | | haskell_csp:is_not_infinite_type(closure([tuple([left]), |
767 | | tuple([mid]),tuple([right]),tuple([receive])])))). |
768 | | :- assert_must_fail((assertz(csp_full_type_constructor(ste,'Inf',['Seq'(dataType('FRUIT'))])), |
769 | | assertz(csp_full_type_constructor(_,'FRUIT', |
770 | | [constructor(apples),construcor(oranges),constructor(pears)])), |
771 | | haskell_csp:is_not_infinite_type(closure([tuple([infinite])])))). |
772 | | :- assert_must_succeed((assertz(csp_full_type_constructor(_,'FRUIT', |
773 | | [constructor(apples),construcor(oranges),constructor(pears)])), |
774 | | haskell_csp:is_not_infinite_type(closure([tuple([left]),tuple([mid]),tuple([right])])))). |
775 | | :- assert_must_fail((assertz(csp_full_type_constructor(_,'FRUIT', |
776 | | [constructor(apples),construcor(oranges),constructor(pears)])), |
777 | | assertz(csp_full_type_constructor(_,'SubMsg',[dataType('Msg')])), |
778 | | assertz(csp_full_type_constructor(_,'Msg',[dataType('SubMsg')])), |
779 | | assertz(csp_full_type_constructor(ste,'Inf',['Seq'(dataType('FRUIT'))])), |
780 | | haskell_csp:is_not_infinite_type(closure([tuple([left]),tuple([mid]), |
781 | | tuple([right]),tuple([infinite]),tuple([receive])])))). |
782 | | |
783 | | :- assert_must_fail(haskell_csp:is_not_infinite_type(setFrom(1))). |
784 | | :- assert_must_fail(haskell_csp:channel_type_is_finite('dotTupleType'([setValue([int(1),int(2)]), setFrom(1)]),2)). |
785 | | :- assert_must_succeed((assertz(name_type('S', setFromTo(1,3))), haskell_csp: channel_type_is_finite('S',2))). |
786 | | |
787 | | /* is_not_infinite_type/1 */ |
788 | | /* check if the Event set is from infinite type */ |
789 | | /* needed for the refinement checker, when generating counter-examples, TODO: re-implement predicate */ |
790 | | is_not_infinite_type(X) :- var(X),!,fail. |
791 | | % at first we are only interesting of checking the whole closure for infinite types |
792 | | is_not_infinite_type(closure(X)) :- !, |
793 | | closure_is_finite_set(X). |
794 | | %% TODO: Cover all other cases for this predicate (like setValue, setFrom, ...) |
795 | | |
796 | | |
797 | | closure_is_finite_set(L) :- |
798 | | maplist(single_element_closure_is_finite,L). |
799 | | |
800 | | % the closure is basically the set of all channels in a specification |
801 | | single_element_closure_is_finite(tuple([Ch|_List])) :- |
802 | | (channel_type_list(Ch,ChannelTypeList) -> true |
803 | | ; print(no_channel_type(Ch))), |
804 | | !, |
805 | | l_channel_type_is_finite(ChannelTypeList,2). |
806 | | single_element_closure_is_finite(_X). |
807 | | |
808 | | channel_type_is_finite(intType,_Rec) :- !,fail. |
809 | | channel_type_is_finite(boolType,_Rec) :- !. |
810 | | channel_type_is_finite(setFromTo(_L,_U),_Rec) :- !. |
811 | | channel_type_is_finite(setFrom(_L),_Rec) :- !,fail. % endless set |
812 | | % we got a dot tuple of types, we need to check for infinity all types in the tuple. |
813 | | channel_type_is_finite('dotTupleType'(List),Rec):-!, |
814 | | l_channel_type_is_finite(List,Rec). |
815 | | channel_type_is_finite('typeTuple'(List),Rec) :- !, |
816 | | l_channel_type_is_finite(List,Rec). % the same as last clausel |
817 | | channel_type_is_finite(setValue(_L),_Rec) :- !. |
818 | | channel_type_is_finite(dataType(DT),Rec) :- |
819 | ? | is_a_datatype(DT,_),!, |
820 | | check_datatype_el(DT,Rec). |
821 | | channel_type_is_finite('Seq'(setValue([])),_Rec) :- !. % Seq({}) is the empty sequence <> |
822 | | channel_type_is_finite('Seq'(_Type),_Rec) :- !, fail. % e.g. Seq({a,b,c}) indicator for endless datatype (there are endless numbers of sequences) |
823 | | channel_type_is_finite(X,Rec) :- |
824 | | name_type(X,Type),!, |
825 | | channel_type_is_finite(Type,Rec). |
826 | | channel_type_is_finite(_X,_Rec). |
827 | | |
828 | | check_datatype_el(DT,MaxRec) :- |
829 | | (MaxRec > 0 -> M1 is MaxRec -1, |
830 | ? | (csp_constructor(_Cons,DT,ArgSubTypes) -> /* Subtypes recursion. */ l_channel_type_is_finite(ArgSubTypes,M1) |
831 | | ; /* constructors from finite type (there is no recursion)*/ true)). |
832 | | /* ending recursion of datatypes (recursion doesn't mean infinite type) */ |
833 | | |
834 | | channel_type_is_finite_rec(Rec,HType) :- |
835 | | channel_type_is_finite(HType,Rec). |
836 | | |
837 | | l_channel_type_is_finite(L,Rec) :- |
838 | | maplist(channel_type_is_finite_rec(Rec),L). |
839 | | |
840 | | /* |
841 | | l_channel_type_is_finite([],_Rec). |
842 | | l_channel_type_is_finite([HType|T],Rec) :- |
843 | | (channel_type_is_finite(HType,Rec) -> |
844 | | l_channel_type_is_finite(T,Rec)). |
845 | | */ |
846 | | |
847 | | /* end of the implementation of is_not_infinite_type/1 predicate */ |
848 | | |
849 | | get_csp_assertions(CSP_Assertions) :- |
850 | | findall(Ass, (is_assertion(Ass),Ass), CSP_Assertions), |
851 | | debug_println(9,CSP_Assertions). |
852 | | |
853 | | /* |
854 | | get_csp_assertions_enum(CSPFile, Result) :- |
855 | | read_compiled_prolog_file(CSPFile,CSP_Assertions,filter_assertion_declarations), |
856 | | enumerate_assertions(CSP_Assertions,Result). |
857 | | |
858 | | :- assert_must_succeed(haskell_csp:enumerate_assertions([a,b,c,d,e,f],[(a,0),(b,1),(c,2),(d,3),(e,4),(f,5)])). |
859 | | :- assert_must_succeed(haskell_csp:enumerate_assertions([],[])). |
860 | | enumerate_assertions(L,R) :- enumerate_assertions_acc(L,R,0). |
861 | | enumerate_assertions_acc([],[],_). |
862 | | enumerate_assertions_acc([H|T],[(H,Acc)|R],Acc) :- New_Acc is Acc +1, enumerate_assertions_acc(T,R,New_Acc). |
863 | | */ |
864 | | |
865 | | cia_consult_without_redefine_warning(File) :- |
866 | | (file_exists(File) -> true ; (add_error(haskell_csp,'CSP-M PL File does not exist: ',File),fail)), |
867 | | debug_println(15,consult_without_redefine(File)), |
868 | | get_set_optional_prolog_flag(redefine_warnings, Old, off), |
869 | | get_set_optional_prolog_flag(single_var_warnings, Old2, off), |
870 | | get_set_optional_prolog_flag(discontiguous_warnings, Old3, off), |
871 | | (load_files(File,[compilation_mode(assert_all)]) %consult(File) |
872 | | -> OK=true ; OK=false), |
873 | | get_set_optional_prolog_flag(redefine_warnings, _, Old), |
874 | | get_set_optional_prolog_flag(single_var_warnings, _, Old2), |
875 | | get_set_optional_prolog_flag(discontiguous_warnings, _, Old3), |
876 | | OK=true. |
877 | | |
878 | | /* ------------------------------------- */ |
879 | | |
880 | | |
881 | | /* THE CSP OPERATIONAL SEMANTICS */ |
882 | | |
883 | | |
884 | | /* ------------------------------------- */ |
885 | | % |
886 | | %trans_pre_compute(X,Results) :- |
887 | | % findall(res(X,A,X1,Residue),call_residue(cspm_trans(X,A,X1),Residue), Results). |
888 | | % |
889 | | % |
890 | | %trans_cont(Results,X,A,X1) :- |
891 | | % member(res(X,A,X1,Residue),Results), |
892 | | % % print(trans_cont(X,A,X1,Residue)),nl, |
893 | | % call(Residue). |
894 | | |
895 | | /* ------------------------------------- */ |
896 | | |
897 | | %cspm_trans(E,_,_) :- print(cspm_trans(E)),nl,fail. |
898 | | |
899 | | :- assert_must_succeed(( haskell_csp:functor_dif(X,f), X=g(_) )). |
900 | | :- assert_must_fail(( haskell_csp:functor_dif(X,f), X=f(_) )). |
901 | | |
902 | | :- block functor_dif(-,?). |
903 | | functor_dif(X,FY) :- functor(X,FX,_), FX\=FY. |
904 | | |
905 | | :- assert_pre(haskell_csp:cspm_trans(E,_,_,_), nonvar(E)). |
906 | | :- assert_post(haskell_csp:cspm_trans(_,A,NE,_), (nonvar(A),nonvar(NE))). |
907 | | :- block cspm_trans(-,?,?,?). |
908 | | % TO DO: comment out for efficiency: |
909 | | /* ------ */ |
910 | | %cspm_trans(X,_,_) :- debug_println(9,cspm_trans(X)), var(X), |
911 | | % add_error(csp_interpreter,'### Variable process expression in cspm_trans !!',X), fail. |
912 | | cspm_trans(X,_,_,_) :- undefined_process_construct(X), |
913 | | (get_preference(cspm_animate_all_processes,true),string_term_with_args(X) -> |
914 | | add_message(cspm_trans,'Warning: Tried to expand a process with non-ground arguments: ',X),fail |
915 | | ;add_error_fail(csp_interpreter,'### Undefined Construct in cspm_trans !! ',X) |
916 | | ). |
917 | | /* ------ */ |
918 | | |
919 | | cspm_trans(stop(_),_,_,_) :- fail. |
920 | | cspm_trans(omega,_,_,_) :- fail. |
921 | | |
922 | | cspm_trans(skip(SrcSpan),tick(SrcSpan),omega,_). |
923 | | %cspm_trans(skip(SrcSpan),tick(SrcSpan),stop(SrcSpan),_). |
924 | | |
925 | | %cspm_trans(cspPrint(X),io(V1,print,no_loc_info_available),cspPrint(X)) :- evaluate_argument(X,V1). |
926 | | |
927 | | cspm_trans('CHAOS'(SrcSpan,_Set),tau(chaos_stop(SrcSpan)),stop(SrcSpan),_). |
928 | | cspm_trans('CHAOS'(SrcSpan,Set),io(V1,Ch,SrcSpan),'CHAOS'(SrcSpan,Set),_WF) :- /* or should we add an intermediate tau ?? */ |
929 | | % print(evaluate_argument(Set,S)),nl, |
930 | | evaluate_argument(Set,S), |
931 | | % print(chaos(S)),nl, |
932 | | expand_channel_pattern_expression(S,ECList,SrcSpan), |
933 | | % print(setup_channel_skeleton(io(V1,Ch,SrcSpan))),nl, |
934 | ? | setup_channel_skeleton(io(V1,Ch,SrcSpan)), |
935 | | % print(chaos(io(V1,Ch),ECList)),nl, |
936 | | hidden(io(V1,Ch,SrcSpan),ECList). |
937 | | |
938 | | % print(hidden(io(V1,Ch,SrcSpan),ECList)),nl. |
939 | | |
940 | | /* external choice */ |
941 | ? | cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(X,A,X1,WF), |
942 | | shift_span_for_left_branch(Span,LSpan), |
943 | ? | merge_span_into_event(A,LSpan,NA), |
944 | | ( top_level_dif(A,tau(_)), Res=X1 |
945 | | ; |
946 | | A=tau(_), tl_normalise('[]'(X1,Y,Span),Res) ). |
947 | ? | cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(Y,A,Y1,WF), |
948 | | shift_span_for_right_branch(Span,RSpan), |
949 | ? | merge_span_into_event(A,RSpan,NA), |
950 | | ( top_level_dif(A,tau(_)), Res=Y1 |
951 | | ; |
952 | | A=tau(_), tl_normalise('[]'(X,Y1,Span),Res) ). |
953 | | |
954 | | /* internal choice */ |
955 | | cspm_trans('|~|'(X,_Y,SrcSpan),tau(int_choice_left(SrcSpan,LSpan)),X,_WF) :- |
956 | | shift_span_for_left_branch(SrcSpan,LSpan). |
957 | | cspm_trans('|~|'(_X,Y,SrcSpan),tau(int_choice_right(SrcSpan,RSpan)),Y,_WF) :- |
958 | | shift_span_for_right_branch(SrcSpan,RSpan). |
959 | | |
960 | | /* -> PREFIX */ |
961 | | /* Note: set restrictions on values are encoded as inGuard Expressions */ |
962 | | cspm_trans(prefix(SPAN1,Values,ChannelExpr,CSP,SPAN2), io(EV,Channel,SPAN), NormCSP,WF) :- |
963 | ? | evaluate_channel_outputs(Values,ChannelExpr,EV,Channel,SPAN,WF), |
964 | | unify_spans(SPAN1,SPAN2,SPAN), |
965 | ? | full_normalise_csp_process(CSP,NormCSP). % ,print(prefix(io(EV,Channel))),nl. |
966 | | |
967 | | |
968 | | /* interleave */ |
969 | | %cspm_trans('|||'(X,Y,Span),A,R,WF) :- cspm_trans(sharing(setValue([]),X,Y),A,R). |
970 | | /* Firing rules for the |||-operator: |
971 | | |
972 | | P -a> P' |
973 | | ---------------------------- |
974 | | P ||| Q -a> P' ||| Q |
975 | | |
976 | | Q -a> Q' |
977 | | ---------------------------- |
978 | | P ||| Q -a> P ||| Q' |
979 | | |
980 | | |
981 | | P -tick> P' |
982 | | ---------------------------- |
983 | | P ||| Q -tau> Omega ||| Q |
984 | | |
985 | | |
986 | | Q -tick> Q' |
987 | | ---------------------------- |
988 | | P ||| Q -tau> P ||| Omega |
989 | | |
990 | | */ |
991 | | |
992 | | cspm_trans('|||'(omega,omega,Span),tick(Span),omega,_). |
993 | | cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :- |
994 | ? | cspm_trans(X, ActionX, X1,WF), |
995 | | shift_span_for_left_branch(ISpan,LSpan), |
996 | | ( ActionX=tick(_), X2=omega |
997 | | ; functor_dif(ActionX,tick), X2=X1 |
998 | | ), |
999 | | merge_span_into_event(ActionX,LSpan,MA), |
1000 | | (ActionX=tick(_) -> A=tau(MA); A=MA), |
1001 | ? | tl_normalise('|||'(X2,Y,ISpan),Res). |
1002 | | cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :- |
1003 | ? | cspm_trans(Y, ActionY, Y1,WF), |
1004 | | shift_span_for_right_branch(ISpan,RSpan), |
1005 | | ( ActionY=tick(_), Y2=omega |
1006 | | ; functor_dif(ActionY,tick), Y2=Y1 |
1007 | | ), |
1008 | | merge_span_into_event(ActionY,RSpan,MA), |
1009 | | (ActionY=tick(_) -> A=tau(MA); A=MA), |
1010 | ? | tl_normalise('|||'(X,Y2,ISpan),Res). |
1011 | | |
1012 | | /* sequential composition */ |
1013 | | cspm_trans(';'(P,Q,SeqSpan),AX,Res,WF) :- |
1014 | ? | cspm_trans(P,A,P1,WF), |
1015 | | ( A=tick(_), |
1016 | | merge_span_into_event(A,SeqSpan,MA), |
1017 | | AX = tau(MA), |
1018 | ? | full_normalise_csp_process(Q,Res) /* is this required ?? */ |
1019 | | ; functor_dif(A,tick), AX=A, |
1020 | | tl_normalise(';'(P1,Q,SeqSpan),Res) |
1021 | | ). |
1022 | | |
1023 | | |
1024 | | /* Sharing: [| a |] */ |
1025 | | cspm_trans(sharing(CList,X,Y,SrcSpan),A,Res,WF) :- |
1026 | | evaluate_argument(CList,EvCList), |
1027 | | expand_channel_pattern_expression(EvCList,ECList,SrcSpan), |
1028 | ? | cspm_trans(esharing(ECList,X,Y,SrcSpan),A,Res,WF). |
1029 | | cspm_trans(esharing(_,omega,omega,SrcSpan), tick(SrcSpan), omega ,_WF). |
1030 | | cspm_trans(esharing(CList,X,Y,SrcSpan), Action, Result,WF) :- |
1031 | ? | cspm_trans(X, ActionX, X1,WF), |
1032 | | ( (ActionX=tick(TS), |
1033 | | shift_span_for_left_branch(SrcSpan,LSpan), |
1034 | | merge_span_into_event(tau(tick(TS)),LSpan,Action), |
1035 | | Result = esharing(CList,omega,Y,SrcSpan)) |
1036 | | ; (functor_dif(ActionX,tick), |
1037 | | shift_span_for_left_branch(SrcSpan,LSpan), |
1038 | | merge_span_into_event(ActionX,LSpan,Action), |
1039 | | not_hidden(ActionX,CList), /* covers tau */ |
1040 | | Result = esharing(CList,X1,Y,SrcSpan)) |
1041 | | ; (ActionX=io(V1,Ch,Sp1), Action = io(V,Ch,Span), |
1042 | | %((transferReq,[int(3),ac1,ac2,true])=(Ch,V1) -> trace ; true), |
1043 | | Result = esharing(CList,X1,Y1,SrcSpan), |
1044 | | unify_spans(Sp1,SrcSpan,SP1b), |
1045 | | hidden(Action,CList), |
1046 | | unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed |
1047 | | % print(call_cspm_transY_B1(Y,io(V2,Ch),Y1)),nl, |
1048 | ? | cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */ |
1049 | | unify_spans(SP1b,Sp2,Span3), |
1050 | | Span = span_info(sharing,Span3) |
1051 | | ) |
1052 | | ). |
1053 | | cspm_trans(esharing(CList,X,Y,SrcSpan), Action2, Result,WF) :- |
1054 | | shift_span_for_right_branch(SrcSpan,RSpan), |
1055 | | % print(esharing_call_cspm_transY_B2(Y,ActionY,Y1)),nl, |
1056 | ? | cspm_trans(Y,ActionY,Y1,WF), /* this gets computed a second time; is there a way to avoid this? */ |
1057 | | %print(esharing_cspm_transY_B2(Y,ActionY)),nl, |
1058 | | ( ActionY = tick(TS), Action=tau(tick(TS)), Result=esharing(CList,X,omega,SrcSpan) |
1059 | | ; functor_dif(ActionY,tick), ActionY = Action, |
1060 | | %print(try_non_sharing(ActionY)),nl, |
1061 | | not_hidden(ActionY,CList), /* covers tau */ |
1062 | | Result = esharing(CList,X,Y1,SrcSpan) |
1063 | | ), |
1064 | | merge_span_into_event(Action,RSpan,Action2). |
1065 | | |
1066 | | |
1067 | | /* Linked Parallel [ l <-> r,.. ] */ |
1068 | | cspm_trans(lParallel(LinkList,X,Y,Span), Action,Result,WF) :- |
1069 | | evaluate_link_list(LinkList,EvLinkRenameList), |
1070 | | %print(evlinklist(LinkList,EvLinkRenameList)),nl, % |
1071 | ? | cspm_trans(elinkParallel(EvLinkRenameList,X,Y,Span),Action,Result,WF). |
1072 | | cspm_trans(elinkParallel(_,omega,omega,Span), tick(Span), omega ,_WF). |
1073 | | cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action,Result,WF) :- |
1074 | ? | cspm_trans(X,AX,X2,WF), % print(elink_x(X,AX,X2,EvLinkRenameList)),nl, print('State: '),print(X),nl, |
1075 | | ( AX = tick(TS), |
1076 | | shift_span_for_left_branch(LinkSpan,LSpan), |
1077 | | merge_span_into_event(tau(tick(TS)),LSpan,Action), |
1078 | | Result=elinkParallel(EvLinkRenameList,omega,Y,LinkSpan) |
1079 | | ; |
1080 | | functor_dif(AX,tick), |
1081 | | ( shift_span_for_left_branch(LinkSpan,LSpan), |
1082 | | merge_span_into_event(AX,LSpan,Action), |
1083 | | Result = elinkParallel(EvLinkRenameList,X2,Y,LinkSpan), |
1084 | ? | not_renamed(AX,EvLinkRenameList) |
1085 | | % ,print(not_renamed(AX,EvLinkRenameList)),nl %% |
1086 | | ; |
1087 | | Action=tau(link(AX,io(V,Ch,Span))), |
1088 | | Result = elinkParallel(EvLinkRenameList,X2,Y2,LinkSpan), |
1089 | ? | force_rename_action(AX,EvLinkRenameList,io(V1,Ch,Sp0)), |
1090 | | unify_spans(LinkSpan,Sp0,Sp1), |
1091 | | %% print(renamed(AX,io(V1,Ch),EvLinkRenameList)),nl, %% |
1092 | | unify_values(V1,V2,V,Ch,Sp1), % try and also incorporate Sp2 Span, without compromising speed |
1093 | | % MAYBE TO DO ?: instantiate V2 as much as possible ! --> in()/dot issues |
1094 | | %% print(cspm_trans(Y,io(V2,Ch,Sp2),Y2)),nl, %% |
1095 | ? | cspm_trans(Y,io(V2,Ch,Sp2),Y2,WF), /* <---- Y will be recomputed for every solution of X !!! */ |
1096 | | unify_spans(Sp1,Sp2,Span3), |
1097 | | %% print(unify(Sp1,Sp2,Span3)),nl, %% |
1098 | | Span = span_info(sharing,Span3) |
1099 | | ) |
1100 | | ). |
1101 | | cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action2, |
1102 | | elinkParallel(EvLinkRenameList,X,YR,LinkSpan),WF) :- |
1103 | | shift_span_for_right_branch(LinkSpan,RSpan), |
1104 | | rev_rename_list(EvLinkRenameList,RevList), |
1105 | ? | cspm_trans(Y,ActionY,Y2,WF), /* TO DO: try and avoid recomputation of cspm_trans(Y) ?! */ |
1106 | | ( ActionY=tick(TS), Action=tau(tick(TS)), YR=omega |
1107 | | ; |
1108 | ? | functor_dif(ActionY,tick),ActionY=Action,YR=Y2,not_renamed(Action,RevList) |
1109 | | ), |
1110 | | merge_span_into_event(Action,RSpan,Action2). |
1111 | | |
1112 | | cspm_trans(aParallel(CListX,X,CListY,Y,SrcSpan),A,NewState,WF) :- %print(expanding_aparx),nl, |
1113 | | evaluate_argument(CListX,EvCListX), |
1114 | | expand_channel_pattern_expression(EvCListX,ECListX,SrcSpan), %print(expanding_apary),nl, |
1115 | ? | evaluate_argument(CListY,EvCListY), |
1116 | | expand_channel_pattern_expression(EvCListY,ECListY,SrcSpan), |
1117 | | Expanded = eaParallel(ECListX,X,ECListY,Y,SrcSpan), |
1118 | | %we have expanded the channel synchronisation sets; avoid recomputing them every time |
1119 | | % TO DO: investigate whether it also makes sense to precompute intersection |
1120 | ? | cspm_trans(Expanded,A,NewState,WF). |
1121 | | cspm_trans(eaParallel(_,omega,_,omega,SrcSpan), tick(SrcSpan), omega ,_WF). |
1122 | | cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),A,eaParallel(ECListX,X2,ECListY,Y1,SrcSpan),WF) :- |
1123 | | %trans_pre_compute(Y,Results), |
1124 | ? | cspm_trans(X, AX, X1,WF), |
1125 | | % print(apar_x(AX, from(X))),nl, |
1126 | | ( X2=X1,Y1=Y, |
1127 | | hidden_or_tau(AX,ECListX), |
1128 | | not_hidden(AX,ECListY), |
1129 | | shift_span_for_left_branch(SrcSpan,LSpan), |
1130 | | merge_span_into_event(AX,LSpan,A) |
1131 | | ; |
1132 | | AX=tick(_TS), X2=omega,Y1=Y, |
1133 | | shift_span_for_left_branch(SrcSpan,LSpan), |
1134 | | merge_span_into_event(tau(AX),LSpan,A) |
1135 | | ; |
1136 | | AX=io(V1,Ch,Sp1), X2=X1, A = io(V,Ch,Span), |
1137 | | % nl,print(try_apar_sync(V1,Ch)),nl, |
1138 | | hidden(io(V1,Ch,Sp1),ECListX), % print(left_ok),nl, % do V1 instead of V ? |
1139 | | hidden(io(V,Ch,Span),ECListY), % print(right_ok),nl, % V2 instead of V |
1140 | | % Synchronisation possible |
1141 | | unify_spans(Sp1,SrcSpan,SP1b), |
1142 | | unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed |
1143 | | %print(trying(aparY(io(V2,Ch,Sp2)))),nl, % |
1144 | ? | cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */ |
1145 | | % trans_cont(Results,Y, io(V2,Ch,Sp2), Y1), |
1146 | | % print(done(aparY(io(V2,Ch,Sp2)))),nl, % |
1147 | | unify_spans(SP1b,Sp2,Span3), |
1148 | | Span = span_info(sharing,Span3) |
1149 | | ). |
1150 | | cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),AS,eaParallel(ECListX,X,ECListY,Y2,SrcSpan),WF) :- |
1151 | ? | cspm_trans(Y, AY, Y1,WF), /* To do: try and avoid recomputation of cspm_trans(Y) ?! */ |
1152 | | ( AY=A, Y2=Y1, |
1153 | | hidden_or_tau(A,ECListY), not_hidden(A,ECListX) |
1154 | | ; |
1155 | | AY=tick(_TS), A = tau(AY), Y2=omega |
1156 | | ), |
1157 | | shift_span_for_right_branch(SrcSpan,RSpan), |
1158 | | merge_span_into_event(A,RSpan,AS). |
1159 | | |
1160 | | /* only used for outside xtl_interface ; not used internally anymore */ |
1161 | ? | cspm_trans(val_of(X,Span),A,NewExpr,WF) :- (symbol(RenamedX,X,_,_) -> cspm_trans(agent_call(Span,RenamedX,[]),A,NewExpr,WF); |
1162 | | cspm_trans(X,A,NewExpr,WF)). |
1163 | | cspm_trans(agent_call(Span,F,Par),NA,NNewExpr,WF) :- |
1164 | ? | unfold_function_call_once(F,Par,Value,Span), |
1165 | ? | cspm_trans(Value,A,NewExpr,WF), |
1166 | ? | full_normalise_csp_process(NewExpr,NNewExpr), |
1167 | | % print(merge_agcall(A,Span)),nl, |
1168 | ? | merge_span_into_event(A,Span,NA). |
1169 | | |
1170 | | % Par = [[x],[y]] |
1171 | | cspm_trans(agent_call_curry(F,Par),NA,NNewExpr,WF) :- |
1172 | | Span=no_loc_info_available, |
1173 | | unfold_function_call_curry_once(F,Par,Value,Span), |
1174 | | cspm_trans(Value,A,NewExpr,WF), |
1175 | | full_normalise_csp_process(NewExpr,NNewExpr), |
1176 | | % print(merge_agcall(A,Span)),nl, |
1177 | | merge_span_into_event(A,Span,NA). |
1178 | | |
1179 | | cspm_trans(builtin_call(X),Action,NewExpr,WF) :- % builtin_call is normally removed by precompilation; but can remain, e.g., for assertions |
1180 | | cspm_trans(X,Action,NewExpr,WF). |
1181 | | cspm_trans(head(X),Action,NewExpr,WF) :- force_evaluate_argument(X,EX),head_list(EX,Result), |
1182 | ? | cspm_trans(Result,Action,NewExpr,WF). |
1183 | | |
1184 | | /* hiding '\\' */ |
1185 | | |
1186 | | cspm_trans('\\'(Expr,CList,Span), A, Res ,WF) :- |
1187 | ? | evaluate_argument(CList,EvCList), |
1188 | | expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available), |
1189 | | % print(ehide(Expr,ECList,Span)),nl, |
1190 | ? | cspm_trans(ehide(Expr,ECList,Span),A,Res,WF). |
1191 | | |
1192 | | cspm_trans(ehide(Expr,CList,Span), A, Res ,WF) :- |
1193 | | % (nonvar(A) -> ((A=io(_,_,_);A=tick(_)) -> ActionX=A ; A=tau(hide(ActionX))) |
1194 | | % ; true), |
1195 | ? | cspm_trans(Expr,ActionX,X,WF), |
1196 | ? | cspm_hide_action(ActionX,X, CList,Span, A,Res). |
1197 | | |
1198 | | |
1199 | | cspm_trans(exception(CList,X,Y,Span), A, Res ,WF) :- |
1200 | | evaluate_argument(CList,EvCList), |
1201 | | expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available), |
1202 | | %print(exception(ECList,X,Y)),nl, |
1203 | ? | cspm_trans(eexception(ECList,X,Y,Span),A,Res,WF). |
1204 | | |
1205 | | cspm_trans(eexception(CList,X,Y,Span),A,Res,WF) :- % expanded version of exception |
1206 | ? | cspm_trans(X, ActionX, X1,WF), |
1207 | | ( functor_dif(ActionX,tick), ActionX=A, |
1208 | | Res = eexception(CList,X1,Y,Span), |
1209 | | not_hidden(A,CList) |
1210 | | ; merge_span_into_event(ActionX,Span,A), |
1211 | | Res = Y, |
1212 | | hidden(ActionX,CList) |
1213 | | ; A=tick(TS), ActionX=tick(TS), Res=omega % is this correct ?? |
1214 | | ). |
1215 | | |
1216 | | |
1217 | | /* timeout */ |
1218 | ? | cspm_trans('[>'(P,Q,SrcSpan),AS,Res,WF) :- cspm_trans(P,A,P1,WF), |
1219 | | ( A=tau(_), Res='[>'(P1,Q,SrcSpan) |
1220 | | ; |
1221 | | top_level_dif(A,tau(_)), % a transition which can be removed by the tau below |
1222 | | Res=P1 ), |
1223 | | shift_span_for_left_branch(SrcSpan,LSpan), |
1224 | | merge_span_into_event(A,LSpan,AS). |
1225 | | cspm_trans('[>'(_P,Q,SrcSpan),tau(timeout(SrcSpan)),Q,_WF). |
1226 | | |
1227 | | |
1228 | | /* interrupt */ |
1229 | | |
1230 | | cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :- |
1231 | ? | cspm_trans(X,A,X1,WF), %%print(interrupt_left(X,A,X1)),nl, |
1232 | | shift_span_for_left_branch(Span,LSpan), |
1233 | | merge_span_into_event(A,LSpan,NA), |
1234 | | ( A=tick(_), Res=X1 |
1235 | | ; functor_dif(A,tick), tl_normalise('/\\'(X1,Y,Span),Res) |
1236 | | ). |
1237 | | cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :- |
1238 | ? | cspm_trans(Y,A,Y1,WF), |
1239 | | shift_span_for_right_branch(Span,RSpan), |
1240 | | merge_span_into_event(A,RSpan,NA), |
1241 | | ( top_level_dif(A,tau(_)), Res=Y1 |
1242 | | ; A=tau(_), tl_normalise('/\\'(X,Y1,Span),Res) |
1243 | | ). |
1244 | | |
1245 | | /* renaming [[ old <- new,... | Generators ]] */ |
1246 | | cspm_trans(procRenamingComp(X,GeneratorList,RenameList),RA,Res,WF) :- |
1247 | | % print(procCompRenaming(GeneratorList)),nl, %% |
1248 | | % warning: does not have the rangeEnum wrapper expected |
1249 | | expand_set_comprehension(rangeEnum(RenameList),GeneratorList,setValue(ExpandedRenames)), |
1250 | | %print(exp(ExpandedRenames)),nl, |
1251 | ? | cspm_trans(procRenaming(ExpandedRenames,X,no_loc_info_available),RA,Res,WF). |
1252 | | |
1253 | | /* renaming [[ old <- new,... ]] */ |
1254 | | cspm_trans(procRenaming(RenameList,X,Span),RA,Res,WF) :- %print(procRename(RenameList)),nl, |
1255 | | evaluate_rename_list(RenameList,ERenameList), |
1256 | ? | cspm_trans(eprocRenaming(ERenameList,X,Span),RA,Res,WF). |
1257 | | cspm_trans(eprocRenaming(RenameList,X,Span),RAS,Res,WF) :- |
1258 | | %print('RENAME: '), translate:print_cspm_state(X),nl, |
1259 | ? | cspm_trans(X,A,X2,WF), |
1260 | | tl_normalise(eprocRenaming(RenameList,X2,Span),Res), |
1261 | | %print(try_rename(A,RenameList,RA,Span)),nl, %% |
1262 | | % it's still possible that A is non-ground term, i.e. there are a non-ground variables (c?x?y) in the sub-process, |
1263 | | % which have to be unified before applying renaming on them. |
1264 | ? | (ground(A) -> true; enumerate_action(A)), |
1265 | ? | rename_action(A,RenameList,RA), |
1266 | | %%% print(done_rename_action(A,RenameList,RA)),nl, |
1267 | | merge_span_into_event(RA,Span,RAS). |
1268 | | % print(merge_span(RA,Span,RAS)),nl, |
1269 | | |
1270 | | /* if then else */ |
1271 | | cspm_trans(ifte(Test,Then,Else,S1,S2,S3),A,X1,WF) :- |
1272 | | %nl,print(checking_if_test(Test,Then,Else)),nl, |
1273 | ? | evaluate_boolean_expression(Test,Res), |
1274 | | % print(if_evaluated_boolean_expression(Test,Res)),nl,nl, |
1275 | ? | cspm_if_trans(Res,Then,Else,A,X1,S1,S2,S3,WF). |
1276 | | |
1277 | | cspm_trans('&'(Test,Then),A,X1,WF) :- S=no_loc_info_available, |
1278 | ? | cspm_trans(ifte(Test,Then,stop(S),S,S,S),A,X1,WF). |
1279 | | |
1280 | | |
1281 | | cspm_trans(repChoice(GeneratorList,Body,Span), Action,X1,WF) :- |
1282 | | %% nl,print(repChoice(GeneratorList,Body)),nl, |
1283 | | replicate_expand_set_comprehension([Body],GeneratorList,setValue(Bodies)), |
1284 | | %% print(bodies(Bodies)),nl, |
1285 | | convert_into_choice(Bodies,Span,CHOICE), |
1286 | | %% print(choice(CHOICE)),nl, |
1287 | ? | cspm_trans(CHOICE,Action,X1,WF). |
1288 | | |
1289 | | cspm_trans(repInternalChoice(GeneratorList,Body,Span), tau(rep_int_choice(Span)),Res,_WF) :- |
1290 | | % print(repInternalChoice(GeneratorList,Span)),nl, |
1291 | | replicate_expand_set_comprehension([Body],GeneratorList,Bodies), |
1292 | | % print(bodies(Bodies)),nl,nl, |
1293 | | (is_empty_set(Bodies,true) |
1294 | | -> add_error(cspm_trans,'Empty set for replicated internal choice: ',Bodies,Span),fail |
1295 | ? | ; is_member_set(Res,Bodies)). |
1296 | | |
1297 | | cspm_trans(repInterleave(GeneratorList,Body,Span), A, X,WF) :- |
1298 | | %% tools:print_bt_message(repInterleave(GeneratorList)), %% |
1299 | | % multiplicity is relevant for |||, so add variables to Body below in case Variables are not used |
1300 | | extract_variables_from_generator_list(GeneratorList,Variables), |
1301 | | replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)), |
1302 | | convert_into_interleave(Bodies,Span,INTLV), |
1303 | | %% tools:print_bt_message(intlv(INTLV)), %% |
1304 | ? | cspm_trans(INTLV,A,X,WF). %, tools:print_bt_message(sol(A,X)). |
1305 | | |
1306 | | |
1307 | | cspm_trans(repSequence(GeneratorList,Body,Span),A,X,WF) :- |
1308 | | % print(repSequence(GeneratorList)),nl, %% |
1309 | | expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)), |
1310 | | % print(bodies(Bodies)),nl, %% |
1311 | | convert_into_seqcomp(Bodies,Span,SEQ), %print(sequential(SEQ)),nl, |
1312 | ? | cspm_trans(SEQ,A,X,WF). |
1313 | | |
1314 | | |
1315 | | cspm_trans(procRepAParallel(GeneratorList,pair(SyncSet,Body),Span), A, X,WF) :- |
1316 | | % multiplicity is relevant for sharing (it makes a difference if 1 or 2 copies are present), so add variables to Body below in case Variables are not used |
1317 | | extract_variables_from_generator_list(GeneratorList,Variables), |
1318 | | replicate_expand_set_comprehension([list([SyncSet,Body,Variables])],GeneratorList,setValue(Bodies)), |
1319 | ? | convert_into_eaParallel(Bodies,Span,APAR,_ALPH), |
1320 | ? | cspm_trans(APAR,A,X,WF). |
1321 | | |
1322 | | |
1323 | | cspm_trans(procRepLinkParallel(SyncSet,GeneratorList,Body,Span), A, X,WF) :- |
1324 | | expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)), |
1325 | | convert_into_linkParallel(Bodies,SyncSet,Span,APAR,Body), |
1326 | | %when((ground(APAR)), |
1327 | ? | cspm_trans(APAR,A,X,WF). |
1328 | | |
1329 | | cspm_trans(procRepSharing(SyncSet,GeneratorList,Body,Span), A, X,WF) :- |
1330 | | % print(procRepSharing(GeneratorList)),nl, |
1331 | | % multiplicity is relevant for sharing, so add variables to Body below in case Variables are not used |
1332 | | extract_variables_from_generator_list(GeneratorList,Variables), |
1333 | | replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)), |
1334 | | % print(bodies(Bodies)),nl, |
1335 | | convert_into_Sharing(Bodies,SyncSet,Span,APAR), %print(repshare(APAR)),nl, |
1336 | ? | cspm_trans(APAR,A,X,WF). |
1337 | | |
1338 | | % ---------- |
1339 | | |
1340 | | cspm_hide_action(ActionX,X, CList,Span, ActionAfterHiding,ResultingCSPExpr) :- |
1341 | | ( functor_dif(ActionX,tick), ActionX=ActionAfterHiding, |
1342 | | tl_normalise(ehide(X,CList,Span),ResultingCSPExpr), |
1343 | | not_hidden(ActionAfterHiding,CList) |
1344 | | ; merge_span_into_event(ActionX,Span,NActionX), |
1345 | | ActionAfterHiding=tau(hide(NActionX)), |
1346 | | tl_normalise(ehide(X,CList,Span),ResultingCSPExpr), |
1347 | | hidden(ActionX,CList) |
1348 | | ; ActionAfterHiding=tick(TS), ActionX=tick(TS), ResultingCSPExpr=omega |
1349 | | ). |
1350 | | |
1351 | | :- block cspm_if_trans(-,?,?,?, ?,?,?,?,?). |
1352 | | cspm_if_trans(true,Then,_Else,AS,X1,_S1,S2,_S3,WF) :- !, %print(ifte_true(Then)),nl, |
1353 | | full_normalise_csp_process(Then,NThen), |
1354 | ? | cspm_trans(NThen,A,X1,WF), |
1355 | | merge_span_into_event(A,S2,AS). |
1356 | | cspm_if_trans(false,_Then,Else,AS,X1,_S1,_S2,S3,WF) :- !, %print(ifte_false(Else)),nl, |
1357 | ? | full_normalise_csp_process(Else,NElse), cspm_trans(NElse,A,X1,WF), |
1358 | | merge_span_into_event(A,S3,AS). |
1359 | | cspm_if_trans(Other,Then,Else,AS,X1,S1,S2,S3,WF) :- |
1360 | | add_internal_error('Internal Error: Not a boolean value inside if-then-else: ', |
1361 | | cspm_if_trans(Other,Then,Else,AS,X1,S1,S2,S3,WF)), |
1362 | | fail. |
1363 | | |
1364 | | :- block convert_into_interleave(-,-,?). |
1365 | | convert_into_interleave([],Span,skip(Span)). |
1366 | | convert_into_interleave([na_tuple([H|_])|T],Span,R) :- convert_into_interleave3(T,H,Span,R). |
1367 | | :- block convert_into_interleave3(-,?,?,?). |
1368 | | convert_into_interleave3([],X,_Span,X). |
1369 | | convert_into_interleave3([na_tuple([H2|_])|T],H1,Span,'|||'(H1,Rest,Span)) :- |
1370 | | convert_into_interleave3(T,H2,Span,Rest). |
1371 | | |
1372 | | |
1373 | | :- block convert_into_choice(-,-,?). |
1374 | | convert_into_choice([],Span,stop(Span)). |
1375 | | convert_into_choice([H|T],Span,R) :- convert_into_choice3(T,H,Span,R). |
1376 | | :- block convert_into_choice3(-,?,?,?). |
1377 | | convert_into_choice3([],X,_Span,X). |
1378 | | convert_into_choice3([H2|T],H1,Span,'[]'(H1,Rest,Span)) :- convert_into_choice3(T,H2,Span,Rest). |
1379 | | |
1380 | | :- block convert_into_seqcomp(-,-,?). |
1381 | | convert_into_seqcomp(Bodies,Span,Res) :- convert_into_seqcomp2(Bodies,Span,Res). |
1382 | | convert_into_seqcomp2([],Span,skip(Span)) :- print(convert_into_seqcomp2([],Span,skip(Span))),nl. |
1383 | | convert_into_seqcomp2([H|T],Span,R) :- convert_into_seqcomp3(T,H,Span,R). |
1384 | | :- block convert_into_seqcomp3(-,?,?,?). |
1385 | | convert_into_seqcomp3([],X,_Span,X). |
1386 | | convert_into_seqcomp3([H2|T],H1,Span,';'(H1,Rest,Span)) :- |
1387 | | convert_into_seqcomp2([H2|T],Span,Rest). |
1388 | | |
1389 | | |
1390 | | :- block convert_into_eaParallel(-,-,?,?). |
1391 | | convert_into_eaParallel([],Span,skip(Span),setValue([])). |
1392 | | convert_into_eaParallel([H|T],Span,APAR,ALPH) :- |
1393 | ? | when(nonvar(T),convert_into_eaParallel3([H|T],Span,APAR,ALPH)). |
1394 | ? | convert_into_eaParallel3([list([Sync,X,_])],_Span,X,ESync) :- !, evaluate_argument(Sync,ESync). |
1395 | | convert_into_eaParallel3([list([CListX,X,_]),L2|T], Span,AlphPar, Alphabet ) :- |
1396 | ? | when(nonvar(T),(convert_into_eaParallel3([L2|T],Span, Rest,RestAlphabet), |
1397 | | evaluate_argument(CListX,ECListX), |
1398 | | evaluate_argument(union(RestAlphabet,ECListX),Alphabet), |
1399 | | /* put more complicated process onto the left: better efficiency for cspm_trans */ |
1400 | | % TO DO: we could think about splitting the list in two |
1401 | | AlphPar = aParallel(RestAlphabet,Rest,ECListX,X,Span))). % only aParallel |
1402 | | |
1403 | | |
1404 | | |
1405 | | :- block convert_into_Sharing(-,?,-,?). |
1406 | | convert_into_Sharing([],_,Span,skip(Span)). |
1407 | | convert_into_Sharing([na_tuple([H|_])|T],SyncSet,Span,R) :- convert_into_Sharing3([H|T],SyncSet,Span,R). |
1408 | | :- block convert_into_Sharing3(-,?,?,?). |
1409 | | convert_into_Sharing3([X],_Sync,_Span,Res) :- !, Res=X. |
1410 | | convert_into_Sharing3([X|T],CListX,Span,sharing(CListX,Rest,X,Span) ) :- |
1411 | | /* put more complicated process onto the left: better efficiency for cspm_trans */ |
1412 | | convert_into_Sharing(T,CListX,Span,Rest). |
1413 | | |
1414 | | :- block convert_into_linkParallel(-,?,?,?,?). |
1415 | | convert_into_linkParallel([],_,Span,skip(Span),Body) :- |
1416 | | add_error(haskell_csp,'Empty Set in Replicated Linked Parallel: ',Body,Span). |
1417 | | convert_into_linkParallel([H|T],SyncSet,Span,APAR,Body) :- |
1418 | | convert_into_linkParallel3([H|T],SyncSet,Span,APAR,Body). |
1419 | | :- block convert_into_linkParallel3(-,?,?,?,?). |
1420 | | convert_into_linkParallel3([X],_Sync,_Span,Res,_) :- !, Res=X. |
1421 | | convert_into_linkParallel3([X|T],CListX,Span,lParallel(CListX,X,Rest,Span),Body ) :- |
1422 | | /* in contrast to convert_into_Sharing3: we cannot put more complicated process onto the left: order matters for linked parallel */ |
1423 | | convert_into_linkParallel(T,CListX,Span,Rest,Body). |
1424 | | |
1425 | | /* ------------------------------------- */ |
1426 | | |
1427 | | /* top_level_normalise */ |
1428 | | /* Just check the top-level of the csp expression to see if it can |
1429 | | be simplified/normalised */ |
1430 | | tl_normalise('[]'(X,Y,Span),R) :- !, %print(tl(X)),nl,print(t2(Y)),nl,nl, |
1431 | | (X=Y -> R=X |
1432 | | ; is_stop(X,_) -> R=Y |
1433 | | ; is_stop(Y,_) -> R=X |
1434 | | ; Y='[]'(X,Y2,_) -> tl_normalise('[]'(X,Y2,Span),R) % X [] X [] Y == X [] Y ; relevant e.g. for ASTD library example |
1435 | | ; Y='[]'(Y2,X,_) -> tl_normalise('[]'(X,Y2,Span),R) |
1436 | | ; X='[]'(Y,X2,_) -> tl_normalise('[]'(Y,X2,Span),R) |
1437 | | ; X='[]'(X2,Y,_) -> tl_normalise('[]'(Y,X2,Span),R) |
1438 | | ; R='[]'(X,Y,Span) |
1439 | | ). /* TO DO: also sort X,Y !? */ |
1440 | | tl_normalise('|||'(X,Y,Span),R) :- !, |
1441 | | (is_stop(X,S),is_stop(Y,_) |
1442 | | -> R=stop(S) |
1443 | | ; ((X==omega;is_skip(X)) -> R=Y /* law 6.16 on page 142 of Roscoe's book */ |
1444 | | ; ((Y==omega;is_skip(Y)) -> R=X /* same law, for RHS */ |
1445 | | ; % this leads to performance loss: tl_normalise should only do top-level normalisation full_normalise_csp_process(X,XR), full_normalise_csp_process(Y,YR), |
1446 | | ((preference(cspm_detailed_animation,true);X @=<Y) |
1447 | | -> R='|||'(X,Y,Span) |
1448 | | ; R='|||'(Y,X,Span)) %% Warning: this can invalidate left-right Span information |
1449 | | ) |
1450 | | ) |
1451 | | ). % we could replace skip|||P by P |
1452 | | % (X==stop -> R=Y ; (Y==stop -> R=X ; R='|||'(X,Y))). P ||| stop not equal to stop (because of omega) |
1453 | | tl_normalise(ehide(X,CList,Span),R) :- !, |
1454 | | (is_stop(X,S) -> R=stop(S) % Concealement law L4 |
1455 | | ; is_skip(X,S) -> R=skip(S) % Concealement law L5 |
1456 | | ; CList == [] -> R=X % Concealement law L1 |
1457 | | ; try_tl_normalise(X,NX),R=ehide(NX,CList,Span)). |
1458 | | tl_normalise(eprocRenaming(RL,X,Span),R) :- !, |
1459 | | (is_stop(X,S) -> R=stop(S) |
1460 | | ; is_skip(X,S) -> R=skip(S) |
1461 | | ; try_tl_normalise(X,NX),R=eprocRenaming(RL,NX,Span)). |
1462 | | tl_normalise(';'(X,Y,SPAN),R) :- !, |
1463 | | (is_skip(X) -> R=Y /* Law on page 140 of Roscoe */ |
1464 | | ; is_stop(X,S) -> R=stop(S) |
1465 | | ; is_skip(Y) -> R=X |
1466 | | ; R = ';'(X,Y,SPAN) ). |
1467 | | tl_normalise('/\\'(X,Y,Span),R) :- !, |
1468 | | (is_stop(X,_) -> R=Y ; (is_stop(Y,_) -> R=X ; R='/\\'(X,Y,Span))). |
1469 | | tl_normalise(ifte(A,B,C,_,_,_),R) :- !, % print(norm_ifte(A)),nl, |
1470 | | evaluate_boolean_expression(A,ARes), |
1471 | | % print(res(ARes)),nl, |
1472 | | tl_normalise_ifte(ARes,B,C,R). |
1473 | | |
1474 | | is_stop(X,S) :- nonvar(X),X=stop(S). |
1475 | | |
1476 | | :- block tl_normalise_ifte(-,?,?,?). |
1477 | | tl_normalise_ifte(true,B,_C,R) :- !,full_normalise_csp_process(B,R). |
1478 | ? | tl_normalise_ifte(false,_,C,R) :- !, full_normalise_csp_process(C,R). |
1479 | | % evaluate_boolean_expression/2 will always throw an exception if A is not a boolean test |
1480 | | % probably this case will never occur |
1481 | | % tl_normalise_ifte(A,B,C,_R) :- add_error(tl_normalise,'Not a boolean test: ',A:B:C). |
1482 | | |
1483 | | try_tl_normalise(A,R) :- (tl_normalise(A,B) -> R=B ; R=A). |
1484 | | |
1485 | | is_skip(X) :- nonvar(X), X=skip(_). |
1486 | | is_skip(X,Y) :- nonvar(X), X=skip(Y). |
1487 | | % TO DO: add rules esharing(_,stop(S),stop(_),_) -> stop(S), |
1488 | | |
1489 | | % P [] STOP = P |
1490 | | :- assert_must_succeed(( |
1491 | | P='[]'(skip(_),stop(span1),span2), |
1492 | | haskell_csp: full_normalise_csp_process(P,NormP), |
1493 | | NormP=skip(_))). |
1494 | | % P [] P = P |
1495 | | :- assert_must_succeed(( |
1496 | | P='[]'(skip(span1),skip(span1),span3), |
1497 | | haskell_csp: full_normalise_csp_process(P,NormP), |
1498 | | NormP=skip(span1))). |
1499 | | % P ||| STOP = STOP |
1500 | | :- assert_must_succeed(( |
1501 | | P='|||'(skip(_),stop(span1),span2), |
1502 | | haskell_csp: full_normalise_csp_process(P,NormP), |
1503 | | NormP=stop(span1))). |
1504 | | % SKIP; (P [] STOP) = P |
1505 | | :- assert_must_succeed(( |
1506 | | P=';'(skip(_),'[]'(skip(span1),stop(span3),span4),span2), |
1507 | | haskell_csp: full_normalise_csp_process(P,NormP), |
1508 | | NormP='[]'(skip(span1),stop(span3),span4))). |
1509 | | % P; SKIP = P |
1510 | | :- assert_must_succeed(( |
1511 | | P=';'(stop(_),skip(span1),span2), |
1512 | | haskell_csp: full_normalise_csp_process(P,NormP), |
1513 | | NormP=stop(_))). |
1514 | | |
1515 | | /* ------------------------------------- */ |
1516 | | %full_normalise_csp_process(P,_) :- print(full_normalise_csp_process(P)),nl,fail. |
1517 | | /* TO DO: add other procRep,... intermediate operators */ |
1518 | ? | full_normalise_csp_process(P,NormP) :- full_normalise_csp_process(P,NormP,outer). |
1519 | | :- block full_normalise_csp_process(-,?,?). |
1520 | | full_normalise_csp_process('|||'(X,Y,Span),Res,_) :- !, |
1521 | | %full_normalise_csp_process(X,NX,inner), full_normalise_csp_process(Y,NY,inner), |
1522 | ? | full_normalise_csp_process(X,NX,outer), full_normalise_csp_process(Y,NY,outer), |
1523 | | tl_normalise('|||'(NX,NY,Span),Res). |
1524 | | % both clausels below will be probably never executed. procRenamingComp/3 and procRepAParallel/3 as |
1525 | | % replicated process expressions will be translated to agent_calls in the compiling/analyzing stage |
1526 | | % of loading the respective CSP model. DEAD CODE: |
1527 | | /*full_normalise_csp_process(procRenamingComp(X,GeneratorList,RenameList),Res,_) :- !, |
1528 | | %print(normalise_procCompRenaming(GeneratorList)),nl, |
1529 | | replicate_expand_set_comprehension(RenameList,GeneratorList,setValue(ExpandedRenames)), |
1530 | | %print(exp(ExpandedRenames)),nl, |
1531 | | Res = procRenaming(ExpandedRenames,X,no_loc_info_available). |
1532 | | full_normalise_csp_process(procRepAParallel(GeneratorList,pair(SyncSet,Body),Span), Res,_) :- !, |
1533 | | %print(procRepAParallel(GeneratorList,SyncSet)),nl, |
1534 | | extract_variables_from_generator_list(GeneratorList,Variables), |
1535 | | replicate_expand_set_comprehension([list([SyncSet,Body,Variables])],GeneratorList,setValue(Bodies)), |
1536 | | %print(bodies(Bodies)),nl, |
1537 | | convert_into_eaParallel(Bodies,Span,APAR,_ALPH), %print(apar(APAR,_ALPH)),nl, |
1538 | | full_normalise_csp_process(APAR,Res,inner). */ |
1539 | | full_normalise_csp_process(repInterleave(GeneratorList,Body,Span),Res,_) :- !, |
1540 | | extract_variables_from_generator_list(GeneratorList,Variables), |
1541 | | replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)), |
1542 | | convert_into_interleave(Bodies,Span,Res). |
1543 | | full_normalise_csp_process(sharing(CList,X,Y,SrcSpan),Res,_) :- !, |
1544 | | evaluate_argument(CList,EvCList), |
1545 | | expand_channel_pattern_expression(EvCList,ECList,SrcSpan), |
1546 | ? | full_normalise_csp_process(X,NX,outer), |
1547 | ? | full_normalise_csp_process(Y,NY,outer), |
1548 | | Res = esharing(ECList,NX,NY,SrcSpan). |
1549 | | full_normalise_csp_process(aParallel(CListX,X,CListY,Y,SrcSpan),Res,_) :- !, |
1550 | ? | evaluate_argument(CListX,EvCListX), |
1551 | | expand_channel_pattern_expression(EvCListX,ECListX,SrcSpan), |
1552 | ? | evaluate_argument(CListY,EvCListY), |
1553 | | expand_channel_pattern_expression(EvCListY,ECListY,SrcSpan), |
1554 | ? | full_normalise_csp_process(X,NX,outer), |
1555 | ? | full_normalise_csp_process(Y,NY,outer), |
1556 | | %print(eaParallel(ECListX,NX,ECListY,NY,SrcSpan)),nl, |
1557 | | Res = eaParallel(ECListX,NX,ECListY,NY,SrcSpan). |
1558 | | /* Unfold if Par ground and unfolded value ground ?? */ |
1559 | | full_normalise_csp_process(agent_call(Span,F,Par),Res,outer) :- % only allow outer agent_calls to be unfolded to avoid infinite expansion for e.g. P(1) = P(1) ||| P(1) |
1560 | | preference(cspm_detailed_animation,false), |
1561 | | %% fail, %% fail: agent_calls are not expanded here, which means better source location feedback in animator |
1562 | | %% WE COULD MAKE THIS AN OPTION IN THE PREFERENCES; I am not sure what the performance impact is |
1563 | | %% for scheduler this leads to a substantial increase in the number of states |
1564 | | !, |
1565 | ? | ((ground(Par),unfold_function_call_once(F,Par,Value,Span), |
1566 | | (ground(Value) ; |
1567 | | agent_can_be_unfolded(Value) |
1568 | | ) |
1569 | | ) |
1570 | ? | -> full_normalise_csp_process(Value,Res,outer) |
1571 | | ; Res = agent_call(Span,F,Par) |
1572 | | ). |
1573 | | full_normalise_csp_process(val_of(RenamedX,Span),NormState,_) :- !, |
1574 | | (symbol(RenamedX,_X,_,_) -> |
1575 | ? | full_normalise_csp_process(agent_call(Span,RenamedX,[]),NormState,_) |
1576 | | ; |
1577 | | % does this occur in some case (see coverage info) |
1578 | | full_normalise_csp_process(RenamedX,NormState,_) |
1579 | | ). |
1580 | | full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_) :- |
1581 | | ground(Test),!, |
1582 | | evaluate_boolean_expression(Test,Res), |
1583 | | (Res == true -> |
1584 | ? | full_normalise_csp_process(Then,R) |
1585 | | ; Res == false -> |
1586 | ? | full_normalise_csp_process(Else,R) |
1587 | | ; |
1588 | | add_internal_error('Internal Error: Not a boolean value inside if-then-else: ', |
1589 | | full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_)),fail |
1590 | | ). |
1591 | | full_normalise_csp_process(ifte(Test,Then,Else,S1,S2,S3),R,_) :- !, |
1592 | | R = ifte(Test,Then,Else,S1,S2,S3). % test could be false or true; top-level test could be evaluated ?! |
1593 | | full_normalise_csp_process('&'(Test,Then),R,_) :- !, R = '&'(Test,Then). % test could be false; don't unfold agent_calls inside Then |
1594 | | full_normalise_csp_process(';'(P,Q,SPAN),R,Scope) :- !, |
1595 | ? | full_normalise_csp_process(P,NP,Scope), |
1596 | | tl_normalise(';'(NP,Q,SPAN),R). |
1597 | | full_normalise_csp_process(prefix(SPAN,Values,ChannelExpr,CSP,SPAN2),R,_) :- !, |
1598 | | (empty_inGuard_set(Values) -> |
1599 | | R=stop(SPAN) % (STOP-step) ?x:{} -> P = STOP (law 1.15) |
1600 | | ; |
1601 | | R = prefix(SPAN,Values,ChannelExpr,CSP,SPAN2) |
1602 | | ). |
1603 | | full_normalise_csp_process(head(List),R,_) :- !, R=head(List). % should we evaluate ?? |
1604 | | full_normalise_csp_process(agent_call(Span,A,Par),R,_) :- !, R=agent_call(Span,A,Par). |
1605 | | % DEAD CODE!!! agent_call_curry/2 will be translated into nested agent_call in the precompiling phase. |
1606 | | %full_normalise_csp_process(agent_call_curry(A,Par),R,_) :- !, print(agent_call_curry(A,Par)),nl,R=agent_call_curry(A,Par). |
1607 | | full_normalise_csp_process(ehide(X,CList,Span),R,_) :- !, |
1608 | ? | full_normalise_csp_process(X,NX,inner), |
1609 | | tl_normalise(ehide(NX,CList,Span),R). |
1610 | | full_normalise_csp_process(eprocRenaming(RL,X,Span),R,_) :- !, |
1611 | ? | full_normalise_csp_process(X,NX,inner), |
1612 | | tl_normalise(eprocRenaming(RL,NX,Span),R). |
1613 | | full_normalise_csp_process(Proc,Res,_) :- |
1614 | | binary_top_level_process_operator_possible_to_be_normalised(Proc,F,X,Y,Span),!, |
1615 | ? | full_normalise_csp_process(X,NX,inner), |
1616 | ? | full_normalise_csp_process(Y,NY,inner), |
1617 | | functor(NTerm,F,3),arg(1,NTerm,NX),arg(2,NTerm,NY),arg(3,NTerm,Span), |
1618 | | tl_normalise(NTerm,Res). |
1619 | ? | full_normalise_csp_process(Proc,Res,_) :- definite_cspm_process_construct(Proc,Spans,Rest,RecCSP), !, |
1620 | | functor(Proc,F,N), functor(Res,F,N), |
1621 | ? | maplist(full_normalise_csp_process_inner(inner),RecCSP,NormRecCSP), |
1622 | ? | definite_cspm_process_construct(Res,Spans,Rest,NormRecCSP). |
1623 | | full_normalise_csp_process(P,R,_) :- !, |
1624 | | add_warning(full_normalise_csp_process,'Could not normalise: ',P),R=P. |
1625 | | |
1626 | | full_normalise_csp_process_inner(ProcLabel,Proc,NProc) :- |
1627 | ? | full_normalise_csp_process(Proc,NProc,ProcLabel). |
1628 | | |
1629 | | binary_top_level_process_operator_possible_to_be_normalised(ProcessTerm,F,X,Y,Span) :- |
1630 | | functor(ProcessTerm,F,3), |
1631 | | memberchk(F,['|||','[]','/\\']), |
1632 | | arg(1,ProcessTerm,X),arg(2,ProcessTerm,Y),arg(3,ProcessTerm,Span). |
1633 | | |
1634 | | empty_inGuard_set(Values) :- |
1635 | | member(inGuard(_X,Set),Values), |
1636 | | is_empty_set(Set,true),!. |
1637 | | |
1638 | | normalise_cspm_state(State,NormState) :- |
1639 | ? | full_normalise_csp_process(State,NormState). |
1640 | | |
1641 | | %% Probably DEAD CODE !!! (wait for the next coverage release to prove this assumption) |
1642 | | :- assert_must_succeed((agent_can_be_unfolded(X), X=procRenamingComp(_,_,_))). |
1643 | | :- assert_must_succeed((agent_can_be_unfolded(X), X=aParallel(_,_,_,_,_))). |
1644 | | agent_can_be_unfolded(procRenamingComp(_,_,_)). |
1645 | | agent_can_be_unfolded(aParallel(_,_,_,_,_)). |
1646 | | agent_can_be_unfolded(repInterleave(_,_,_)). |
1647 | | |
1648 | | /* ------------------------------------- */ |
1649 | | |
1650 | | |
1651 | | /* EVALUATING Agent Call arguments */ |
1652 | | |
1653 | | evaluate_agent_call_parameters(AgentName,Par,_,_) :- var(AgentName),!, |
1654 | | add_internal_error('Internal Error: Trying to call VARIABLE function: ',evaluate_agent_call_parameters(AgentName,Par,_,_)),fail. |
1655 | | evaluate_agent_call_parameters(AgentName,Par,_,_) :- var(Par),!, |
1656 | | add_internal_error('Internal Error: Trying to call VARIABLE parameters: ',evaluate_agent_call_parameters(AgentName,Par,_,_)),fail. |
1657 | | %evaluate_agent_call_parameters(agent_call(AName,[]),Par,EAgentCall) :- atomic(AName),!, |
1658 | | % /* then AName must represent a lambda function which has been compiled ?!!? */ |
1659 | | % l_evaluate_arguments(Par,EPar), |
1660 | | % EAgentCall =.. [AName|EPar]. |
1661 | | evaluate_agent_call_parameters(_Call,Par,EPar,_) :- Par==[],!, EPar=[]. % nothing to evaluate |
1662 | | evaluate_agent_call_parameters(AgentNameExpr,Par,_EAgentCall,Span) :- \+ atomic(AgentNameExpr),!, |
1663 | | add_error(haskell_csp,'Trying to call non-atomic function: ',agent_call(AgentNameExpr,Par),Span),fail. |
1664 | | evaluate_agent_call_parameters(AName,Par,EPar,Span) :- |
1665 | | length(Par,Arity), |
1666 | | (agent_parameters(AName,Arity,LazyStrictList) |
1667 | | -> true |
1668 | | ; add_error(evaluate_agent_call_parameters,'Unknown function call: ',(AName/Arity),Span) |
1669 | | ), |
1670 | ? | l_evaluate_arguments(Par,LazyStrictList,EPar). |
1671 | | % EAgentCall =.. [AName|EPar]. |
1672 | | |
1673 | | |
1674 | | l_evaluate_arguments([],[],[]). |
1675 | | l_evaluate_arguments([A|T],[Lazy|TL],[EA|ET]) :- |
1676 | | %% print(eval_arg(A,Lazy)),nl, %% |
1677 | ? | (Lazy=lazy -> evaluate_argument(A,EA) |
1678 | ? | ; force_evaluate_argument(A,EA) |
1679 | | ), |
1680 | | %% print(arg_res(A,EA)),nl, %% |
1681 | ? | l_evaluate_arguments(T,TL,ET). |
1682 | | |
1683 | | |
1684 | | evaluate_lambda_arguments([],[],[]). |
1685 | | evaluate_lambda_arguments([A|T],[FormalPar|FT],[EA|ET]) :- |
1686 | | %% print(eval_arg(A,Lazy)),nl, |
1687 | | (var(FormalPar) -> A=EA % will be copied into lambda body and evaluated then evaluate_argument(A,EA) |
1688 | | ; force_evaluate_argument(A,EA) % it is a pattern; we need to evaluate argument |
1689 | | ), |
1690 | | %% print(arg_res(A,EA)),nl, |
1691 | | evaluate_lambda_arguments(T,FT,ET). |
1692 | | /* ------------------------------------- */ |
1693 | | |
1694 | | /* EVALUATING Channel arguments */ |
1695 | | |
1696 | | setup_skel(_,in(_)). |
1697 | | |
1698 | | setup_channel_skeleton(io(V,Ch,_)) :- |
1699 | ? | channel_type_list(Ch,ChannelTypes), |
1700 | | maplist(setup_skel,ChannelTypes,V). |
1701 | | |
1702 | | /* ------------------------------------- */ |
1703 | | |
1704 | | /* enumerate_action(A) : if part of the inputs of A are not determined: enumerate |
1705 | | possible values */ |
1706 | | |
1707 | | cspm_trans_enum(E,A,E2) :- |
1708 | | init_wait_flags(WF), |
1709 | ? | cspm_trans(E,A,E2,WF), |
1710 | | % tools:print_bt_message(grounding_waitflags(A)), %% |
1711 | ? | ground_wait_flags(WF), |
1712 | | % TO DO: we could also add enumerate_action to the WF store: in principle sets inGuards should be smaller |
1713 | | % tools:print_bt_message(enumerate_action(E,A)), %% |
1714 | ? | enumerate_action(A) |
1715 | | % ,tools:print_bt_message(finished_enumerate_action(A)),nl %% |
1716 | | . |
1717 | | |
1718 | | |
1719 | | /* TO DO: add enumeration to hide + removed values by rename; use tau(V,Ch) ?? */ |
1720 | | |
1721 | | enumerate_action(X) :- X \= tick(_), X\=tau(_), X\= io(_,_,_), !, |
1722 | | add_internal_error('Internal error: Unknown CSP event: ', enumerate_action(X)). |
1723 | | enumerate_action(tick(_)). |
1724 | ? | enumerate_action(tau(X)) :- (nonvar(X) -> enumerate_tau_argument(X) ; true). |
1725 | | enumerate_action(io(Vals,Channel,Span)) :- |
1726 | | if((channel_type_list(Channel,ChannelTypes)), |
1727 | ? | (enume_ch_vals(ChannelTypes,Vals,Channel,Span,io(Vals,Channel,Span))), |
1728 | | add_error(enumerate_action,'Channel not declared: ',Channel,Span)). |
1729 | | |
1730 | | enumerate_tau_argument(io(V,C,S)) :- !,enumerate_action(io(V,C,S)). |
1731 | ? | enumerate_tau_argument(hide(X)) :- !,enumerate_action(X). |
1732 | | enumerate_tau_argument(link(_AX,AY)) :- !,enumerate_action(AY). |
1733 | | enumerate_tau_argument(_). |
1734 | | |
1735 | | :- use_module(probsrc(translate),[translate_event/2]). |
1736 | | %% enume_ch_vals(T,V,C,_Span,FullEvent) :- print(enume_ch_vals(T,V,C)),nl,fail. %% |
1737 | | enume_ch_vals([],[],_,_Span,_) :- !. |
1738 | | enume_ch_vals([],Vals,_Channel,Span,FullEvent) :- !, |
1739 | | (Vals = [in(V)] |
1740 | | -> empty_tuple(V) /* the empty dotTuple */ |
1741 | | ; translate_event(FullEvent,ES), |
1742 | | add_error(enumerate_action,'Too many output values on channel: ',ES:Vals, Span) |
1743 | | ). |
1744 | | enume_ch_vals([Type|RestTypes],Vals,Channel,Span,FullEvent) :- % T \= [], |
1745 | ? | enume_ch_vals2(Vals,Type,RestTypes,Channel,Span,FullEvent). |
1746 | | |
1747 | | enume_ch_vals2(X,Type,_RestTypes,_Channel,Span,FullEvent) :- % print(ecv2(X,Type,RestTypes,Channel)),nl, |
1748 | | var(X),!, |
1749 | | translate_event(FullEvent,ES), |
1750 | | add_error(haskell_csp,'Variable value list on channel: ',ES:X:Type,Span),fail. |
1751 | | enume_ch_vals2([],Type,RestTypes,_Channel,Span,FullEvent) :- !, |
1752 | | translate_event(FullEvent,ES), |
1753 | | add_error(enumerate_action,'Too few output values on channel: ',ES:[Type:RestTypes], Span). |
1754 | | enume_ch_vals2([in(V)|TAIL],Type,RestTypes,Channel,Span,FullEvent) :- nonvar(V), |
1755 | | V=tuple(X),nonvar(X),X=[H|T], \+ csp_constructor(H,_,_), |
1756 | | !, % sometimes an in contains dot tuples; test above not very elegant; can we simplify this ?? |
1757 | | (T==[] -> |
1758 | | enume_ch_vals2([in(H)|TAIL],Type,RestTypes,Channel,Span,FullEvent) |
1759 | | ; enume_ch_vals2([in(H),in(tuple(T))|TAIL],Type,RestTypes,Channel,Span,FullEvent)). |
1760 | | enume_ch_vals2([in(V)|TAIL],Type,RestTypes,Channel,Span,_FullEvent) :- |
1761 | | TAIL==[],!, /* only treat it as a tail_in(X) if it is definitely at the end of the list |
1762 | | see example LetTestChannel -> TEST(2) process for complication if we do |
1763 | | not check that TAIL==[] */ |
1764 | | (RestTypes=[] |
1765 | ? | -> enumerate_channel_input_value(Type,V,Channel,Span) |
1766 | ? | ; enumerate_channel_input_value('dotTupleType'([Type|RestTypes]),V,Channel,Span) |
1767 | | ). |
1768 | | enume_ch_vals2([IODVal|TV],Type,RestTypes,Channel,Span,FullEvent) :- !, |
1769 | ? | enumerate_channel_value_type(IODVal,Type,Channel,Span), |
1770 | ? | enume_ch_vals(RestTypes,TV,Channel,Span,FullEvent). |
1771 | | |
1772 | | |
1773 | | enumerate_channel_value_type(IOD,Type,Channel,Span) :- |
1774 | | %print(enumerate_channel_value_type(IOD,Type,Channel,Span)),nl, |
1775 | | (IOD=in(HX) %; IOD=dot(HX)) |
1776 | ? | -> enumerate_channel_input_value(Type,HX,Channel,Span) |
1777 | | ; (ground(IOD) |
1778 | | -> check_channel_input_output_value(IOD,Type,Channel,Span,'Type error in channel input: ') |
1779 | ? | ; enumerate_channel_input_value(Type,IOD,Channel,Span) |
1780 | | ) |
1781 | | ). |
1782 | | |
1783 | | check_channel_input_output_value(X,Type,Ch,Span,ErrMsg) :- |
1784 | | when(ground(X), ((peel_in(X,PX),is_member_set_alsoPat(PX,Type)) -> true |
1785 | | ; add_error(check_channel_output_value,ErrMsg,(Ch:(val(X):type(Type))),Span))). |
1786 | | |
1787 | | /* peel input values which may lurk inside datavalues, especially records */ |
1788 | | peel_in(in(X),R) :- !, R=X. |
1789 | | peel_in(record(F,L),R) :- !, |
1790 | | R=record(F,PL), |
1791 | | maplist(peel_in,L,PL). |
1792 | | peel_in(X,X). |
1793 | | |
1794 | | :- assert_must_succeed(( haskell_csp:enumerate_channel_input_value(setFromTo(1,3),R,c,unknown), |
1795 | | R==int(2) )). |
1796 | | |
1797 | | enumerate_channel_input_value(Type,Val,Ch,Span) :- |
1798 | | MAXRECURSIONDEPTH = 2, |
1799 | ? | enumerate_channel_input_value(Type,Val,Ch,MAXRECURSIONDEPTH,Span). |
1800 | | |
1801 | | |
1802 | | enumerate_channel_input_value(Type,Val,Ch,MaxRec,Span) :- |
1803 | | (ground(Val) |
1804 | | -> check_channel_input_output_value(Val,Type,Ch,Span,'Type error in channel output: ') |
1805 | ? | ; enumerate_channel_input_value1(Type,Val,Ch,MaxRec,Span) |
1806 | | ). |
1807 | | |
1808 | | enumerate_channel_input_value1(Type,Val,Ch,MaxRec,Span) :- |
1809 | | ((nonvar(Val),Val=in(VX)) /* can happen when question marks occur inside records, ... */ |
1810 | ? | -> enumerate_channel_input_value1_1(Type,VX,Ch,MaxRec,Span) |
1811 | ? | ; enumerate_channel_input_value1_1(Type,Val,Ch,MaxRec,Span) |
1812 | | ). |
1813 | | |
1814 | | enumerate_channel_input_value1_1(Type,Val,Ch,MaxRec,Span) :- |
1815 | | ( (nonvar(Val),Val=alsoPat(X,Y)) -> |
1816 | ? | enumerate_channel_input_value2(Type,X,Ch,MaxRec,Span), |
1817 | | %enumerate_channel_input_value2(Type,Y,Ch,MaxRec,Span), |
1818 | | unify_also_patterns(X,Y,_R) |
1819 | | ; (nonvar(Val),Val=appendPat(X,FunHead)) -> |
1820 | | agent_compiled(FunHead,_Value,_SRCSPAN), |
1821 | ? | enumerate_channel_input_value2(Type,X,Ch,MaxRec,Span) |
1822 | ? | ; enumerate_channel_input_value2(Type,Val,Ch,MaxRec,Span) |
1823 | | ). |
1824 | | |
1825 | | :- dynamic ignore_infinite_datatypes/0. % set from refinement_checker; very HACKY |
1826 | | |
1827 | | %enumerate_channel_input_value2(T,V,Ch,_MaxRec) :- print(enumerate_channel_input_value(T,V,Ch)),nl,fail. |
1828 | | :- assert_must_succeed((findall(Res, enumerate_channel_input_value2('Set'(setValue([int(1),int(2)])),Res,_Ch,_MaxRec,_Span),L), |
1829 | | L == [setValue([int(1),int(2)]),setValue([int(1)]),setValue([int(2)]),setValue([])])). |
1830 | | |
1831 | | enumerate_channel_input_value2(intType,X,Ch,_MaxRec,_Span) :- !, |
1832 | ? | enumerate_basic_type(X,integer,trigger_true(Ch)). % NOTE : this uses MAXINT preference value! |
1833 | | enumerate_channel_input_value2(boolType,X,_Ch,_MaxRec,_Span) :- !,(X=true ; X=false). |
1834 | | enumerate_channel_input_value2(setFromTo(Low,Up),Res,Ch,_MaxRec,Span) :- !, |
1835 | | set_enumeration_result(Res,int(X),Ch,setFromTo(Low,Up),Span), |
1836 | ? | enumerate_csp_int(X,Low,Up). |
1837 | | /*(preference(use_clpfd_solver,true),clpfd_interface: fd_var(Res) -> |
1838 | | clpfd_interface: csp_clpfd_labeling([ffc,enum],[Res]) |
1839 | | ; set_enumeration_result(Res,int(X),Ch,setFromTo(Low,Up),Span), |
1840 | | enumerate_csp_int(X,Low,Up) |
1841 | | ).*/ |
1842 | | enumerate_channel_input_value2(setFrom(Low),V,Ch,_MaxRec,Span) :- !, |
1843 | | add_symbol_span(Ch,Span,CSpan), |
1844 | | add_error(enumerate_channel_input_value,'Cannot enumerate infinite Type: ',(Ch,(setFrom(Low),V)),CSpan). |
1845 | | enumerate_channel_input_value2('Set'(X),Res,_Ch,_MaxRec,_Span) :- !, /* Probably DEAD CODE */ |
1846 | | enum_subset(X,Res). |
1847 | | enumerate_channel_input_value2('dotTupleType'(List),Res,Ch,MaxRec,Span) :- !, |
1848 | | set_enumeration_tuple_result(Res,RR,Ch,'dotTupleType'(List),Span), |
1849 | ? | l_enumerate_channel_input_value2(List,RR,Ch,dot_tuple,MaxRec,Span). |
1850 | | enumerate_channel_input_value2('typeTuple'(List),Res,Ch,MaxRec,Span) :- !, |
1851 | | set_enumeration_result(Res,na_tuple(RR),Ch,'typeTuple'(List),Span), |
1852 | | % print(enum_tuple('typeTuple'(List),Res,Ch)),nl, |
1853 | ? | l_enumerate_channel_input_value2(List,RR,Ch,type_tuple,MaxRec,Span). |
1854 | ? | enumerate_channel_input_value2(setValue(L),R,_Ch,_MaxRec,_Span) :- !,member(R,L). /* R should be list skeleton at least */ |
1855 | ? | enumerate_channel_input_value2(dataType(DT),C,Channel,MaxRec,Span) :- is_a_datatype(DT,_), !, |
1856 | ? | enumerate_datatype_el(DT,C,Channel,MaxRec,Span). |
1857 | | % TO DO: add all other types supported by is_member_set |
1858 | | enumerate_channel_input_value2('Seq'(setValue([])),V,_Ch,_MaxRec,_Span) :- !, V= list([]). |
1859 | | enumerate_channel_input_value2('Seq'(Type),V,Ch,_MaxRec,Span) :- !, |
1860 | | (ignore_infinite_datatypes -> V=sequence % needed for the Trace Debugger in Tcl/Tk |
1861 | | ; add_symbol_span(Ch,Span,CSpan), |
1862 | | add_error(enumerate_channel_input_value,'Cannot enumerate infinite Seq Type: ',(Ch,('Seq'(Type),V)),CSpan)). |
1863 | | enumerate_channel_input_value2(agent_call(_Src, Name,Patterns),Val,Ch,_MaxRec,Span) :- !, |
1864 | | unfold_function_call_once(Name,Patterns,Res,Span), |
1865 | | evaluate_argument(Res,Res1), |
1866 | | enumerate_channel_input_value(Res1,Val,Ch,Span). |
1867 | | enumerate_channel_input_value2(Type,V,Ch,_MaxRec,Span) :- |
1868 | | add_symbol_span(Ch,Span,CSpan), |
1869 | | add_error(enumerate_channel_input_value,'Illegal type for channel: ',(Ch,(Type,V)),CSpan). |
1870 | | |
1871 | | :- dynamic enum_warning_occured/3. |
1872 | | :- use_module(probsrc(tools_strings),[ajoin/2]). |
1873 | | |
1874 | | enumerate_datatype_el(DT,C,Channel,_MaxRec,Span) :- |
1875 | ? | if(csp_constant(C,DT),true, |
1876 | | (nonvar(C),C \= record(_,_), |
1877 | | add_error(enumerate_datatype_el,'Type error for channel input variable: ', Channel:(C,type(DT)),Span), |
1878 | | fail)). |
1879 | | enumerate_datatype_el(DT,C,Channel,MaxRec,Span) :- |
1880 | | ((MaxRec>0 ; nonvar(C)) |
1881 | | ->((nonvar(C) -> M1 = MaxRec ; M1 is MaxRec-1), |
1882 | | C=record(Cons,Fields), |
1883 | ? | csp_constructor(Cons,DT,ArgSubTypes), |
1884 | | % print(recurse_enum_rec(Cons,DT,ArgSubTypes,Fields)),nl, |
1885 | ? | l_enumerate_channel_input_value2(ArgSubTypes,Fields,Channel,dot_tuple,M1,Span)) |
1886 | | ; enum_warning_occured(DT,Channel,Span) -> fail |
1887 | | ; ajoin(['Maximum recursion depth reached on channel "',Channel, |
1888 | | '" for enumeration of datatype : '],Msg), |
1889 | | add_message(csp,Msg,DT,Span), |
1890 | | assertz(enum_warning_occured(DT,Channel,Span)), |
1891 | | % THIS used to return a variable when ignore_infinite_datatypes true, but causes problems for test 2349 |
1892 | | fail |
1893 | | ). |
1894 | | |
1895 | | % ensure that ResVar is a tuple and flatten the tuple |
1896 | | set_enumeration_tuple_result(ResVar,ResultTerm,Channel,ExpectedType,Span) :- |
1897 | | ((tuple(TL)=ResVar;dotTuple(TL)=ResVar) -> |
1898 | | %print(flattening(ResVar)),nl, |
1899 | | flatten_tuple_value(TL,ResultTerm) /* ok, no type error */ |
1900 | | ; add_symbol_span(Channel,Span,CSpan), |
1901 | | add_error(set_enumeration_tuple_result,'Type error for instantiated channel input variable: ',Channel:(ResVar,type(ExpectedType)),CSpan), |
1902 | | fail). |
1903 | | |
1904 | | %%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR flatten_tuple_value/2, flatten_inner_tuple_value/2 and flatten2/3 %%%%%%%%%%%%%%%%%%%%%%%%%% |
1905 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value(X,R), R == X)). |
1906 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([],R), R == [])). |
1907 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),int(2)])],R), R == [X,int(1),int(2)])). |
1908 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([tuple([]),tuple([int(1),int(2)]),X,Y,tuple([int(10)])],R), R == [int(1),int(2),X,Y,int(10)])). |
1909 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),Y,int(2),Z])],R), R == [X,int(1),Y,int(2),Z])). |
1910 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([X,tuple([int(1),Y,int(2),Z]),int(3)],R), R == [X,int(1),Y,int(2),Z,int(3)])). |
1911 | | :- assert_must_succeed((haskell_csp: flatten_tuple_value([],[]))). |
1912 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1913 | | |
1914 | | flatten_tuple_value(X,R) :- var(X),!, R=X. % this can happen if we have a single in(X) representing ch?x |
1915 | | flatten_tuple_value([],[]). |
1916 | | flatten_tuple_value([H|T],R) :- flatten2(H,T,R). |
1917 | | |
1918 | | flatten_inner_tuple_value(X,R) :- var(X),!, print(variable_inner_tuple(X)),nl, R=[X]. |
1919 | | flatten_inner_tuple_value([],[]). |
1920 | | flatten_inner_tuple_value([H|T],R) :- flatten2(H,T,R). |
1921 | | |
1922 | | flatten2(VAR,T,Res) :- var(VAR),!, Res=[VAR|TR],flatten_inner_tuple_value(T,TR). |
1923 | | flatten2(tuple(LH),T,R) :- !, flatten_inner_tuple_value(LH,FLH), |
1924 | | append(FLH,TR,R), flatten_inner_tuple_value(T,TR). |
1925 | | flatten2(H,T,[H|TR]) :- flatten_inner_tuple_value(T,TR). |
1926 | | |
1927 | | set_enumeration_result(ResVar,ResultTerm,Channel,ExpectedType,Span) :- |
1928 | | (ResVar=ResultTerm -> true /* ok, no type error */ |
1929 | | ; |
1930 | | add_symbol_span(Channel,Span,CSpan), |
1931 | | add_error(set_enumeration_result,'Type error for instantiated channel input variable: ',Channel:(val(ResVar),type(ExpectedType)),CSpan), |
1932 | | fail). |
1933 | | |
1934 | | l_enumerate_channel_input_value2([],R,Ch,_SType,_MaxRec,Span) :- !, |
1935 | | (var(R) -> R=[] |
1936 | | ; R=[] -> true |
1937 | | ; add_error(l_enumerate_channel_input_value,'Too many arguments on channel: ',(Ch,R),Span),fail). |
1938 | | l_enumerate_channel_input_value2([HType|T],[HVal|TV],Ch,SType,MaxRec,Span) :- !, |
1939 | | ((TV==[],SType=dot_tuple) -> % enume the rest of the channel types to HVal (only for dotTuple types) |
1940 | ? | enume_ch_vals([HType|T],[in(HVal)],Ch,Span,io([],Ch)) % TO DO: full event |
1941 | | ; |
1942 | ? | enumerate_channel_input_value(HType,HVal,Ch,MaxRec,Span), %% <-- add Span |
1943 | ? | l_enumerate_channel_input_value2(T,TV,Ch,SType,MaxRec,Span) |
1944 | | ). |
1945 | | l_enumerate_channel_input_value2([HType|T],[],Ch,_SType,_MaxRec,Span) :- !, |
1946 | | add_error(l_enumerate_channel_input_value,'Not enough arguments on channel: ',(Ch,[HType|T]),Span),fail. |
1947 | | l_enumerate_channel_input_value2(X,Y,Ch,SType,MR,Span) :- |
1948 | | add_internal_error('Illegal arguments: ',l_enumerate_channel_input_value2(X,Y,Ch,SType,MR,Span)),fail. |
1949 | | |
1950 | | get_symbol_span(S,SPAN) :- atomic(S),symbol(S,_,SPAN,_),!. |
1951 | | get_symbol_span(S,SPAN) :- nonvar(S),functor(S,FS,_),symbol(FS,_,SPAN,_),!. |
1952 | | get_symbol_span(_S,no_loc_info_available). |
1953 | | |
1954 | | |
1955 | | add_symbol_error(Src,Msg,Term,Ch) :- |
1956 | | get_symbol_span(Ch,Span), |
1957 | | add_error(Src,Msg,Term,Span). |
1958 | | |
1959 | | add_symbol_span(Ch,Span,OutSpan) :- get_symbol_span(Ch,SSpan), |
1960 | | SSpan \= no_loc_info_available, |
1961 | | !, |
1962 | | unify_spans(Span,SSpan,OutSpan). |
1963 | | add_symbol_span(_,S,S). |
1964 | | |
1965 | | % just like above, but can also be called with ordinary spans |
1966 | | add_error_with_span(Src,Msg,Term,Span) :- |
1967 | | (Span=symbol(S) -> get_symbol_span(S,Span2) ; Span2=Span), |
1968 | | add_error(Src,Msg,Term,Span2). |
1969 | | |
1970 | | add_internal_error_with_span(Src,Msg,Term,Span) :- |
1971 | | (Span=symbol(S) -> get_symbol_span(S,Span2) ; Span2 = Span), |
1972 | | add_internal_error(Src,Msg,Term,Span2). |
1973 | | |
1974 | | /* ------------------------------------- */ |
1975 | | /* BOOLEAN EXPRESSIONS */ |
1976 | | /* ------------------------------------- */ |
1977 | | |
1978 | | %%%%%%%% UNIT TESTS FOR TESTING check_boolean_expressions/1,cond_check_boolean_expression/2,ifte_check_boolean_expression/3 %%%%%%% |
1979 | | |
1980 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(true))). |
1981 | | :- assert_must_fail((haskell_csp: check_boolean_expression(X), X = false)). |
1982 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(bool_not(false)))). |
1983 | | :- assert_must_fail((haskell_csp: check_boolean_expression(X), X = false)). |
1984 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(bool_or(true,_X)))). |
1985 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(bool_not('<='(int(1),int(0)))))). |
1986 | | :- assert_must_fail((haskell_csp: check_boolean_expression(bool_not('<='(int(1),int(10)))))). |
1987 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(bool_and('<='(int(1),int(10)), true)))). |
1988 | | :- assert_must_fail((haskell_csp: check_boolean_expression(bool_and(false,'<='(int(1),int(10)))))). |
1989 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(bool_or('<='(int(1),int(0)), true)))). |
1990 | | :- assert_must_fail((haskell_csp: check_boolean_expression(bool_or(false,'<='(int(1),int(0)))))). |
1991 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('<='(int(10),int(X))), X = 30)). |
1992 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('>='(int(10),int(X))), X = 3)). |
1993 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('<='(int(10),int(X))), X = 10)). |
1994 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('>='(int(10),int(X))), X = 10)). |
1995 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('<'(int(10),int(X))), X = 30)). |
1996 | | :- assert_must_succeed((haskell_csp: check_boolean_expression('>'(int(10),int(X))), X = 3)). |
1997 | | :- assert_must_fail((haskell_csp: check_boolean_expression('<'(int(10),int(X))), X = 10)). |
1998 | | :- assert_must_fail((haskell_csp: check_boolean_expression('>'(int(10),int(X))), X = 10)). |
1999 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(20)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)))). |
2000 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(10)),span,span,span)))). |
2001 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(10)),span,span,span)))). |
2002 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(ifte(X,'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)), |
2003 | | X = head(listExp(rangeEnum(['<='(int(2),int(3)),'>'(int(2),int(3))]))))). |
2004 | | :- assert_must_fail((haskell_csp: check_boolean_expression(ifte(X,'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span)), |
2005 | | X = head(listExp(rangeEnum(['<='(int(2),int(1)),'>'(int(2),int(3))]))))). |
2006 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<'(int(2),int(3)),'>'(int(2),int(3))])))))). |
2007 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([true,false])))))). |
2008 | | :- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([false,false])))))). |
2009 | | :- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([false,true])))))). |
2010 | | :- assert_must_fail((haskell_csp: check_boolean_expression((head(listExp(rangeEnum([null(listExp(rangeEnum([false,true])))]))))))). |
2011 | | :- assert_must_fail((haskell_csp: check_boolean_expression((head(listExp(rangeEnum([empty(setValue([int(1),int(2)]))]))))))). |
2012 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([])))))). |
2013 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([bool_not(false)])))))). |
2014 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum([bool_or(true,false)])))))). |
2015 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<='(int(2),int(3)),'>'(int(2),int(3))])))))). |
2016 | | :- assert_must_fail((haskell_csp: check_boolean_expression(head(listExp(rangeEnum(['<='(int(2),int(1)),'>'(int(2),int(3))])))))). |
2017 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(null(listExp(rangeEnum([])))))). |
2018 | | :- assert_must_fail((haskell_csp: check_boolean_expression(null(listExp(rangeEnum([int(1),int(2),int(3)])))))). |
2019 | | :- assert_must_succeed((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([])))))). |
2020 | | :- assert_must_fail((haskell_csp: check_boolean_expression(empty(setExp(rangeEnum([int(1),int(2),int(3)])))))). |
2021 | | :- assert_must_succeed((haskell_csp: is_boolean_expression(true), haskell_csp: is_boolean_expression(false))). |
2022 | | |
2023 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
2024 | | |
2025 | | :- block check_boolean_expression(-). |
2026 | | |
2027 | | %check_boolean_expression(E) :- %print(check_boolean_expression(E)),nl, |
2028 | | % var(E),add_error(check_boolean_expression,'Variable boolean expression:',E),fail. |
2029 | | check_boolean_expression(true) :- !. |
2030 | | check_boolean_expression(false) :- !, fail. |
2031 | | check_boolean_expression(bool_not(BExpr1)) :- !, |
2032 | | evaluate_boolean_expression(BExpr1,false). /* provide custom check_not_... predicate ?? */ |
2033 | | check_boolean_expression(bool_and(BExpr1,BExpr2)) :- !, |
2034 | | check_boolean_expression(BExpr1), |
2035 | ? | check_boolean_expression(BExpr2). |
2036 | | check_boolean_expression(bool_or(BExpr1,BExpr2)) :- !, |
2037 | | evaluate_boolean_expression(BExpr1,R1), |
2038 | | cond_check_boolean_expression(R1,BExpr2). |
2039 | | check_boolean_expression(ifte(Test,Then,Else,_,_,_)) :- !, |
2040 | | evaluate_boolean_expression(Test,TestRes), %print(check_bool_ifte(Test,TestRes)),nl, |
2041 | | ifte_check_boolean_expression(TestRes,Then,Else). |
2042 | | check_boolean_expression(head(X)) :- !, force_evaluate_argument(X,EX),head_list(EX,HResult), |
2043 | | check_boolean_expression(HResult). |
2044 | | check_boolean_expression(null(Arg1)) :- !, force_evaluate_argument(Arg1,EX), is_null_list(EX,true). |
2045 | | check_boolean_expression(empty(Arg1)) :- !, force_evaluate_argument(Arg1,EX), is_empty_set(EX,true). |
2046 | | check_boolean_expression(agent_call(Span,F,Par)) :- !, /* in this context we need the result of the function call */ |
2047 | | unfold_function_call_once(F,Par,Body,Span), |
2048 | | %when(nonvar(Body), |
2049 | | check_boolean_expression(Body). |
2050 | | check_boolean_expression('member'(Arg1,Arg2)) :- !, % after bool_binary_op: there is a special rule for member there |
2051 | | force_evaluate_argument(Arg1,EX), |
2052 | | force_evaluate_argument_for_member_check(Arg2,EY), %print(lazy_member(EX,EY)),nl, |
2053 | | % causes 10 % slowdown on basin_olderog_bank, but code is probably required similar to evaluate_boolean_expression below |
2054 | | % when(ground(EX), (ground(EY) -> is_member_set(EX,EY) |
2055 | | % ; /* exploring lazy expression */ force_evaluate_argument(EY,REY),is_member_set(EX,REY))). |
2056 | ? | when((ground(EX),ground(EY)), is_member_set(EX,EY)). |
2057 | | check_boolean_expression(BExpr) :- %covering all boolean expression with relational operators instead of '==' and '!='% |
2058 | | relational_binary_op(BExpr,Arg1,Arg2,EX,EY,Call),!, |
2059 | | evaluate_int_argument(Arg1,EX), |
2060 | | evaluate_int_argument(Arg2,EY), |
2061 | | Call. |
2062 | | check_boolean_expression(BExpr) :- |
2063 | | bool_binary_op(BExpr,Arg1,Arg2,EX,EY,Call), !, |
2064 | | %print(bool_binary_op(Arg1,Arg2,Call)),nl, % |
2065 | | force_evaluate_argument(Arg1,EX), |
2066 | | force_evaluate_argument(Arg2,EY), |
2067 | ? | when((ground(EX),ground(EY)), Call). |
2068 | | check_boolean_expression(X) :- |
2069 | | add_error(haskell_csp,'Not a boolean expression: ',X), |
2070 | | fail. |
2071 | | |
2072 | | |
2073 | | :- block cond_check_boolean_expression(-,?). |
2074 | | cond_check_boolean_expression(true,_). |
2075 | | cond_check_boolean_expression(false,BExpr2) :- check_boolean_expression(BExpr2). |
2076 | | |
2077 | | :- block ifte_check_boolean_expression(-,?,?). |
2078 | | ifte_check_boolean_expression(true,Then,_) :- !, check_boolean_expression(Then). |
2079 | | ifte_check_boolean_expression(false,_,Else) :- !, check_boolean_expression(Else). |
2080 | | % evaluate_boolean_expression/3 will raise an error if the boolean expression in the ifte-condition cannot be evaluated to true or false => Internal Error |
2081 | | ifte_check_boolean_expression(Other,Then,Else) :- add_internal_error(/*ifte_check_boolean_expression,*/ |
2082 | | 'Internal Error: Not a boolean inside if-then-else test: ', |
2083 | | ifte_check_boolean_expression(Other,Then,Else)),fail. |
2084 | | |
2085 | | :- block evaluate_boolean_expression(-,?). |
2086 | | %evaluate_boolean_expression(E,_) :- %print(evaluate_boolean_expression(E)),nl, |
2087 | | % var(E),add_error(evaluate_boolean_expression,'Variable boolean expression:',E),fail. |
2088 | | evaluate_boolean_expression(true,R) :- !, R=true. |
2089 | | evaluate_boolean_expression(false,R) :- !, R=false. |
2090 | | evaluate_boolean_expression(bool_not(BExpr1),Res) :- !, |
2091 | | evaluate_boolean_expression(BExpr1,R1), |
2092 | | negate(R1,Res). |
2093 | | evaluate_boolean_expression(bool_and(BExpr1,BExpr2),Res) :- !, |
2094 | | evaluate_boolean_expression(BExpr1,R1), |
2095 | | cond_evalf_boolean_expression(R1,BExpr2,Res). |
2096 | | evaluate_boolean_expression(bool_or(BExpr1,BExpr2),Res) :- !, |
2097 | | evaluate_boolean_expression(BExpr1,R1), |
2098 | | cond_evalt_boolean_expression(R1,BExpr2,Res). |
2099 | | % when(ground(R1), |
2100 | | % (R1=true -> Res = true |
2101 | | % ; evaluate_boolean_expression(BExpr2,Res))). |
2102 | | evaluate_boolean_expression('<'(Arg1,Arg2),Res) :- !, |
2103 | | evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than(EX,EY,Res). |
2104 | | evaluate_boolean_expression('>'(Arg1,Arg2),Res) :- !, |
2105 | | evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than(EY,EX,Res). |
2106 | | evaluate_boolean_expression('<='(Arg1,Arg2),Res) :- !, |
2107 | | evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than_equal(EX,EY,Res). |
2108 | | evaluate_boolean_expression('>='(Arg1,Arg2),Res) :- !, |
2109 | | evaluate_int_argument(Arg1,EX),evaluate_int_argument(Arg2,EY),safe_less_than_equal(EY,EX,Res). |
2110 | | evaluate_boolean_expression(ifte(Test,Then,Else,_,_,_),R) :- !, |
2111 | | evaluate_boolean_expression(Test,TestRes), |
2112 | | ifte_eval_boolean_expression(TestRes,Then,Else,R). |
2113 | | evaluate_boolean_expression(head(X),R) :- !, force_evaluate_argument(X,EX),head_list(EX,HResult), |
2114 | | evaluate_boolean_expression(HResult,R). |
2115 | | evaluate_boolean_expression(agent_call(Span,F,Par),R) :- !, /* in this context we need the result of the function call */ |
2116 | | unfold_function_call_once(F,Par,Body,Span), |
2117 | | %when(nonvar(Body), |
2118 | | evaluate_boolean_expression(Body,R). |
2119 | | evaluate_boolean_expression(prolog_constraint(C),Res) :- !, %% print(prolog_constraint(C)),nl, |
2120 | | (call(C) -> Res = true ; Res = false). |
2121 | | evaluate_boolean_expression(null(Arg1),Res) :- !, force_evaluate_argument(Arg1,EX), is_null_list(EX,Res). |
2122 | | evaluate_boolean_expression(empty(Arg1),Res) :- !, force_evaluate_argument(Arg1,EX), is_empty_set(EX,Res). |
2123 | | evaluate_boolean_expression(BExpr,Res) :- |
2124 | | bool_binary_op(BExpr,Arg1,Arg2,EX,EY,Call), !, % print(binop(BExpr,Arg1,Arg2)),nl, |
2125 | | force_evaluate_argument(Arg1,EX), |
2126 | | force_evaluate_argument(Arg2,EY), %print(ebe(Call)),nl, |
2127 | | when((ground(EX),ground(EY)), |
2128 | | (Call -> Res = true ; Res = false)). |
2129 | | evaluate_boolean_expression('member'(Arg1,Arg2),Res) :- !, % after bool_binary_op: there is a special rule for member there |
2130 | | force_evaluate_argument(Arg1,EX), |
2131 | | force_evaluate_argument_for_member_check(Arg2,EY), %print(lazy_member(EX,EY)),nl, |
2132 | ? | when(ground(EX), |
2133 | | (ground(EY) -> (is_member_set(EX,EY) -> Res = true ; Res = false) |
2134 | | ; /* exploring lazy expression */ force_evaluate_argument(EY,REY),(is_member_set(EX,REY) -> Res = true ; Res = false))). |
2135 | | evaluate_boolean_expression(builtin_call(X),Res) :- !, evaluate_boolean_expression(X,Res). |
2136 | | evaluate_boolean_expression(X,_R) :- |
2137 | | add_error(haskell_csp,'Not a boolean expression: ',X), |
2138 | | fail. |
2139 | | |
2140 | | |
2141 | | :- block negate(-,?). |
2142 | | negate(true,false). |
2143 | | negate(false,true). |
2144 | | |
2145 | | :- block cond_evalt_boolean_expression(-,?,?). |
2146 | | cond_evalt_boolean_expression(true,_,true). |
2147 | | cond_evalt_boolean_expression(false,BExpr2,Res) :- evaluate_boolean_expression(BExpr2,Res). |
2148 | | |
2149 | | :- block cond_evalf_boolean_expression(-,?,?). |
2150 | | cond_evalf_boolean_expression(false,_,false). |
2151 | | cond_evalf_boolean_expression(true,BExpr2,Res) :- evaluate_boolean_expression(BExpr2,Res). |
2152 | | |
2153 | | :- block ifte_eval_boolean_expression(-,?,?,?). |
2154 | | ifte_eval_boolean_expression(true,Then,_,Res) :- !, evaluate_boolean_expression(Then,Res). |
2155 | | ifte_eval_boolean_expression(false,_,Else,Res) :- !, evaluate_boolean_expression(Else,Res). |
2156 | | ifte_eval_boolean_expression(Other,Then,Else,Res) :- /* evaluate_boolean_expression/2 will catch the error if there |
2157 | | is no boolean expression test, thus internal_error must be generated for this clause. */ |
2158 | | add_internal_error('Not a boolean inside if-then-else boolean expression test: ', |
2159 | | ifte_eval_boolean_expression(Other,Then,Else,Res)),fail. |
2160 | | |
2161 | | bool_binary_int_op('<'(X,Y),X,Y,EX,EY,'<'(EX,EY)). |
2162 | | bool_binary_int_op('>'(X,Y),X,Y,EX,EY,'>'(EX,EY)). |
2163 | | bool_binary_int_op('>='(X,Y),X,Y,EX,EY,'>='(EX,EY)). |
2164 | | bool_binary_int_op('<='(X,Y),X,Y,EX,EY,'=<'(EX,EY)). |
2165 | | |
2166 | | relational_binary_op('<'(X,Y),X,Y,EX,EY,safe_less_than(EX,EY)). |
2167 | | relational_binary_op('>'(X,Y),X,Y,EX,EY,safe_less_than(EY,EX)). |
2168 | | relational_binary_op('<='(X,Y),X,Y,EX,EY,safe_less_than_equal(EX,EY)). |
2169 | | relational_binary_op('>='(X,Y),X,Y,EX,EY,safe_less_than_equal(EY,EX)). |
2170 | | |
2171 | | bool_binary_op('elem'(X,Y),X,Y,EX,EY,is_elem_list(EX,EY)). |
2172 | | %bool_binary_op('member'(X,Y),X,Y,EX,EY,is_member_set(EX,EY)) :- (X=setValue(_) -> false;true). |
2173 | | bool_binary_op('member'(X,'Set'(Y)),X,Y,EX,EY,is_subset_of(EX,EY)) :- |
2174 | | (X\=setValue(_) -> false; \+ground(X) -> false; true). |
2175 | | bool_binary_op('=='(X,Y),X,Y,EX,EY,equal_element(EX,EY)). |
2176 | | bool_binary_op('!='(X,Y),X,Y,EX,EY,not_equal_element(EX,EY)). |
2177 | | |
2178 | | bool_binary_op_symbolic('member'(X,Y),X,Y,EX,EY,is_member_set(EX,EY)). % dealt with separately |
2179 | | |
2180 | | unary_op(null(X),X,EX,is_null_list(EX)). |
2181 | | unary_op(empty(X),X,EX,is_empty_set(EX,true)). |
2182 | | |
2183 | | is_boolean_expression(true). |
2184 | | is_boolean_expression(false). |
2185 | | is_boolean_expression(bool_not(_)). |
2186 | | is_boolean_expression(bool_and(_,_)). |
2187 | | is_boolean_expression(bool_or(_,_)). |
2188 | | is_boolean_expression(X) :- |
2189 | | (unary_op(X,_,_,_) ; bool_binary_op(X,_,_,_,_,_) ; bool_binary_op_symbolic(X,_,_,_,_,_) ; bool_binary_int_op(X,_,_,_,_,_)). |
2190 | | |
2191 | | |
2192 | | /* ------------------------------------- */ |
2193 | | /* SEQUENCES */ |
2194 | | /* ------------------------------------- */ |
2195 | | |
2196 | | :- use_module(probcspsrc(csp_sequences)). |
2197 | | |
2198 | | /* ------------------------------------- */ |
2199 | | /* VALUE EXPRESSIONS */ |
2200 | | /* ------------------------------------- */ |
2201 | | |
2202 | | :- type channelio +--> (atomic ; dotTuple(list(atomic))). |
2203 | | |
2204 | | :- type channel_set +--> (setValue(list(channelio)) ; closure(list(channelio))). |
2205 | | |
2206 | | :- type cspm_expr +--> (type(cspm_arith_expr) ; type(channel_set) ; atomic ; agent_call(ground,nonvar,list(any)) ). |
2207 | | |
2208 | | :- type cspm_arith_expr +--> (int(integer) ; |
2209 | | '+'(cspm_arith_expr,cspm_arith_expr) ; |
2210 | | '-'(cspm_arith_expr,cspm_arith_expr) ; |
2211 | | '*'(cspm_arith_expr,cspm_arith_expr) ; |
2212 | | '/'(cspm_arith_expr,cspm_arith_expr) ; |
2213 | | '%'(cspm_arith_expr,cspm_arith_expr) ). |
2214 | | |
2215 | | % forcing arguments in the context of a member check; will be used as second arg to is_member_set |
2216 | | % This means that certain things do not need to be computed (Union for example) |
2217 | | :- block force_evaluate_argument_for_member_check(-,?). |
2218 | | force_evaluate_argument_for_member_check(agent_call(Span,F,Par),R) :- !, |
2219 | | %print(unfold(F,Par,Body)),nl, |
2220 | | unfold_function_call_once(F,Par,Body,Span), |
2221 | ? | force_evaluate_argument_for_member_check(Body,R). |
2222 | | % keep the following symbolic: |
2223 | | force_evaluate_argument_for_member_check(setExp(rangeEnum(T),G),R) :- nonvar(T),T=[H|TT],TT==[], var(H), !, |
2224 | | % if the tuples T have more than one element, we currently cannot check membership symbolically |
2225 | | R=setExp(rangeEnum(T),G). % TO DO expand for rangeClosed,... |
2226 | | force_evaluate_argument_for_member_check('Union'(L),R) :- !, |
2227 | | force_evaluate_argument_for_member_check_into_list(L,LL), %print(evalUnion(L,LL)),nl, |
2228 | | R='Union'(LL). |
2229 | | force_evaluate_argument_for_member_check('Inter'(L),R) :- !, |
2230 | | force_evaluate_argument_for_member_check_into_list(L,LL), R='Inter'(LL). |
2231 | | force_evaluate_argument_for_member_check('Seq'(L),R) :- !, R='Seq'(L). |
2232 | | |
2233 | ? | force_evaluate_argument_for_member_check(X,EX) :- force_evaluate_argument(X,EX). |
2234 | | |
2235 | | % force evaluating a set into a list of elements; do not worry about checking duplicates in list |
2236 | | :- block force_evaluate_argument_for_member_check_into_list(-,?). |
2237 | | %force_evaluate_argument_for_member_check_into_list(A,R) :- print(force_evaluate_argument_for_member_check_into_list(A,R)),nl,fail. |
2238 | | force_evaluate_argument_for_member_check_into_list(agent_call(Span,F,Par),R) :- !, |
2239 | | /* in this context we need the result of the function call */ |
2240 | | unfold_function_call_once(F,Par,Body,Span), |
2241 | | force_evaluate_argument_for_member_check_into_list(Body,R). |
2242 | | force_evaluate_argument_for_member_check_into_list(setExp(rangeEnum(L)),R) :- !, |
2243 | | force_evaluate_list_for_member_check(L,LL),R=setExp(rangeEnum(LL)). |
2244 | | force_evaluate_argument_for_member_check_into_list(X,EX) :- force_evaluate_argument(X,EX). |
2245 | | |
2246 | | :- block force_evaluate_list_for_member_check(-,?). |
2247 | | force_evaluate_list_for_member_check([],R) :- !,R=[]. |
2248 | | force_evaluate_list_for_member_check([H|T],R) :- !, R=[EH|ET], |
2249 | | force_evaluate_argument_for_member_check(H,EH), |
2250 | | force_evaluate_list_for_member_check(T,ET). |
2251 | | force_evaluate_list_for_member_check(X,R) :- |
2252 | | add_internal_error('Iternal Error: Could not evaluate list: ',force_evaluate_list_for_member_check(X,R)),R=X. |
2253 | | |
2254 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR force_evaluate_argument/2, evaluate_argument/2 and evaluate_expression/2 %%%%%%%%%%%%%%%%%%%%%%% |
2255 | | :- assert_must_succeed((haskell_csp: force_evaluate_argument(listFromTo(1,3),R), R == list([int(1),int(2),int(3)]))). |
2256 | | :- assert_must_succeed((haskell_csp: evaluate_argument(listFromTo(1,3),R), R == list([int(1),int(2),int(3)]))). |
2257 | | :- assert_must_succeed((haskell_csp: evaluate_argument(listFrom(1),R), R == listFrom(1))). |
2258 | | :- assert_must_succeed((haskell_csp: evaluate_argument(setFromTo(1,3),R), R == setFromTo(1,3))). |
2259 | | :- assert_must_succeed((haskell_csp: evaluate_argument(list([int(1),int(2)]),R), R == list([int(1),int(2)]))). |
2260 | | :- assert_must_succeed((haskell_csp: force_evaluate_argument(listPat([int(1),int(2)]),R), R == list([int(1),int(2)]))). |
2261 | | :- assert_must_succeed((haskell_csp: evaluate_argument(ifte('<='(int(3),int(20)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span),R) ,R == true)). |
2262 | | :- assert_must_succeed(( |
2263 | | haskell_csp: evaluate_argument(ifte('<='(int(3),int(2)),'>='(int(2),int(1)),'<='(int(3),int(1)),span,span,span),R), R ==false)). |
2264 | | :- assert_must_succeed((haskell_csp: evaluate_argument(ifte('<='(int(3),int(2)),int(1),int(2),span,span,span),R), R == int(2))). |
2265 | | :- assert_must_succeed((haskell_csp: evaluate_argument(dataType('FRUIT'),R), R == dataType('FRUIT'))). |
2266 | | :- assert_must_succeed((haskell_csp: evaluate_argument(concat(listExp(rangeEnum([listFromTo(1,3),listExp(rangeEnum([int(4)]))]))),R), |
2267 | | R == list([int(1),int(2),int(3),int(4)]))). |
2268 | | :- assert_must_succeed((haskell_csp: evaluate_argument(listPat([int(1),int(2)]),R), R == list([int(1),int(2)]))). |
2269 | | :- assert_must_succeed((haskell_csp: evaluate_argument(tuplePat([int(1),int(2)]),R), R == na_tuple([int(1),int(2)]))). |
2270 | | :- assert_must_succeed((haskell_csp: evaluate_expression(setExp(rangeEnum([int(1),int(2)])),R), R == setValue([int(1),int(2)]))). |
2271 | | :- assert_must_succeed((haskell_csp: evaluate_expression(setFromTo(1,3),R), R == setValue([int(1),int(2),int(3)]))). |
2272 | | :- assert_must_succeed((haskell_csp: evaluate_expression(stop(src),R), R == 'Typed expression is a process construct.')). |
2273 | | :- assert_must_succeed((haskell_csp: evaluate_expression(left,R), R == 'Typed expression is a channel name.')). |
2274 | | :- assert_must_succeed((haskell_csp: evaluate_expression('Msg1',R), R == setValue(['A','B']))). |
2275 | | :- assert_must_succeed((haskell_csp: evaluate_expression('Msg1',R), R == setValue(['A','B']))). |
2276 | | :- assert_must_succeed((haskell_csp: evaluate_expression(builtin_call(set(listExp(rangeEnum([int(1),int(1)])))),R), R == setValue([int(1)]))). |
2277 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
2278 | | |
2279 | | evaluate_expression(X,R) :- var(X),!, |
2280 | | add_internal_error('Internal Error: Variable expression to evaluate: ',evaluate_expression(X,R)), |
2281 | | fail. |
2282 | | evaluate_expression('Events',R) :- !, |
2283 | | findall(Channel,is_a_channel_name(Channel),CL), |
2284 | | evaluate_list(CL,CLL), closure_expand(CLL,R). |
2285 | | evaluate_expression(closure(X),R) :- !, |
2286 | | evaluate_list(X,XL), closure_expand(XL,R). |
2287 | | evaluate_expression(builtin_call(X),R) :- !, evaluate_expression(X,R). |
2288 | | evaluate_expression(setExp(X),R) :- !, evaluate_set_expression(X,EX),expand_symbolic_set(EX,R,evaluate_expression). |
2289 | | evaluate_expression(setFromTo(Low,Up),R) :- !, expand_symbolic_set(setFromTo(Low,Up),R,evaluate_expression). |
2290 | | evaluate_expression(val_of(X,Src),R) :- !, evaluate_argument2(val_of(X,Src),R). |
2291 | | evaluate_expression(DT,R) :- is_a_datatype(DT,_),!, |
2292 | | expand_symbolic_set(dataType(DT),R,eval). |
2293 | | evaluate_expression(Proc,R) :- definite_cspm_process_expression(Proc),!, R='Typed expression is a process construct.'. |
2294 | | evaluate_expression(Ch,R) :- is_a_channel_name(Ch),!, R='Typed expression is a channel name.'. |
2295 | | evaluate_expression(E,R) :- force_evaluate_argument(E,R). |
2296 | | |
2297 | | :- block force_evaluate_argument(-,?). |
2298 | | force_evaluate_argument(Num,R) :- number(Num),!,R=int(Num). |
2299 | | force_evaluate_argument(agent_call(Span,F,Par),R) :- !, /* in this context we need the result of the function call */ |
2300 | ? | unfold_function_call_once(F,Par,Body,Span), |
2301 | ? | force_evaluate_argument(Body,R). |
2302 | | force_evaluate_argument(setExp(RangeExpr,Generators),R) :- !, |
2303 | | expand_set_comprehension(RangeExpr,Generators,R). |
2304 | | %force_evaluate_argument(comprehensionGenerator(Var,Set),R) :- !, |
2305 | | % R = comprehensionGenerator(Var,ESet), |
2306 | | % force_evaluate_argument(Set,ESet). |
2307 | | force_evaluate_argument(ifte(Test,Then,Else,_S1,_S2,_S3),R) :- !, |
2308 | | evaluate_boolean_expression(Test,TestRes), % print(force_ifte(Test,TestRes)),nl, |
2309 | ? | ifte_force_evaluate_argument(TestRes,Then,Else,R). |
2310 | | force_evaluate_argument(list(X),R) :- !, %print(eval_list(X)),nl, |
2311 | | force_evaluate_list(X,EX), % use force_evaluate_list_skel ??; perf. problem in misusing_lists |
2312 | | R=list(EX). |
2313 | | force_evaluate_argument(listPat(X),R) :- !, %print(eval_list(X)),nl, |
2314 | | force_evaluate_list(X,EX), % use force_evaluate_list_skel ??; perf. problem in misusing_lists |
2315 | | R=list(EX). |
2316 | | force_evaluate_argument(listFromTo(X,Y),Res) :- !, expand_sequence(listFromTo(X,Y),Res). |
2317 | | force_evaluate_argument(listExp(S),ERes) :- !, evaluate_list_expression(S,Res), expand_sequence(Res,ERes). |
2318 | | %force_evaluate_argument(setValue(X),R) :- !, force_evaluate_set(X,R), print(fes(X,R)),nl. |
2319 | | % Maybe we should ensure that setValues are always force evaluated: we only need to |
2320 | | % take care when using set operations for replicated operators |
2321 | | force_evaluate_argument(Destr,Result) :- destructor(Destr),!, % we may need to further evaluate result |
2322 | | evaluate_argument2(Destr,EX), % do ordinary evaluation |
2323 | | force_evaluate_argument(EX,Result). |
2324 | ? | force_evaluate_argument(E,R) :- evaluate_argument2(E,R). /* could there be lazy constructs lurking deep inside E ??? */ |
2325 | | |
2326 | | destructor(head(_)). |
2327 | | destructor(na_tuple_projection(_,_,_)). |
2328 | | destructor(tuple_projection(_,_,_)). |
2329 | | %destructor(record(_,_)). |
2330 | | % records ? |
2331 | | |
2332 | | |
2333 | | :- block ifte_force_evaluate_argument(-,?,?,?). |
2334 | ? | ifte_force_evaluate_argument(true,Then,_,Res) :- !, force_evaluate_argument(Then,Res). |
2335 | | ifte_force_evaluate_argument(false,_,Else,Res) :- !, force_evaluate_argument(Else,Res). |
2336 | | /* See comment for the error clause of the ifte_evaluate_argument/4 predicate. Same argument as below |
2337 | | for assuming the error clause as caused by internal call only. */ |
2338 | | ifte_force_evaluate_argument(Other,Then,Else,Res) :- |
2339 | | add_internal_error('Internal Error: Not a boolean inside if-then-else test: ', |
2340 | | ifte_force_evaluate_argument(Other,Then,Else,Res) ),fail. |
2341 | | |
2342 | | :- block ifte_evaluate_argument(-,?,?,?). |
2343 | | ifte_evaluate_argument(true,Then,_,Res) :- !, evaluate_argument(Then,Res). |
2344 | | ifte_evaluate_argument(false,_,Else,Res) :- !, evaluate_argument(Else,Res). |
2345 | | /* evaluate_boolean_expression/2 predicate is called before ifte_evaluate_argument/4. |
2346 | | evaluate_boolean_expression/2 provides as result either true or false, that's why only internal call can |
2347 | | raise error for this predicate. */ |
2348 | | ifte_evaluate_argument(Other,Then,Else,Res) :- |
2349 | | add_internal_error('Internal Error: Not a boolean inside if-then-else test: ', |
2350 | | ifte_evaluate_argument(Other,Then,Else,Res)),fail. |
2351 | | |
2352 | | %evaluate_argument(E,R) :- print(evaluate_argument(E,R)),nl, |
2353 | | %(nonvar(R) -> true ; when(nonvar(R),(print(inst_eval(E,R)),nl,trace))), evaluate_argument1(E,R). |
2354 | | :- block evaluate_argument(-,?). |
2355 | ? | evaluate_argument(Expr,Res) :- evaluate_argument2(Expr,Res). |
2356 | | |
2357 | | evaluate_argument2(ifte(Test,Then,Else,_S1,_S2,_S3),R) :- !, |
2358 | | evaluate_boolean_expression(Test,TestRes), %print(ifte(Test,TestRes)),nl, |
2359 | | ifte_evaluate_argument(TestRes,Then,Else,R). |
2360 | | % when(ground(TestRes),(TestRes=true -> evaluate_argument(Then,R) ; evaluate_argument(Else,R))). |
2361 | | evaluate_argument2(int(X),R) :- !,R=int(X). |
2362 | | % case should be added because of the clpfd-library |
2363 | | evaluate_argument2(Num,R) :- number(Num),!,R=int(Num). |
2364 | | evaluate_argument2(true,R) :- !,R=true. |
2365 | | evaluate_argument2(false,R) :- !,R=false. |
2366 | | evaluate_argument2(negate(X),Result) :- !, Result = int(Res), |
2367 | | evaluate_int_argument(X,EX), |
2368 | | safe_is(Res,-(EX)). |
2369 | | evaluate_argument2('+'(X,Y),Result) :- !, Result = int(Res), |
2370 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2371 | | safe_is(Res,EX+EY). |
2372 | | evaluate_argument2('-'(X,Y),Result) :- !, Result = int(Res), |
2373 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2374 | | safe_is(Res,EX-EY). |
2375 | | evaluate_argument2('*'(X,Y),Result) :- !, Result = int(Res), |
2376 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2377 | | safe_is(Res,EX * EY). |
2378 | | evaluate_argument2('/'(X,Y),Result) :- !, Result = int(Res), |
2379 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2380 | | safe_is(Res,EX // EY). |
2381 | | evaluate_argument2('%'(X,Y),Result) :- !, Result = int(Res), |
2382 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2383 | | safe_is(Res,EX mod EY). |
2384 | | evaluate_argument2(length(X),Result) :- !, force_evaluate_argument(X,EX),length_list(EX,Result). |
2385 | | evaluate_argument2('#'(X),Result) :- !, force_evaluate_argument(X,EX),length_list(EX,Result). |
2386 | | evaluate_argument2(head(X),Result) :- !, force_evaluate_argument(X,EX), |
2387 | | head_list(EX,Result). |
2388 | | evaluate_argument2(tail(X),Result) :- !, force_evaluate_argument(X,EX),tail_list(EX,Result). |
2389 | | evaluate_argument2('^'(X,Y),Result) :- !, |
2390 | | force_evaluate_argument(X,EX),force_evaluate_argument(Y,EY), |
2391 | | %print('^'(X,EX,Y,EY)),nl, |
2392 | | append_list(EX,EY,Result). %, print(append_list(EX,EY,Result)),nl. |
2393 | | evaluate_argument2(concat(X),Result) :- !, force_evaluate_argument(X,EX), |
2394 | | concat_lists(EX,Result). |
2395 | | evaluate_argument2(listFromTo(X,Y),Res) :- !, |
2396 | | %evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2397 | | expand_sequence(listFromTo(X,Y),Res). |
2398 | | evaluate_argument2(listFrom(X),Res) :- !, Res = listFrom(X). % already evaluated |
2399 | | evaluate_argument2(listExp(S),Res) :- !, evaluate_list_expression(S,Res). |
2400 | | evaluate_argument2(listExp(RangeExpr,Generators),R) :- !, %print(listExp(Generators,RangeExpr)),nl, |
2401 | | expand_listcomprehension(RangeExpr,Generators,R). %, print(res(R)),nl. |
2402 | | %evaluate_argument2(listComp(Generators,Tuples),R) :- !, %force_evaluate_list(Generators,EGen), |
2403 | | % expand_sequence(listComp(Generators,Tuples),R). |
2404 | | evaluate_argument2(set(X),Res) :- !, evaluate_argument2(seq_to_set(X),Res). |
2405 | | evaluate_argument2(seq(X),Res) :- !, evaluate_argument2(set_to_seq(X),Res). |
2406 | | evaluate_argument2(set_to_seq(X),Res) :- !, |
2407 | | force_evaluate_argument(X,EX), |
2408 | | convert_set_to_seq(EX,Res). |
2409 | | evaluate_argument2(seq_to_set(X),Res) :- !, |
2410 | | force_evaluate_argument(X,EX), |
2411 | | convert_seq_to_set(EX,Res). |
2412 | | evaluate_argument2(setFromTo(X,Y),Res) :- !, Res = setFromTo(X,Y). % already computed set expression |
2413 | | evaluate_argument2(setExp(S),Res) :- !, evaluate_set_expression(S,Res). |
2414 | | evaluate_argument2(setExp(RangeExpr,Generators),R) :- !, %print(setExp(Generators,RangeExpr)),nl, |
2415 | | expand_set_comprehension(RangeExpr,Generators,R). |
2416 | | evaluate_argument2(setValue(X),R) :- !, R=setValue(X). |
2417 | | evaluate_argument2(singleSetPatValue(X,Span),R) :- !, force_evaluate_argument(X,EX), |
2418 | | %print(singleSetPatValue(X,EX,R)),nl, |
2419 | | singleSetElement(EX,R,Span). |
2420 | | evaluate_argument2('Seq'(X),R) :- !, evaluate_argument(X,EX),R='Seq'(EX). |
2421 | | evaluate_argument2(intType,R) :- !, R=intType. |
2422 | | evaluate_argument2(boolType,R) :- !, R=boolType. |
2423 | | %evaluate_argument2(setEnum(X),R) :- !, evaluate_list(X,XL), evaluate_set(XL,R). |
2424 | | |
2425 | | evaluate_argument2(closureComp(Generators,Tuples),R) :- !, |
2426 | | % print(closureComp(Generators,Tuples)),nl, |
2427 | | expand_symbolic_set(setExp(rangeEnum(Tuples),Generators),setValue(List),evaluate_argument_closureComp), |
2428 | | % print(closureset(List)),nl, |
2429 | | evaluate_argument2(closure(List),R). %print(doneclosureComp(R)),nl. |
2430 | | evaluate_argument2(closure(X),R) :- !, %print(eval(closure(X))),nl, |
2431 | | evaluate_list(X,XL), % print(evaluate_closure(XL,R)),nl, |
2432 | | evaluate_closure(XL,R). |
2433 | | %expand_channel_pattern_expression(closure(X),R,no_loc_info_available). |
2434 | | evaluate_argument2('Events',R) :- !, |
2435 | | findall(Channel,is_a_channel_name(Channel),CL), |
2436 | | evaluate_argument2(closure(CL),R). |
2437 | ? | evaluate_argument2(union(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY), |
2438 | ? | union_set(EX,EY,Result). |
2439 | | evaluate_argument2('Union'(X),Result) :- !, force_evaluate_argument(X,EX), |
2440 | ? | big_union(EX,Result). |
2441 | | evaluate_argument2('Inter'(X),Result) :- !, force_evaluate_argument(X,EX), |
2442 | ? | big_inter(EX,Result). |
2443 | ? | evaluate_argument2(diff(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY), |
2444 | | %print(diff_set(X,EX,Y,EY)),nl, |
2445 | | diff_set(EX,EY,Result). |
2446 | ? | evaluate_argument2(inter(X,Y),Result) :- !, force_evaluate_argument(X,EX), force_evaluate_argument(Y,EY), |
2447 | ? | inter_set(EX,EY,Result). |
2448 | ? | evaluate_argument2(card(X),Result) :- !, evaluate_argument(X,EX), |
2449 | | cardinality(EX,Result). |
2450 | | evaluate_argument2('Set'(X),Result) :- !, %print(subsets(X)),nl, |
2451 | | evaluate_argument(X,EX), |
2452 | | %print(calling_subsets(EX)),nl, |
2453 | | subsets(EX,Result). %, print(subset_result(Result)),nl. |
2454 | | evaluate_argument2(agent_call(Span,F,Par),R) :- !, |
2455 | ? | evaluate_agent_call(F,Par,R,Span). |
2456 | | evaluate_argument2(agent_call_curry(F,Par),R) :- !, |
2457 | | Span=no_loc_info_available, |
2458 | | unfold_function_call_curry_once(F,Par,Value,Span), |
2459 | | evaluate_argument(Value,R). |
2460 | | evaluate_argument2(val_of(VAR,Span),R) :- !, /* this can only happen inside channel type expressions; |
2461 | | other val_of's are compiled away by haskell_csp_analyzer */ |
2462 | | unfold_function_call_once(VAR,[],Body,Span), |
2463 | | evaluate_argument(Body,R). |
2464 | | evaluate_argument2([],R) :- !,R=[]. |
2465 | | evaluate_argument2([H|T],R) :- !,R=[H|T]. /* list of channel outputs */ |
2466 | | evaluate_argument2(builtin_call(X),R) :- !, evaluate_argument(X,R). |
2467 | | evaluate_argument2(dotTuple(X),R) :- !, evaluate_dot_tuple(X,R). |
2468 | | evaluate_argument2(dotTupleType(TupleArgs),R) :- !, |
2469 | | evaluate_list(TupleArgs,ETupleArgs), R = dotTupleType(ETupleArgs). |
2470 | | evaluate_argument2(dotpat(X),R) :- !, evaluate_dot_tuple(X,R). |
2471 | | evaluate_argument2(tuple(F),R) :- !, R=tuple(F). |
2472 | | evaluate_argument2(alsoPat(X,Y),R) :- !, |
2473 | | evaluate_argument2(X,EX), |
2474 | | evaluate_argument2(Y,EY), |
2475 | | R=alsoPat(EX,EY). |
2476 | | evaluate_argument2(lambda(A,B),R) :- !, %print(eval(lambda(A,B))),nl, |
2477 | | R=lambda(A,B), |
2478 | | (ground(A) -> true ; |
2479 | | mynumbervars(A)). /* numbervars to avoid nonvar states for ProB (slows down hashing,...) */ |
2480 | | evaluate_argument2(tuplePat(TupleArgs),R) :- !, /* a non-associative tuple */ |
2481 | | R = na_tuple(EA),force_evaluate_list(TupleArgs,EA). |
2482 | | evaluate_argument2(tupleExp(TupleArgs),R) :- !, /* a non-associative tuple; same as tuplePat but not in pattern position */ |
2483 | ? | R = na_tuple(EA),force_evaluate_list(TupleArgs,EA). |
2484 | | evaluate_argument2(typeTuple(TupleArgs),R) :- !, |
2485 | | evaluate_list(TupleArgs,ETupleArgs), R = typeTuple(ETupleArgs). |
2486 | | evaluate_argument2(na_tuple(F),R) :- !, R=na_tuple(F). /* non-associative tuple */ |
2487 | | evaluate_argument2(na_tuple_projection(Nr,Tuple,Span),R) :- !, |
2488 | | evaluate_int_argument(Nr,ENr,Span), |
2489 | | force_evaluate_argument(Tuple,ETuple), |
2490 | | na_tuple_projection(ENr,ETuple,R,Span). |
2491 | | evaluate_argument2(list_projection(Nr,Len,List,Span),R) :- !, |
2492 | | evaluate_int_argument(Nr,ENr,Span), |
2493 | | evaluate_int_argument(Len,ELen,Span), |
2494 | | force_evaluate_argument(List,EList), |
2495 | | list_projection(ENr,ELen,EList,R,Span). |
2496 | | evaluate_argument2(tuple_projection(Nr,Tuple,Span),R) :- !, |
2497 | | evaluate_int_argument(Nr,ENr,Span), |
2498 | | force_evaluate_argument(Tuple,ETuple), |
2499 | | tuple_projection(ENr,ETuple,R,Span). |
2500 | | evaluate_argument2(record(C,F),R) :- !, R=record(C,F). |
2501 | | evaluate_argument2(list(X),R) :- !, %print(eval_list(X)),nl, |
2502 | | %evaluate_list(X,EX), |
2503 | | R=list(X). % TO DO: check if we also need listPat |
2504 | | evaluate_argument2(listPat(X),R) :- !, |
2505 | | evaluate_list(X,EX), R=list(EX). |
2506 | | evaluate_argument2(rename(X,Y),R) :- !, |
2507 | | evaluate_rename_channel_expression(X,RX), /* should we evaluate ??? */ |
2508 | | evaluate_rename_channel_expression(Y,RY), |
2509 | | R=rename(RX,RY). |
2510 | | evaluate_argument2(link(X,Y),R) :- !, |
2511 | | evaluate_rename_channel_expression(X,RX), /* should we evaluate ??? */ |
2512 | | evaluate_rename_channel_expression(Y,RY), |
2513 | | R=link(RX,RY). |
2514 | | evaluate_argument2(dataType(DT),R) :- !, R=dataType(DT). |
2515 | | evaluate_argument2(Channel,R) :- |
2516 | | atomic(Channel),is_a_channel_name(Channel),!,R=tuple([Channel]). |
2517 | | evaluate_argument2(DT,R) :- name_type(DT,DT_Def), !, R=DT_Def. |
2518 | | evaluate_argument2(DT,R) :- dataTypeDef(DT,_), !, R=dataType(DT). |
2519 | | evaluate_argument2(DT,R) :- subTypeDef(DT,_), !, R=dataType(DT). |
2520 | | evaluate_argument2(X,R) :- valid_constant(X),!,R=X. |
2521 | | evaluate_argument2(X,R) :- agent_functor(X,_),!,R=X. /* when a function name is passed */ |
2522 | | evaluate_argument2(X,R) :- |
2523 | | is_csp_constructor(X),!,R=X. /* FDR does not allow this as a valid value; but can be fed into closure */ |
2524 | | evaluate_argument2(X,R) :- |
2525 | | (undefined_process_construct(X) -> |
2526 | ? | (is_boolean_expression(X) -> evaluate_boolean_expression(X,R) |
2527 | | /* we have a boolean value; we could also decide not to evaluate the argument and put R=X*/ |
2528 | | ; add_error(evaluate_argument2,'Cannot evaluate expression: ',X), R=X |
2529 | | ) |
2530 | | ; R=X /* we have a process description which is simply kept as is */ |
2531 | | ). |
2532 | | |
2533 | | % setExp(.) |
2534 | | evaluate_set_expression(rangeEnum(List),Res) :- !, %evaluate_list(List,XL), |
2535 | | evaluate_set(List,Res).%evaluate_set(List,Res,evaluate_argument). |
2536 | | evaluate_set_expression(rangeClosed(X,Y),Res) :- !, |
2537 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2538 | | ((number(X),number(Y),X>Y) -> Res= setValue([]) ; Res = setFromTo(EX,EY)). |
2539 | | evaluate_set_expression(rangeOpen(X),Res) :- !,Res = setFrom(EX), |
2540 | | evaluate_int_argument(X,EX). |
2541 | | evaluate_set_expression(A,Res) :- |
2542 | | add_internal_error('Internal Error: Unknown setExp: ',evaluate_set_expression(A,Res)),Res=[]. |
2543 | | |
2544 | | % listExp(.) |
2545 | | evaluate_list_expression(rangeEnum(List),Res) :- !, Res=list(LR), evaluate_list(List,LR). |
2546 | | evaluate_list_expression(rangeClosed(X,Y),Res) :- !, % print(evaluate_rangeClosed(X,Y)),nl, |
2547 | | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), |
2548 | | ((number(X),number(Y),X>Y) -> Res= list([]) ; Res = listFromTo(EX,EY)). |
2549 | | evaluate_list_expression(rangeOpen(X),Res) :- !,Res = listFrom(EX), |
2550 | | evaluate_int_argument(X,EX). |
2551 | | evaluate_list_expression(A,Res) :- /* CSP-M Parser cannot generate list expression, |
2552 | | which is not of the type rangeEnum/1, rangeClosed/2, rangeOpen/1. |
2553 | | That's why we can assume that in this case we have internal error. */ |
2554 | | add_internal_error('Internal Error: Unknown listExp: ',evaluate_list_expression(A,Res)),Res=[]. |
2555 | | |
2556 | | |
2557 | | |
2558 | | evaluate_function_name(F,EF) :- |
2559 | | (atomic(F) -> EF=F ; force_evaluate_argument(F,EF)). |
2560 | | |
2561 | | evaluate_agent_call(F,Par,Res,Span) :- % print(eval_agent_call(F,Par)),nl, |
2562 | ? | evaluate_function_name(F,EF),evaluate_agent_call2(EF,Par,Res,Span). |
2563 | | |
2564 | | evaluate_agent_call2(lambda(Args,Body),Par,R,Span) :- !, |
2565 | | unfold_function_call_once2(lambda(Args,Body),Par,NBody,Span), |
2566 | ? | evaluate_argument(NBody,R). |
2567 | | evaluate_agent_call2(F,Par,R,Span) :- !, |
2568 | | (atomic(F) -> true |
2569 | | ; add_error(evaluate_argument,'Illegal function name for function application: ',agent_call(F,Par),Span),fail), |
2570 | | X =.. [F|Par], |
2571 | | ((is_csp_process(X) ; is_possible_csp_process(X)) % ATTENTION: the parameter in is_possible_csp_process/1 can be a function call, which can be missunderstood as process |
2572 | | % a reimplementation of the is_possible_csp_process/1 is needed. |
2573 | | -> R=agent_call(Span,F,Par) %%%, print(keeping(X)),nl) |
2574 | | /* keep agent_calls lazily; they are processes. If we unfold then the variables will be |
2575 | | propagated into the term; causing problems by instantiation (see e.g. Repeat(Proc) = Proc ; Repeat(Proc)) */ |
2576 | | /* QUESTION: what about is_possible_csp_process ??? */ |
2577 | | ; unfold_function_call_once2(F,Par,Body,Span), |
2578 | ? | evaluate_argument(Body,R) /* TO DO: avoid re-checking when(nonvar ... for recursive calls ?*/ |
2579 | | % force_evaluate_argument(Body,R) |
2580 | | ). |
2581 | | |
2582 | | % -------------------------------------------------------- |
2583 | | % integer expressions |
2584 | | % -------------------------------------------------------- |
2585 | | |
2586 | | % -------------------------------------------------------- |
2587 | | |
2588 | | evaluate_int_argument(A,Res) :- evaluate_int_argument(A,Res,no_loc_info_available). |
2589 | | |
2590 | | :- block evaluate_int_argument(-,?,?). |
2591 | | |
2592 | | evaluate_int_argument(int(X),R,_) :- !, R=X. |
2593 | | evaluate_int_argument(agent_call(Span,F,Par),R,Span) :- !, /* in this context we need the result of the function call */ |
2594 | | unfold_function_call_once(F,Par,Body,Span), |
2595 | | %print(unfolded(F,Par,Body)),nl, |
2596 | | evaluate_int_argument(Body,R,Span). |
2597 | | evaluate_int_argument(Expr,IntRes,Span) :- |
2598 | | force_evaluate_argument(Expr,Res), % because we need an integer, i.e., agent_calls need to be unfolded |
2599 | | (Res = int(IntRes) -> true |
2600 | | ; (Res \= int(_), add_error(haskell_csp,'Expression does not evaluate to integer: ','='(Expr,Res),Span), |
2601 | | fail) |
2602 | | ). |
2603 | | |
2604 | | :- block evaluate_list(-,?). |
2605 | | evaluate_list([],R) :- !,R=[]. |
2606 | | evaluate_list([H|T],R) :- !, R=[EH|ET],evaluate_argument(H,EH), evaluate_list(T,ET). |
2607 | | evaluate_list(X,R) :- add_internal_error('Internal Error: Could not evaluate: ',evaluate_list(X,R)),R=X. |
2608 | | |
2609 | | :- block evaluate_type_list(-,?). |
2610 | | evaluate_type_list([],R) :- !,R=[]. |
2611 | | evaluate_type_list([H|T],R) :- !, R=[EH|ET], |
2612 | ? | translate_to_type_expr(H,TypeH), |
2613 | ? | evaluate_argument(TypeH,EH), |
2614 | | evaluate_type_list(T,ET). |
2615 | | evaluate_type_list(X,R) :- |
2616 | | add_internal_error('Internal Error: Could not evaluate: ',evaluate_type_list(X,R)),R=X. |
2617 | | |
2618 | | translate_to_type_expr(tupleExp(TupleArgs),R) :- !, |
2619 | | R = typeTuple(TupleArgsRes), |
2620 | | compile_tuple_args(TupleArgs,TupleArgsRes). |
2621 | | translate_to_type_expr(dotTuple(TupleArgs),R) :- !, |
2622 | | R = dotTupleType(TupleArgsRes), |
2623 | | compile_tuple_args(TupleArgs,TupleArgsRes). |
2624 | | translate_to_type_expr(X,CX) :- |
2625 | ? | haskell_csp_analyzer:compile_body(X,'compile_tuple_args',[],[],CX). |
2626 | | |
2627 | | compile_tuple_args([],R) :- !,R=[]. |
2628 | | compile_tuple_args([H|T],R) :- !, |
2629 | | R=[CH|RH], |
2630 | | haskell_csp_analyzer:compile_body(H,'compile_tuple_args',[],[],CH), |
2631 | | compile_tuple_args(T,RH). |
2632 | | |
2633 | | % ----------------------------------------------------- |
2634 | | |
2635 | | |
2636 | | |
2637 | | |
2638 | | force_evaluate_list(L,_EL) :- %print(force_evaluate_list(L,_EL)),nl, |
2639 | | var(L),!, add_error(haskell_csp,'Trying to force evaluation of variable: ',L),fail. |
2640 | | force_evaluate_list([],R) :- !,R=[]. |
2641 | | force_evaluate_list([H|T],R) :- !, R=[EH|ET], |
2642 | ? | force_evaluate_argument(H,EH), %force_evaluate_argument(H,EH), |
2643 | ? | force_evaluate_list(T,ET). |
2644 | | force_evaluate_list(X,R) :- |
2645 | | add_internal_error('Could not (force) evaluate list: ',force_evaluate_list(X,R)),R=X. |
2646 | | |
2647 | | unfold_function_call_curry_once(F,[],F,_Span). |
2648 | | unfold_function_call_curry_once(F,[Args|As],Value,Span) :- |
2649 | | unfold_function_call_once(F,Args,Val,Span),!, |
2650 | | % Val is a lambda-function |
2651 | | unfold_function_call_curry_once(Val,As,Value,Span). |
2652 | | |
2653 | | unfold_function_call_once(F,Par,Res,Span) :- |
2654 | | evaluate_function_name(F,EF), |
2655 | ? | unfold_function_call_once2(EF,Par,Res,Span). |
2656 | | |
2657 | | unfold_function_call_once2(lambda(Args,Body),Parameters,R,Span) :- !, |
2658 | | %print(unfold_lambda(Args,Parameters,Body,R)),nl, |
2659 | | % varnumbers(lambda(Args,Body),lambda(CA,CB)), /* lift the frozen parameter-vars back to real-variables; we should only lift variables in Args ! */ |
2660 | | lift(Args,CA,Body,CB), |
2661 | | % print(lifted_lambda(CA,CB)),nl, |
2662 | | evaluate_lambda_arguments(Parameters,CA,EvalParas), |
2663 | | (CA=EvalParas -> R = CB |
2664 | | ; add_error(cspm_trans,'Could not unify lambda args: ', lambda(CA,Parameters,body(Body)),Span),fail). |
2665 | | unfold_function_call_once2(FunName,Parameters,R,Span) :- %print(unfold(FunName,Parameters)),nl, |
2666 | ? | evaluate_agent_call_parameters(FunName,Parameters,EvalParas,Span), |
2667 | | %%print(call_agent_compiled(FunName,Parameters,EX)),nl, |
2668 | | call_agent_compiled(FunName,Parameters,EvalParas,R,Span). |
2669 | | |
2670 | | :- block call_agent_compiled(-,?,?,?,?),call_agent_compiled(?,?,-,?,?). |
2671 | | call_agent_compiled(FunCall,_,[],Res,Span) :- !, % no parameters |
2672 | | call_agent_compiled2(FunCall,Res,Span). |
2673 | | call_agent_compiled(FunName,_Parameters,EvalParas,Res,Span) :- |
2674 | | EX =.. [FunName|EvalParas], |
2675 | | (ground(EvalParas) -> call_agent_compiled2(EX,Res,Span) |
2676 | | ; %print(not_ground_call(FunName,Parameters,EvalParas)),nl, %typechecker:debug_non_ground_term(EX), |
2677 | | is_nonvar_list_skel(EvalParas,OK), % was when(ground(EX),...) |
2678 | | call_agent_compiled1(EX,Res,OK,Span) |
2679 | | ). |
2680 | | :- block is_nonvar_list_skel(-,?). |
2681 | | %is_nonvar_list_skel([],true). % clause not coverable, [] is always ground (see ground(EvalParas) -> .. in the body of last clause of call_agent_compiled/5) |
2682 | | is_nonvar_list_skel([H|T],R) :- is_nonvar_list_skel(T,H,R). |
2683 | | :- block is_nonvar_list_skel(-,?,?),is_nonvar_list_skel(?,-,?). |
2684 | | is_nonvar_list_skel([],_,true). |
2685 | ? | is_nonvar_list_skel([H|T],_,R) :- is_nonvar_list_skel(T,H,R). |
2686 | | |
2687 | | :- block call_agent_compiled1(?,?,-,?). |
2688 | ? | call_agent_compiled1(EX,Res,_,Span) :- call_agent_compiled2(EX,Res,Span). |
2689 | | |
2690 | | call_agent_compiled2(EX,Res,Span) :- |
2691 | ? | (agent_compiled(EX,Value,_SRCSPAN) |
2692 | | -> %print(unfolded(Value,Res,EX)),nl, |
2693 | | %(EX='OZS@__25'(_,_) -> trace ; true), |
2694 | | Res=Value /* local cut imposes functional interpetation */ |
2695 | | ; functor(EX,F,N), functor(Skel,F,N), |
2696 | | (is_defined_agent(Skel) -> add_cspm_error(cspm_trans,'No matching case for function call: ',EX,Span) |
2697 | | ; add_cspm_error(cspm_trans,'Trying to apply undefined process/function: ',EX,Span)), |
2698 | | fail |
2699 | | ). |
2700 | | |
2701 | | safe_is(X,Expr) :- when(ground(Expr), X is Expr). |
2702 | | |
2703 | | add_cspm_error(Source,Msg,CSPE,Span) :- |
2704 | | (translate_cspm_state(CSPE,Transl) -> true ; Transl=CSPE), |
2705 | | add_error(Source,Msg,Transl,Span). |
2706 | | |
2707 | | /* ------------------------------------- */ |
2708 | | /* Renaming related predicates */ |
2709 | | /* ------------------------------------- */ |
2710 | | |
2711 | | |
2712 | | :- assert_must_succeed(( |
2713 | | retractall(csp_full_type_constructor(_,_,_)), |
2714 | | haskell_csp:rename_action(io([int(1)],left,unknown(test)),[rename(right,left),rename(left,mid)],Res), |
2715 | | Res== io([int(1)],mid,unknown(test)) )). |
2716 | | :- assert_must_succeed(( |
2717 | | retractall(csp_full_type_constructor(_,_,_)), |
2718 | | haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(right,left),rename(left,mid)],Res), |
2719 | | Res== io([int(1)],ack,unknown(test)) )). |
2720 | | :- assert_must_succeed(( |
2721 | | retractall(csp_full_type_constructor(_,_,_)), |
2722 | | haskell_csp:rename_action(io([int(1)],right,unknown(test)),[rename(ack,right),rename(right,dotTuple([mid,int(2)]))],Res), |
2723 | | Res== io([int(2),int(1)],mid,unknown(test)) )). |
2724 | | :- assert_must_succeed(( |
2725 | | retractall(csp_full_type_constructor(_,_,_)), |
2726 | | haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(ack,left),rename(ack,right)],Res), |
2727 | | Res== io([int(1)],left,unknown(test)) )). |
2728 | | :- assert_must_succeed(( |
2729 | | retractall(csp_full_type_constructor(_,_,_)), |
2730 | | haskell_csp:rename_action(io([int(1)],ack,unknown(test)),[rename(ack,left),rename(ack,right)],Res), |
2731 | | Res== io([int(1)],right,unknown(test)) )). |
2732 | | % :- assert_must_succeed(( |
2733 | | % haskell_csp:haskell_csp:rename_action(io([int(0)],gen,unknown(test)), |
2734 | | % [rename(gen,gen1),rename(gen,dotTuple([gen2,int(1)])), |
2735 | | % rename(dotTuple([gen,int(0)]),dotTuple([gen2,int(9),int(9)])), |
2736 | | % rename(stop(no_loc_info_available),dotTuple([gen2,int(2)+int(3)]))],R), |
2737 | | % R == io([int(1),int(0)],gen2,unknown(test)) )). |
2738 | | |
2739 | | :- block rename_action(-,?,-). |
2740 | | rename_action(tick(TS),_,tick(TS)). |
2741 | | rename_action(tau(X),_,tau(X)). |
2742 | | rename_action(io(V,Ch,Span),RenamePatternList,Res) :- Res=io(_,_,_), |
2743 | ? | match_pattern_list(RenamePatternList,V,Ch,Span,Res,false). |
2744 | | |
2745 | | force_rename_action(io(V,Ch,Span),RenamePatternList,Res) :- /* as above; but renaming must occur */ |
2746 | ? | match_pattern_list(RenamePatternList,V,Ch,Span,Res,true). % true: means MatchOccured: not allowed to not rename |
2747 | | |
2748 | | %not_renamed(tick(_),_). % case cannot occur, functor_dif(AX,tick) is always called before the not_renamed/2 predicate |
2749 | | not_renamed(tau(_X),_). |
2750 | | not_renamed(io(V,Ch,_Span),RenamePatternList) :- |
2751 | ? | not_covered_action(RenamePatternList,V,Ch). |
2752 | | |
2753 | | not_covered_action([],_,_). |
2754 | | not_covered_action([rename(ChPat,_NewCh)|T],V,Ch) :- |
2755 | | (ChPat= tuple([Ch2|TPat2]) %dotTuple([Ch2|T2]) |
2756 | | -> (dif(Ch,Ch2) ; Ch=Ch2,no_match_list(TPat2,V))%,print(nca_dif(V,T2)),nl |
2757 | | ; dif(Ch,ChPat) |
2758 | ? | ), not_covered_action(T,V,Ch). |
2759 | | |
2760 | | :- assert_must_succeed(( haskell_csp:no_match_list([int(1)],[int(2)]) )). |
2761 | | :- assert_must_succeed(( haskell_csp:no_match_list([int(2)],[int(1),int(2)]) )). |
2762 | | :- assert_must_fail(( haskell_csp:no_match_list([],[int(1),int(2)]) )). |
2763 | | :- assert_must_fail(( haskell_csp:no_match_list([int(2),int(3)],[int(2),int(3)]) )). |
2764 | | %% :- assert_must_fail(( haskell_csp:no_match_list([out(int(2)),out(int(3))],[int(2),int(3)]) )). |
2765 | | :- assert_must_succeed(( haskell_csp:no_match_list(X,[int(2),int(1)]), |
2766 | | X=[int(2),int(2)])). |
2767 | | |
2768 | | % check if a rename pattern matches a value on a channel: |
2769 | | no_match_list(RenPattern,ChValue) :- % print(no_match_list(A,B)),nl, |
2770 | | l_match_pattern_value(RenPattern,ChValue,match_false). |
2771 | | |
2772 | | % check if a value matches an entry in the ChannelPatternList |
2773 | | match_list(ChannelPatternList,V,Ch,Span) :- |
2774 | | match_pattern_list(ChannelPatternList,V,Ch,Span,true,true). |
2775 | | |
2776 | | :- block match_pattern_value(-,?,?), match_pattern_value(?,-,?). |
2777 | | match_pattern_value(record(C,PatArgs),record(VC,ValArgs),Res) :- !, |
2778 | | match_record(C,PatArgs,VC,ValArgs,Res). |
2779 | | match_pattern_value(tuple(L1),tuple(L2),Res) :- !, |
2780 | | l_match_pattern_value(L1,L2,Res). |
2781 | | match_pattern_value(X,tuple([H|Rest]),Res) :- !,(H=X -> Res = match_true(Rest); Res=match_false). |
2782 | | match_pattern_value(X,dotTuple([H|Rest]),Res) :- !,(H=X -> Res = match_true(Rest); Res=match_false). |
2783 | | match_pattern_value(X,record([X|Rest]),Res) :- !, Res = match_true(Rest). |
2784 | | match_pattern_value(Pat,Val,Res) :- |
2785 | | when(?=(Pat,Val),(unify_check(Pat,Val) |
2786 | | -> Res=match_true([]) ; Res=match_false)). |
2787 | | |
2788 | | unify_check(int(V1),I2) :- !, |
2789 | | (I2=int(V2) -> V1=V2 |
2790 | | %; preference(use_clpfd_solver,true), number(I2) -> V1 = I2 |
2791 | | ; add_internal_error('Type error in unification of values: ',unify_check(int(V1),I2)),fail). |
2792 | | unify_check(true,I2) :- !, |
2793 | | (I2=true -> true ; I2=false -> fail |
2794 | | ; add_internal_error('Type error in unification of values: ',unify_check(true,I2)),fail). |
2795 | | unify_check(false,I2) :- !, |
2796 | | (I2=false -> true ; I2=true -> fail |
2797 | | ; add_internal_error('Type error in unification of values: ',unify_check(false,I2)),fail). |
2798 | | unify_check(V,V). |
2799 | | |
2800 | | |
2801 | | |
2802 | | :- block match_record(-,?,?,?,?), match_record(?,?,-,?,?). |
2803 | | match_record(C1,_,C2,_,Res) :- C1\=C2,!, Res=match_false. |
2804 | | match_record(C,PatArgs,C,ValArgs,Res) :- l_match_pattern_value(PatArgs,ValArgs,Res). |
2805 | | |
2806 | | :- block l_match_pattern_value(-,?,?). |
2807 | | l_match_pattern_value(vclosure,_T,R) :- !, R=match_true(vclosure). |
2808 | | l_match_pattern_value([],T,R) :- !, R=match_true(T). |
2809 | | l_match_pattern_value([H|T],Y,R) :- !, l_match_pattern_value1(Y,H,T,R). |
2810 | | l_match_pattern_value(I,V,R) :- |
2811 | | add_internal_error('Could not evaluate: ',l_match_pattern_value(I,V,R)),fail. |
2812 | | |
2813 | | :- block l_match_pattern_value1(-,?,?,?). |
2814 | | l_match_pattern_value1([],H,T,R) :- !, add_error(haskell_csp,'Too many values in rename pattern: ',[H|T]), R=match_false. |
2815 | | l_match_pattern_value1([IODVal|IT],Pat,TPat,R) :- !, |
2816 | | get_value_alsoPat(IODVal,PV), |
2817 | | match_pattern_value(Pat,PV,Res), |
2818 | | % print(matched(Pat,PV,Res,TPat,IT)),nl, % |
2819 | | l_match_pattern_value2(Res,TPat,IT,R). |
2820 | | |
2821 | | :- block l_match_pattern_value2(-,?,?,?). |
2822 | | l_match_pattern_value2(match_true(M),TailPat,TailValue,Res) :- |
2823 | | ((TailPat=[],TailValue==[]) -> Res=match_true(M) % avoid error message in conjoin |
2824 | | ; TailPat=vclosure -> Res = match_true([]) % ignore match M; |
2825 | | % there could be strange pattern match, but |
2826 | | % it can happen that a partial record was provided (e.g., [|{|c_s.c_picks, in philosophers.csp) |
2827 | | ; (is_list(M),M\=[]) -> % one of the list arguments was a tuple, we need to pattern match the rest of the tuple arguments |
2828 | | append(TailValue,M,TailValue1), |
2829 | | l_match_pattern_value(TailPat,TailValue1,Res) |
2830 | | ; |
2831 | | l_match_pattern_value(TailPat,TailValue,RT), % print(conjoin(RT,match_true(M),Res)),nl, |
2832 | | conjoin_match(RT,match_true(M),Res)). |
2833 | | l_match_pattern_value2(match_false,_,_,match_false). |
2834 | | |
2835 | | :- block get_value_alsoPat(-,?). |
2836 | | get_value_alsoPat(X,Res) :- |
2837 | | get_value(X,R), |
2838 | | (nonvar(R),R=alsoPat(V1,_V2) -> Res=V1 ; Res=R). |
2839 | | |
2840 | | :- block conjoin_match(-,?,?), conjoin_match(?,-,?). |
2841 | | conjoin_match(match_false,_,match_false). |
2842 | | conjoin_match(match_true(_T),match_false,match_false). |
2843 | | conjoin_match(match_true(T1),match_true(T2),Res) :- %append(T1,T2,TT). |
2844 | | (T2==[] -> Res=match_true(T1) /* note T2: is the first match, T1 the later one */ |
2845 | | ; T2==vclosure -> Res=match_true(T1) /* vclosure can propagate to the next level up */ |
2846 | | ; conjoin_error(T2,T1,ResMatch), Res=match_true(ResMatch)). |
2847 | | |
2848 | | % note: records (for example) are gradually enumerated; hence delay error message until we know the value of the inner match |
2849 | | % check if we have a pattern match like rec.a.?.b.? -> this cannot be handled by us nor by FDR |
2850 | | :- block conjoin_error(-,?,?). |
2851 | | conjoin_error([],T1,M) :- !, M=T1. |
2852 | | conjoin_error(vclosure,T1,M) :- !, M=T1. |
2853 | | conjoin_error(T2,T1,T1) :- add_error(conjoin_match,'Rename pattern is incomplete in the middle. Ignoring first match: ',T2:T1). |
2854 | | |
2855 | | :- assert_must_succeed(( |
2856 | | haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)|vclosure])],[in(X),in(dotTuple([Y,Z]))],a,span,true,true), |
2857 | | X=int(0), Y=int(0), Z=int(2))). |
2858 | | :- assert_must_succeed(( |
2859 | | haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)|vclosure])],[in(X),in(Y)],a,span,true,true), |
2860 | | X=int(0), Y=tuple([int(0),int(2)]))). |
2861 | | :- assert_must_succeed(( |
2862 | | haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)]),tuple([d|vclosure])],[in(X),in(Y)],a,span,true,true), |
2863 | | X=int(0), Y=tuple([int(0),int(2)]))). |
2864 | | :- assert_must_fail(( |
2865 | | haskell_csp:match_pattern_list([tuple([a,int(0),int(0),int(2)]),tuple([c,int(0)|vclosure]),tuple([d|vclosure])],[in(X),in(Y)],a,span,true,true), |
2866 | | X=int(0), Y=tuple([int(0),int(3)]))). |
2867 | | :- assert_must_fail(( |
2868 | | haskell_csp:match_pattern_list([tuple([c,int(0)|vclosure]),tuple([d|vclosure]),tuple([a,int(0),int(0),int(2)])],[in(X),in(Y)],a,span,true,true), |
2869 | | X=int(0), Y=tuple([int(0),int(3),int(2)]))). |
2870 | | |
2871 | | % match_pattern_list(PatOrRenameList, Value,Channel,Span, Rename/MatchResult, HasMatchAlreadyOccured) |
2872 | | match_pattern_list([],V,Ch,Span,io(V,Ch,SpanV),MatchOccured) :- %print(no_match(V,Ch,MatchOccured)),nl, |
2873 | | set_span(SpanV,Span,match_pattern_list(Ch,V)), |
2874 | | MatchOccured=false. % only allow unrenamed action if no match occured earlier |
2875 | | match_pattern_list([rename(ChPat,NewCh)|T],V,Ch,Span,Res,MatchOccured) :- !, |
2876 | | % print(checking_pat_match(ChPat,Ch,V)),nl, %% |
2877 | | match_pattern_value(ChPat,tuple([Ch|V]),MatchRes), |
2878 | ? | rename_action3(MatchRes,T,NewCh,V,Ch,Span,Res,MatchOccured). |
2879 | | match_pattern_list([ChPat|T],V,Ch,Span,Res,MatchOccured) :- % for aParallel |
2880 | | % print(checking_pat_match(ChPat,Ch,V)),nl, %% |
2881 | | match_pattern_value(ChPat,tuple([Ch|V]),MatchRes), |
2882 | | pat_match_action3(MatchRes,T,V,Ch,Span,Res,MatchOccured). |
2883 | | |
2884 | | :- block pat_match_action3(-, ?,?,?,?, ?,?). |
2885 | | pat_match_action3(match_true(Rest), _T, _V,_Ch,_Span, Res,_MatchOccured) :- |
2886 | | (Rest=[] -> Res=true ; Rest=vclosure -> Res=true). % when doing a pat_match: we only allow full matches |
2887 | | %pat_match_action3(match_true(_),T,V,Ch,Span,Res,_) :- match_pattern_list(T,V,Ch,Span,Res,true). |
2888 | | pat_match_action3(match_false,T,V,Ch,Span,Res,MatchOccured) :- match_pattern_list(T,V,Ch,Span,Res,MatchOccured). |
2889 | | |
2890 | | :- block rename_action3(-, ?,?, ?,?,?, ?,?). |
2891 | | rename_action3(match_true(Rest), _T,NewCh, _V,_Ch,Span, Res,_MatchOccured) :- |
2892 | | r_compose(NewCh,Rest,Span,Res). |
2893 | ? | rename_action3(match_true(_),T,_NewCh,V,Ch,Span,Res,_) :- match_pattern_list(T,V,Ch,Span,Res,true). |
2894 | ? | rename_action3(match_false,T,_NewCh,V,Ch,Span,Res,MatchOccured) :- match_pattern_list(T,V,Ch,Span,Res,MatchOccured). |
2895 | | |
2896 | | r_compose(NewCh,Rest,Span,io(VRes,ResultingChannel,VSpan)) :- |
2897 | | set_span(VSpan,Span,r_compose(NewCh)), |
2898 | | %% print(rename_match(NewCh,Rest)),nl, %% |
2899 | | evaluate_argument(dotTuple([NewCh|Rest]), ResultTuple), |
2900 | | (ResultTuple = tuple([TCh|TV]) |
2901 | | -> ResultingChannel=TCh,VRes=TV |
2902 | | ; add_internal_error('Illegal result tuple: ', evaluate_argument(dotTuple([NewCh|Rest]), ResultTuple)), |
2903 | | ResultingChannel=NewCh, VRes=Rest |
2904 | | ). |
2905 | | |
2906 | | |
2907 | | evaluate_rename_list([],[]). |
2908 | | evaluate_rename_list([rename(X,Y)|T],[rename(EX,EY)|ET]) :- |
2909 | | evaluate_rename_channel_expression(X,EX), |
2910 | | evaluate_rename_channel_expression(Y,EY), |
2911 | | evaluate_rename_list(T,ET). |
2912 | | |
2913 | | evaluate_link_list('linkList'(L),R) :- !,evaluate_link_list2(L,R). |
2914 | | evaluate_link_list('linkListComp'(GeneratorList,LinkList),R) :- !, |
2915 | | %print(procCompLinkList(GeneratorList,LinkList)),nl, |
2916 | | % warning: LinkList does not have the rangeEnum wrapper expected |
2917 | | expand_set_comprehension(rangeEnum(LinkList),GeneratorList,setValue(ExpandedLinks)), |
2918 | | evaluate_link_list2(ExpandedLinks,R). |
2919 | | evaluate_link_list(LL,R) :- |
2920 | | add_internal_error('Cannot evaluate for Linked Parallel: ',evaluate_link_list(LL,R)),fail. |
2921 | | |
2922 | | evaluate_link_list2([],[]). |
2923 | | evaluate_link_list2([link(X,Y)|T],[rename(EX,EY)|ET]) :- /* note: link becomes rename */ |
2924 | | evaluate_rename_channel_expression(X,EX), |
2925 | | evaluate_rename_channel_expression(Y,EY), |
2926 | | evaluate_link_list2(T,ET). |
2927 | | |
2928 | | rev_rename_list([],[]). |
2929 | | rev_rename_list([rename(X,Y)|T],[rename(Y,X)|RT]) :- rev_rename_list(T,RT). |
2930 | | |
2931 | | |
2932 | | evaluate_rename_channel_expression(E,RE) :- evaluate_argument(E,RE). |
2933 | | % (E=dotTuple([CH|V]) |
2934 | | % -> (RE=dotTuple([CH|EV]), |
2935 | | % l_evaluate_arguments(V,EV)) |
2936 | | % ; RE=E |
2937 | | % ). |
2938 | | |
2939 | | %%%%%%%%% DEAD CODE %%%%%%%%%%%% |
2940 | | /* |
2941 | | get_renamelist_range([],[]). |
2942 | | get_renamelist_range([rename(_X,Y)|T],[Y|DT]) :- |
2943 | | get_renamelist_range(T,DT). |
2944 | | */ |
2945 | | |
2946 | | /* ------------------------------------- */ |
2947 | | |
2948 | | /* hidden(Action, ChannelPatternList) */ |
2949 | | /* check whether an Action is covered by a CSP Channel Pattern List */ |
2950 | | |
2951 | | hidden(tau(_),_) :- fail. |
2952 | | hidden(tick(_),_) :- fail. |
2953 | | hidden(io(V,Ch,Span), ChannelPatternList) :- match_list(ChannelPatternList,V,Ch,Span). |
2954 | | |
2955 | | /* same as hidden but allows tau; useful for alphab. parallel */ |
2956 | | :- block hidden_or_tau(-,?). |
2957 | | hidden_or_tau(tau(_),_). |
2958 | | hidden_or_tau(tick(_),_) :- fail. |
2959 | | hidden_or_tau(io(V,Ch,Span), ChannelPatternList) :- match_list(ChannelPatternList,V,Ch,Span). |
2960 | | |
2961 | | |
2962 | | expand_channel_pattern_expression(X,_,SrcSpan) :- |
2963 | | % nl,print(expand_channel_pattern_expression(X)),nl, |
2964 | | var(X), !, |
2965 | | add_error(haskell_csp,'VARIABLE in expand_channel_pattern_expression: ',X,SrcSpan),fail. |
2966 | | expand_channel_pattern_expression(agent_call(Span,F,Par),Res,SrcSpan) :- !, |
2967 | | unfold_function_call_once(F,Par,Body,Span), expand_channel_pattern_expression(Body,Res,SrcSpan). |
2968 | | expand_channel_pattern_expression(setValue(List),EList,SrcSpan) :- !,l_expand(List,EList,SrcSpan). |
2969 | | expand_channel_pattern_expression(closure(List),EList,_SrcSpan) :- !, |
2970 | | %print(haskell_csp:l_cexpand(List,EList)),nl, |
2971 | | l_cexpand(List,EList). |
2972 | | %% this two clauses are already computed by expanding the setValue(-) and closure(-) predicates above (DEAD CODE) |
2973 | | /* expand_channel_pattern_expression([],R,_SrcSpan) :- !, R=[]. */ /* already computed */ |
2974 | | /*expand_channel_pattern_expression([tuple([C|T])|T2],R,SrcSpan) :- !,*/ /* already computed */ |
2975 | | /* (check_channel_value_is_complete(C,T,SrcSpan) |
2976 | | -> R=[tuple([C|T])|R2] ; R=R2), |
2977 | | expand_channel_pattern_expression(T2,R2,SrcSpan). |
2978 | | */ |
2979 | | expand_channel_pattern_expression(Exp,_,SrcSpan) :- |
2980 | | add_error(haskell_csp,'Unknown expand_channel_pattern_expression: ',Exp,SrcSpan),fail. |
2981 | | |
2982 | | /* translate a list of channel pattern expr. into uniform format */ |
2983 | | l_expand(X,R,SrcSpan) :- var(X), |
2984 | | add_internal_error_with_span(haskell_csp,'Variable List for l_expand',X,SrcSpan), R=[]. |
2985 | | l_expand(List,Res,SrcSpan) :- |
2986 | | convlist(expand_1(SrcSpan),List,Res). |
2987 | | |
2988 | | expand_1(SrcSpan,El,R) :- |
2989 | | expand(El,R,SrcSpan),!. |
2990 | | |
2991 | | /* |
2992 | | l_expand([],[],_). |
2993 | | l_expand([H|T],Res,SrcSpan) :- |
2994 | | (expand(H,EH,SrcSpan)->Res=[EH|ET];Res=ET), |
2995 | | l_expand(T,ET,SrcSpan). |
2996 | | */ |
2997 | | |
2998 | | expand(tuple([Ch|List]),R,SrcSpan) :- !,R=tuple([Ch|List]), |
2999 | | check_channel_value_is_complete(Ch,List,SrcSpan). |
3000 | | expand(Channel,R,SrcSpan) :- |
3001 | | (atomic(Channel) -> R=tuple([Channel]) |
3002 | | ; add_error(haskell_csp,'Non-atomic argument: ',expand(Channel,R,SrcSpan)),fail). |
3003 | | |
3004 | | check_channel_value_is_complete(Ch,List,SrcSpan) :- |
3005 | | (channel_type_list(Ch,ChannelTypes) |
3006 | | -> |
3007 | | (same_length(ChannelTypes,List) -> true |
3008 | | ; length(ChannelTypes,CL), length(List,L), |
3009 | | (CL>L -> add_error(check_channel_value,'Incomplete event: ','.'(Ch,List),SrcSpan) |
3010 | | ; add_error(check_channel_value,'Too many values for event: ','.'(Ch,List),SrcSpan) |
3011 | | ), fail |
3012 | | ) |
3013 | | ; add_error(haskell_csp,'Undefined channel: ','.'(Ch,List),SrcSpan),fail |
3014 | | ). |
3015 | | |
3016 | | |
3017 | | /* translate a list of channel pattern expr. into uniform format and add closure at end of list */ |
3018 | | l_cexpand(X,R) :- var(X), add_error(l_cexpand,'Variable List',X), R=[]. |
3019 | | l_cexpand(L,EL) :- maplist(cl_expand,L,EL). |
3020 | | |
3021 | | % what about pat(_,_) |
3022 | | cl_expand(tuple([Ch|List]),R) :- !, R = tuple([Ch|EL]),append_vclosure(List,EL). %, print(app_vcl(Ch,List,EL)),nl. |
3023 | | cl_expand(Channel,R) :- |
3024 | | (atomic(Channel) -> R = tuple([Channel|vclosure]) |
3025 | | ; add_error(haskell_csp, 'Non-atomic argument: ',cl_expand(Channel,R)),fail). |
3026 | | |
3027 | | |
3028 | | append_vclosure([record(X,Fields)],Res) :- incomplete_record(record(X,Fields),[_|_],_),!, |
3029 | | Res = [record(X,EFields)|vclosure], |
3030 | | append_vclosure(Fields,EFields). |
3031 | | append_vclosure([],vclosure). |
3032 | | append_vclosure([H|T],[H|VT]) :- append_vclosure(T,VT). |
3033 | | |
3034 | | |
3035 | | /* not_hidden(Action, ChannelPatternList) */ |
3036 | | /* check whether an Action is *not* covered by a CSP Channel Pattern List */ |
3037 | | |
3038 | | /* not_hidden_test(io(tail_in(X),outf), |
3039 | | [pat([int(2)],outf),pat([int(3)],outf),pat([int(8)],outf)]) */ |
3040 | | |
3041 | | :- block not_hidden(-,?). |
3042 | | not_hidden(tau(_),_). |
3043 | | not_hidden(tick(_),_). |
3044 | | not_hidden(io(V,Ch,Span),ChannelPatternList) :- % print(not_hidden_test(V,Ch,ChannelPatternList)),nl, % |
3045 | | %not_hidden_test(ChannelPatternList,V,Ch,Span). |
3046 | | match_pattern_list(ChannelPatternList,V,Ch,Span,io(_,_,_),false). % Result is true in case match occurs with list |
3047 | | |
3048 | | |
3049 | | /* ------------------------------------- */ |
3050 | | |
3051 | | :- block get_value(-,?). |
3052 | | |
3053 | | get_value(in(V),R) :- !,R=V. |
3054 | | get_value(out(V),R) :- !, add_internal_error('Obsolete out: ',get_value(out(V),R)), R=V. |
3055 | | get_value(dot(V),R) :- !, add_internal_error('Obsolete dot: ',get_value(out(V),R)), R=V. |
3056 | | get_value(record(Constructor,Fields),R) :- !, R = record(Constructor,ValueFields), |
3057 | | l_get_value(Fields,ValueFields). |
3058 | | get_value(V,V). |
3059 | | |
3060 | | :- block l_get_value(-,?). |
3061 | | l_get_value(L,VL) :- maplist(get_value,L,VL). |
3062 | | |
3063 | ? | valid_constant(X) :- atomic(X), (csp_constant(X,_) -> true ; fail). |
3064 | | |
3065 | | |
3066 | | /* ------------------------------------------ */ |
3067 | | /* SPAN Utilities */ |
3068 | | /* ------------------------------------------ */ |
3069 | | |
3070 | | %%%%%%%%%%%%%%%%%%%%% UNIT TESTS FOR THE SPAN UTILITIES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
3071 | | :- assert_must_succeed((haskell_csp: extract_span_info(_S,Info),Info == [])). |
3072 | | :- assert_must_succeed((haskell_csp: extract_span_info(span_info(info,src_span(3,9,3,12,45,3)),R),R == [info])). |
3073 | | :- assert_must_succeed((haskell_csp: extract_span_info(src_position(3,9,3,12), R),R == [])). |
3074 | | :- assert_must_succeed((haskell_csp: extract_span_info(src_span(3,9,3,12,45,3), R),R == [])). |
3075 | | :- assert_must_succeed((haskell_csp: extract_span_info(unknown(_), R),R == [])). |
3076 | | :- assert_must_succeed((haskell_csp: extract_span_info(multi_span(3,9,3,12,45,3,span_info(info,src_span(3,9,3,12,45,3))), R), |
3077 | | R == [info])). |
3078 | | :- assert_must_succeed((haskell_csp: extract_span_info(src_span_operator(span_info(info, |
3079 | | src_span(94417,10,94421,21,1496266,98)),src_span(94421,2,94421,4,1496345,2)),R), R == [info])). |
3080 | | :- assert_must_succeed((haskell_csp: extract_span_info(no_loc_info_available,R), R == [])). |
3081 | | |
3082 | | :- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,45,3),S,R),S== src_span(3,9,3,12,45,3), R == src_span(3,9,3,12,45,3))). |
3083 | | :- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,45,3),src_span(4,9,5,16,40,5),R), |
3084 | | R == multi_span(3,9,3,12,45,3,src_span(4,9,5,16,40,5)))). |
3085 | | :- assert_must_succeed((haskell_csp: unify_spans(src_span_operator(src_span(94417,10,94421,21,1496266,98),src_span(94421,2,94421,4,1496345,2)),SP2, R), SP2 == src_span(94421,2,94421,4,1496345,2), |
3086 | | R == src_span_operator(src_span(94417,10,94421,21,1496266,98),src_span(94421,2,94421,4,1496345,2)))). |
3087 | | :- assert_must_succeed((haskell_csp: unify_spans(unknown(_),SP2,R), SP2 == R)). |
3088 | | :- assert_must_succeed((haskell_csp: unify_spans(no_loc_info_available,SP2,R), SP2 == R)). |
3089 | | :- assert_must_succeed((haskell_csp: unify_spans(src_span(3,9,3,12,12,3), no_loc_info_available,R), R == src_span(3,9,3,12,12,3))). |
3090 | | :- assert_must_succeed((haskell_csp: unify_spans(span_info(info,src_span(3,9,3,12,45,3)),src_span(3,9,3,12,45,3),R), |
3091 | | R == span_info(info,src_span(3,9,3,12,45,3)))). |
3092 | | :- assert_must_succeed((haskell_csp: unify_spans(src_position(3,9,3,12),src_span(4,9,4,15,45,6),R), |
3093 | | R == multi_span(3,9,3,21,3,12,src_span(4,9,4,15,45,6)))). |
3094 | | :- assert_must_succeed((extract_span_from_event2(start_cspm_MAIN,SPAN, start_cspm_MAIN,_), SPAN == src(3,1,3,5,20,4))). |
3095 | | :- assert_must_succeed((extract_span_from_event2(start_cspm('REC'),SPAN,start_cspm('REC'),_), SPAN == src(8,1,8,4,4,3))). |
3096 | | :- assert_must_fail((extract_span_from_event(_X,_Span,_T,_NS))). |
3097 | | :- assert_must_succeed((extract_span_info(src_position(_,_,_,_),R1), R1 ==[], extract_span_info(unknown(_),R2), R2 ==[])). |
3098 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
3099 | | |
3100 | | % span can already be set: |
3101 | | % problem: rename_action in eprocRenaming has to instantiate Span; in other contexts hidden should not instantiate span |
3102 | | set_span(SpanVar,SpanValue,PP) :- nonvar(SpanVar),!, |
3103 | | debug_println(9,span_already_set(PP,SpanValue)). |
3104 | | % print('*** Span already set to: '), print(SpanVar),nl, |
3105 | | % print('*** tried to assign value: '),print(SpanValue),nl,print('*** Context: '), print(PP),nl. |
3106 | | set_span(S,S,_C). % :- print(setting_span(S,_C)),nl. |
3107 | | |
3108 | | extract_span_info(Span,Info) :- var(Span),!,Info=[]. |
3109 | | extract_span_info(span_info(Info,Span),[Info|T]) :- extract_span_info(Span,T). |
3110 | | extract_span_info(src_position(_,_,_,_),[]). |
3111 | | extract_span_info(src_span(_,_,_,_,_,_),[]). |
3112 | | extract_span_info(src_span_operator(WholeSP1,_JustOperatorSP2),T) :- extract_span_info(WholeSP1,T). |
3113 | | extract_span_info(unknown(_),[]). |
3114 | | extract_span_info(multi_span(_,_,_,_,_,_,SP1),T) :- extract_span_info(SP1,T). |
3115 | | extract_span_info(no_loc_info_available,[]). |
3116 | | |
3117 | | :- block unify_spans(-,?,?). |
3118 | | %unify_spans(S,_,R) :- !,R=S. % commenting this in gains 10 % performance, e.g., on crossing.csp benchmark |
3119 | | unify_spans(SP1,SP2,R) :- ( unify_spans1(SP1,SP2,R) -> true |
3120 | | ; add_internal_error('Failed: ',unify_spans(SP1,SP2,R)),set_span(SP1,R,unify_spans)). |
3121 | | :- block unify_spans1(-,?,?). |
3122 | | unify_spans1(SP1,SP2,R) :- nonvar(R),!, |
3123 | | debug_println(9,span_already_computed(R,unify_spans(SP1,SP2))). |
3124 | | unify_spans1(span_info(Info,SP1),SP2,R) :- !, R=span_info(Info,RS), |
3125 | | unify_spans1(SP1,SP2,RS). |
3126 | | unify_spans1(src_position(StartLine,SC,OffsetByte,LenBytes),SP2,R) :- number(SC), number(LenBytes),!, |
3127 | | EndLine = StartLine, EC is SC+LenBytes, |
3128 | | gen_multi_span(SP2, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R). |
3129 | | unify_spans1(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R) :- !, |
3130 | | unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R). |
3131 | | unify_spans1(src_span_operator(SP1,SP2),SP3,R) :- !, R=src_span_operator(SP1,SP23), |
3132 | | unify_spans1(SP2,SP3,SP23). |
3133 | | unify_spans1(multi_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes,SP1),SP2,R) :- !, |
3134 | | unify_spans1(SP1,SP2,TailS), |
3135 | | gen_multi_span(TailS, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R). |
3136 | | unify_spans1(unknown(_),S,R) :- !, R=S. |
3137 | | unify_spans1(no_loc_info_available,S,R) :- !, R=S. |
3138 | | unify_spans1(S,_,S) :- add_error(unify_spans1,'Unknown Span: ',S). |
3139 | | |
3140 | | |
3141 | | :- block unify_spans2(-,?,?). |
3142 | | unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),S,R) :- |
3143 | | S=src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),!, R=S. |
3144 | | unify_spans2(src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes),SP2,R) :- !, |
3145 | | gen_multi_span(SP2, StartLine,SC,EndLine,EC,OffsetByte,LenBytes, R). |
3146 | | |
3147 | | |
3148 | | :- block gen_multi_span(-, ?,?,?,?, ?,?,?). |
3149 | | gen_multi_span(no_loc_info_available, StartLine,SC,EndLine,EC, OffsetByte,LenBytes, R) :- !, |
3150 | | R = src_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes). |
3151 | | gen_multi_span(Span2,StartLine,SC,EndLine,EC,OffsetByte,LenBytes,R) :- |
3152 | | R = multi_span(StartLine,SC,EndLine,EC,OffsetByte,LenBytes, Span2),!. |
3153 | | |
3154 | | |
3155 | | :- block merge_span_into_event(?,-,?). |
3156 | | merge_span_into_event(Event,no_loc_info_available,NewEvent) :- !, |
3157 | | NewEvent=Event. |
3158 | | merge_span_into_event(Event,AdditionalSpan,NewEvent) :- |
3159 | | (extract_span_from_event(Event,SPAN,Templ,NewSPAN) |
3160 | ? | -> Templ = NewEvent, unify_spans(SPAN,AdditionalSpan,NewSPAN) |
3161 | | ; (%add_error(merge_span_into_event,'Unknown Event: ',Event), |
3162 | | % sometimes we cannot extract a source span, e.g., tau(repInternalChoice ...) |
3163 | | NewEvent = Event) |
3164 | | ). |
3165 | | |
3166 | | %type_of_event(io( or colour_of_event ... |
3167 | | extract_span_from_event(Event,_Span,_Template,_NewSpan) :- var(Event), |
3168 | | debug_println(9,'### extract_span_from_event variable'),!,fail. |
3169 | | extract_span_from_event(Event,Span,Template,NewSpan) :- process_algebra_mode,!, |
3170 | | extract_span_from_event2(Event,Span,Template,NewSpan). |
3171 | | |
3172 | | %:- block extract_span_from_event2(-,?,?,?). |
3173 | | extract_span_from_event2(start_cspm_MAIN,SPAN,start_cspm_MAIN,_) :- !,get_symbol_span('MAIN',SPAN). |
3174 | | extract_span_from_event2(start_cspm(S),SPAN,start_cspm(S),_) :- !,get_symbol_span(S,SPAN). |
3175 | | extract_span_from_event2(io(Ev,Ch,SPAN),SPAN,io(Ev,Ch,NewSPAN),NewSPAN). |
3176 | | extract_span_from_event2(tau(link(Left,Right)),SPAN,Templ,NS) :- !, Templ = tau(link(Left,RTempl)), |
3177 | | extract_span_from_event2(Right,SPAN,RTempl,NS). % the linking code already puts info into right branch |
3178 | | %extract_span_from_event2(Left,RS,LTempl,RS), |
3179 | | %unify_spans(LS,RS,NS). |
3180 | | extract_span_from_event2(tau(hide(Event)),SPAN,Templ,NS) :- !, Templ = tau(hide(ETempl)), |
3181 | | extract_span_from_event2(Event,SPAN,ETempl,NS). |
3182 | | %extract_span_from_event2(tau(repInternalChoice(X)),no_loc_info_available,Templ,NS) :- !, Templ = tau(repInternalChoice(X)). |
3183 | | extract_span_from_event2(tau(int_choice_left(S,LSpan)),SPAN,Templ,NS) :- !, |
3184 | | Templ = tau(int_choice_left(S,NS)), |
3185 | | SPAN = LSpan. |
3186 | | extract_span_from_event2(tau(int_choice_right(S,RSpan)),SPAN,Templ,NS) :- !, |
3187 | | Templ = tau(int_choice_right(S,NS)), |
3188 | | SPAN = RSpan. |
3189 | | extract_span_from_event2(tau(Event),SPAN,tau(Templ),NS) :- simple_tau_event(Event,Constructor,SPAN),!, |
3190 | | functor(Templ,Constructor,1), |
3191 | | arg(1,Templ,NS). |
3192 | | %%extract_span_from_event2(i(SPAN),SPAN,i(NS),NS). %% deprecated |
3193 | | extract_span_from_event2(tick(SPAN),SPAN,tick(NS),NS). |
3194 | | |
3195 | | simple_tau_event(chaos_stop(Span),chaos_stop,Span). |
3196 | | simple_tau_event(timeout(Span),timeout,Span). |
3197 | | %simple_tau_event(int_choice_left(_,SrcSpan),int_choice_left,SrcSpan). |
3198 | | %shift_span_for_left_branch(SrcSpan,LSpan). |
3199 | | %simple_tau_event(int_choice_right(_,SrcSpan),int_choice_right,SrcSpan). |
3200 | | %shift_span_for_right_branch(SrcSpan,RSpan). |
3201 | | simple_tau_event(rep_int_choice(Span),rep_int_choice,Span). |
3202 | | simple_tau_event(tick(Span),tick,Span). |
3203 | | |
3204 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_span(3,1,_,_,4,_),R), |
3205 | | R == src_span(3,1,3,2,4,1))). |
3206 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_position(3,1,3,_),R), |
3207 | | R == src_position(3,1,3,1))). |
3208 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src_span_operator(_SP,src_span(3,1,_,_,4,_)),R), |
3209 | | R == src_span(3,1,3,2,4,1))). |
3210 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(no_loc_info_available,R), |
3211 | | R == no_loc_info_available)). |
3212 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(unknown,R), |
3213 | | R == unknown)). |
3214 | | :- assert_must_succeed((haskell_csp: shift_span_for_left_branch(src,R), |
3215 | | R == src)). |
3216 | | :- block shift_span_for_left_branch(-,?). |
3217 | | shift_span_for_left_branch(src_span(StartLine,SC,_EndLine,_EC,Off,_LenBytes),R) :- !, |
3218 | | NEC is SC+1, |
3219 | | R=src_span(StartLine,SC,StartLine,NEC,Off,1). |
3220 | | shift_span_for_left_branch(src_position(StartLine,SC,Off,_LenBytes),R) :- !, |
3221 | | R = src_position(StartLine,SC,Off,1). |
3222 | | shift_span_for_left_branch(src_span_operator(_WholeSpan,JustOperator),R) :- !, |
3223 | | shift_span_for_left_branch(JustOperator,R). |
3224 | | shift_span_for_left_branch(no_loc_info_available,R) :- !, R=no_loc_info_available. |
3225 | | shift_span_for_left_branch(unknown(I),R) :- !, R=unknown(I). |
3226 | | shift_span_for_left_branch(X,X):- debug_println(9,not_shifting_left(X)). |
3227 | | |
3228 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_span(_,_,3,2,6,5),R), |
3229 | | R == src_span(3,1,3,2,10,1))). |
3230 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_position(3,1,3,4),R), |
3231 | | R == src_position(3,4,6,1))). |
3232 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src_span_operator(_SP,src_span(_,_,3,2,6,5)),R), |
3233 | | R == src_span(3,1,3,2,10,1))). |
3234 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(no_loc_info_available,R), |
3235 | | R == no_loc_info_available)). |
3236 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(unknown,R), |
3237 | | R == unknown)). |
3238 | | :- assert_must_succeed((haskell_csp: shift_span_for_right_branch(src,R), |
3239 | | R == src)). |
3240 | | |
3241 | | :- block shift_span_for_right_branch(-,?). |
3242 | | shift_span_for_right_branch(src_span(_StartLine,_SC,EndLine,EC,Off,LenBytes),R) :- !, |
3243 | | NL is 1, NSC is EC-1, NO is Off+LenBytes-1, |
3244 | | R=src_span(EndLine,NSC,EndLine,EC,NO,NL). |
3245 | | shift_span_for_right_branch(src_position(StartLine,SC,Off,LenBytes),R) :- !, |
3246 | | NL is 1, NSC is SC+LenBytes-1, NO is Off+LenBytes-1, |
3247 | | R = src_position(StartLine,NSC,NO,NL). |
3248 | | shift_span_for_right_branch(src_span_operator(_WholeSpan,JustOperator),R) :- !, |
3249 | | shift_span_for_right_branch(JustOperator,R). |
3250 | | shift_span_for_right_branch(no_loc_info_available,R) :- !, R=no_loc_info_available. |
3251 | | shift_span_for_right_branch(unknown(I),R) :- !, R=unknown(I). |
3252 | | shift_span_for_right_branch(X,X):- debug_println(9,not_shifting_right(X)). |
3253 | | |
3254 | | |
3255 | | % ---------------------- |
3256 | | |
3257 | | get_cspm_identifier(channel,ID) :- channel(ID,_). |
3258 | | get_cspm_identifier(datatype,DT) :- is_a_datatype(DT,_). |