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