1 % (c) 2016-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_keywords,[classical_b_keyword/1, translate_keyword_id/2,
6 raw_backtranslate_keyword_ids/2,
7 % info about translated identifiers when pretty-printing Event-B to classical B:
8 keyword_to_id_cache/2, id_to_keyword_cache/2]).
9
10
11 :- use_module(module_information).
12 :- module_info(group,tools).
13 :- module_info(description,'This module is responsible for translating identifiers which happen to be keywords').
14
15 :- use_module(library(lists)).
16
17 % info about translated identifiers when pretty-printing Event-B to classical B:
18 :- dynamic keyword_to_id_cache/2, id_to_keyword_cache/2.
19
20 :- use_module(eventhandling,[register_event_listener/3]).
21 :- register_event_listener(clear_specification,reset_translate_keywords,
22 'Reset Keyword Translation.').
23 reset_translate_keywords :-
24 retractall(keyword_to_id_cache(_,_)),
25 retractall(id_to_keyword_cache(_,_)).
26
27
28 % translate a keyword
29 translate_keyword_id(ID,R) :- keyword_to_id_cache(ID,TID),!, R=TID.
30 translate_keyword_id(ID,R) :-
31 atom_concat(ID,'__',R), % TO DO: gensym with assert
32 assert(keyword_to_id_cache(ID,R)),
33 assert(id_to_keyword_cache(R,ID)). % store that if an external tool gives us infos using ids we can translate back
34
35 :- meta_predicate map_over(2,*,*).
36 :- meta_predicate map_over_raw_expr(*,2,*).
37 % conjunct(pos(2,-1,1,1,1,44),conjunct(pos(3,-1,1,1,1,26),equal(pos(4,-1,1,1,1,13),identifier(pos(5,-1,1,1,1,6),left__),boolean_true(pos(6,-1,1,10,1,13))),equal(pos(7,-1,1,17,1,26),identifier(pos(8,-1,1,17,1,21),rel__),empty_set(pos(9,-1,1,25,1,26)))),equal(pos(10,-1,1,30,1,44),identifier(pos(11,-1,1,30,1,36),right__),boolean_false(pos(12,-1,1,40,1,44))))
38 raw_backtranslate_keyword_ids(RawExpr,Res) :- \+ keyword_to_id_cache(_,_),!, Res=RawExpr.
39 raw_backtranslate_keyword_ids(RawExpr,Res) :- map_over_raw_expr(RawExpr,backtranslate_id,Res).
40
41 backtranslate_id(identifier(Pos,ID),identifier(Pos,NewID)) :-
42 (id_to_keyword_cache(ID,KeywordID) -> NewID=KeywordID ; NewID = ID).
43
44 map_over(P,RawExpr,Res) :- map_over_raw_expr(RawExpr,P,Res).
45 map_over_raw_expr(RawExpr,P,Res) :- call(P,RawExpr,NewRawExpr),!,
46 Res=NewRawExpr.
47 map_over_raw_expr(conjunct(Pos,A,B),P,conjunct(Pos,MA,MB)) :- !,
48 map_over_raw_expr(A,P,MA),
49 map_over_raw_expr(B,P,MB).
50 map_over_raw_expr(disjunct(Pos,A,B),P,disjunct(Pos,MA,MB)) :- !,
51 map_over_raw_expr(A,P,MA),
52 map_over_raw_expr(B,P,MB).
53 map_over_raw_expr(equal(Pos,A,B),P,equal(Pos,MA,MB)) :- !,
54 map_over_raw_expr(A,P,MA),
55 map_over_raw_expr(B,P,MB).
56 map_over_raw_expr(A,_,R) :- atomic(A),!,R=A.
57 map_over_raw_expr(F,P,MF) :- F =.. [Functor,Pos|Args],
58 maplist(map_over(P),Args,NewArgs),
59 MF =.. [Functor,Pos|NewArgs].
60
61 classical_b_keyword('FIN').
62 classical_b_keyword('FIN1').
63 classical_b_keyword('POW').
64 classical_b_keyword('POW1').
65 %classical_b_keyword('__first_of_pair').
66 %classical_b_keyword('__second_of_pair').
67 classical_b_keyword(arity).
68 classical_b_keyword(bin).
69 classical_b_keyword(bool).
70 classical_b_keyword(btree).
71 classical_b_keyword(card).
72 classical_b_keyword(closure).
73 classical_b_keyword(closure1).
74 classical_b_keyword(conc).
75 classical_b_keyword(const).
76 classical_b_keyword(dom).
77 classical_b_keyword(father).
78 classical_b_keyword(finite).
79 classical_b_keyword(first).
80 classical_b_keyword(fnc).
81 classical_b_keyword(front).
82 classical_b_keyword(id).
83 classical_b_keyword(infix).
84 classical_b_keyword(inter).
85 classical_b_keyword(iseq).
86 classical_b_keyword(iseq1).
87 classical_b_keyword(items).
88 classical_b_keyword(iterate).
89 classical_b_keyword(last).
90 classical_b_keyword(left).
91 classical_b_keyword(max).
92 classical_b_keyword(min).
93 classical_b_keyword(mirror).
94 classical_b_keyword(not).
95 classical_b_keyword(perm).
96 classical_b_keyword(postfix).
97 classical_b_keyword(pred).
98 classical_b_keyword(prefix).
99 classical_b_keyword(prj1).
100 classical_b_keyword(prj2).
101 classical_b_keyword(ran).
102 classical_b_keyword(rank).
103 classical_b_keyword(rel).
104 classical_b_keyword(rev).
105 classical_b_keyword(right).
106 classical_b_keyword(seq).
107 classical_b_keyword(seq1).
108 classical_b_keyword(size).
109 classical_b_keyword(sizet).
110 classical_b_keyword(son).
111 classical_b_keyword(sons).
112 classical_b_keyword(subtree).
113 classical_b_keyword(succ).
114 classical_b_keyword(tail).
115 classical_b_keyword(top).
116 classical_b_keyword(tree).
117 classical_b_keyword(union).
118 % facts above can be generated by:
119 % findall(ID,translate:function_like(_,ID),L),sort(L,SL), member(ID,SL), portray_clause(classical_b_keyword(ID)),fail.
120
121 classical_b_keyword('BOOL').
122 classical_b_keyword('FALSE').
123 classical_b_keyword('MAXINT').
124 classical_b_keyword('MININT').
125 classical_b_keyword('STRING').
126 classical_b_keyword('TRUE').
127 % facts above can be generated by:
128 % findall(ID,translate:constants(_,ID),L),sort(L,SL), member(ID,SL), portray_clause(classical_b_keyword(ID)),fail.
129
130 classical_b_keyword('INT').
131 classical_b_keyword('INTEGER').
132 classical_b_keyword('NAT').
133 classical_b_keyword('NAT1').
134 classical_b_keyword('NATURAL').
135 classical_b_keyword('NATURAL1').
136 % facts above can be generated by:
137 % findall(ID,(translate:eventb_integer_mapping(A,B),(ID=A;ID=B)),L),sort(L,SL), member(ID,SL), portray_clause(classical_b_keyword(ID)),fail.
138
139 % quantified operators:
140 classical_b_keyword('INTER').
141 classical_b_keyword('PI').
142 classical_b_keyword('SIGMA').
143 classical_b_keyword('UNION').
144
145 % additional substitution/structuring keywords
146 classical_b_keyword('ABSTRACT_CONSTANTS').
147 classical_b_keyword('ABSTRACT_VARIABLES').
148 classical_b_keyword('ANY').
149 classical_b_keyword('ASSERT').
150 classical_b_keyword('ASSERTIONS').
151 classical_b_keyword('BE').
152 classical_b_keyword('BEGIN').
153 classical_b_keyword('CASE').
154 classical_b_keyword('CHOICE').
155 classical_b_keyword('CONCRETE_CONSTANTS').
156 classical_b_keyword('CONCRETE_VARIABLES').
157 classical_b_keyword('CONSTANTS').
158 classical_b_keyword('CONSTRAINTS').
159 classical_b_keyword('DEFINITIONS').
160 classical_b_keyword('DO').
161 classical_b_keyword('EITHER').
162 classical_b_keyword('ELSE').
163 classical_b_keyword('ELSIF').
164 classical_b_keyword('END').
165 classical_b_keyword('EVENT').
166 classical_b_keyword('EXTENDS').
167 classical_b_keyword('IF').
168 classical_b_keyword('IMPLEMENTATION').
169 classical_b_keyword('IMPORTS').
170 classical_b_keyword('IN').
171 classical_b_keyword('INCLUDES').
172 classical_b_keyword('INITIALISATION').
173 classical_b_keyword('INITIALIZATION').
174 classical_b_keyword('INVARIANT').
175 classical_b_keyword('LET').
176 classical_b_keyword('LOCAL_OPERATIONS').
177 classical_b_keyword('MACHINE').
178 classical_b_keyword('MODEL').
179 classical_b_keyword('OF').
180 classical_b_keyword('OPERATIONS').
181 classical_b_keyword('OR').
182 classical_b_keyword('PRE').
183 classical_b_keyword('PROMOTES').
184 classical_b_keyword('PROPERTIES').
185 classical_b_keyword('REFINEMENT').
186 classical_b_keyword('REFINES').
187 classical_b_keyword('SEES').
188 classical_b_keyword('SELECT').
189 classical_b_keyword('SETS').
190 classical_b_keyword('skip').
191 classical_b_keyword('SYSTEM').
192 classical_b_keyword('THEN').
193 classical_b_keyword('USES').
194 classical_b_keyword('VALUES').
195 classical_b_keyword('VARIABLES').
196 classical_b_keyword('VARIANT').
197 classical_b_keyword('WHERE').
198 classical_b_keyword('WHILE').
199 classical_b_keyword('WITH').
200