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(z_tools,
6		[decorate_vars/3,
7		find_unchanged/3,
8		vars_of_decl/2,
9		z_conjunction/2,
10		z_conjunctiont/2,
11		z_disjunction/2,
12		z_counter/2,
13		z_translate_identifier/2,
14		z_translate_identifiers/2,
15		z_translate_typed_identifiers/4,
16		z_translate_typed_identifier/4,
17		z_translate_identifier_list/2,
18		append_not_duplicate/3
19		% create_z_let/6 % now in bsyntaxtree_quantifiers
20		]).
21
22		:- use_module(library(lists)).
23
24		:- use_module(probsrc(tools)).
25		:- use_module(probsrc(self_check)).
26		:- use_module(probsrc(bsyntaxtree)).
27
28		:- use_module(probsrc(module_information)).
29		:- module_info(group,proz).
30		:- module_info(description,'This module provides several helper predicates for ProZ.').
31
32
33		%*******************************************************************************
34		% translates an Z identifier of the form "name(Name,Appendix)" to a B identifier
35		z_translate_identifier(name(ZName,Deco), BName) :-
36		atom_concat(ZName, Deco, BName).
37		z_translate_identifiers([],[]).
38		z_translate_identifiers([ZName|ZRest],[BName|BRest]) :-
39		z_translate_identifier(ZName,BName),
40		z_translate_identifiers(ZRest,BRest).
41
42		z_translate_identifier_list([],[]).
43		z_translate_identifier_list([ZName|ZRest],['Identifier'(BName)|BRest]) :-
44		z_translate_identifier(ZName,BName),
45		z_translate_identifier_list(ZRest,BRest).
46
47
48		z_translate_typed_identifier(name(ZName,Deco),Type,Infos,TExpr) :-
49		ajoin([ZName,Deco],Id),
50		create_texpr(identifier(Id),Type,[zname(ZName,Deco)|Infos],TExpr).
51
52		z_translate_typed_identifiers([],[],_,[]).
53		z_translate_typed_identifiers([ZName|Zrest],[Type|Trest],Infos,[TExpr|Brest]) :-
54		z_translate_typed_identifier(ZName,Type,Infos,TExpr),
55		z_translate_typed_identifiers(Zrest,Trest,Infos,Brest).
56
57		%*******************************************************************************
58		% Returns a term with a unique number appended
59		:- dynamic z_counter_db/1.
60		z_counter_db(1).
61
62		z_counter(Name,NewName) :-
63		retract(z_counter_db(C)),
64		C1 is C + 1,
65		assertz(z_counter_db(C1)),
66		atom_codes(Name,NC), number_codes(C,CC),
67		append(NC,CC,NewC),
68		atom_codes(NewName,NewC).
69
70
71		%*******************************************************************************
72		% returns the list of variables that are declarated
73		vars_of_decl(Decls,Vars) :-
74		findall(V,
75		(member(decl(Vars,_Type),Decls),member(V,Vars)),
76		Vars).
77
78
79		%*******************************************************************************
80		% appends a list to another while ignoring duplicate entries
81		append_not_duplicate(A,B,Result) :-
82		remove_all(B,A,D),
83		append(A,D,Result).
84
85
86		%*******************************************************************************
87		% decorates variables
88		decorate_vars(In,Deco,Out) :- (Deco = '' -> In=Out ; decorate_vars2(In,Deco,Out)).
89		decorate_vars2([],_,[]).
90		decorate_vars2([name(Name,D1)|Rest],Deco,[name(Name,D2)|DRest]) :-
91		atom_concat(D1,Deco,D2),
92		decorate_vars2(Rest,Deco,DRest).
93
94
95		%********************************************************************************
96		% find unchanged variables
97
98		find_unchanged(ti(body(Decls,Where),Type),UnchangedVars,ti(body(Decls,RestWhere),Type)) :-
99		find_unchanged2(Where,UnchangedVars,RestWhere).
100		find_unchanged2([],[],[]) :- !.
101		find_unchanged2([ti(equal(ti(ref(name(Name,DecoA),[]),_),
102		ti(ref(name(Name,DecoB),[]),_)),bool)|ExprRest],
103		[name(Name,'')|UnchangedRest],Rest) :-
104		( (DecoA = '', DecoB = '\'') % TODO: Use library(lists)
105		; (DecoA = '\'', DecoB = '')),!,
106		find_unchanged2(ExprRest,UnchangedRest,Rest).
107		find_unchanged2([Pred|Rest],Unchanged,[Pred|FRest]) :- find_unchanged2(Rest,Unchanged,FRest).
108
109
110		%*******************************************************************************
111		% build the conjunction/disjunction of a list of predicates
112		% the result is a single predicate
113
114		z_conjunction(List,Result) :- lcombine(List,and,truth,Result).
115		z_disjunction(List,Result) :- lcombine(List,or,falsity,Result).
116
117		lcombine(List,Op,Neutral,Result) :-
118		lcombine2(List,Op,Neutral,Neutral,Result).
119		lcombine2([],_,_,Result,Result).
120		lcombine2([A|Rest],Op,Neutral,Acc,Result) :-
121		lcombine3(Acc,A,Op,Neutral,Inter),
122		lcombine2(Rest,Op,Neutral,Inter,Result).
123		lcombine3(Neutral,B,_,Neutral,B) :- !.
124		lcombine3(A,Neutral,_,Neutral,A) :- !.
125		lcombine3(A,B,Op,_,Result) :- Result =.. [Op,A,B].
126
127
128		z_conjunctiont(List,Result) :-
129		z_conjunctiont2(List,ti(truth,bool),Result).
130		z_conjunctiont2([],Result,Result).
131		z_conjunctiont2([A|Rest],Acc,Result) :-
132		z_conjunctiont3(Acc,A,Inter),
133		z_conjunctiont2(Rest,Inter,Result).
134		z_conjunctiont3(ti(truth,bool),B,B) :- !.
135		z_conjunctiont3(A,ti(truth,bool),A) :- !.
136		z_conjunctiont3(A,B,ti(and(A,B),bool)).
137
138
139		% ****************************************************