1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2025-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5
6		:- module(prover_utils,[member_hyps/2, equal_terms/2,
7		rewrite/4, with_ids/2, rewrite_pairwise/4, rewrite_pairwise_rev/4,
8		member_of/3, member_of_bin_op/3,
9		select_op/4, select_op/5,
10		op_to_list/3, list_to_op/3,
11		remove_duplicates_for_op/3, without_duplicates/2,
12		negate/2,
13		new_identifier/2, used_identifiers/2, used_identifiers_list/2, possible_identifier/1,
14		range_ids/3, new_identifiers/3, new_aux_identifier/2,
15		free_identifiers/2,
16		is_fun/4, is_rel/4, is_surj/3, is_inj/3,
17		is_natural_set/1, is_natural1_set/1, is_integer_set/1,
18		is_less_eq/3, is_less/3, is_equality/3, is_inequality/3,
19		comparison/1,
20		sym_unify/4, is_inter/3, is_minus/2, is_empty/2, is_negation/2,
21		of_integer_type/2, singleton_set/2,
22		split_composition/3,
23		type_expression/2, get_type_expression/2, is_deferred_or_enumerated_set/2,
24		get_typed_identifiers/2, get_typed_identifiers/3,
25		get_meta_info/3, update_meta_infos/4, add_meta_info/4, remove_meta_info/4,
26		translate_norm_expr_term/2, create_descr/3, create_descr/4]).
27
28
29		:- use_module(probsrc(module_information),[module_info/2]).
30		:- module_info(group,sequent_prover).
31		:- module_info(description,'This module provides hyp managament and other utilities on sequents and hyps').
32
33		:- use_module(library(lists)).
34		:- use_module(probsrc(tools),[ajoin/2, list_difference/3]).
35
36		member_hyps(Goal,Hyps) :-
37	?	(member(Goal,Hyps) -> true
38		; equiv(Goal,G2), member(G2,Hyps) -> true), !.
39		member_hyps(Goal,Hyps) :-
40		ground(Goal),
41	?	member(G2,Hyps),
42	?	comparable(Goal,G2),
43		list_representation(Goal,L1),
44		list_representation(G2,L2),
45		equal_length(L1,L2),
46	?	stronger_list(L2,L1).
47
48
49		% replace by normalisation
50		equiv(equal(A,B),equal(B,A)).
51		equiv(not_equal(A,B),not_equal(B,A)).
52		equiv(greater(A,B),less(B,A)).
53		equiv(less(A,B),greater(B,A)).
54		equiv(greater_equal(A,B),less_equal(B,A)).
55		equiv(less_equal(A,B),greater_equal(B,A)).
56
57		% ----------------
58
59		% rewrite X to E
60		rewrite(X,Y,E,NewE) :- equal_terms(X,E),!, NewE=Y.
61		rewrite(_X,_Y,E,NewE) :- atomic(E),!, NewE=E.
62		rewrite(_X,_Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
63		rewrite(X,_,E,NewE) :- with_ids(E,Ids), member(X,Ids),!, NewE=E.
64		rewrite(X,Y,C,NewC) :- C=..[Op|Args],
65		l_rewrite(Args,X,Y,NewArgs),
66		NewC =.. [Op|NewArgs].
67
68		l_rewrite([],_,_,[]).
69		l_rewrite([H|T],X,Y,[RH|RT]) :- rewrite(X,Y,H,RH), l_rewrite(T,X,Y,RT).
70
71		with_ids(exists(Ids,_),Ids).
72		with_ids(event_b_comprehension_set(Ids,_,_),Ids).
73		with_ids(forall(Ids,_,_),Ids).
74		with_ids(quantified_union(Ids,_,_),Ids).
75		with_ids(quantified_intersection(Ids,_,_),Ids).
76
77
78		rewrite_pairwise_rev(Ids1,Ids2,P,NewP) :-
79		reverse(Ids1,RevIds1),
80		reverse(Ids2,RevIds2),
81		rewrite_pairwise(RevIds1,RevIds2,P,NewP).
82
83		rewrite_pairwise([],[],E,E).
84		rewrite_pairwise([X|TX],[Y|TY],E,Res) :-
85		rewrite(X,Y,E,NewE),
86		rewrite_pairwise(TX,TY,NewE,Res).
87
88		% ----------------
89
90		equal_terms(X,Y) :- nonvar(X),simple_term_to_unify(X), !, Y=X. % avoid normalising Y
91		equal_terms(X,Y) :- nonvar(Y),simple_term_to_unify(Y), !, X=Y. % ditto for X
92		equal_terms(X,X) :- !.
93		equal_terms(X,Y) :- % both must be nonvar; otherwise unification would have succeeded
94	?	(cannot_change_functor(X,F) -> functor(Y,F,_) ; cannot_change_functor(Y,F) -> functor(X,F,_) ; true),
95		ground(X), ground(Y),
96		list_representation(X,LX),
97		list_representation(Y,LY),
98		equal_op(LX,LY),
99		equal_length(LX,LY),
100		equal_lists(LX,LY).
101
102		% true if list_representation cannot change functor and no other functor can generate it
103		% useful to quickly check top-level functor before normalising full terms
104		% TODO: extend; basically only arithmetic operators are simplified, and can be changed into numbers
105		% TODO: not sure the exclude zero/one rules should be part of equal_terms? can Rodin replay those?
106		cannot_change_functor(implication(_,_),implication).
107		cannot_change_functor(equal(_,_),equal).
108		cannot_change_functor(member(_,_),member).
109		cannot_change_functor(negation(_),negation).
110		cannot_change_functor(truth,truth).
111		cannot_change_functor(C,F) :- comm_binop(C,F,_,_).
112
113		% simple terms where we can simply use Prolog unification
114		simple_term_to_unify('$'(_)).
115		%simple_term(Nr) :- integer(Nr). % numbers require evaluation of other part!
116
117		equal_lists(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), SL1 = SL2.
118
119	?	stronger_list(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), list_implies(SL1,SL2).
120
121		list_implies([],[]).
122		list_implies([H1|T1], [H2|T2]) :-
123	?	implies(H1,H2),
124		list_implies(T1,T2).
125
126		% a hypothesis "a > b" is a sufficient condition to discharge the goal "a >= b" with HYP
127		implies(X,X).
128		implies(c(L,equal),c(L,greater_equal)).
129		implies(c(L,equal),c(RL,greater_equal)) :- reverse(L,RL).
130		implies(c(L,greater),c(L,greater_equal)).
131		implies(c(L,greater),c(L,not_equal)).
132
133		comparable(G1,G2) :- functor(G1,T1,2), functor(G2,T2,2), comparison(T1), comparison(T2).
134		comparable(G1,G2) :- G1=..[F,P], G2=..[F,Q], !, comparable(P,Q).
135		comparable(G1,G2) :- functor(G1,F,_), functor(G2,F,_). % TODO: why is this req. weaker than in clause above for arity 1?
136
137		comparison(equal).
138		comparison(greater).
139		comparison(greater_equal).
140		comparison(less).
141		comparison(less_equal).
142		comparison(not_equal).
143
144		list_representation(A,B,OList,L3) :-
145		list_representation(A,OList,L1),
146		list_representation(B,[],L2),
147		append(L1,L2,L3).
148
149		list_representation(C,L) :- list_representation(C,[],L).
150		list_representation('$'(X),L,Res) :- !, Res=[X|L].
151		list_representation(less_equal(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater_equal)].
152		list_representation(greater_equal(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater_equal)].
153		list_representation(less(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater)].
154		list_representation(greater(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater)].
155		list_representation(minus(A,B),OList,NList) :- !,
156		collect_subtrahend(minus(A,B),Subtraction),
157		Subtraction = [Minuend, Subtrahend],
158		exclude_nr(Subtrahend, 0, NSubtrahend), % exclude(zero, Subtrahend, NSubtrahend),
159		(NSubtrahend == [] -> NList = [Minuend] ;
160		append(OList,[c([Minuend, NSubtrahend],minus)],NList)).
161		list_representation(div(A,B),OList,NList) :- !,
162		collect_divisor(div(A,B),Division),
163		Division = [Divident, Divisor],
164		exclude_nr(Divisor, 1, NDivisor), %exclude(one, Divisor, NDivisor),
165		(NDivisor == [] -> NList = [Divident] ;
166		append(OList,[c([Divident, NDivisor],div)],NList)).
167		list_representation(C,OList,Res) :-
168		comm_binop(C,F,A,B), !,
169		collect_components(A,B,OList,NList,F),
170		Res=[c(NList,F)].
171		list_representation(add(A,B),OList,Res) :- !,
172		collect_components(A,B,OList,NList,add),
173		exclude_nr(NList,0,NList2), %exclude(zero, NList, NList2),
174		(NList2 == [] -> Res = [0] ;
175		NList2 \= [_]-> Res = [c(NList2,add)] ;
176		Res = NList2).
177		list_representation(multiplication(A,B),OList,Res) :- !,
178		collect_components(A,B,OList,NList,multiplication),
179		exclude_nr(NList,1,NList2), %exclude(one, NList, NList2),
180		(member(0, NList2) -> Res = [0] ;
181		NList2 == [] -> Res = [1] ;
182		NList2 \= [_]-> Res = [c(NList2,multiplication)] ;
183		Res = NList2).
184		list_representation(set_extension(A),OList,Res) :- !,
185		list_representation_of_list(A,OList,NList), sort(NList,S), Res=[c(S,set_extension)].
186		list_representation([A|T],OList,Res) :- !, list_representation_of_list([A|T],OList,NList), Res=[c(NList,list)].
187		list_representation(C,OList,Res) :- C=..[F,A], !, list_representation(A,OList,NList), Res=[c(NList,F)].
188		list_representation(C,OList,Res) :-
189		C=..[F,A,B],!,
190		list_representation(A,B,OList,NList), Res=[c(NList,F)].
191		list_representation(X,L,[X|L]) :- atomic(X).
192
193		comm_binop(conjunct(A,B),conjunct,A,B).
194		comm_binop(disjunct(A,B),disjunct,A,B).
195		comm_binop(intersection(A,B),intersection,A,B).
196		comm_binop(union(A,B),union,A,B).
197
198		list_representation_of_list([],OList,OList).
199		list_representation_of_list([A|T],OList,NList) :- list_representation(A,OList,L1), list_representation_of_list(T,[],L2),append(L1,L2,NList).
200
201		one(X) :- X is 1.
202		zero(X) :- X is 0.
203		exclude_nr([],_,[]).
204		exclude_nr([H|T],Nr,Res) :-
205		(H==Nr -> exclude_nr(T,Nr,Res) ; Res=[H|TR], exclude_nr(T,Nr,TR)).
206
207		collect_components(A,B,OList,NList,T) :-
208		collect_component(A,OList,L1,T),
209		collect_component(B,L1,NList,T).
210
211		collect_component('$'(X),OList,NList,_) :- !,
212		append(OList,[X],NList).
213		collect_component(X,OList,NList,_) :-
214		atomic(X),!,
215		append(OList,[X],NList).
216		collect_component(C,OList,NList,T) :-
217		C=..[T,A,B],!,
218		collect_components(A,B,OList,NList,T).
219		collect_component(X,OList,NList,_) :-
220		list_representation(X,[],L1),
221		append(OList,L1,NList).
222
223		collect_subtrahend(minus(A, B), [LA, Sub]) :-
224		A \= minus(_,_), !,
225		list_representation(A,[LA]),
226		(B = 0 -> Sub = [] ;
227		list_representation(B,[LB]), Sub = [LB]).
228		collect_subtrahend(minus(A, B), [Minuend, NSubtrahends]) :-
229		collect_subtrahend(A, [Minuend, Subtrahends]),
230		list_representation(B,LB),
231		append(Subtrahends, LB, NSubtrahends).
232
233		collect_divisor(div(A, B), [LA, Div]) :-
234		A \= div(_,_), !,
235		list_representation(A,[LA]),
236		(B = 1 -> Div = [] ;
237		list_representation(B,[LB]), Div = [LB]).
238		collect_divisor(div(A, B), [Divident, NDivisors]) :-
239		collect_divisor(A, [Divident, Divisors]),
240		list_representation(B,LB),
241		append(Divisors, LB, NDivisors).
242
243		:- use_module(library(samsort)).
244
245		sort_list(L,R) :- sort_components(L,S), samsort(S,R).
246		sort_components([],[]).
247		sort_components([c(L,T)|Rest], Res) :-
248		commutative_op(T), !,
249		sort_list(L,SL),
250		sort_components(Rest,R),
251		Res=[c(SL,T)|R].
252		sort_components([c(L,T)|Rest], Res) :- !, % non-commutative
253		sort_components(L,L2),
254		sort_components(Rest,R),
255		Res=[c(L2,T)|R].
256		% sort list of subtrahends or divisors
257		sort_components([E|Rest], [E|R]) :- atomic(E), !, sort_components(Rest,R).
258		sort_components([E|Rest], [F|R]) :- sort_list(E,F), sort_components(Rest,R).
259
260		commutative_op(disjunct). commutative_op(conjunct). commutative_op(equivalence).
261		commutative_op(union). commutative_op(intersection).
262		commutative_op(add). commutative_op(multiplication).
263		commutative_op(equal). commutative_op(not_equal).
264		commutative_op(negation). commutative_op(unary_minus). % these are unary ?!
265		commutative_op(set_extension). commutative_op(list).
266
267
268		equal_op(L1,L2) :- L1 = [c(_,T1)], L2 = [c(_,T2)], !, T1 = T2.
269		equal_op([E1],[E2]) :- E1 \= [c(_,_)], E2 \= [c(_,_)].
270
271		equal_length(L1,L2) :- L1 = [c(A1,_)], L2 = [c(A2,_)], !, same_length(A1, A2).
272		equal_length([_],[_]).
273
274
275		% -------------------------
276
277
278		% check if X is either equal to Term or is a sub-term, traversing all binary operators Op
279		member_of(Op,X,Term) :- functor(Term,Op,2), !,
280	?	(arg(1,Term,A),member_of(Op,X,A) ; arg(2,Term,B), member_of(Op,X,B)).
281		% TODO: this will not find P if P uses top-level functor Op itself! Review all uses and see if this is ok
282		member_of(_,P,P).
283
284		% difference to member_of: this requires top-level of Term to be binary operator
285		member_of_bin_op(Op,X,Term) :- functor(Term,Op,2), !,
286	?	(arg(1,Term,A),member_of(Op,X,A) ; arg(2,Term,B), member_of(Op,X,B)).
287
288		% select and remove (first occurrence of) X:
289		select_op(X,C,Rest,Op) :- C=..[Op,A,B],
290	?	(select_op(X,A,RA,Op), conjoin4(RA,B,Rest,Op)
291		;
292	?	select_op(X,B,RB,Op), conjoin4(A,RB,Rest,Op)), !.
293		select_op(X,X,E,Op) :- neutral_element(Op,E).
294		select_op(X,Y,E,Op) :- neutral_element(Op,E), equal_terms(X,Y).
295
296		% replace (first occurrence of) X by Z:
297		select_op(X,C,Z,New,Op) :- C=..[Op,A,B],
298		(select_op(X,A,Z,RA,Op), conjoin4(RA,B,New,Op) ;
299		select_op(X,B,Z,RB,Op), conjoin4(A,RB,New,Op)), !.
300		select_op(X,X,Z,Z,_) :- !.
301		select_op(X,Y,Z,Z,_) :- equal_terms(X,Y).
302
303		conjoin4(E,X,R,Op) :- neutral_element(Op,E), !, R=X.
304		conjoin4(X,E,R,Op) :- neutral_element(Op,E), !, R=X.
305		conjoin4(X,Y,C,Op) :- C=..[Op,X,Y].
306
307		neutral_element(conjunct,true) :- !.
308		neutral_element(disjunct,false) :- !.
309		neutral_element(add,0) :- !.
310		neutral_element(multiplication,1) :- !.
311		neutral_element(_,placeholder).
312
313		% -------------------------
314
315		remove_duplicates_for_op(C,Res,Op) :-
316		functor(C,Op,_), % ensure that we have the desired functor as top-level
317		op_to_list(C,List,Op),
318		without_duplicates(List,ResL),
319		list_to_op(ResL,Res,Op).
320
321		without_duplicates(L,Res) :- without_duplicates(L,[],Res).
322
323		without_duplicates([],List,List).
324		without_duplicates([E|R],Filtered,Res) :-
325	?	member(F,Filtered),
326		equal_terms(E,F),!,
327		without_duplicates(R,Filtered,Res).
328		without_duplicates([E|R],Filtered, Res) :-
329		\+ member(E,Filtered),
330		append(Filtered,[E],New),
331		without_duplicates(R,New,Res).
332
333
334		op_to_list(Term,NList,Op) :-
335		op_to_list(Term,[],NList,Op).
336		op_to_list(Term,OList,NList,Op) :-
337		Term=..[Op,A,B],!,
338		op_to_list(B,OList,L1,Op),
339		op_to_list(A,L1,NList,Op).
340		op_to_list(Term,L,[Term|L],_). % Note: if L=[] then we did not have Op as top-level functor!
341
342		list_to_op([A],Res,_) :- !, Res=A.
343		list_to_op([A,B|L],Res,Op) :- C=..[Op,A,B], list_to_op(L,C,Res,Op).
344		list_to_op([],C,C,_).
345		list_to_op([X|T],C,Res,Op) :- NC=..[Op,C,X], list_to_op(T,NC,Res,Op).
346
347		% ------------------
348
349		negate(truth,Res) :- !, Res=falsity.
350		negate(falsity,Res) :- !, Res=truth.
351		negate(equal(X,Y),R) :- !, R=not_equal(X,Y).
352		negate(not_equal(X,Y),R) :- !, R=equal(X,Y).
353		negate(greater(X,Y),R) :- !, R=less_equal(X,Y).
354		negate(less(X,Y),R) :- !, R=greater_equal(X,Y).
355		negate(greater_equal(X,Y),R) :- !, R=less(X,Y).
356		negate(less_equal(X,Y),R) :- !, R=greater(X,Y).
357		negate(disjunct(X,Y),R) :- !, R=conjunct(NX,NY), negate(X,NX), negate(Y,NY).
358		negate(conjunct(X,Y),R) :- !, R=disjunct(NX,NY), negate(X,NX), negate(Y,NY).
359		negate(implication(X,Y),R) :- !, R=conjunct(X,NY), negate(Y,NY).
360		negate(negation(X),R) :- !, R=X.
361		negate(P,negation(P)).
362
363		% ------------------------
364
365
366		new_identifier(Expr,I) :-
367		used_identifiers(Expr,L),
368	?	possible_identifier(X),
369		I = '$'(X),
370	?	\+ member(I,L),!.
371
372		% -------------
373
374		used_identifiers_list(List,UsedIds) :-
375		used_identifiers(List,AllIds),
376		sort(AllIds,UsedIds).
377
378		used_identifiers(Term,AllIds) :- used_identifiers(Term,AllIds,[]).
379
380		used_identifiers(Term) --> {atomic(Term)}, !, [].
381		used_identifiers(Term) --> {Term = '$'(E), atomic(E)}, !, [Term].
382		used_identifiers(C) -->
383		{C =.. [_|Args]},
384		l_used_identifiers(Args).
385
386		l_used_identifiers([]) --> [].
387		l_used_identifiers([H|T]) --> used_identifiers(H), l_used_identifiers(T).
388
389		% -------------
390
391		free_identifiers(Term,AllIds) :- free_identifiers(Term,AllIds,[]).
392
393		free_identifiers(exists(Ids,P),Res1,Res2) :- !,
394		free_identifiers(P,Free), % TODO: pass FreeImp as parameter and filter
395		list_difference(Free,Ids,Res),
396		append(Res,Res1,Res2).
397		free_identifiers(Term,Res2,Res1) :-
398		(Term = forall(Ids,P,E)
399		; Term = event_b_comprehension_set(Ids,E,P)
400		; Term = quantified_intersection(Ids,P,E)
401		; Term = quantified_union(Ids,P,E)), !,
402		free_identifiers(implication(P,E),FreeImp), % TODO: pass FreeImp as parameter and filter
403		list_difference(FreeImp,Ids,Res),
404		append(Res,Res2,Res1).
405		free_identifiers(Term) --> {atomic(Term)}, !, [].
406		free_identifiers(Term) --> {Term = '$'(E), atomic(E)}, !, [Term].
407		free_identifiers(C) -->
408		{C =.. [_|Args]},
409		l_free_identifiers(Args).
410
411		l_free_identifiers([]) --> [].
412		l_free_identifiers([H|T]) --> free_identifiers(H), l_free_identifiers(T).
413
414		% -------------
415
416		identifier(x).
417		identifier(y).
418		identifier(z).
419
420	?	possible_identifier(Z) :- identifier(Z).
421		possible_identifier(Z) :- identifier(X), identifier(Y), atom_concat(X,Y,Z).
422
423		new_identifiers(Expr,1,[Id]) :- !, new_identifier(Expr,Id).
424	?	new_identifiers(Expr,Nr,Ids) :- used_identifiers(Expr,L), possible_identifier(X), I = '$'(X), \+ member(I,L), !, range_ids(X,Nr,Ids).
425
426	?	range_ids(X,Nr,L) :- range(X,1,Nr,L).
427		range(X,I,I,['$'(XI)]) :- atom_int_concat(X,I,XI).
428	?	range(X,I,K,['$'(XI)|L]) :- I < K, I1 is I + 1, atom_int_concat(X,I,XI), range(X,I1,K,L).
429
430		atom_int_concat(X,I,XI) :-
431		atom_codes(X,CX),
432		number_codes(I,CI),
433		append(CX,CI,COut),
434		atom_codes(XI,COut).
435
436		new_aux_identifier(IdsTypes,X) :-
437	?	possible_identifier(X),
438	?	\+ member(b(identifier(X),_,_),IdsTypes),!.
439
440		% -------------------------
441
442		is_fun(partial_function(DOM,RAN),partial,DOM,RAN).
443		is_fun(partial_injection(DOM,RAN),partial,DOM,RAN).
444		is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN).
445		is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN).
446		is_fun(total_function(DOM,RAN),total,DOM,RAN).
447		is_fun(total_injection(DOM,RAN),total,DOM,RAN).
448		is_fun(total_surjection(DOM,RAN),total,DOM,RAN).
449		is_fun(total_bijection(DOM,RAN),total,DOM,RAN).
450
451		is_rel(F,Type,DOM,RAN) :- is_fun(F,Type,DOM,RAN).
452		is_rel(relations(DOM,RAN),partial,DOM,RAN).
453		is_rel(total_relation(DOM,RAN),total,DOM,RAN).
454		is_rel(surjection_relation(DOM,RAN),partial,DOM,RAN).
455		is_rel(total_surjection_relation(DOM,RAN),total,DOM,RAN).
456
457		is_surj(total_bijection(DOM,RAN),DOM,RAN).
458		is_surj(total_surjection(DOM,RAN),DOM,RAN).
459		is_surj(partial_surjection(DOM,RAN),DOM,RAN).
460		is_surj(surjection_relation(DOM,RAN),DOM,RAN).
461		is_surj(total_surjection_relation(DOM,RAN),DOM,RAN).
462
463		is_inj(partial_injection(DOM,RAN),DOM,RAN).
464		is_inj(partial_bijection(DOM,RAN),DOM,RAN).
465		is_inj(total_injection(DOM,RAN),DOM,RAN).
466		is_inj(total_bijection(DOM,RAN),DOM,RAN).
467
468
469		is_natural_set(natural_set).
470		is_natural_set('NATURAL').
471
472		is_natural1_set(natural1_set).
473		is_natural1_set('NATURAL1').
474
475		is_integer_set(integer_set).
476		is_integer_set('INTEGER').
477
478		is_less_eq(less_equal(P,Q),P,Q).
479		is_less_eq(greater_equal(Q,P),P,Q).
480
481		is_less(less(P,Q),P,Q).
482		is_less(greater(Q,P),P,Q).
483
484		is_equality(equal(A,B),X,Y) :- ((X,Y) = (A,B) ; (X,Y) = (B,A)).
485
486		% check if we have an inequality between two terms
487	?	is_inequality(negation(Eq),X,Y) :- is_equality(Eq,X,Y).
488		is_inequality(not_equal(A,B),X,Y) :- ((X,Y) = (A,B) ; (X,Y) = (B,A)).
489
490		%is_equivalence(equivalence(A,B),A,B).
491		%is_equivalence(equivalence(B,A),A,B).
492
493
494		% symmetric / commutative unification; useful for commutative operators
495		sym_unify(A,B,A,B).
496		sym_unify(A,B,B,A).
497
498		is_inter(intersection(A,B),A,B). % TODO: extend to nested inter
499		is_inter(intersection(B,A),A,B).
500
501		is_minus(NE,E) :- number(NE), NE < 0, E is abs(NE) ; NE = unary_minus(E).
502
503	?	is_empty(Expr,Term) :- is_equality(Expr,Term,empty_set).
504		is_empty(Expr,Term) :- Expr = subset(Term,empty_set).
505
506		is_negation(Q,negation(P)) :- equal_terms(P,Q).
507
508		of_integer_type('$'(E),Info) :-
509		atomic(E),
510		of_integer_type(E,Info).
511		of_integer_type(E,Info) :-
512		get_meta_info(ids_types,Info,STypes),
513		member(b(identifier(E),integer,_),STypes).
514
515		singleton_set(set_extension([X]),X).
516
517
518		split_composition(Comp,LComp,RComp) :-
519		Comp = composition(_,_),
520		op_to_list(Comp,List,composition),
521		append(L,R,List),
522		list_to_op(L,LComp,composition),
523		list_to_op(R,RComp,composition).
524
525		% ----------------------------
526
527		% check if something is a pure type expression
528		type_expression(bool_set,_).
529		type_expression(Z,_) :- is_integer_set(Z).
530		type_expression(S,Info) :- is_deferred_or_enumerated_set(S,Info).
531	?	type_expression(pow_subset(Ty),Info) :- type_expression(Ty,Info).
532	?	type_expression(cartesian_product(Ty1,Ty2),Info) :- type_expression(Ty1,Info), type_expression(Ty2,Info).
533		% there are more type expressions not in Event-B:
534		type_expression(string_set,_).
535		type_expression(real_set,_).
536		type_expression(typeset,_).
537
538		get_type_expression(integer,'INTEGER').
539		get_type_expression(boolean,bool_set).
540		get_type_expression(set(S),pow_subset(T)) :- get_type_expression(S,T).
541		get_type_expression(couple(A,B),cartesian_product(S,T)) :- get_type_expression(A,S), get_type_expression(B,T).
542
543		% ------------------------
544
545		get_typed_identifiers(NormExpr,List) :- get_typed_identifiers(NormExpr,[],List).
546
547		get_typed_identifiers(NormExpr,Scope,List) :-
548		convert_norm_expr_to_raw(NormExpr,ParsedRaw),
549		Quantifier = forall,
550		bmachine:b_type_open_predicate(Quantifier,ParsedRaw,Scope,TypedPred,[]), !,
551		(TypedPred = b(forall(List0,_,_),_,_) -> List=List0 ; List=[]).
552		% already known IDs from scope are ignored, no forall is generated if there are no new IDs
553		get_typed_identifiers(NormExpr,_,List) :-
554		used_identifiers(NormExpr,Ids),
555		maplist(any_type,Ids,List).
556
557		any_type('$'(X),b(identifier(X),any,[])).
558
559		% ------------------------
560
561		is_deferred_or_enumerated_set('$'(Set),Info) :-
562		get_meta_info(rawsets,Info,RawSets), % also covers enumerated sets in Event-B; TODO: adapt for classical B??
563		member(deferred_set(_,Set),RawSets).
564
565		get_meta_info(Key,Info,Content) :- El=..[Key,Content], memberchk(El,Info), !.
566		get_meta_info(_,_,[]).
567
568		update_meta_infos(Key,Info,Values,Info1) :-
569		get_meta_info(Key,Info,Content),
570		Content \= [], !,
571		Old=..[Key,Content],
572		New=..[Key,Values],
573		select(Old,Info,New,Info1).
574		update_meta_infos(Key,Info,Values,[El|Info]) :- El=..[Key,Values].
575
576		add_meta_info(Key,Info,Value,Info1) :- add_meta_infos(Key,Info,[Value],Info1).
577
578		add_meta_infos(Key,Info,Values,Info1) :-
579		get_meta_info(Key,Info,Content),
580		Content \= [], !,
581		Old=..[Key,Content],
582		append(Values,Content,NewContent),
583		New=..[Key,NewContent],
584		select(Old,Info,New,Info1).
585		add_meta_infos(Key,Info,Values,[El|Info]) :- El=..[Key,Values].
586
587		remove_meta_info(Key,Info,Value,Info1) :-
588		get_meta_info(Key,Info,Content),
589		Old=..[Key,Content],
590		select(Value,Content,Content0),
591		New=..[Key,Content0],
592		select(Old,Info,New,Info1).
593
594
595		% ----------------------------
596
597		:- use_module(probsrc(translate),[with_translation_mode/2]).
598		:- use_module(wdsrc(well_def_hyps),[convert_norm_expr_to_raw/2,translate_norm_expr_with_limit/3]).
599		translate_norm_expr_term(Term,Str) :-
600		catch(with_translation_mode(unicode,translate_norm_expr_with_limit(Term,300,Str)),Exc,
601		(format(user_output,'Cannot translate ~w due to ~w~n',[Term,Exc]),Str='???')).
602
603
604		create_descr(Rule,T,Descr) :- translate_norm_expr_term(T,TS),
605		ajoin([Rule,' (',TS,')'],Descr).
606		create_descr(Rule,S,T,Descr) :- translate_norm_expr_term(T,TS),
607		ajoin([Rule,' (',S,',',TS,')'],Descr).