1 % (c) 2009-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(translate,
6 [print_bexpr_or_subst/1, l_print_bexpr_or_subst/1,
7 print_bexpr/1, debug_print_bexpr/1, nested_print_bexpr/1, nested_print_bexpr_as_classicalb/1,
8 print_bexpr_stream/2,
9 print_components/1,
10 print_bexpr_with_limit/2,
11 print_unwrapped_bexpr_with_limit/1,print_bvalue/1, l_print_bvalue/1, print_bvalue_stream/2,
12 translate_params_for_dot/2,
13 print_machine/1,
14 translate_machine/3,
15 set_unicode_mode/0, unset_unicode_mode/0, unicode_mode/0,
16 set_latex_mode/0, unset_latex_mode/0, latex_mode/0,
17 set_translation_mode/1, unset_translation_mode/1,
18 translate_bexpression_to_unicode/2,
19 translate_bexpression/2, translate_subst_or_bexpr_in_mode/3,
20 translate_bexpression_with_limit/3, translate_bexpression_with_limit/2,
21 translate_bexpression_to_codes/2,
22 translate_predicate_into_machine/2,
23 get_bexpression_column_template/4,
24 translate_subst_or_bexpr/2, translate_subst_or_bexpr_with_limit/3,
25 translate_substitution/2, print_subst/1,
26 translate_bvalue/2, translate_bvalue_to_codes/2,
27 translate_bvalue_with_limit/3,
28 translate_bvalue_with_type/3, translate_bvalue_with_type_and_limit/4,
29 translate_bvalue_for_expression/3, translate_bvalue_for_expression_with_limit/4,
30 translate_bvalue_with_tlatype/3,
31 print_state/1,
32 translate_bstate/2, translate_bstate_limited/2,
33 print_bstate/1, translate_context/2, print_context/1,
34 translate_any_state/2, %translate_b_state_to_comma_list_codes/3,
35 print_value_variable/1,
36 print_cspm_state/1, translate_cspm_state/2,
37 print_csp_value/1, translate_csp_value/2,
38 translate_cspm_expression/2,
39 translate_properties_with_limit/2,
40 translate_event/2,translate_events/2,
41 translate_event_with_target_id/4,
42 translate_event_with_src_and_target_id/4, translate_event_with_src_and_target_id/5,
43 get_non_det_modified_vars_in_target_id/3,
44 translate_event_with_limit/3,
45 translate_state_errors/2,translate_state_error/2,
46 translate_event_error/2,
47 translate_prolog_constructor/2, translate_prolog_constructor_in_mode/2,
48 pretty_type/2,
49 explain_state_error/3,
50 explain_event_trace/2,
51 generate_typing_predicates/2,
52
53 print_raw_machine_terms/1,
54 print_raw_bexpr/1,
55
56 print_span/1, translate_span/2,
57 translate_span_with_filename/2,
58
59 set_type_to_maximal_texpr/2, type_set/2, % should probably be moved to other module
60
61 translate_error_term/2,
62
63 set_translation_constants/1, set_translation_context/1,
64 clear_translation_constants/0,
65
66 set_print_type_infos/1,
67 suppress_rodin_positions/0,
68
69 install_b_portray_hook/0,remove_b_portray_hook/0,
70
71 translate_eventb_to_classicalb/3,
72 return_csp_closure_value/2
73
74 ]).
75
76 :- use_module(tools).
77
78 :- use_module(module_information).
79 :- module_info(group,tools).
80 :- module_info(description,'This module is responsible for pretty-printing B and CSP, source spans, ...').
81
82 :- use_module(library(lists)).
83 :- use_module(library(codesio)).
84 :- use_module(library(terms)).
85 :- use_module(library(avl)).
86
87 :- use_module(debug).
88 :- use_module(error_manager).
89 :- use_module(self_check).
90 :- use_module(b_global_sets).
91 :- use_module(specfile,[csp_with_bz_mode/0,process_algebra_mode/0,
92 animation_minor_mode/1,set_animation_minor_mode/1,
93 remove_animation_minor_mode/0,
94 animation_mode/1,set_animation_mode/1, csp_mode/0,
95 translate_operation_name/2]).
96 :- use_module(bsyntaxtree).
97 %:- use_module('smv/smv_trans',[smv_print_initialisation/2]).
98 :- use_module(preferences,[get_preference/2, preference/2, set_preference/2]).
99 :- use_module(bmachine_structure).
100
101 % print a list of expressions or substitutions
102 l_print_bexpr_or_subst([]).
103 l_print_bexpr_or_subst([H|T]) :-
104 print_bexpr_or_subst(H),
105 (T=[] -> true
106 ; (get_texpr_type(H,Type),Type==subst -> print('; ') ; print(', '),
107 l_print_bexpr_or_subst(T))
108 ).
109
110 print_bexpr_or_subst(E) :- get_texpr_type(E,T),T==subst,!, print_subst(E).
111 print_bexpr_or_subst(precondition(A,B)) :- !, print_subst(precondition(A,B)).
112 print_bexpr_or_subst(any(A,B,C)) :- !, print_subst(any(A,B,C)).
113 print_bexpr_or_subst(select(A)) :- !, print_subst(select(A)). % TO DO: add more cases ?
114 print_bexpr_or_subst(E) :- print_bexpr(E).
115
116 print_unwrapped_bexpr_with_limit(Expr) :- print_unwrapped_bexpr_with_limit(Expr,200).
117 print_unwrapped_bexpr_with_limit(Expr,Limit) :-
118 translate:print_bexpr_with_limit(b(Expr,pred,[]),Limit),nl.
119 debug_print_bexpr(E) :- debug:debug_mode(off) -> true ; print_bexpr(E).
120 print_bexpr(Expr) :- translate_bexpression(Expr,R), print(R).
121 print_bexpr_with_limit(Expr,Limit) :- translate_bexpression_with_limit(Expr,Limit,R), print(R).
122 print_bvalue(Val) :- translate_bvalue(Val,TV), print(TV).
123 print_bexpr_stream(S,Expr) :- translate_bexpression(Expr,R), write(S,R).
124 print_bvalue_stream(S,Val) :- translate_bvalue(Val,R), write(S,R).
125
126 print_components(C) :- print_components(C,0).
127 print_components([],Nr) :- print('Nr of components: '),print(Nr),nl.
128 print_components([component(Pred,Vars)|T],Nr) :- N1 is Nr+1,
129 print('Component: '), print(N1), print(' over '), print(Vars),nl,
130 print_bexpr(Pred),nl,
131 print_components(T,N1).
132
133 l_print_bvalue([]).
134 l_print_bvalue([H|T]) :- print_bvalue(H), print(' : '),l_print_bvalue(T).
135
136 nested_print_bexpr_as_classicalb(E) :-
137 (animation_minor_mode(X)
138 -> remove_animation_minor_mode,
139 call_cleanup(nested_print_bexpr(E), set_animation_minor_mode(X))
140 ; nested_print_bexpr(E)).
141
142 nested_print_bexpr([]) :- !.
143 nested_print_bexpr([H|T]) :- !,nested_print_bexpr(H),nl,nested_print_bexpr(T).
144 nested_print_bexpr(Expr) :- nbp(Expr,'&',0).
145
146 nbp(b(E,_,Info),Type,Indent) :- nbp2(E,Type,Info,Indent).
147 nbp2(E,Type,_Info,Indent) :- get_binary_op(E,NewType,LHS,RHS),!,
148 inc_indent(NewType,Type,Indent,NIndent),
149 print_bracket(Indent,NIndent,'('),
150 nbp(LHS,NewType,NIndent),
151 print_indent(NIndent), print(NewType),nl,
152 nbp(RHS,NewType,NIndent),
153 print_bracket(Indent,NIndent,')').
154 nbp2(lazy_let_pred(TID,LHS,RHS),Type,_Info,Indent) :-
155 def_get_texpr_id(TID,ID),!,
156 NewType=lazy_let_pred(TID),
157 inc_indent(NewType,Type,Indent,NIndent),
158 print_indent(Indent), format('LET ~w = (~n',[ID]),
159 nbp(LHS,NewType,NIndent),
160 print_indent(NIndent), print(') IN ('),nl,
161 nbp(RHS,NewType,NIndent),
162 print_indent(NIndent),print(')'),nl.
163 nbp2(negation(LHS),_Type,_Info,Indent) :- !,
164 inc_indent(negation,false,Indent,NIndent),
165 print_indent(Indent), print('not('),nl,
166 nbp(LHS,negation,NIndent),
167 print_indent(Indent), print(')'),nl.
168 nbp2(let_predicate(Ids,Exprs,Pred),_Type,_Info,Indent) :- !,
169 inc_indent(let_predicate,false,Indent,NIndent),
170 pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
171 print_indent(Indent),format('#~s.( /* LET */~n',[Codes]),
172 pp_expr_let_pred_exprs(Ids,Exprs,_LimitReached,Codes2,[]),
173 print_indent(Indent), format('~s~n',[Codes2]),
174 print_indent(NIndent), print('&'),nl,
175 nbp(Pred,let_predicate,NIndent),
176 print_indent(Indent), print(')'),nl.
177 nbp2(exists(Ids,Pred),_Type,_Info,Indent) :- !,
178 inc_indent(exists,false,Indent,NIndent),
179 pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
180 print_indent(Indent),format('#~s.(~n',[Codes]),
181 nbp(Pred,exists,NIndent),
182 print_indent(Indent), print(')'),nl.
183 nbp2(forall(Ids,LHS,RHS),_Type,_Info,Indent) :- !,
184 inc_indent(forall,false,Indent,NIndent),
185 pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
186 print_indent(Indent),format('!~s.(~n',[Codes]),
187 nbp(LHS,forall,NIndent),
188 print_indent(NIndent), print('=>'),nl,
189 nbp(RHS,forall,NIndent),
190 print_indent(Indent), print(')'),nl.
191 nbp2(E,_,Info,Indent) :- print_indent(Indent), print_bexpr(b(E,pred,Info)),nl.
192
193 get_binary_op(conjunct(LHS,RHS),'&',LHS,RHS).
194 get_binary_op(disjunct(LHS,RHS),'or',LHS,RHS).
195 get_binary_op(implication(LHS,RHS),'=>',LHS,RHS).
196 get_binary_op(equivalence(LHS,RHS),'<=>',LHS,RHS).
197
198 inc_indent(Type,CurType,I,NewI) :- (Type=CurType -> NewI=I ; NewI=s(I)).
199 print_bracket(I,I,_) :- !.
200 print_bracket(I,_NewI,Bracket) :-
201 print_indent(I), print(Bracket),nl.
202
203 print_indent(s(X)):- !,
204 print(' '),
205 print_indent(X).
206 print_indent(_).
207
208 /* =============================================== */
209 /* Translating expressions and values into strings */
210 /* =============================================== */
211
212
213
214
215
216 translate_params_for_dot(List,TransList) :- translate_params_for_dot(List,TransList,-3).
217 translate_params_for_dot([],'',_).
218 translate_params_for_dot([H|T],Res,Nr) :-
219 translate_property_with_limit(H,100,TH),
220 (Nr>2 -> N1=1 ; N1 is Nr+1),
221 translate_params_for_dot(T,TT,N1),
222 string_concatenate(TH,TT,Res1),
223 (N1=1 -> string_concatenate(',\n',Res1,Res)
224 ; (Nr>(-3) -> string_concatenate(',',Res1,Res) ; Res=Res1)).
225
226 translate_channel_values(X,['_'|T],T) :- var(X),!.
227 translate_channel_values([],S,S) :- !.
228 translate_channel_values([tuple([])|T],S,R) :- !,
229 translate_channel_values(T,S,R).
230 translate_channel_values([in(tuple([]))|T],S,R) :- !,
231 translate_channel_values(T,S,R).
232 translate_channel_values([H|T],['.'|S],R) :- !,
233 ((nonvar(H),H=in(X))
234 -> Y=X
235 ; Y=H
236 ),
237 pp_csp_value(Y,S,S2),
238 translate_channel_values(T,S2,R).
239 translate_channel_values(tail_in(X),S,T) :-
240 (X=[] ; X=[_|_]), !, translate_channel_values(X,S,T).
241 translate_channel_values(_X,['??'|S],S).
242
243
244
245 pp_single_csp_value(V,'_') :- var(V),!.
246 pp_single_csp_value(X,'_cyclic_') :- cyclic_term(X),!.
247 pp_single_csp_value(int(X),A) :- atomic(X),!,number_chars(X,Chars),atom_chars(A,Chars).
248
249 :- assert_must_succeed((translate_cspm_expression(listExp(rangeOpen(2)),R), R == '<2..>')).
250 :- assert_must_succeed((translate_cspm_expression(listFrom(2),R), R == '<2..>')).
251 :- assert_must_succeed((translate_cspm_expression(listFromTo(2,6),R), R == '<2..6>')).
252 :- assert_must_succeed((translate_cspm_expression(setFromTo(2,6),R), R == '{2..6}')).
253 :- assert_must_succeed((translate_cspm_expression('#'(listFromTo(2,6)),R), R == '#<2..6>')).
254 :- assert_must_succeed((translate_cspm_expression(inGuard(x,setFromTo(1,5)),R), R == '?x:{1..5}')).
255 :- assert_must_succeed((translate_cspm_expression(builtin_call(int(3)),R), R == '3')).
256 :- assert_must_succeed((translate_cspm_expression(set_to_seq(setValue([int(1),int(2)])),R), R == 'seq({1,2})')).
257 :- assert_must_succeed((translate_cspm_expression(diff(setValue([int(1)]),setValue([])),R), R == 'diff({1},{})')).
258 :- assert_must_succeed((translate_cspm_expression(inter(setValue([int(1)]),setValue([])),R), R == 'inter({1},{})')).
259 :- assert_must_succeed((translate_cspm_expression(lambda([x,y],'*'(x,y)),R), R == '\\ x,y @ (x*y)')).
260 :- assert_must_succeed((translate_cspm_expression(lambda([x,y],'/'(x,y)),R), R == '\\ x,y @ (x/y)')).
261 :- assert_must_succeed((translate_cspm_expression(lambda([x,y],'%'(x,y)),R), R == '\\ x,y @ (x%y)')).
262 :- assert_must_succeed((translate_cspm_expression(rename(x,y),R), R == 'x <- y')).
263 :- assert_must_succeed((translate_cspm_expression(link(x,y),R), R == 'x <-> y')).
264 :- assert_must_succeed((translate_cspm_expression(agent_call_curry(f,[[a,b],[c]]),R), R == 'f(a,b)(c)')).
265
266 translate_cspm_expression(Expr, Text) :-
267 (pp_csp_value(Expr,Atoms,[]) -> ajoin(Atoms,Text)
268 ; print('Pretty printing expression failed: '),print(Expr),nl).
269
270 pp_csp_value(X,[A|S],S) :- pp_single_csp_value(X,A),!.
271 pp_csp_value(setValue(L),['{'|S],T) :- !,pp_csp_value_l(L,',',S,['}'|T],inf).
272 pp_csp_value(setExp(rangeEnum(L)),['{'|S],T) :- !,pp_csp_value_l(L,',',S,['}'|T],inf).
273 pp_csp_value(setExp(rangeEnum(L),Gen),['{'|S],T) :- !,
274 copy_term((L,Gen),(L2,Gen2)), numbervars((L2,Gen2),1,_),
275 pp_csp_value_l(L2,',',S,['|'|S2],inf),
276 pp_csp_value_l(Gen2,',',S2,['}'|T],inf).
277 pp_csp_value(avl_set(A),['{'|S],T) :- !,avl_domain(A,L),pp_csp_value_l(L,',',S,['}'|T],inf).
278 pp_csp_value(setExp(rangeClosed(L,U)),['{'|S],T) :- !, pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['}'|T]).
279 pp_csp_value(setExp(rangeOpen(L)),['{'|S],T) :- !, pp_csp_value(L,S,['..}'|T]).
280 % TO DO: pretty print comprehensionGuard; see prints in coz-example.csp ; test 1846
281 pp_csp_value(comprehensionGenerator(Var,Body),S,T) :- !, pp_csp_value(Var,S,['<-'|S1]),
282 pp_csp_value(Body,S1,T).
283 pp_csp_value(listExp(rangeEnum(L)),['<'|S],T) :- !,pp_csp_value_l(L,',',S,['>'|T],inf).
284 pp_csp_value(listExp(rangeClosed(L,U)),['<'|S],T) :- !, pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['>'|T]).
285 pp_csp_value(listExp(rangeOpen(L)),['<'|S],T) :- !, pp_csp_value(L,S,['..>'|T]).
286 pp_csp_value(setFromTo(L,U),['{'|S],T) :- !,
287 pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['}'|T]).
288 pp_csp_value(setFrom(L),['{'|S],T) :- !,
289 pp_csp_value(L,S,['..}'|T]).
290 pp_csp_value(closure(L), ['{|'|S],T) :- !,pp_csp_value_l(L,',',S,['|}'|T],inf).
291 pp_csp_value(list(L),['<'|S],T) :- !,pp_csp_value_l(L,',',S,['>'|T],inf).
292 pp_csp_value(listFromTo(L,U),['<'|S],T) :- !,
293 pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['>'|T]).
294 pp_csp_value(listFrom(L),['<'|S],T) :- !,
295 pp_csp_value(L,S,['..>'|T]).
296 pp_csp_value('#'(L),['#'|S],T) :- !,pp_csp_value(L,S,T).
297 pp_csp_value('^'(X,Y),S,T) :- !,pp_csp_value(X,S,['^'|S1]), pp_csp_value(Y,S1,T).
298 pp_csp_value(linkList(L),S,T) :- !,pp_csp_value_l(L,',',S,T,inf).
299 pp_csp_value(in(X),['?'|S],T) :- !,pp_csp_value(X,S,T).
300 pp_csp_value(inGuard(X,Set),['?'|S],T) :- !,pp_csp_value(X,S,[':'|S1]),
301 pp_csp_value(Set,S1,T).
302 pp_csp_value(out(X),['!'|S],T) :- !,pp_csp_value(X,S,T).
303 pp_csp_value(alsoPat(X,_Y),S,T) :- !,pp_csp_value(X,S,T).
304 pp_csp_value(appendPat(X,_Fun),S,T) :- !,pp_csp_value(X,S,T).
305 pp_csp_value(tuple(vclosure),S,T) :- !, S=T.
306 pp_csp_value(tuple([X]),S,T) :- !,pp_csp_value_in(X,S,T).
307 pp_csp_value(tuple([X|vclosure]),S,T) :- !,pp_csp_value_in(X,S,T).
308 pp_csp_value(tuple([H|TT]),S,T) :- !,pp_csp_value_in(H,S,['.'|S1]),pp_csp_value(tuple(TT),S1,T).
309 pp_csp_value(dotTuple([]),['unit_channel'|S],S) :- ! .
310 pp_csp_value(dotTuple([H]),S,T) :- !, pp_csp_value_in(H,S,T).
311 pp_csp_value(dotTuple([H|TT]),S,T) :- !, pp_csp_value_in(H,S,['.'|S1]),
312 pp_csp_value(dotTuple(TT),S1,T).
313 pp_csp_value(tupleExp(Args),S,T) :- !,pp_csp_args(Args,S,T,'(',')').
314 pp_csp_value(na_tuple(Args),S,T) :- !,pp_csp_args(Args,S,T,'(',')').
315 pp_csp_value(record(Name,Args),['('|S],T) :- !,pp_csp_value(tuple([Name|Args]),S,[')'|T]).
316 pp_csp_value(val_of(Name,_Span),S,T) :- !, pp_csp_value(Name,S,T).
317 pp_csp_value(builtin_call(X),S,T) :- !,pp_csp_value(X,S,T).
318 pp_csp_value(seq_to_set(X),['set('|S],T) :- !,pp_csp_value(X,S,[')'|T]).
319 pp_csp_value(set_to_seq(X),['seq('|S],T) :- !,pp_csp_value(X,S,[')'|T]).
320 %pp_csp_value('\\'(B,C,S),S1,T) :- !, pp_csp_process(ehide(B,C,S),S1,T).
321 pp_csp_value(agent_call(_Span,Agent,Parameters),['('|S],T) :- !,
322 pp_csp_value(Agent,S,S1),
323 pp_csp_args(Parameters,S1,[')'|T],'(',')').
324 pp_csp_value(agent_call_curry(Agent,Parameters),S,T) :- !,
325 pp_csp_value(Agent,S,S1),
326 pp_csp_curry_args(Parameters,S1,T).
327 pp_csp_value(lambda(Parameters,Body),['\\ '|S],T) :- !,
328 pp_csp_args(Parameters,S,[' @ '|S1],'',''),
329 pp_csp_value(Body,S1,T).
330 pp_csp_value(rename(X,Y),S,T) :- !,pp_csp_value(X,S,[' <- '|S1]),
331 pp_csp_value(Y,S1,T).
332 pp_csp_value(link(X,Y),S,T) :- !,pp_csp_value(X,S,[' <-> '|S1]),
333 pp_csp_value(Y,S1,T).
334 % binary operators:
335 pp_csp_value(Expr,['('|S],T) :- bynary_numeric_operation(Expr,E1,E2,OP),!,
336 pp_csp_value(E1,S,[OP|S2]),
337 pp_csp_value(E2,S2,[')'|T]).
338 % built-in functions for sets
339 pp_csp_value(empty(A),[empty,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
340 pp_csp_value(card(A),[card,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
341 pp_csp_value('Set'(A),['Set','('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
342 pp_csp_value('Inter'(A1),['Inter','('|S],T) :- !,pp_csp_value(A1,S,[')'|T]).
343 pp_csp_value('Union'(A1),['Union','('|S],T) :- !,pp_csp_value(A1,S,[')'|T]).
344 pp_csp_value(diff(A1,A2),[diff,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
345 pp_csp_value(inter(A1,A2),[inter,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
346 pp_csp_value(union(A1,A2),[union,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
347 pp_csp_value(member(A1,A2),[member,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
348 % built-in functions for sequences
349 pp_csp_value(null(A),[null,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
350 pp_csp_value(length(A),[length,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
351 pp_csp_value(head(A),[head,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
352 pp_csp_value(tail(A),[tail,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
353 pp_csp_value(elem(A1,A2),[elem,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
354 pp_csp_value(concat(A1,A2),[concat,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').
355 pp_csp_value('Seq'(A),['Seq','('|S],T) :- !, pp_csp_value(A,S,[')'|T]).
356 % vclosure
357 pp_csp_value(Expr,S,T) :- is_list(Expr),!,pp_csp_value(closure(Expr),S,T).
358 % Type expressions
359 pp_csp_value(dotTupleType([H]),S,T) :- !, pp_csp_value_in(H,S,T).
360 pp_csp_value(dotTupleType([H|TT]),S,T) :- !,pp_csp_value_in(H,S,['.'|S1]), pp_csp_value(dotTupleType(TT),S1,T).
361 pp_csp_value(typeTuple(Args),S,T) :- !, pp_csp_args(Args,S,T,'(',')').
362 pp_csp_value(dataType(T),[T|S],S) :- ! .
363 pp_csp_value(boolType,['Bool'|S],S) :- ! .
364 pp_csp_value(intType,['Int'|S],S) :- ! .
365 pp_csp_value(dataTypeDef([H]),S,T) :- !, pp_csp_value(H,S,T).
366 pp_csp_value(dataTypeDef([H|TT]),S,T) :- !, pp_csp_value(H,S,['|'|S1]),
367 pp_csp_value(dataTypeDef(TT),S1,T).
368 pp_csp_value(constructor(Name),[Name|S],S) :- ! .
369 pp_csp_value(constructorC(C,Type),[C,'('|S],T) :- !, pp_csp_value(Type,S,[')'|T]).
370 % Argument of function can be process
371
372 pp_csp_value(Expr,S,T) :- pp_csp_process(Expr,S,T),!. % pp_csp_process has a catch-all !!! TO DO: look at this
373 pp_csp_value(Expr,S,T) :- csp_with_bz_mode,!,pp_value(Expr,S,T).
374 pp_csp_value(X, [A|S], S) :- % ['<< ',A,' >>'|S],S) :- % the << >> pose problems when checking against FDR
375 write_to_codes(X,Codes),atom_codes_with_limit(A,Codes).
376
377 pp_csp_value_in(H,S,T) :- nonvar(H),H=in(X),!, pp_csp_value(X,S,T).
378 pp_csp_value_in(H,S,T) :- pp_csp_value(H,S,T).
379
380 print_csp_value(Val) :- pp_csp_value(Val,Atoms,[]), ajoin(Atoms,Text),
381 print(Text).
382
383 translate_csp_value(Val,Text) :- pp_csp_value(Val,Atoms,[]), ajoin(Atoms,Text).
384
385 return_csp_closure_value(closure(S),List) :- pp_csp_value_l1(S,List).
386 return_csp_closure_value(setValue(S),List) :- pp_csp_value_l1(S,List).
387
388 pp_csp_value_l1([Expr|Rest],List) :-
389 ( nonvar(Rest),Rest=[] ->
390 pp_csp_value(Expr,T,[]),ajoin(T,Value),List=[Value]
391 ; pp_csp_value_l1(Rest,R),pp_csp_value(Expr,T,[]),ajoin(T,Value),List=[Value|R]
392 ).
393
394 pp_csp_args([],T,T,_LPar,_RPar).
395 pp_csp_args([H|TT],[LPar|S],T,LPar,RPar) :- pp_csp_value(H,S,S1), pp_csp_args2(TT,S1,T,RPar).
396 pp_csp_args2([],[RPar|T],T,RPar).
397 pp_csp_args2([H|TT],[','|S],T,RPar) :- pp_csp_value(H,S,S1), pp_csp_args2(TT,S1,T,RPar).
398
399 pp_csp_curry_args([],T,T).
400 pp_csp_curry_args([H|TT],S,T) :- is_list(H), pp_csp_args(H,S,S1,'(',')'), pp_csp_curry_args(TT,S1,T).
401
402 pp_csp_value_l(V,_Sep,['...'|S],S,N) :- (var(V) ; (N \= inf -> N<1;fail)), !.
403 pp_csp_value_l([],_Sep,S,S,_).
404 pp_csp_value_l([Expr|Rest],Sep,S,T,Nr) :-
405 ( nonvar(Rest),Rest=[] ->
406 pp_csp_value(Expr,S,T)
407 ; otherwise ->
408 (Nr=inf -> N1 = Nr ; N1 is Nr-1),
409 pp_csp_value(Expr,S,[Sep|S1]),pp_csp_value_l(Rest,Sep,S1,T,N1)).
410
411 :- assert_must_succeed((translate:convert_set_into_sequence([(int(1),int(5))],Seq),
412 check_eqeq(Seq,[int(5)]))).
413 :- assert_must_succeed((translate:convert_set_into_sequence([(int(2),X),(int(1),int(5))],Seq),
414 check_eq(Seq,[int(5),X]))).
415
416 convert_set_into_sequence(Set,Seq) :-
417 nonvar(Set), \+ animation_minor_mode(eventb),
418 convert_set_into_sequence1(Set,Seq).
419 convert_set_into_sequence1(avl_set(A),Seq) :- !,
420 avl_size(A,Sz),size_is_in_set_limit(Sz),convert_avlset_into_sequence(A,Seq).
421 convert_set_into_sequence1([],Seq) :- !, Seq=[].
422 convert_set_into_sequence1(Set,Seq) :-
423 convert_set_into_sequence2(Set,0,_,SetElems,Seq),ground(SetElems).
424 convert_set_into_sequence2([],_Max,([],[]),_,_Seq).
425 convert_set_into_sequence2([Pair|T],Max,Last,SetElems,Seq) :-
426 nonvar(Pair),nonvar(T),Pair=(Index,H),ground(Index),
427 Index=int(Nr),
428 insert_el_into_seq(Nr,H,Seq,SetElems,L),
429 (Nr>Max -> NMax=Nr,NLast=L ; NMax=Max,NLast=Last),
430 convert_set_into_sequence2(T,NMax,NLast,SetElems,Seq).
431 insert_el_into_seq(1,H,[H|L],[set|L2],(L,L2)) :- !.
432 insert_el_into_seq(N,H,[_|T],[_|T2],Last) :- N>1, N1 is N-1, insert_el_into_seq(N1,H,T,T2,Last).
433
434 convert_avlset_into_sequence(Avl,Sequence) :-
435 \+ animation_minor_mode(eventb),
436 convert_avlset_into_sequence2(Avl,1,Sequence).
437 convert_avlset_into_sequence2(Avl,_Index,[]) :-
438 empty_avl(Avl),!.
439 convert_avlset_into_sequence2(Avl,Index,[Head|Tail]) :-
440 avl_del_min(Avl, Min, _ ,NewAvl),
441 nonvar(Min), Min=(L,Head),
442 ground(L), L=int(Index),
443 Index2 is Index + 1,
444 convert_avlset_into_sequence2(NewAvl,Index2,Tail).
445
446 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
447 % translate new syntax tree -- work in progress
448 :- assert_must_succeed((translate_cspm_state(lambda([x,y],'|~|'(prefix(_,[],x,skip(_),_),prefix(_,[],y,skip(_),_),_)),R), R == 'CSP: \\ x,y @ (x->SKIP) |~| (y->SKIP)')).
449 :- assert_must_succeed((translate_cspm_state(agent_call_curry('F',[[a,b],[c]]),R), R == 'CSP: F(a,b)(c)')).
450 :- assert_must_succeed((translate_cspm_state(ifte(bool_not('<'(x,3)),';'(esharing([a],'/\\'('P1','P2',span),procRenaming([rename(r,s)],'Q',span),span),lParallel([link(b,c)],'R','S',span),span),'[>'(elinkParallel([link(h1,h2)],'G1','G2',span),exception([a],'H1','H2',span),span),span1,span2,span3),R), R == 'CSP: if not((x<3)) then ((P1) /\\ (P2) [|{|a|}|] Q[[r <- s]]) ; (R [{|b <-> c|}] S) else (G1 [{|h1 <-> h2|}] G2) [> (H1 [|{|a|}|> H2)')).
451 :- assert_must_succeed((translate_cspm_state(aParallel([a,b],'P',[b,c],'Q',span),R), R == 'CSP: P [{|a,b|} || {|b,c|}] Q')).
452 :- assert_must_succeed((translate_cspm_state(eaParallel([a,b],'P',[b,c],'Q',span),R), R == 'CSP: P [{|a,b|} || {|b,c|}] Q')).
453 :- assert_must_succeed((translate_cspm_state(eexception([a,b],'P','Q',span),R), R == 'CSP: P [|{|a,b|}|> Q')).
454
455 print_cspm_state(State) :- translate_cspm_state(State,T), print(T).
456
457 translate_cspm_state(State,Text) :-
458 ( pp_csp_process(State,Atoms,[]) -> true
459 ; print(pp_csp_process_failed(State)),nl,Atoms=State),
460 ajoin(['CSP: '|Atoms],Text).
461
462 pp_csp_process(skip(_Span),S,T) :- !, S=['SKIP'|T].
463 pp_csp_process(stop(_Span),S,T) :- !, S=['STOP'|T].
464 pp_csp_process('CHAOS'(_Span,Set),['CHAOS('|S],T) :- !,
465 pp_csp_value(Set,S,[')'|T]).
466 pp_csp_process(val_of(Agent,_Span),S,T) :- !,
467 pp_csp_value(Agent,S,T).
468 pp_csp_process(builtin_call(X),S,T) :- !,pp_csp_process(X,S,T).
469 pp_csp_process(agent(F,Body,_Span),S,T) :- !,
470 F =.. [Agent|Parameters],
471 pp_csp_value(Agent,S,S1),
472 pp_csp_args(Parameters,S1,[' = '|S2],'(',')'),
473 pp_csp_value(Body,S2,T).
474 pp_csp_process(agent_call(_Span,Agent,Parameters),S,T) :- !,
475 pp_csp_value(Agent,S,S1),
476 pp_csp_args(Parameters,S1,T,'(',')').
477 pp_csp_process(agent_call_curry(Agent,Parameters),S,T) :- !,
478 pp_csp_value(Agent,S,S1),
479 pp_csp_curry_args(Parameters,S1,T).
480 pp_csp_process(lambda(Parameters,Body),['\\ '|S],T) :- !,
481 pp_csp_args(Parameters,S,[' @ '|S1],'',''),
482 pp_csp_value(Body,S1,T).
483 pp_csp_process('\\'(B,C,S),S1,T) :- !, pp_csp_process(ehide(B,C,S),S1,T).
484 pp_csp_process(ehide(Body,ChList,_Span),['('|S],T) :- !,
485 pp_csp_process(Body,S,[')\\('|S1]),
486 pp_csp_value(ChList,S1,[')'|T]).
487 pp_csp_process(let(Decls,P),['let '| S],T) :- !,
488 maplist(translate_cspm_state,Decls,Texts),
489 ajoin_with_sep(Texts,' ',Text),
490 S=[Text,' within '|S1],
491 pp_csp_process(P,S1,T).
492 pp_csp_process(Expr,['('|S],T) :- binary_csp_op(Expr,X,Y,Op),!,
493 pp_csp_process(X,S,[') ',Op,' ('|S1]),
494 pp_csp_process(Y,S1,[')'|T]).
495 pp_csp_process(Expr,S,T) :- sharing_csp_op(Expr,X,Middle,Y,Op1,Op2),!,
496 pp_csp_process(X,S,[Op1|S1]),
497 pp_csp_value(Middle,S1,[Op2|S2]),
498 pp_csp_process(Y,S2,T).
499 pp_csp_process(Expr,S,T) :- asharing_csp_op(Expr,X,MiddleX,MiddleY,Y,Op1,MOp,Op2),!,
500 pp_csp_process(X,S,[Op1|S1]),
501 pp_csp_value(MiddleX,S1,[MOp|S2]),
502 pp_csp_value(MiddleY,S2,[Op2|S3]),
503 pp_csp_process(Y,S3,T).
504 pp_csp_process(Expr,S,T) :- renaming_csp_op(Expr,X,RList,Op1,Op2),!,
505 pp_csp_process(X,S,[Op1|S1]),
506 pp_csp_value_l(RList,',',S1,[Op2|T],10).
507 pp_csp_process(prefix(_SPAN1,Values,ChannelExpr,CSP,_SPAN2),S,T) :- !,
508 pp_csp_value_l([ChannelExpr|Values],'',S,['->'|S2],20),
509 pp_csp_process(CSP,S2,T).
510 pp_csp_process('&'(Test,Then),S,T) :- !,
511 pp_csp_bool_expr(Test,S,['&'|S2]),
512 pp_csp_process(Then,S2,T).
513 pp_csp_process(ifte(Test,Then,Else,_SPAN1,_SPAN2,_SPAN3),[' if '|S],T) :- !,
514 pp_csp_bool_expr(Test,S,[' then '|S2]),
515 pp_csp_process(Then,S2,[' else '|S3]),
516 pp_csp_process(Else,S3,T).
517 pp_csp_process(head(A),[head,'('|S],T) :- !, pp_csp_process(A,S,[')'|T]).
518 pp_csp_process(X,[X|T],T).
519
520 pp_csp_bool_expr(bool_not(BE),['not('|S],T) :- !, pp_csp_bool_expr(BE,S,[')'|T]).
521 pp_csp_bool_expr(BE,['('|S],T) :- binary_bool_op(BE,BE1,BE2,OP), !,
522 pp_csp_bool_expr(BE1,S,[OP|S2]),
523 pp_csp_bool_expr(BE2,S2,[')'|T]).
524 pp_csp_bool_expr(BE,[OP,'('|S],T) :- binary_pred(BE,BE1,BE2,OP), !,
525 pp_csp_value(BE1,S,[','|S2]),
526 pp_csp_value(BE2,S2,[')'|T]).
527 pp_csp_bool_expr(BE,S,T) :- pp_csp_value(BE,S,T).
528
529 bynary_numeric_operation('+'(X,Y),X,Y,'+').
530 bynary_numeric_operation('-'(X,Y),X,Y,'-').
531 bynary_numeric_operation('*'(X,Y),X,Y,'*').
532 bynary_numeric_operation('/'(X,Y),X,Y,'/').
533 bynary_numeric_operation('%'(X,Y),X,Y,'%').
534
535 binary_pred('member'(X,Y),X,Y,member).
536 binary_pred('<'(X,Y),X,Y,'<').
537 binary_pred('>'(X,Y),X,Y,'>').
538 binary_pred('>='(X,Y),X,Y,'>=').
539 binary_pred('<='(X,Y),X,Y,'=<').
540 binary_pred('elem'(X,Y),X,Y,is_elem_list).
541 binary_pred('=='(X,Y),X,Y,equal_element).
542 binary_pred('!='(X,Y),X,Y,not_equal_element).
543
544
545 binary_bool_op('<'(X,Y),X,Y,'<').
546 binary_bool_op('>'(X,Y),X,Y,'>').
547 binary_bool_op('>='(X,Y),X,Y,'>=').
548 binary_bool_op('<='(X,Y),X,Y,'=<').
549 binary_bool_op('=='(X,Y),X,Y,'==').
550 binary_bool_op('!='(X,Y),X,Y,'!=').
551 binary_bool_op(bool_and(X,Y),X,Y,'&&').
552 binary_bool_op(bool_or(X,Y),X,Y,'||').
553
554 binary_csp_op('|||'(X,Y,_Span),X,Y,'|||').
555 binary_csp_op('[]'(X,Y,_Span),X,Y,'[]').
556 binary_csp_op('|~|'(X,Y,_Span),X,Y,'|~|').
557 binary_csp_op(';'(X,Y,_Span),X,Y,';').
558 binary_csp_op('[>'(P,Q,_SrcSpan),P,Q,'[>').
559 binary_csp_op('/\\'(P,Q,_SrcSpan),P,Q,'/\\').
560
561 sharing_csp_op(esharing(CList,X,Y,_SrcSpan),X,CList,Y,' [|','|] ').
562 sharing_csp_op(sharing(CList,X,Y,_SrcSpan),X,CList,Y,' [|','|] ').
563 sharing_csp_op(lParallel(LinkList,X,Y,_Span),X,LinkList,Y,' [','] ').
564 sharing_csp_op(elinkParallel(LinkList,X,Y,_Span),X,LinkList,Y,' [','] ').
565 sharing_csp_op(exception(CList,X,Y,_SrcSpan),X,CList,Y,' [|','|> ').
566 sharing_csp_op(eexception(CList,X,Y,_SrcSpan),X,CList,Y,' [|','|> ').
567
568 asharing_csp_op(aParallel(CListX,X,CListY,Y,_SrcSpan),X,CListX,CListY,Y,' [',' || ','] ').
569 asharing_csp_op(eaParallel(CListX,X,CListY,Y,_SrcSpan),X,CListX,CListY,Y,' [',' || ','] ').
570
571 renaming_csp_op(procRenaming(RenameList,X,_SrcSpan),X,RenameList,'[[',']]').
572 renaming_csp_op(eprocRenaming(RenameList,X,_SrcSpan),X,RenameList,'[[',']]').
573
574 :- use_module(bmachine,[b_get_machine_operation_parameter_types/2, b_is_operation_name/1]).
575
576 translate_events([],[]).
577 translate_events([E|Erest],[Out|Orest]) :-
578 translate_event(E,Out),
579 translate_events(Erest,Orest).
580
581
582 % a version of translate_event which has access to the target state id:
583 % this allows to translate setup_constants, intialise by inserting target constants or values
584
585 translate_event_with_target_id(Term,Dst,Limit,Str) :-
586 translate_event_with_src_and_target_id(Term,unknown,Dst,Limit,Str).
587 translate_event_with_src_and_target_id(Term,Src,Dst,Str) :-
588 translate_event_with_src_and_target_id(Term,Src,Dst,5000,Str).
589
590 translate_event_with_src_and_target_id(Term,Src,Dst,Limit,Str) :-
591 get_preference(expand_avl_upto,CurLim),
592 SetLim is Limit/2,% at least two symbols per element
593 (CurLim<0 ; SetLim < CurLim),!,
594 temporary_set_preference(expand_avl_upto,SetLim,CHNG),
595 translate_event_with_target_id2(Term,Src,Dst,Limit,Str),
596 reset_temporary_preference(expand_avl_upto,CHNG).
597 translate_event_with_src_and_target_id(Term,Src,Dst,Limit,Str) :-
598 translate_event_with_target_id2(Term,Src,Dst,Limit,Str).
599
600 translate_event_with_target_id2(Term,_,Dst,Limit,Str) :-
601 functor(Term,'$setup_constants',_),
602 get_preference(show_initialisation_arguments,true),
603 state_space:visited_expression(Dst,concrete_constants(State)),
604 get_non_det_constant(State,NonDetState),
605 !,
606 translate_b_state_to_comma_list_codes("SETUP_CONSTANTS",NonDetState,Limit,Codes),
607 atom_codes_with_limit(Str,Limit,Codes).
608 translate_event_with_target_id2(Term,_,Dst,Limit,Str) :-
609 functor(Term,'$initialise_machine',_),
610 get_preference(show_initialisation_arguments,true),
611 bmachine:b_get_operation_non_det_modifies('$initialise_machine',NDModVars),
612 state_space:visited_expression(Dst,State), get_variables(State,VarsState),
613 (NDModVars \= []
614 ->
615 include(non_det_modified_var(NDModVars),VarsState,ModVarsState) % first show non-det variables
616 % we could add a preference for whether to show the deterministicly assigned variables at all
617 %exclude(non_det_modified_var(NDModVars),VarsState,ModVarsState2),
618 %append(ModVarsState1,ModVarsState2,ModVarsState)
619 ; ModVarsState = VarsState),
620 !,
621 translate_b_state_to_comma_list_codes("INITIALISATION",ModVarsState,Limit,Codes),
622 atom_codes_with_limit(Str,Limit,Codes).
623 translate_event_with_target_id2(Term,Src,Dst,Limit,Str) :-
624 atomic(Term), % only applied to operations without parameters
625 ? specfile:b_mode,
626 get_non_det_modified_vars_in_target_id(Term,Dst,ModVarsState0), % only show non-det variables
627 (Src \= unknown,
628 state_space:visited_expression(Src,SrcState), get_variables(SrcState,PriorVarsState)
629 -> exclude(var_not_really_modified(PriorVarsState),ModVarsState0,ModVarsState)
630 % we could also optionally filter out vars which have the same value for all outgoing transitions of Src
631 ; ModVarsState = ModVarsState0
632 ),
633 !,
634 atom_codes(Term,TermCodes),
635 translate_b_state_to_comma_list_codes(TermCodes,ModVarsState,Limit,Codes),
636 atom_codes_with_limit(Str,Limit,Codes).
637 translate_event_with_target_id2(Term,_,_,Limit,Str) :- translate_event_with_limit(Term,Limit,Str).
638
639
640 get_non_det_modified_vars_in_target_id(OpName,DstId,ModVarsState0) :-
641 bmachine:b_get_operation_non_det_modifies(OpName,NDModVars),
642 NDModVars \= [], % a variable is non-deterministically written
643 state_space:visited_expression(DstId,State),
644 get_variables(State,VarsState),
645 include(non_det_modified_var(NDModVars),VarsState,ModVarsState0).
646
647 :- use_module(library(ordsets)).
648 non_det_modified_var(NDModVars,bind(Var,_)) :- ord_member(Var,NDModVars).
649
650 var_not_really_modified(PriorState,bind(Var,Val)) :-
651 ? (member(bind(Var,PVal),PriorState) -> PVal=Val).
652
653 get_variables(const_and_vars(_,VarsState),S) :- !, S=VarsState.
654 get_variables(S,S).
655
656 :- dynamic non_det_constants/2.
657
658 % compute which constants are non-deterministically assigned and which ones not
659 % TODO: maybe move to state space and invalidate info in case execute operation by predicate used
660 get_non_det_constant(Template,Result) :- non_det_constants(A,B),!, (A,B)=(Template,Result).
661 get_non_det_constant(Template,Result) :-
662 state_space:transition(root,_,DstID),
663 state_space:visited_expression(DstID,concrete_constants(State)), %print(get_non_det_constant(DstID)),nl,
664 !,
665 findall(D,(state_space:transition(root,_,D),D \= DstID),OtherDst),
666 compute_non_det_constants2(OtherDst,State),
667 non_det_constants(Template,Result).
668 get_non_det_constant(A,A).
669
670 compute_non_det_constants2([],State) :- adapt_state(State,Template,Result),
671 (Result = [] -> assert(non_det_constants(A,A)) % in case all variables are deterministic: just show them
672 ; assert(non_det_constants(Template,Result))).
673 compute_non_det_constants2([Dst|T],State) :-
674 state_space:visited_expression(Dst,concrete_constants(State2)),
675 lub_state(State,State2,NewState),
676 compute_non_det_constants2(T,NewState).
677
678 lub_state([],[],[]).
679 lub_state([bind(V,H1)|T1],[bind(V,H2)|T2],[bind(V,H3)|T3]) :-
680 (H1==H2 -> H3=H1 ; H3='$NONDET'), lub_state(T1,T2,T3).
681
682 adapt_state([],[],[]).
683 adapt_state([bind(ID,Val)|T],[bind(ID,X)|TX],[bind(ID,X)|TY]) :- Val='$NONDET',!,
684 adapt_state(T,TX,TY).
685 adapt_state([bind(ID,_)|T],[bind(ID,_)|TX],TY) :- % Value is deterministic: do not copy
686 adapt_state(T,TX,TY).
687
688
689
690 % ------------------------------------
691
692 translate_event_with_limit(Event,Limit,Out) :-
693 translate_event2(Event,Atoms,[]),!,
694 ajoin_with_limit(Atoms,Limit,Out).
695 %,print(done),debug:print_debug_stats,nl.% , print(Out),nl.
696 translate_event_with_limit(Event,_,Out) :- add_error(translate_event_with_limit,'Could not translate event: ', Event),
697 Out = '???'.
698
699 translate_event(Event,Out) :- %print(translate),print_debug_stats,nl,
700 translate_event2(Event,Atoms,[]),!,
701 ajoin(Atoms,Out).
702 %,print(done),debug:print_debug_stats,nl.% , print(Out),nl.
703 translate_event(Event,Out) :-
704 add_error(translate_event,'Could not translate event: ', Event),
705 Out = '???'.
706 /* BEGIN CSP */
707 translate_event2(start_cspm(Process),['start_cspm('|S],T) :- process_algebra_mode,!,pp_csp_value(Process,S,[')'|T]).
708 %% translate_event2(i(_Span),['i'|T],T) :- process_algebra_mode,!. /* CSP */ %% deprecated
709 translate_event2(tick(_Span),['tick'|T],T) :- process_algebra_mode,!. /* CSP */
710 translate_event2(tau(hide(Action)),['tau(hide('|S],T) :- process_algebra_mode,nonvar(Action), !,
711 translate_event2(Action,S,['))'|T]). /* CSP */
712 translate_event2(tau(link(Action1,Action2)),['tau(link('|S],T) :- /* CSP */
713 nonvar(Action1), nonvar(Action2), process_algebra_mode, !,
714 translate_event2(Action1,S,['<->'|S1]),
715 translate_event2(Action2,S1,['))'|T]).
716 translate_event2(tau(Info),['tau(',Fun,')'|T],T) :-
717 nonvar(Info), process_algebra_mode,!, /* CSP */
718 functor(Info,Fun,_). %(translate_event(Info,Fun) -> true ; functor(Info,Fun,_)),
719 translate_event2(io(V,Ch,_Span),S,T) :- process_algebra_mode,!, /* CSP */
720 (specfile:csp_with_bz_mode ->
721 S=['CSP:'|S1],
722 translate_event2(io(V,Ch),S1,T)
723 ; otherwise ->
724 translate_event2(io(V,Ch),S,T)
725 ).
726 translate_event2(io(X,Channel),S,T) :- process_algebra_mode,!, /* CSP */
727 (X=[] -> translate_event2(Channel,S,T)
728 ; (translate_event2(Channel,S,S1),
729 translate_channel_values(X,S1,T))
730 ).
731 /* END CSP */
732 translate_event2('$JUMP'(Name),[A|T],T) :- write_to_codes(Name,Codes),
733 atom_codes_with_limit(A,Codes).
734 translate_event2('-->'(Operation,ResultValues),S,T) :- nonvar(ResultValues),
735 ResultValues=[_|_],!,
736 translate_event2(Operation,S,['-->',ValuesStr|T]),
737 translate_bvalues(ResultValues,ValuesStr).
738 translate_event2(Op,[TOpName|S],T) :-
739 nonvar(Op), Op =.. [OpName|Args],
740 translate_operation_name(OpName,TOpName),
741 ( Args=[] -> S=T
742 ; otherwise ->
743 S=['(',ValuesStr,')'|T],
744 ? ((get_preference(show_eventb_any_arguments,false), % otherwise we have additional ANY parameters !
745 ? \+ is_init(OpName), % order of variables does not always correspond to Variable order used by b_get_machine_operation_parameter_types ! TO DO - Fix this in b_initialise_machine2 (see Interlocking.mch CSP||B model)
746 ? specfile:b_mode,
747 b_is_operation_name(OpName),
748 b_get_machine_operation_parameter_types(OpName,ParTypes),
749 ParTypes \= [])
750 -> translate_bvalues_with_types(Args,ParTypes,ValuesStr)
751 %; is_init(OpName) -> b_get_machine_operation_typed_parameters(OpName,TypedParas),
752 ; translate_bvalues(Args,ValuesStr))
753 ),!.
754 translate_event2(Op,[A|T],T) :-
755 %['<< ',A,' >>'|T],T) :- % the << >> pose problems when checking against FDR
756 write_to_codes(Op,Codes),
757 atom_codes_with_limit(A,Codes).
758
759 is_init('$initialise_machine').
760 is_init('$setup_constants').
761
762 translate_bvalues_with_types(Values,Types,Output) :-
763 %set_up_limit_reached(Codes,1000,LimitReached),
764 pp_value_l_with_types(Values,',',Types,_LimitReached,Codes,[]),!,
765 atom_codes_with_limit(Output,Codes).
766 translate_bvalues_with_types(Values,T,Output) :-
767 add_internal_error('Call failed: ',translate_bvalues_with_types(Values,T,Output)),
768 translate_bvalues(Values,Output).
769
770 pp_value_l_with_types([],_Sep,[],_) --> !.
771 pp_value_l_with_types([Expr|Rest],Sep,[TE|TT],LimitReached) -->
772 ( {nonvar(Rest),Rest=[]} ->
773 pp_value_with_type(Expr,TE,LimitReached)
774 ; {otherwise} ->
775 pp_value_with_type(Expr,TE,LimitReached),ppatom(Sep),
776 pp_value_l_with_types(Rest,Sep,TT,LimitReached)).
777
778
779 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
780
781 % pretty-print properties
782 translate_properties_with_limit([],[]).
783 translate_properties_with_limit([P|Prest],[Out|Orest]) :-
784 translate_property_with_limit(P,320,Out), % reduced limit as we now have evaluation view + possibility to inspect all of value
785 translate_properties_with_limit(Prest,Orest).
786
787 translate_property_with_limit(Prop,Limit,Output) :-
788 (pp_property(Prop,Limit,Output) -> true ; (add_error(translate_property,'Could not translate property: ',Prop),Output='???')).
789 pp_property(Prop,Limit,Output) :-
790 pp_property_without_plugin(Prop,Limit,Output).
791 pp_property_without_plugin(=(Key,Value),_,A) :-
792 !,ajoin([Key,' = ',Value],A).
793 pp_property_without_plugin(':'(Key,Value),_,A) :-
794 !,ajoin([Key,' : ',Value],A).
795 pp_property_without_plugin(info(I),_,I) :- !.
796 pp_property_without_plugin(Prop,Limit,A) :-
797 write_to_codes(Prop,Codes),
798 atom_codes_with_limit(A,Limit,Codes).
799
800
801 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
802 :- use_module(tools_meta,[translate_term_into_atom_with_max_depth/3]).
803
804 % pretty-print errors belonging to a certain state
805 translate_error_term(Var,S) :- var(Var),!,
806 translate_term_into_atom_with_max_depth(Var,5,S).
807 translate_error_term('@fun'(X,F),S) :-
808 translate:translate_bvalue(X,TX), translate:translate_bvalue(F,TF),!,
809 % translate_term_into_atom_with_max_depth('@fun'(TX,TF),5,S).
810 (get_error_span_for_value(F,Span)
811 -> ajoin(['Function argument: ',TX, ', function value: ',TF,' defined at ',Span],S)
812 ; ajoin(['Function argument: ',TX, ', function value: ',TF],S)
813 ).
814 translate_error_term('@rel'(Arg,Res1,Res2),S) :-
815 translate:translate_bvalue(Arg,TA), translate:translate_bvalue(Res1,R1),
816 translate:translate_bvalue(Res2,R2),!,
817 ajoin(['Function argument: ',TA, ', two possible values: ',R1,', ',R2],S).
818 translate_error_term([operation(Name,Env)],S) :-
819 translate:translate_any_state(Env,TEnv), !,
820 translate_term_into_atom_with_max_depth(operation(Name,TEnv),10,S).
821 translate_error_term(error(E1,E2),S) :- !, translate_prolog_error(E1,E2,S).
822 translate_error_term(b(B,T,I),S) :-
823 translate_subst_or_bexpr_with_limit(b(B,T,I),1000,do_not_report_errors,S),!. % do not report errors, otherwise we end in an infinite loop of adding errors while adding errors
824 translate_error_term(T,S) :- translate_term_into_atom_with_max_depth(T,5,S).
825
826 % try and get error location for span:
827 get_error_span_for_value(Var,_) :- var(Var),!,fail.
828 get_error_span_for_value(closure(_,_,Body),Span) :- translate_span_with_filename(Body,Span), Span \= ''.
829
830 translate_prolog_error(existence_error(procedure,Pred),_,S) :- !,
831 translate_term_into_atom_with_max_depth('Unknown Prolog predicate:'(Pred),8,S).
832 translate_prolog_error(existence_error(source_sink,File),_,S) :- !,
833 translate_term_into_atom_with_max_depth('Could not access file:'(File),8,S).
834 translate_prolog_error(E1,_,S) :- translate_term_into_atom_with_max_depth(E1,8,S).
835
836 translate_state_errors([],[]).
837 translate_state_errors([E|ERest],[Out|ORest]) :-
838 ( E = eventerror(Event,EError,_) ->
839 translate_event_error(EError,Msg),
840 ajoin([Event,': ',Msg],Out)
841 ; translate_state_error(E,Out) -> true
842 ; otherwise -> functor(E,Out,_) ),
843 translate_state_errors(ERest,ORest).
844
845 translate_error_context(E,TE) :- translate_error_context2(E,Codes,[]),
846 atom_codes_with_limit(TE,Codes).
847 translate_error_context2(span_context(Span,Context)) --> !,
848 translate_error_context2(Context),
849 translate_span(Span,only_subsidiary).
850 translate_error_context2([H]) --> !,translate_error_context2(H).
851 translate_error_context2(checking_invariant) --> !,
852 {get_specification_description_codes(invariant,A)}, A. %"INVARIANT".
853 translate_error_context2(checking_assertions) --> !,
854 {get_specification_description_codes(assertions,A)}, A. %"ASSERTIONS".
855 translate_error_context2(checking_negation_of_invariant(_State)) --> !,
856 "not(INVARIANT)".
857 translate_error_context2(operation(OpName,_State)) --> !,
858 {translate_operation_name(OpName,TOp)},
859 ppterm(TOp).
860 translate_error_context2(checking_context(Check,Name)) --> !,
861 ppterm(Check),ppterm(Name).
862 translate_error_context2(X) --> "???:", ppterm(X).
863
864 ?print_span(Span) :- translate_span(Span,Atom), !, print(Atom).
865 print_span(S) :- print(span(S)).
866
867 ?translate_span(Span,Atom) :- translate_span(Span,only_subsidiary,Codes,[]),
868 atom_codes_with_limit(Atom,Codes).
869 translate_span_with_filename(Span,Atom) :-
870 translate_span(Span,always_print_filename,Codes,[]),
871 atom_codes_with_limit(Atom,Codes).
872
873 ?translate_span(Span,PrintFileNames) --> {extract_line_col(Span,Srow,Scol,_Erow,_Ecol)},!,
874 ? "(Line:",ppterm(Srow)," Col:",ppterm(Scol),
875 %"-",ppterm(Erow),":",ppterm(Ecol),
876 ? translate_span_file_opt(Span,PrintFileNames),
877 % TO DO: print short version of extract_additional_description ?
878 ")".
879 translate_span(Span,PrintFileNames) -->
880 % for Event-B, e.g., line-col fails but we can get a section/file name
881 "(File:",translate_span_file(Span,PrintFileNames),!,")".
882 translate_span(_,_PrintFileNames) --> "".
883
884 translate_span_file(Span,always_print_filename) -->
885 {extract_tail_file_name(Span,Filename)},!,
886 %{bmachine:b_get_main_filenumber(MainFN), Nr \= MainFN},!,
887 ":", ppterm(Filename).
888 translate_span_file(Span,_) -->
889 {extract_subsidiary_tail_file_name(Span,Filename)},
890 %{bmachine:b_get_main_filenumber(MainFN), Nr \= MainFN},!,
891 !,
892 ":", ppterm(Filename).
893 translate_span_file_opt(Span,Print) --> translate_span_file(Span,Print).
894 translate_span_file_opt(_,_) --> "".
895
896
897 explain_span_file(Span) -->
898 {extract_subsidiary_tail_file_name(Span,Filename)},
899 %{bmachine:b_get_main_filenumber(MainFN), Nr \= MainFN},!,
900 "\n### File: ", ppterm(Filename).
901 explain_span_file(_) --> "".
902
903 explain_span(span_predicate(Pred,LS,S)) --> !, explain_span2(span_predicate(Pred,LS,S)),
904 explain_local_state(LS).
905 explain_span(Span) --> explain_span2(Span).
906 explain_span2(Span) --> {extract_line_col(Span,Srow,Scol,Erow,Ecol)},!,
907 "\n### Line: ",ppterm(Srow),", Column: ",ppterm(Scol),
908 " until Line: ",ppterm(Erow),", Column: ",ppterm(Ecol),
909 explain_span_file(Span),
910 explain_span_context(Span).
911 explain_span2(_) --> "".
912
913 explain_span_context(Span) --> {extract_additional_description(Span,Msg),!},
914 "\n### within ", ppterm(Msg). % context of span, such as definition call hierarchy
915 explain_span_context(_) --> "".
916
917 explain_local_state([]) --> !, "".
918 explain_local_state(LS) --> "\n Local State: ", pp_b_state(LS).
919
920 translate_event_error(Error,Out) :-
921 ( translate_event_error2(Error,Out) -> true
922 ; otherwise ->
923 functor(Error,F,_),
924 ajoin(['** Unable to translate event error: ',F,' **'],Out)).
925 translate_event_error2(no_witness_found(Type,Var,_Predicate),Out) :-
926 def_get_texpr_id(Var,Id),
927 ajoin(['no witness was found for ',Type,' ',Id],Out).
928 translate_event_error2(simulation_error(_Events),Out) :-
929 Out = 'no matching abstract event was found'.
930 translate_event_error2(action_not_executable(_Action),Out) :-
931 Out = 'action was not executable'.
932 translate_event_error2(invalid_modification(Var,_Pre,_Post),Out) :-
933 def_get_texpr_id(Var,Id),
934 ajoin(['modification of variable ', Id, ' not allowed'],Out).
935 translate_event_error2(variant_negative(_CType,_Variant,_Value),Out) :-
936 Out = 'enabled for negative variant'.
937 translate_event_error2(invalid_variant(anticipated,_Expr,_Pre,_Post),Out) :-
938 Out = 'variant increased'.
939 translate_event_error2(invalid_variant(convergent,_Expr,_Pre,_Post),Out) :-
940 Out = 'variant not decreased'.
941 translate_event_error2(invalid_theorem_in_guard(_Theorem),Out) :-
942 Out = 'theorem in guard evaluates to false'.
943 translate_event_error2(event_wd_error(_TExpr,Source),Out) :-
944 ajoin(['WD error for ',Source],Out).
945 translate_event_error2(event_other_error(Msg),Out) :- Out=Msg.
946
947 translate_state_error(abort_error(_TYPE,Msg,ErrTerm,ErrorContext),Out) :- !,
948 translate_error_term(ErrTerm,ES),
949 translate_error_context(ErrorContext,EC),
950 ajoin([EC,': ',Msg,': ',ES],Out).
951 translate_state_error('CLPFD_integer_overflow',Out) :- !,
952 Out = 'CLPFD integer overflow'.
953 translate_state_error(max_state_errors_reached(Nr),Out) :- !,
954 ajoin(['Max. number of state errors reached: ', Nr],Out).
955 translate_state_error(Unknown,Out) :-
956 add_error(translate_state_error,'Unknown state error: ',Unknown),
957 Out = '*** Unknown State Error ***'.
958
959
960 explain_error_context1([H],Span) --> !,explain_error_context1(H,Span).
961 explain_error_context1(span_context(Span,Context),Span) --> !,
962 explain_span(Span),"\n",
963 explain_error_context2(Context).
964 explain_error_context1(Ctxt,unknown) --> explain_error_context2(Ctxt).
965
966 explain_error_context2([H]) --> !,explain_error_context2(H).
967 explain_error_context2(span_context(Span,Context)) --> !,
968 explain_span(Span),"\n",
969 explain_error_context2(Context).
970 explain_error_context2(checking_invariant) --> !,
971 {get_specification_description_codes(invariant,I)}, I, ":\n ", %"INVARIANT:\n ",
972 pp_current_state. % assumes explain is called in the right state ! ; otherwise we need to store the state id
973 explain_error_context2(checking_assertions) --> !,
974 {get_specification_description_codes(assertions,A)}, A, ":\n ", %"ASSERTIONS:\n ",
975 pp_current_state. % assumes explain is called in the right state ! ; otherwise we need to store the state id
976 explain_error_context2(checking_negation_of_invariant(State)) --> !,
977 "not(INVARIANT):\n State: ",
978 pp_b_state(State).
979 explain_error_context2(operation('$setup_constants',StateID)) --> !,
980 {get_specification_description_codes(properties,P)}, P, ":\n State: ",
981 pp_context_state(StateID).
982 explain_error_context2(operation(OpName,StateID)) --> !,
983 {get_specification_description_codes(operation,OP)}, OP, ": ", %"EVENT/OPERATION: ",
984 {translate_operation_name(OpName,TOp)},
985 ppterm(TOp), "\n ",
986 pp_context_state(StateID).
987 explain_error_context2(checking_context(Check,Name)) --> !,
988 ppterm(Check),ppterm(Name), "\n ".
989 explain_error_context2(X) --> "UNKNOWN ERROR CONTEXT:\n ", ppterm(X).
990
991 :- use_module(specfile,[get_specification_description/2]).
992 get_specification_description_codes(Tag,Codes) :- get_specification_description(Tag,Atom), atom_codes(Atom,Codes).
993
994 explain_state_error(Error,Span,Out) :-
995 explain_state_error2(Error,Span,Out,[]),!.
996 explain_state_error(_Error,unknown,"Sorry, the detailed output failed.\n").
997
998 explain_abort_error_type(well_definedness_error) --> !, "An expression was not well-defined.\n".
999 explain_abort_error_type(while_variant_error) --> !, "A while-loop VARIANT error occurred.\n".
1000 explain_abort_error_type(while_invariant_violation) --> !, "A while-loop INVARIANT error occurred.\n".
1001 explain_abort_error_type(precondition_error) --> !, "A precondition (PRE) error occurred.\n".
1002 explain_abort_error_type(assert_error) --> !, "An ASSERT error occurred.\n".
1003 explain_abort_error_type(Type) --> "Error occurred: ", ppterm(Type), "\n".
1004
1005 explain_state_error2(abort_error(TYPE,Msg,ErrTerm,ErrContext),Span) -->
1006 explain_abort_error_type(TYPE),
1007 "Reason: ", ppterm(Msg), "\n",
1008 "Details: ", {translate_error_term(ErrTerm,ErrS)},ppterm(ErrS), "\n",
1009 "Context: ", explain_error_context1(ErrContext,Span).
1010 explain_state_error2(max_state_errors_reached(Nr),unknown) -->
1011 "Too many error occurred for this state.\n",
1012 "Not all errors are shown.\n",
1013 "Number of errors is at least: ", ppterm(Nr).
1014 explain_state_error2(eventerror(_Event,Error,Trace),unknown) --> % TO DO: also extract loc info ?
1015 {translate_event_error(Error,Msg)},
1016 ppatom(Msg),
1017 "\nA detailed trace containing the error:\n",
1018 "--------------------------------------\n",
1019 explain_event_trace(Trace).
1020
1021 show_parameter_values([],[]) --> !.
1022 show_parameter_values([P|Prest],[V|Vrest]) -->
1023 show_parameter_value(P,V),
1024 show_parameter_values(Prest,Vrest).
1025 show_parameter_value(P,V) -->
1026 " ",pp_expr(P,_,_LR)," = ",pp_value(V),"\n".
1027
1028 explain_event_trace(Trace,Codes) :-
1029 explain_event_trace(Trace,Codes,[]).
1030
1031 explain_event_trace([]) --> !.
1032 explain_event_trace([Step|Trest]) -->
1033 "\n",
1034 ( explain_event_step(Step) -> ""
1035 ; {functor(Step,F,_)} ->
1036 " (no rule to explain event step ",ppatom(F),")\n"),
1037 explain_event_trace(Trest).
1038 explain_event_step(event(Name,Section)) --> !,
1039 "Event ",ppterm(Name)," in model ",ppterm(Section),
1040 ":\n".
1041 explain_event_step(true_guard(Parameters,Values,Guard)) --> !,
1042 ( {Parameters==[]} -> ""
1043 ; " for the parameters:\n",
1044 show_parameter_values(Parameters,Values)),
1045 " the guard is true:",
1046 explain_predicate(Guard,4),"\n".
1047 explain_event_step(variant_checked_pre(CType,Variant,Value)) -->
1048 " ",ppatom(CType)," event: checking if the variant if non-negative:\n",
1049 " variant: ",pp_expr(Variant,_,_LR),"\n",
1050 " its value: ",pp_value(Value),"\n".
1051 explain_event_step(variant_negative(CType,Variant,Value)) -->
1052 explain_event_step(variant_checked_pre(CType,Variant,Value)),
1053 " ERROR: variant is negative\n".
1054 explain_event_step(variant_checked_post(CType,Variant,EntryValue,ExitValue)) -->
1055 " ",ppatom(CType)," event: checking if the variant is ",
1056 ( {CType==convergent} -> "decreased:\n" ; "not increased:\n"),
1057 " variant: ", pp_expr(Variant,_,_LR), "\n",
1058 " its value before: ", pp_value(EntryValue),"\n",
1059 " its value after: ", pp_value(ExitValue),"\n".
1060 explain_event_step(invalid_variant(CType,Variant,EntryValue,ExitValue)) -->
1061 explain_event_step(variant_checked_post(CType,Variant,EntryValue,ExitValue)),
1062 " ERROR: variant has ",
1063 ({CType==convergent} -> "not been decreased\n"; "has been increased\n").
1064 explain_event_step(eval_witness(Type,Id,Value,Predicate)) -->
1065 witness_intro(Id,Predicate,Type),
1066 " found witness:\n",
1067 " ", pp_expr(Id,_,_LR), " = ", pp_value(Value), "\n".
1068 explain_event_step(no_witness_found(Type,Id,Predicate)) -->
1069 witness_intro(Id,Predicate,Type),
1070 " ERROR: no solution for witness predicate found!\n".
1071 explain_event_step(action(Lhs,_Rhs,Values)) -->
1072 " executing an action:\n",
1073 show_assignments(Lhs,Values).
1074 explain_event_step(action_set(Lhs,_Rhs,ValueSet,Values)) -->
1075 " executing an action:\n ",
1076 pp_expr_l(Lhs,_LR)," :: ",pp_value(ValueSet),"\n choosing\n",
1077 show_assignments(Lhs,Values).
1078 explain_event_step(action_pred(Ids,Pred,Values)) -->
1079 " executing an action:\n ",
1080 pp_expr_l(Ids,_LR1)," :| ",pp_expr(Pred,_,_LR2),"\n choosing\n",
1081 show_assignments(Ids,Values).
1082 explain_event_step(action_not_executable(TAction)) -->
1083 explain_action_not_executable(TAction).
1084 explain_event_step(error(Error,_Id)) -->
1085 % the error marker serves to link to a stored state-error by its ID
1086 explain_event_step(Error).
1087 explain_event_step(simulation_error(Errors)) -->
1088 " no guard of a refined event was satisfiable:\n",
1089 explain_simulation_errors(Errors).
1090 explain_event_step(invalid_theorem_in_guard(Theorem)) -->
1091 " the following theorem evaluates to false:",
1092 explain_predicate(Theorem,4),"\n".
1093 explain_event_step(invalid_modification(Var,Pre,Post)) -->
1094 " the variable ", pp_expr(Var,_,_LR), " has been modified.\n",
1095 " The event is not allowed to modify the variable because its abstract event does not modify it.\n",
1096 " Old value: ", pp_value(Pre), "\n",
1097 " New value: ", pp_value(Post), "\n".
1098 explain_event_step(event_wd_error(TExpr,Source)) -->
1099 " Well-Definedness ERROR for ", ppatom(Source), "\n",
1100 " ", pp_expr(TExpr,_,_LR), "\n".
1101 explain_event_step(event_other_error(Msg)) --> ppatom(Msg).
1102
1103 explain_action_not_executable(TAction) --> {is_assignment_to(TAction,IDs)},!,
1104 " ERROR: the following assignment to ", ppatoms(IDs),"was not executable\n",
1105 " (probably in conflict with another assignment):",
1106 translate_subst_with_indention(TAction,4).
1107 explain_action_not_executable(TAction) -->
1108 " ERROR: the following action was not executable:",
1109 translate_subst_with_indention(TAction,4).
1110
1111 is_assignment_to(b(assign(LHS,_),_,_),IDs) :- get_texpr_ids(LHS,IDs).
1112
1113 witness_intro(Id,Predicate,Type) -->
1114 " evaluating witness for abstract ", ppatom(Type), " ", pp_expr(Id,_,_LR1), "\n",
1115 " witness predicate: ", pp_expr(Predicate,_,_LR2), "\n".
1116
1117 show_assignments([],[]) --> !.
1118 show_assignments([Lhs|Lrest],[Val|Vrest]) -->
1119 " ",pp_expr(Lhs,_,_LimitReached), " := ", pp_value(Val), "\n",
1120 show_assignments(Lrest,Vrest).
1121
1122 /* unused at the moment:
1123 explain_state([]) --> !.
1124 explain_state([bind(Varname,Value)|Rest]) --> !,
1125 " ",ppterm(Varname)," = ",pp_value(Value),"\n",
1126 explain_state(Rest).
1127 explain_guards([]) --> "".
1128 explain_guards([Event|Rest]) -->
1129 {get_texpr_expr(Event,rlevent(Name,_Section,_Status,_Params,Guard,_Theorems,_Act,_VWit,_PWit,_Unmod,_Evt))},
1130 "\n",ppatom(Name),":",
1131 explain_predicate(Guard),
1132 explain_guards(Rest).
1133 explain_predicate(Guard,I,O) :-
1134 explain_predicate(Guard,2,I,O).
1135 */
1136 explain_predicate(Guard,Indention,I,O) :-
1137 pred_over_lines(0,Guard,(Indention,I),(_,O)).
1138
1139 explain_simulation_errors([]) --> !.
1140 explain_simulation_errors([Error|Rest]) -->
1141 explain_simulation_error(Error),
1142 explain_simulation_errors(Rest).
1143 explain_simulation_error(event(Name,Section,Guard)) -->
1144 " guard for event ", ppatom(Name),
1145 " in ", ppatom(Section), ":",
1146 explain_predicate(Guard,6),"\n".
1147
1148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1149 % pretty-print a state
1150
1151
1152 print_state(State) :- b_state(State), !,print_bstate(State).
1153 print_state(csp_and_b_root) :- csp_with_bz_mode, !,
1154 print('(MAIN || B)').
1155 print_state(csp_and_b(CSPState,BState)) :- csp_with_bz_mode, !,
1156 print_bstate(BState), translate_cspm_state(CSPState,Text), print(Text).
1157 print_state(CSPState) :- csp_mode,!,translate_cspm_state(CSPState,Text), print(Text).
1158 print_state(State) :- animation_mode(xtl),!,print(State).
1159 print_state(State) :- print('*** Unknown state: '),print(State).
1160
1161 b_state(root).
1162 b_state(concrete_constants(_)).
1163 b_state(const_and_vars(_,_)).
1164 b_state(expanded_const_and_vars(_,_,_)).
1165 b_state([bind(_,_)|_]).
1166 b_state([]).
1167
1168 print_bstate(State) :- translate_bstate(State,Output), print(' '),print(Output).
1169
1170 translate_any_state(State,Output) :-
1171 pp_any_state(State,Codes,[]),
1172 atom_codes_with_limit(Output,Codes).
1173 translate_bstate(State,Output) :-
1174 pp_b_state(State,Codes,[]),
1175 atom_codes_with_limit(Output,Codes).
1176
1177 % a version which tries to generate smaller strings
1178 translate_bstate_limited(State,Output) :-
1179 temporary_set_preference(expand_avl_upto,2,CHNG),
1180 call_cleanup((pp_b_state(State,Codes,[]),
1181 atom_codes_with_limit(Output,200,Codes)),
1182 reset_temporary_preference(expand_avl_upto,CHNG)).
1183
1184
1185 pp_b_state(X) --> try_pp_b_state(X),!.
1186 pp_b_state(X) --> {add_error(pp_b_state,'Could not translate state: ',X)}.
1187
1188 try_pp_b_state(VAR) --> {var(VAR)},!, "_?VAR?_", {add_error(pp_b_state,'Variable state: ',VAR)}.
1189 try_pp_b_state(root) --> !, "root".
1190 try_pp_b_state(concrete_constants(Constants)) --> !,"Constants: ",
1191 pp_b_state(Constants).
1192 try_pp_b_state(const_and_vars(ID,Vars)) --> !,
1193 "Constants:",ppterm(ID),", Vars:",
1194 {set_translation_constants(ID)}, /* extract constants which stand for deferred set elements */
1195 pp_b_state(Vars),
1196 {clear_translation_constants}.
1197 try_pp_b_state(expanded_const_and_vars(ID,Vars,_)) --> !, "EXPANDED ",
1198 try_pp_b_state(const_and_vars(ID,Vars)).
1199 try_pp_b_state([]) --> !, "/* empty state */".
1200 try_pp_b_state([bind(Varname,Value)|Rest]) --> !,
1201 "( ",ppterm(Varname),"=",
1202 pp_value(Value),
1203 ({Rest = []} -> []; " ",and_symbol,"\n "),
1204 pp_b_state_list(Rest).
1205
1206
1207 pp_b_state_list([]) --> !, " )".
1208 pp_b_state_list([bind(Varname,Value)|Rest]) --> !,
1209 ppterm(Varname),"=",
1210 pp_value(Value),
1211 ({Rest = []} -> [] ; " ",and_symbol,"\n "),
1212 pp_b_state_list(Rest).
1213 pp_b_state_list(X) --> {add_error(pp_b_state_list,'Could not translate: ',X)}.
1214
1215 % a version of pp which generates no newline; can be used for printing SETUP_CONSTANTS, INITIALISATION
1216 pp_b_state_comma_list([],_,_) --> !, ")".
1217 pp_b_state_comma_list(_,Cur,Limit) --> {Cur >= Limit}, !, "...".
1218 pp_b_state_comma_list([bind(Varname,Value)|Rest],Cur,Limit) --> !,
1219 %{print(c(Varname,Cur,Limit)),nl},
1220 start_size(Ref),
1221 ppterm(Varname),"=",
1222 pp_value(Value),
1223 ({Rest = []} -> [] ; ","),
1224 end_size(Ref,Size), % compute size increase wrt Ref point
1225 {Cur1 is Cur+Size},
1226 pp_b_state_comma_list(Rest,Cur1,Limit).
1227 pp_b_state_comma_list(X,_,_) --> {add_error(pp_b_state_comma_list,'Could not translate: ',X)}.
1228
1229 start_size(X,X,X).
1230 end_size(RefVar,Len,X,X) :- % compute how many chars the dcg has added wrt start_size
1231 len(RefVar,X,Len).
1232 ?len(Var,X,Len) :- (var(Var) ; Var==X),!, Len=0.
1233 len([],_,0).
1234 len([_|T],X,Len) :- len(T,X,L1), Len is L1+1.
1235
1236 % can be used e.g. for setup_constants, initialise
1237 translate_b_state_to_comma_list_codes(FUNCTORCODES,State,Limit,ResCodes) :-
1238 pp_b_state_comma_list(State,0,Limit,Codes,[]),
1239 append("(",Codes,C0),
1240 append(FUNCTORCODES,C0,ResCodes).
1241 % ----------------
1242
1243 % printing and translating error contexts
1244 print_context(State) :- translate_context(State,Output), print(Output).
1245
1246 translate_context(Context,Output) :-
1247 pp_b_context(Context,Codes,[]),
1248 atom_codes_with_limit(Output,250,Codes).
1249
1250 pp_b_context([]) --> !.
1251 pp_b_context([C|Rest]) --> !,
1252 pp_b_context(C),
1253 pp_b_context(Rest).
1254 pp_b_context(translate_context) --> !, " ERROR CONTEXT: translate_context". % error occurred within translate_context
1255 pp_b_context(operation(Name,StateID)) --> !,
1256 " ERROR CONTEXT: ",
1257 {get_specification_description_codes(operation,OP)}, OP, ":", % "OPERATION:"
1258 ({var(Name)} -> ppterm('ALL') ; {translate_operation_name(Name,TName)},ppterm(TName)),
1259 ",",pp_context_state(StateID).
1260 pp_b_context(checking_invariant) --> !,
1261 " ERROR CONTEXT: INVARIANT CHECKING,", pp_cur_context_state.
1262 pp_b_context(checking_negation_of_invariant(State)) --> !,
1263 " ERROR CONTEXT: NEGATION_OF_INVARIANT CHECKING, State:", pp_b_state(State).
1264 pp_b_context(checking_assertions) --> !,
1265 " ERROR CONTEXT: ASSERTION CHECKING,", pp_cur_context_state.
1266 pp_b_context(checking_context(Check,Name)) --> !,
1267 ppterm(Check),ppterm(Name).
1268 pp_b_context(C) --> ppterm(C),pp_cur_context_state.
1269
1270 pp_cur_context_state --> {state_space:get_current_context_state(ID)}, !,pp_context_state(ID).
1271 pp_cur_context_state --> ", unknown context state.".
1272
1273 % assumes we are in the right state:
1274 pp_current_state --> {state_space:current_expression(ID,_)}, !,pp_context_state(ID).
1275 pp_current_state --> ", unknown current context state.".
1276
1277 % TO DO: limit length/size of generated error description
1278 pp_context_state(ID) --> {state_space:visited_expression(ID,State)},!, % we have a state ID
1279 " State ID:", ppterm(ID), ",", pp_context_state2(State).
1280 pp_context_state(State) --> pp_context_state3(State).
1281
1282 pp_context_state2(_) --> {debug:debug_mode(off)},!.
1283 pp_context_state2(State) --> pp_context_state3(State).
1284
1285 pp_context_state3(State) --> " State: ",pp_any_state_with_limit(State,10).
1286
1287 pp_any_state_with_limit(State,Limit) -->
1288 {get_preference(expand_avl_upto,CurLim),
1289 (CurLim<0 ; Limit < CurLim),
1290 !,
1291 temporary_set_preference(expand_avl_upto,Limit,CHNG)},
1292 pp_any_state(State),
1293 {reset_temporary_preference(expand_avl_upto,CHNG)}.
1294 pp_any_state_with_limit(State,_Limit) --> pp_any_state(State).
1295
1296 pp_any_state(X) --> try_pp_b_state(X),!.
1297 pp_any_state(csp_and_b(P,B)) --> "CSP: ",{pp_csp_process(P,Atoms,[])},!,atoms_to_codelist(Atoms),
1298 " || B: ", try_pp_b_state(B).
1299 pp_any_state(P) --> "CSP: ",{pp_csp_process(P,Atoms,[])},!,atoms_to_codelist(Atoms).
1300 pp_any_state(X) --> "Other formalism: ",ppterm(X). % CSP state
1301
1302 atoms_to_codelist([]) --> [].
1303 atoms_to_codelist([Atom|T]) --> ppterm(Atom), atoms_to_codelist(T).
1304
1305 % ----------------
1306
1307 :- dynamic deferred_set_constant/3.
1308
1309 set_translation_context(const_and_vars(ConstID,_)) :- !,
1310 %% print_message(setting_translation_constants(ConstID)),
1311 set_translation_constants(ConstID).
1312 set_translation_context(expanded_const_and_vars(ConstID,_,_)) :- !,
1313 set_translation_constants(ConstID).
1314 set_translation_context(_).
1315
1316 set_translation_constants(_) :- clear_translation_constants,
1317 get_preference(dot_print_use_constants,false),!.
1318 set_translation_constants(ConstID) :- var(ConstID),!,
1319 add_error(set_translation_constants,'Variable used as ConstID: ',ConstID).
1320 set_translation_constants(ConstID) :-
1321 state_space:visited_expression(ConstID,concrete_constants(ConstantsStore)),!,
1322 %% print_message(setting_constants(ConstID)),%%
1323 (treat_constants(ConstantsStore) -> true ; print_message(fail)).
1324 set_translation_constants(ConstID) :-
1325 add_error(set_translation_constants,'Unknown ConstID: ',ConstID).
1326
1327 clear_translation_constants :- %print_message(clearing),%%
1328 retractall(deferred_set_constant(_,_,_)).
1329
1330 treat_constants([]).
1331 treat_constants([bind(CstName,Val)|T]) :-
1332 ((Val=fd(X,GSet),b_global_deferred_set(GSet))
1333 -> (deferred_set_constant(GSet,X,_)
1334 -> true /* duplicate def of value */
1335 ; assert(deferred_set_constant(GSet,X,CstName))
1336 )
1337 ; true
1338 ),
1339 treat_constants(T).
1340
1341
1342
1343 translate_bvalue_with_tlatype(Value,Type,Output) :-
1344 ( pp_tla_value(Type,Value,Codes,[]) ->
1345 atom_codes_with_limit(Output,Codes)
1346 ; add_error(translate_bvalue,'Could not translate TLA value: ',Value),
1347 Output='???').
1348
1349 pp_tla_value(function(_Type1,_Type2),[]) --> !,
1350 ppcodes("<<>>").
1351 pp_tla_value(function(integer,T2),avl_set(Set)) -->
1352 {convert_avlset_into_sequence(Set,Seq)}, !,
1353 pp_tla_with_sep("<< "," >>",",",T2,Seq).
1354 pp_tla_value(function(T1,T2),Set) -->
1355 {is_printable_set(Set,Values)},!,
1356 pp_tla_with_sep("(",")"," @@ ",function_value(T1,T2),Values).
1357 pp_tla_value(function_value(T1,T2),(L,R)) -->
1358 !,pp_tla_value(T1,L),":>",pp_tla_value(T2,R).
1359 pp_tla_value(set(Type),Set) -->
1360 {is_printable_set(Set,Values)},!,
1361 pp_tla_with_sep("{","}",",",Type,Values).
1362 pp_tla_value(tuple(Types),Value) -->
1363 {pairs_to_list(Types,Value,Values,[]),!},
1364 pp_tla_with_sep("<< "," >>",",",Types,Values).
1365 pp_tla_value(record(Fields),rec(FieldValues)) -->
1366 % TODO: Check if we can safely assume that Fields and FieldValues have the
1367 % same order
1368 !, {sort_tla_fields(Fields,FieldValues,RFields,RFieldValues)},
1369 pp_tla_with_sep("[","]",", ",RFields,RFieldValues).
1370 pp_tla_value(field(Name,Type),field(_,Value)) -->
1371 !, ppatom_opt_scramble(Name)," |-> ",pp_tla_value(Type,Value).
1372 pp_tla_value(_Type,Value) -->
1373 % fallback: use B's pretty printer
1374 pp_value(Value).
1375
1376 is_printable_set(avl_set(A),List) :- avl_domain(A,List).
1377 is_printable_set([],[]).
1378 is_printable_set([H|T],[H|T]).
1379
1380 pairs_to_list([_],Value) --> !,[Value].
1381 pairs_to_list([_|Rest],(L,R)) -->
1382 pairs_to_list(Rest,L),[R].
1383
1384
1385 sort_tla_fields([],_,[],[]).
1386 sort_tla_fields([Field|RFields],ValueFields,RFieldTypes,ResultValueFields) :-
1387 ( Field=field(Name,Type) -> true
1388 ; Field= opt(Name,Type) -> true),
1389 ( selectchk(field(Name,Value),ValueFields,RestValueFields),
1390 field_value_present(Field,Value,Result) ->
1391 % Found the field in the record value
1392 RFieldTypes = [field(Name,Type) |RestFields],
1393 ResultValueFields = [field(Name,Result)|RestValues],
1394 sort_tla_fields(RFields,RestValueFields,RestFields,RestValues)
1395 ; otherwise ->
1396 % didn't found the field in the value -> igore
1397 sort_tla_fields(RFields,ValueFields,RFieldTypes,ResultValueFields)
1398 ).
1399 field_value_present(field(_,_),RecValue,RecValue). % Obligatory fields are always present
1400 field_value_present(opt(_,_),OptValue,Value) :-
1401 % Optional fields are present if the field is of the form TRUE |-> Value.
1402 ( is_printable_set(OptValue,Values) -> Values=[(_TRUE,Value)]
1403 ; otherwise ->
1404 add_error(translate,'exptected set for TLA optional record field'),
1405 fail
1406 ).
1407
1408 pp_tla_with_sep(Start,End,Sep,Type,Values) -->
1409 ppcodes(Start),pp_tla_with_sep_aux(Values,End,Sep,Type).
1410 pp_tla_with_sep_aux([],End,_Sep,_Type) -->
1411 ppcodes(End).
1412 pp_tla_with_sep_aux([Value|Rest],End,Sep,Type) -->
1413 % If a single type is given, we interpret it as the type
1414 % for each element of the list, if it is a list, we interpret
1415 % it one different type for every value in the list.
1416 { ( Type=[CurrentType|RestTypes] -> true
1417 ; otherwise -> CurrentType = Type, RestTypes=Type) },
1418 pp_tla_value(CurrentType,Value),
1419 ( {Rest=[_|_]} -> ppcodes(Sep); {true} ),
1420 pp_tla_with_sep_aux(Rest,End,Sep,RestTypes).
1421
1422
1423 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1424 % pretty-print a value
1425 translate_bvalue_to_codes(V,Output) :-
1426 ( pp_value(V,_LimitReached,Codes,[]) ->
1427 Output=Codes
1428 ; add_error(translate_bvalue_to_codes,'Could not translate bvalue: ',V),
1429 Output="???").
1430 translate_bvalue(V,Output) :-
1431 %set_up_limit_reached(Codes,1000000,LimitReached), % we could set a very high-limit, like max_atom_length
1432 ( pp_value(V,_LimitReached,Codes,[]) ->
1433 atom_codes_with_limit(Output,Codes) % just catches representation error
1434 ; add_error(translate_bvalue,'Could not translate bvalue: ',V),
1435 Output='???').
1436 :- use_module(preferences).
1437 translate_bvalue_with_limit(V,Limit,Output) :-
1438 get_preference(expand_avl_upto,Max),
1439 ((Max>Limit % no sense in printing larger AVL trees
1440 ; Max = -1) % or setting limit to -1 for full value
1441 -> set_preference(expand_avl_upto,Limit)
1442 ; true),
1443 call_cleanup(translate_bvalue_with_limit_aux(V,Limit,Output),
1444 set_preference(expand_avl_upto,Max)).
1445 translate_bvalue_with_limit_aux(V,Limit,Output) :-
1446 set_up_limit_reached(Codes,Limit,LimitReached),
1447 ( pp_value(V,LimitReached,Codes,[]) ->
1448 atom_codes_with_limit(Output,Limit,Codes)
1449 % ,length(Codes,Len), (Len>Limit -> format('pp(~w) codes:~w, limit:~w, String=~s~n~n',[LimitReached,Len,Limit,Codes]) ; true)
1450 ; add_error(translate_bvalue_with_limit,'Could not translate bvalue: ',V),
1451 Output='???').
1452
1453 translate_bvalues(Values,Output) :-
1454 %set_up_limit_reached(Codes,1000000,LimitReached), % we could set a very high-limit, like max_atom_length
1455 pp_value_l(Values,',',_LimitReached,Codes,[]),!,
1456 atom_codes_with_limit(Output,Codes).
1457 translate_bvalues(Values,O) :-
1458 add_internal_error('Call failed: ',translate_bvalues(Values,O)), O='??'.
1459
1460 translate_bvalue_for_expression(Value,TExpr,Output) :-
1461 animation_minor_mode(tla),
1462 expression_has_tla_type(TExpr,TlaType),!,
1463 translate_bvalue_with_tlatype(Value,TlaType,Output).
1464 translate_bvalue_for_expression(Value,TExpr,Output) :-
1465 get_texpr_type(TExpr,Type),
1466 translate_bvalue_with_type(Value,Type,Output).
1467
1468 translate_bvalue_for_expression_with_limit(Value,TExpr,_Limit,Output) :-
1469 animation_minor_mode(tla),
1470 expression_has_tla_type(TExpr,TlaType),!,
1471 translate_bvalue_with_tlatype(Value,TlaType,Output). % TO DO: treat Limit
1472 translate_bvalue_for_expression_with_limit(Value,TExpr,Limit,Output) :-
1473 get_texpr_type(TExpr,Type),
1474 translate_bvalue_with_type_and_limit(Value,Type,Limit,Output).
1475
1476 expression_has_tla_type(TExpr,Type) :-
1477 get_texpr_info(TExpr,Infos),
1478 memberchk(tla_type(Type),Infos).
1479
1480 % a more refined pretty printing: takes Type information into account; useful for detecting sequences
1481 translate_bvalue_with_type(Value,_,Output) :- var(Value),!,
1482 translate_bvalue(Value,Output).
1483 translate_bvalue_with_type(Value,Type,Output) :-
1484 adapt_value_according_to_type(Type,Value,NewValue),
1485 translate_bvalue(NewValue,Output).
1486
1487 translate_bvalue_with_type_and_limit(Value,Type,Limit,Output) :-
1488 get_preference(expand_avl_upto,CurLim),
1489 SetLim is Limit//2, % at least two symbols per element
1490 %print(translate(SetLim,CurLim)),nl,
1491 (CurLim<0 ; SetLim < CurLim),!,
1492 temporary_set_preference(expand_avl_upto,SetLim,CHNG),
1493 translate_bvalue_with_type_and_limit2(Value,Type,Limit,Output),
1494 reset_temporary_preference(expand_avl_upto,CHNG).
1495 translate_bvalue_with_type_and_limit(Value,Type,Limit,Output) :-
1496 translate_bvalue_with_type_and_limit2(Value,Type,Limit,Output).
1497 translate_bvalue_with_type_and_limit2(Value,_,Limit,Output) :- var(Value),!,
1498 translate_bvalue_with_limit(Value,Limit,Output).
1499 translate_bvalue_with_type_and_limit2(Value,Type,Limit,Output) :-
1500 adapt_value_according_to_type(Type,Value,NewValue),
1501 translate:translate_bvalue_with_limit(NewValue,Limit,Output).
1502 %debug:watch(translate:translate_bvalue_with_limit(NewValue,Limit,Output)).
1503
1504 :- use_module(avl_tools,[quick_avl_approximate_size/2]).
1505 adapt_value_according_to_type(integer,V,R) :- !,R=V.
1506 adapt_value_according_to_type(string,V,R) :- !,R=V.
1507 adapt_value_according_to_type(boolean,V,R) :- !,R=V.
1508 adapt_value_according_to_type(global(_),V,R) :- !,R=V.
1509 adapt_value_according_to_type(couple(TA,TB),(VA,VB),R) :- !, R=(RA,RB),
1510 adapt_value_according_to_type(TA,VA,RA),
1511 adapt_value_according_to_type(TB,VB,RB).
1512 adapt_value_according_to_type(set(Type),avl_set(A),Res) :-
1513 quick_avl_approximate_size(A,S),S<20,
1514 custom_explicit_sets:expand_custom_set_to_list(avl_set(A),List),!,
1515 maplist(adapt_value_according_to_type(Type),List,Res).
1516 adapt_value_according_to_type(set(_Type),V,R) :- !,R=V.
1517 adapt_value_according_to_type(seq(Type),V,R) :- !,
1518 (convert_set_into_sequence(V,VS)
1519 -> l_adapt_value_according_to_type(VS,Type,AVS),
1520 R=sequence(AVS)
1521 ; R=V).
1522 adapt_value_according_to_type(record(_Fields),Value,R) :- !, % to do: convert inside record
1523 R=Value.
1524 adapt_value_according_to_type(freetype(_),Value,R) :- !, R=Value.
1525 adapt_value_according_to_type(any,Value,R) :- !, R=Value.
1526 adapt_value_according_to_type(Type,Value,R) :- print(adapt_value_according_to_type_unknown(Type,Value)),nl,
1527 R=Value.
1528
1529 l_adapt_value_according_to_type([],_Type,R) :- !,R=[].
1530 l_adapt_value_according_to_type([H|T],Type,[AH|AT]) :-
1531 adapt_value_according_to_type(Type,H,AH),
1532 l_adapt_value_according_to_type(T,Type,AT).
1533
1534 pp_value_with_type(E,T,LimitReached) --> {adapt_value_according_to_type(T,E,AdaptedE)},
1535 pp_value(AdaptedE,LimitReached).
1536
1537 pp_value(V,In,Out) :- set_up_limit_reached(In,1000,LimitReached),
1538 pp_value(V,LimitReached,In,Out).
1539
1540 % LimitReached is a flag: when it is grounded to limit_reached this instructs pp_value to stop generating output
1541 pp_value(_,LimitReached) --> {LimitReached==limit_reached},!, "...".
1542 pp_value(V,_) --> {var(V)},!,underscore_symbol.
1543 pp_value('$VAR'(N),_) --> !,pp_numberedvar(N).
1544 pp_value(X,_) --> {cyclic_term(X)},!,underscore_symbol,"cyclic",underscore_symbol.
1545 pp_value(fd(X),_) --> !,ppatom(X). %% ???
1546 pp_value(fd(X,GSet),_) --> {var(X)},!,
1547 ppatom(GSet),":", ppnumber(X). %":??".
1548 pp_value(fd(X,GSet),_) -->
1549 {b_global_sets:is_b_global_constant(GSet,X,Res)},!,
1550 ppatom_opt_scramble(Res).
1551 pp_value(fd(X,GSet),_) --> {deferred_set_constant(GSet,X,Cst)},!,
1552 ppatom_opt_scramble(Cst).
1553 pp_value(fd(X,M),_) --> !,ppatom_opt_scramble(M),ppnumber(X).
1554 pp_value(int(X),_) --> !,ppnumber(X).
1555 pp_value(string(X),_) --> !,string_start_symbol,ppstring_opt_scramble(X),string_end_symbol.
1556 pp_value(global_set(X),_) --> {atomic(X),integer_set_mapping(X,Y)},!,ppatom(Y).
1557 pp_value(term(X),_) --> {var(X)},!,"term(",underscore_symbol,")".
1558 pp_value(freetype(X),_) --> {pretty_freetype(X,P)},!,ppatom_opt_scramble(P).
1559 pp_value(pred_true /* bool_true */,_) --> %!,"TRUE". % TO DO: in latex_mode: surround by mathit
1560 {constants_in_mode(pred_true,Symbol)},!,ppatom(Symbol).
1561 pp_value(pred_false /* bool_false */,_) --> %!,"FALSE".
1562 {constants_in_mode(pred_false,Symbol)},!,ppatom(Symbol).
1563 %pp_value(bool_true) --> !,"TRUE". % old version; still in some test traces which are printed
1564 %pp_value(bool_false) --> !,"FALSE".
1565 pp_value([],_) --> !,empty_set_symbol.
1566 pp_value(freeval(_,Case,Value),_) -->
1567 {ground(Case),ground(Value),Value=term(Case)},!,ppatom_opt_scramble(Case).
1568 pp_value(sequence(List),LimitReached) --> !,
1569 ({List=[]} -> pp_empty_sequence ; pp_sequence_with_limit(List,LimitReached)).
1570 pp_value([Head|Tail],LimitReached) --> {get_preference(translate_print_all_sequences,true),
1571 convert_set_into_sequence([Head|Tail],Elements)},
1572 !,
1573 pp_sequence(Elements,LimitReached).
1574 pp_value([Head|Tail],LimitReached) --> !, {set_brackets(L,R)},
1575 ppatom(L),
1576 pp_value_l_with_limit([Head|Tail],',',LimitReached),
1577 ppatom(R).
1578 %pp_value([Head|Tail]) --> !,
1579 % {( convert_set_into_sequence([Head|Tail],Elements) ->
1580 % (Start,End) = ('[',']')
1581 % ; otherwise ->
1582 % Elements = [Head|Tail],
1583 % (Start,End) = ('{','}'))},
1584 % ppatom(Start),pp_value_l(Elements,','),ppatom(End).
1585 pp_value( (A,B) ,LimitReached) --> !,
1586 "(",pp_inner_value(A,LimitReached),
1587 maplet_symbol,
1588 pp_value(B,LimitReached),")".
1589 pp_value(avl_set(A),LimitReached) --> !,
1590 {avl_size(A,Sz)},
1591 {set_brackets(LBrace,RBrace)},
1592 ? ( {size_is_in_set_limit(Sz),(Sz>2 ; get_preference(translate_print_all_sequences,true)),
1593 avl_max(A,(int(Sz),_)), % a sequence has minimum int(1) and maximum int(Sz)
1594 convert_avlset_into_sequence(A,Seq)} ->
1595 pp_sequence(Seq,LimitReached)
1596 ; {otherwise} ->
1597 ( {Sz=0} -> left_set_bracket," /* empty avl_set */ ",right_set_bracket
1598 ? ; {(size_is_in_set_limit(Sz) ; Sz < 3)} -> % if Sz 3 we will print at least two elements anyway
1599 {avl_domain(A,List)},
1600 ppatom(LBrace),pp_value_l(List,',',LimitReached),ppatom(RBrace)
1601 ; {(Sz<5 ; \+ size_is_in_set_limit(4))} ->
1602 {avl_min(A,Min),avl_max(A,Max)},
1603 hash_card_symbol, % "#"
1604 ppnumber(Sz),":", left_set_bracket,
1605 pp_value(Min,LimitReached),",",ldots,",",pp_value(Max,LimitReached),right_set_bracket
1606 ; {otherwise} ->
1607 {avl_min(A,Min),avl_next(Min,A,Nxt),avl_max(A,Max),avl_prev(Max,A,Prev)},
1608 hash_card_symbol, % "#",
1609 ppnumber(Sz),":", left_set_bracket,
1610 pp_value(Min,LimitReached),",",pp_value(Nxt,LimitReached),",",ldots,",",
1611 pp_value(Prev,LimitReached),",",pp_value(Max,LimitReached),right_set_bracket )).
1612
1613 pp_value(field(Name,Value),LimitReached) --> !,
1614 ppatom_opt_scramble(Name),":",pp_value(Value,LimitReached). % : for fields has priority 120 in French manual
1615 pp_value(rec(Rec),LimitReached) --> !,
1616 {function_like_in_mode(rec,Symbol)},
1617 ppatom(Symbol), "(",pp_value_l(Rec,',',LimitReached),")".
1618 pp_value(struct(Rec),LimitReached) --> !,
1619 {function_like_in_mode(struct,Symbol)},
1620 ppatom(Symbol), "(", pp_value_l(Rec,',',LimitReached),")".
1621 pp_value(term(no_value_for(Id)),_) --> !,
1622 "undefined ",ppatom(Id).
1623 pp_value(closure(Ids,Type,B),_LimitReached) -->
1624 {var(Ids) ; var(Type) ; var(B)},!,
1625 add_internal_error('Illegal value: ',pp_value_illegal_closure(Ids,Type,B)),
1626 "<< ILLEGAL ",write_to_codes(closure(Ids,Type,B))," >>".
1627 pp_value(closure([Id],[Type],Membership),LimitReached) -->
1628 { get_texpr_expr(Membership,member(Elem,Set)),
1629 get_texpr_id(Elem,Id),get_texpr_type(Elem,Type),!},
1630 pp_expr_m(Set,299,LimitReached).
1631 pp_value(closure(Variables,Types,Predicate),LimitReached) --> {\+ size_is_in_set_limit(1)},
1632 !, % do not print body; just print hash value
1633 {make_closure_ids(Variables,Types,Ids), term_hash(Predicate,PH)},
1634 left_set_bracket, % { Ids | #PREDICATE#(HASH) }
1635 pp_expr_l_pair_in_mode(Ids,LimitReached),
1636 pp_such_that_bar,
1637 " ",hash_card_symbol,"PREDICATE",hash_card_symbol,"(",ppnumber(PH),") ", right_set_bracket.
1638 pp_value(closure(Variables,Types,Predicate),LimitReached) --> !,
1639 {make_closure_ids(Variables,Types,Ids)},
1640 pp_comprehension_set(Ids,Predicate,LimitReached).% TODO: propagate LimitReached
1641 pp_value(freeval(_,Case,Value),LimitReached) --> {ground(Case)},!,
1642 ppatom_opt_scramble(Case),"(",pp_value(Value,LimitReached),")".
1643 pp_value(X,_) --> {animation_mode(xtl)},!,
1644 write_to_codes(X).
1645 pp_value(X,_) --> % the << >> pose problems when checking against FDR
1646 "<< ",write_to_codes(X)," >>".
1647
1648 % avoid printing parentheses:
1649 % (x,y,z) = ((x,y),z)
1650 pp_inner_value( (A,B) , LimitReached) --> !, % do not print parentheses in this context
1651 pp_inner_value(A,LimitReached),maplet_symbol,
1652 pp_value(B,LimitReached).
1653 pp_inner_value( Value , LimitReached) --> pp_value( Value , LimitReached).
1654
1655 size_is_in_set_limit(Size) :- get_preference(expand_avl_upto,Max),
1656 (Max<0 -> true /* no limit */
1657 ; Size =< Max).
1658
1659 % instantiate LimitReached argument as soon as a list exceeds a certain limit
1660 set_up_limit_reached(_,Neg,_) :- Neg<0,!. % negative number means unlimited
1661 set_up_limit_reached(_,0,LimitReached) :- !, LimitReached = limit_reached.
1662 set_up_limit_reached(List,Limit,LimitReached) :-
1663 block_set_up_limit_reached(List,Limit,LimitReached).
1664 :- block block_set_up_limit_reached(-,?,?).
1665 block_set_up_limit_reached([],_,_).
1666 block_set_up_limit_reached([_|T],Limit,LimitReached) :-
1667 (Limit<1 -> LimitReached=limit_reached
1668 ; L1 is Limit-1, block_set_up_limit_reached(T,L1,LimitReached)).
1669
1670 % pretty print LimitReached, requires %:- block block_set_up_limit_reached(-,?,-).
1671 /*
1672 pp_lr(LR) --> {LR==limit_reached},!, " *LR* ".
1673 pp_lr(LR) --> {frozen(LR,translate:block_set_up_limit_reached(_,Lim,_))},!, " ok(", ppnumber(Lim),") ".
1674 pp_lr(LR) --> {frozen(LR,G)},!, " ok(", ppterm(G),") ".
1675 pp_lr(_) --> " ok ".
1676 */
1677
1678
1679 pp_value_l_with_limit(V,Sep,LimitReached) --> {get_preference(expand_avl_upto,Max)},
1680 pp_value_l(V,Sep,Max,LimitReached).
1681 pp_value_l(V,Sep,LimitReached) --> pp_value_l(V,Sep,-1,LimitReached).
1682
1683 pp_value_l(V,_Sep,_,_) --> {var(V)},!,"...".
1684 pp_value_l(_,_,_,LimitReached) --> {LimitReached==limit_reached},!,"...".
1685 pp_value_l('$VAR'(N),_Sep,_,_) --> !,"}\\/{",pp_numberedvar(N),"}".
1686 pp_value_l([],_Sep,_,_) --> !.
1687 pp_value_l([Expr|Rest],Sep,Limit,LimitReached) -->
1688 ( {nonvar(Rest),Rest=[]} ->
1689 pp_value(Expr,LimitReached)
1690 ; {Limit=0} -> "..."
1691 ; {otherwise} ->
1692 pp_value(Expr,LimitReached),
1693 % no separator for closure special case
1694 ({nonvar(Rest) , Rest = closure(_,_,_)} -> {true} ; ppatom(Sep)) ,
1695 {L1 is Limit-1} ,
1696 % convert avl_set(_) in a list's tail to a Prolog list
1697 {nonvar(Rest) , Rest = avl_set(_) -> custom_explicit_sets:expand_custom_set_to_list(Rest,LRest) ; LRest = Rest} ,
1698 pp_value_l(LRest,Sep,L1,LimitReached)).
1699 pp_value_l(avl_set(A),_Sep,_,LimitReached) --> pp_value(avl_set(A),LimitReached).
1700 pp_value_l(closure(A,B,C),_Sep,_,LimitReached) --> "}\\/", pp_value(closure(A,B,C),LimitReached).
1701
1702 make_closure_ids([],[],[]).
1703 make_closure_ids([V|Vrest],[T|Trest],[TExpr|TErest]) :-
1704 create_texpr(identifier(V),T,[],TExpr),
1705 make_closure_ids(Vrest,Trest,TErest).
1706
1707 % symbol for starting and ending a sequence:
1708 pp_begin_sequence --> {animation_minor_mode(tla)},!,"<<".
1709 pp_begin_sequence --> {get_preference(translate_print_cs_style_sequences,true)},!,"".
1710 pp_begin_sequence --> "[".
1711 pp_end_sequence --> {animation_minor_mode(tla)},!,">>".
1712 pp_end_sequence --> {get_preference(translate_print_cs_style_sequences,true)},!,"".
1713 pp_end_sequence --> "]".
1714
1715 pp_separator_sequence('') :- get_preference(translate_print_cs_style_sequences,true),!.
1716 pp_separator_sequence(',').
1717
1718 % string for empty sequence
1719 pp_empty_sequence --> {animation_minor_mode(tla)},!, "<< >>".
1720 pp_empty_sequence --> {get_preference(translate_print_cs_style_sequences,true)},!,
1721 ( {latex_mode} -> "\\lambda" ; [955]). % 955 is lambda symbol in Unicode
1722 pp_empty_sequence --> "[]".
1723
1724 % symbols for function application:
1725 pp_function_left_bracket --> {animation_minor_mode(tla)},!, "[".
1726 pp_function_left_bracket --> "(".
1727
1728 pp_function_right_bracket --> {animation_minor_mode(tla)},!, "]".
1729 pp_function_right_bracket --> ")".
1730
1731 pp_sequence(Elements,LimitReached) --> {pp_separator_sequence(Sep)},
1732 pp_begin_sequence,
1733 pp_value_l(Elements,Sep,LimitReached),
1734 pp_end_sequence.
1735 pp_sequence_with_limit(Elements,LimitReached) --> {pp_separator_sequence(Sep)},
1736 pp_begin_sequence,
1737 pp_value_l_with_limit(Elements,Sep,LimitReached),
1738 pp_end_sequence.
1739
1740 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1741 % machines
1742
1743 :- use_module(eventhandling,[register_event_listener/3]).
1744 :- register_event_listener(clear_specification,reset_translate,
1745 'Reset Translation Caches.').
1746 reset_translate :- retractall(bugly_scramble_id_cache(_,_)), retractall(non_det_constants(_,_)).
1747 %reset_translate :- set_print_type_infos(none),
1748 % set_preference(translate_suppress_rodin_positions_flag,false).
1749
1750 suppress_rodin_positions :-
1751 set_preference(translate_suppress_rodin_positions_flag,true).
1752
1753 set_print_type_infos(none) :- !,
1754 set_preference(translate_force_all_typing_infos,false),
1755 set_preference(translate_print_typing_infos,false).
1756 set_print_type_infos(needed) :- !,
1757 set_preference(translate_force_all_typing_infos,false),
1758 set_preference(translate_print_typing_infos,true).
1759 set_print_type_infos(all) :- !,
1760 set_preference(translate_force_all_typing_infos,true),
1761 set_preference(translate_print_typing_infos,true).
1762 set_print_type_infos(Err) :-
1763 add_internal_error('Illegal type: ',set_print_type_infos(Err)).
1764
1765
1766 :- use_module(tools_files,[put_codes/2]).
1767 print_machine(M) :-
1768 nl, translate_machine(M,Msg,true), put_codes(Msg,user_output), nl,
1769 flush_output(user_output),!.
1770 print_machine(M) :- add_internal_error('Printing failed: ',print_machine(M)).
1771
1772
1773 translate_machine(M,Codes,AdditionalInfo) :-
1774 temporary_set_preference(translate_ids_to_parseable_format,true,CHNG),
1775 retractall(print_additional_machine_info),
1776 (AdditionalInfo=true -> assert(print_additional_machine_info) ; true),
1777 call_cleanup(translate_machine1(M,(0,Codes),(_,[])),
1778 reset_temporary_preference(translate_ids_to_parseable_format,CHNG)).
1779
1780 % useful if we wish to translate just a selection of sections without MACHINE/END
1781 translate_section_list(SL,Codes) :- init_machine_translation,
1782 translate_machine2(SL,SL,no_end,(0,Codes),(_,[])).
1783
1784 translate_machine1(machine(Name,Sections)) -->
1785 indent('MACHINE '), {adapt_machine_name(Name,AName)}, insertstr(AName),
1786 {init_machine_translation},
1787 translate_machine2(Sections,Sections,end).
1788 translate_machine2([],_,end) --> !, insertstr('\nEND\n').
1789 translate_machine2([],_,_) --> !, insertstr('\n').
1790 translate_machine2([P|Rest],All,End) -->
1791 translate_mpart(P,All),
1792 translate_machine2(Rest,All,End).
1793
1794 adapt_machine_name('dummy(uses)',R) :- !,R='MAIN'.
1795 adapt_machine_name(X,X).
1796
1797 :- dynamic section_header_generated/1.
1798 :- dynamic print_additional_machine_info/0.
1799 print_additional_machine_info.
1800
1801 init_machine_translation :- retractall(section_header_generated(_)).
1802
1803 % start a part of a section
1804 mpstart(Title,I) -->
1805 insertstr('\n'),insertstr(Title),
1806 indention_level(I,I2), {I2 is I+2}.
1807 % end a part of a section
1808 mpend(I) -->
1809 indention_level(_,I).
1810
1811 mpstart_section(Section,Title,AltTitle,I,In,Out) :-
1812 (\+ section_header_generated(Section)
1813 -> mpstart(Title,I,In,Out), assert(section_header_generated(Section))
1814 ; mpstart(AltTitle,I,In,Out) /* use alternative title; section header already generated */
1815 ).
1816
1817 translate_mpart(Section/I,All) --> %{print(Section),nl},
1818 ( {I=[]} -> {true}
1819 ; translate_mpart2(Section,I,All) -> {true}
1820 ; {otherwise} ->
1821 insertstr('\nSection '),insertstr(Section),insertstr(': '),
1822 insertstr('<< pretty-print failed >>')
1823 ).
1824 translate_mpart2(deferred_sets,I,_) -->
1825 mpstart_section(sets,'SETS /* deferred */',' ; /* deferred */',P),
1826 indent_expr_l_sep(I,';'),mpend(P).
1827 translate_mpart2(enumerated_sets,_I,_) --> []. % these are now pretty printed below
1828 %mpstart('ENUMERATED SETS',P),indent_expr_l_sep(I,';'),mpend(P).
1829 translate_mpart2(enumerated_elements,I,_) --> %{print(enum_els(I)),nl},
1830 {translate_enums(I,[],Res)},
1831 mpstart_section(sets,'SETS /* enumerated */',' ; /* enumerated */',P),
1832 indent_expr_l_sep(Res,';'),mpend(P).
1833 translate_mpart2(parameters,I,_) --> mpstart('PARAMETERS',P),indent_expr_l_sep(I,','),mpend(P).
1834 translate_mpart2(internal_parameters,I,_) --> {print_additional_machine_info},!,mpstart('/* INTERNAL_PARAMETERS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).
1835 translate_mpart2(internal_parameters,_I,_) --> [].
1836 translate_mpart2(abstract_variables,I,_) --> mpstart('ABSTRACT_VARIABLES',P),indent_expr_l_sep(I,','),mpend(P).
1837 translate_mpart2(concrete_variables,I,_) --> mpstart('CONCRETE_VARIABLES',P),indent_expr_l_sep(I,','),mpend(P).
1838 translate_mpart2(abstract_constants,I,_) --> mpstart('ABSTRACT_CONSTANTS',P),indent_expr_l_sep(I,','),mpend(P).
1839 translate_mpart2(concrete_constants,I,_) --> mpstart('CONCRETE_CONSTANTS',P),indent_expr_l_sep(I,','),mpend(P).
1840 translate_mpart2(promoted,I,_) --> {print_additional_machine_info},!,
1841 mpstart('/* PROMOTED OPERATIONS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).
1842 translate_mpart2(promoted,_I,_) --> [].
1843 translate_mpart2(unpromoted,I,_) --> {print_additional_machine_info},!,
1844 mpstart('/* NOT PROMOTED OPERATIONS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).
1845 translate_mpart2(unpromoted,_I,_) --> [].
1846 translate_mpart2(constraints,I,All) --> mpart_typing('CONSTRAINTS',[parameters],All,I).
1847 translate_mpart2(invariant,I,All) --> mpart_typing('INVARIANT', [abstract_variables,concrete_variables],All,I).
1848 translate_mpart2(linking_invariant,_I,_) --> [].
1849 translate_mpart2(properties,I,All) --> mpart_typing('PROPERTIES',[abstract_constants,concrete_constants],All,I).
1850 translate_mpart2(assertions,I,_) --> mpstart('ASSERTIONS',P),indent_expr_l_sep(I,';'),mpend(P).
1851 translate_mpart2(initialisation,S,_) --> mpstart('INITIALISATION',P),translate_inits(S),mpend(P).
1852 translate_mpart2(definitions,Defs,_) --> {print_additional_machine_info},!,mpstart('/* DEFINITIONS',P),translate_defs(Defs),insertstr(' */'),mpend(P).
1853 translate_mpart2(definitions,_Defs,_) --> [].
1854 translate_mpart2(operation_bodies,Ops,_) --> mpstart('OPERATIONS',P),translate_ops(Ops),mpend(P).
1855 translate_mpart2(used,Used,_) --> {print_additional_machine_info},!,mpstart('/* USED',P),translate_used(Used),insertstr(' */'),mpend(P).
1856 translate_mpart2(used,_Used,_) --> [].
1857 translate_mpart2(freetypes,Freetypes,_) --> mpstart('FREETYPES',P),translate_freetypes(Freetypes),mpend(P).
1858 translate_mpart2(meta,_Infos,_) --> [].
1859 translate_mpart2(operators,Operators,_) -->
1860 insertstr('\n/* Event-B operators:'), % */
1861 indention_level(I,I2), {I2 is I+2},
1862 translate_eventb_operators(Operators),
1863 indention_level(I2,I),
1864 insertstr('\n*/').
1865 translate_mpart2(values,Values,_) -->
1866 mpstart('VALUES',P),indent_expr_l_sep(Values,';'),mpend(P).
1867
1868 % Add typing predicates to a predicate
1869 mpart_typing(Title,Section,Sections,PredI) -->
1870 {mpart_typing2(Section,Sections,PredI,PredO)},
1871 ( {is_truth(PredO)} -> [] % TO DO: in animation_minor_mode(z) for INVARIANT: force adding typing predicates (translate_print_typing_infos)
1872 ; {otherwise} ->
1873 mpstart(Title,P),
1874 pred_over_lines(0,PredO),
1875 mpend(P)).
1876
1877 mpart_typing2(Sections,AllSections,PredI,PredO) :-
1878 get_preference(translate_print_typing_infos,true),!,
1879 get_all_ids(Sections,AllSections,Ids),
1880 add_typing_predicates(Ids,PredI,PredO).
1881 mpart_typing2(_Section,_Sections,Pred,Pred).
1882
1883 get_all_ids([],_Sections,[]).
1884 get_all_ids([Section|Srest],Sections,Ids) :-
1885 memberchk(Section/Ids1,Sections),
1886 append(Ids1,Ids2,Ids),
1887 get_all_ids(Srest,Sections,Ids2).
1888
1889 add_optional_typing_predicates(Ids,In,Out) :-
1890 ( get_preference(translate_print_typing_infos,true) -> add_typing_predicates(Ids,In,Out)
1891 ; is_truth(In) -> add_typing_predicates(Ids,In,Out)
1892 ; otherwise -> In=Out).
1893
1894 add_normal_typing_predicates(Ids,In,Out) :- % used to call add_typing_predicates directly
1895 (add_optional_typing_predicates(Ids,In,Out) -> true
1896 ; add_internal_error('Failed: ',add_normal_typing_predicates(Ids)), In=Out).
1897
1898 add_typing_predicates([],P,P) :- !.
1899 add_typing_predicates(Ids,Pin,Pout) :-
1900 remove_already_typed_ids(Pin,Ids,UntypedIds),
1901 generate_typing_predicates(UntypedIds,Typing),
1902 conjunction_to_list(Pin,Pins),
1903 remove_duplicate_predicates(Typing,Pins,Typing2),
1904 append(Typing2,[Pin],Preds),
1905 conjunct_predicates(Preds,Pout).
1906
1907 remove_already_typed_ids(_TExpr,Ids,Ids) :-
1908 get_preference(translate_force_all_typing_infos,true),!.
1909 remove_already_typed_ids(TExpr,Ids,UntypedIds) :-
1910 get_texpr_expr(TExpr,Expr),
1911 remove_already_typed_ids2(Expr,Ids,UntypedIds).
1912 remove_already_typed_ids2(conjunct(A,B),Ids,UntypedIds) :- !,
1913 remove_already_typed_ids(A,Ids,I1),
1914 remove_already_typed_ids(B,I1,UntypedIds).
1915 remove_already_typed_ids2(lazy_let_pred(_,_,A),Ids,UntypedIds) :- !,
1916 remove_already_typed_ids(A,Ids,UntypedIds). % TO DO: check for variable clases with lazy_let ids ???
1917 remove_already_typed_ids2(Expr,Ids,UntypedIds) :-
1918 is_typing_predicate(Expr,Id),
1919 create_texpr(identifier(Id),_,_,TId),
1920 select(TId,Ids,UntypedIds),!.
1921 remove_already_typed_ids2(_,Ids,Ids).
1922 is_typing_predicate(member(A,_),Id) :- get_texpr_id(A,Id).
1923 is_typing_predicate(subset(A,_),Id) :- get_texpr_id(A,Id).
1924 is_typing_predicate(subset_strict(A,_),Id) :- get_texpr_id(A,Id).
1925
1926 remove_duplicate_predicates([],_Old,[]).
1927 remove_duplicate_predicates([Pred|Prest],Old,Result) :-
1928 ( is_duplicate_predicate(Pred,Old) -> Result = Rest
1929 ; otherwise -> Result = [Pred|Rest]),
1930 remove_duplicate_predicates(Prest,Old,Rest).
1931 is_duplicate_predicate(Pred,List) :-
1932 remove_all_infos(Pred,Pattern),
1933 memberchk(Pattern,List).
1934
1935 generate_typing_predicates(TIds,Preds) :-
1936 maplist(generate_typing_predicate, TIds, Preds).
1937 generate_typing_predicate(TId,Pred) :-
1938 get_texpr_type(TId,Type),
1939 remove_all_infos_and_ground(TId,TId2), % clear all infos
1940 (type_set(Type,TSet) -> create_texpr(member(TId2,TSet),pred,[],Pred)
1941 ; add_error(generate_typing_predicate,'Illegal type: ',Type),
1942 is_truth(Pred)
1943 ).
1944
1945 % translate a ProB type to a typed expression representing the maximal type
1946 set_type_to_maximal_texpr(ProBType,TExpr) :- replace_seq(ProBType,MType),type_set(MType,TExpr).
1947
1948 % replace all occurences of seq/1 by couple(....)
1949 replace_seq(set(T),Res) :- !, Res=set(RT),replace_seq(T,RT).
1950 replace_seq(seq(T),Res) :- !, Res=set(couple(integer,RT)),replace_seq(T,RT).
1951 replace_seq(couple(A,B),Res) :- !, Res=couple(RA,RB),replace_seq(A,RA), replace_seq(B,RB).
1952 replace_seq(X,X).
1953
1954 % translate a ProB type into a B expression so that we can write x:TSet
1955 type_set(Type,TSet) :-
1956 ( var(Type) -> add_error_and_fail(translate,'type_set Type is variable: ',Type)
1957 ; otherwise ->
1958 type_set2(Type,Set,Infos),
1959 create_texpr(Set,set(Type),Infos,TSet)).
1960 type_set2(set(T),pow_subset(Set),[]) :-
1961 type_set(T,Set).
1962 type_set2(seq(T),seq(Set),[]) :- type_set(T,Set).
1963 type_set2(couple(TA,TB),cartesian_product(SetA,SetB),[]) :-
1964 type_set(TA,SetA), type_set(TB,SetB).
1965 %type_set2(global(G),identifier(G),[given_set]).
1966 type_set2(global(G),value(global_set(G)),[given_set]). % avoids variable capture/clash
1967 type_set2(integer,integer_set('INTEGER'),[]).
1968 type_set2(string,string_set,[]).
1969 type_set2(boolean,bool_set,[]).
1970 type_set2(record(TFields), struct(Rec),[]) :-
1971 create_texpr(rec(SFields),record(TFields),[],Rec),
1972 type_set_fields(TFields,SFields).
1973 %type_set2(freetype(Id),identifier(Id),[given_set]).
1974 type_set2(freetype(Id),freetype_set(Id),[]).
1975 type_set2(constant(L),value(Terms),[]) :- % these types occur in Event-B for Theory plugin inductive datatypes
1976 maplist(create_term,L,Terms).
1977 create_term(T,term(T)).
1978 type_set_fields([],[]).
1979 type_set_fields([field(Id,Type)|TFrest],[field(Id,TSet)|EFrest]) :-
1980 type_set(Type,TSet),
1981 type_set_fields(TFrest,EFrest).
1982
1983
1984 % translate enumerated constant list into enumerate set definition
1985 translate_enums([],Acc,Acc).
1986 translate_enums([EnumCst|T],Acc,Res) :- %get_texpr_id(EnumCst,Id),
1987 get_texpr_type(EnumCst,global(GlobalSet)),
1988 insert_enum_cst(Acc,EnumCst,GlobalSet,Acc2),
1989 translate_enums(T,Acc2,Res).
1990
1991 insert_enum_cst([],ID,Type,[enumerated_set_def(Type,[ID])]).
1992 insert_enum_cst([enumerated_set_def(Type,Lst)|T],ID,Type2,[enumerated_set_def(Type,Lst2)|TT]) :-
1993 (Type=Type2
1994 -> Lst2 = [ID|Lst], TT=T
1995 ; Lst2 = Lst, insert_enum_cst(T,ID,Type2,TT)
1996 ).
1997
1998 % pretty-print the initialisation section of a machine
1999 translate_inits(Inits) -->
2000 ( {is_list_simple(Inits)} ->
2001 translate_inits2(Inits)
2002 ; {otherwise} ->
2003 indention_level(I,I2),{I2 is I+2},
2004 translate_subst_begin_end(Inits),
2005 indention_level(_,I)).
2006 translate_inits2([]) --> !.
2007 translate_inits2([init(Name,Subst)|Rest]) -->
2008 indent('/* '),insertstr(Name),insertstr(': */ '),
2009 translate_subst_begin_end(Subst),
2010 translate_inits2(Rest).
2011
2012 % pretty-print the definitions of a machine
2013 translate_defs([]) --> !.
2014 translate_defs([Def|Rest]) --> translate_def(Def),translate_defs(Rest).
2015 translate_def(definition_decl(Name,DefType,_Pos,Args,Expr,_Deps)) -->
2016 {def_description(DefType,Desc)}, indent(Desc),insertstr(Name),
2017 {transform_raw_list(Args,TArgs)},
2018 translate_op_params(TArgs),
2019 ( {show_def_body(Expr)}
2020 -> insertstr(' == '), {transform_raw(Expr,TExpr)},
2021 (translate_def_body(DefType,TExpr) -> [] ; insertstr('CANNOT PRETTY PRINT'))
2022 ; {true}
2023 ),
2024 insertstr(';').
2025 def_description(substitution,'SUBSTITUTION ').
2026 def_description(expression,'EXPRESSION ').
2027 def_description(predicate,'PREDICATE ').
2028 translate_def_body(substitution,B) --> translate_subst_begin_end(B).
2029 translate_def_body(expression,B) --> indent_expr(B).
2030 translate_def_body(predicate,B) --> indent_expr(B).
2031
2032 show_def_body(integer(_,_)).
2033 show_def_body(boolean_true(_)).
2034 show_def_body(boolean_false(_)).
2035 % show_def_body(_) % comment in to pretty print all defs
2036
2037 % ------------- RAW EXPRESSIONS
2038
2039 % try and print raw machine term or parts thereof (e.g. sections)
2040 print_raw_machine_terms(Var) :- var(Var), !,print('VAR !!'),nl.
2041 print_raw_machine_terms([]) :- !.
2042 print_raw_machine_terms([H|T]) :- !,
2043 print_raw_machine_terms(H), print(' '),
2044 print_raw_machine_terms(T).
2045 print_raw_machine_terms(Term) :- raw_machine_term(Term,String,Sub),!,
2046 format('~n~w ',[String]),
2047 print_raw_machine_terms(Sub),nl.
2048 print_raw_machine_terms(expression_definition(A,B,C,D)) :- !,
2049 print_raw_machine_terms(predicate_definition(A,B,C,D)).
2050 print_raw_machine_terms(substitution_definition(A,B,C,D)) :- !,
2051 print_raw_machine_terms(predicate_definition(A,B,C,D)).
2052 print_raw_machine_terms(predicate_definition(_,Name,Paras,RHS)) :-
2053 Paras==[],!,
2054 format('~n ~w == ',[Name]),
2055 print_raw_machine_terms(RHS),nl.
2056 print_raw_machine_terms(predicate_definition(_,Name,Paras,RHS)) :- !,
2057 format('~n ~w(',[Name]),
2058 print_raw_machine_terms_sep(Paras,','),
2059 format(') == ',[]),
2060 print_raw_machine_terms(RHS),nl.
2061 print_raw_machine_terms(operation(_,Name,Return,Paras,RHS)) :- !,
2062 format('~n ',[]),
2063 (Return=[] -> true
2064 ; print_raw_machine_terms_sep(Return,','),
2065 format(' <-- ',[])
2066 ),
2067 print_raw_machine_terms(Name),
2068 (Paras=[] -> true
2069 ; format(' (',[]),
2070 print_raw_machine_terms_sep(Paras,','),
2071 format(')',[])
2072 ),
2073 format(' = ',[]),
2074 print_raw_machine_terms(RHS),nl.
2075 print_raw_machine_terms(Term) :- print_raw_bexpr(Term).
2076
2077
2078 print_raw_machine_terms_sep([],_) :- !.
2079 print_raw_machine_terms_sep([H],_) :- !,
2080 print_raw_machine_terms(H).
2081 print_raw_machine_terms_sep([H|T],Sep) :- !,
2082 print_raw_machine_terms(H),print(Sep),print_raw_machine_terms_sep(T,Sep).
2083
2084 raw_machine_term(machine(M),'',M).
2085 raw_machine_term(generated(_,M),'',M).
2086 raw_machine_term(machine_header(_,Name,_Params),Name,[]). % TO DO: treat Params
2087 raw_machine_term(abstract_machine(_,_,Header,M),'MACHINE',[Header,M]).
2088 raw_machine_term(properties(_,P),'PROPERTIES',P).
2089 raw_machine_term(operations(_,P),'OPERATIONS',P).
2090 raw_machine_term(definitions(_,P),'DEFINITIONS',P).
2091 raw_machine_term(constants(_,P),'CONSTANTS',P).
2092 raw_machine_term(variables(_,P),'VARIABLES',P).
2093 raw_machine_term(invariant(_,P),'INVARIANT',P).
2094 raw_machine_term(assertions(_,P),'ASSERTIONS',P).
2095 raw_machine_term(constraints(_,P),'CONSTRAINTS',P).
2096 raw_machine_term(sets(_,P),'SETS',P).
2097 raw_machine_term(deferred_set(_,P),P,[]). % TO DO: enumerated_set ...
2098 %raw_machine_term(identifier(_,P),P,[]).
2099
2100 print_raw_bexpr(Raw) :- % a tool (not perfect) to print raw ASTs
2101 transform_raw(Raw,TExpr), print_bexpr_or_subst(TExpr).
2102
2103 transform_raw_list(Var,Res) :- var(Var),!,
2104 add_internal_error('Var raw expression list:',transform_raw_list(Var,Res)),
2105 Res= [b(identifier('$$VARIABLE_LIST$$'),any,[raw])].
2106 transform_raw_list(Args,TArgs) :- maplist(transform_raw,Args,TArgs).
2107
2108 transform_raw(Var,Res) :- %print(raw(Var)),nl,
2109 var(Var), !, add_internal_error('Var raw expression:',transform_raw(Var,Res)),
2110 Res= b(identifier('$$VARIABLE$$'),any,[raw]).
2111 transform_raw(precondition(_,Pre,Body),Res) :- !, Res= b(precondition(TP,TB),subst,[raw]),
2112 transform_raw(Pre,TP),
2113 transform_raw(Body,TB).
2114 transform_raw(identifier(_,M),Res) :- !, Res= b(identifier(M),any,[raw]).
2115 transform_raw(integer(_,M),Res) :- !, Res= b(integer(M),integer,[raw]).
2116 transform_raw(let_expression(_,_Ids,Eq,Body),Res) :- !,
2117 transform_raw(conjunct(_,Eq,Body),Res). % TO DO: fix and generate let_expression(Ids,ListofExprs,Body)
2118 transform_raw(let_predicate(_,_Ids,Eq,Body),Res) :- !,
2119 transform_raw(conjunct(_,Eq,Body),Res). % ditto
2120 transform_raw(forall(_,Ids,Body),Res) :- !,
2121 (Body=implication(_,LHS,RHS) -> true ; LHS=truth,RHS=Body),
2122 transform_raw(forall(_,Ids,LHS,RHS),Res).
2123 transform_raw(record_field(_,Rec,identifier(_,Field)),Res) :- !, Res = b(record_field(TRec,Field),any,[]),
2124 transform_raw(Rec,TRec).
2125 transform_raw(rec_entry(_,identifier(_,Field),Rec),Res) :- !, Res = field(Field,TRec),
2126 transform_raw(Rec,TRec).
2127 transform_raw(couple(_,L),Res) :- !, transform_raw_list_to_couple(L,Res). % couples are represented by lists
2128 transform_raw(function(_,F,L),Res) :- !, transform_raw(F,TF),
2129 Res = b(function(TF,Args),any,[]),
2130 transform_raw_list_to_couple(L,Args). % args are represented by lists
2131 transform_raw(Atom,Res) :- atomic(Atom),!,Res=Atom.
2132 transform_raw([H|T],Res) :- !, maplist(transform_raw,[H|T],Res).
2133 transform_raw(OtherOp,b(Res,Type,[used_ids([])])) :- OtherOp =..[F,_Pos|Rest],
2134 maplist(transform_raw,Rest,TRest),
2135 (get_type(F,FT) -> Type=FT ; Type=any),
2136 Res =.. [F|TRest].
2137 transform_raw_list_to_couple([R],Res) :- !, transform_raw(R,Res).
2138 transform_raw_list_to_couple([R1|T],Res) :- !, Res=b(couple(TR1,TT),any,[]),
2139 transform_raw(R1,TR1),transform_raw_list_to_couple(T,TT).
2140 get_type(conjunct,pred).
2141 get_type(disjunct,pred).
2142 get_type(implication,pred).
2143 get_type(equivalence,pred).
2144 get_type(member,pred).
2145 get_type(equal,pred).
2146 get_type(not_equal,pred).
2147 get_type(not_member,pred).
2148 get_type(subset,pred).
2149 get_type(not_subset,pred).
2150
2151 % -------------
2152
2153
2154 % pretty-print the operations of a machine
2155 translate_ops([]) --> !.
2156 translate_ops([Op|Rest]) -->
2157 translate_op(Op),
2158 ({Rest=[]} -> {true}; insertstr(';'),indent),
2159 translate_ops(Rest).
2160 translate_op(Op) -->
2161 { get_texpr_expr(Op,operation(Id,Res,Params,Body)) },
2162 translate_operation(Id,Res,Params,Body).
2163 translate_operation(Id,Res,Params,Body) -->
2164 indent,translate_op_results(Res),
2165 pp_expr_indent(Id),
2166 translate_op_params(Params),
2167 insertstr(' = '),
2168 indention_level(I1,I2),{I2 is I1+2,type_infos_in_subst(Params,Body,Body2)},
2169 translate_subst_begin_end(Body2),
2170 indention_level(_,I1).
2171 translate_op_results([]) --> !.
2172 translate_op_results(Ids) --> pp_expr_indent_l(Ids), insertstr(' <-- ').
2173 translate_op_params([]) --> !.
2174 translate_op_params(Ids) --> insertstr('('),pp_expr_indent_l(Ids), insertstr(')').
2175
2176 translate_subst_begin_end(TSubst) -->
2177 {get_texpr_expr(TSubst,Subst),subst_needs_begin_end(Subst),
2178 create_texpr(block(TSubst),subst,[],Block)},!,
2179 translate_subst(Block).
2180 translate_subst_begin_end(Subst) -->
2181 translate_subst(Subst).
2182
2183 subst_needs_begin_end(assign(_,_)).
2184 subst_needs_begin_end(assign_single_id(_,_)).
2185 subst_needs_begin_end(parallel(_)).
2186 subst_needs_begin_end(sequence(_)).
2187 subst_needs_begin_end(operation_call(_,_,_)).
2188
2189 type_infos_in_subst([],Subst,Subst) :- !.
2190 type_infos_in_subst(Ids,SubstIn,SubstOut) :-
2191 get_preference(translate_print_typing_infos,true),!,
2192 type_infos_in_subst2(Ids,SubstIn,SubstOut).
2193 type_infos_in_subst(_Ids,Subst,Subst).
2194 type_infos_in_subst2(Ids,SubstIn,SubstOut) :-
2195 get_texpr_expr(SubstIn,precondition(P1,S)),!,
2196 get_texpr_info(SubstIn,Info),
2197 create_texpr(precondition(P2,S),pred,Info,SubstOut),
2198 add_typing_predicates(Ids,P1,P2).
2199 type_infos_in_subst2(Ids,SubstIn,SubstOut) :-
2200 create_texpr(precondition(P,SubstIn),pred,[],SubstOut),
2201 generate_typing_predicates(Ids,Typing),
2202 conjunct_predicates(Typing,P).
2203
2204
2205
2206
2207
2208 % pretty-print the internal section about included and used machines
2209 translate_used([]) --> !.
2210 translate_used([Used|Rest]) -->
2211 translate_used2(Used),
2212 translate_used(Rest).
2213 translate_used2(includeduse(Name,Id,NewTExpr)) -->
2214 indent,pp_expr_indent(NewTExpr),
2215 insertstr(' --> '), insertstr(Name), insertstr(':'), insertstr(Id).
2216
2217 % pretty-print the internal information about freetypes
2218 translate_freetypes([]) --> !.
2219 translate_freetypes([Freetype|Frest]) -->
2220 translate_freetype(Freetype),
2221 translate_freetypes(Frest).
2222 translate_freetype(freetype(Name,Cases)) -->
2223 {pretty_freetype(Name,PName)},
2224 indent(PName),insertstr(': '),
2225 indention_level(I1,I2),{I2 is I1+2},
2226 translate_freetype_cases(Cases),
2227 indention_level(_,I1).
2228 translate_freetype_cases([]) --> !.
2229 translate_freetype_cases([case(Name,constant(_))|Rest]) -->
2230 !,indent(Name),translate_freetype_cases(Rest).
2231 translate_freetype_cases([case(Name,Type)|Rest]) -->
2232 {pretty_type(Type,PT)},
2233 indent(Name),
2234 insertstr('('),insertstr(PT),insertstr(')'),
2235 translate_freetype_cases(Rest).
2236
2237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2238 % substitutions
2239
2240 translate_subst_or_bexpr(Stmt,String) :- get_texpr_type(Stmt,subst),!,
2241 translate_substitution(Stmt,String).
2242 translate_subst_or_bexpr(ExprOrPred,String) :-
2243 translate_bexpression(ExprOrPred,String).
2244
2245 translate_subst_or_bexpr_with_limit(Stmt,Limit,String) :-
2246 translate_subst_or_bexpr_with_limit(Stmt,Limit,report_errors,String).
2247 translate_subst_or_bexpr_with_limit(Stmt,_Limit,ReportErrors,String) :- get_texpr_type(Stmt,subst),!,
2248 translate_substitution(Stmt,String,ReportErrors). % TO DO: use limit
2249 translate_subst_or_bexpr_with_limit(ExprOrPred,Limit,ReportErrors,String) :-
2250 translate_bexpression_with_limit(ExprOrPred,Limit,ReportErrors,String).
2251
2252 print_subst(Stmt) :- translate_substitution(Stmt,T), print(T).
2253 translate_substitution(Stmt,String) :- translate_substitution(Stmt,String,report_errors).
2254 translate_substitution(Stmt,String,_) :- translate_subst_with_indention(Stmt,0,Codes,[]),
2255 (Codes = [10|C] -> true ; Codes=[13|C] -> true ; Codes=C), % peel off leading newline
2256 atom_codes_with_limit(String, C),!.
2257 translate_substitution(Stmt,String,report_errors) :-
2258 add_error(translate_substitution,'Could not translate substitution: ',Stmt),String='???'.
2259
2260 translate_subst_with_indention(TS,Indention,I,O) :-
2261 translate_subst(TS,(Indention,I),(_,O)).
2262
2263 translate_subst(TS) -->
2264 ( {get_texpr_expr(TS,S)} ->
2265 %indent_rodin_label(TS), % comment in to pretty print substitution labels
2266 translate_subst2(S)
2267 ; {otherwise} -> translate_subst2(TS)).
2268
2269 % will print (first) rodin or pragma label indendent
2270 :- public indent_rodin_label/3.
2271 indent_rodin_label(_TExpr) --> {get_preference(translate_suppress_rodin_positions_flag,true),!}.
2272 indent_rodin_label(_TExpr) --> {get_preference(bugly_pp_scrambling,true),!}.
2273 indent_rodin_label(TExpr) --> {bsyntaxtree:get_texpr_labels(TExpr,Names)},!, % note: this will only get the first label
2274 indent('/* @'),pp_ids_indent(Names),insertstr('*/ '). % this syntax cannot be read back in
2275 indent_rodin_label(_TExpr) --> [].
2276
2277 pp_ids_indent([]) --> !, [].
2278 pp_ids_indent([ID|T]) --> !,pp_expr_indent(identifier(ID)), insertstr(' '),pp_ids_indent(T).
2279 pp_ids_indent(X) --> {add_error(pp_ids_indent,'Not a list of atoms: ',pp_ids_indent(X))}.
2280
2281 translate_subst2(skip) -->
2282 indent(skip).
2283 translate_subst2(operation(Id,Res,Params,Body)) --> translate_operation(Id,Res,Params,Body). % not really a substition that can appear normally
2284 translate_subst2(precondition(P,S)) -->
2285 indent('PRE '), pred_over_lines(2,P), indent('THEN'), insert_subst(S), indent('END').
2286 translate_subst2(assertion(P,S)) -->
2287 indent('ASSERT '), pp_expr_indent(P), indent('THEN'), insert_subst(S), indent('END').
2288 translate_subst2(block(S)) -->
2289 indent('BEGIN'), insert_subst(S), indent('END').
2290 translate_subst2(assign(L,R)) -->
2291 indent,pp_expr_indent_l(L),insertstr(' := '),pp_expr_indent_l(R).
2292 translate_subst2(assign_single_id(L,R)) -->
2293 translate_subst2(assign([L],[R])).
2294 translate_subst2(becomes_element_of(L,R)) -->
2295 indent,pp_expr_indent_l(L),insertstr(' :: '),pp_expr_indent(R).
2296 translate_subst2(becomes_such(L,R)) -->
2297 indent,pp_expr_indent_l(L),insertstr(' : '), insertstr('('),
2298 { add_optional_typing_predicates(L,R,R1) },
2299 pp_expr_indent(R1), insertstr(')').
2300 translate_subst2(evb2_becomes_such(L,R)) --> translate_subst2(becomes_such(L,R)).
2301 translate_subst2(if([Elsif|Rest])) -->
2302 { get_if_elsif(Elsif,P,S) },
2303 indent('IF '), pp_expr_indent(P), insertstr(' THEN'),
2304 insert_subst(S),
2305 translate_ifs(Rest).
2306 translate_subst2(choice(Ss)) --> indent(' CHOICE'),
2307 split_over_lines(Ss,'OR'),
2308 indent('END'). % indentation seems too far
2309 translate_subst2(parallel(Ss)) -->
2310 split_over_lines(Ss,'||').
2311 translate_subst2(init_statement(S)) --> insert_subst(S).
2312 translate_subst2(sequence(Ss)) -->
2313 split_over_lines(Ss,';').
2314 translate_subst2(operation_call(Id,Rs,As)) -->
2315 indent,translate_op_results(Rs),
2316 pp_expr_indent(Id),
2317 translate_op_params(As).
2318 translate_subst2(external_subst_call(Symbol,Args)) -->
2319 indent,
2320 pp_expr_indent(identifier(Symbol)),
2321 translate_op_params(Args).
2322 translate_subst2(any(Ids,Pred,Subst)) -->
2323 indent('ANY '), pp_expr_indent_l(Ids),
2324 indent('WHERE '),
2325 {add_optional_typing_predicates(Ids,Pred,Pred2)},
2326 pred_over_lines(2,Pred2), indent('THEN'),
2327 insert_subst(Subst),
2328 indent('END').
2329 translate_subst2(select(Whens)) -->
2330 translate_whens(Whens,'SELECT '),
2331 indent('END').
2332 translate_subst2(select(Whens,Else)) -->
2333 translate_whens(Whens,'SELECT '),
2334 indent('ELSE'), insert_subst(Else),
2335 indent('END').
2336 translate_subst2(var(Ids,S)) -->
2337 indent('VAR '),
2338 pp_expr_indent_l(Ids),
2339 indent('IN'),insert_subst(S),
2340 indent('END').
2341 translate_subst2(let(Ids,P,S)) -->
2342 indent('LET '),
2343 pp_expr_indent_l(Ids),
2344 insertstr(' BE '), pp_expr_indent(P),
2345 indent('IN'), insert_subst(S),
2346 indent('END').
2347 translate_subst2(lazy_let_subst(TID,P,S)) -->
2348 indent('LET '),
2349 pp_expr_indent_l([TID]),
2350 insertstr(' BE '), pp_expr_indent(P), % could be expr or pred
2351 indent('IN'), insert_subst(S),
2352 indent('END').
2353 translate_subst2(case(Expression,Cases,ELSE)) -->
2354 % CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END
2355 indent('CASE '),
2356 pp_expr_indent(Expression), insertstr(' OF'),
2357 indent('EITHER '), translate_cases(Cases),
2358 indent('ELSE '), insert_subst(ELSE), % we could drop this if ELSE is skip ?
2359 indent('END END').
2360 translate_subst2(while(Pred,Subst,Inv,Var)) -->
2361 indent('WHILE '), pp_expr_indent(Pred),
2362 indent('DO'),insert_subst(Subst),
2363 indent('INVARIANT '),pp_expr_indent(Inv),
2364 indent('VARIANT '),pp_expr_indent(Var),
2365 indent('END').
2366 translate_subst2(while1(Pred,Subst,Inv,Var)) -->
2367 indent('WHILE /* 1 */ '), pp_expr_indent(Pred),
2368 indent('DO'),insert_subst(Subst),
2369 indent('INVARIANT '),pp_expr_indent(Inv),
2370 indent('VARIANT '),pp_expr_indent(Var),
2371 indent('END').
2372 translate_subst2(rlevent(Id,Section,Status,Parameters,Guard,Theorems,Actions,VWitnesses,PWitnesses,_Unmod,Refines)) -->
2373 indent,
2374 insert_status(Status),
2375 insertstr('EVENT '), insertstr(Id), insertstr(' = /'), insertstr('* of machine '),
2376 insertstr(Section),insertstr(' */'),
2377 insert_variant(Status),
2378 ( {Parameters=[], get_texpr_expr(Guard,truth)} ->
2379 {true} % indent('BEGIN ')
2380 ; {Parameters=[]} ->
2381 indent('WHEN '),
2382 pred_over_lines(2,Guard)
2383 ; {otherwise} ->
2384 indent('ANY '),pp_expr_indent_l(Parameters),
2385 indent('WHERE '),
2386 pred_over_lines(2,Guard) ),
2387 ( {VWitnesses=[],PWitnesses=[]} ->
2388 []
2389 ; {otherwise} ->
2390 {append(VWitnesses,PWitnesses,Witnesses)},
2391 indent('WITH '),pp_witness_l(Witnesses) ),
2392 {( Actions=[] ->
2393 create_texpr(skip,subst,[],Subst)
2394 ; otherwise ->
2395 create_texpr(parallel(Actions),subst,[],Subst))},
2396 ( {Theorems=[]} -> {true}
2397 ; {otherwise} ->
2398 indent('THEOREMS '),
2399 preds_over_lines(2,Theorems)),
2400 indent('THEN '), insert_subst(Subst),
2401 pp_refines_l(Refines,Id),
2402 indent('END').
2403
2404 % translate cases of a CASE statement
2405 translate_cases([]) --> !,[].
2406 translate_cases([CaseOr|T]) -->
2407 {get_texpr_expr(CaseOr,case_or(Exprs,Subst))},!,
2408 pp_expr_indent_l(Exprs),
2409 insertstr(' THEN '),
2410 insert_subst(Subst),
2411 ({T==[]} -> {true}
2412 ; indent('OR '), translate_cases(T)).
2413 translate_cases(L) -->
2414 {add_internal_error('Cannot translate CASE list: ',translate_cases(L,_,_))}.
2415
2416 insert_status(TStatus) -->
2417 {get_texpr_expr(TStatus,Status),
2418 status_string(Status,String)},
2419 insertstr(String).
2420 status_string(ordinary,'').
2421 status_string(anticipated(_),'ANTICIPATED ').
2422 status_string(convergent(_),'CONVERGENT ').
2423
2424 insert_variant(TStatus) -->
2425 {get_texpr_expr(TStatus,Status)},
2426 insert_variant2(Status).
2427 insert_variant2(ordinary) --> !.
2428 insert_variant2(anticipated(Variant)) --> insert_variant3(Variant).
2429 insert_variant2(convergent(Variant)) --> insert_variant3(Variant).
2430 insert_variant3(Variant) -->
2431 indent('USING VARIANT '),pp_expr_indent(Variant).
2432
2433 pp_refines_l([],_) --> [].
2434 pp_refines_l([Ref|Rest],Id) -->
2435 pp_refines(Ref,Id),pp_refines_l(Rest,Id).
2436 pp_refines(Refined,_Id) -->
2437 % indent(Id), insertstr(' REFINES '),
2438 indent('REFINES '),
2439 insert_subst(Refined).
2440
2441 pp_witness_l([]) --> [].
2442 pp_witness_l([Witness|WRest]) -->
2443 pp_witness(Witness),pp_witness_l(WRest).
2444 pp_witness(Expr) -->
2445 indention_level(I1,I2),
2446 {get_texpr_expr(Expr,witness(Id,Pred)),
2447 I2 is I1+2},
2448 indent, pp_expr_indent(Id), insertstr(': '),
2449 pp_expr_indent(Pred),
2450 indention_level(_,I1).
2451
2452
2453 translate_whens([],_) --> !.
2454 translate_whens([When|Rest],T) -->
2455 {get_texpr_expr(When,select_when(P,S))},!,
2456 indent(T), pred_over_lines(2,P),
2457 indent('THEN '),
2458 insert_subst(S),
2459 translate_whens(Rest,'WHEN ').
2460 translate_whens(L,_) -->
2461 {add_internal_error('Cannot translate WHEN: ',translate_whens(L,_,_,_))}.
2462
2463 split_over_lines([],_) --> !.
2464 split_over_lines([S|Rest],Symbol) --> !,
2465 indention_level(I1,I2),{atom_codes(Symbol,X),length(X,N),I2 is I1+N+1},
2466 translate_subst_check(S),
2467 split_over_lines2(Rest,Symbol,I1,I2).
2468 split_over_lines(S,Symbol) --> {add_error(split_over_lines,'Illegal argument: ',Symbol:S)}.
2469
2470 split_over_lines2([],_,_,_) --> !.
2471 split_over_lines2([S|Rest],Symbol,I1,I2) -->
2472 indention_level(_,I1), indent(Symbol),
2473 indention_level(_,I2), translate_subst(S),
2474 split_over_lines2(Rest,Symbol,I1,I2).
2475
2476 pred_over_lines(N,Pred) -->
2477 {conjunction_to_list(Pred,List)},
2478 preds_over_lines(N,List).
2479 preds_over_lines(N,Preds) -->
2480 indention_level(I1,I2),{I2 is I1+N},
2481 preds_over_lines1(Preds),
2482 indention_level(_,I1).
2483 preds_over_lines1([]) --> !, preds_over_lines1([b(truth,pred,[])]).
2484 preds_over_lines1([H|T]) -->
2485 indent(' '), ({T==[]} -> pp_expr_indent(H) ; pp_expr_m_indent(H,40)),
2486 preds_over_lines2(T).
2487 preds_over_lines2([]) --> !.
2488 preds_over_lines2([E|Rest]) -->
2489 indent('& '),
2490 pp_expr_m_indent(E,40),
2491 preds_over_lines2(Rest).
2492
2493 translate_ifs([]) --> !,
2494 indent('END').
2495 translate_ifs([Elsif]) -->
2496 {get_if_elsif(Elsif,P,S),
2497 optional_type(P,truth)},!,
2498 indent('ELSE'), insert_subst(S), indent('END').
2499 translate_ifs([Elsif|Rest]) -->
2500 {get_if_elsif(Elsif,P,S)},!,
2501 indent('ELSIF '), pp_expr_indent(P), insertstr(' THEN'),
2502 insert_subst(S),
2503 translate_ifs(Rest).
2504 translate_ifs(ElseList) -->
2505 {functor(ElseList,F,A),add_error(translate_ifs,'Could not translate IF-THEN-ELSE: ',F/A-ElseList),fail}.
2506
2507 get_if_elsif(Elsif,P,S) :-
2508 (optional_type(Elsif,if_elsif(P,S)) -> true
2509 ; add_internal_error('Is not an if_elsif:',get_if_elsif(Elsif,P,S)), fail).
2510
2511 insert_subst(S) -->
2512 indention_level(I,I2),{I2 is I+2},
2513 translate_subst_check(S),
2514 indention_level(_,I).
2515
2516 translate_subst_check(S) --> translate_subst(S),!.
2517 translate_subst_check(S) -->
2518 {b_functor(S,F,A),add_error(translate_subst,'Could not translate substitution: ',F/A-S),fail}.
2519
2520 b_functor(b(E,_,_),F,A) :- !,functor(E,F,A).
2521 b_functor(E,F,A) :- functor(E,F,A).
2522
2523 indent_expr(Expr) -->
2524 indent, pp_expr_indent(Expr).
2525 %indent_expr_l([]) --> !.
2526 %indent_expr_l([Expr|Rest]) -->
2527 % indent_expr(Expr), indent_expr_l(Rest).
2528 indent_expr_l_sep([],_) --> !.
2529 indent_expr_l_sep([Expr|Rest],Sep) -->
2530 indent_expr(Expr),
2531 {(Rest=[] -> RealSep='' ; RealSep=Sep)},
2532 insert_atom(RealSep), % the threaded argument is a pair, not directly a string !
2533 indent_expr_l_sep(Rest,Sep).
2534 %indention_level(L) --> indention_level(L,L).
2535 indention_level(Old,New,(Old,S),(New,S)).
2536 indention_codes(Old,New,(Indent,Old),(Indent,New)).
2537 indent --> indent('').
2538 indent(M,(I,S),(I,T)) :- indent2(I,M,S,T).
2539 indent2(Level,Msg) -->
2540 "\n",do_indention(Level),ppatom(Msg).
2541
2542 insert_atom(Sep,(I,S),(I,T)) :- ppatom(Sep,S,T).
2543
2544 insertstr(M,(I,S),(I,T)) :- ppterm(M,S,T).
2545 insertcodes(M,(I,S),(I,T)) :- ppcodes(M,S,T).
2546
2547 do_indention(0,T,R) :- !, R=T.
2548 do_indention(N,[32|I],O) :-
2549 N>0,N2 is N-1, do_indention(N2,I,O).
2550
2551 optional_type(Typed,Expr) :- get_texpr_expr(Typed,E),!,Expr=E.
2552 optional_type(Expr,Expr).
2553
2554 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2555 % expressions and predicates
2556
2557 % pretty-type an expression in an indent-environment
2558 % currently, the indent level is just thrown away
2559 pp_expr_indent(Expr,(I,S),(I,T)) :-
2560 pp_expr(Expr,_,_LimitReached,S,T).
2561 pp_expr_indent_l(Exprs,(I,S),(I,T)) :-
2562 pp_expr_l(Exprs,_LR,S,T).
2563 pp_expr_m_indent(Expr,MinPrio,(I,S),(I,T)) :-
2564 pp_expr_m(Expr,MinPrio,_LimitReached,S,T).
2565
2566
2567 is_boolean_value(b(B,boolean,_),BV) :- boolean_aux(B,BV).
2568 boolean_aux(boolean_true,pred_true).
2569 boolean_aux(boolean_false,pred_false).
2570 boolean_aux(value(V),BV) :- nonvar(V),!,BV=V.
2571
2572
2573 constants_in_mode(F,S) :-
2574 constants(F,S1), translate_in_mode(F,S1,S).
2575
2576 constants(pred_true,'TRUE').
2577 constants(pred_false,'FALSE').
2578 constants(boolean_true,'TRUE').
2579 constants(boolean_false,'FALSE').
2580 constants(max_int,'MAXINT').
2581 constants(min_int,'MININT').
2582 constants(empty_set,'{}').
2583 constants(bool_set,'BOOL').
2584 constants(string_set,'STRING').
2585 constants(empty_sequence,'[]').
2586 constants(event_b_identity,'id').
2587
2588 constants(truth,Res) :- animation_minor_mode(eventb),!,Res=true.
2589 constants(truth,Res) :- animation_minor_mode(tla),!,Res='TRUE'.
2590 constants(truth,'(TRUE:BOOL)'). % __truth; we could also do TRUE=TRUE
2591 constants(falsity,Res) :- animation_minor_mode(eventb),!,Res=false.
2592 constants(falsity,Res) :- animation_minor_mode(tla),!,Res='FALSE'.
2593 constants(falsity,'(TRUE=FALSE)'). % __falsity
2594
2595 function_like_in_mode(F,S) :-
2596 function_like(F,S1),
2597 translate_in_mode(F,S1,S).
2598
2599 function_like(convert_bool,bool).
2600 function_like(successor,succ).
2601 function_like(predecessor,pred).
2602 function_like(max,max).
2603 function_like(min,min).
2604 function_like(card,card).
2605 function_like(pow_subset,'POW').
2606 function_like(pow1_subset,'POW1').
2607 function_like(fin_subset,'FIN').
2608 function_like(fin1_subset,'FIN1').
2609 function_like(identity,id).
2610 function_like(first_projection,prj1).
2611 function_like(first_of_pair,'__first_of_pair'). % will be dealt with separately to generate parsable representation
2612 function_like(second_projection,prj2).
2613 function_like(second_of_pair,'__second_of_pair'). % will be dealt with separately to generate parsable representation
2614 function_like(iteration,iterate).
2615 function_like(reflexive_closure,closure).
2616 function_like(closure,closure1).
2617 function_like(domain,dom).
2618 function_like(range,ran).
2619 function_like(seq,seq).
2620 function_like(seq1,seq1).
2621 function_like(iseq,iseq).
2622 function_like(iseq1,iseq1).
2623 function_like(perm,perm).
2624 function_like(size,size).
2625 function_like(first,first).
2626 function_like(last,last).
2627 function_like(front,front).
2628 function_like(tail,tail).
2629 function_like(rev,rev).
2630 function_like(general_concat,conc).
2631 function_like(general_union,union).
2632 function_like(general_intersection,inter).
2633 function_like(trans_function,fnc).
2634 function_like(trans_relation,rel).
2635 function_like(tree,tree).
2636 function_like(btree,btree).
2637 function_like(const,const).
2638 function_like(top,top).
2639 function_like(sons,sons).
2640 function_like(prefix,prefix).
2641 function_like(postfix,postfix).
2642 function_like(sizet,sizet).
2643 function_like(mirror,mirror).
2644 function_like(rank,rank).
2645 function_like(father,father).
2646 function_like(son,son).
2647 function_like(subtree,subtree).
2648 function_like(arity,arity).
2649 function_like(bin,bin).
2650 function_like(left,left).
2651 function_like(right,right).
2652 function_like(infix,infix).
2653
2654 function_like(rec,rec).
2655 function_like(struct,struct).
2656
2657 function_like(negation,not).
2658 function_like(bag_items,items).
2659
2660 function_like(finite,finite). % from Event-B, TO DO: if \+ animation_minor_mode(eventb) then print as S:FIN(S)
2661
2662 unary_prefix(unary_minus,-,210).
2663 unary_prefix(mu,'MU',210) :- animation_minor_mode(z).
2664
2665 unary_prefix_parentheses(compaction,'compaction').
2666 unary_prefix_parentheses(bag_items,'bag_items').
2667 unary_prefix_parentheses(mu,'MU') :- \+ animation_minor_mode(z). % write with () for external function
2668
2669 unary_postfix(reverse,'~',230). % relational inverse
2670
2671
2672 always_surround_by_parentheses(parallel_product).
2673 always_surround_by_parentheses(composition).
2674
2675 binary_infix_symbol(b(T,_,_),Symbol) :- functor(T,F,2), binary_infix_in_mode(F,Symbol,_,_).
2676
2677 % EXPR * EXPR --> EXPR
2678 binary_infix(composition,';',20,left).
2679 binary_infix(overwrite,'<+',160,left).
2680 binary_infix(direct_product,'><',160,left).
2681 binary_infix(parallel_product,'||',20,left).
2682 binary_infix(concat,'^',160,left).
2683 binary_infix(relations,'<->',125,left).
2684 binary_infix(partial_function,'+->',125,left).
2685 binary_infix(total_function,'-->',125,left).
2686 binary_infix(partial_injection,'>+>',125,left).
2687 binary_infix(total_injection,'>->',125,left).
2688 binary_infix(partial_surjection,'+->>',125,left).
2689 binary_infix(total_surjection,Symbol,125,left) :-
2690 (animation_minor_mode(eventb) -> Symbol = '->>'; Symbol = '-->>').
2691 binary_infix(total_bijection,'>->>',125,left).
2692 binary_infix(partial_bijection,'>+>>',125,left).
2693 binary_infix(total_relation,'<<->',125,left). % only in Event-B
2694 binary_infix(surjection_relation,'<->>',125,left). % only in Event-B
2695 binary_infix(total_surjection_relation,'<<->>',125,left). % only in Event-B
2696 binary_infix(insert_front,'->',160,left).
2697 binary_infix(insert_tail,'<-',160,left).
2698 binary_infix(domain_restriction,'<|',160,left).
2699 binary_infix(domain_subtraction,'<<|',160,left).
2700 binary_infix(range_restriction,'|>',160,left).
2701 binary_infix(range_subtraction,'|>>',160,left).
2702 binary_infix(intersection,'/\\',160,left).
2703 binary_infix(union,'\\/',160,left).
2704 binary_infix(restrict_front,'/|\\',160,left).
2705 binary_infix(restrict_tail,'\\|/',160,left).
2706 binary_infix(couple,'|->',160,left).
2707 binary_infix(interval,'..',170,left).
2708 binary_infix(add,+,180,left).
2709 binary_infix(minus,-,180,left).
2710 binary_infix(set_subtraction,'\\',180,left) :- animation_minor_mode(eventb),!.
2711 binary_infix(set_subtraction,-,180,left).
2712 binary_infix(minus_or_set_subtract,-,180,left).
2713 binary_infix(multiplication,*,190,left).
2714 binary_infix(cartesian_product,**,190,left) :- animation_minor_mode(eventb),!.
2715 binary_infix(cartesian_product,*,190,left).
2716 binary_infix(mult_or_cart,*,190,left). % in case type checker not yet run
2717 binary_infix(div,/,190,left).
2718 binary_infix(floored_div,div,190,left).
2719 binary_infix(modulo,mod,190,left).
2720 binary_infix(power_of,**,200,right).
2721
2722
2723 % PRED * PRED --> PRED
2724 binary_infix(implication,'=>',30,left).
2725 binary_infix(conjunct,'&',40,left).
2726 binary_infix(disjunct,or,40,left).
2727 binary_infix(equivalence,'<=>',60,left).
2728
2729
2730 % EXPR * EXPR --> PRED
2731 binary_infix(equal,=,60,left).
2732 binary_infix(not_equal,'/=',160,left).
2733 binary_infix(less_equal,'<=',160,left).
2734 binary_infix(less,'<',160,left).
2735 binary_infix(greater_equal,'>=',160,left).
2736 binary_infix(greater,'>',160,left).
2737 binary_infix(member,':',60,left).
2738 binary_infix(not_member,'/:',160,left).
2739 binary_infix(subset,'<:',110,left).
2740 binary_infix(subset_strict,'<<:',110,left).
2741 binary_infix(not_subset,'/<:',110,left).
2742 binary_infix(not_subset_strict,'/<<:',110,left).
2743
2744 binary_infix(values_entry,'=',60,left).
2745
2746 :- dynamic latex_mode/0, unicode_mode/0, atelierb_pp_mode/0.
2747 %latex_mode.
2748 %unicode_mode.
2749
2750
2751 set_unicode_mode :- assert(unicode_mode).
2752 set_latex_mode :- assert(latex_mode).
2753 unset_unicode_mode :-
2754 (retract(unicode_mode) -> true ; add_internal_error('Was not in Unicode mode: ',unset_unicode_mode)).
2755 unset_latex_mode :-
2756 (retract(latex_mode) -> true
2757 ; add_internal_error('Was not in Latex mode: ',unset_latex_mode)).
2758
2759 % TO DO: provide better stack-based setting/unsetting of modes or use options parameter
2760 set_translation_mode(ascii) :- !,retractall(unicode_mode), retractall(latex_mode).
2761 set_translation_mode(unicode) :- !,assert(unicode_mode).
2762 set_translation_mode(latex) :- !,assert(latex_mode).
2763 set_translation_mode(Mode) :- add_internal_error('Illegal mode:',set_translation_mode(Mode)).
2764
2765
2766 unset_translation_mode(ascii) :- !.
2767 unset_translation_mode(unicode) :- !,unset_unicode_mode.
2768 unset_translation_mode(latex) :- !,unset_latex_mode.
2769 unset_translation_mode(Mode) :- add_internal_error('Illegal mode:',unset_translation_mode(Mode)).
2770
2771
2772 exists_symbol --> {latex_mode},!, "\\exists ".
2773 exists_symbol --> {unicode_mode},!, [8707].
2774 exists_symbol --> "#".
2775 forall_symbol --> {latex_mode},!, "\\forall ".
2776 forall_symbol --> {unicode_mode},!, [8704].
2777 forall_symbol --> "!".
2778 dot_symbol --> {latex_mode},!, "\\cdot ".
2779 dot_symbol --> {unicode_mode},!, [183]. %"·". % dot also used in Rodin
2780 dot_symbol --> ".".
2781 set_brackets(X,Y) :- latex_mode,!,X='\\{', Y='\\}'.
2782 set_brackets('{','}').
2783 left_set_bracket --> {latex_mode},!, "\\{ ".
2784 left_set_bracket --> "{".
2785 right_set_bracket --> {latex_mode},!, "\\} ".
2786 right_set_bracket --> "}".
2787 maplet_symbol --> {latex_mode},!, "\\mapsto ".
2788 maplet_symbol --> {unicode_mode},!, [8614].
2789 maplet_symbol --> "|->".
2790
2791 lambda_symbol --> {unicode_mode},!, [955]. % '\x3BB\'
2792 lambda_symbol --> {latex_mode},!, "\\lambda ".
2793 lambda_symbol --> "%".
2794
2795 and_symbol --> {unicode_mode},!, [8743]. % ''\x2227\''
2796 and_symbol --> {latex_mode},!, "\\wedge ".
2797 and_symbol --> "&".
2798
2799 hash_card_symbol --> {latex_mode},!, "\\# ".
2800 hash_card_symbol --> "#".
2801 ldots --> {latex_mode},!, "\\ldots ".
2802 ldots --> "...".
2803
2804 empty_set_symbol --> {get_preference(translate_print_all_sequences,true)},!, pp_empty_sequence.
2805 empty_set_symbol --> {unicode_mode},!, [8709].
2806 empty_set_symbol --> {latex_mode},!, "\\emptyset ".
2807 empty_set_symbol --> "{}".
2808
2809 underscore_symbol --> {latex_mode},!, "\\_".
2810 underscore_symbol --> "_".
2811
2812 string_start_symbol --> {latex_mode},!, "\\textnormal{``".
2813 string_start_symbol --> """".
2814 string_end_symbol --> {latex_mode},!, "''}".
2815 string_end_symbol --> """".
2816
2817
2818 unary_postfix_in_mode(Op,Trans2,Prio) :-
2819 unary_postfix(Op,Trans,Prio), % print(op(Op,Trans)),nl,
2820 translate_in_mode(Op,Trans,Trans2).
2821
2822 binary_infix_in_mode(Op,Trans2,Prio,Assoc) :-
2823 binary_infix(Op,Trans,Prio,Assoc), % print(op(Op,Trans)),nl,
2824 translate_in_mode(Op,Trans,Trans2).
2825
2826 latex_integer_set_translation('NATURAL', '\\mathbb N '). % \nat in bsymb.sty
2827 latex_integer_set_translation('NATURAL1', '\\mathbb N_1 '). % \natn
2828 latex_integer_set_translation('INTEGER', '\\mathbb Z '). % \intg
2829
2830 latex_translation(empty_set, '\\emptyset ').
2831 latex_translation(implication, '\\mathbin\\Rightarrow ').
2832 latex_translation(conjunct,'\\wedge ').
2833 latex_translation(disjunct,'\\vee ').
2834 latex_translation(equivalence,'\\mathbin\\Leftrightarrow ').
2835 latex_translation(negation,'\\neg ').
2836 latex_translation(not_equal,'\\neq ').
2837 latex_translation(less_equal,'\\leq ').
2838 latex_translation(greater_equal,'\\geq ').
2839 latex_translation(member,'\\in ').
2840 latex_translation(not_member,'\\not\\in ').
2841 latex_translation(subset,'\\subseteq ').
2842 latex_translation(subset_strict,'\\subset ').
2843 latex_translation(not_subset,'\\not\\subseteq ').
2844 latex_translation(not_subset_strict,'\\not\\subset ').
2845 latex_translation(union,'\\cup ').
2846 latex_translation(intersection,'\\cap ').
2847 latex_translation(couple,'\\mapsto ').
2848 latex_translation(cartesian_product,'\\times').
2849 latex_translation(rec,'\\mathit{rec}').
2850 latex_translation(struct,'\\mathit{struct}').
2851 latex_translation(convert_bool,'\\mathit{bool}').
2852 latex_translation(max,'\\mathit{max}').
2853 latex_translation(min,'\\mathit{min}').
2854 latex_translation(modulo,'\\mod ').
2855 latex_translation(card,'\\mathit{card}').
2856 latex_translation(successor,'\\mathit{succ}').
2857 latex_translation(predecessor,'\\mathit{pred}').
2858 latex_translation(domain,'\\mathit{dom}').
2859 latex_translation(range,'\\mathit{ran}').
2860 latex_translation(size,'\\mathit{size}').
2861 latex_translation(first,'\\mathit{first}').
2862 latex_translation(last,'\\mathit{last}').
2863 latex_translation(front,'\\mathit{front}').
2864 latex_translation(tail,'\\mathit{tail}').
2865 latex_translation(rev,'\\mathit{rev}').
2866 latex_translation(seq,'\\mathit{seq}').
2867 latex_translation(seq1,'\\mathit{seq}_{1}').
2868 latex_translation(perm,'\\mathit{perm}').
2869 latex_translation(fin_subset,'\\mathit{FIN}').
2870 latex_translation(fin1_subset,'\\mathit{FIN}_{1}').
2871 latex_translation(first_projection,'\\mathit{prj}_{1}').
2872 latex_translation(second_projection,'\\mathit{prj}_{2}').
2873 latex_translation(pow_subset,'\\mathbb P\\hbox{}'). % POW \pow would require bsymb.sty
2874 latex_translation(pow1_subset,'\\mathbb P_1'). % POW1 \pown would require bsymb.sty
2875 latex_translation(concat,'\\hat{~}').
2876 latex_translation(relations,'\\mathbin\\leftrightarrow'). % <->, \rel requires bsymb.sty
2877 latex_translation(total_relation,'\\mathbin{\\leftarrow\\mkern-14mu\\leftrightarrow}'). % <<-> \trel requires bsymb.sty
2878 latex_translation(total_surjection_relation,'\\mathbin{\\leftrightarrow\\mkern-14mu\\leftrightarrow}'). % <<->> \strel requires bsymb.sty
2879 latex_translation(surjection_relation,'\\mathbin{\\leftrightarrow\\mkern-14mu\\rightarrow}'). % <->> \srel requires bsymb.sty
2880 latex_translation(partial_function,'\\mathbin{\\mkern6mu\\mapstochar\\mkern-6mu\\rightarrow}'). % +-> \pfun requires bsymb.sty, but \mapstochar is not supported by Mathjax
2881 latex_translation(partial_injection,'\\mathbin{\\mkern9mu\\mapstochar\\mkern-9mu\\rightarrowtail}'). % >+> \pinj requires bsymb.sty
2882 latex_translation(partial_surjection,'\\mathbin{\\mkern6mu\\mapstochar\\mkern-6mu\\twoheadrightarrow}'). % >+> \psur requires bsymb.sty
2883 latex_translation(total_function,'\\mathbin\\rightarrow'). % --> \tfun would require bsymb.sty
2884 latex_translation(total_surjection,'\\mathbin\\twoheadrightarrow'). % -->> \tsur requires bsymb.sty
2885 latex_translation(total_injection,'\\mathbin\\rightarrowtail'). % >-> \tinj requires bsymb.sty
2886 latex_translation(total_bijection,'\\mathbin{\\rightarrowtail\\mkern-18mu\\twoheadrightarrow}'). % >->> \tbij requires bsymb.sty
2887 latex_translation(domain_restriction,'\\mathbin\\lhd'). % <| domres requires bsymb.sty
2888 latex_translation(range_restriction,'\\mathbin\\rhd'). % |> ranres requires bsymb.sty
2889 latex_translation(domain_subtraction,'\\mathbin{\\lhd\\mkern-14mu-}'). % <<| domsub requires bsymb.sty
2890 latex_translation(range_subtraction,'\\mathbin{\\rhd\\mkern-14mu-}'). % |>> ransub requires bsymb.sty
2891 latex_translation(overwrite,'\\mathbin{\\lhd\\mkern-9mu-}'). % <+ \ovl requires bsymb.sty
2892 latex_translation(general_sum,'\\Sigma ').
2893 latex_translation(general_product,'\\Pi ').
2894 latex_translation(lambda,'\\lambda ').
2895 latex_translation(quantified_union,'\\bigcup\\nolimits'). % \Union requires bsymb.sty
2896 latex_translation(quantified_intersection,'\\bigcap\\nolimits'). % \Inter requires bsymb.sty
2897 %latex_translation(truth,'\\top').
2898 %latex_translation(falsity,'\\bot').
2899 latex_translation(truth,'{\\color{olive} \\top}'). % requires \usepackage{xcolor} in Latex
2900 latex_translation(falsity,'{\\color{red} \\bot}').
2901 latex_translation(boolean_true,'{\\color{olive} \\mathit{TRUE}}').
2902 latex_translation(boolean_false,'{\\color{red} \\mathit{FALSE}}').
2903 latex_translation(pred_true,'{\\color{olive} \\mathit{TRUE}}').
2904 latex_translation(pred_false,'{\\color{red} \\mathit{FALSE}}').
2905 latex_translation(reverse,'^{-1}').
2906
2907 unicode_translation(implication, '\x21D2\').
2908 unicode_translation(conjunct,'\x2227\').
2909 unicode_translation(disjunct,'\x2228\').
2910 unicode_translation(negation,'\xAC\').
2911 unicode_translation(equivalence,'\x21D4\').
2912 unicode_translation(not_equal,'\x2260\').
2913 unicode_translation(less_equal,'\x2264\').
2914 unicode_translation(greater_equal,'\x2265\').
2915 unicode_translation(member,'\x2208\').
2916 unicode_translation(not_member,'\x2209\').
2917 unicode_translation(subset,'\x2286\').
2918 unicode_translation(subset_strict,'\x2282\').
2919 unicode_translation(not_subset,'\x2288\').
2920 unicode_translation(not_subset_strict,'\x2284\').
2921 unicode_translation(union,'\x222A\').
2922 unicode_translation(intersection,'\x2229\').
2923 unicode_translation(cartesian_product,'\xD7\').
2924 unicode_translation(couple,'\x21A6\').
2925 unicode_translation(div,'\xF7\').
2926 %unicode_translation(floored_div,'\xF7\'). % should we provide another Unicode character here ?
2927 unicode_translation(power_of,'\x2191\'). % does not exist in Rodin ?? upwards arrow used; find better symbol
2928 unicode_translation(interval,'\x2025\').
2929 unicode_translation(domain_restriction,'\x25C1\').
2930 unicode_translation(domain_subtraction,'\x2A64\').
2931 unicode_translation(range_restriction,'\x25B7\').
2932 unicode_translation(range_subtraction,'\x2A65\').
2933 unicode_translation(relations,'\x2194\').
2934 unicode_translation(partial_function,'\x21F8\').
2935 unicode_translation(total_function,'\x2192\').
2936 unicode_translation(partial_injection,'\x2914\').
2937 unicode_translation(partial_surjection,'\x2900\').
2938 unicode_translation(total_injection,'\x21A3\').
2939 unicode_translation(total_surjection,'\x21A0\').
2940 unicode_translation(total_bijection,'\x2916\').
2941 unicode_translation('INTEGER','\x2124\').
2942 unicode_translation('NATURAL','\x2115\').
2943 unicode_translation('NATURAL1','\x2115\\x2081\'). % \x2115\ is subscript 1
2944 unicode_translation(pow_subset,'\x2119\').
2945 unicode_translation(pow1_subset,'\x2119\\x2081\'). % \x2115\ is subscript 1
2946 unicode_translation(lambda,'\x3BB\').
2947 unicode_translation(general_product,'\x220F\').
2948 unicode_translation(general_sum,'\x2211\').
2949 unicode_translation(empty_set,'\x2205\').
2950 unicode_translation(truth,'\x22A4\'). % 8868 in decimal
2951 unicode_translation(falsity,'\x22A5\'). % 8869 in decimal
2952 unicode_translation(direct_product,'\x2297\').
2953 unicode_translation(parallel_product,'\x2225\').
2954 unicode_translation(reverse,'\x207B\\xB9\'). % the one ¹ is ASCII 185
2955 % unicode_translation(infinity,'\x221E\'). % 8734 in decimal
2956 unicode_translation(concat,'\x2312\').
2957 unicode_translation(insert_front,'\x21FE\').
2958 unicode_translation(insert_tail,'\x21FD\').
2959 unicode_translation(restrict_front,'\x2191\').
2960 unicode_translation(restrict_tail,'\x2192\').
2961 unicode_translation(forall, '\x2200\'). % usually forall_symbol used
2962 unicode_translation(exists, '\x2203\'). % usually exists_symbol used
2963
2964 atelierb_pp_translation(set_minus,'_moinsE').
2965 atelierb_pp_translation(cartesian_product,'_multE').
2966 atelierb_pp_translation('INTEGER','INTEGER').
2967 atelierb_pp_translation('INT','INTEGER').
2968 atelierb_pp_translation('NATURAL','NATURAL').
2969 atelierb_pp_translation('NAT','NATURAL').
2970 atelierb_pp_translation(boolean_true,btrue).
2971 atelierb_pp_translation(boolean_false,bfalse).
2972 atelierb_pp_translation(truth,'TRUE').
2973 atelierb_pp_translation(falsity,'FALSE').
2974
2975 quantified_in_mode(F,S) :-
2976 quantified(F,S1), translate_in_mode(F,S1,S).
2977
2978 translate_in_mode(F,S1,S) :-
2979 ( unicode_mode, unicode_translation(F,S) -> true
2980 ; latex_mode, latex_translation(F,S) -> true
2981 ; atelierb_pp_mode, atelierb_pp_translation(F,S) -> true
2982 ; S1=S).
2983
2984 quantified(general_sum,'SIGMA').
2985 quantified(general_product,'PI').
2986 quantified(quantified_union,'UNION').
2987 quantified(quantified_intersection,'INTER').
2988 quantified(lambda,X) :- atom_codes(X,[37]).
2989
2990
2991 translate_prolog_constructor(C,R) :- unary_prefix(C,R,_),!.
2992 translate_prolog_constructor(C,R) :- unary_postfix(C,R,_),!.
2993 translate_prolog_constructor(C,R) :- binary_infix_in_mode(C,R,_,_),!.
2994 translate_prolog_constructor(C,R) :- function_like_in_mode(C,R),!.
2995 translate_prolog_constructor(C,R) :- constants_in_mode(C,R),!.
2996 translate_prolog_constructor(C,R) :- quantified_in_mode(C,R),!.
2997
2998 % translate the Prolog constuctor of an AST node into a form for printing to the user
2999 translate_prolog_constructor_in_mode(Constructor,Result) :-
3000 unicode_mode,
3001 unicode_translation(Constructor,Unicode),!, Result=Unicode.
3002 translate_prolog_constructor_in_mode(Constructor,Result) :-
3003 latex_mode,
3004 latex_translation(Constructor,Latex),!, Result=Latex.
3005 translate_prolog_constructor_in_mode(C,R) :- translate_prolog_constructor(C,R).
3006
3007 translate_subst_or_bexpr_in_mode(latex,TExpr,String) :- !, assert(latex_mode),
3008 call_cleanup(translate_subst_or_bexpr(TExpr,String), (retract(latex_mode)->true)).
3009 translate_subst_or_bexpr_in_mode(unicode,TExpr,String) :- !, assert(unicode_mode),
3010 call_cleanup(translate_subst_or_bexpr(TExpr,String), (retract(unicode_mode)->true)).
3011 translate_subst_or_bexpr_in_mode(atelierb_pp,TExpr,String) :- !, assert(atelierb_pp_mode),
3012 call_cleanup(translate_subst_or_bexpr(TExpr,String), (retract(atelierb_pp_mode)->true)).
3013 translate_subst_or_bexpr_in_mode(Mode,TExpr,String) :-
3014 (Mode==ascii -> true ; add_internal_error('Illegal mode: ',translate_subst_or_bexpr_in_mode(Mode,TExpr,String))),
3015 translate_subst_or_bexpr(TExpr,String).
3016
3017
3018 translate_bexpression_to_unicode(TExpr,String) :-
3019 set_unicode_mode,
3020 call_cleanup(translate_bexpression(TExpr,String),unset_unicode_mode).
3021
3022 translate_bexpression(TExpr,String) :-
3023 (pp_expr(TExpr,String) -> true
3024 ; (add_error(translate_bexpression,'Could not translate bexpression: ',TExpr),String='???')).
3025
3026 translate_bexpression_to_codes(TExpr,Codes) :-
3027 reset_pp,
3028 pp_expr(TExpr,_,_LimitReached,Codes,[]).
3029
3030 pp_expr(TExpr,String) :-
3031 translate_bexpression_to_codes(TExpr,Codes),
3032 atom_codes_with_limit(String, Codes).
3033
3034 translate_bexpression_with_limit(T,S) :- translate_bexpression_with_limit(T,200,report_errors,S).
3035 translate_bexpression_with_limit(TExpr,Limit,String) :-
3036 translate_bexpression_with_limit(TExpr,Limit,report_errors,String).
3037 translate_bexpression_with_limit(TExpr,Limit,ReportErrors,String) :-
3038 (catch_call(pp_expr_with_limit(TExpr,Limit,String)) -> true
3039 ; (ReportErrors=report_errors,
3040 add_error(translate_bexpression,'Could not translate bexpression: ',TExpr),String='???')).
3041
3042 pp_expr_with_limit(TExpr,Limit,String) :-
3043 set_up_limit_reached(Codes,Limit,LimitReached),
3044 reset_pp,
3045 pp_expr(TExpr,_,LimitReached,Codes,[]),
3046 atom_codes_with_limit(String, Limit, Codes).
3047
3048
3049
3050 % pretty-type an expression, if the expression has a priority >MinPrio, parenthesis
3051 % can be ommitted, if not the expression has to be put into parenthesis
3052 pp_expr_m(TExpr,MinPrio,LimitReached,S,Srest) :-
3053 add_outer_paren(Prio,MinPrio,S,Srest,X,Xrest), % use co-routine to instantiate S as soon as possible
3054 pp_expr(TExpr,Prio,LimitReached,X,Xrest).
3055
3056 :- block add_outer_paren(-,?,?,?,?,?).
3057 add_outer_paren(Prio,MinPrio,S,Srest,X,Xrest) :-
3058 ( Prio > MinPrio -> % was >=, but problem with & / or with same priority or with non associative operators !
3059 S=X, Srest=Xrest
3060 ; otherwise ->
3061 [Open] = "(", [Close] = ")",
3062 S = [Open|X], Xrest = [Close|Srest]).
3063
3064 :- use_module(translate_keywords,[classical_b_keyword/1, translate_keyword_id/2]).
3065 translated_identifier('_zzzz_binary',R) :- !,
3066 (latex_mode -> R='z''''' ; R='z__'). % TO DO: could cause clash with user IDs
3067 translated_identifier('_zzzz_unary',R) :- !,
3068 (latex_mode -> R='z''' ; R='z_'). % TO DO: ditto
3069 translated_identifier('__RANGE_LAMBDA__',R) :- !,
3070 (latex_mode -> R='\\lambda\'' ; R = 'RANGE_LAMBDA'). %ditto
3071 % TO DO: do we need to treat _prj_arg1__, _prj_arg2__, _lambda_result_ here ?
3072 translated_identifier(ID,Res) :- get_preference(bugly_pp_scrambling,true),
3073 !,
3074 bugly_scramble_id(ID,Res).
3075 translated_identifier(NameWithDots,R) :-
3076 get_preference(translate_ids_to_parseable_format,true),
3077 atom_codes(NameWithDots,Codes),[Dot]=".",
3078 memberchk(Dot,Codes),!,
3079 replace_codes(Codes,Dot,"__",NewCodes,[]),
3080 atom_codes(R,NewCodes).
3081 translated_identifier(NameStartingWithUnderscores,R) :-
3082 get_preference(translate_ids_to_parseable_format,true),
3083 atom_codes(NameStartingWithUnderscores,Codes),[Underscore]="_",
3084 Codes = [Underscore,Underscore|NewCodes],!,
3085 atom_codes(R,NewCodes).
3086 translated_identifier(ID,R) :- atom(ID),
3087 get_preference(translate_ids_to_parseable_format,true),
3088 \+ animation_minor_mode(eventb),
3089 % most useful when converting Event-B to classical B
3090 classical_b_keyword(ID),
3091 !,
3092 translate_keyword_id(ID,R).
3093 translated_identifier(ID,Result) :- %print_message(translate(ID)),
3094 latex_mode,!,
3095 my_greek_latex_escape_atom(ID,Greek,Res),
3096 (Greek=greek -> Result = Res ; ajoin(['\\mathit{',Res,'}'],Result)).
3097 translated_identifier(X,X).
3098
3099 :- use_module(tools,[latex_escape_atom/2]).
3100
3101 greek_symbol('Delta').
3102 greek_symbol('Gamma').
3103 greek_symbol('Lambda').
3104 greek_symbol('Phi').
3105 greek_symbol('Pi').
3106 greek_symbol('Psi').
3107 greek_symbol('Rho').
3108 greek_symbol('Omega').
3109 greek_symbol('Sigma').
3110 greek_symbol('Theta').
3111 greek_symbol('Upsilon').
3112 greek_symbol('Xi').
3113 greek_symbol('alpha').
3114 greek_symbol('beta').
3115 greek_symbol('delta').
3116 greek_symbol('chi').
3117 greek_symbol('epsilon').
3118 greek_symbol('eta').
3119 greek_symbol('gamma').
3120 greek_symbol('kappa').
3121 greek_symbol('lambda').
3122 greek_symbol('mu').
3123 greek_symbol('nu').
3124 greek_symbol('phi').
3125 greek_symbol('psi').
3126 greek_symbol('rho').
3127 greek_symbol('sigma').
3128 greek_symbol('tau').
3129 greek_symbol('theta').
3130 greek_symbol('upsilon').
3131 greek_symbol('varepsilon').
3132 greek_symbol('varphi').
3133 greek_symbol('varpi').
3134 greek_symbol('varrho').
3135 greek_symbol('varsigma').
3136 greek_symbol('vartheta').
3137 greek_symbol('xi').
3138 greek_symbol('zeta').
3139 % other Latex math symbols
3140 greek_symbol('vdash').
3141 greek_symbol('models').
3142
3143
3144 my_greek_latex_escape_atom(A,greek,Res) :- greek_symbol(A),get_preference(latex_pp_greek_ids,true),!,
3145 atom_concat('\\',A,Res).
3146 my_greek_latex_escape_atom(A,no_greek,EA) :- latex_escape_atom(A,EA).
3147
3148 % ppatom + scramble if BUGYLY is TRUE
3149 ppatom_opt_scramble(Name) --> {get_preference(bugly_pp_scrambling,true)},!,
3150 {bugly_scramble_id(Name,ScrName)},
3151 ppatom(ScrName).
3152 ppatom_opt_scramble(Name) --> pp_atom_opt_latex(Name).
3153
3154 :- use_module(tools,[b_escape_string_atom/2]).
3155 % a version of ppatom which encodes/quotes symbols inside strings such as quotes "
3156 ppstring_opt_scramble(Name) --> {var(Name)},!,ppatom(Name).
3157 ppstring_opt_scramble(Name) --> {get_preference(bugly_pp_scrambling,true)},!,
3158 {bugly_scramble_id(Name,ScrName)},
3159 ppatom(ScrName).
3160 ppstring_opt_scramble(Name) --> {b_escape_string_atom(Name,EscName)},
3161 pp_atom_opt_latex(EscName).
3162
3163 pp_atom_opt_latex(Name) --> {latex_mode},!,
3164 {my_greek_latex_escape_atom(Name,_,EscName)},
3165 % should we add \mathrm{.} or \mathit{.}?
3166 ppatom(EscName).
3167 pp_atom_opt_latex(Name) --> ppatom(Name).
3168
3169 pp_atom_opt_latex_mathit(Name) --> {latex_mode},!,
3170 {latex_escape_atom(Name,EscName)},
3171 "\\mathit{",ppatom(EscName),"}".
3172 pp_atom_opt_latex_mathit(Name) --> ppatom(Name).
3173
3174 pp_atom_opt_mathit(EscName) --> {latex_mode},!,
3175 % we assume already escaped
3176 "\\mathit{",ppatom(EscName),"}".
3177 pp_atom_opt_mathit(Name) --> ppatom(Name).
3178
3179 pp_space --> {latex_mode},!, "\\ ".
3180 pp_space --> " ".
3181
3182 opt_scramble_id(ID,Res) :- get_preference(bugly_pp_scrambling,true),!,
3183 bugly_scramble_id(ID,Res).
3184 opt_scramble_id(ID,ID).
3185
3186 :- use_module(probsrc(gensym),[gensym/2]).
3187 :- dynamic bugly_scramble_id_cache/2.
3188 bugly_scramble_id(ID,Res) :- var(ID),!, add_internal_error('Illegal call: ',bugly_scramble_id(ID,Res)), ID=Res.
3189 bugly_scramble_id(ID,Res) :- bugly_scramble_id_cache(ID,ScrambledID),!,
3190 Res=ScrambledID.
3191 bugly_scramble_id(ID,Res) :- %print(gen_id(ID,Res)),nl,
3192 genbuglynr(Nr), ajoin(['aa',Nr],ScrambledID),
3193 assert(bugly_scramble_id_cache(ID,ScrambledID)),
3194 Res = ScrambledID.
3195
3196 :- dynamic bugly_count/1.
3197 bugly_count(0).
3198 genbuglynr(Nr) :-
3199 retract(bugly_count(Nr)), N1 is Nr + 1,
3200 assert(bugly_count(N1)).
3201
3202 replace_codes([],_,_) --> !.
3203 replace_codes([C|Rest],S,N) --> replace_codes2(C,S,N),replace_codes(Rest,S,N).
3204 replace_codes2(S,S,N,I,O) :- !,append(N,O,I).
3205 replace_codes2(S,_,_) --> [S].
3206
3207 is_lambda_result_id(b(identifier(ID),_,_INFO),Suffix) :- % _INFO=[lambda_result], sometiems _INFO=[]
3208 is_lambda_result_name(ID,Suffix).
3209 is_lambda_result_name(LAMBDA_RESULT,Suffix) :- atomic(LAMBDA_RESULT),
3210 atom_codes(LAMBDA_RESULT,[95,108,97,109,98,100,97,95,114,101,115,117,108,116,95|Suffix]). % _lambda_result_
3211
3212 pp_expr(TE,P) --> %{print('OBSOLETE'),nl,nl},
3213 pp_expr(TE,P,_LimitReached).
3214
3215 pp_expr(TExpr,Prio,_) --> {var(TExpr)},!,"_",{Prio=500}.
3216 pp_expr(_,Prio,LimitReached) --> {LimitReached==limit_reached},!,"...",{Prio=500}.
3217 pp_expr(LambdaID,Prio,_) --> {is_lambda_result_id(LambdaID,Suffix)},!, {Prio=500},
3218 {append("LAMBDA_RESULT___",Suffix,ASCII), atom_codes(R,ASCII)}, ppatom(R).
3219 pp_expr(TExpr,Prio,LimitReached) -->
3220 ( {is_texpr(TExpr)} -> pp_expr0(TExpr,Prio,LimitReached)
3221 ; pp_expr2(TExpr,Prio,LimitReached)).
3222
3223 pp_expr0(TExpr,Prio,_LimitReached) -->
3224 {animation_minor_mode(eventb),
3225 get_texpr_expr(TExpr,Expr),
3226 get_texpr_info(TExpr,Info)},
3227 pp_theory_operator(Expr,Info,Prio),!.
3228 pp_expr0(TExpr,Prio,LimitReached) -->
3229 { %get_texpr_type(TExpr,Type), % we could dispatch depending on type
3230 get_texpr_expr(TExpr,Expr),get_texpr_info(TExpr,Info),get_texpr_type(TExpr,Type),
3231 check_info(Expr,Type,Info)},
3232 pp_rodin_label(TExpr),
3233 (pp_expr1(Expr,Type,Info,Prio,LimitReached) -> {true}
3234 ; {add_error(translate,'Could not translate:',Expr,Expr),fail}
3235 ).
3236
3237 check_info(Expr,_,Info) :- var(Info), add_error(translate,'Illegal info field for expression: ', Expr),fail.
3238 check_info(_,_,_).
3239
3240 pp_theory_operator(general_sum(_,Membercheck,_),_Info,500) -->
3241 {get_texpr_expr(Membercheck,member(_,Arg))},
3242 ppatom('SUM('),pp_expr(Arg,_),ppatom(')').
3243 pp_theory_operator(general_product(_,Membercheck,_),_Info,500) -->
3244 {get_texpr_expr(Membercheck,member(_Couple,Arg))},
3245 ppatom('PRODUCT('),pp_expr(Arg,_),ppatom(')').
3246 pp_theory_operator(function(_,Arg),Info,500) -->
3247 {memberchk_in_info(theory_operator(O,N),Info),decouplise_expr(N,Arg,Args)},
3248 ppatom(O),"(",pp_expr_l_sep(Args,",",_LR),")".
3249 pp_theory_operator(member(Arg,_),Info,500) -->
3250 {memberchk_in_info(theory_operator(O,N),Info),decouplise_expr(N,Arg,Args)},
3251 ppatom(O),"(",pp_expr_l_sep(Args,",",_LR),")".
3252
3253 decouplise_expr(1,E,R) :- !,R=[E].
3254 decouplise_expr(N,E,R) :-
3255 get_texpr_expr(E,couple(A,B)),!,
3256 N2 is N-1,
3257 decouplise_expr(N2,A,R1),append(R1,[B],R).
3258 decouplise_expr(N,E,[E]) :-
3259 print_message(call_failed(decouplise_expr(N,E,_))),nl.
3260
3261 % will pretty print (first) rodin or pragma label
3262 pp_rodin_label(_TExpr) --> {get_preference(translate_suppress_rodin_positions_flag,true),!}.
3263 pp_rodin_label(_TExpr) --> {get_preference(bugly_pp_scrambling,true),!}.
3264 pp_rodin_label(TExpr) --> {bsyntaxtree:get_texpr_labels(TExpr,Label)},!,
3265 pp_start_label_pragma,ppatoms_opt_latex(Label),pp_end_label_pragma.
3266 pp_rodin_label(_TExpr) --> [].
3267
3268 pp_start_label_pragma --> {atelierb_pp_mode},!, "/*@label ".
3269 pp_start_label_pragma --> "/* @". % shorter version, for viewing in UI
3270 pp_end_label_pragma --> " */ ".
3271
3272 ppatoms([]) --> !, [].
3273 ppatoms([ID|T]) --> !,ppatom(ID), " ", ppatoms(T).
3274 ppatoms(X) --> {add_error(ppatoms,'Not a list of atoms: ',ppatoms(X))}.
3275
3276 ppatoms_opt_latex([]) --> !, [].
3277 ppatoms_opt_latex([ID|T]) --> !,pp_atom_opt_latex(ID), " ", ppatoms_opt_latex(T).
3278 ppatoms_opt_latex(X) --> {add_error(ppatoms_opt_latex,'Not a list of atoms: ',ppatoms_opt_latex(X))}.
3279
3280 :- use_module(bsyntaxtree,[is_set_type/2]).
3281 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
3282 pp_expr1(Expr,_,_,Prio,_) --> {var(Expr)},!,"_",{Prio=500}.
3283 pp_expr1(event_b_comprehension_set(Ids,E,P),Type,_Info,Prio,LimitReached) -->
3284 {print(event_b_comp(Ids,E,P)),nl,
3285 b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,E,P,Type, NewExpression), print(conv),nl},!,
3286 pp_expr(NewExpression,Prio,LimitReached).
3287 pp_expr1(comprehension_set([I1,I2,_I3],P),_,Info,500,LimitReached) -->
3288 /* This comprehension set was a projection function (prj1/prj2) */
3289 ? {member_in_info(was(Prj),Info),(Prj=prj1;Prj=prj2),!,
3290 lookup_membership(I1,P,Set1), lookup_membership(I2,P,Set2)},
3291 ppatom(Prj),"(",pp_expr(Set1,_,LimitReached),",",pp_expr(Set2,_),")".
3292 pp_expr1(union(b(event_b_identity,Type,_), b(closure(Rel),Type,_)),_,Info,500,LimitReached) -->
3293 /* closure(Rel) = id \/ closure1(Rel) */
3294 {member_in_info(was(reflexive_closure),Info)},!,
3295 "closure(",pp_expr(Rel,_,LimitReached),")".
3296 pp_expr1(comprehension_set([_],_),_,Info,500,_LimitReached) -->
3297 {memberchk_in_info(freetype(P),Info),!},ppatom(P).
3298 % used instead of constants(Expr,Symbol) case below:
3299 pp_expr1(comprehension_set([TID],b(B,_,_)),Type,Info,Prio,LimitReached) -->
3300 {memberchk_in_info(was(integer_set(S)),Info)},
3301 {S='INTEGER' -> B=truth
3302 ; get_texpr_id(TID,ID),B=greater_equal(TID2,b(integer(I),_,_)), get_texpr_id(TID2,ID),
3303 (I=0 -> S='NATURAL' ; I=1,S='NATURAL1')}, % TO DO: check bounds
3304 !,
3305 pp_expr1(integer_set(S),Type,Info,Prio,LimitReached).
3306 pp_expr1(interval(b(A,_,_),B),Type,Info,Prio,LimitReached) -->
3307 {memberchk_in_info(was(integer_set(S)),Info)},
3308 {B=b(max_int,integer,_)}, % TO DO ? allow value(int(Mx))
3309 {A=min_int -> S='INT' ; A=integer(0) -> S='NAT' ; A=integer(1),S='NAT1'},
3310 !,
3311 pp_expr1(integer_set(S),Type,Info,Prio,LimitReached).
3312 pp_expr1(falsity,_,Info,Prio,LimitReached) --> {memberchk_in_info(was(Pred),Info)},!,
3313 ({(unicode_mode ; latex_mode)}
3314 -> {translate_in_mode(falsity,'falsity',Symbol)},
3315 ppatom(Symbol),
3316 ({get_preference(pp_propositional_logic_mode,true)} -> {true}
3317 ; " ", enter_comment, " ", pp_expr2(Pred,Prio,LimitReached), " ", exit_comment)
3318 ; enter_comment, " falsity ",exit_comment, " ",
3319 pp_expr2(Pred,Prio,LimitReached)). % Pred is not wrapped
3320 pp_expr1(truth,_,Info,Prio,LimitReached) --> {memberchk_in_info(was(Pred),Info)},!,
3321 ({(unicode_mode ; latex_mode)}
3322 -> {translate_in_mode(truth,'truth',Symbol)},
3323 ppatom(Symbol),
3324 ({get_preference(pp_propositional_logic_mode,true)} -> {true}
3325 ; " ",enter_comment, " ", pp_expr2(Pred,Prio,LimitReached), " ", exit_comment)
3326 ; enter_comment, " truth ", exit_comment, " ",
3327 pp_expr2(Pred,Prio,LimitReached)). % Pred is not wrapped
3328 % TO DO: do this for other expressions as well; but then we have to ensure that ast_cleanup generates complete was(_) infos
3329 % :- load_files(library(system), [when(compile_time), imports([environ/2])]). % directive moved above to avoid Spider warning
3330 pp_expr1(event_b_identity,Type,_Info,500,_LimitReached) -->
3331 {\+ animation_minor_mode(eventb)}, %{atelierb_pp_mode},
3332 {is_set_type(Type,couple(ElType,ElType))},
3333 !,
3334 "id(", {pretty_type(ElType,S)},ppatom(S), ")".
3335 :- if(environ(prob_safe_mode,true)).
3336 pp_expr1(exists(Parameters,_),_,Info,_Prio,_LimitReached) -->
3337 {\+ member_in_info(used_ids(_),Info),
3338 add_error(translate,'Missing used_ids Info for exists: ',Parameters:Info),fail}.
3339 %pp_expr1(exists(Ids,P1),_,Info,250) --> !, { member_in_info(used_ids(Used),Info)},
3340 % exists_symbol,pp_expr_ids_in_mode(Ids,LimitReached),
3341 % {add_normal_typing_predicates(Ids,P1,P)},
3342 % " /* Used = ", ppterm(Used), " */ ",
3343 % ".",pp_expr_m(P,221).
3344 :- endif.
3345 pp_expr1(Expr,_,Info,Prio,LimitReached) --> {member_in_info(sharing(ID,Count,_,_),Info),number(Count),Count>1},!,
3346 "( ",enter_comment," CSE ",ppnumber(ID), ":#", ppnumber(Count),
3347 ({member_in_info(contains_wd_condition,Info)} -> " (wd) " ; " "),exit_comment, " ",
3348 pp_expr2(Expr,Prio,LimitReached), ")".
3349 %pp_expr1(Expr,_,Info,Prio) --> {member_in_info(contains_wd_condition,Info)},!,
3350 % "( /* (wd) */ ", pp_expr2(Expr,Prio), ")".
3351 % pp_expr1(Expr,subst,_Info,Prio) --> !, translate_subst2(Expr,Prio). % TO DO: also allow substitutions here
3352 pp_expr1(Expr,_,_Info,Prio,LimitReached) --> pp_expr2(Expr,Prio,LimitReached).
3353
3354 lookup_membership(TId,P,Set) :-
3355 get_texpr_id(TId,Id),get_texpr_id(Temp,Id),
3356 create_texpr(member(Temp,Set),pred,_,Member),
3357 ? member_in_conjunction(Member,P),!.
3358 lookup_membership(TId,P,b(set_extension([EqValue]),set(T),[])) :-
3359 get_texpr_id(TId,Id),get_texpr_id(Temp,Id),
3360 create_texpr(equal(Temp,EqValue),pred,_,Equal),
3361 get_texpr_type(EqValue,T),
3362 member_in_conjunction(Equal,P),!.
3363 lookup_membership(TId,_P,atom_string(TS)) :- % atom_string used as wrapper for pp_expr2
3364 get_texpr_type(TId,Type),pretty_type(Type,TS).
3365 % add_error(translate,'Failed: ',lookup_membership(TId,P,Set)), Set=unknown.
3366
3367
3368 pp_expr2(Expr,_,_LimitReached) --> {var(Expr)},!,"_".
3369 pp_expr2(_,_,LimitReached) --> {LimitReached==limit_reached},!,"...".
3370 pp_expr2(value(V),Prio,LimitReached) --> !,
3371 {(nonvar(V),V=closure(_,_,_) -> Prio=300 ; Prio=500)}, pp_value(V,LimitReached).
3372 pp_expr2(atom_string(V),500,_) --> !,pp_atom_opt_latex_mathit(V). % hardwired_atom
3373 pp_expr2(global_set(V),500,_) --> !,ppatom_opt_scramble(V).
3374 pp_expr2(freetype_set(V),500,_) --> !,{pretty_freetype(V,P)},ppatom_opt_scramble(P).
3375 pp_expr2(lazy_lookup_expr(I),500,_) --> !, ppatom_opt_scramble(I).
3376 pp_expr2(lazy_lookup_pred(I),500,_) --> !, ppatom_opt_scramble(I).
3377 pp_expr2(identifier(I),500,_) --> !,
3378 {( I=op(Id) -> true; I=Id)},
3379 ( {atomic(Id)} -> ({translated_identifier(Id,TId)},ppatom(TId))
3380 ; {otherwise} ->
3381 "'",ppterm(Id), "'").
3382 pp_expr2(integer(N),500,_) --> !, ppnumber(N).
3383 pp_expr2(integer_set(S),500,_) --> !,
3384 {integer_set_mapping(S,T)},ppatom(T).
3385 pp_expr2(string(S),500,_) --> !, string_start_symbol, ppstring_opt_scramble(S), string_end_symbol.
3386 pp_expr2(set_extension(Ext),500,LimitReached) --> !, {set_brackets(L,R)},
3387 pp_expr_wrap_l(L,Ext,R,LimitReached).
3388 pp_expr2(sequence_extension(Ext),500,LimitReached) --> !,
3389 pp_begin_sequence,
3390 ({get_preference(translate_print_cs_style_sequences,true)} -> pp_expr_l_sep(Ext,"",LimitReached)
3391 ; pp_expr_l_sep(Ext,",",LimitReached)),
3392 pp_end_sequence.
3393 pp_expr2(assign(LHS,RHS),10,LimitReached) --> !,
3394 pp_expr_wrap_l(',',LHS,'',LimitReached), ":=", pp_expr_wrap_l(',',RHS,'',LimitReached).
3395 pp_expr2(assign_single_id(LHS,RHS),10,LimitReached) --> !, pp_expr2(assign([LHS],[RHS]),10,LimitReached).
3396 pp_expr2(parallel(RHS),10,LimitReached) --> !,
3397 pp_expr_wrap_l('||',RHS,'',LimitReached).
3398 pp_expr2(sequence(RHS),10,LimitReached) --> !,
3399 pp_expr_wrap_l(';',RHS,'',LimitReached).
3400 pp_expr2(comprehension_set(Ids,P1),500,LimitReached) --> !,
3401 pp_comprehension_set(Ids,P1,LimitReached).
3402 pp_expr2(event_b_comprehension_set(Ids,E,P1),500,LimitReached) --> !, % normally conversion above should trigger; this is if we call pp_expr for untyped expressions
3403 pp_event_b_comprehension_set(Ids,E,P1,LimitReached).
3404 pp_expr2(recursive_let(Id,S),500,LimitReached) --> !,
3405 ({animation_minor_mode(eventb)} -> "" % otherwise we get strange characters in Rodin
3406 ; enter_comment," recursive ID ", pp_expr(Id,_,LimitReached), " ", exit_comment),
3407 pp_expr(S,_,LimitReached).
3408 pp_expr2(image(A,B),300,LimitReached) --> !,
3409 pp_expr_m(A,249,LimitReached),"[", % was 0; but we may have to bracket A; e.g., f <| {2} [{2}] is not ok; 250 is priority of lambda
3410 pp_expr_m(B,0,LimitReached),"]". % was 500, now set to 0: we never need an outer pair of () !?
3411 pp_expr2(function(A,B),300,LimitReached) --> !,
3412 pp_expr_m(A,249,LimitReached), % was 0; but we may have to bracket A; e.g., f <| {2} (2) is not ok; 250 is priority of lambda
3413 pp_function_left_bracket,
3414 pp_expr_m(B,0,LimitReached), % was 500, now set to 0: we never need an outer pair of () !?
3415 pp_function_right_bracket.
3416 pp_expr2(definition(A,B),300,LimitReached) --> !, % definition call; usually inlined,...
3417 ppatom(A),
3418 pp_function_left_bracket,
3419 pp_expr_l_sep(B,",",LimitReached),
3420 pp_function_right_bracket.
3421 pp_expr2(operation_call_in_expr(A,B),300,LimitReached) --> !,
3422 pp_expr_m(A,249,LimitReached),
3423 pp_function_left_bracket,
3424 pp_expr_l_sep(B,",",LimitReached),
3425 pp_function_right_bracket.
3426 pp_expr2(enumerated_set_def(GS,ListEls),200,LimitReached) --> !, % for pretty printing enumerate set defs
3427 {reverse(ListEls,RLE)}, /* they have been inserted in inverse order */
3428 ppatom_opt_scramble(GS), "=", pp_expr_wrap_l('{',RLE,'}',LimitReached).
3429 pp_expr2(forall(Ids,D1,P),250,LimitReached) --> !, % TO DO ?: adapt priority in Event-B mode ? also for exists,...
3430 forall_symbol,pp_expr_ids_in_mode(Ids,LimitReached),
3431 {add_normal_typing_predicates(Ids,D1,D)},
3432 dot_symbol,pp_expr_m(b(implication(D,P),pred,[]),221,LimitReached).
3433 pp_expr2(exists(Ids,P1),250,LimitReached) --> !,
3434 exists_symbol,pp_expr_ids_in_mode(Ids,LimitReached),
3435 {add_normal_typing_predicates(Ids,P1,P)},
3436 dot_symbol,pp_expr_m(P,221,LimitReached).
3437 pp_expr2(record_field(R,I),250,LimitReached) --> !,
3438 pp_expr_m(R,251,LimitReached),"'",ppatom_opt_scramble(I).
3439 pp_expr2(rec(Fields),500,LimitReached) --> !,
3440 {function_like_in_mode(rec,Symbol)},
3441 ppatom(Symbol), "(",pp_expr_fields(Fields,LimitReached),")".
3442 pp_expr2(struct(Rec),500,LimitReached) -->
3443 {get_texpr_expr(Rec,rec(Fields)),Val=false ; get_texpr_expr(Rec,value(rec(Fields)))},!,
3444 {function_like_in_mode(struct,Symbol)},
3445 ppatom(Symbol), "(",
3446 ({Val==false} -> pp_expr_fields(Fields,LimitReached)
3447 ; pp_value_l(Fields,',',LimitReached)),
3448 ")".
3449 pp_expr2(freetype_case(FT,L,Expr),500,LimitReached) --> !,
3450 pp_freetype_term('__is_ft_case',FT,L,Expr,LimitReached).
3451 pp_expr2(freetype_constructor(_FT,L,Expr),500,LimitReached) --> !,
3452 ppatom_opt_scramble(L),ppatom('('),pp_expr(Expr,_,LimitReached),ppatom(')').
3453 pp_expr2(freetype_destructor(FT,L,Expr),500,LimitReached) --> !,
3454 pp_freetype_term('__ft~',FT,L,Expr,LimitReached).
3455 pp_expr2(let_predicate(Ids,Exprs,P),1,LimitReached) --> !,
3456 pp_expr_let_exists(Ids,Exprs,P,LimitReached). % instead of pp_expr_let
3457 pp_expr2(let_expression(Ids,Exprs,P),1,LimitReached) --> !,
3458 pp_expr_let(Ids,Exprs,P,LimitReached).
3459 pp_expr2(let_expression_global(Ids,Exprs,P),1,LimitReached) --> !, " /", "* global *", "/ ",
3460 pp_expr_let(Ids,Exprs,P,LimitReached).
3461 pp_expr2(lazy_let_pred(Id,Expr,P),Pr,LimitReached) --> !, pp_expr2(lazy_let_expr(Id,Expr,P),Pr,LimitReached).
3462 pp_expr2(lazy_let_subst(Id,Expr,P),Pr,LimitReached) --> !, pp_expr2(lazy_let_expr(Id,Expr,P),Pr,LimitReached).
3463 pp_expr2(lazy_let_expr(Id,Expr,P),1,LimitReached) --> !,
3464 pp_expr_let([Id],[Expr],P,LimitReached).
3465 pp_expr2(norm_conjunct(Cond,[]),1,LimitReached) --> !, % norm_conjunct: flattened version generated by b_interpreter_check,...
3466 "( ",pp_expr(Cond,_,LimitReached), ")".
3467 pp_expr2(norm_conjunct(Cond,[H|T]),1,LimitReached) --> !,
3468 "( ",pp_expr(Cond,_,LimitReached), ") ", and_symbol, " (", pp_expr2(norm_conjunct(H,T),_,LimitReached), ")".
3469 pp_expr2(assertion_expression(Cond,_Msg,Expr),1,LimitReached) --> !,
3470 " ", enter_comment, " ASSERT ",
3471 pp_expr_m(Cond,30,LimitReached),
3472 " IN ", exit_comment,
3473 pp_expr_m(Expr,30,LimitReached).
3474 %pp_expr2(assertion_expression(Cond,_Msg,Expr),1) --> !,
3475 % "__ASSERT ",pp_expr_m(Cond,30),
3476 % " IN ", pp_expr_m(Expr,30).
3477 pp_expr2(partition(S,Elems),500,LimitReached) -->
3478 {animation_minor_mode(eventb) ;
3479 \+ atelierb_pp_mode, length(Elems,Len), Len>50 % we need to print a quadratic number of disjoints
3480 },!,
3481 "partition(",pp_expr(S,_,LimitReached),
3482 ({Elems=[]} -> ")" ; pp_expr_wrap_l(',',Elems,')',LimitReached)).
3483 pp_expr2(partition(S,Elems),500,LimitReached) --> !,
3484 "(",pp_expr(S,_,LimitReached), " = ",
3485 ({Elems=[]} -> "{})"
3486 ; pp_expr_l_sep(Elems,"\\/",LimitReached), pp_all_disjoint(Elems,LimitReached),")").
3487 pp_expr2(if_then_else(If,Then,Else),1,LimitReached) --> {animation_minor_mode(z)},!,
3488 "\\IF ",pp_expr_m(If,30,LimitReached),
3489 " \\THEN ",pp_expr_m(Then,30,LimitReached),
3490 " \\ELSE ",pp_expr_m(Else,30,LimitReached).
3491 %pp_expr2(if_then_else(If,Then,Else),1) --> {unicode_mode},!,
3492 % "if ",pp_expr_m(If,30), " then ",pp_expr_m(Then,30), " else ",pp_expr_m(Else,30).
3493 pp_expr2(if_then_else(If,Then,Else),Prio,LimitReached) --> {atelierb_pp_mode},!,
3494 % print IF-THEN-ELSE using a translation that Atelier-B can understand:
3495 {get_texpr_type(Then,Type),
3496 ARG = b(boolean_true,integer,[]), AT=boolean, % we could use unit type or BOOL here
3497 gen_fresh_id_if_necessary('_zzzz_unary',b(if_then_else(If,Then,Else),Type,[]),ID1),
3498 gen_fresh_id_if_necessary('_zzzz_binary',b(if_then_else(If,Then,Else),Type,[]),ID2),
3499 Id1 = b(identifier(ID1),AT,[]), % a dummy argument
3500 Id2 = b(identifier(ID2),Type,[]), % The result
3501 Eq1 = b(equal(Id2,Then),pred,[]), Eq2 = b(equal(Id2,Else),pred,[]),
3502 Pred1 = b(implication(If,Eq1),pred,[]),
3503 Pred2 = b(implication(b(negation(If),pred,[]),Eq2),pred,[]),
3504 Pred = b(conjunct(Pred1,Pred2),pred,[]),
3505 FUN = b(comprehension_set([Id1,Id2],Pred),set(couple(AT,Type)),[]),
3506 Expr = b(function(FUN,ARG),Type,[])},
3507 % construct {d,x| If => x=Then & not(if) => x=Else}(TRUE)
3508 pp_expr(Expr,Prio,LimitReached).
3509 pp_expr2(if_then_else(If,Then,Else),1,LimitReached) -->
3510 pp_atom_opt_mathit('IF'),pp_space, % "IF ",
3511 pp_expr_m(If,30,LimitReached),
3512 pp_space, pp_atom_opt_mathit('THEN'),pp_space, %" THEN ",
3513 pp_expr_m(Then,30,LimitReached),
3514 pp_space, pp_atom_opt_mathit('ELSE'),pp_space, %" ELSE ",
3515 pp_expr_m(Else,30,LimitReached),
3516 pp_space, pp_atom_opt_mathit('END'). %" END"
3517 pp_expr2(kodkod(Id,Identifiers),300,LimitReached) -->
3518 "KODKOD_CALL(",ppnumber(Id),": ",pp_expr_ids(Identifiers,LimitReached),")".
3519 pp_expr2(Expr,500,_) -->
3520 {constants_in_mode(Expr,Symbol)},!,ppatom(Symbol).
3521 pp_expr2(equal(A,B),Prio,LimitReached) -->
3522 {get_preference(pp_propositional_logic_mode,true), % a mode for printing propositional logic formuli
3523 is_boolean_value(B,BV),
3524 get_texpr_id(A,_)},!,
3525 ({BV=pred_true} -> pp_expr(A,Prio,LimitReached)
3526 ; pp_expr2(negation(b(equal(A,b(boolean_true,boolean,[])),pred,[])),Prio,LimitReached)).
3527 pp_expr2(Expr,Prio,LimitReached) -->
3528 {functor(Expr,F,1),
3529 unary_prefix(F,Symbol,Prio),!,
3530 arg(1,Expr,Arg),APrio is Prio+1},
3531 ppatom(Symbol), " ",
3532 pp_expr_m(Arg,APrio,LimitReached).
3533 pp_expr2(Expr,500,LimitReached) -->
3534 {functor(Expr,F,1),
3535 unary_prefix_parentheses(F,Symbol),!,
3536 arg(1,Expr,Arg)},
3537 pp_atom_opt_latex(Symbol), "(", pp_expr(Arg,_,LimitReached), ")".
3538 pp_expr2(Expr,Prio,LimitReached) -->
3539 {functor(Expr,F,1),
3540 unary_postfix_in_mode(F,Symbol,Prio),!,
3541 arg(1,Expr,Arg),APrio is Prio+1},
3542 pp_expr_m(Arg,APrio,LimitReached),ppatom(Symbol).
3543 pp_expr2(power_of(Left,Right),Prio,LimitReached) --> {latex_mode},!, % special case, as we need to put {} around RHS
3544 {Prio=200, LPrio is Prio+1, RPrio = Prio},
3545 pp_expr_m(Left,LPrio,LimitReached),
3546 "^{",
3547 pp_expr_m(Right,RPrio,LimitReached),
3548 "}".
3549 pp_expr2(Expr,OPrio,LimitReached) -->
3550 {functor(Expr,F,2),
3551 binary_infix_in_mode(F,Symbol,Prio,Ass),!,
3552 arg(1,Expr,Left),
3553 arg(2,Expr,Right),
3554 ( Ass = left, binary_infix_symbol(Left,Symbol) -> LPrio is Prio-1, RPrio is Prio+1
3555 ; Ass = right, binary_infix_symbol(Right,Symbol) -> LPrio is Prio+1, RPrio is Prio-1
3556 ; otherwise -> LPrio is Prio+1, RPrio is Prio+1)},
3557 % Note: Prio+1 is actually not necessary, Prio would be sufficient, as pp_expr_m uses a strict comparison <
3558 ({always_surround_by_parentheses(F)} -> "(",{OPrio=1000} ; {OPrio=Prio}),
3559 pp_expr_m(Left,LPrio,LimitReached),
3560 " ", ppatom(Symbol), " ",
3561 pp_expr_m(Right,RPrio,LimitReached),
3562 ({always_surround_by_parentheses(F)} -> ")" ; []).
3563 pp_expr2(first_of_pair(X),500,LimitReached) --> {get_texpr_type(X,couple(From,To))},!,
3564 {pretty_type(From,FromT), pretty_type(To,ToT)},
3565 "prj1(", % TO DO: Latex version
3566 pp_atom_opt_latex(FromT), ",", pp_atom_opt_latex(ToT), ")(",
3567 pp_expr(X,_,LimitReached),")".
3568 pp_expr2(second_of_pair(X),500,LimitReached) --> {get_texpr_type(X,couple(From,To))},!,
3569 {pretty_type(From,FromT), pretty_type(To,ToT)},
3570 "prj2(", pp_atom_opt_latex(FromT), ",", pp_atom_opt_latex(ToT), ")(",
3571 pp_expr(X,_,LimitReached),")".
3572 pp_expr2(Call,500,LimitReached) --> {external_call(Call,Symbol,Args)},!,
3573 ({invisible_external_pred(Symbol)}
3574 -> "1=1 /* ",pp_expr_m(atom_string(Symbol),20,LimitReached),pp_expr_wrap_l('(',Args,') */',LimitReached)
3575 ; pp_expr_m(atom_string(Symbol),20,LimitReached),
3576 pp_expr_wrap_l('(',Args,')',LimitReached) % pp_expr_wrap_l('/*EXT:*/(',Args,')')
3577 ).
3578 pp_expr2(card(A),500,LimitReached) --> {latex_mode, get_preference(latex_pp_greek_ids,true)},!,
3579 "|",pp_expr_m(A,0,LimitReached),"|".
3580 pp_expr2(Expr,500,LimitReached) -->
3581 {functor(Expr,F,_),
3582 function_like_in_mode(F,Symbol),!,
3583 Expr =.. [F|Args]},
3584 ppatom(Symbol),pp_expr_wrap_l('(',Args,')',LimitReached).
3585 pp_expr2(Expr,250,LimitReached) -->
3586 {functor(Expr,F,3),
3587 quantified_in_mode(F,Symbol),
3588 Expr =.. [F,Ids,P1,E],
3589 !,
3590 add_normal_typing_predicates(Ids,P1,P)},
3591 ppatom(Symbol),pp_expr_ids(Ids,LimitReached),".(",
3592 pp_expr_m(P,11,LimitReached),pp_such_that_bar(E),
3593 pp_expr_m(E,11,LimitReached),")".
3594 pp_expr2(Expr,Prio,_LimitReached) -->
3595 {functor(Expr,F,N),print(pp_expr2_unknown_expr(functor(F/N),prio(Prio),expr(Expr))),nl, % trace,
3596 %add_internal_error('Unknown Expression: ',pp_expr2(Expr,Prio)),
3597 Prio=20},
3598 ppterm(Expr).
3599
3600 invisible_external_pred('LEQ_SYM_BREAK'). % just for symmetry breaking foralls,...
3601 external_call(external_function_call(Symbol,Args),Symbol,Args).
3602 external_call(external_pred_call(Symbol,Args),Symbol,Args).
3603 external_call(external_subst_call(Symbol,Args),Symbol,Args).
3604
3605 pp_all_disjoint([H1,H2],LimitReached) --> !, " ",and_symbol," ", pp_disjoint(H1,H2,LimitReached).
3606 pp_all_disjoint([H1|T],LimitReached) --> pp_all_disjoint_aux(T,H1,LimitReached), pp_all_disjoint(T,LimitReached).
3607 pp_all_disjoint([],_) --> "".
3608
3609 pp_all_disjoint_aux([],_,_) --> "".
3610 pp_all_disjoint_aux([H2|T],H1,LimitReached) --> " ",and_symbol," ",
3611 pp_disjoint(H1,H2,LimitReached), pp_all_disjoint_aux(T,H1,LimitReached).
3612
3613 pp_disjoint(H1,H2,LimitReached) --> pp_expr(H1,_), "/\\", pp_expr(H2,_,LimitReached), " = {}".
3614
3615
3616 :- use_module(bsyntaxtree,[is_a_disjunct/3]).
3617
3618 pp_comprehension_set([ID1|T],Body,LimitReached) --> {is_a_disjunct(Body,B1,B2),
3619 get_last(T,ID1,_FrontIDs,LastID),
3620 is_lambda_result_id(LastID,_Suffix)},!, % we seem to have the union of two lambda expressions
3621 "(", pp_comprehension_set([ID1|T],B1,LimitReached),
3622 " \\/ ", pp_comprehension_set([ID1|T],B2,LimitReached), ")".
3623 pp_comprehension_set([b(identifier('_pred_'),integer,_),
3624 b(identifier('_lambda_result_'),integer,_)],Body,_) -->
3625 {Body = b(equal(LR,T),pred,_),
3626 LR = b(identifier('_lambda_result_'),integer,_),
3627 T = b(minus(ARG,One),integer,_),
3628 One = b(integer(1),integer,_),
3629 ARG = b(identifier('_pred_'),integer,_)},
3630 !,
3631 "pred".
3632 pp_comprehension_set([b(identifier('_succ_'),integer,_),
3633 b(identifier('_lambda_result_'),integer,_)],Body,_) -->
3634 {Body = b(equal(LR,T),pred,_),
3635 LR = b(identifier('_lambda_result_'),integer,_),
3636 T = b(add(ARG,One),integer,_),
3637 One = b(integer(1),integer,_),
3638 ARG = b(identifier('_succ_'),integer,_)},
3639 !,
3640 "succ".
3641 pp_comprehension_set([ID1|T],Body,LimitReached) --> {get_last(T,ID1,FrontIDs,LastID),
3642 is_lambda_result_id(LastID,Suffix),
3643 % nl, print(lambda(Body,T,ID1)),nl,
3644 (is_an_equality(Body,From,ToExpr) -> LambdaBody = b(truth,pred,[])
3645 ; is_a_conjunct(Body,LambdaBody,Equality),
3646 is_an_equality(Equality,From,ToExpr)),
3647 is_lambda_result_id(From,Suffix)},!,
3648 {add_normal_typing_predicates(FrontIDs,LambdaBody,TLambdaBody)},
3649 lambda_symbol, % "%"
3650 pp_lambda_identifiers(FrontIDs,LimitReached),
3651 ".(",
3652 pp_expr_m(TLambdaBody,11,LimitReached), % Check 11 against prio of . and |
3653 pp_such_that_bar(ToExpr),
3654 pp_expr_m(ToExpr,11,LimitReached),
3655 ")".
3656 pp_comprehension_set(Ids,P1,LimitReached) -->
3657 left_set_bracket,
3658 pp_expr_l_pair_in_mode(Ids,LimitReached),
3659 {add_normal_typing_predicates(Ids,P1,P)},
3660 pp_such_that_bar(P),
3661 pp_expr_m(P,11,LimitReached),
3662 right_set_bracket.
3663
3664 pp_event_b_comprehension_set(Ids,E,P1,LimitReached) -->
3665 left_set_bracket,pp_expr_l_pair_in_mode(Ids,LimitReached),
3666 {add_normal_typing_predicates(Ids,P1,P)},
3667 pp_such_that_bar(P),pp_expr_m(P,11,LimitReached),
3668 " . ", pp_expr_m(E,11,LimitReached),right_set_bracket.
3669
3670 pp_lambda_identifiers([H1,H2|T],LimitReached) --> {\+ animation_minor_mode(eventb)},!,
3671 "(",pp_expr_l([H1,H2|T],LimitReached),")".
3672 pp_lambda_identifiers(L,LimitReached) --> pp_expr_l_pair_in_mode(L,LimitReached).
3673
3674 pp_such_that_bar(_) --> {latex_mode},!, "\\mid ".
3675 pp_such_that_bar(b(unary_minus(_),_,_)) --> !, " | ". % otherwise AtelierB complains about illegal token |-
3676 pp_such_that_bar(_Next) --> "|".
3677 pp_such_that_bar --> {latex_mode},!, "\\mid ".
3678 pp_such_that_bar --> "|".
3679
3680 is_an_equality(b(equal(A,B),_,_),A,B).
3681
3682 integer_set_mapping(A,B) :- unicode_mode, unicode_translation(A,B),!.
3683 integer_set_mapping(A,B) :- latex_mode, latex_integer_set_translation(A,B),!.
3684 integer_set_mapping(A,B) :- atelierb_pp_mode, atelierb_pp_translation(A,B),!.
3685 integer_set_mapping(A,B) :-
3686 animation_minor_mode(eventb),eventb_integer_mapping(A,B),!.
3687 integer_set_mapping(ISet,Res) :- atomic(ISet),!,Res=ISet.
3688 integer_set_mapping(_ISet,'integer_set(??)').
3689
3690 eventb_integer_mapping('INTEGER','INT').
3691 eventb_integer_mapping('NATURAL','NAT').
3692 eventb_integer_mapping('NATURAL1','NAT1').
3693
3694 :- dynamic comment_level/1.
3695 reset_pp :- retractall(comment_level(_)).
3696 enter_comment --> {retract(comment_level(N))},!, "(*", {N1 is N+1, assert(comment_level(N1))}.
3697 enter_comment --> "/*", {assert(comment_level(1))}.
3698 exit_comment --> {retract(comment_level(N))},!,
3699 ({N>1} -> "*)", {N1 is N-1, assert(comment_level(N1))} ; "*/").
3700 exit_comment --> "*/", {add_internal_error('Unmatched closing comment:',exit_comment)}.
3701 % TO DO: ensure reset_pp is called when starting to pretty print, in case timeout occurs in previous pretty prints
3702
3703 %get_last([b(identifier(_lambda_result_10),set(couple(integer,set(couple(integer,integer)))),[])],b(identifier(i),integer,[]),[b(identifier(i),integer,[])],b(identifier(_lambda_result_10),set(couple(integer,set(couple(integer,integer)))),[]))
3704
3705 get_last([],Last,[],Last).
3706 get_last([H2|T],H1,[H1|LT],Last) :- get_last(T,H2,LT,Last).
3707
3708 pp_expr_wrap_l(Pre,Expr,Post,LimitReached) -->
3709 ppatom(Pre),pp_expr_l(Expr,LimitReached),ppatom(Post).
3710 pp_freetype_term(Term,FT,L,Expr,LimitReached) -->
3711 {pretty_freetype(FT,P)},
3712 ppatom(Term),"(",ppatom_opt_scramble(P),",",
3713 ppatom(L),",",pp_expr_m(Expr,500,LimitReached),")".
3714
3715 % print a list of expressions, seperated by commas
3716 pp_expr_l_pair_in_mode(List,LimitReached) --> {animation_minor_mode(eventb)},!,pp_expr_l_sep(List,"|->",LimitReached).
3717 pp_expr_l_pair_in_mode(List,LimitReached) --> pp_expr_l_sep(List,",",LimitReached).
3718 pp_expr_l(List,LimitReached) --> pp_expr_l_sep(List,",",LimitReached).
3719 pp_expr_l_sep([Expr],_,LimitReached) --> !,
3720 pp_expr_m(Expr,0,LimitReached).
3721 pp_expr_l_sep(List,Sep,LimitReached) --> pp_expr_l2(List,Sep,LimitReached).
3722 pp_expr_l2([],_Sep,_) --> !.
3723 pp_expr_l2([Expr|Rest],Sep,LimitReached) -->
3724 pp_expr_m(Expr,116,LimitReached),pp_expr_l3(Rest,Sep,LimitReached).
3725 pp_expr_l3([],_Sep,_) --> !.
3726 pp_expr_l3(Rest,Sep,LimitReached) -->
3727 Sep,pp_expr_l2(Rest,Sep,LimitReached).
3728
3729 % print the fields of a record
3730 pp_expr_fields([field(Name,Expr)],LimitReached) --> !,
3731 ppatom_opt_scramble(Name),":",pp_expr_m(Expr,120,LimitReached).
3732 pp_expr_fields(Fields,LimitReached) -->
3733 pp_expr_fields2(Fields,LimitReached).
3734 pp_expr_fields2([],_) --> !.
3735 pp_expr_fields2([field(Name,Expr)|Rest],LimitReached) -->
3736 ppatom_opt_scramble(Name),":",
3737 pp_expr_m(Expr,116,LimitReached),
3738 pp_expr_fields3(Rest,LimitReached).
3739 pp_expr_fields3([],_) --> !.
3740 pp_expr_fields3(Rest,LimitReached) -->
3741 ",",pp_expr_fields2(Rest,LimitReached).
3742
3743 % TO DO: test more fully; identifiers seem to be wrapped in brackets
3744 pp_expr_let_exists(Ids,Exprs,P,LimitReached) -->
3745 exists_symbol,
3746 ({animation_minor_mode(eventb)} -> % otherwise we get strange characters in Rodin, no (.) allowed in Rodin
3747 pp_expr_l_pair_in_mode(Ids,LimitReached),
3748 ".("
3749 ; " /* LET */ (",
3750 pp_expr_l_pair_in_mode(Ids,LimitReached),
3751 ").("
3752 ),
3753 pp_expr_let_pred_exprs(Ids,Exprs,LimitReached),
3754 " ",and_symbol," ", pp_expr_m(P,5,LimitReached), ")".
3755
3756 pp_expr_let_pred_exprs([],[],_) --> !.
3757 pp_expr_let_pred_exprs([Id|Irest],[Expr|Erest],LimitReached) -->
3758 " ",pp_expr_let_id(Id,LimitReached),
3759 "=",pp_expr_m(Expr,400,LimitReached),
3760 ( {Irest=[]} -> [] ; " ", and_symbol),
3761 pp_expr_let_pred_exprs(Irest,Erest,LimitReached).
3762
3763 % print a LET expression (no B syntax, used in translated Z
3764 % models)
3765 pp_expr_let(Ids,Exprs,P,LimitReached) -->
3766 "LET ", pp_expr_ids_in_mode(Ids,LimitReached),
3767 " BE ", pp_expr_let_pred_exprs(Ids,Exprs,LimitReached),
3768 " IN ",pp_expr_m(P,5,LimitReached),
3769 " END".
3770
3771 pp_expr_let_id(ID,LimitReached) --> {atomic(ID),!, print(unwrapped_let_id(ID)),nl},
3772 pp_expr_m(identifier(ID),500,LimitReached).
3773 pp_expr_let_id(ID,LimitReached) --> pp_expr_m(ID,500,LimitReached).
3774
3775 % print a list of identifiers
3776 pp_expr_ids_in_mode([],_) --> !.
3777 pp_expr_ids_in_mode(Ids,LimitReached) --> {animation_minor_mode(eventb) ; Ids=[_]},!,
3778 pp_expr_l(Ids,LimitReached). % no (.) allowed in Event-B; not necessary in B if only one id
3779 pp_expr_ids_in_mode(Ids,LimitReached) --> "(",pp_expr_l(Ids,LimitReached),")".
3780 pp_expr_ids([],_) --> !.
3781 pp_expr_ids(Ids,LimitReached) -->
3782 % ( {Ids=[Id]} -> pp_expr_m(Id,221)
3783 % ; {otherwise} ->
3784 "(",pp_expr_l(Ids,LimitReached),")".
3785
3786
3787 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3788 % pretty print types for error messages
3789
3790 pretty_type(Type,String) :-
3791 pretty_type_l([Type],[String]).
3792
3793 pretty_type_l(Types,Strings) :-
3794 extract_vartype_names(Types,N),
3795 pretty_type2_l(Types,N,Strings).
3796 pretty_type2_l([],_,[]).
3797 pretty_type2_l([T|TRest],Names,[S|SRest]) :-
3798 pretty_type2(T,Names,noparen,S),
3799 pretty_type2_l(TRest,Names,SRest).
3800
3801 :- if(current_prolog_flag(dialect,sicstus)).
3802 :- if((current_prolog_flag(version_data,sicstus(4,X,_,_,_)),X<3)).
3803 :- use_module(library(terms),[term_variables/2]). % is built-in in SICSTUS 4.3
3804 :- endif.
3805 :- endif.
3806 extract_vartype_names(Types,names(Variables,Names)) :-
3807 term_variables(Types,Variables),
3808 name_variables(Variables,1,Names).
3809
3810 pretty_type2(X,names(Vars,Names),_,Name) :- var(X),!,exact_member_lookup(X,Name,Vars,Names).
3811 pretty_type2(any,_,_,'?').
3812 pretty_type2(set(T),N,_,Text) :- nonvar(T),T=couple(A,B),!,
3813 pretty_type2(A,N,paren,AT), pretty_type2(B,N,paren,BT),
3814 ajoin(['(',AT,'<->',BT,')'],Text).
3815 pretty_type2(set(T),N,_,Text) :-
3816 pretty_type2(T,N,noparen,TT), ajoin(['POW(',TT,')'],Text).
3817 pretty_type2(seq(T),N,_,Text) :-
3818 pretty_type2(T,N,noparen,TT), ajoin(['seq(',TT,')'],Text).
3819 pretty_type2(couple(A,B),N,Paren,Text) :-
3820 pretty_type2(A,N,paren,AT),pretty_type2(B,N,paren,BT),
3821 ajoin([AT,'*',BT],Prod),
3822 ( Paren == noparen ->
3823 Text = Prod
3824 ; otherwise ->
3825 ajoin(['(',Prod,')'],Text)).
3826 pretty_type2(string,_,_,'STRING').
3827 pretty_type2(integer,_,_,'INTEGER').
3828 pretty_type2(boolean,_,_,'BOOL').
3829 pretty_type2(global(G),_,_,A) :- ajoin([G],A).
3830 pretty_type2(freetype(Id),N,_,A) :- pretty_freetype2(Id,N,A).
3831 pretty_type2(pred,_,_,predicate).
3832 pretty_type2(subst,_,_,substitution).
3833 pretty_type2(constant(List),_N,_,A) :- ajoin_with_sep(List,',',P), ajoin(['{',P,'}'],A).
3834 pretty_type2(record(Fields),N,_,Text) :-
3835 pretty_type_fields(Fields,N,FText),
3836 ajoin(['struct(',FText,')'],Text).
3837 pretty_type2(op(Params,Results),N,_,Text) :-
3838 pretty_type_l(Params,N,PText),
3839 ( nonvar(Results),Results=[] ->
3840 ajoin(['operation(',PText,')'],Text)
3841 ; otherwise ->
3842 pretty_type_l(Results,N,RText),
3843 ajoin([RText,'<--operation(',PText,')'],Text) ).
3844 pretty_type2(definition(DefType,_,_),_,_,DefType).
3845 pretty_type2(witness,_,_,witness).
3846 pretty_type_l(L,_,'...') :- var(L),!.
3847 pretty_type_l([],_,'') :- !.
3848 pretty_type_l([E|Rest],N,Text) :-
3849 pretty_type2(E,N,noparen,EText),
3850 ( nonvar(Rest),Rest=[] ->
3851 EText=Text
3852 ; otherwise ->
3853 pretty_type_l(Rest,N,RText),
3854 ajoin([EText,',',RText],Text)).
3855
3856 pretty_type_fields(L,_,'...') :- var(L),!.
3857 pretty_type_fields([],_,'').
3858 pretty_type_fields([field(Name,Type)|FRest],N,Text) :-
3859 pretty_type2(Type,N,noparen,TText),
3860 ptf_seperator(FRest,Sep),
3861 pretty_type_fields(FRest,N,RestText),
3862 opt_scramble_id(Name,ScrName),
3863 ajoin([ScrName,':',TText,Sep,RestText],Text).
3864 ptf_seperator(L,', ') :- var(L),!.
3865 ptf_seperator([],'') :- !.
3866 ptf_seperator(_,', ').
3867
3868 pretty_freetype(Id,A) :-
3869 extract_vartype_names(Id,N),
3870 pretty_freetype2(Id,N,A).
3871 pretty_freetype2(Id,_,A) :- var(Id),!,A='_'.
3872 pretty_freetype2(Id,_,A) :- atomic(Id),!,Id=A.
3873 pretty_freetype2(Id,N,A) :-
3874 Id=..[Name|TypeArgs],
3875 pretty_type2_l(TypeArgs,N,PArgs),
3876 ajoin_with_sep(PArgs,',',P),
3877 ajoin([Name,'(',P,')'],A).
3878
3879 name_variables([],_,[]).
3880 name_variables([_|VRest],Index,[Name|NRest]) :-
3881 ( nth1(Index,"ABCDEFGHIJKLMNOPQRSTUVWXYZ",C) -> SName = [C]
3882 ; otherwise -> number_codes(Index,SName)),
3883 append("_",SName,CName),atom_codes(Name,CName),
3884 Next is Index+1,
3885 name_variables(VRest,Next,NRest).
3886
3887 ppatom(Var) --> {var(Var)},!, ppatom('$VARIABLE').
3888 ppatom(Cmp) --> {compound(Cmp)},!, ppatom('$COMPOUND_TERM').
3889 ppatom(Atom) --> {safe_atom_codes(Atom,Codes)}, ppcodes(Codes).
3890
3891 ppnumber(Number) --> {var(Number)},!,pp_clpfd_variable(Number).
3892 ppnumber(inf) --> !,"inf".
3893 ppnumber(minus_inf) --> !,"minus_inf".
3894 ppnumber(Number) --> {number(Number),number_codes(Number,Codes)},!, ppcodes(Codes).
3895 ppnumber(Number) --> {add_internal_error('Not a number: ',ppnumber(Number,_,_)),fail}.
3896
3897 pp_numberedvar(N) --> "_",ppnumber(N),"_".
3898
3899 pp_clpfd_variable(X) --> "?:",{fd_dom(X,Dom)},write_to_codes(Dom), pp_frozen_info(X).
3900
3901 pp_frozen_info(_X) --> {get_preference(translate_print_frozen_infos,false)},!,[].
3902 pp_frozen_info(X) -->
3903 ":(",{frozen(X,Goal)},
3904 write_goal_with_max_depth(Goal),
3905 ")".
3906
3907 write_goal_with_max_depth((A,B)) --> !, "(",write_goal_with_max_depth(A),
3908 ", ", write_goal_with_max_depth(B), ")".
3909 write_goal_with_max_depth(Term) --> write_with_max_depth(3,Term).
3910
3911 write_with_max_depth(Depth,Term,S1,S2) :- write_term_to_codes(Term,S1,S2,[max_depth(Depth)]).
3912
3913 ppterm(Term) --> write_to_codes(Term).
3914 ppcodes([],S,S).
3915 ppcodes([C|Rest],[C|In],Out) :- ppcodes(Rest,In,Out).
3916
3917 % for debugging:
3918 :- public b_portray_hook/1.
3919 b_portray_hook(X) :-
3920 ground(X),
3921 (is_texpr(X) -> print('{# '),print_bexpr_or_subst(X),print(' #}')).
3922
3923 install_b_portray_hook :- % mainly for the Prolog debugger
3924 assert(( user:portray(X) :- translate:b_portray_hook(X) )).
3925 remove_b_portray_hook :-
3926 retractall( user:portray(_) ).
3927
3928
3929 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3930 % Pretty-print of Event-B models as classical B
3931
3932 translate_eventb_to_classicalb(EBMachine,AddInfo,Rep) :-
3933 ( conversion_check(EBMachine) ->
3934 convert_eventb_classicalb(EBMachine,CBMachine),
3935 call_cleanup(( set_animation_mode(b), % clear minor mode "eventb"
3936 translate_machine(CBMachine,Rep,AddInfo),!),
3937 set_animation_minor_mode(eventb))
3938 ; \+ animation_minor_mode(eventb) -> add_error(translate,'Conversion only applicable to Event-B models')
3939 ; otherwise ->
3940 add_error_and_fail(translate,'Conversion not applicable, check if you limited the number of abstract level to 0')
3941 ).
3942
3943 convert_eventb_classicalb(EBMachine,CBMachine) :-
3944 select_section(operation_bodies,In,Out,EBMachine,CBMachine1),
3945 maplist(convert_eventop,In,Out),
3946 select_section(initialisation,IIn,IOut,CBMachine1,CBMachine),
3947 convert_event(IIn,[],IOut).
3948 convert_eventop(EBOp,CBOp) :-
3949 get_texpr_expr(EBOp,operation(Id,[],Args,EBBody)),
3950 get_texpr_info(EBOp,Info),
3951 convert_event(EBBody,Args,CBBody),
3952 % Remove the arguments
3953 create_texpr(operation(Id,[],[],CBBody),op([],[]),Info,CBOp).
3954 convert_event(TEvent,Parameters,TSubstitution) :-
3955 get_texpr_expr(TEvent,rlevent(_Id,_Section,_Status,_Parameters,Guard,_Theorems,Actions,_VariableWitnesses,_ParameterWitnesses,_Ums,_Refined)),
3956 in_parallel(Actions,PAction),
3957 convert_event2(Parameters,Guard,PAction,TSubstitution).
3958 convert_event2([],Guard,Action,Action) :-
3959 is_truth(Guard),!.
3960 convert_event2([],Guard,Action,Select) :-
3961 !,create_texpr(select([When]),subst,[],Select),
3962 create_texpr(select_when(Guard,Action),subst,[],When).
3963 convert_event2(Parameters,Guard,Action,Any) :-
3964 create_texpr(any(Parameters,Guard,Action),subst,[],Any).
3965 in_parallel([],Skip) :- !,create_texpr(skip,subst,[],Skip).
3966 in_parallel([A],A) :- !.
3967 in_parallel(Actions,Parallel) :- create_texpr(parallel(Actions),subst,[],Parallel).
3968
3969 conversion_check(Machine) :-
3970 animation_mode(b),
3971 animation_minor_mode(eventb),
3972 get_section(initialisation,Machine,Init),
3973 get_texpr_expr(Init,rlevent(_Id,_Sec,_St,_Par,_Grd,_Thms,_Act,_VW,_PW,_Ums,[])).
3974
3975 % ------------------------------------------------------------
3976
3977 % divide a B typed expression into columns for CSV export or Table viewing of its values
3978 get_bexpression_column_template(b(couple(A,B),_,_),(AVal,BVal),ColHeaders,Columns) :- !,
3979 get_bexpression_column_template(A,AVal,AHeaders,AColumns),
3980 get_bexpression_column_template(B,BVal,BHeaders,BColumns),
3981 append(AHeaders,BHeaders,ColHeaders),
3982 append(AColumns,BColumns,Columns).
3983 get_bexpression_column_template(TypedExpr,Value,[ColHeader],[Value]) :-
3984 translate:translate_bexpression_with_limit(TypedExpr,100,ColHeader).
3985
3986
3987 :- use_module(gensym,[gensym/2]).
3988 gen_fresh_id_if_necessary(Default,Expr,FreshID) :-
3989 occurs_in_expr(Default,Expr),!,
3990 gensym('__FRESH_ID__',FreshID). % assumes _Fresh_XXX not used
3991 gen_fresh_id_if_necessary(Default,_,Default).
3992
3993
3994 % a version of member that creates an error when info list not instantiated
3995 member_in_info(X,T) :- var(T),!, add_internal_error('Illegal info field:', member_in_info(X,T)),fail.
3996 member_in_info(X,[X|_]).
3997 ?member_in_info(X,[_|T]) :- member_in_info(X,T).
3998
3999 memberchk_in_info(X,T) :- var(T),!, add_internal_error('Illegal info field:', memberchk_in_info(X,T)),fail.
4000 memberchk_in_info(X,[X|_]) :- !.
4001 memberchk_in_info(X,[_|T]) :- memberchk_in_info(X,T).
4002
4003 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4004
4005 :- use_module(library(clpfd)).
4006
4007 % print also partially instantiated variables with CLP(FD) Info
4008 print_value_variable(X) :- var(X), !, print(X).
4009 print_value_variable(int(X)) :- print('int('), print_clpfd_variable(X), print(')').
4010 print_value_variable(fd(X,T)) :- print('fd('), print_clpfd_variable(X), print(','), print(T),print(')').
4011 print_value_variable(X) :- print(X).
4012
4013 print_clpfd_variable(X) :- var(X),!,print(X), print(':'), fd_dom(X,Dom), print(Dom), print_frozen_info(X).
4014 print_clpfd_variable(X) :- print(X).
4015
4016 %print_clpfd_variables([]).
4017 %print_clpfd_variables([H|T]) :- print('CLPFD: '),print_clpfd_variable(H), nl, print_clpfd_variables(T).
4018
4019
4020 :- public l_print_frozen_info/1.
4021 l_print_frozen_info([]).
4022 l_print_frozen_info([H|T]) :- print(H), print(' '),
4023 (var(H) -> print_frozen_info(H) ;
4024 H=fd_var(V,_) -> print_frozen_info(V) ; true), l_print_frozen_info(T).
4025
4026 print_frozen_info(X) :- frozen(X,Goal), print_frozen_goal(Goal).
4027 print_frozen_goal((A,B)) :- !, print_frozen_goal(A), print(','), print_frozen_goal(B).
4028 print_frozen_goal(prolog:trig_nondif(_A,_B,R,_S)) :- !, frozen(R,G2), print_frozen_goal2(G2).
4029 print_frozen_goal(G) :- print_frozen_goal2(G).
4030 print_frozen_goal2(V) :- var(V),!, print(V).
4031 print_frozen_goal2(true) :- !.
4032 print_frozen_goal2((A,B)) :- !, print_frozen_goal2(A), print(','), print_frozen_goal2(B).
4033 print_frozen_goal2(G) :- print(' :: '), tools_printing:print_term_summary(G).
4034
4035
4036 /* Event-B operators */
4037 translate_eventb_operators([]) --> !.
4038 translate_eventb_operators([Name-Call|Rest]) -->
4039 translate_eventb_operator(Call,Name),
4040 translate_eventb_operators(Rest).
4041
4042 translate_eventb_operator(Module:Call,Name) -->
4043 insertcodes("\n "),
4044 indention_codes(In,Out),
4045 {Call =.. [Functor|Args],atom_concat('pp_',Functor,PPFunctor),
4046 PPCall =.. [PPFunctor|Args],
4047 catch( (call(Module:PPCall,Name,In,Out) -> R=ok; R=fail),
4048 error(_,_),
4049 R=error),
4050 ( R = ok -> true
4051 ; otherwise ->
4052 print_operator_failure(Name,Module,Functor,In,Out))}.
4053 print_operator_failure(Name,Module,Functor) -->
4054 ppterm(Name),
4055 ppcodes(": Operator implemented by "),
4056 ppatom(Module),ppcodes(":"),ppatom(Functor).
4057
4058 % ---------------------------------------
4059
4060 % translate a predicate into B machine for manipulation
4061 translate_predicate_into_machine(Pred,ResultAtom) :-
4062 bsyntaxtree:find_typed_identifier_uses(Pred, TUsedIds),
4063 get_texpr_ids(TUsedIds,UsedIds), print(used(UsedIds)),nl,
4064 add_typing_predicates(TUsedIds,Pred,TPred),
4065 set_print_type_infos(all),
4066 specfile:set_animation_mode(b), % clear eventb minor mode; to do: set back
4067 translate_bexpression(TPred,PredAtom), %print(res(UsedIds,ResultAtom)),nl,
4068 set_print_type_infos(none),
4069 ajoin_with_sep(UsedIds,', ',AllIds),
4070 bmachine:get_full_b_machine(_Name,BMachine),
4071 include(relevant_section,BMachine,RelevantSections),
4072 % TO DO: we could filter out enumerate/deferred sets not occuring in Pred
4073 translate_section_list(RelevantSections,SetsParas),
4074 atom_codes(ASP,SetsParas),
4075 ajoin(['MACHINE UnsatCore',ASP,'CONSTANTS ',AllIds,'\nPROPERTIES\n ',PredAtom,'\nEND\n'],ResultAtom).
4076
4077 relevant_section(deferred_sets/_).
4078 relevant_section(enumerated_elements/_).
4079 relevant_section(parameters/_).
4080
4081 % ---------------------------------------