| 1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(csp_sets,[ %is_a_set/1, % reported as an unnecessary export by infolog | |
| 6 | %evaluate_set/3, | |
| 7 | evaluate_set/2, | |
| 8 | % force_evaluate_set/2, % export superfluous (used in haskell_csp.pl) | |
| 9 | evaluate_closure/2, | |
| 10 | is_empty_set/2, | |
| 11 | is_member_set/2, | |
| 12 | is_subset_of/2, % reported as superfluous by infolog, though predicate called by meta call in haskell_csp.pl (see last two clauses of check_boolean_expression/1 in haskell_csp.pl) | |
| 13 | %is_member_comprehension_set/3, | |
| 14 | extract_variables_from_generator_list/2, | |
| 15 | try_get_cardinality_for_wait_flag/2, | |
| 16 | subsets/2, enum_subset/2, | |
| 17 | cardinality/2, | |
| 18 | singleSetElement/3, | |
| 19 | union_set/3,diff_set/3,inter_set/3, | |
| 20 | equal_element/2, not_equal_element/2, | |
| 21 | expand_set_comprehension/3, replicate_expand_set_comprehension/3, | |
| 22 | expand_symbolic_set/3, | |
| 23 | big_union/2, big_inter/2, | |
| 24 | unify_also_patterns/3, | |
| 25 | closure_expand/2, | |
| 26 | is_member_set_alsoPat/2 | |
| 27 | %,csp_full_expanded_type/2 | |
| 28 | %,expand_int_value/2 | |
| 29 | ]). | |
| 30 | ||
| 31 | :- use_module(probsrc(module_information)). | |
| 32 | :- module_info(group,csp). | |
| 33 | :- module_info(description,'Operations on CSP sets.'). | |
| 34 | ||
| 35 | /******* SICSTUS libraries *******/ | |
| 36 | :- use_module(library(lists)). | |
| 37 | %:- load_files(library(detcheck), [when(compile_time), if(changed)]). | |
| 38 | /******* ---------------- *******/ | |
| 39 | ||
| 40 | /*************** PROB modules ****************/ | |
| 41 | :- use_module(probsrc(tools),[remove_variables/3,flatten/2,exact_member/2]). | |
| 42 | :- use_module(probsrc(error_manager)). | |
| 43 | :- use_module(probsrc(self_check)). | |
| 44 | %% :- use_module(probsrc(preferences),[preference/2]). | |
| 45 | %% :- use_module(probsrc(debug)). | |
| 46 | %-------- CSP modules: | |
| 47 | :- use_module(probcspsrc(haskell_csp_analyzer),[is_csp_constructor/1]). | |
| 48 | :- use_module(probcspsrc(haskell_csp), | |
| 49 | [is_a_datatype/2, csp_constructor/3, channel/2, dataTypeDef/2,channel_type_list/2, | |
| 50 | evaluate_argument/2,force_evaluate_argument/2,force_evaluate_argument_for_member_check/2,evaluate_int_argument/2, | |
| 51 | check_boolean_expression/1, enumerate_channel_input_value/4,enumerate_datatype_el/5]). | |
| 52 | :- use_module(probcspsrc(csp_sequences)). | |
| 53 | :- use_module(probcspsrc(haskell_csp_analyzer),[csp_full_type_constructor/3,csp_full_type_constant/2]). | |
| 54 | ||
| 55 | /*************** ----------- ****************/ | |
| 56 | ||
| 57 | % -------------------------------------------------------- | |
| 58 | % SETS | |
| 59 | % -------------------------------------------------------- | |
| 60 | ||
| 61 | % Possible sets: | |
| 62 | % setValue([]) | |
| 63 | % setValue([el1,...,eln]) sorted, without duplicates | |
| 64 | % setFromTo(int(Low),int(Up)) | |
| 65 | % ... intType,.... | |
| 66 | ||
| 67 | :- assert_must_succeed(is_a_set(setFrom(1))). | |
| 68 | :- assert_must_succeed(is_a_set(dataType(bool))). | |
| 69 | :- assert_must_succeed(is_a_set(dotTupleType(list([int,int])))). | |
| 70 | :- assert_must_succeed(is_a_set(setExp(val,int))). | |
| 71 | :- assert_must_succeed(is_a_set(closureComp(_,_))). | |
| 72 | :- assert_must_succeed(is_a_set('Seq'(setValue([1,2,3])))). | |
| 73 | ||
| 74 | is_a_set(setValue(_)). | |
| 75 | is_a_set(closure(_)). | |
| 76 | is_a_set(setFromTo(_,_)). | |
| 77 | is_a_set(setFrom(_)). | |
| 78 | is_a_set(intType). | |
| 79 | is_a_set(boolType). | |
| 80 | is_a_set(dataType(_)). | |
| 81 | is_a_set(dotTupleType(_)). | |
| 82 | is_a_set(setExp(_,_)). | |
| 83 | is_a_set(closureComp(_,_)). % right? | |
| 84 | is_a_set('Seq'(_)). | |
| 85 | %is_a_set(DT) :- dataTypeDef(DT,_). | |
| 86 | ||
| 87 | ||
| 88 | :- assert_must_succeed(( csp_sets:evaluate_set([int(3)],R), R == setValue([int(3)]) )). | |
| 89 | ||
| 90 | evaluate_set([],R) :- !, R=setValue([]). | |
| 91 | evaluate_set([H|T],R) :- !, haskell_csp:evaluate_argument(H,EH), evaluate_set(T,ET), | |
| 92 | add_element(EH,ET,R). | |
| 93 | evaluate_set(X,_) :- add_internal_error('Internal Error: Could not evaluate: ',evaluate_set(X,_)),fail. | |
| 94 | ||
| 95 | force_evaluate_set([],R) :- !, R=setValue([]). | |
| 96 | force_evaluate_set([H|T],R) :- !, haskell_csp:force_evaluate_argument(H,EH), | |
| 97 | force_evaluate_set(T,ET), | |
| 98 | add_element(EH,ET,R). | |
| 99 | force_evaluate_set(X,_) :- add_internal_error('Interal Error: Could not evaluate: ',force_evaluate_set(X,_)),fail. | |
| 100 | ||
| 101 | ||
| 102 | /* This implementation of evanluate_set/2 make the Basin_Bank_CSP benchmark's performnance slower. */ | |
| 103 | /* | |
| 104 | % Functor can be evaluate_argument/2 or force_evaluate_argument/2 | |
| 105 | % Clause match is only possible through internal call. CSP-M parser always provide list inside rangeEnum(). | |
| 106 | % See implementation of haskell_csp: evaluate_set_expression/2. | |
| 107 | evaluate_set(L,Set,Functor) :- is_list(L),!, | |
| 108 | evaluate_set(L,setValue([]),Set,Functor). | |
| 109 | evaluate_set(X,_,_Functor) :- | |
| 110 | add_internal_error('Internal Error: Could not evaluate: ',evaluate_set(X)),fail. | |
| 111 | ||
| 112 | evaluate_set([],Set,Set,_Functor). | |
| 113 | evaluate_set([H|T],Set,R,Functor) :- | |
| 114 | % this variant of defining the argument call is less memory wasteful than the ordinary way (Call =.. [Functor|Args]) | |
| 115 | functor(Call,Functor,2), | |
| 116 | arg(1,Call,H),arg(2,Call,EH), | |
| 117 | haskell_csp:Call,!, | |
| 118 | add_element(EH,Set,Set1), | |
| 119 | evaluate_set(T,Set1,R,Functor). | |
| 120 | */ | |
| 121 | ||
| 122 | evaluate_closure(X,closure(RS)) :- (X=tuple(XList) -> true ; X=XList), | |
| 123 | evaluate_set(XList,setValue(RS)).%evaluate_set(XList,setValue(RS),evaluate_argument). | |
| 124 | ||
| 125 | :- use_module(probcspsrc(csp_sequences),[is_empty_list/2]). | |
| 126 | :- use_module(probcspsrc(csp_basic)). | |
| 127 | ||
| 128 | :- assert_must_succeed((csp_sets: is_empty_set(setValue([setValue([])]),R), R == false)). | |
| 129 | :- assert_must_succeed((csp_sets: is_empty_set(setValue([]),R), R == true)). | |
| 130 | :- assert_must_succeed((csp_sets: is_empty_set(setFromTo(3,1),R), R == true)). | |
| 131 | :- assert_must_succeed((csp_sets: is_empty_set(closure([tuple(ack),tuple(rec)]),R), R == false)). | |
| 132 | :- assert_must_succeed((csp_sets: is_empty_set(setFrom(1),R), R == false)). | |
| 133 | ||
| 134 | :- block is_empty_set(-,?). | |
| 135 | is_empty_set(setValue(X),R) :- !, is_empty_list(X,R). | |
| 136 | is_empty_set(closure(X),R) :- !, is_empty_list(X,R). | |
| 137 | is_empty_set(setFromTo(Low,Up),R) :- !, safe_less_than(Up,Low,R). | |
| 138 | is_empty_set(setFrom(_),R) :- !, R=false. | |
| 139 | is_empty_set(X,_) :- add_error(csp_sets,'Could not evaluate: ',is_empty_set(X)),fail. | |
| 140 | ||
| 141 | ||
| 142 | :- assert_must_succeed(( csp_sets:is_member_set(X,setValue([int(1),int(9)])), X=int(9) )). | |
| 143 | :- assert_must_fail(( csp_sets:is_member_set(X,setValue([int(1),int(9)])), X=int(3) )). | |
| 144 | :- assert_must_succeed((csp_sets: is_member_set(int(10),setFrom(5)))). | |
| 145 | :- assert_must_fail((csp_sets: is_member_set(int(3),setFrom(5)))). | |
| 146 | :- assert_must_succeed( is_member_set(na_tuple([int(3)]),typeTuple([setFromTo(1,10)])) ). | |
| 147 | :- assert_must_succeed( is_member_set(na_tuple([int(3),int(4)]),typeTuple([setFromTo(1,10),setValue([int(1),int(2),int(3),int(4)])])) ). | |
| 148 | :- assert_must_succeed( is_member_set(tuple([int(3),int(4)]),dotTupleType([setFromTo(1,10),setValue([int(1),int(2),int(3),int(4)])])) ). | |
| 149 | ||
| 150 | is_member_set(El,S) :- is_member_set2(S,El). | |
| 151 | ||
| 152 | :- block is_member_set2(-,?). | |
| 153 | is_member_set2(setValue(Set),El) :- !, blocking_member(El,Set). | |
| 154 | is_member_set2(boolType,X) :- !, (X=true;X=false). | |
| 155 | is_member_set2(intType,R) :- !, R=int(_). | |
| 156 | is_member_set2(setFromTo(Low,Up),R) :- !, R=int(X), | |
| 157 | is_member_from_to(X,Low,Up). | |
| 158 | is_member_set2(setFrom(Low),int(X)) :- !, is_member_from(X,Low). | |
| 159 | is_member_set2('Seq'(X),C) :- expand_sequence(C,list(EC)), !, list_elements_member_set(EC,X). | |
| 160 | is_member_set2('dotTupleType'(X),T) :- !,(T=tuple(TT) ; T=dotTuple(TT)), l_dot_is_member_set(TT,X). %%%%%% see trace output | |
| 161 | is_member_set2('typeTuple'(X),T) :- !, T=na_tuple(TT), l_is_member_set(TT,X). | |
| 162 | is_member_set2(dataType(DT),C) :- is_a_datatype(DT,L),!, % to do: precompute this | |
| 163 | ( (atomic(C),member(constructor(C),L)) ; ( C=record(Cons,Fields), | |
| 164 | csp_constructor(Cons,DT,ArgSubTypes), | |
| 165 | maplist(haskell_csp:get_value_alsoPat,Fields,Fields1), % could be possible that some of the elements are wrapped in in(.) or alsoPat(.,.) | |
| 166 | l_dot_is_member_set(Fields1,ArgSubTypes) ) | |
| 167 | ). | |
| 168 | is_member_set2(setExp(RangeExpr),C) :- !, is_member_set2(setExp(RangeExpr,[]),C). | |
| 169 | is_member_set2(setExp(RangeExpr,GeneratorSet),C) :- !, | |
| 170 | is_member_comprehension_set(C,RangeExpr,GeneratorSet). | |
| 171 | % print(is_member_comprehension_set(C,Tuple,GeneratorSet)),nl. | |
| 172 | % what about closureComp ? | |
| 173 | is_member_set2('Union'(LS),El) :- ground(El),!,is_member_union(LS,El). | |
| 174 | is_member_set2('Union'(LS),El) :- !,force_evaluate_argument('Union'(LS),ES), is_member_set2(ES,El). | |
| 175 | is_member_set2('Inter'(LS),El) :- !,is_member_inter(LS,El). | |
| 176 | is_member_set2(agent_call(Span,F,Par),El) :- !, haskell_csp: unfold_function_call_once(F,Par,Body,Span), | |
| 177 | force_evaluate_argument_for_member_check(Body,R), is_member_set(El,R). | |
| 178 | is_member_set2(closure(Cl),El) :- !, closure_expand(Cl,R),is_member_set(El,R). | |
| 179 | is_member_set2(S,El) :- haskell_csp: name_type(S,Type),!,is_member_set2(Type,El). | |
| 180 | is_member_set2(R,X) :- add_error(csp_sets,'Could not evaluate: ',is_member_set(X,R)),fail. | |
| 181 | ||
| 182 | :- assert_must_fail(csp_sets: is_member_union(setExp(rangeEnum([])),int(1))). | |
| 183 | ||
| 184 | :- block is_member_union(-,?). | |
| 185 | is_member_union(LS,El) :- | |
| 186 | (deconstruct_set_of_sets(LS,H,T) -> | |
| 187 | %print(lazy_Union(El,H,T)),nl, % args should not be setComp; otherwise we have problem with cut below | |
| 188 | (is_member_set2(H,El) -> true ; is_member_set2('Union'(T),El)) | |
| 189 | ; empty_set_of_sets(LS) -> fail | |
| 190 | ; add_error_fail(is_member_set,'Illegal argument: ','Union'(LS))). | |
| 191 | :- block is_member_inter(-,?). | |
| 192 | is_member_inter(LS,El) :- | |
| 193 | (deconstruct_set_of_sets(LS,H,T) -> | |
| 194 | is_member_set2(H,El), | |
| 195 | (empty_set_of_sets(T) -> true ; is_member_set2('Inter'(T),El)) | |
| 196 | ; empty_set_of_sets(T) -> add_error(is_member_set2,'Empty set not allowed for Inter(-): ',T) | |
| 197 | ; add_error_fail(is_member_set,'Illegal argument: ','Inter'(LS))). | |
| 198 | ||
| 199 | :- block is_member_from_to(-,-,?),is_member_from_to(-,?,-). | |
| 200 | is_member_from_to(X,Low,Up) :- ground(X),!,geq(X,Low), leq(X,Up). | |
| 201 | is_member_from_to(X,Low,Up) :- enumerate_csp_int(X,Low,Up). | |
| 202 | :- block geq(?,-). | |
| 203 | geq(X,Low) :- X>=Low. | |
| 204 | :- block leq(?,-). | |
| 205 | leq(X,Up) :- X=<Up. | |
| 206 | ||
| 207 | :- block is_member_from(-,?),is_member_from(?,-). | |
| 208 | is_member_from(X,Low) :- X >= Low. | |
| 209 | ||
| 210 | :- block blocking_member(?,-). | |
| 211 | blocking_member(X,[H|T]) :- | |
| 212 | (equal_element(X,H) ; blocking_member(X,T)). | |
| 213 | ||
| 214 | :- assert_must_succeed((csp_sets: l_dot_is_member_set([int(1),int(2),int(3)],['dotTupleType'([setFromTo(1,3),setFrom(1),setFromTo(1,3)])]))). | |
| 215 | :- assert_must_fail((csp_sets: l_dot_is_member_set([int(1),int(2),int(3)],['dotTupleType'([setFromTo(1,3),setFromTo(1,3),setFrom(14)])]))). | |
| 216 | :- assert_must_succeed((csp_sets: l_dot_is_member_set([int(1),int(2),int(3),int(10),int(9)], | |
| 217 | ['dotTupleType'([setFromTo(1,3),setFrom(1),setFromTo(1,3)]),intType,setValue([int(1),int(9),int(10)])]))). | |
| 218 | :- assert_must_fail((csp_sets: l_dot_is_member_set([int(1),int(2),int(3),int(10),int(11)], | |
| 219 | ['dotTupleType'([setFromTo(1,3),setFrom(1),setFromTo(1,3)]),intType,setValue([int(1),int(9),int(10)])]))). | |
| 220 | :- assert_must_succeed((csp_sets: l_dot_is_member_set([int(10),int(9),int(1),int(2),int(3)], | |
| 221 | ['dotTupleType'([intType,setValue([int(1),int(9),int(10)]),setFromTo(1,3),setFrom(1),setFromTo(1,3)])]))). | |
| 222 | ||
| 223 | l_dot_is_member_set(L,TL) :- | |
| 224 | unfold_dot_tuples(L,R), | |
| 225 | l_unfold_datatype_dot_tuple(TL,TR), | |
| 226 | l_is_member_set(R,TR). | |
| 227 | ||
| 228 | l_is_member_set(SetList,SetList1) :- | |
| 229 | is_list(SetList),!, | |
| 230 | maplist(is_member_set,SetList,SetList1). | |
| 231 | l_is_member_set(L,S) :- add_internal_error('Internal Error: Could not evaluate: ', l_is_member_set(L,S)),fail. | |
| 232 | ||
| 233 | :- assert_must_succeed((csp_sets: unfold_dot_tuples([],[]))). | |
| 234 | :- assert_must_succeed((csp_sets: unfold_dot_tuples([int(1),tuple([int(2),int(3)]),int(4)],R), R == [int(1),int(2),int(3),int(4)])). | |
| 235 | :- assert_must_succeed((csp_sets: unfold_dot_tuples([int(1),int(2),int(3),int(4)],R), R == [int(1),int(2),int(3),int(4)])). | |
| 236 | :- assert_must_succeed((csp_sets: unfold_dot_tuples([tuple([int(1),int(5)]),tuple([int(2),int(3)])],R), R == [int(1),int(5),int(2),int(3)])). | |
| 237 | :- assert_must_succeed((csp_sets: unfold_dot_tuples([tuple([int(1),tuple([int(2),int(3)])])],R), R == [int(1),int(2),int(3)])). | |
| 238 | ||
| 239 | unfold_dot_tuples([],[]). | |
| 240 | unfold_dot_tuples([H|T],R) :- | |
| 241 | ((nonvar(H),(H = tuple(L) ; H=dotTuple(L))) -> unfold_dot_tuples(L,LRes), append(LRes,R1,R) ; R=[H|R1]), unfold_dot_tuples(T,R1). | |
| 242 | ||
| 243 | :- assert_must_succeed((csp_sets: l_unfold_datatype_dot_tuple([],[]))). | |
| 244 | :- assert_must_succeed((csp_sets: l_unfold_datatype_dot_tuple(['dotTupleType'([intType,setValue([int(1),int(9),int(10)])])],R), R == [intType,setValue([int(1),int(9),int(10)])])). | |
| 245 | :- assert_must_succeed((csp_sets: l_unfold_datatype_dot_tuple([intType,intType],R), R == [intType,intType])). | |
| 246 | :- assert_must_succeed((csp_sets: l_unfold_datatype_dot_tuple(['dotTupleType'([intType,setValue([int(1),int(9),int(10)])]),'dotTupleType'([intType,setValue([int(1),int(9),int(10)])])],R), | |
| 247 | R == [intType,setValue([int(1),int(9),int(10)]),intType,setValue([int(1),int(9),int(10)])])). | |
| 248 | ||
| 249 | unfold_datatype_dot_tuple(DT,R) :- | |
| 250 | (nonvar(DT), DT = 'dotTupleType'(L) -> R=L ; R=[DT]). | |
| 251 | ||
| 252 | l_unfold_datatype_dot_tuple(LDotTypes,Res) :- | |
| 253 | maplist(unfold_datatype_dot_tuple,LDotTypes,R), | |
| 254 | append(R,Res). | |
| 255 | ||
| 256 | list_elements_member_set([],_) :- !. | |
| 257 | list_elements_member_set([H|T],Set) :- !, is_member_set2(Set,H), list_elements_member_set(T,Set). | |
| 258 | list_elements_member_set(L,S) :- add_internal_error('Internal Error: Could not evaluate: ', list_elements_member_set(L,S)),fail. | |
| 259 | ||
| 260 | :- assert_must_succeed((csp_sets: deconstruct_set_of_sets(setExp(rangeEnum([int(1),int(2),int(3)])),H,T),H==int(1),T == setExp(rangeEnum([int(2),int(3)])))). | |
| 261 | :- assert_must_succeed((csp_sets: deconstruct_set_of_sets(setValue([int(1),int(2),int(3)]),H,T),H==int(1),T == setValue([int(2),int(3)]))). | |
| 262 | :- assert_must_fail((csp_sets: deconstruct_set_of_sets(setValue([]),_H,_T))). | |
| 263 | ||
| 264 | %deconstruct_set_of_sets(setEnum([H|T]),H,setEnum(T)). | |
| 265 | deconstruct_set_of_sets(setExp(rangeEnum([H|T])),H,setExp(rangeEnum(T))). | |
| 266 | deconstruct_set_of_sets(setValue(V),H,setValue(T)) :- deconstruct_setValue(V,H,T). | |
| 267 | :- block deconstruct_setValue(-,?,?). | |
| 268 | deconstruct_setValue([H|T],H,T). | |
| 269 | ||
| 270 | :- assert_must_succeed((csp_sets: empty_set_of_sets(setValue([])))). | |
| 271 | empty_set_of_sets(setExp(rangeEnum([]))). | |
| 272 | empty_set_of_sets(setValue(X)) :- is_empty_list(X,true). | |
| 273 | ||
| 274 | :- assert_must_succeed(( csp_sets:cardinality(setValue([int(1),int(9)]),R), R==int(2) )). | |
| 275 | :- block cardinality(-,?). | |
| 276 | cardinality(setValue(S),R) :- my_length(S,C),!,R=int(C). | |
| 277 | cardinality(setFromTo(Low,Up),R) :- !, | |
| 278 | R=int(C), when((ground(Low),ground(Up)),compute_from_to_cardinality(Low,Up,C)). | |
| 279 | cardinality(setFrom(Low),_) :- !, | |
| 280 | add_error(csp_sets,'Trying to compute cardinality of infinite set: ',set_from(Low)),fail. | |
| 281 | cardinality(closure(ChannelList),R) :- !,my_length(Closure,C), R=int(C), | |
| 282 | when(ground(ChannelList), | |
| 283 | expand_symbolic_set(closure(ChannelList),setValue(Closure),closure_cardinality)). | |
| 284 | cardinality(dataType(DT),R) :- !,R=int(C),my_length(DTSet,C), | |
| 285 | expand_symbolic_set(dataType(DT),setValue(DTSet),datatype_set_cardinality). | |
| 286 | cardinality(X,_R) :- add_error(csp_sets,'Could not compute card of: ',X),fail. | |
| 287 | ||
| 288 | :- assert_must_succeed((csp_sets: compute_from_to_cardinality(1,3,C), C == 3)). | |
| 289 | :- assert_must_succeed((csp_sets: compute_from_to_cardinality(-1,3,C), C == 5)). | |
| 290 | :- assert_must_succeed((csp_sets: compute_from_to_cardinality(3,1,C), C == 0)). | |
| 291 | :- assert_must_succeed((csp_sets: compute_from_to_cardinality(-3,1,C), C == 5)). | |
| 292 | :- assert_must_succeed((csp_sets: compute_from_to_cardinality(-3,-1,C), C == 3)). | |
| 293 | ||
| 294 | compute_from_to_cardinality(Low,Up,C) :- | |
| 295 | (Up<Low -> | |
| 296 | C is 0 | |
| 297 | ; C is Up-Low+1 | |
| 298 | ). | |
| 299 | ||
| 300 | my_length(L,Len) :- my_length_aux(L,0,Len). | |
| 301 | :- block my_length_aux(-,?,?). | |
| 302 | my_length_aux([],Acc,Acc). | |
| 303 | my_length_aux([_|T],Acc,R) :- A1 is Acc+1, my_length_aux(T,A1,R). | |
| 304 | ||
| 305 | ||
| 306 | try_get_cardinality_for_wait_flag(setValue(S),R) :- try_get_length(S,C),!,R=C. | |
| 307 | try_get_cardinality_for_wait_flag(setFromTo(Low,Up),C) :- | |
| 308 | ground(Low),ground(Up),!,C is Up-Low+1. | |
| 309 | try_get_cardinality_for_wait_flag(_,1000). | |
| 310 | ||
| 311 | try_get_length(X,_) :- var(X),!,fail. | |
| 312 | try_get_length([],0). | |
| 313 | try_get_length([_|T],R) :- try_get_length(T,R1), R is R1+1. | |
| 314 | ||
| 315 | :- block singleSetElement(-,?,?). | |
| 316 | singleSetElement(S,El,Span) :- expand_symbolic_set(S,setValue(V),singleSetElement), | |
| 317 | singleSetElement_aux(V,El,Span). | |
| 318 | ||
| 319 | :- block singleSetElement_aux(-,?,?). | |
| 320 | singleSetElement_aux([H|T],El,_Span) :- (var(T);T==[]),!,H=El. | |
| 321 | singleSetElement_aux(Set,_El,Span) :- | |
| 322 | add_error(singleSetElement,'This is not a singleton set: ',setValue(Set),Span),fail. | |
| 323 | ||
| 324 | :- assert_must_succeed(( csp_sets:is_subset_of(R,setValue([int(2),int(4)])), | |
| 325 | R = setValue([int(4)]) )). | |
| 326 | :- assert_must_fail(( csp_sets:is_subset_of(R,setValue([int(2),int(4)])), | |
| 327 | R = setValue([int(3)]) )). | |
| 328 | :- block is_subset_of(-,?), is_subset_of(?,-). | |
| 329 | is_subset_of(X,Y) :- | |
| 330 | expand_symbolic_set(X,setValue(EX),is_subset_of_x), | |
| 331 | expand_symbolic_set(Y,setValue(EY),is_subset_of_y), | |
| 332 | is_subset_of2(EX,EY). | |
| 333 | ||
| 334 | :- block is_subset_of2(-,?). | |
| 335 | is_subset_of2([],_). | |
| 336 | is_subset_of2([H|T],S) :- remove_element(H,S,S2), is_subset_of2(T,S2). | |
| 337 | ||
| 338 | :- assert_must_succeed(( csp_sets:subsets(setValue([int(1),int(9)]),R), | |
| 339 | R==setValue([ setValue([int(1),int(9)]),setValue([int(9)]),setValue([int(1)]),setValue([]) ]) )). | |
| 340 | ||
| 341 | subsets(S,setValue(RS)) :- expand_symbolic_set(S,setValue(ES),subsets),sub2(ES,RS). | |
| 342 | ||
| 343 | :- block sub2(-,?). | |
| 344 | sub2([],[setValue([])]). | |
| 345 | sub2([El|T],Res) :- sub2(T,TR), sub3(TR,El,Res). | |
| 346 | ||
| 347 | :- block sub3(-,?,?). | |
| 348 | sub3([],_,[]). | |
| 349 | sub3([setValue(S1)|T],El,[setValue([El|S1]),setValue(S1)|ST]) :- sub3(T,El,ST). | |
| 350 | ||
| 351 | ||
| 352 | :- assert_must_succeed(( csp_sets:enum_subset(setValue([int(1),int(9)]),R), | |
| 353 | R==setValue([int(9)]) )). | |
| 354 | enum_subset(S,setValue(Subset)) :- expand_symbolic_set(S,setValue(ES),enum_subset), | |
| 355 | enum_sub2(ES,Subset). | |
| 356 | enum_sub2([],[]). | |
| 357 | enum_sub2([El|T],Res) :- | |
| 358 | (Res = [El|T2], enum_sub2(T,T2)) | |
| 359 | ; enum_sub2(T,Res). | |
| 360 | ||
| 361 | :- assert_must_succeed(( csp_sets:add_element(int(3),setValue([int(1),int(9)]),R), R==setValue([int(1),int(3),int(9)]) )). | |
| 362 | :- assert_must_succeed(( csp_sets:add_element(int(3),setValue([int(1),int(3),int(9)]),R), R==setValue([int(1),int(3),int(9)]) )). | |
| 363 | :- assert_must_succeed(( csp_sets:add_element(int(11),setValue([int(1),int(9)]),R), R==setValue([int(1),int(9),int(11)]) )). | |
| 364 | :- assert_must_succeed(( csp_sets:add_element(int(1),setValue([int(3),int(9)]),R), R==setValue([int(1),int(3),int(9)]) )). | |
| 365 | :- assert_must_succeed(( csp_sets:add_element(setValue([int(3)]),setValue([]),R), R==setValue([setValue([int(3)])]) )). | |
| 366 | :- assert_must_succeed(( csp_sets:add_element(boolType,setValue([]),R), R == setValue([setValue([true,false])]))). | |
| 367 | ||
| 368 | :- block add_element(-,?,?), add_element(?,-,?). | |
| 369 | add_element(El,S,Res) :- Res = setValue(R), expand_symbolic_set(S,setValue(ES),add_element), | |
| 370 | (is_a_set(El) -> expand_symbolic_set(El,ExEl,add_element) ; ExEl=El), % normalise element before storing in set | |
| 371 | when(ground(ExEl),add_element1(ES,ExEl,R)). | |
| 372 | % when( (/* ground(El),*/ nonvar(ES)), add_element2(ES,El,R)). | |
| 373 | ||
| 374 | :- block add_element1(-,?,?). | |
| 375 | %add_element1(T,El,Res) :- print(add_element1(T,El,Res)),nl,fail. | |
| 376 | add_element1([],El,[El]). | |
| 377 | add_element1([H|T],El,Res) :- when(?=(El,H),(El @=<H -> (El=H -> Res = [El|T] ; Res = [El,H|T]) | |
| 378 | ; (Res=[H|R2],add_element1(T,El,R2)))). | |
| 379 | ||
| 380 | :- assert_must_succeed(( csp_sets:union_set(setValue([int(3),int(4)]),setValue([int(2),int(9)]),R), | |
| 381 | R == setValue([int(2),int(3),int(4),int(9)]) )). | |
| 382 | :- assert_must_succeed(( csp_sets:union_set(setValue([int(3),int(4)]),setValue([int(4),int(9)]),R), | |
| 383 | R == setValue([int(3),int(4),int(9)]) )). | |
| 384 | :- assert_must_succeed(( csp_sets:union_set(setValue([int(3),int(4)]),setValue([]),R), | |
| 385 | R == setValue([int(3),int(4)]) )). | |
| 386 | :- assert_must_succeed(( csp_sets:union_set(setValue([]),setValue([int(3),int(4)]),R), | |
| 387 | R == setValue([int(3),int(4)]) )). | |
| 388 | :- block union_set(-,?,?), union_set(?,-,?). | |
| 389 | union_set(S1,S2,Res) :- Res = setValue(R), expand_symbolic_set(S1,setValue(ES1),union_set1), | |
| 390 | expand_symbolic_set(S2,setValue(ES2),union_set2), | |
| 391 | when(ground((ES1,ES2)),union_add_elements(ES1,ES2,R,none,none)) | |
| 392 | % , print(union(S1,S2,Res)),nl | |
| 393 | . | |
| 394 | ||
| 395 | union_add_elements([],R,R,_,_). | |
| 396 | union_add_elements([H|T],[],[H|T],PrevH1,_) :- (ground(H) -> check_sorted(union_set,PrevH1,H) ; true). | |
| 397 | union_add_elements([H1|T1],[H2|T2],Res,PrevH1,PrevH2) :- %check_sorted(union_set,PrevH1,H1), % unnecessary call | |
| 398 | when((ground(H1),ground(H2)), | |
| 399 | (check_sorted(union_set,PrevH1,H1), check_sorted(union_set,PrevH2,H2), | |
| 400 | (H1=H2 -> Res=[H1|RT],union_add_elements(T1,T2,RT,H1,H1) | |
| 401 | ; (H1 @=< H2 -> Res=[H1|RT], union_add_elements(T1,[H2|T2],RT,H1,none) | |
| 402 | ; Res=[H2|RT], union_add_elements([H1|T1],T2,RT,none,H2)) ))). | |
| 403 | ||
| 404 | check_sorted(Src,PrevH,H) :- ((PrevH=none;PrevH @< H) -> true ; add_error(Src,'CSP set not sorted: ',[PrevH,H])). | |
| 405 | ||
| 406 | :- assert_must_succeed(( csp_sets:diff_set(setValue([int(3),int(4)]),setValue([int(2),int(3)]),R), | |
| 407 | R == setValue([int(4)]) )). | |
| 408 | :- assert_must_succeed(( csp_sets:diff_set(setValue([int(3),int(4)]),setValue([int(2),int(5)]),R), | |
| 409 | R == setValue([int(3),int(4)]) )). | |
| 410 | :- assert_must_succeed(( csp_sets:diff_set(setValue([int(3),int(4)]),setValue([int(2),int(3),int(4),int(5),int(9)]),R), | |
| 411 | R == setValue([]) )). | |
| 412 | ||
| 413 | :- block diff_set(-,?,?), diff_set(?,-,?). | |
| 414 | diff_set(S1,S2,Res) :- Res = setValue(R), expand_symbolic_set(S1,setValue(ES1),diff_set1), | |
| 415 | expand_symbolic_set(S2,setValue(ES2),diff_set2), | |
| 416 | when(ground((ES1,ES2)),diff_elements(ES1,ES2,R)). | |
| 417 | %, print(diff(S1,S2,Res,ES1,ES2)),nl. | |
| 418 | ||
| 419 | diff_elements([],_,[]). | |
| 420 | diff_elements([H|T],S2,Res) :- | |
| 421 | (remove_element(H,S2,S3) | |
| 422 | -> diff_elements(T,S3,Res) | |
| 423 | ; (Res=[H|R2], diff_elements(T,S2,R2)) | |
| 424 | ). | |
| 425 | ||
| 426 | %:- block remove_element(-,?,?), remove_element(?,-,?). | |
| 427 | remove_element(X,[H|T],R) :- | |
| 428 | (selectchk(X,[H|T],R) | |
| 429 | -> true | |
| 430 | ; equal_element(X,H) | |
| 431 | -> R=T | |
| 432 | ; (X@>H, /* diff set assumes that arguments are already evaluated ! */ | |
| 433 | R=[H|RT], remove_element(X,T,RT)) | |
| 434 | ). | |
| 435 | ||
| 436 | ||
| 437 | :- assert_must_succeed(( csp_sets:inter_set(setValue([int(3),int(4)]),setValue([int(2),int(4)]),R), | |
| 438 | R == setValue([int(4)]) )). | |
| 439 | :- assert_must_succeed(( csp_sets:inter_set(setValue([int(3),int(4)]),setValue([int(3),int(4)]),R), | |
| 440 | R == setValue([int(3),int(4)]) )). | |
| 441 | :- assert_must_succeed(( csp_sets:inter_set(setValue([int(3),int(4)]),setFromTo(4,5),R), | |
| 442 | R == setValue([int(4)]) )). | |
| 443 | :- assert_must_succeed(( csp_sets:inter_set(setValue([int(2)]),setFromTo(0,1),R), | |
| 444 | R == setValue([]) )). | |
| 445 | :- assert_must_succeed(( csp_sets:inter_set(setFrom(1),setFromTo(3,5),R), | |
| 446 | R == setValue([int(3),int(4),int(5)]))). | |
| 447 | :- assert_must_succeed(( csp_sets:inter_set(setFrom(6),setFromTo(3,5),R), | |
| 448 | R == setValue([]))). | |
| 449 | :- assert_must_succeed(( csp_sets:inter_set(setFrom(6),setValue([]),R), | |
| 450 | R == setValue([]))). | |
| 451 | ||
| 452 | :- block inter_set(-,?,?), inter_set(?,-,?). | |
| 453 | inter_set(S1,S2,Res) :- Res = setValue(R), | |
| 454 | (S1=setFrom(Low) -> | |
| 455 | expand_symbolic_set(S2,setValue(ES2),inter_set1), | |
| 456 | when(ground((Low,ES2)),inter_merge_elements_from(ES2,Low,R)) | |
| 457 | ;S2=setFrom(Low) -> | |
| 458 | expand_symbolic_set(S1,setValue(ES1),inter_set2), | |
| 459 | when(ground((ES1,Low)),inter_merge_elements_from(ES1,Low,R)) | |
| 460 | ; | |
| 461 | expand_symbolic_set(S1,setValue(ES1),inter_set1), | |
| 462 | expand_symbolic_set(S2,setValue(ES2),inter_set2), | |
| 463 | when(ground((ES1,ES2)),inter_merge_elements(ES1,ES2,R)) | |
| 464 | ). | |
| 465 | ||
| 466 | inter_merge_elements([],_R,[]). | |
| 467 | inter_merge_elements([_|_],[],[]). | |
| 468 | inter_merge_elements([H1|T1],[H2|T2],Res) :- | |
| 469 | (equal_element(H1,H2) | |
| 470 | -> (Res = [H1|TR], inter_merge_elements(T1,T2,TR)) | |
| 471 | ; (H1@<H2 -> inter_merge_elements(T1,[H2|T2],Res) | |
| 472 | ; inter_merge_elements([H1|T1],T2,Res) | |
| 473 | ) | |
| 474 | ). | |
| 475 | ||
| 476 | inter_merge_elements_from([],_Low,[]). | |
| 477 | inter_merge_elements_from([int(H)|T],Low,Res) :- | |
| 478 | ((Low =< H) -> | |
| 479 | Res = [int(H)|TR], inter_merge_elements_from(T,Low,TR) | |
| 480 | ; | |
| 481 | inter_merge_elements_from(T,Low,Res) | |
| 482 | ). | |
| 483 | ||
| 484 | :- assert_must_succeed((X=true, csp_sets: equal_element(true, X))). | |
| 485 | :- assert_must_fail((X=false, csp_sets: equal_element(true, X))). | |
| 486 | :- assert_must_succeed((X=false, csp_sets: equal_element(false, X))). | |
| 487 | :- assert_must_fail((X=true, csp_sets: equal_element(false, X))). | |
| 488 | :- assert_must_succeed((R=setFrom(1),csp_sets: equal_element(setFrom(1), R))). | |
| 489 | :- assert_must_fail((R=setFrom(2),csp_sets: equal_element(setFrom(1), R))). | |
| 490 | :- assert_must_fail((R=intType,csp_sets: equal_element(setFrom(1), R))). | |
| 491 | :- assert_must_succeed((R=setFromTo(1,46), csp_sets: equal_element(setFromTo(1,46),R))). | |
| 492 | :- assert_must_fail((R=setFromTo(1,2), csp_sets: equal_element(setFromTo(1,46),R))). | |
| 493 | :- assert_must_fail((R=setFrom(1), csp_sets: equal_element(setFromTo(1,46),R))). | |
| 494 | :- assert_must_succeed((R=setValue([int(1),int(2),int(3)]), csp_sets: equal_element(setFromTo(1,3),R))). | |
| 495 | :- assert_must_succeed((R=setValue([]), csp_sets: equal_element(setFromTo(3,1),R))). | |
| 496 | :- assert_must_fail((R=setValue([int(1),int(2),int(3)]), csp_sets: equal_element(setFromTo(1,4),R))). | |
| 497 | :- assert_must_fail((R=setFrom(10), csp_sets: equal_element(setValue(_X), R))). | |
| 498 | :- assert_must_succeed((R=boolType, csp_sets: equal_element(setValue([true,false]),R))). | |
| 499 | :- assert_must_succeed((R=setFromTo(1,1), csp_sets: equal_element(setValue([int(1)]),R))). | |
| 500 | :- assert_must_succeed((R=tuple([v1,int(0),na_tuple([int(0),int(0)])]), csp_sets: equal_element(tuple([v1,tuple([int(0),na_tuple([int(0),int(0)])])]),R))). | |
| 501 | :- assert_must_succeed((R=tuple([v1,tuple([int(0),na_tuple([int(0),int(0)])])]), csp_sets: equal_element(tuple([v1,int(0),na_tuple([int(0),int(0)])]),R))). | |
| 502 | :- assert_must_succeed((R=record(v1,[int(0),na_tuple([int(0),int(0)])]), csp_sets: equal_element(tuple([v1,tuple([int(0),na_tuple([int(0),int(0)])])]),R))). | |
| 503 | ||
| 504 | equal_element(X,Y) :- | |
| 505 | (var(X);var(Y)),!,X=Y. | |
| 506 | equal_element(true,X) :- !, | |
| 507 | ( X=true -> true | |
| 508 | ; X=false -> fail | |
| 509 | ; add_error_fail(haskell_csp,'Type error in equality: ',true=X) | |
| 510 | ). | |
| 511 | equal_element(false,X) :- !, | |
| 512 | ( X=false -> true | |
| 513 | ; X=true -> fail | |
| 514 | ; add_error_fail(haskell_csp,'Type error in equality: ',false=X) | |
| 515 | ). | |
| 516 | equal_element(int(X),R) :- !, | |
| 517 | (R=int(Y) -> X=Y | |
| 518 | ; add_error_fail(haskell_csp,'Type error in equality: ',int(X)=R) | |
| 519 | ). | |
| 520 | equal_element(setFrom(X),R) :- !, | |
| 521 | (R=setFrom(Y) -> X=Y | |
| 522 | ; is_a_set(R) -> fail | |
| 523 | ; add_error_fail(haskell_csp,'Type error in equality: ',setFrom(X)=R) | |
| 524 | ). | |
| 525 | equal_element(setFromTo(X,Y),R) :- !, | |
| 526 | (R=setFromTo(X2,Y2) -> X=X2,Y=Y2 | |
| 527 | ; (R=setValue(_) ;R=setExp(_,_)) -> equal_sets(setFromTo(X,Y),R) | |
| 528 | ; is_a_set(R) -> fail % Set different for setValue and setExp | |
| 529 | ; add_error_fail(haskell_csp,'Type error in equality: ',setFromTo(X,Y)=R) | |
| 530 | ). | |
| 531 | equal_element(setValue(X),R) :- !, | |
| 532 | (R=setValue(Y) -> equal_setValue(X,Y) | |
| 533 | ; R=setFrom(_) -> fail % infinite set cannot be equal to finite one | |
| 534 | ; is_a_set(R) -> expand_symbolic_set(R,setValue(ER),equal_element), equal_setValue(X,ER) | |
| 535 | ; add_error_fail(haskell_csp,'Type error in equality: ',setValue(X)=R) | |
| 536 | ). | |
| 537 | equal_element(list(X),R) :- !, | |
| 538 | (R=list(Y) -> X=Y | |
| 539 | ;add_error_fail(haskell_csp,'Type error in equality: ',list(X)=R) | |
| 540 | ). | |
| 541 | equal_element(na_tuple(X),R) :- !, | |
| 542 | (R=na_tuple(Y) -> X=Y | |
| 543 | ;add_error_fail(haskell_csp,'Type error in equality: ',na_tuple(X)=R) | |
| 544 | ). | |
| 545 | equal_element(tuple(X),R) :- !, | |
| 546 | ( R=tuple(Y) -> (X=Y ; equal_interleaved_dot_tuples(X,Y)) | |
| 547 | ; R=record(C,A) -> X=[H|T], C=H, (T=A ; equal_interleaved_dot_tuples(T,A)) | |
| 548 | ; add_error_fail(haskell_csp,'Type error in equality: ',tuple(X)=R) | |
| 549 | ). | |
| 550 | equal_element(dotTuple(X),R) :- !, | |
| 551 | ( R=tuple(Y) -> (X=Y ; equal_interleaved_dot_tuples(X,Y)) | |
| 552 | ; R=record(C,A) -> X=[H|T], C=H, (T=A ; equal_interleaved_dot_tuples(T,A)) | |
| 553 | ; add_error_fail(haskell_csp,'Type error in equality: ',dotTuple(X)=R) | |
| 554 | ). | |
| 555 | equal_element(record(C,A),R) :- | |
| 556 | get_constructor_type(C,Type),!, | |
| 557 | ((R=record(C2,A2),get_constructor_type(C2,Type)) -> C=C2,(A=A2 ; equal_interleaved_dot_tuples(A,A2)) % missing subtype checks | |
| 558 | ; R=tuple([H|T]) -> (H=C,(T=A ; equal_interleaved_dot_tuples(A,T))) | |
| 559 | ; (atomic(R),get_constant_type(R,Type)) -> fail | |
| 560 | ; R=agent_call(_,_,_) -> force_evaluate_argument(R,Res),equal_element(record(C,A),Res) | |
| 561 | ; add_error_fail(haskell_csp,'Type error in equality: ',record(C,A)=R) | |
| 562 | ). | |
| 563 | equal_element(X,R) :- | |
| 564 | atomic(X),get_constant_type(X,Type),!, | |
| 565 | ((atomic(R),get_constant_type(R,Type)) -> X=R | |
| 566 | ;(R=record(C,_Args),get_constructor_type(C,Type)) -> fail | |
| 567 | ; add_error_fail(haskell_csp,'Type error in equality: ',X=R) | |
| 568 | ). | |
| 569 | equal_element(Set,R) :- | |
| 570 | is_a_set(Set),!, | |
| 571 | expand_symbolic_set(Set,ES,equal_element), | |
| 572 | equal_element(ES,R). | |
| 573 | % To do: Further Improve this predicate, and check typing | |
| 574 | equal_element(X,Y) :- print(equal_element(X,Y)),nl,X=Y. | |
| 575 | ||
| 576 | equal_interleaved_dot_tuples(X,Y) :- | |
| 577 | unify_tuple_elements(X,Y,R,tuple), | |
| 578 | (X=R -> true; unfold_dot_tuples(X,XR),XR=R). | |
| 579 | ||
| 580 | equal_sets(setFromTo(X,Y),R) :- | |
| 581 | ((R=setValue(S),ground((X,Y,S))) -> | |
| 582 | cardinality(setFromTo(X,Y),int(N)), | |
| 583 | length(S,N), | |
| 584 | expand_from_to(X,Y,XYSet), | |
| 585 | diff_elements(XYSet,S,[]) | |
| 586 | ; | |
| 587 | expand_symbolic_set(setFromTo(X,Y),ES,equal_element), | |
| 588 | equal_element(ES,R) | |
| 589 | ). | |
| 590 | % check if two lists inside setValue are equal; should be sorted ! | |
| 591 | % as all elements that appear in setValue are normalised we could simply use Prolog Unification: X=Y ? | |
| 592 | equal_setValue(X,Y) :- | |
| 593 | (var(X);var(Y)),!,X=Y. | |
| 594 | equal_setValue(L1,L2) :- | |
| 595 | maplist(equal_element,L1,L2). | |
| 596 | ||
| 597 | get_constructor_type(C,Type) :- csp_full_type_constructor(C,DT,_ArgTypes),!,Type=DT. | |
| 598 | get_constructor_type(C,_) :- add_internal_error(/*get_constructor_type,*/'Internal Error: Unknown record constructor: ',C),fail. | |
| 599 | get_constant_type(C,Type) :- csp_full_type_constant(C,DataType),!,Type=DataType. | |
| 600 | get_constant_type(C,Type) :- csp_full_type_constructor(C,DataType,_ArgTypes),!, | |
| 601 | % a type constructor is passed as an atomic value; some CSP specs do this (stc.csp of Kharmeh PhD spec) | |
| 602 | Type=constructor(DataType). | |
| 603 | get_constant_type(C,_) :- add_internal_error(/*get_constant_type,*/'Internal Error: Unknown constant: ',C),fail. | |
| 604 | ||
| 605 | :- assert_must_fail((X=true, csp_sets: not_equal_element(true, X))). | |
| 606 | :- assert_must_succeed((X=false, csp_sets: not_equal_element(true, X))). | |
| 607 | :- assert_must_fail((X=false, csp_sets: not_equal_element(false, X))). | |
| 608 | :- assert_must_succeed((X=true, csp_sets: not_equal_element(false, X))). | |
| 609 | :- assert_must_fail((R=setFrom(1),csp_sets: not_equal_element(setFrom(1), R))). | |
| 610 | :- assert_must_succeed((R=setFrom(2),csp_sets: not_equal_element(setFrom(1), R))). | |
| 611 | :- assert_must_succeed((R=intType,csp_sets: not_equal_element(setFrom(1), R))). | |
| 612 | :- assert_must_fail((R=setFromTo(1,46), csp_sets: not_equal_element(setFromTo(1,46),R))). | |
| 613 | :- assert_must_succeed((R=setFromTo(1,2), csp_sets: not_equal_element(setFromTo(1,46),R))). | |
| 614 | :- assert_must_succeed((R=setFrom(1), csp_sets: not_equal_element(setFromTo(1,46),R))). | |
| 615 | :- assert_must_fail((R=setValue([int(1),int(2),int(3)]), csp_sets: not_equal_element(setFromTo(1,3),R))). | |
| 616 | :- assert_must_fail((R=setValue([]), csp_sets: not_equal_element(setFromTo(3,1),R))). | |
| 617 | :- assert_must_succeed((R=setValue([int(1),int(2),int(3)]), csp_sets: not_equal_element(setFromTo(1,4),R))). | |
| 618 | :- assert_must_succeed((R=setFrom(10), csp_sets: not_equal_element(setValue(_X), R))). | |
| 619 | :- assert_must_fail((R=boolType, csp_sets: not_equal_element(setValue([true,false]),R))). | |
| 620 | :- assert_must_fail((R=setFromTo(1,1), csp_sets: not_equal_element(setValue([int(1)]),R))). | |
| 621 | :- assert_must_succeed((R=tuple([int(1),int(2)]), csp_sets: not_equal_element(tuple([int(1),int(3)]), R))). | |
| 622 | :- assert_must_fail((R=tuple([int(1),int(2)]), csp_sets: not_equal_element(tuple([int(1),int(2)]), R))). | |
| 623 | :- assert_must_succeed((R=na_tuple([int(1),int(2)]), csp_sets: not_equal_element(na_tuple([int(1),int(3)]), R))). | |
| 624 | :- assert_must_fail((R=na_tuple([int(1),int(2)]), csp_sets: not_equal_element(na_tuple([int(1),int(2)]), R))). | |
| 625 | :- assert_must_succeed((R=list([int(1),int(2)]), csp_sets: not_equal_element(list([int(1),int(3)]), R))). | |
| 626 | :- assert_must_fail((R=list([int(1),int(2)]), csp_sets: not_equal_element(list([int(1),int(2)]), R))). | |
| 627 | :- assert_must_succeed((R=record(seq,[int(1),int(2)]), csp_sets: not_equal_element(record(seq,[int(1),int(3)]), R))). | |
| 628 | :- assert_must_fail((R=record(seq,[int(1),int(2)]), csp_sets: not_equal_element(record(seq,[int(1),int(2)]), R))). | |
| 629 | ||
| 630 | not_equal_element(X,Y) :- var(X),!,dif(X,Y). | |
| 631 | not_equal_element(true,X) :- !, | |
| 632 | (X=false -> true | |
| 633 | ; X=true -> fail | |
| 634 | ; add_error_fail(haskell_csp,'Type error in disequality: ',true\=X) | |
| 635 | ). | |
| 636 | not_equal_element(false,X) :- !, | |
| 637 | (X=true -> true | |
| 638 | ; X=false -> fail | |
| 639 | ; add_error_fail(haskell_csp,'Type error in disequality: ',false\=X) | |
| 640 | ). | |
| 641 | not_equal_element(int(X),R) :- !, | |
| 642 | (R=int(Y) -> X\=Y | |
| 643 | ; add_error_fail(haskell_csp,'Type error in disequality: ',int(X)\=R) | |
| 644 | ). | |
| 645 | not_equal_element(setFrom(X),R) :- !, | |
| 646 | (R=setFrom(Y) -> X\=Y | |
| 647 | ; is_a_set(R) -> true | |
| 648 | ; add_error_fail(haskell_csp,'Type error in disequality: ',setFrom(X)\=R) | |
| 649 | ). | |
| 650 | not_equal_element(setFromTo(X,Y),R) :- !, | |
| 651 | (R=setFrom(X2,Y2) -> (X,Y)\=(X2,Y2) | |
| 652 | ; R=setFrom(_) -> true | |
| 653 | ; is_a_set(R) -> expand_symbolic_set(setFromTo(X,Y),ES,equal_element), not_equal_element(ES,R) | |
| 654 | ; add_error_fail(haskell_csp,'Type error in disequality: ',setFromTo(X,Y)\=R) | |
| 655 | ). | |
| 656 | not_equal_element(setValue(X),R) :- !, | |
| 657 | (R=setValue(Y) -> not_equal_setValue(X,Y) | |
| 658 | ; R=setFrom(_) -> true /* infinite set cannot be equal to finite one */ | |
| 659 | ; is_a_set(R) -> expand_symbolic_set(R,setValue(ER),equal_element), not_equal_setValue(X,ER) | |
| 660 | ; add_error_fail(haskell_csp,'Type error in disequality: ',setValue(X)\=R) | |
| 661 | ). | |
| 662 | not_equal_element(list(X),R) :- !, | |
| 663 | (R=list(Y) -> X\=Y | |
| 664 | ; add_error_fail(haskell_csp,'Type error in disequality: ',list(X)\=R) | |
| 665 | ). | |
| 666 | not_equal_element(na_tuple(X),R) :- !, | |
| 667 | (R=na_tuple(Y) -> X\=Y | |
| 668 | ; add_error_fail(haskell_csp,'Type error in disequality: ',na_tuple(X)\=R) | |
| 669 | ). | |
| 670 | not_equal_element(tuple(X),R) :- !, | |
| 671 | ( R=tuple(Y) -> X\=Y | |
| 672 | ; R=record(C,A) -> X=[H|T], (C\=H ; (T\=A , \+equal_interleaved_dot_tuples(T,A))) | |
| 673 | ; add_error_fail(haskell_csp,'Type error in disequality: ',tuple(X)\=R) | |
| 674 | ). | |
| 675 | not_equal_element(record(C,A),R) :- !, | |
| 676 | (atomic(R) -> true | |
| 677 | ; R=record(C2,A2) -> (C\=C2 ; (A\=A2 , \+equal_interleaved_dot_tuples(A,A2))) | |
| 678 | ; R=tuple([H|T]) -> (H\=C ; (A\=T , \+equal_interleaved_dot_tuples(A,T))) | |
| 679 | ; add_error_fail(haskell_csp,'Type error in disequality: ',record(C,A)\=R) | |
| 680 | ). | |
| 681 | not_equal_element(Set,R) :- | |
| 682 | is_a_set(Set), | |
| 683 | expand_symbolic_set(Set,ES,equal_element), | |
| 684 | not_equal_element(ES,R). | |
| 685 | not_equal_element(X,R) :- atomic(X),!, | |
| 686 | (atomic(R) -> X\=R | |
| 687 | ; R=record(_,_) -> fail | |
| 688 | ; add_error_fail(haskell_csp,'Type error in disequality: ',X\=R) | |
| 689 | ). | |
| 690 | not_equal_element(X,Y) :- dif(X,Y). | |
| 691 | ||
| 692 | % we normalise all elements that appear in setValue; dif or \= is sufficient | |
| 693 | not_equal_setValue(X,Y) :- dif(X,Y). | |
| 694 | ||
| 695 | /* expand_symbolic_set */ | |
| 696 | /* force expansion of symbolic sets into explicit sets */ | |
| 697 | ||
| 698 | /* testing the equality: {x*y | x <- {1,3}, y <- {2,4}} == {2,4,6,12} */ | |
| 699 | :- assert_must_succeed(( csp_sets:expand_symbolic_set(setExp(rangeEnum(['*'(_x,_y)] ), | |
| 700 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 701 | comprehensionGenerator(_y,setValue([int(2),int(4)]))] ),R,test), R = setValue([int(2),int(4),int(6),int(12)]))). | |
| 702 | :- assert_must_succeed(( csp_sets:expand_symbolic_set(boolType,R,_X), R == setValue([true,false]))). | |
| 703 | /* testing the equality: {(x,y) | x <- {0..100}, y <- { -99..5}, x+y == 100} == {(95,5),(96,4),(97,3),(98,2),(99,1),(100,0)} */ | |
| 704 | :- assert_must_succeed(( csp_sets:expand_symbolic_set(setExp(rangeEnum([tuplePat([_x,_y])]), | |
| 705 | [comprehensionGenerator(_x,setFromTo(0,100)), | |
| 706 | comprehensionGenerator(_y,setFromTo(-99,5)),comprehensionGuard('=='('+'(_x,_y),'int'(100)))] ),R,test), | |
| 707 | R = setValue([na_tuple([int(95),int(5)]),na_tuple([int(96),int(4)]),na_tuple([int(97),int(3)]), | |
| 708 | na_tuple([int(98),int(2)]),na_tuple([int(99),int(1)]),na_tuple([int(100),int(0)])]))). | |
| 709 | ||
| 710 | %expand_symbolic_set(X,R) :- print(expand_symbolic_set(X,R)),nl,fail. | |
| 711 | expand_symbolic_set(X,R,Context) :- var(X),!, | |
| 712 | add_error(expand_symbolic_set,'Variable argument for expand_symbolic_set, Context: ',Context), | |
| 713 | R=X. | |
| 714 | expand_symbolic_set(dataType(T),R,Context) :- !, R=setValue(SET), | |
| 715 | (dataTypeDef(T,Def) | |
| 716 | -> %print(dt(T,Def,SET)),nl, | |
| 717 | expand_datatypedefbody(Def,T,SET,Context) | |
| 718 | ; add_error(csp_sets,'Could not expand dataType. No datatype definition for: ',T:context(Context)), | |
| 719 | SET=[] | |
| 720 | ). | |
| 721 | expand_symbolic_set(closure(X),R,_Context) :- !, closure_expand(X,R). | |
| 722 | expand_symbolic_set(setValue(X),R,_Context) :- !, R=setValue(X). | |
| 723 | expand_symbolic_set(setFrom(X),R,Context) :- !, add_warning(expand_symbolic_set,'Warning: Tried to expand infinite set: ',setFrom(X):context(Context)),R=setFrom(X). | |
| 724 | expand_symbolic_set(setFromTo(Low,Up),R,_Context) :- !,R=setValue(RS),expand_from_to(Low,Up,RS). | |
| 725 | expand_symbolic_set(setExp(RangeExpr,GeneratorList),R,_Context) :- !, | |
| 726 | expand_set_comprehension(RangeExpr,GeneratorList,R). | |
| 727 | expand_symbolic_set(listFromTo(X,Y),_,Context) :- | |
| 728 | add_error(expand_symbolic_set,'Type error; expected set: ',listFromTo(X,Y):context(Context)),fail. | |
| 729 | expand_symbolic_set(agent_call(Span,F,Par),R,Context) :- !, | |
| 730 | force_evaluate_argument(agent_call(Span,F,Par),RF), | |
| 731 | expand_symbolic_set(RF,R,Context). | |
| 732 | expand_symbolic_set(boolType,R,_Context) :- !, R = setValue([true,false]). | |
| 733 | expand_symbolic_set(dotTupleType(L),R,_Context) :- !, % we want to expand some more complicated Types like {0..2}.({0..2},{0..2}) | |
| 734 | %print(expand_symbolic_set(dotTupleType(L))),nl, | |
| 735 | l_unfold_datatype_dot_tuple([dotTupleType(L)],RL), | |
| 736 | findall(Val,haskell_csp: enumerate_channel_input_value2(dotTupleType(RL),Val,_Ch,2,no_loc_info_available),Set), | |
| 737 | R = setValue(Set). | |
| 738 | expand_symbolic_set(typeTuple(L),R,_Context) :- !, | |
| 739 | haskell_csp: evaluate_type_list(L,LR), | |
| 740 | findall(Val,haskell_csp: enumerate_channel_input_value2(typeTuple(LR),Val,_Ch,2,no_loc_info_available),Set), | |
| 741 | R = setValue(Set). | |
| 742 | expand_symbolic_set(Set,R,Context) :- | |
| 743 | add_error(expand_symbolic_set,'Could not expand set: ',Set:context(Context)),R=Set. | |
| 744 | ||
| 745 | :- block expand_from_to(-,?,?), expand_from_to(?,-,?). | |
| 746 | expand_from_to(X,Y,R) :- expand_from_to2(X,Y,R). | |
| 747 | expand_from_to2(X,Y,R) :- X>Y,!, R=[]. | |
| 748 | expand_from_to2(X,Y,[int(X)|T]) :- X1 is X+1, expand_from_to2(X1,Y,T). | |
| 749 | ||
| 750 | expand_datatypedefbody([],_DT,R,_) :- !, R=[]. | |
| 751 | expand_datatypedefbody([constructor(C)|T],DT,R,Context) :- !, R=[C|ET], | |
| 752 | expand_datatypedefbody(T,DT,ET,Context). | |
| 753 | expand_datatypedefbody([constructorC(Cons,Type)|T],DT,R,Context) :- !, | |
| 754 | (haskell_csp:channel_type_is_finite(Type,2) -> | |
| 755 | findall(Record,csp_sets:expand_constructor_to_record(Cons,DT,2,Record),L), | |
| 756 | append(L,RT,R), | |
| 757 | expand_datatypedefbody(T,DT,RT,Context) | |
| 758 | ; add_error(csp_sets, 'Could not expand infinite datatype body: ',constructorC(Cons,Type):context(Context)),fail | |
| 759 | ). | |
| 760 | expand_datatypedefbody(L,_DT,R,Context) :- | |
| 761 | add_internal_error('Internal Error: Could not expand datatype body (potentially infinite): ',L:context(Context)), | |
| 762 | R=[]. | |
| 763 | ||
| 764 | expand_constructor_to_record(Cons,DT,MaxRec,Res) :- | |
| 765 | Res=record(Cons,_L), | |
| 766 | enumerate_datatype_el(DT,Res,_Channel,MaxRec,no_loc_info_available). | |
| 767 | ||
| 768 | /* ------------------ */ | |
| 769 | /* EXPANDING CLOSURES */ | |
| 770 | /* ------------------ */ | |
| 771 | ||
| 772 | /* csp_sets:closure_expand([tuple([outf])],R),print(R),nl */ | |
| 773 | ||
| 774 | closure_expand(ListOfEls,setValue(ExpandedList)) :- | |
| 775 | %print(closure_expand(ListOfEls)),nl, | |
| 776 | when(ground(ListOfEls), | |
| 777 | (findall(EEl,(member(El,ListOfEls), | |
| 778 | closure_expand_single_element(El,EEl)),EEls), | |
| 779 | %print(expanded(EEls)),nl, | |
| 780 | sort(EEls,ExpandedList) /* is sort ok wrt to @< used by various set operations?? */ | |
| 781 | )). | |
| 782 | ||
| 783 | closure_expand_single_element(tuple([Ch|List]),R) :- | |
| 784 | channel_type_list(Ch,ChannelTypeList),!, R = tuple([Ch|NewList]), | |
| 785 | %print(tuple([Ch|NewList],ChannelTypeList)),nl, | |
| 786 | %% print(gen_expanded_list(ChannelTypeList,List,NewList,Ch)),nl, | |
| 787 | gen_expanded_list(ChannelTypeList,List,NewList,Ch). | |
| 788 | closure_expand_single_element(Cons,C) :- | |
| 789 | is_csp_constructor(Cons),!, | |
| 790 | csp_constructor(Cons,DT,_ArgSubTypes), | |
| 791 | %print(csp_constructor(Cons,DT,_ArgSubTypes)),nl, | |
| 792 | C=record(Cons,_Fields), | |
| 793 | enumerate_datatype_el(DT,C,_Ch,2,no_loc_information). | |
| 794 | closure_expand_single_element(tuple([Ch|_]),_R) :- !, | |
| 795 | add_error(csp_sets,'Cannot compute closure: This is not a defined channel: ',Ch), | |
| 796 | fail. | |
| 797 | closure_expand_single_element(X,_R) :- | |
| 798 | add_error(csp_sets,'Cannot expand closure: ',X), | |
| 799 | fail. | |
| 800 | ||
| 801 | gen_expanded_list([],List,[],Channel) :- | |
| 802 | (List=[] -> | |
| 803 | true | |
| 804 | ; add_error(csp_sets,'Pattern list too long for channel: ',(List,Channel)) | |
| 805 | ). | |
| 806 | gen_expanded_list([Type|TT],List,Res,Channel) :- | |
| 807 | (List=[H|LT] | |
| 808 | -> (is_incomplete_record(H,CompletedH,RecType) | |
| 809 | -> ((LT==[] -> | |
| 810 | true | |
| 811 | ; add_error(gen_expanded_list,'Incomplete Record at non-tail position:',Channel:H) | |
| 812 | ), | |
| 813 | enumerate_channel_input_value(dataType(RecType),CompletedH,Channel,no_loc_info_available), | |
| 814 | %%print(enum(Type,CompletedH,Channel)),nl, | |
| 815 | Res = [CompletedH|RT] | |
| 816 | ) | |
| 817 | ; Res=[H|RT] | |
| 818 | ) | |
| 819 | ; Res=[NewEl|RT],LT=List, /* is it ok not to put dot(NewEl) here ? */ | |
| 820 | enumerate_channel_input_value(Type,NewEl,Channel,no_loc_info_available) | |
| 821 | ), | |
| 822 | gen_expanded_list(TT,LT,RT,Channel). | |
| 823 | ||
| 824 | :- assert_must_succeed((assertz(csp_sets: csp_full_type_constructor(sq,values,[dataType(values), dataType(values)])), | |
| 825 | is_incomplete_record(record(sq,['A']), _R, values), | |
| 826 | retractall(csp_sets:csp_full_type_constructor(_,_,_)))). | |
| 827 | :- assert_must_fail((assertz(csp_sets: csp_full_type_constructor(sq,values,[dataType(values), dataType(values)])), | |
| 828 | is_incomplete_record(record(sq,['A','B']), _R, values), | |
| 829 | retractall(csp_sets:csp_full_type_constructor(_,_,_)))). | |
| 830 | is_incomplete_record(record(Constructor,Fields),record(Constructor,FullFields),Type) :- | |
| 831 | csp_full_type_constructor(Constructor,Type,SubTypes), | |
| 832 | length(SubTypes,NrReqArgs), | |
| 833 | length(Fields,NrFields), | |
| 834 | (NrReqArgs > NrFields | |
| 835 | -> ( %print(record_incomplete(Constructor,Fields,SubTypes)),nl, | |
| 836 | length(FullFields,NrReqArgs), | |
| 837 | append(Fields,_,FullFields) | |
| 838 | %print(completed(record(Constructor,FullFields))),nl | |
| 839 | ) | |
| 840 | ; ((NrReqArgs<NrFields -> add_error(csp_sets,'Too many arguments for record: ',Constructor:Fields) ; true), | |
| 841 | fail) | |
| 842 | ). | |
| 843 | /* ------------------ */ | |
| 844 | /* SET COMPREHENSIONS */ | |
| 845 | /* ------------------ */ | |
| 846 | ||
| 847 | expand_set_comprehension(RangeExpr,GeneratorList,Res) :- | |
| 848 | %%%% print(expand_set_comprehension(RangeExpr,GeneratorList,Res)),nl, | |
| 849 | get_waitvars_for_generator_list(GeneratorList,WaitVars), | |
| 850 | %print(get_waitvars_for_generator_list(GeneratorList,WaitVars)),nl, | |
| 851 | when(ground(WaitVars), generate_set_comprehension_solutions(RangeExpr,GeneratorList,Res)). | |
| 852 | ||
| 853 | generate_set_comprehension_solutions(RangeExpr,GeneratorList,Res) :- | |
| 854 | treat_generators(GeneratorList,GenVars,Sets,Guard), | |
| 855 | findall(EExpr,get_generators_solution(Guard,GenVars,RangeExpr,Sets,EExpr),Expressions), | |
| 856 | %print(force_evaluate_set(Expressions,Res)),nl, | |
| 857 | force_evaluate_set(Expressions,Res).%evaluate_set(Expressions,Res,force_evaluate_argument). | |
| 858 | ||
| 859 | get_generators_solution(Guard,GenVars,RangeExpr,Sets,EExpr) :- | |
| 860 | check_boolean_expression(Guard), | |
| 861 | %print(generator_sol(guard(Guard),GenVars,Sets)),nl, | |
| 862 | generator_sol(GenVars,Sets,set), % unifies the variables of the comprehension generator expressions (e.g. x <- {0..10}) | |
| 863 | %print(checking_range),nl, | |
| 864 | member_range_expr(RangeExpr,EExpr). | |
| 865 | ||
| 866 | /* not used anymore | |
| 867 | % temporary CLPFD will be not used for CSP | |
| 868 | check_boolean_expression_set(Guard) :- | |
| 869 | preference(use_clpfd_solver,true), | |
| 870 | arith_boolean_expression(Guard,EvBExpr),!, | |
| 871 | set_clpfd_constraints(EvBExpr). | |
| 872 | check_boolean_expression_set(Guard) :- | |
| 873 | check_boolean_expression(Guard). | |
| 874 | ||
| 875 | arith_boolean_expression(BExpr,EvBExpr) :- | |
| 876 | functor(BExpr,F,2),arg(1,BExpr,Arg1),arg(2,BExpr,Arg2), | |
| 877 | %BExpr =.. [F,Arg1,Arg2], | |
| 878 | (F == '=='; F == '!='; F == '<'; F == '<='; F == '>'; F == '>='),!, | |
| 879 | cspm_compute_arith_expression(Arg1,EArg1), | |
| 880 | cspm_compute_arith_expression(Arg2,EArg2), | |
| 881 | functor(EvBExpr,F,2),arg(1,EvBExpr,EArg1),arg(2,EvBExpr,EArg2). | |
| 882 | %EBExpr=..[F,EArg1,EArg2]. | |
| 883 | ||
| 884 | set_clpfd_constraints('=='(X,Y)) :- !, | |
| 885 | clpfd_interface:csp_clpfd_eq(X,Y). | |
| 886 | set_clpfd_constraints('!='(X,Y)) :- !, | |
| 887 | clpfd_interface:csp_clpfd_neq(X,Y). | |
| 888 | set_clpfd_constraints('<'(X,Y)) :- !, | |
| 889 | clpfd_interface:csp_clpfd_lt(X,Y). | |
| 890 | set_clpfd_constraints('<='(X,Y)) :- !, | |
| 891 | clpfd_interface:csp_clpfd_leq(X,Y). | |
| 892 | set_clpfd_constraints('>'(X,Y)) :- !, | |
| 893 | clpfd_interface:csp_clpfd_gt(X,Y). | |
| 894 | set_clpfd_constraints('>='(X,Y)) :- !, | |
| 895 | clpfd_interface:csp_clpfd_geq(X,Y). | |
| 896 | ||
| 897 | ||
| 898 | cspm_compute_arith_expression(Expr,Res) :- | |
| 899 | var(Expr),!,Res=Expr. | |
| 900 | cspm_compute_arith_expression('-'(Arg1),Value) :- !, | |
| 901 | cspm_compute_arith_expression(Arg1,SV1), | |
| 902 | Value = '-'(SV1). | |
| 903 | cspm_compute_arith_expression('-'(Arg1,Arg2),Value) :- !, | |
| 904 | cspm_compute_arith_expression(Arg1,SV1), | |
| 905 | cspm_compute_arith_expression(Arg2,SV2), | |
| 906 | Value = '-'(SV1,SV2). | |
| 907 | cspm_compute_arith_expression('+'(Arg1,Arg2),Value) :- !, | |
| 908 | cspm_compute_arith_expression(Arg1,SV1), | |
| 909 | cspm_compute_arith_expression(Arg2,SV2), | |
| 910 | Value = '+'(SV1,SV2). | |
| 911 | cspm_compute_arith_expression('*'(Arg1,Arg2),Value) :- !, | |
| 912 | cspm_compute_arith_expression(Arg1,SV1), | |
| 913 | cspm_compute_arith_expression(Arg2,SV2), | |
| 914 | Value = '*'(SV1,SV2). | |
| 915 | cspm_compute_arith_expression(int(Expr),Expr) :- !. | |
| 916 | */ | |
| 917 | ||
| 918 | ||
| 919 | :- assert_must_succeed((csp_sets: member_range_expr(rangeEnum([int(1),int(2),int(3)]),int(E)), E == 2)). | |
| 920 | :- assert_must_fail((csp_sets: member_range_expr(rangeEnum([]),_E))). | |
| 921 | :- assert_must_succeed((csp_sets: member_range_expr(rangeClosed(int(1),int(5)),int(E)), E == 3)). | |
| 922 | :- assert_must_fail((csp_sets: member_range_expr(rangeClosed(int(3),int(1)),_E))). | |
| 923 | % no lazy-evaluation, argument E must be initialized before calling member_range_expr(rangeOpen(int(_)),E) | |
| 924 | :- assert_must_succeed((E = int(30000), csp_sets: member_range_expr(rangeOpen(int(1)),E))). | |
| 925 | :- assert_must_fail((E = int(1), csp_sets: member_range_expr(rangeOpen(int(3)),E))). | |
| 926 | ||
| 927 | member_range_expr(rangeEnum(ExprList),EExpr) :- !, | |
| 928 | /*(preference(use_clpfd_solver,true),nonvar(ExprList) -> | |
| 929 | %print(expr_list_1(ExprList)),nl, | |
| 930 | term_variables(ExprList,Vars), | |
| 931 | %print(csp_clpfd_labeling([ffc,enum],Vars)),nl, | |
| 932 | clpfd_interface: csp_clpfd_labeling([ffc,enum],Vars) | |
| 933 | ; true | |
| 934 | ),*/ | |
| 935 | member(Expr,ExprList),force_evaluate_argument(Expr,EExpr). | |
| 936 | member_range_expr(rangeClosed(X,Y),EExpr) :- !, | |
| 937 | evaluate_int_argument(X,EX),evaluate_int_argument(Y,EY), | |
| 938 | is_member_set(EExpr,setFromTo(EX,EY)). | |
| 939 | member_range_expr(rangeOpen(X),EExpr) :- !, | |
| 940 | evaluate_int_argument(X,EX), | |
| 941 | is_member_set(EExpr,setFrom(EX)). % could flounder if Guard not specific enough?! | |
| 942 | /* Internal error. CSP-M Parser guarantees that the expression on the left side of | in the parsed comprehension set is one of | |
| 943 | the rangeEnum(-), rangeClosed(_,_) or rangeOpen(-) predicates. */ | |
| 944 | member_range_expr(Range,_) :- | |
| 945 | add_internal_error('Internal Error: Illegal range expr in set comprehension: ',Range),fail. | |
| 946 | ||
| 947 | % compute the variables that have to be ground before expanding a set comprehension: | |
| 948 | get_waitvars_for_generator_list(GeneratorList,WaitVars) :- | |
| 949 | extract_local_variables_from_generator_list(GeneratorList,LocalVars), | |
| 950 | term_variables(GeneratorList,GVars), | |
| 951 | % Do not wait on local variables, they will never be grounded: | |
| 952 | remove_variables(GVars,LocalVars,WaitVars). | |
| 953 | ||
| 954 | % Note: this predicate is also called for the replicated operators ! The expressions can | |
| 955 | % be CSPM agents : do not use force_evaluate | |
| 956 | replicate_expand_set_comprehension(ExprList,GeneratorList,Res) :- | |
| 957 | %% print(replicate_expand_setComp(ExprList,GeneratorList)),nl, %%% | |
| 958 | extract_local_variables_from_generator_list(GeneratorList,LocalVars), | |
| 959 | term_variables(GeneratorList,GVars), | |
| 960 | % Do not wait on local variables, they will never be grounded: | |
| 961 | remove_variables(GVars,LocalVars,WaitVars), | |
| 962 | when(ground(WaitVars), generate_replicate_set_comprehension_solutions(ExprList,GeneratorList,Res)). | |
| 963 | ||
| 964 | generate_replicate_set_comprehension_solutions(ExprList,GeneratorList,Res) :- | |
| 965 | treat_generators(GeneratorList,GenVars,Sets,Guard), | |
| 966 | findall(EExpr,get_replicate_generators_solution(Guard,GenVars,ExprList,Sets,EExpr),Expressions), | |
| 967 | evaluate_set(Expressions,Res).%evaluate_set(Expressions,Res,evaluate_argument). | |
| 968 | ||
| 969 | get_replicate_generators_solution(Guard,GenVars,ExprList,Sets,EExpr) :- | |
| 970 | check_boolean_expression(Guard), | |
| 971 | generator_sol(GenVars,Sets,replicated), % unifies the variables of the comprehension generator expressions (e.g. x <- {0..10}) | |
| 972 | member(Expr,ExprList), | |
| 973 | evaluate_argument(Expr,EExpr). | |
| 974 | ||
| 975 | generator_sol([],[],_Context). | |
| 976 | generator_sol([Pattern|VT],[Set|ST],Context) :- | |
| 977 | (ground(Set) -> true ; print(generator_sol_set_non_ground(Set)),nl), % for nested set comprehension this could actually be non-ground | |
| 978 | translate_pattern(Pattern,TranslPattern), | |
| 979 | % print(evaluated_pattern(TranslPattern,Pattern,Set)),nl, | |
| 980 | (ground(TranslPattern) -> /* we do not need to enumerate; generator variable already ground */ | |
| 981 | force_evaluate_argument_for_member_check(Set,ESet), | |
| 982 | is_member_set_alsoPat(TranslPattern,ESet) | |
| 983 | ; force_evaluate_argument(Set,EvSet), | |
| 984 | is_member_clpfd(TranslPattern,EvSet,Context) | |
| 985 | ), | |
| 986 | % print(gen_is_member(TranslPattern,Pattern,Set)),nl, | |
| 987 | generator_sol(VT,ST,Context). | |
| 988 | ||
| 989 | % constraining the variables domains | |
| 990 | /*is_member_clpfd(Pat,EvSet,set) :- | |
| 991 | preference(use_clpfd_solver,true), | |
| 992 | simple(Pat),check_intset_type(EvSet),!, | |
| 993 | csp_set_pattern_constraints(EvSet,Pat). | |
| 994 | ||
| 995 | csp_set_pattern_constraints(setFrom(Low),Pat) :- !, | |
| 996 | Up=sup, | |
| 997 | clpfd_interface: csp_clpfd_domain([Pat],Low,Up). | |
| 998 | csp_set_pattern_constraints(setFromTo(Low,Up),Pat) :- !, | |
| 999 | clpfd_interface: csp_clpfd_domain([Pat],Low,Up). | |
| 1000 | csp_set_pattern_constraints(setValue(L),Pat) :- !, | |
| 1001 | maplist(expand_int_value,L,LDom), | |
| 1002 | clpfd_interface:csp_in_fdset(Pat,LDom). | |
| 1003 | ||
| 1004 | expand_int_value(int(X),X). | |
| 1005 | ||
| 1006 | check_intset_type(setFrom(_Low)) :- !. | |
| 1007 | check_intset_type(setFromTo(_Low,_Up)) :- !. | |
| 1008 | check_intset_type(setValue(L)) :- | |
| 1009 | maplist(functor1(int,1),L),!. | |
| 1010 | ||
| 1011 | functor1(Name,N,Term) :- | |
| 1012 | functor(Term,Name,N). | |
| 1013 | ||
| 1014 | */ | |
| 1015 | ||
| 1016 | is_member_clpfd(Pat,EvSet,_Context) :- | |
| 1017 | expand_symbolic_set(EvSet,ESet,generator_sol), | |
| 1018 | is_member_set_alsoPat(Pat,ESet). | |
| 1019 | ||
| 1020 | is_member_set_alsoPat(TranslPattern,ESet) :- | |
| 1021 | (nonvar(TranslPattern), | |
| 1022 | TranslPattern = alsoPat(X,Y) -> | |
| 1023 | is_member_set(X,ESet), | |
| 1024 | unify_also_patterns(X,Y) | |
| 1025 | ; is_member_set(TranslPattern,ESet) | |
| 1026 | ). | |
| 1027 | ||
| 1028 | unify_also_patterns(X,Y) :- | |
| 1029 | unify_also_patterns(X,Y,R), | |
| 1030 | evaluate_argument(X,EX), | |
| 1031 | evaluate_argument(Y,EY), | |
| 1032 | ((EX=EY;EY=R) -> true % both patterns should be equal | |
| 1033 | ; add_error_fail(csp_sets, 'Both patterns in the also pattern do not match: ', alsoPat(X,Y)) | |
| 1034 | ). | |
| 1035 | ||
| 1036 | ||
| 1037 | ||
| 1038 | ||
| 1039 | %%%%%%%%%%%% Unit Tests for unify_also_patterns/3 %%%%%%%%%%%%%% | |
| 1040 | :- assert_must_succeed((csp_sets: unify_also_patterns(int(3),int(X),R), X == 3, R == int(3))). | |
| 1041 | :- assert_must_fail((csp_sets: unify_also_patterns(int(3),int(4),_R))). | |
| 1042 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([X,Y,Z]),tuple([c,int(1),int(2)]),R), X == c, Y == int(1), Z == int(2), R == tuple([c,int(1),int(2)]))). | |
| 1043 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([X,_Y]),tuple([c,int(1),int(2)]),R), X == c, R == tuple([c,tuple([int(1),int(2)])]))). | |
| 1044 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([c,int(1),int(2)]),tuple([X,Y,Z]),R), X == c, Y == int(1), Z == int(2), R == tuple([c,int(1),int(2)]))). | |
| 1045 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([c,int(1),int(2)]),tuple([X,_Y]),R), X == c, R == tuple([c,tuple([int(1),int(2)])]))). | |
| 1046 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([c,int(1),int(2),int(3)]),tuple([X,_Y]),R), X == c, R == tuple([c,tuple([int(1),int(2),int(3)])]))). | |
| 1047 | :- assert_must_succeed((csp_sets: unify_also_patterns(record(c,[int(1),int(2)]),record(c,[X,Y]),R), X == int(1), Y == int(2), R == record(c,[int(1),int(2)]))). | |
| 1048 | :- assert_must_succeed((csp_sets: unify_also_patterns(record(c,[int(1),int(2)]),tuple([c,X,Y]),R), X == int(1), Y == int(2), R == record(c,[int(1),int(2)]))). | |
| 1049 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([c,int(1),int(2)]),record(c,[X,Y]),R), X == int(1), Y == int(2), R == record(c,[int(1),int(2)]))). | |
| 1050 | :- assert_must_succeed((csp_sets: unify_also_patterns(tuple([c,int(1),int(2)]),record(c,[_X]),R), R == record(c,[tuple([int(1),int(2)])]))). | |
| 1051 | :- assert_must_succeed((csp_sets: unify_also_patterns(record(c,[int(1),int(2)]),Y,R), Y == record(c,[int(1),int(2)]), R == record(c,[int(1),int(2)]))). | |
| 1052 | :- assert_must_succeed((csp_sets:unify_also_patterns(record(c,[_A]),tuple([c,int(1),na_tuple([int(2),int(3)])]),D), D == record(c,[tuple([int(1),na_tuple([int(2),int(3)])])]))). | |
| 1053 | :- assert_must_succeed((csp_sets: unify_also_patterns(na_tuple([X,Y,Z]),na_tuple([c,int(1),int(2)]),R), X == c, Y == int(1), Z == int(2), R == na_tuple([c,int(1),int(2)]))). | |
| 1054 | :- assert_must_succeed((csp_sets: unify_also_patterns(list([X,Y,Z]),list([c,int(1),int(2)]),R), X == c, Y == int(1), Z == int(2), R == list([c,int(1),int(2)]))). | |
| 1055 | %%%%%%%%%%%% Unit Tests for unify_also_patterns/3 %%%%%%%%%%%%%% | |
| 1056 | ||
| 1057 | unify_also_patterns(X,Y,R) :- (var(X) ; var(Y)), !, X=Y,R=Y. | |
| 1058 | unify_also_patterns(int(X),int(Y),int(R)) :- !,int(X)=int(Y),R=X. | |
| 1059 | unify_also_patterns(tuple(L),Tuple,tuple(R)) :- (Tuple = tuple(L1); Tuple = dotTuple(L1)),!,unify_tuple_elements(L,L1,R,tuple). | |
| 1060 | unify_also_patterns(dotTuple(L),Tuple,tuple(R)) :- (Tuple = tuple(L1); Tuple = dotTuple(L1)),!,unify_tuple_elements(L,L1,R,tuple). | |
| 1061 | unify_also_patterns(X,Y,record(CR,LR)) :- | |
| 1062 | ( X = record(CX,LX) -> !, | |
| 1063 | ( Y=tuple([H|T]) -> CX=H,!,unify_tuple_elements([CX|LX],[H|T],R,tuple),R=[CR|LR] | |
| 1064 | ; Y=dotTuple([H|T]) -> CX=H,!,unify_tuple_elements([CX|LX],[H|T],R,dotTuple),R=[CR|LR] | |
| 1065 | ; Y=record(CY,LY) -> CX=CY,!,unify_tuple_elements([CX|LX],[CY|LY],R,tuple),R=[CR|LR] | |
| 1066 | ; atomic(Y) -> fail % in case we are comparing a record with a simple constructor | |
| 1067 | ; add_error_fail(unify_also_patterns, 'Could not unify values (inside of set comprehension): ',unify_also_patterns(X,Y)) | |
| 1068 | ) | |
| 1069 | ; Y = record(_,_) -> !, unify_also_patterns(Y,X,record(CR,LR)) | |
| 1070 | ; fail). | |
| 1071 | unify_also_patterns(na_tuple(L),na_tuple(L1),na_tuple(R)) :- !,unify_tuple_elements(L,L1,R,na_tuple). | |
| 1072 | unify_also_patterns(list(X),list(Y),list(R)) :- !,if(list(X)=list(Y),R=Y,fail). | |
| 1073 | % add_error_fail(unify_also_patterns,'Unification type failure: ', '='(list(X),list(Y)))). | |
| 1074 | unify_also_patterns(X,Y,_R) :- add_error_fail(csp_sets, 'Could not unify values (inside of set comprehension): ',unify_also_patterns(X,Y)). | |
| 1075 | ||
| 1076 | ||
| 1077 | %%%%%%%%%%%% Unit Tests for unify_tuple_elements/3 %%%%%%%%%%%%%% | |
| 1078 | :- assert_must_succeed((csp_sets: unify_tuple_elements([int(1),int(2)],[int(1),int(2)],R,_), R == [int(1),int(2)])). | |
| 1079 | :- assert_must_succeed((csp_sets: unify_tuple_elements([int(1),int(2),int(3)],[int(1),_X],R,tuple), R == [int(1),tuple([int(2),int(3)])])). | |
| 1080 | :- assert_must_succeed((csp_sets: unify_tuple_elements([int(1),_X],[int(1),int(2),int(3)],R,tuple), R == [int(1),tuple([int(2),int(3)])])). | |
| 1081 | :- assert_must_succeed((csp_sets: unify_tuple_elements([int(0),int(1),int(2),int(3)],[int(0),tuple([int(1),int(2),int(3)])],R,tuple), R == [int(0),int(1),int(2),int(3)])). | |
| 1082 | %%%%%%%%%%%% Unit Tests for unify_tuple_elements/3 %%%%%%%%%%%%%% | |
| 1083 | ||
| 1084 | unify_tuple_elements([],[],R,_TupleType) :- !,R=[]. | |
| 1085 | unify_tuple_elements([HX|TX],[HY|TY],R,TupleType) :- !, | |
| 1086 | unfold_dot_tuples([HX|TX],[HHX|TTX]),unfold_dot_tuples([HY|TY],[HHY|TTY]), %still possible that some tuples() are lurking inside of the dot tuple list | |
| 1087 | ( (TTY = [], var(HHY), TTX \= [], TupleType=tuple) -> unify_to_rest([HHX,TTX], R, TupleType),[HHY]=R | |
| 1088 | ; (TTX = [], var(HHX), TTY \= [], TupleType=tuple) -> unify_to_rest([HHY,TTY], R, TupleType),[HHX]=R | |
| 1089 | ; csp_tuples: unify_arg2(HHX,HHY,HR,no_loc_info_available), unify_tuple_elements(TTX,TTY,TR,TupleType),R = [HR|TR]). | |
| 1090 | % we don't need to raise an exception when we cannot unify the tuple elements. | |
| 1091 | %unify_tuple_elements(X,Y,_R,_TupleType) :- add_error_fail(csp_sets, 'Could not unify values (inside of set comprehension): ', unify_tuple_elements(X,Y)). | |
| 1092 | ||
| 1093 | unify_to_rest(L,R,Tuple) :- | |
| 1094 | flatten(L,FL), | |
| 1095 | functor(Term,Tuple,1),arg(1,Term,FL), | |
| 1096 | R = [Term]. | |
| 1097 | ||
| 1098 | treat_generators(Generators,Pats,Sets,ResGuard) :- | |
| 1099 | treat_generators(Generators,Pats,Sets,true,ResGuard). | |
| 1100 | %,print(treat_generators(Generators,Pats,Sets,true,ResGuard)),nl. | |
| 1101 | ||
| 1102 | treat_generators([],Pats,Sets,Guard,ResGuard) :- | |
| 1103 | Pats=[],Sets=[],ResGuard=Guard. | |
| 1104 | treat_generators([H|T],Pats,Sets,CurGuard,ResGuard) :- | |
| 1105 | (H=comprehensionGenerator(Pat,Set) -> | |
| 1106 | Pats=[Pat|PatT],Sets=[Set|SetT], | |
| 1107 | CurGuard1=CurGuard | |
| 1108 | ;H=comprehensionGuard(Guard) -> | |
| 1109 | PatT=Pats,SetT=Sets, | |
| 1110 | % Choosing the order of the first two arguments does matter. why? (see CSP/ref_becnchmarks/basin_olderog_bank.csp example) | |
| 1111 | clever_bool_and(CurGuard,Guard,CurGuard1) | |
| 1112 | ; | |
| 1113 | add_internal_error('Internal Error: Could not treat Set Comprehension Generator List: ',[H|T]),fail | |
| 1114 | ), | |
| 1115 | treat_generators(T,PatT,SetT,CurGuard1,ResGuard). | |
| 1116 | ||
| 1117 | clever_bool_and(true,X,R) :- !,R=X. | |
| 1118 | clever_bool_and(X,true,R) :- !,R=X. | |
| 1119 | clever_bool_and(G1,G2,bool_and(G1,G2)). | |
| 1120 | ||
| 1121 | :- use_module(probcspsrc(csp_tuples),[is_constructor/3]). | |
| 1122 | % maybe we should use same code as for compile_head_para | |
| 1123 | ||
| 1124 | :- assert_must_succeed((csp_sets:l_translate_pattern([emptySet,set([X]),'Set'(setValue([int(1),int(2)])),dotpat([Y,Z,emptySet])],R), | |
| 1125 | R == [setValue([]),setValue([X]),setValue([int(1),int(2)]),tuple([Y,Z,setValue([])])])). | |
| 1126 | ||
| 1127 | translate_pattern(V,R) :- var(V),!,R=V. | |
| 1128 | translate_pattern(dotpat([X|T]),R) :- nonvar(X), is_constructor(X,Constructor,_SubTypes), | |
| 1129 | l_translate_pattern(T,LT),!, R=record(Constructor,LT). | |
| 1130 | translate_pattern(dotpat(T),R) :- l_translate_pattern(T,LT),!, R=tuple(LT). | |
| 1131 | translate_pattern(tuplePat(T),R) :- l_translate_pattern(T,LT),!, R=na_tuple(LT). | |
| 1132 | translate_pattern(listPat(List),R) :- l_translate_pattern(List,LT),!, R=list(LT). | |
| 1133 | translate_pattern(singleSetPat(List),R) :- l_translate_pattern(List,LT),!, R=setValue(LT). | |
| 1134 | translate_pattern(emptySet,R) :- !, R=setValue([]). | |
| 1135 | translate_pattern(set(List),R) :- l_translate_pattern(List,LT),!, R=setValue(LT). | |
| 1136 | translate_pattern('Set'(S),R) :- !,R=S. | |
| 1137 | translate_pattern(appendPattern([H|T]),R) :- T==[],!, translate_pattern(H,R). | |
| 1138 | translate_pattern(appendPattern([H|T]),R) :- nonvar(H),H=listPat(HH), | |
| 1139 | haskell_csp:is_list_skeleton(HH), | |
| 1140 | l_translate_pattern(HH,LHH), | |
| 1141 | translate_pattern(appendPattern(T),list(LTT)),!, append(LHH,LTT,ResL),R=list(ResL). | |
| 1142 | % more complicated append patterns | |
| 1143 | translate_pattern(alsoPattern([X,Y]),R) :- !, translate_pattern(X,XR),translate_pattern(Y,YR),R = alsoPat(XR,YR). | |
| 1144 | translate_pattern(X,R) :- ground(X),force_evaluate_argument(X,EX),!,R=EX. | |
| 1145 | translate_pattern(X,X) :- | |
| 1146 | add_internal_error('Internal Error: Could not translate pattern: ',X). | |
| 1147 | ||
| 1148 | l_translate_pattern(Patterns,TranslatedPatterns) :- | |
| 1149 | maplist(translate_pattern,Patterns,TranslatedPatterns). | |
| 1150 | ||
| 1151 | :- assert_must_succeed(( is_member_comprehension_set(int(12), | |
| 1152 | rangeEnum(['*'(_x,_y)]), | |
| 1153 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 1154 | comprehensionGenerator(_y,setValue([int(1),int(2),int(4)]))]) )). | |
| 1155 | :- assert_must_fail(( is_member_comprehension_set(int(11), | |
| 1156 | rangeEnum(['*'(_x,_y)]), | |
| 1157 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 1158 | comprehensionGenerator(_y,setValue([int(1),int(2),int(4)]))]) )). | |
| 1159 | :- assert_must_succeed(( is_member_comprehension_set(int(X), | |
| 1160 | rangeEnum(['*'(_x,_y)]), | |
| 1161 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 1162 | comprehensionGenerator(_y,setValue([int(1),int(2),int(4)]))]),X=12 )). | |
| 1163 | /* | |
| 1164 | :- assert_must_succeed(( csp_sets:is_member_comprehension_set(int(X), | |
| 1165 | rangeEnum([XX,YY]),[comprehensionGenerator(XX,setExp(rangeClosed(int(3),int(4)))), | |
| 1166 | comprehensionGenerator(YY,setExp(rangeClosed('+'(int(XX),int(2)),'+'(int(XX),int(3)))))]),X=7 )). | |
| 1167 | */ | |
| 1168 | ||
| 1169 | is_member_comprehension_set(X,rangeEnum(ExprList),GeneratorList) :- ExprList=[Expr|TT],TT==[],var(Expr),!, | |
| 1170 | get_waitvars_for_generator_list(GeneratorList,WaitVars), | |
| 1171 | when(ground(WaitVars), | |
| 1172 | (treat_generators(GeneratorList,Vars,Sets,Guard), | |
| 1173 | % print(treat_generators(for(X,ExprList),Vars,Sets,Guard)),nl, | |
| 1174 | Expr=X, | |
| 1175 | check_boolean_expression(Guard), | |
| 1176 | % print(checked(Guard,Vars,Sets)),nl, | |
| 1177 | generator_sol(Vars,Sets,set))). | |
| 1178 | is_member_comprehension_set(X,ExprList,GeneratorList) :- !, %ExprList = [_,_|_],fail,!, | |
| 1179 | /* if more than one element in ExprList: | |
| 1180 | we need to expand it; we cannot instantiate the single variable and just check the generators,guards | |
| 1181 | otherwise pending co-routines can occur (e.g., { x , x1 | x<-{1..4}, x1 <-{x+2..x+3} } ) | |
| 1182 | Also: currently we cannot check it symbolically if the elment of ExprList is not a variable */ | |
| 1183 | % print(expanding_comprehension_set(ExprList,GeneratorList)),nl, | |
| 1184 | expand_set_comprehension(ExprList,GeneratorList,ExpandedSet), | |
| 1185 | is_member_set(X,ExpandedSet). | |
| 1186 | is_member_comprehension_set(X,T,G) :- | |
| 1187 | add_error_fail(is_member_comprehension_set,'Could not evaluate: ', is_member_comprehension_set(X,T,G)). | |
| 1188 | ||
| 1189 | ||
| 1190 | :- assert_must_succeed(( csp_sets:extract_variables_from_generator_list( | |
| 1191 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 1192 | comprehensionGenerator(_y,setValue([int(1),int(2),int(4)]))],R), | |
| 1193 | R == [_x,_y])). | |
| 1194 | ||
| 1195 | % TODO: does not extract local quantified variables for nested set comprehensions ! | |
| 1196 | % extract locally quantified variables from a set comprehension generator list | |
| 1197 | extract_variables_from_generator_list([],R) :- !,R=[]. | |
| 1198 | extract_variables_from_generator_list([comprehensionGuard(_)|T],Res) :- !, | |
| 1199 | extract_variables_from_generator_list(T,Res). | |
| 1200 | extract_variables_from_generator_list([comprehensionGenerator(Var,Set)|T],Res) :- !, | |
| 1201 | check_variable(Var), | |
| 1202 | extract_variables_from_generator_list(T,TVar), | |
| 1203 | term_variables(Var,Vars), | |
| 1204 | add_variables(Vars,TVar,Res,Set). | |
| 1205 | extract_variables_from_generator_list(X,R) :- | |
| 1206 | add_internal_error('Not a generator list: ', X), | |
| 1207 | R=[]. | |
| 1208 | ||
| 1209 | :- assert_must_succeed(( csp_sets:extract_local_variables_from_generator_list( | |
| 1210 | [comprehensionGenerator(_x,setValue([int(1),int(3)])), | |
| 1211 | comprehensionGenerator(_y,setValue([int(1),int(2),int(4)]))],R), | |
| 1212 | R == [_x,_y])). | |
| 1213 | % TODO: does not extract local quantified variables for nested set comprehensions ! | |
| 1214 | % extract locally quantified variables from a set comprehension generator list | |
| 1215 | extract_local_variables_from_generator_list([],R) :- !,R=[]. | |
| 1216 | extract_local_variables_from_generator_list([comprehensionGuard(_)|T],Res) :- !, | |
| 1217 | extract_local_variables_from_generator_list(T,Res). | |
| 1218 | extract_local_variables_from_generator_list([comprehensionGenerator(Var,Set)|T],Res) :- !, | |
| 1219 | check_variable(Var), | |
| 1220 | extract_local_variables_from_generator_list(T,TVar), | |
| 1221 | term_variables(Var,Vars), | |
| 1222 | add_variables(Vars,TVar,Res1,Set), | |
| 1223 | extract_local_variables_from_set_expression(Set,Res1,Res). | |
| 1224 | extract_local_variables_from_generator_list(X,R) :- | |
| 1225 | add_internal_error('Not a generator list: ', X), | |
| 1226 | R=[]. | |
| 1227 | ||
| 1228 | % TODO: are there any operators we are missing !?? | |
| 1229 | extract_local_variables_from_set_expression(X,I,O) :- var(X),!, | |
| 1230 | %add_error(extract_local_variables_from_set_expression,'Variable expr. :',X), | |
| 1231 | I=O. | |
| 1232 | extract_local_variables_from_set_expression(Set,InVar,OutVar) :- unary_set_op(Set,A),!, | |
| 1233 | extract_local_variables_from_set_expression(A,InVar,OutVar). | |
| 1234 | extract_local_variables_from_set_expression(Set,InVar,OutVar) :- binary_set_op(Set,A,B),!, | |
| 1235 | extract_local_variables_from_set_expression(A,InVar,V1), | |
| 1236 | extract_local_variables_from_set_expression(B,V1,OutVar). | |
| 1237 | extract_local_variables_from_set_expression(setEnum(List),InVar,OutVar) :- !, | |
| 1238 | l_extract_local_variables_from_set_expression(List,InVar,OutVar). | |
| 1239 | extract_local_variables_from_set_expression(closureComp(Generators,Set),In,Out) :- !, | |
| 1240 | extract_local_variables_from_generator_list(Generators,GV), | |
| 1241 | add_variables(GV,In,Out,Set). | |
| 1242 | extract_local_variables_from_set_expression(setExp(RangeExpr,Generators),In,Out) :- !, | |
| 1243 | extract_local_variables_from_generator_list(Generators,GV), | |
| 1244 | add_variables(GV,In,Out,RangeExpr). | |
| 1245 | ||
| 1246 | extract_local_variables_from_set_expression(_Set,In,Out) :- | |
| 1247 | %print(uncovered_set_extract(_Set)),nl, | |
| 1248 | Out=In. | |
| 1249 | % what if we have a set of values, containing e.g. the card operator on setComprehensions !! | |
| 1250 | % TO DO: maybe propagate local variables up in haskell_csp_analyzer.pl and make available to setComp ?? | |
| 1251 | ||
| 1252 | unary_set_op(builtin_call(X),R) :- unary_set_op(X,R). | |
| 1253 | unary_set_op('Union'(A),A). | |
| 1254 | unary_set_op('Inter'(A),A). | |
| 1255 | binary_set_op(builtin_call(X),A,B) :- binary_set_op(X,A,B). | |
| 1256 | binary_set_op(union(A,B),A,B). | |
| 1257 | binary_set_op(diff(A,B),A,B). | |
| 1258 | binary_set_op(inter(A,B),A,B). | |
| 1259 | ||
| 1260 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([],X,Y), Y == X)). | |
| 1261 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([builtin_call(union(S,setExp(rangeEnum([_I])))), | |
| 1262 | builtin_call(union(_X,_Y))],S,Out), Out == S)). | |
| 1263 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([builtin_call(union(_S,setExp(rangeEnum([I])))), | |
| 1264 | builtin_call(union(_X,_Y))],_I,Out), Out == I)). | |
| 1265 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([builtin_call(union(_S,setExp(rangeEnum([_I])))), | |
| 1266 | builtin_call(inter(X,_Y))],X,Out), Out == X)). | |
| 1267 | :- assert_must_succeed((csp_sets: csp_sets: extract_local_variables_from_generator_list([comprehensionGenerator(rangeEnum([Y]),setExp(rangeEnum([X]),[comprehensionGenerator(X,setExp(rangeClosed(int(1),int(4))))]))],L), L == [X,Y])). | |
| 1268 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([setEnum([S,Y,_X]), | |
| 1269 | builtin_call('Inter'(Y))],S,Out), Out == S)). | |
| 1270 | :- assert_must_succeed((csp_sets:l_extract_local_variables_from_set_expression([builtin_call('Union'(_S)), | |
| 1271 | builtin_call('Inter'(Y))],Y,Out), Out == Y)). | |
| 1272 | ||
| 1273 | l_extract_local_variables_from_set_expression(X,I,O) :- var(X),!, | |
| 1274 | add_internal_error(/*l_extract_local_variables_from_set_expression,*/'Variable expr. :',X), I=O. | |
| 1275 | l_extract_local_variables_from_set_expression([],In,Out) :- !, Out = In. | |
| 1276 | l_extract_local_variables_from_set_expression([H|T],In,Out) :- !, | |
| 1277 | extract_local_variables_from_set_expression(H,In,In2), | |
| 1278 | l_extract_local_variables_from_set_expression(T,In2,Out). | |
| 1279 | l_extract_local_variables_from_set_expression(X,In,Out) :- | |
| 1280 | add_internal_error('Unknown expr.: ',X), In=Out. | |
| 1281 | ||
| 1282 | ||
| 1283 | check_variable(V) :- atomic(V), channel(V,_),!, | |
| 1284 | add_error(csp_sets,'Channel name used for local variable: ',V). | |
| 1285 | check_variable(_). | |
| 1286 | ||
| 1287 | add_variables([],TVar,TVar,_). | |
| 1288 | add_variables([Var|T],TVar,Res,Set) :- | |
| 1289 | (exact_member(Var,TVar) | |
| 1290 | -> (add_error(csp_sets,'Variable appears twice in Generator list:', | |
| 1291 | (Var,[comprehensionGenerator(Var,Set)|T])), | |
| 1292 | /* TODO: FIX; this is actually allowed ?? !! */ | |
| 1293 | TVar1 = TVar) | |
| 1294 | ; TVar1 = [Var|TVar]), | |
| 1295 | add_variables(T,TVar1,Res,Set). | |
| 1296 | ||
| 1297 | /* --------- */ | |
| 1298 | /* BIG UNION */ | |
| 1299 | /* --------- */ | |
| 1300 | ||
| 1301 | ||
| 1302 | :- assert_must_succeed(( csp_sets:big_union(setValue([setValue([int(3),int(4)]),setValue([int(2),int(9)])]),R), | |
| 1303 | R == setValue([int(2),int(3),int(4),int(9)]) )). | |
| 1304 | ||
| 1305 | :- block big_union(-,?). | |
| 1306 | big_union(S1,Res) :- %print(big_union(S1,Res)),nl, | |
| 1307 | expand_symbolic_set(S1,setValue(ES1),big_union), | |
| 1308 | %%print(big2(ES1)),nl, | |
| 1309 | big_union_add(ES1,setValue([]),Res). %, print(big_res(Res)),nl. | |
| 1310 | ||
| 1311 | big_union_add([],R,R). | |
| 1312 | big_union_add([H|T],S2,Res) :- union_set(H,S2,S3), | |
| 1313 | big_union_add(T,S3,Res). | |
| 1314 | ||
| 1315 | ||
| 1316 | ||
| 1317 | /* --------- */ | |
| 1318 | /* BIG INTER */ | |
| 1319 | /* --------- */ | |
| 1320 | ||
| 1321 | ||
| 1322 | :- assert_must_succeed(( csp_sets:big_inter(setValue([setValue([int(3),int(4)]),setValue([int(2),int(4)])]),R), | |
| 1323 | R == setValue([int(4)]) )). | |
| 1324 | :- assert_must_succeed(( csp_sets:big_inter(setValue([setValue([int(3),int(4)]),setValue([int(2),int(4)]),setValue([])]),R), | |
| 1325 | R == setValue([]) )). | |
| 1326 | ||
| 1327 | ||
| 1328 | :- block big_inter(-,?). | |
| 1329 | big_inter(S1,Res) :- | |
| 1330 | expand_symbolic_set(S1,setValue(ES1),big_inter), | |
| 1331 | (ES1 = [H|T] | |
| 1332 | -> big_inter_del(T,H,Res) | |
| 1333 | ; (add_error(csp_sets,'At least one set needed for Inter: ','Inter'(S1)), | |
| 1334 | fail) | |
| 1335 | ). | |
| 1336 | ||
| 1337 | big_inter_del([],R,R). | |
| 1338 | big_inter_del([H|T],S2,Res) :- inter_set(H,S2,S3), | |
| 1339 | big_inter_del(T,S3,Res). | |
| 1340 |