| 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 | | |