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 | | % --------------------------------------- |