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