1		:- module(input_syntax_tree, [remove_raw_position_info/2
2		,get_raw_position_info/2
3		,extract_raw_identifiers/2
4		,get_definition_name/2
5		,raw_replace/3
6		,raw_conjunct/2
7		,create_fresh_identifier/3
8		]).
9
10
11		:- use_module(error_manager).
12
13		get_raw_position_info(Compound,Info) :-
14		compound(Compound),
15		functor(Compound,_,Arity), Arity>0,
16		arg(1,Compound,Info),
17		Info = pos(_,_,_,_,_,_),!.
18		get_raw_position_info(Compound,Info) :-
19		add_internal_error('Could not get position info: ',get_raw_position_info(Compound,Info)),
20		Info = unknown.
21
22		:- use_module(tools,[safe_functor/4]).
23
24		remove_raw_position_info([],Output) :- !,Output=[].
25		remove_raw_position_info([I|Irest],[O|Orest]) :-
26		!,remove_raw_position_info(I,O),
27		remove_raw_position_info(Irest,Orest).
28		remove_raw_position_info(Input,Output) :-
29		compound(Input),functor(Input,Functor,Arity),Arity>0,!,
30		Arity2 is Arity-1,
31		functor(Output,Functor,Arity2),
32		remove_raw_position_info2(1,Arity,Input,Output).
33		remove_raw_position_info(Input,Input).
34
35
36		remove_raw_position_info2(Pos,Arity,Input,Output) :-
37		Pos < Arity,!,Pos2 is Pos+1,
38		arg(Pos2,Input,IA), arg(Pos,Output,OA),
39		remove_raw_position_info(IA,OA),
40		remove_raw_position_info2(Pos2,Arity,Input,Output).
41		remove_raw_position_info2(_Pos,_Arity,_Input,_Output).
42
43		:- use_module(library(ordsets),[ord_union/3, ord_member/2]).
44		extract_raw_identifiers(Ast,Ids) :-
45		extract_raw_identifiers2(Ast,[],Unsorted,[]),
46		sort(Unsorted,Ids).
47		extract_raw_identifiers2([],_) --> !,[].
48		extract_raw_identifiers2([I|Irest],Bound) -->
49		!,extract_raw_identifiers2(I,Bound),
50		extract_raw_identifiers2(Irest,Bound).
51		extract_raw_identifiers2(identifier(_,I),Bound) --> !,add_if_free(I,Bound).
52		extract_raw_identifiers2(definition(_,I,Args),Bound) --> !,
53		add_if_free(I,Bound), extract_raw_identifiers2(Args,Bound).
54		extract_raw_identifiers2(Input,Bound) -->
55		{raw_quantifier(Input,Ids,Subs)},!,
56		%{append(Ids,Bound,NewBound)},
57		{ord_union(Ids,Bound,NewBound)},
58		extract_raw_identifiers2(Subs,NewBound).
59		extract_raw_identifiers2(Input,Bound) -->
60		{compound(Input),functor(Input,_Functor,Arity),Arity>1,!},
61		extract_raw_identifiers3(2,Arity,Input,Bound).
62		extract_raw_identifiers2(_,_) --> [].
63
64		add_if_free(Id,Bound,In,Out) :-
65		( ord_member(Id,Bound) -> In=Out
66		; otherwise -> In=[Id|Out]).
67
68		extract_raw_identifiers3(Pos,Arity,Input,Bound) -->
69		{Pos=<Arity,!,Pos2 is Pos+1, arg(Pos,Input,Arg)},
70		extract_raw_identifiers2(Arg,Bound),
71		extract_raw_identifiers3(Pos2,Arity,Input,Bound).
72		extract_raw_identifiers3(_Pos,_Arity,_Input,_Bound) --> [].
73
74		:- use_module(library(lists),[maplist/3]).
75		raw_quantifier(Expr,SortedIds,Subs) :-
76		raw_quantifier_aux(Expr,RawIds,Subs),
77		maplist(raw_id,RawIds,Ids),
78		sort(Ids,SortedIds).
79		raw_id(identifier(_,ID),ID).
80
81		raw_quantifier_aux(forall(_,Ids,P),Ids,[P]).
82		raw_quantifier_aux(exists(_,Ids,P),Ids,[P]).
83		raw_quantifier_aux(comprehension_set(_,Ids,P),Ids,[P]).
84		raw_quantifier_aux(event_b_comprehension_set(_,Ids,E,P),Ids,[E,P]).
85		raw_quantifier_aux(lambda(Ids,P,E),Ids,[P,E]).
86		raw_quantifier_aux(general_sum(_,Ids,P,E),Ids,[P,E]).
87		raw_quantifier_aux(general_product(_,Ids,P,E),Ids,[P,E]).
88		raw_quantifier_aux(quantified_union(_,Ids,P,E),Ids,[P,E]).
89		raw_quantifier_aux(quantified_intersection(_,Ids,P,E),Ids,[P,E]).
90		raw_quantifier_aux(any(_,Ids,P,S),Ids,[P,S]).
91		raw_quantifier_aux(let(_,Ids,P,S),Ids,[P,S]).
92		raw_quantifier_aux(var(_,Ids,S),Ids,[S]).
93		raw_quantifier_aux(recursive_let(_,Id,E),[Id],[E]).
94
95		get_definition_name(expression_definition(_Pos,Name,_Args,_Body),Name).
96		get_definition_name(predicate_definition(_Pos,Name,_Args,_Body),Name).
97		get_definition_name(substitution_definition(_Pos,Name,_Args,_Body),Name).
98
99		% raw_replace(+InputAST,-Replaces,+OutputAST):
100		% InputAST: A raw AST as it comes from the parser (without type information)
101		% Replaces: A list of "replace(Id,Expr)" where Id the the identifier which
102		% should be replaced by the expression Expr
103		% OutputAST: A raw AST where all matching identifiers are replaced by their
104		% expression
105		% used for rewriting DEFINITION calls
106		raw_replace(Expr,[],Expr) :- !.
107		raw_replace(Old,Replaces,New) :-
108		get_introduced_ids(Replaces,IntroducedIds), %print(intro(IntroducedIds)),nl,
109		raw_replace2(Old,Replaces,IntroducedIds,New).
110		raw_replace2([],_,_,[]) :- !.
111		raw_replace2([E|Rest],Replaces,IntroducedIds,[N|NRest]) :- !,
112		raw_replace2(E,Replaces,IntroducedIds,N),
113		raw_replace2(Rest,Replaces,IntroducedIds,NRest).
114		raw_replace2(rewrite_protected(X),_Replaces,_,rewrite_protected(Y)) :- !,X=Y.
115		raw_replace2(identifier(_,Old),Replaces,_,New) :-
116		memberchk(replace(Old,New),Replaces),!.
117		raw_replace2(Expr,_,IntroducedIds,_) :-
118		quantifier_capture_warning(Expr,IntroducedIds),
119		fail.
120		raw_replace2(Expr,Replaces,IntroducedIds,New) :-
121		safe_functor(raw_replace2_expr,Expr,Functor,Arity),
122		safe_functor(raw_replace2_new,New,Functor,Arity),
123		raw_replace3(Arity,Expr,Replaces,IntroducedIds,New).
124		raw_replace3(0,_,_,_,_) :- !.
125		raw_replace3(N,Expr,Replaces,IntroducedIds,NExpr) :-
126		arg(N,Expr,Old),
127		arg(N,NExpr,New),
128		raw_replace2(Old,Replaces,IntroducedIds,New),
129		N2 is N-1,
130		raw_replace3(N2,Expr,Replaces,IntroducedIds,NExpr).
131
132		:- use_module(library(ordsets),[ord_union/2, ord_intersection/3]).
133		% 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
134		quantifier_capture_warning(Expr,IntroducedIds) :-
135		raw_quantifier(Expr,SortedIds,_Body),
136		ord_intersection(IntroducedIds,SortedIds,Clash),
137		Clash \= [],
138		% TO DO?: check if we really use a corresponding LHS identifier in Body: extract_raw_identifiers(Body,UsedIds), maplist(get_lhs_id,Replaces,LHSIds),
139		%format('Quantifier ids: ~w~nIntroduced Ids: ~w~n',[SortedIds,IntroducedIds]),
140		arg(1,Expr,Pos),
141		add_warning(definition_variable_capture,'Quantifier may capture identifiers in DEFINITION arguments: ',Clash,Pos).
142
143		% compute which ids are introduced by performing the replacements
144		get_introduced_ids(Replaces,Ids) :- maplist(get_rhs_ids,Replaces,ListOfList),
145		ord_union(ListOfList,Ids).
146		get_rhs_ids(replace(_,New),Ids) :- extract_raw_identifiers(New,Ids).
147		%get_lhs_id(replace(Id,_),Id).
148
149		raw_conjunct([],truth(none)).
150		raw_conjunct([H|T],R) :-
151		( T=[] -> H=R
152		; otherwise ->
153		R=conjunct(none,H,RT),
154		raw_conjunct(T,RT)
155		).
156
157		%raw_occurs(ID,Term) :- raw_id(Term,ID).
158		%raw_occurs(ID,Term) :- compound(Term), Term =.. [_Func,_Pos|Args],
159		% member(A,Args), raw_occurs(ID,A).
160
161
162		% create_fresh_identifier(+PreferredName,+Ast,-Name):
163		% Generates an identifier that does not occur in Ast
164		% PreferredName: An atom with the preferred name of the identifier
165		% Ast: An untyped AST
166		% Name: An identifier (an atom) that does not occur free in AST,
167		% If PreferredName does not occur free in AST, it's 'PreferredName',
168		% otherwise it's 'PreferredName_N' where N is a natural number
169		create_fresh_identifier(PreferredName,Ast,Name) :-
170		extract_raw_identifiers(Ast,UsedIds),
171		( memberchk(PreferredName,UsedIds) ->
172		% Allready in use, find a fresh one by adding a number
173		atom_codes(PreferredName,PreferredCodes),
174		create_fresh_identifier_aux(PreferredCodes,UsedIds,1,Name)
175		; otherwise ->
176		Name = PreferredName).
177		create_fresh_identifier_aux(PreferredCodes,UsedIds,I,Name) :-
178		number_codes(I,ICodes),append(PreferredCodes,[95|ICodes],Codes),
179		atom_codes(NewName,Codes),
180		( memberchk(NewName,UsedIds) ->
181		% Allready in use, try again with a higher number
182		I2 is I+1,
183		create_fresh_identifier_aux(PreferredCodes,UsedIds,I2,Name)
184		; otherwise ->
185		Name = NewName).