1 % (c) 2012-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(kernel_strings, [empty_string/1,
6 string_length/2,
7 string_to_int_wf/4,
8 int_to_string/2,
9 int_to_dec_string/3,
10 string_is_int/2,
11 to_string/2,
12 string_append_wf/4,
13 string_split_wf/4,
14 string_join_wf/5,
15 string_chars/2,
16 string_codes/2,
17 substring_wf/6,
18 format_to_string/3, convert_b_sequence_to_list_of_atoms/3,
19
20 % utilities:
21 split_atom_string/3,
22 generate_code_sequence/3
23 ]).
24
25 % Strings in ProB are represented by terms of the form string(PrologAtom)
26
27 :- use_module(error_manager).
28 :- use_module(self_check).
29 :- use_module(library(lists)).
30
31 :- use_module(module_information,[module_info/2]).
32 :- module_info(group,kernel).
33 :- module_info(description,'This module provides (external) functions to manipulate B strings.').
34
35 empty_string(string('')).
36
37 :- use_module(kernel_objects,[exhaustive_kernel_succeed_check/1,exhaustive_kernel_fail_check/1,
38 exhaustive_kernel_check_wf/2,exhaustive_kernel_fail_check_wf/2]).
39
40 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_length(string(''),int(0)))).
41 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_length(string('a'),int(1)))).
42 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_length(string('aa'),int(2)))).
43 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:string_length(string('a'),int(0)))).
44 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:string_length(string('a'),int(2)))).
45
46 :- use_module(kernel_objects,[greater_than_equal/2]).
47
48 :- block string_length(-,-).
49 string_length(SA,int(L)) :-
50 greater_than_equal(int(L),int(0)),
51 string_len2(SA,L).
52 :- block string_len2(-,-).
53 string_len2(SA,L) :-
54 L==0,!,
55 empty_string(SA).
56 string_len2(string(A),L) :-
57 string_len3(A,L).
58 :- block string_len3(-,-).
59 string_len3(A,L) :-
60 L==0,
61 !,
62 empty_string_atom(A).
63 % in case A is not known and L=1 we could enumerate chars ??
64 string_len3(A,L) :-
65 string_len4(A,L).
66 :- block string_len4(-,?).
67 string_len4(A,L) :-
68 atom_length(A,LL), LL=L. % delay unification due to bug in SICStus atom_length
69 % bug in SICStus: dif(X,1), atom_length(a,X) succeeds in 4.2.0 and 4.2.1
70
71
72 % ----------------------------
73
74
75 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_to_int_wf(string('11'),int(11),unknown,WF),WF)).
76 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_strings:string_to_int_wf(string('11'),int(1),unknown,WF),WF)).
77 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_strings:string_to_int_wf(string('1'),int(11),unknown,WF),WF)).
78 :- assert_must_fail((kernel_strings:string_to_int_wf(S,int(11),u,WF),kernel_strings:string_to_int_wf(S,int(12),u,WF))).
79
80 :- block string_to_int_wf(-,-,?,?).
81 string_to_int_wf(string(S),int(I),Span,WF) :-
82 string_to_int2(S,I,Span,WF).
83
84 :- block string_to_int2(-,-,?,?).
85 string_to_int2(S,Res,Span,WF) :- var(S), % we know the number; we cannot construct the string as leading spaces/0s are ok
86 % with an injective string_to_int conversion we could invert the function
87 !,
88 frozen(S,Goal), %print(s2int(S,Res,Goal)),nl,
89 (incompatible_goal(Goal,S,Res) -> %print(prune(S,Res)),nl,
90 fail ; true),
91 strint_to_int3(S,Res,Span,WF).
92 string_to_int2(S,Res,Span,WF) :- strint_to_int3(S,Res,Span,WF).
93
94 :- use_module(kernel_waitflags,[add_wd_error_set_result/6]).
95 :- block strint_to_int3(-,?,?,?).
96 strint_to_int3(S,Res,Span,WF) :-
97 atom_codes(S,C),
98 on_exception(error(syntax_error(_),_),
99 integer_number_codes(C,S,Res,Span,WF),
100 add_wd_error_set_result('### Could not convert string to integer: ',S,Res,0,Span,WF)).
101 %add_error_and_fail(external_functions,'### Could not convert string to integer: ',S)),
102
103 integer_number_codes(C,S,Res,Span,WF) :-
104 number_codes(Num,C),
105 (integer(Num) -> Res=Num
106 ; %add_error_and_fail(external_functions,'### String represents a floating point number (expected integer): ',S)).
107 add_wd_error_set_result('### String represents a floating point number (expected integer): ',S,Res,0,Span,WF)).
108
109 % check if another pending co-routine transforms the same string into another number
110 incompatible_goal((A,B),S,Res) :-
111 (incompatible_goal(A,S,Res) -> true ; incompatible_goal(B,S,Res)).
112 incompatible_goal(kernel_strings:strint_to_int3(S2,Res2,_,_),S,Res) :-
113 number(Res2),
114 S==S2, Res2 \= Res.
115
116 % ----------------------------
117
118 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_string(int(0),string('0')))).
119 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_string(int(10),string('10')))).
120 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_string(int(-10),string('-10')))).
121 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:int_to_string(int(0),string('1')))).
122 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:int_to_string(int(1),string('01')))).
123
124 % difference to string_to_int: do not throw error when string cannot be converted to integer
125
126 :- block int_to_string(-,?).
127 int_to_string(int(I),S) :- int_to_string2(I,S).
128
129 :- block int_to_string2(-,?).
130 int_to_string2(Num,Res) :-
131 number_codes(Num,C),
132 atom_codes(S,C), Res=string(S).
133
134
135 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string('0'),pred_true))).
136 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string('-10'),pred_true))).
137 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string('1267650600228229401496703205376'),pred_true))). %// 2^100
138 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string('1.0'),pred_false))).
139 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string(''),pred_false))).
140 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_is_int(string('-'),pred_false))).
141
142 :- block string_is_int(-,?).
143 string_is_int(string(S),Res) :-
144 string_is_int2(S,Res).
145
146 :- block string_is_int2(-,?).
147 string_is_int2(S,Res) :-
148 atom_codes(S,C),
149 on_exception(error(syntax_error(_),_),
150 (number_codes(Num,C),
151 (integer(Num)->Res=pred_true;Res=pred_false)),
152 Res=pred_false).
153
154
155 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(0),int(1),string('0.0')))).
156 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(21),int(1),string('2.1')))).
157 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(121),int(2),string('1.21')))).
158 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(101),int(2),string('1.01')))).
159 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(-101),int(2),string('-1.01')))).
160 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(-101),int(3),string('-0.101')))).
161 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(121),int(0),string('121')))).
162 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:int_to_dec_string(int(121),int(-2),string('12100')))).
163
164 :- block int_to_dec_string(-,?,?), int_to_dec_string(?,-,?).
165 int_to_dec_string(int(I),int(Prec),S) :- int_to_dec_string2(I,Prec,S).
166
167 :- block int_to_dec_string2(-,?,?), int_to_dec_string2(?,-,?).
168 int_to_dec_string2(I,Prec,String) :-
169 Prec=<0,
170 !,
171 IP is I * (10^abs(Prec)),
172 int_to_string2(IP,String).
173 int_to_dec_string2(I,Prec,String) :- %Prec>0,
174 PowTen is 10^Prec,
175 IntVal is I // PowTen,
176 number_codes(IntVal,IVC),
177 ((IntVal=0, I<0) -> Prefix = [45|IVC] % need to add leading -
178 ; Prefix = IVC),
179 DecVal is abs(I) mod PowTen,
180 number_codes(DecVal,DVC),
181 length(DVC,Digits),
182 NrZeros is Prec-Digits,
183 length(Zeros,NrZeros),
184 maplist(is_zero,Zeros),
185 append(Zeros,DVC,Suffix),
186 append(Prefix,[46|Suffix],Codes), % 46 is the dot .
187 atom_codes(Atom,Codes),
188 String = string(Atom).
189
190 is_zero(48). % ascii code of zero 0
191 % -------------------
192
193
194 :- use_module(kernel_tools,[ground_value_check/2]).
195
196 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:to_string(int(10),string('10')))).
197 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:to_string(pred_true,string('TRUE')))).
198 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:to_string([],string('{}')))).
199 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:to_string(string('01'),string('01')))).
200 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:to_string(int(1),string('01')))).
201
202 :- block to_string(-,?).
203 to_string(int(I),S) :- !,
204 int_to_string2(I,S).
205 to_string(string(S),Res) :- !,
206 Res=string(S). % we already have a string; nothing needs to be done
207 to_string(Value,S) :- ground_value_check(Value,GrValue), to_string_aux(GrValue,Value,S).
208
209 :- block to_string_aux(-,?,?).
210 to_string_aux(_,Value,Str) :- to_string_aux(Value,Str).
211
212 :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
213 :- use_module(translate,[translate_bvalue/2]).
214 % convert_to_avl
215 to_string_aux(Value,Str) :-
216 normalise_value_for_to_string(Value,NValue),
217 temporary_set_preference(expand_avl_upto,100000,CHNG),
218 translate_bvalue(NValue,Atom),
219 reset_temporary_preference(expand_avl_upto,CHNG),
220 Str=string(Atom).
221
222
223 :- use_module(store,[normalise_value_for_var/3]).
224 % normalise_value_for_var normalises values for storing; for printing we need to do less work
225 % e.g., we do not need to normalise AVL values; we could add further cases for records ...
226 normalise_value_for_to_string(avl(A),R) :- !, R=avl(A).
227 normalise_value_for_to_string((A,B),R) :- !, R=(NA,NB),
228 normalise_value_for_to_string(A,NA),
229 normalise_value_for_to_string(B,NB).
230 normalise_value_for_to_string(A,R) :- normalise_value_for_var(to_string,A,R).
231
232
233
234 % -------------------
235
236 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_append_wf(string('a'),string('b'),string('ab'),WF),WF)).
237 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_append_wf(string('0'),string('1'),string('01'),WF),WF)).
238 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_append_wf(string('aa'),string(''),string('aa'),WF),WF)).
239 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_append_wf(string(''),string('aa'),string('aa'),WF),WF)).
240 :- assert_must_succeed(exhaustive_kernel_fail_check_wf(kernel_strings:string_append_wf(string('0'),string('1'),string('1'),WF),WF)).
241
242 :- block string_append_wf(-,?,-,?), string_append_wf(?,-,-,?).
243 string_append_wf(string(A),string(B),string(C),WF) :- %print(app(A,B,C)),nl,
244 app2(A,B,C,WF).
245 :- block app2(-,?,-,?), app2(?,-,-,?).
246 app2(A,B,C,_WF) :- %print(app2(A,B,C)),nl,
247 nonvar(A),nonvar(B),!,atom_concat(A,B,CC), /* overcome bug in SICStus; delay unification */
248 CC=C. %, print(app2(A,B,C)),nl.
249 app2(A,B,C,WF) :- atom_codes(C,CC), app3(A,B,CC,WF).
250
251 :- use_module(kernel_waitflags,[get_wait_flag/4]).
252 app3(A,B,CC,WF) :-
253 ( nonvar(B) -> atom_codes(B,BB), append(AA,BB,CC), atom_codes(A,AA)
254 ; nonvar(A) -> atom_codes(A,AA), append(AA,BB,CC), atom_codes(B,BB)
255 ; length(CC,CLen), %print(enum(CC,CLen)),nl,
256 get_wait_flag(CLen,'STRING_APPEND',WF,LWF),
257 app4(A,B,CC,WF,LWF)
258 ).
259 :- block app4(-,?,-,?,-), app4(?,-,-,?,-).
260 app4(A,B,CC,WF,_) :- (nonvar(A) ; nonvar(B)), !, % no need to enumerate
261 app3(A,B,CC,WF).
262 app4(A,B,CC,_WF,_) :- %print(enumerating(CC)),nl,
263 append(AA,BB,CC), % will be non-deterministic
264 atom_codes(A,AA), atom_codes(B,BB).
265
266 % -------------------------------------------------
267
268 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_split_wf(string('01001'),string('1'),[(int(1),string('0')),(int(2),string('00')),(int(3),string(''))],no_wf_available))).
269 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_split_wf(string('789'),string('1'),[(int(1),string('789'))],no_wf_available))).
270 :- assert_must_succeed(exhaustive_kernel_fail_check(kernel_strings:string_split_wf(string('aaa'),string('a'),[(int(1),string('a')),(int(2),string('a'))],no_wf_available))).
271
272 % function to split a string into a list of strings which were delimited by a separator
273 % WARNING: if the seperator is of length more than one, then first match-strategy will be used
274 :- block string_split_wf(?,-,?,?), string_split_wf(-,?,-,?).
275 string_split_wf(string(A),string(B),R,WF) :-
276 string_split2(A,B,R,WF).
277 :- block string_split2(?,-,?,?),string_split2(-,?,-,?).
278 string_split2(Atom,Seperator,SplitAtomList,WF) :-
279 (var(Atom) ; var(Seperator)),
280 !, % currently : separator always known
281 expand_custom_set_to_list(SplitAtomList,ExpandedSplitAtomList,Done,string_split2),
282 string_split3(Atom,Seperator,SplitAtomList,Done,ExpandedSplitAtomList,WF).
283 string_split2(Atom,Separator,SplitAtomList,WF) :- % normal forward mode: atom and separator known:
284 string_split_forward(Atom,Separator,SplitAtomList,WF).
285
286 string_split_forward(Atom,Separator,SplitAtomList,WF) :-
287 split_atom_string(Atom,Separator,List), % safe_call ?
288 convert_prolog_to_b_list(List,SplitAtomList,WF).
289
290 :- block string_split3(?,-,?,?,?,?),string_split3(-,?,?,-,?,?). % we need to know the seperator: TO DO : improve this
291 string_split3(Atom,Seperator,SplitAtomList,Done,_ExpandedSplitAtomList,WF) :-
292 var(Done),
293 !,
294 string_split_forward(Atom,Seperator,SplitAtomList,WF).
295 string_split3(Atom,Seperator,SplitAtomList,_Done,ExpandedSplitAtomList,WF) :-
296 ExpandedSplitAtomList \= [], % split("",sep) --> [""] not the empty list; note: this is not a WD error, the constraint STRING_SPLIT(a,b) = [] is simply unsatisfiable
297 !,
298 sort(ExpandedSplitAtomList,SL),
299 maplist(drop_index,SL,IL), % also: no WD error needs to be raised if this is not a sequence
300 convert_b_to_prolog_atoms(IL,PL,Done),
301 atom_codes(Seperator,SepCodes),
302 append(SepCodes,_,SepCodes2),
303 split4(Done,SepCodes2,PL,Seperator,Atom,SplitAtomList,WF).
304
305
306 :- use_module(probsrc(tools_strings),[ajoin/2]).
307
308 :- block split4(-,?,?,?,-,?,?), split4(-,?,?,-,?,?,?).
309 % unblock either when Done or when both Atom and Sperator known
310 split4(Done,_SepCodes2,_PL,Seperator,Atom,SplitAtomList,WF) :-
311 var(Done),
312 !,
313 % we can now compute forwards anyhow; ignore backwards direction
314 string_split_forward(Atom,Seperator,SplitAtomList,WF).
315 split4(_,SepCodes2,PL,Seperator,Atom,_,_) :-
316 maplist(not_suffix_atom(SepCodes2),PL), % check that seperator occurs in no split atom: e.g. STRING_SPLIT(r,"_") = ["a","_","c"] should fail
317 insert_sep(PL,Seperator,PL2),
318 ajoin(PL2,Atom).
319
320 insert_sep([],_,[]).
321 insert_sep([H],_,R) :- !, R=[H].
322 insert_sep([H|T],Sep,[H,Sep|IT]) :- insert_sep(T,Sep,IT).
323
324 not_suffix_atom(SepCodes,Atom) :- \+ suffix_atom(SepCodes,Atom).
325 suffix_atom(SepCodes,Atom) :-
326 atom_codes(Atom,AL),
327 append(_,SepCodes,AL).
328
329 % ------------------------
330
331 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_join_wf([(int(1),string('0')),(int(2),string('00')),(int(3),string(''))],string('1'),string('01001'),unknown,WF),WF)).
332 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_join_wf([(int(1),string('0')),(int(2),string('00'))],string('1'),string('0100'),unknown,WF),WF)).
333 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:string_join_wf([(int(1),string('0'))],string('1'),string('0'),unknown,WF),WF)).
334
335 :- block string_join_wf(?,-,?,?,?), string_join_wf(-,?,?,?,?).
336 string_join_wf(SplitAtoms,string(Sep),Res,Span,WF) :- string_join2(SplitAtoms,Sep,Res,Span,WF).
337
338 % this is not reversible ["a","b"],"_" -> "a_b" but ["a_b"],"_" -> "a_b" has same result
339 :- block string_join2(?,-,?,?,?),string_join2(-,?,?,?,?).
340 string_join2(SplitAtomList,Seperator,Result,Span,WF) :-
341 expand_custom_set_to_list_wf(SplitAtomList,ExpandedSplitAtomList,Done,string_join2,WF),
342 string_join3(Result,Seperator,SplitAtomList,Done,ExpandedSplitAtomList,Span,WF).
343
344 :- use_module(kernel_objects,[equal_object/3, equal_object_optimized_wf/4, equal_object_wf/4]).
345 :- block string_join3(?,-,?,?,?,?,?),string_join3(?,?,?,-,?,?,?). % we need to know the seperator: TO DO : improve this
346 string_join3(Result,Seperator,_SplitAtomList,_Done,ExpandedSplitAtomList,Span,WF) :-
347 %ExpandedSplitAtomList \= [], % commented out this means that STRING_JOIN([],sep) = ""
348 % result of split("",sep) --> [""] : this is not the empty list; i.e., STRING_JOIN is then no longer injective
349 !,
350 sort(ExpandedSplitAtomList,SL),
351 drop_index_with_seq_check(SL,1,IL,Span,WF),
352 convert_b_to_prolog_atoms(IL,PL,Done2),
353 when(nonvar(Done2),
354 (insert_sep(PL,Seperator,PL2),
355 ajoin(PL2,Atom),
356 equal_object_optimized_wf(Result,string(Atom),string_join,WF))).
357 %string_join3(Result,_Seperator,SplitAtomList,_Done,[],Span,WF) :-
358 % add_wd_error_set_result('### STRING_JOIN not defined for empty sequence: ',SplitAtomList,Result,string(''),Span,WF).
359
360 % -----------------------
361
362 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_chars(string(''),[]))).
363 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_chars(string('010'),[(int(1),string('0')),(int(2),string('1')),(int(3),string('0'))]))).
364 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_chars(string('a'),[(int(1),string('a'))]))).
365
366 :- block string_chars(-,-).
367 % to do: make it reversible
368 string_chars(Str,SeqRes) :- nonvar(Str), Str=string(A), ground(A),!,
369 string_chars2(A,SeqRes).
370 string_chars(Str,SeqRes) :- when((ground(Str);ground(SeqRes)),string_chars1(Str,SeqRes)).
371
372 string_chars1(Str,SeqRes) :- nonvar(Str), Str=string(A), ground(A),!,
373 string_chars2(A,SeqRes).
374 string_chars1(Str,SeqRes) :-
375 expand_custom_set_to_list(SeqRes,ExpandedAtomList,Done,string_chars1),
376 string_chars3(Str,SeqRes,ExpandedAtomList,Done).
377
378 :- use_module(kernel_objects,[equal_object_optimized/3]).
379 string_chars2(A,SeqRes) :- atom_codes(A,AA), generate_char_seq(AA,1,CharSeq),
380 equal_object_optimized(CharSeq,SeqRes,string_chars2).
381
382 :- use_module(probsrc(tools_strings),[ajoin/2]).
383
384 :- block string_chars3(-,?,?,-).
385 string_chars3(Str,SeqRes,_ExpandedAtomList,_Done) :-
386 nonvar(Str), Str=string(A), ground(A),
387 !,
388 string_chars2(A,SeqRes).
389 string_chars3(Str,_SeqRes,ExpandedAtomList,Done) :-
390 nonvar(Done),
391 !,
392 sort(ExpandedAtomList,SL),
393 maplist(drop_index,SL,IL),
394 kernel_strings:convert_b_to_prolog_atoms(IL,PL,Done2),
395 when(nonvar(Done2),
396 (ajoin(PL,Atom),
397 equal_object(Str,string(Atom),string_chars))).
398 string_chars3(Str,SeqRes,ExpandedAtomList,Done) :- % Str is only partially instantiated
399 when((ground(Str);nonvar(Done)),string_chars3(Str,SeqRes,ExpandedAtomList,Done)).
400 generate_char_seq([],_,[]).
401 generate_char_seq([Code|T],Nr,[(int(Nr),string(CS))|TSeq]) :-
402 atom_codes(CS,[Code]),
403 N1 is Nr+1, generate_char_seq(T,N1,TSeq).
404
405 drop_index((int(_),R),R).
406
407 :- block drop_index_with_seq_check(-,?,?,?,?).
408 drop_index_with_seq_check([],_,[],_,_).
409 drop_index_with_seq_check([(int(Nr),R)|T],Expected,[R|TR],Span,WF) :-
410 (Nr=Expected -> E1 is Expected+1, drop_index_with_seq_check(T,E1,TR,Span,WF)
411 ; ajoin(['### Unexpected index: ',Nr,'! Argument for STRING_JOIN is not a sequence! Expected next index to be: '],Msg),
412 add_wd_error_set_result(Msg,Expected,TR,[],Span,WF)
413 ).
414
415 % ------------------------
416
417 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_codes(string(''),[]))).
418 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:string_codes(string('010'),[(int(1),int(48)),(int(2),int(49)),(int(3),int(48))]))).
419
420 :- block string_codes(-,-).
421 string_codes(string(A),SeqRes) :- string_codes2(A,SeqRes).
422
423 :- use_module(custom_explicit_sets,[expand_custom_set_to_list/4, expand_custom_set_to_list_wf/5]).
424
425 :- block string_codes2(-,-).
426 string_codes2(A,SeqRes) :-
427 nonvar(A),
428 !,
429 string_codes4(A,SeqRes).
430 string_codes2(A,SeqRes) :-
431 SeqRes==[],
432 !,
433 empty_string_atom(A).
434 string_codes2(A,SeqRes) :- expand_custom_set_to_list(SeqRes,SeqList,_,string_codes2),
435 when((nonvar(A);ground(SeqList)), string_codes3(A,SeqList)).
436
437 string_codes3(A,SeqRes) :-
438 nonvar(A),
439 !,
440 string_codes4(A,SeqRes).
441 string_codes3(A,SeqRes) :-
442 sort(SeqRes,SSeqRes),
443 extract_codes(SSeqRes,1,Codes),
444 atom_codes(A,Codes).
445 string_codes4(A,SeqRes) :-
446 atom_codes(A,AA), generate_code_sequence(AA,1,CodeSeq),
447 equal_object_optimized(CodeSeq,SeqRes,string_codes4).
448
449 generate_code_sequence([],_,[]).
450 generate_code_sequence([Code|T],Nr,[(int(Nr),int(Code))|TSeq]) :-
451 N1 is Nr+1, generate_code_sequence(T,N1,TSeq).
452
453 extract_codes([],_,[]).
454 extract_codes([(int(Nr),int(Code))|T],N,[Code|CT]) :-
455 (Nr==N -> true ; add_error(extract_codes,'Unexpected index: ',(Nr,N))),
456 N1 is N+1, extract_codes(T,N1,CT).
457
458
459 empty_string_atom('').
460
461 % ------------------------
462
463 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:substring_wf(string(abcd),int(1),int(2),string(ab),unknown,WF),WF)).
464 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:substring_wf(string(abcd),int(1),int(6),string(abcd),unknown,WF),WF)).
465 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:substring_wf(string(abcd),int(4),int(6),string(d),unknown,WF),WF)).
466 :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_strings:substring_wf(string(abcd),int(4),int(0),string(''),unknown,WF),WF)).
467
468
469 :- block substring_wf(-,?,?,?,?,?),substring_wf(?,-,?,?,?,?),substring_wf(?,?,-,?,?,?).
470 substring_wf(string(S),int(From),int(Len),Res,Span,WF) :-
471 substring(S,From,Len,Res,Span,WF).
472
473 :- block substring(-,?,?,?,?,?),substring(?,-,?,?,?,?),substring(?,?,-,?,?,?).
474 substring(_,From,_Len,Res,Span,WF) :- From<1,!,
475 add_wd_error_set_result('### From index for SUB_STRING must be positive: ',From,Res,string(''),Span,WF).
476 substring(S,From,Len,Res,_Span,_WF) :-
477 PrefixLen is From-1, Length=Len,
478 (Length < 1 -> empty_string_atom(ResAtom)
479 ; atom_codes(S,Codes),
480 (sublist(Codes, SelectedCodes, PrefixLen , Length, _)
481 -> true
482 ; sublist(Codes, SelectedCodes, PrefixLen , RealLength, 0),
483 RealLength < Length
484 -> true
485 ; empty_string_atom(ResAtom) % Deal with case that PrefixLen beyond length of string
486 ),
487 atom_codes(ResAtom,SelectedCodes)
488 ),
489 Res = string(ResAtom).
490
491
492
493
494 % ------------------------
495
496 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:format_to_string(string('abc'),[],string('abc')))).
497 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:format_to_string(string('abc~wfg'),[(int(1),string('de'))],string('abcdefg')))).
498 :- assert_must_succeed(exhaustive_kernel_succeed_check(kernel_strings:format_to_string(string('abc~wfg~w'),[(int(1),string('de')),(int(2),string('h'))],string('abcdefgh')))).
499
500 :- block format_to_string(-,?,?).
501 format_to_string(string(FormatString),BSeqOfValues,Res) :-
502 convert_b_sequence_to_list_of_atoms(BSeqOfValues,ListOfAtoms,Done),
503 format_to_string_aux(Done,FormatString,ListOfAtoms,Res).
504
505 :- use_module(library(codesio),[format_to_codes/3]).
506 :- block format_to_string_aux(-,?,?,?), format_to_string_aux(?,-,?,?).
507 format_to_string_aux(_,FormatString,ListOfAtoms,Res) :-
508 % print(format_to_codes(FormatString,Atoms,Codes)),nl,
509 format_to_codes(FormatString,ListOfAtoms,Codes),
510 atom_codes(Atom,Codes),
511 Res = string(Atom).
512
513 :- use_module(custom_explicit_sets,[is_set_value/2, expand_custom_set_to_list_gg/4]).
514
515 % convert a B sequence into a list of atoms; pretty printing if necessary
516 :- block convert_b_sequence_to_list_of_atoms(-,?,?).
517 convert_b_sequence_to_list_of_atoms(BSeqOfValues,Res,Done) :-
518 is_set_value(BSeqOfValues,convert_b_sequence_to_list_of_atoms),
519 !,
520 expand_custom_set_to_list_gg(BSeqOfValues,ESet,GG,kernel_strings), % could use _gg version
521 (GG=guaranteed_ground -> GrESet=true ; ground_value_check(ESet,GrESet)),
522 convert_aux(GrESet,ESet,Res,Done).
523 convert_b_sequence_to_list_of_atoms(SingleValue,[S],Done) :-
524 translate_bvalue(SingleValue,XS),
525 add_warning(kernel_strings,'B sequence expected, obtained single value: ',XS),
526 ground_value_check(SingleValue,GrValue), to_string_aux(GrValue,SingleValue,string(S)), Done=GrValue.
527
528 :- block convert_aux(-,?,?,?), convert_aux(?,-,?,?).
529 convert_aux(_,ESet,ListOfAtoms,Done) :-
530 sort(ESet,SortedESet),
531 maplist(get_string,SortedESet,ListOfAtoms),
532 Done=true.
533
534 get_string((_,string(S)),R) :- !,R=S.
535 get_string((_,X),R) :- !,to_string_aux(X,string(R)).
536 get_string(X,R) :-
537 translate_bvalue(X,XS),
538 add_warning(kernel_strings,'B sequence expected, obtained set containing: ',XS),
539 to_string_aux(X,string(R)).
540
541
542 % ------------------------
543 % UTILITIES
544 % ------------------------
545
546
547 :- assert_must_succeed((kernel_strings:split_atom_string('ef,g',',',R), R==[ef,g])).
548 :- assert_must_succeed((kernel_strings:split_atom_string('ab,cd,ef,g',',',R), R==['ab','cd',ef,g])).
549 :- assert_must_succeed((kernel_strings:split_atom_string('ab','a',R), R==['','b'])).
550 :- assert_must_succeed((kernel_strings:split_atom_string('','a',R), R==[''])).
551 :- assert_must_succeed((kernel_strings:split_atom_string('STRING1','',R), R==['STRING1'])).
552 :- assert_must_succeed((kernel_strings:split_atom_string('mod274,mod276,mod277,mod282,mod283,mod284,mod285,mod286',',',R), R==[mod274,mod276,mod277,mod282,mod283,mod284,mod285,mod286])).
553
554 split_atom_string(Atom,Sep,SplitList) :- %print(split_atom_string(Atom,Sep)),nl,
555 atom_chars(Sep,SepAscii),
556 (SepAscii=[] -> SplitList = [Atom]
557 ; SepAscii = [H|T], atom_chars(Atom,ListAscii),
558 split3(ListAscii,H,T,Match,Match,SplitList)).
559
560 % MatchSoFar is passed in two variables: one to instantiate and one with the Result of the match
561 % this avoids calling reverse
562 split3([],_,_,MatchSoFarIn,MatchSoFarRes,R) :- !,
563 MatchSoFarIn=[], % match complete, ground tail of match
564 atom_chars(Atom,MatchSoFarRes),R=[Atom].
565 split3([H|List],H,Sep,MatchSoFarIn,MatchSoFarRes,Res) :-
566 append(Sep,Tail,List),
567 !, % we have a match with a separator
568 MatchSoFarIn=[], % match complete
569 atom_chars(Atom,MatchSoFarRes),
570 Res=[Atom|R2], split3(Tail,H,Sep,NewMatch,NewMatch,R2).
571 split3([H|T],HS,Sep,[H|MatchSoFarIn],MatchSoFarRes,Res) :- % no match
572 split3(T,HS,Sep,MatchSoFarIn,MatchSoFarRes,Res).
573
574
575
576 % -----------------------
577 :- use_module(custom_explicit_sets,[try_expand_and_convert_to_avl/2]).
578
579 convert_prolog_to_b_list(PL,BL,WF) :-
580 convert_prolog_to_b_list_aux(PL,1,CPL),
581 try_expand_and_convert_to_avl(CPL,CPL2),
582 equal_object_wf(CPL2,BL,convert_prolog_to_b_list,WF).
583
584
585 convert_prolog_to_b_list_aux([],_,[]).
586 convert_prolog_to_b_list_aux([H|T],Index,[(int(Index),CH)|CT]) :-
587 convert_prolog_to_b_term(H,CH),
588 I1 is Index+1, convert_prolog_to_b_list_aux(T,I1,CT).
589
590 convert_prolog_to_b_term(N,R) :-
591 number(N),!,
592 R=int(N).
593 convert_prolog_to_b_term(A,R) :-
594 atomic(A),!,
595 R=string(A).
596 convert_prolog_to_b_term(A,R) :-
597 add_internal_error('Illegal Prolog term: ',convert_prolog_to_b_term(A,R)), R=A.
598
599
600 % a version that delays converting and sets Done to done when all B Atoms have been grounded
601 :- block convert_b_to_prolog_atoms(-,?,?).
602 convert_b_to_prolog_atoms([],[],done).
603 convert_b_to_prolog_atoms([BAtom|T],[PrologAtom|PT],Done) :-
604 convert_b_to_prolog_atoms_aux(BAtom,PrologAtom,DoneAtom),
605 convert_b_to_prolog_atoms(T,PT,DoneT),
606 both_done(DoneAtom,DoneT,Done).
607
608 :- block both_done(-,?,?), both_done(?,-,?).
609 both_done(_,_,done).
610
611 :- block convert_b_to_prolog_atoms_aux(-,?,?).
612 convert_b_to_prolog_atoms_aux(pred_true,'TRUE',done).
613 convert_b_to_prolog_atoms_aux(pred_false,'FALSE',done).
614 convert_b_to_prolog_atoms_aux(string(S),PrologAtom,Done) :-
615 convert_b_to_prolog_atoms_aux2(S,PrologAtom,Done).
616 convert_b_to_prolog_atoms_aux(int(S),PrologAtom,Done) :-
617 convert_b_to_prolog_atoms_aux2(S,PrologAtom,Done).
618
619 :- block convert_b_to_prolog_atoms_aux2(-,?,?).
620 convert_b_to_prolog_atoms_aux2(Atom,Atom,done).