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