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