1 % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(input_syntax_tree, [remove_raw_position_info/2
6 ,get_raw_position_info/2
7 ,try_get_raw_position_info/2 % same but without checks
8 ,extract_raw_identifiers/2
9 ,get_definition_name/2
10 ,raw_replace/3
11 ,raw_conjunct/2
12 ,create_fresh_identifier/3
13 ,map_over_raw_expr/3
14 ]).
15
16 :- use_module(module_information,[module_info/2]).
17 :- module_info(group,typechecker).
18 :- module_info(description,'Utilities on the raw AST.').
19
20 :- meta_predicate map_over(2,*,*).
21 :- meta_predicate map_over_raw_expr(*,2,*).
22
23 :- use_module(error_manager).
24 :- use_module(probsrc(tools_strings),[ajoin/2]).
25 :- use_module(tools_positions, [is_position/1]).
26 :- use_module(tools,[safe_functor/4]).
27 :- use_module(translate,[translate_raw_bexpr_with_limit/3]).
28
29 get_raw_position_info(Compound,Info) :-
30 try_get_raw_position_info(Compound,Info),
31 is_position(Info),!.
32 get_raw_position_info(Compound,Info) :-
33 add_internal_error('Could not get position info: ',get_raw_position_info(Compound,Info)),
34 Info = unknown.
35
36 try_get_raw_position_info(Compound,Info) :-
37 compound(Compound),
38 functor(Compound,_,Arity), Arity>0,
39 arg(1,Compound,Info).
40
41
42 remove_raw_position_info([],Output) :- !,Output=[].
43 remove_raw_position_info([I|Irest],[O|Orest]) :-
44 !,remove_raw_position_info(I,O),
45 remove_raw_position_info(Irest,Orest).
46 remove_raw_position_info(Input,Output) :-
47 compound(Input),functor(Input,Functor,Arity),Arity>0,!,
48 Arity2 is Arity-1,
49 functor(Output,Functor,Arity2),
50 remove_raw_position_info2(1,Arity,Input,Output).
51 remove_raw_position_info(Input,Input).
52
53
54 remove_raw_position_info2(Pos,Arity,Input,Output) :-
55 Pos < Arity,!,Pos2 is Pos+1,
56 arg(Pos2,Input,IA), arg(Pos,Output,OA),
57 remove_raw_position_info(IA,OA),
58 remove_raw_position_info2(Pos2,Arity,Input,Output).
59 remove_raw_position_info2(_Pos,_Arity,_Input,_Output).
60
61 :- use_module(library(ordsets),[ord_union/3, ord_member/2]).
62 extract_raw_identifiers(Ast,Ids) :-
63 extract_raw_identifiers2(Ast,[],Unsorted,[]),
64 sort(Unsorted,Ids).
65 extract_raw_identifiers2([],_) --> !,[].
66 extract_raw_identifiers2([I|Irest],Bound) -->
67 !,extract_raw_identifiers2(I,Bound),
68 extract_raw_identifiers2(Irest,Bound).
69 extract_raw_identifiers2(identifier(_,I),Bound) --> !,add_if_free(I,Bound).
70 extract_raw_identifiers2(definition(_,I,Args),Bound) --> !,
71 add_if_free(I,Bound),
72 extract_raw_identifiers2(Args,Bound). % Note: we do not see the Ids inside the definition body!
73 extract_raw_identifiers2(Input,Bound) -->
74 {raw_quantifier(Input,Ids,Subs)},!,
75 %{append(Ids,Bound,NewBound)},
76 {sort(Ids,SIds),ord_union(SIds,Bound,NewBound)},
77 extract_raw_identifiers2(Subs,NewBound).
78 extract_raw_identifiers2(Input,Bound) -->
79 {compound(Input),functor(Input,_Functor,Arity),Arity>1,!},
80 extract_raw_identifiers3(2,Arity,Input,Bound).
81 extract_raw_identifiers2(_,_) --> [].
82
83 add_if_free(Id,Bound,In,Out) :-
84 %(ordsets:is_ordset(Bound) -> true ; add_internal_error('Not ordset: ',add_if_free(Id,Bound))),
85 (ord_member(Id,Bound) -> In=Out ; In=[Id|Out]).
86
87 extract_raw_identifiers3(Pos,Arity,Input,Bound) -->
88 {Pos=<Arity,!,Pos2 is Pos+1, arg(Pos,Input,Arg)},
89 extract_raw_identifiers2(Arg,Bound),
90 extract_raw_identifiers3(Pos2,Arity,Input,Bound).
91 extract_raw_identifiers3(_Pos,_Arity,_Input,_Bound) --> [].
92
93 :- use_module(library(lists),[maplist/3]).
94 raw_quantifier(Expr,SortedIds,Subs) :-
95 raw_quantifier_aux(Expr,RawIds,Subs),
96 maplist(raw_id,RawIds,Ids),
97 sort(Ids,SortedIds).
98 raw_id(identifier(_,ID),ID).
99
100 raw_quantifier_aux(forall(_,Ids,P),Ids,[P]).
101 raw_quantifier_aux(exists(_,Ids,P),Ids,[P]).
102 raw_quantifier_aux(comprehension_set(_,Ids,P),Ids,[P]).
103 raw_quantifier_aux(event_b_comprehension_set(_,Ids,E,P),Ids,[E,P]).
104 raw_quantifier_aux(lambda(_,Ids,P,E),Ids,[P,E]).
105 raw_quantifier_aux(general_sum(_,Ids,P,E),Ids,[P,E]).
106 raw_quantifier_aux(general_product(_,Ids,P,E),Ids,[P,E]).
107 raw_quantifier_aux(quantified_union(_,Ids,P,E),Ids,[P,E]).
108 raw_quantifier_aux(quantified_intersection(_,Ids,P,E),Ids,[P,E]).
109 raw_quantifier_aux(any(_,Ids,P,S),Ids,[P,S]).
110 raw_quantifier_aux(let(_,Ids,P,S),Ids,[P,S]).
111 raw_quantifier_aux(var(_,Ids,S),Ids,[S]).
112 raw_quantifier_aux(recursive_let(_,Id,E),[Id],[E]).
113
114 get_definition_name(expression_definition(_Pos,Name,_Args,_Body),Name).
115 get_definition_name(predicate_definition(_Pos,Name,_Args,_Body),Name).
116 get_definition_name(substitution_definition(_Pos,Name,_Args,_Body),Name).
117
118 :- use_module(parsercall, [transform_string_template/3]).
119
120 % raw_replace(+InputAST,-Replaces,+OutputAST):
121 % InputAST: A raw AST as it comes from the parser (without type information)
122 % Replaces: A list of "replace(Id,Expr)" where Id the the identifier which
123 % should be replaced by the expression Expr
124 % OutputAST: A raw AST where all matching identifiers are replaced by their
125 % expression
126 % used for rewriting DEFINITION calls
127 raw_replace(Expr,[],Expr) :- !.
128 raw_replace(Old,Replaces,New) :-
129 get_introduced_ids(Replaces,IntroducedIds), %print(intro(IntroducedIds)),nl,
130 raw_replace2(Old,Replaces,IntroducedIds,New).
131 raw_replace2([],_,_,[]) :- !.
132 raw_replace2([E|Rest],Replaces,IntroducedIds,[N|NRest]) :- !,
133 raw_replace2(E,Replaces,IntroducedIds,N),
134 raw_replace2(Rest,Replaces,IntroducedIds,NRest).
135 raw_replace2(rewrite_protected(X),_Replaces,_,rewrite_protected(Y)) :- !,X=Y.
136 raw_replace2(becomes_such(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_such(Pos,NVars,NCond)) :- !,
137 raw_replace2(Cond,Replaces,IntroducedIds,NCond),
138 raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).
139 raw_replace2(becomes_element_of(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_element_of(Pos,NVars,NCond)) :- !,
140 raw_replace2(Cond,Replaces,IntroducedIds,NCond),
141 raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).
142 % TODO: support more raw AST nodes with identifier lists
143 raw_replace2(identifier(Pos,Old),Replaces,_,New) :- !,
144 (memberchk(replace(Old,New),Replaces) -> true ; New=identifier(Pos,Old)).
145 raw_replace2(record_field(RPos,Record,Field),Replaces,IntroducedIds,record_field(RPos,NRecord,NField)) :- !,
146 raw_replace2(Record,Replaces,IntroducedIds,NRecord),
147 (Field=identifier(_,FieldName),
148 raw_replace2(Field,Replaces,IntroducedIds,NField)
149 -> (NField=identifier(_,NewFieldName)
150 -> (NewFieldName=FieldName -> true
151 ; ajoin(['Rewriting field name ',FieldName,' during definition expansion to: '],Msg),
152 add_message(definition_rewrite,Msg,NewFieldName,RPos)
153 )
154 ; translate_raw_bexpr_with_limit(NField,50,FS),
155 ajoin(['Rewriting field name ',FieldName,' to an illegal expression: '],Msg),
156 (try_get_raw_position_info(NField,NFPos) -> true ; NFPos=RPos),
157 add_warning(definition_rewrite,Msg,FS,NFPos)
158 )
159 ; NField=Field).
160 raw_replace2(multiline_template(Pos,TS),Replaces,Ids,New) :- !, % rewrite template, it may contain expressions with ids
161 transform_string_template(TS,Pos,RawExpr),
162 raw_replace2(RawExpr,Replaces,Ids,New).
163 raw_replace2(Expr,_,IntroducedIds,_) :-
164 quantifier_capture_warning(Expr,IntroducedIds),
165 fail.
166 raw_replace2(X,_Replaces,_,Res) :- simple_expr(X), !,Res=X.
167 raw_replace2(Expr,Replaces,IntroducedIds,New) :-
168 safe_functor(raw_replace2_expr,Expr,Functor,Arity),
169 safe_functor(raw_replace2_new,New,Functor,Arity),
170 raw_replace3(Arity,Expr,Replaces,IntroducedIds,New).
171 raw_replace3(0,_,_,_,_) :- !.
172 raw_replace3(N,Expr,Replaces,IntroducedIds,NExpr) :-
173 arg(N,Expr,Old),
174 arg(N,NExpr,New),
175 raw_replace2(Old,Replaces,IntroducedIds,New),
176 N2 is N-1,
177 raw_replace3(N2,Expr,Replaces,IntroducedIds,NExpr).
178
179 simple_expr(real(_,_)).
180 simple_expr(string(_,_)).
181 simple_expr(integer(_,_)).
182
183
184 % replace a list of identifiers in the orginal AST which should remain a list of identifiers
185 % we allow
186 raw_replace_id_list([],_,_,[]).
187 raw_replace_id_list([identifier(Pos,Old)|T],Replaces,Intro,Res) :- !,
188 (memberchk(replace(Old,New),Replaces)
189 -> (flatten_couple_id_list(New,Res,Tail) -> NT=Tail
190 ; ajoin(['Rewriting identifier ',Old,' to an illegal value during definition expansion: '],Msg),
191 add_warning(definition_rewrite,Msg,New,Pos),
192 Res = [New|NT]
193 )
194 ; Res=[identifier(Pos,Old)|NT]
195 ), raw_replace_id_list(T,Replaces,Intro,NT).
196 raw_replace_id_list([H|T],Replaces,Intro,[H|NT]) :-
197 arg(1,H,Pos),
198 add_warning(definition_rewrite,'Not an identifier in raw AST: ',H,Pos), % should not happen
199 raw_replace_id_list(T,Replaces,Intro,NT).
200
201 % flatten a couple list of identifiers; can happen when we have vars == x,y and pass vars to a definition as argument
202 flatten_couple_id_list(couple(_Pos,List)) --> !,
203 % one could check that in Pos we have a pos_context with definition_call
204 l_flatten_couple_id_list(List).
205 flatten_couple_id_list(OtherVal) --> {OtherVal=identifier(_,_)},[OtherVal].
206
207 l_flatten_couple_id_list([]) --> [].
208 l_flatten_couple_id_list([H|T]) --> !, flatten_couple_id_list(H), l_flatten_couple_id_list(T).
209
210 :- use_module(library(ordsets),[ord_union/2, ord_intersection/3]).
211 % this can happen e.g. for egt(x) == (#y.(y:NAT1 & y<100 & x<y)) when calling egt(y+1), i.e., replacing x by y+1 in body of DEFINITION
212 quantifier_capture_warning(Expr,IntroducedIds) :-
213 raw_quantifier(Expr,SortedIds,_Body),
214 ord_intersection(IntroducedIds,SortedIds,Clash),
215 Clash \= [],
216 % TO DO?: check if we really use a corresponding LHS identifier in Body: extract_raw_identifiers(Body,UsedIds), maplist(get_lhs_id,Replaces,LHSIds),
217 %format('Quantifier ids: ~w~nIntroduced Ids: ~w~n',[SortedIds,IntroducedIds]),
218 arg(1,Expr,Pos),
219 add_warning(definition_variable_capture,'Quantifier may capture identifiers in DEFINITION arguments: ',Clash,Pos).
220
221 % compute which ids are introduced by performing the replacements
222 get_introduced_ids(Replaces,Ids) :- maplist(get_rhs_ids,Replaces,ListOfList),
223 ord_union(ListOfList,Ids).
224 get_rhs_ids(replace(_,New),Ids) :- extract_raw_identifiers(New,Ids).
225 %get_lhs_id(replace(Id,_),Id).
226
227 raw_conjunct([],truth(none)).
228 raw_conjunct([H|T],R) :-
229 ( T=[] -> H=R
230 ;
231 R=conjunct(none,H,RT),
232 raw_conjunct(T,RT)
233 ).
234
235 %raw_occurs(ID,Term) :- raw_id(Term,ID).
236 %raw_occurs(ID,Term) :- compound(Term), Term =.. [_Func,_Pos|Args],
237 % member(A,Args), raw_occurs(ID,A).
238
239
240 % create_fresh_identifier(+PreferredName,+Ast,-Name):
241 % Generates an identifier that does not occur in Ast
242 % PreferredName: An atom with the preferred name of the identifier
243 % Ast: An untyped AST
244 % Name: An identifier (an atom) that does not occur free in AST,
245 % If PreferredName does not occur free in AST, it's 'PreferredName',
246 % otherwise it's 'PreferredName_N' where N is a natural number
247 create_fresh_identifier(PreferredName,Ast,Name) :-
248 extract_raw_identifiers(Ast,UsedIds),
249 ( memberchk(PreferredName,UsedIds) ->
250 % Allready in use, find a fresh one by adding a number
251 atom_codes(PreferredName,PreferredCodes),
252 create_fresh_identifier_aux(PreferredCodes,UsedIds,1,Name)
253 ;
254 Name = PreferredName).
255 create_fresh_identifier_aux(PreferredCodes,UsedIds,I,Name) :-
256 number_codes(I,ICodes),append(PreferredCodes,[95|ICodes],Codes),
257 atom_codes(NewName,Codes),
258 ( memberchk(NewName,UsedIds) ->
259 % Allready in use, try again with a higher number
260 I2 is I+1,
261 create_fresh_identifier_aux(PreferredCodes,UsedIds,I2,Name)
262 ;
263 Name = NewName).
264
265 % map a predicate over the raw AST to transform it
266
267 map_over(P,RawExpr,Res) :- map_over_raw_expr(RawExpr,P,Res).
268
269 map_over_raw_expr(RawExpr,P,Res) :- call(P,RawExpr,NewRawExpr),!,
270 Res=NewRawExpr.
271 map_over_raw_expr(conjunct(Pos,A,B),P,conjunct(Pos,MA,MB)) :- !,
272 map_over_raw_expr(A,P,MA),
273 map_over_raw_expr(B,P,MB).
274 map_over_raw_expr(disjunct(Pos,A,B),P,disjunct(Pos,MA,MB)) :- !,
275 map_over_raw_expr(A,P,MA),
276 map_over_raw_expr(B,P,MB).
277 map_over_raw_expr(equal(Pos,A,B),P,equal(Pos,MA,MB)) :- !,
278 map_over_raw_expr(A,P,MA),
279 map_over_raw_expr(B,P,MB).
280 map_over_raw_expr(A,_,R) :- atomic(A),!,R=A.
281 map_over_raw_expr(A,P,R) :- raw_syntax_traversion(A,Fixed,Args),!,
282 functor(A,F,N), functor(R,F,N),
283 raw_syntax_traversion(R,Fixed,NewArgs),
284 maplist(map_over(P),Args,NewArgs).
285 map_over_raw_expr(F,P,MF) :- F =.. [Functor,Pos|Args], % default: arg1 is position, rest is sub-arguments
286 maplist(map_over(P),Args,NewArgs),
287 MF =.. [Functor,Pos|NewArgs].
288
289 raw_syntax_traversion(conjunct(Pos,List),con(Pos),List). % n-ary conjunct
290 raw_syntax_traversion(disjunct(Pos,List),disj(Pos),List). % n-ary disjunct
291 raw_syntax_traversion(comprehension_set(Pos,Ids,Body),cs(Pos,Ids),[Body]).
292 raw_syntax_traversion(lambda(Pos,Ids,Pred,Expr),lm(Pos,Ids),[Pred,Expr]).
293 raw_syntax_traversion(symbolic_comprehension_set(Pos,Ids,Body),sc(Pos,Ids),[Body]).
294 raw_syntax_traversion(symbolic_event_b_comprehension_set(Pos,Ids,Pred,Body),sc(Pos,Ids),[Pred,Body]).
295 raw_syntax_traversion(symbolic_lambda(Pos,Ids,Pred,Expr),symlam(Pos,Ids),[Pred,Expr]).
296 raw_syntax_traversion(function(Pos,Fun,List),fun(Pos),[Fun|List]). % function call
297 raw_syntax_traversion(sequence_extension(Pos,List),sqext(Pos),List).
298 raw_syntax_traversion(set_extension(Pos,List),sext(Pos),List).
299 % TODO: let_predicate, label, description, ....
300
301