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(tools_positions, [is_position/1]).
25
26		get_raw_position_info(Compound,Info) :-
27		try_get_raw_position_info(Compound,Info),
28		is_position(Info),!.
29		get_raw_position_info(Compound,Info) :-
30		add_internal_error('Could not get position info: ',get_raw_position_info(Compound,Info)),
31		Info = unknown.
32
33		try_get_raw_position_info(Compound,Info) :-
34		compound(Compound),
35		functor(Compound,_,Arity), Arity>0,
36		arg(1,Compound,Info).
37
38		:- use_module(tools,[safe_functor/4]).
39
40		remove_raw_position_info([],Output) :- !,Output=[].
41		remove_raw_position_info([I|Irest],[O|Orest]) :-
42		!,remove_raw_position_info(I,O),
43		remove_raw_position_info(Irest,Orest).
44		remove_raw_position_info(Input,Output) :-
45		compound(Input),functor(Input,Functor,Arity),Arity>0,!,
46		Arity2 is Arity-1,
47		functor(Output,Functor,Arity2),
48		remove_raw_position_info2(1,Arity,Input,Output).
49		remove_raw_position_info(Input,Input).
50
51
52		remove_raw_position_info2(Pos,Arity,Input,Output) :-
53		Pos < Arity,!,Pos2 is Pos+1,
54		arg(Pos2,Input,IA), arg(Pos,Output,OA),
55		remove_raw_position_info(IA,OA),
56		remove_raw_position_info2(Pos2,Arity,Input,Output).
57		remove_raw_position_info2(_Pos,_Arity,_Input,_Output).
58
59		:- use_module(library(ordsets),[ord_union/3, ord_member/2]).
60		extract_raw_identifiers(Ast,Ids) :-
61		extract_raw_identifiers2(Ast,[],Unsorted,[]),
62		sort(Unsorted,Ids).
63		extract_raw_identifiers2([],_) --> !,[].
64		extract_raw_identifiers2([I|Irest],Bound) -->
65		!,extract_raw_identifiers2(I,Bound),
66		extract_raw_identifiers2(Irest,Bound).
67		extract_raw_identifiers2(identifier(_,I),Bound) --> !,add_if_free(I,Bound).
68		extract_raw_identifiers2(definition(_,I,Args),Bound) --> !,
69		add_if_free(I,Bound),
70		extract_raw_identifiers2(Args,Bound). % Note: we do not see the Ids inside the definition body!
71		extract_raw_identifiers2(Input,Bound) -->
72		{raw_quantifier(Input,Ids,Subs)},!,
73		%{append(Ids,Bound,NewBound)},
74		{sort(Ids,SIds),ord_union(SIds,Bound,NewBound)},
75		extract_raw_identifiers2(Subs,NewBound).
76		extract_raw_identifiers2(Input,Bound) -->
77		{compound(Input),functor(Input,_Functor,Arity),Arity>1,!},
78		extract_raw_identifiers3(2,Arity,Input,Bound).
79		extract_raw_identifiers2(_,_) --> [].
80
81		add_if_free(Id,Bound,In,Out) :-
82		%(ordsets:is_ordset(Bound) -> true ; add_internal_error('Not ordset: ',add_if_free(Id,Bound))),
83		(ord_member(Id,Bound) -> In=Out ; In=[Id|Out]).
84
85		extract_raw_identifiers3(Pos,Arity,Input,Bound) -->
86		{Pos=<Arity,!,Pos2 is Pos+1, arg(Pos,Input,Arg)},
87		extract_raw_identifiers2(Arg,Bound),
88		extract_raw_identifiers3(Pos2,Arity,Input,Bound).
89		extract_raw_identifiers3(_Pos,_Arity,_Input,_Bound) --> [].
90
91		:- use_module(library(lists),[maplist/3]).
92		raw_quantifier(Expr,SortedIds,Subs) :-
93		raw_quantifier_aux(Expr,RawIds,Subs),
94		maplist(raw_id,RawIds,Ids),
95		sort(Ids,SortedIds).
96		raw_id(identifier(_,ID),ID).
97
98		raw_quantifier_aux(forall(_,Ids,P),Ids,[P]).
99		raw_quantifier_aux(exists(_,Ids,P),Ids,[P]).
100		raw_quantifier_aux(comprehension_set(_,Ids,P),Ids,[P]).
101		raw_quantifier_aux(event_b_comprehension_set(_,Ids,E,P),Ids,[E,P]).
102		raw_quantifier_aux(lambda(_,Ids,P,E),Ids,[P,E]).
103		raw_quantifier_aux(general_sum(_,Ids,P,E),Ids,[P,E]).
104		raw_quantifier_aux(general_product(_,Ids,P,E),Ids,[P,E]).
105		raw_quantifier_aux(quantified_union(_,Ids,P,E),Ids,[P,E]).
106		raw_quantifier_aux(quantified_intersection(_,Ids,P,E),Ids,[P,E]).
107		raw_quantifier_aux(any(_,Ids,P,S),Ids,[P,S]).
108		raw_quantifier_aux(let(_,Ids,P,S),Ids,[P,S]).
109		raw_quantifier_aux(var(_,Ids,S),Ids,[S]).
110		raw_quantifier_aux(recursive_let(_,Id,E),[Id],[E]).
111
112		get_definition_name(expression_definition(_Pos,Name,_Args,_Body),Name).
113		get_definition_name(predicate_definition(_Pos,Name,_Args,_Body),Name).
114		get_definition_name(substitution_definition(_Pos,Name,_Args,_Body),Name).
115
116		:- use_module(parsercall, [transform_string_template/3]).
117
118		% raw_replace(+InputAST,-Replaces,+OutputAST):
119		% InputAST: A raw AST as it comes from the parser (without type information)
120		% Replaces: A list of "replace(Id,Expr)" where Id the the identifier which
121		% should be replaced by the expression Expr
122		% OutputAST: A raw AST where all matching identifiers are replaced by their
123		% expression
124		% used for rewriting DEFINITION calls
125		raw_replace(Expr,[],Expr) :- !.
126		raw_replace(Old,Replaces,New) :-
127		get_introduced_ids(Replaces,IntroducedIds), %print(intro(IntroducedIds)),nl,
128		raw_replace2(Old,Replaces,IntroducedIds,New).
129		raw_replace2([],_,_,[]) :- !.
130		raw_replace2([E|Rest],Replaces,IntroducedIds,[N|NRest]) :- !,
131		raw_replace2(E,Replaces,IntroducedIds,N),
132		raw_replace2(Rest,Replaces,IntroducedIds,NRest).
133		raw_replace2(rewrite_protected(X),_Replaces,_,rewrite_protected(Y)) :- !,X=Y.
134		raw_replace2(identifier(Pos,Old),Replaces,_,New) :- !,
135		(memberchk(replace(Old,New),Replaces) -> true ; New=identifier(Pos,Old)).
136		raw_replace2(multiline_template(Pos,TS),Replaces,Ids,New) :- !, % rewrite template, it may contain expressions with ids
137		atom_codes(TS,Codes),
138		transform_string_template(Codes,Pos,RawExpr),
139		raw_replace2(RawExpr,Replaces,Ids,New).
140		raw_replace2(Expr,_,IntroducedIds,_) :-
141		quantifier_capture_warning(Expr,IntroducedIds),
142		fail.
143		raw_replace2(X,_Replaces,_,Res) :- simple_expr(X), !,Res=X.
144		raw_replace2(Expr,Replaces,IntroducedIds,New) :-
145		safe_functor(raw_replace2_expr,Expr,Functor,Arity),
146		safe_functor(raw_replace2_new,New,Functor,Arity),
147		raw_replace3(Arity,Expr,Replaces,IntroducedIds,New).
148		raw_replace3(0,_,_,_,_) :- !.
149		raw_replace3(N,Expr,Replaces,IntroducedIds,NExpr) :-
150		arg(N,Expr,Old),
151		arg(N,NExpr,New),
152		raw_replace2(Old,Replaces,IntroducedIds,New),
153		N2 is N-1,
154		raw_replace3(N2,Expr,Replaces,IntroducedIds,NExpr).
155
156		simple_expr(real(_,_)).
157		simple_expr(string(_,_)).
158		simple_expr(integer(_,_)).
159
160		:- use_module(library(ordsets),[ord_union/2, ord_intersection/3]).
161		% 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
162		quantifier_capture_warning(Expr,IntroducedIds) :-
163		raw_quantifier(Expr,SortedIds,_Body),
164		ord_intersection(IntroducedIds,SortedIds,Clash),
165		Clash \= [],
166		% TO DO?: check if we really use a corresponding LHS identifier in Body: extract_raw_identifiers(Body,UsedIds), maplist(get_lhs_id,Replaces,LHSIds),
167		%format('Quantifier ids: ~w~nIntroduced Ids: ~w~n',[SortedIds,IntroducedIds]),
168		arg(1,Expr,Pos),
169		add_warning(definition_variable_capture,'Quantifier may capture identifiers in DEFINITION arguments: ',Clash,Pos).
170
171		% compute which ids are introduced by performing the replacements
172		get_introduced_ids(Replaces,Ids) :- maplist(get_rhs_ids,Replaces,ListOfList),
173		ord_union(ListOfList,Ids).
174		get_rhs_ids(replace(_,New),Ids) :- extract_raw_identifiers(New,Ids).
175		%get_lhs_id(replace(Id,_),Id).
176
177		raw_conjunct([],truth(none)).
178		raw_conjunct([H|T],R) :-
179		( T=[] -> H=R
180		;
181		R=conjunct(none,H,RT),
182		raw_conjunct(T,RT)
183		).
184
185		%raw_occurs(ID,Term) :- raw_id(Term,ID).
186		%raw_occurs(ID,Term) :- compound(Term), Term =.. [_Func,_Pos|Args],
187		% member(A,Args), raw_occurs(ID,A).
188
189
190		% create_fresh_identifier(+PreferredName,+Ast,-Name):
191		% Generates an identifier that does not occur in Ast
192		% PreferredName: An atom with the preferred name of the identifier
193		% Ast: An untyped AST
194		% Name: An identifier (an atom) that does not occur free in AST,
195		% If PreferredName does not occur free in AST, it's 'PreferredName',
196		% otherwise it's 'PreferredName_N' where N is a natural number
197		create_fresh_identifier(PreferredName,Ast,Name) :-
198		extract_raw_identifiers(Ast,UsedIds),
199		( memberchk(PreferredName,UsedIds) ->
200		% Allready in use, find a fresh one by adding a number
201		atom_codes(PreferredName,PreferredCodes),
202		create_fresh_identifier_aux(PreferredCodes,UsedIds,1,Name)
203		;
204		Name = PreferredName).
205		create_fresh_identifier_aux(PreferredCodes,UsedIds,I,Name) :-
206		number_codes(I,ICodes),append(PreferredCodes,[95|ICodes],Codes),
207		atom_codes(NewName,Codes),
208		( memberchk(NewName,UsedIds) ->
209		% Allready in use, try again with a higher number
210		I2 is I+1,
211		create_fresh_identifier_aux(PreferredCodes,UsedIds,I2,Name)
212		;
213		Name = NewName).
214
215		% map a predicate over the raw AST to transform it
216
217		map_over(P,RawExpr,Res) :- map_over_raw_expr(RawExpr,P,Res).
218
219		map_over_raw_expr(RawExpr,P,Res) :- call(P,RawExpr,NewRawExpr),!,
220		Res=NewRawExpr.
221		map_over_raw_expr(conjunct(Pos,A,B),P,conjunct(Pos,MA,MB)) :- !,
222		map_over_raw_expr(A,P,MA),
223		map_over_raw_expr(B,P,MB).
224		map_over_raw_expr(disjunct(Pos,A,B),P,disjunct(Pos,MA,MB)) :- !,
225		map_over_raw_expr(A,P,MA),
226		map_over_raw_expr(B,P,MB).
227		map_over_raw_expr(equal(Pos,A,B),P,equal(Pos,MA,MB)) :- !,
228		map_over_raw_expr(A,P,MA),
229		map_over_raw_expr(B,P,MB).
230		map_over_raw_expr(A,_,R) :- atomic(A),!,R=A.
231		map_over_raw_expr(A,P,R) :- raw_syntax_traversion(A,Fixed,Args),!,
232		functor(A,F,N), functor(R,F,N),
233		raw_syntax_traversion(R,Fixed,NewArgs),
234		maplist(map_over(P),Args,NewArgs).
235		map_over_raw_expr(F,P,MF) :- F =.. [Functor,Pos|Args], % default: arg1 is position, rest is sub-arguments
236		maplist(map_over(P),Args,NewArgs),
237		MF =.. [Functor,Pos|NewArgs].
238
239		raw_syntax_traversion(conjunct(Pos,List),con(Pos),List). % n-ary conjunct
240		raw_syntax_traversion(disjunct(Pos,List),disj(Pos),List). % n-ary disjunct
241		raw_syntax_traversion(comprehension_set(Pos,Ids,Body),cs(Pos,Ids),[Body]).
242		raw_syntax_traversion(lambda(Pos,Ids,Pred,Expr),lm(Pos,Ids),[Pred,Expr]).
243		raw_syntax_traversion(symbolic_comprehension_set(Pos,Ids,Body),sc(Pos,Ids),[Body]).
244		raw_syntax_traversion(symbolic_lambda(Pos,Ids,Pred,Expr),symlam(Pos,Ids),[Pred,Expr]).
245		raw_syntax_traversion(function(Pos,Fun,List),fun(Pos),[Fun|List]). % function call
246		raw_syntax_traversion(sequence_extension(Pos,List),sqext(Pos),List).
247		raw_syntax_traversion(set_extension(Pos,List),sext(Pos),List).
248		% TODO: let_predicate, label, description, ....
249
250