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		,raw_operator/1
16		,raw_symbolic_annotation/2
17		,raw_operator_term/1, raw_literal_term/1, raw_special_set_term/1
18		]).
19
20		:- use_module(module_information,[module_info/2]).
21		:- module_info(group,typechecker).
22		:- module_info(description,'Utilities on the raw AST.').
23
24		:- meta_predicate map_over(2,*,*).
25		:- meta_predicate map_over_raw_expr(*,2,*).
26
27		:- use_module(error_manager).
28		:- use_module(probsrc(tools_strings),[ajoin/2]).
29		:- use_module(tools_positions, [is_position/1, update_position_filenumber/4]).
30		:- use_module(tools,[safe_functor/4]).
31		:- use_module(translate,[translate_raw_bexpr_with_limit/3]).
32
33		get_raw_position_info(Compound,Info) :-
34		try_get_raw_position_info(Compound,Info),
35		is_position(Info),!.
36		get_raw_position_info(Compound,Info) :-
37		add_internal_error('Could not get position info: ',get_raw_position_info(Compound,Info)),
38		Info = unknown.
39
40		try_get_raw_position_info(Compound,Info) :-
41		compound(Compound),
42		functor(Compound,_,Arity), Arity>0,
43		arg(1,Compound,Info).
44
45		update_raw_position_info(Compound,Pos,NewCompound,NewPos) :-
46		compound(Compound),
47		Compound =.. [Functor,Pos|Rest],
48		NewCompound =.. [Functor,NewPos|Rest].
49
50		remove_raw_position_info([],Output) :- !,Output=[].
51		remove_raw_position_info([I|Irest],[O|Orest]) :-
52		!,remove_raw_position_info(I,O),
53		remove_raw_position_info(Irest,Orest).
54		remove_raw_position_info(Input,Output) :-
55		compound(Input),functor(Input,Functor,Arity),Arity>0,!,
56		Arity2 is Arity-1,
57		functor(Output,Functor,Arity2),
58		remove_raw_position_info2(1,Arity,Input,Output).
59		remove_raw_position_info(Input,Input).
60
61
62		remove_raw_position_info2(Pos,Arity,Input,Output) :-
63		Pos < Arity,!,Pos2 is Pos+1,
64		arg(Pos2,Input,IA), arg(Pos,Output,OA),
65		remove_raw_position_info(IA,OA),
66		remove_raw_position_info2(Pos2,Arity,Input,Output).
67		remove_raw_position_info2(_Pos,_Arity,_Input,_Output).
68
69		:- use_module(library(ordsets),[ord_union/3, ord_member/2]).
70		extract_raw_identifiers(Ast,Ids) :-
71		extract_raw_identifiers2(Ast,[],Unsorted,[]),
72		sort(Unsorted,Ids).
73		extract_raw_identifiers2([],_) --> !,[].
74		extract_raw_identifiers2([I|Irest],Bound) -->
75		!,extract_raw_identifiers2(I,Bound),
76		extract_raw_identifiers2(Irest,Bound).
77		extract_raw_identifiers2(identifier(_,I),Bound) --> !,add_if_free(I,Bound).
78		extract_raw_identifiers2(definition(_,I,Args),Bound) --> !,
79		add_if_free(I,Bound),
80		extract_raw_identifiers2(Args,Bound). % Note: we do not see the Ids inside the definition body!
81		extract_raw_identifiers2(Input,Bound) -->
82		{raw_quantifier(Input,Ids,Subs)},!,
83		%{append(Ids,Bound,NewBound)},
84		{sort(Ids,SIds),ord_union(SIds,Bound,NewBound)},
85		extract_raw_identifiers2(Subs,NewBound).
86		extract_raw_identifiers2(Input,Bound) -->
87		{compound(Input),functor(Input,_Functor,Arity),Arity>1,!},
88		extract_raw_identifiers3(2,Arity,Input,Bound).
89		extract_raw_identifiers2(_,_) --> [].
90
91		add_if_free(Id,Bound,In,Out) :-
92		%(ordsets:is_ordset(Bound) -> true ; add_internal_error('Not ordset: ',add_if_free(Id,Bound))),
93		(ord_member(Id,Bound) -> In=Out ; In=[Id|Out]).
94
95		extract_raw_identifiers3(Pos,Arity,Input,Bound) -->
96		{Pos=<Arity,!,Pos2 is Pos+1, arg(Pos,Input,Arg)},
97		extract_raw_identifiers2(Arg,Bound),
98		extract_raw_identifiers3(Pos2,Arity,Input,Bound).
99		extract_raw_identifiers3(_Pos,_Arity,_Input,_Bound) --> [].
100
101		:- use_module(library(lists),[maplist/3]).
102		raw_quantifier(Expr,SortedIds,Subs) :-
103		raw_quantifier_aux(Expr,RawIds,Subs),
104		maplist(raw_id,RawIds,Ids),
105		sort(Ids,SortedIds).
106		raw_id(identifier(_,ID),ID).
107
108		raw_quantifier_aux(SymTerm,Ids,Subs) :- raw_symbolic_annotation(SymTerm,Term),!,
109		raw_quantifier_aux(Term,Ids,Subs).
110		raw_quantifier_aux(forall(_,Ids,P),Ids,[P]).
111		raw_quantifier_aux(exists(_,Ids,P),Ids,[P]).
112		raw_quantifier_aux(comprehension_set(_,Ids,P),Ids,[P]).
113		raw_quantifier_aux(event_b_comprehension_set(_,Ids,E,P),Ids,[E,P]).
114		raw_quantifier_aux(lambda(_,Ids,P,E),Ids,[P,E]).
115		raw_quantifier_aux(general_sum(_,Ids,P,E),Ids,[P,E]).
116		raw_quantifier_aux(general_product(_,Ids,P,E),Ids,[P,E]).
117		raw_quantifier_aux(quantified_intersection(_,Ids,P,E),Ids,[P,E]).
118		raw_quantifier_aux(quantified_union(_,Ids,P,E),Ids,[P,E]).
119		raw_quantifier_aux(any(_,Ids,P,S),Ids,[P,S]).
120		raw_quantifier_aux(let(_,Ids,P,S),Ids,[P,S]).
121		raw_quantifier_aux(var(_,Ids,S),Ids,[S]).
122		raw_quantifier_aux(recursive_let(_,Id,E),[Id],[E]).
123
124		get_definition_name(expression_definition(_Pos,Name,_Args,_Body),Name).
125		get_definition_name(predicate_definition(_Pos,Name,_Args,_Body),Name).
126		get_definition_name(substitution_definition(_Pos,Name,_Args,_Body),Name).
127
128		:- use_module(parsercall, [transform_string_template/3]).
129
130		% raw_replace(+InputAST,-Replaces,+OutputAST,DefName):
131		% InputAST: A raw AST as it comes from the parser (without type information)
132		% Replaces: A list of "replace(Id,Expr)" where Id the the identifier which
133		% should be replaced by the expression Expr
134		% OutputAST: A raw AST where all matching identifiers are replaced by their
135		% expression
136		% DefName: name of definition for which we do the rewrite
137		% used for rewriting DEFINITION calls
138		raw_replace(Expr,[],Expr,_) :- !.
139		raw_replace(Old,Replaces,New,DefName) :-
140		get_introduced_ids(Replaces,IntroducedIds), %print(intro(IntroducedIds)),nl,
141	?	raw_replace2(Old,Replaces,IntroducedIds,New,DefName).
142		raw_replace2([],_,_,[],_) :- !.
143		raw_replace2([E|Rest],Replaces,IntroducedIds,[N|NRest],DefName) :- !,
144	?	raw_replace2(E,Replaces,IntroducedIds,N,DefName),
145	?	raw_replace2(Rest,Replaces,IntroducedIds,NRest,DefName).
146		raw_replace2(rewrite_protected(X),_Replaces,_,rewrite_protected(Y),_) :- !,X=Y.
147		raw_replace2(becomes_such(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_such(Pos,NVars,NCond),DefName) :- !,
148		raw_replace2(Cond,Replaces,IntroducedIds,NCond,DefName),
149		raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).
150		raw_replace2(becomes_element_of(Pos,Vars,Cond),Replaces,IntroducedIds,becomes_element_of(Pos,NVars,NCond),DefName) :- !,
151		raw_replace2(Cond,Replaces,IntroducedIds,NCond,DefName),
152		raw_replace_id_list(Vars,Replaces,IntroducedIds,NVars).
153		% TODO: support more raw AST nodes with identifier lists
154		raw_replace2(identifier(Pos,Old),Replaces,_,New,_) :- !,
155		(memberchk(replace(Old,New),Replaces) -> true ; New=identifier(Pos,Old)).
156		raw_replace2(record_field(RPos,Record,Field),Replaces,IntroducedIds,record_field(RPos,NRecord,NField),DefName) :- !,
157		raw_replace2(Record,Replaces,IntroducedIds,NRecord,DefName),
158		(Field=identifier(_,FieldName),
159		raw_replace2(Field,Replaces,IntroducedIds,NField,DefName)
160		-> (NField=identifier(_,NewFieldName)
161		-> (NewFieldName=FieldName -> true
162		; ajoin(['Rewriting field name ',FieldName,' during definition expansion to: '],Msg),
163		add_message(definition_rewrite,Msg,NewFieldName,RPos)
164		)
165		; translate_raw_bexpr_with_limit(NField,50,FS),
166		ajoin(['Rewriting field name ',FieldName,' to an illegal expression: '],Msg),
167		(try_get_raw_position_info(NField,NFPos) -> true ; NFPos=RPos),
168		add_warning(definition_rewrite,Msg,FS,NFPos)
169		)
170		; NField=Field).
171		raw_replace2(multiline_template(Pos,TS),Replaces,Ids,New,DefName) :- !,
172		% rewrite template, it may contain expressions with ids
173	?	transform_string_template(TS,Pos,RawExpr),
174		raw_replace2(RawExpr,Replaces,Ids,New,DefName).
175		raw_replace2(Expr,_,IntroducedIds,_,DefName) :-
176		quantifier_capture_warning(Expr,IntroducedIds,DefName),
177		fail.
178		raw_replace2(X,_Replaces,_,Res,_) :- simple_expr(X), !,Res=X.
179		raw_replace2(Expr,Replaces,IntroducedIds,New,DefName) :-
180		safe_functor(raw_replace2_expr,Expr,Functor,Arity),
181		safe_functor(raw_replace2_new,New,Functor,Arity),
182	?	raw_replace3(Arity,Expr,Replaces,IntroducedIds,New,DefName).
183		raw_replace3(0,_,_,_,_,_) :- !.
184		raw_replace3(N,Expr,Replaces,IntroducedIds,NExpr,DefName) :-
185		arg(N,Expr,Old),
186		arg(N,NExpr,New),
187	?	raw_replace2(Old,Replaces,IntroducedIds,New,DefName),
188		N2 is N-1,
189		raw_replace3(N2,Expr,Replaces,IntroducedIds,NExpr,DefName).
190
191		simple_expr(real(_,_)).
192		simple_expr(string(_,_)).
193		simple_expr(integer(_,_)).
194
195
196		% replace a list of identifiers in the orginal AST which should remain a list of identifiers
197		% we allow
198		raw_replace_id_list([],_,_,[]).
199		raw_replace_id_list([identifier(Pos,Old)|T],Replaces,Intro,Res) :- !,
200		(memberchk(replace(Old,New),Replaces)
201		-> (flatten_couple_id_list(New,Res,Tail) -> NT=Tail
202		; ajoin(['Rewriting identifier ',Old,' to an illegal value during definition expansion: '],Msg),
203		add_warning(definition_rewrite,Msg,New,Pos),
204		Res = [New|NT]
205		)
206		; Res=[identifier(Pos,Old)|NT]
207		), raw_replace_id_list(T,Replaces,Intro,NT).
208		raw_replace_id_list([H|T],Replaces,Intro,[H|NT]) :-
209		arg(1,H,Pos),
210		add_warning(definition_rewrite,'Not an identifier in raw AST: ',H,Pos), % should not happen
211		raw_replace_id_list(T,Replaces,Intro,NT).
212
213		% flatten a couple list of identifiers; can happen when we have vars == x,y and pass vars to a definition as argument
214		flatten_couple_id_list(couple(_Pos,List)) --> !,
215		% one could check that in Pos we have a pos_context with definition_call
216		l_flatten_couple_id_list(List).
217		flatten_couple_id_list(OtherVal) --> {OtherVal=identifier(_,_)},[OtherVal].
218
219		l_flatten_couple_id_list([]) --> [].
220		l_flatten_couple_id_list([H|T]) --> !, flatten_couple_id_list(H), l_flatten_couple_id_list(T).
221
222		:- use_module(library(ordsets),[ord_union/2, ord_intersection/3]).
223		% 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
224		quantifier_capture_warning(Expr,IntroducedIds,DefName) :-
225		raw_quantifier(Expr,SortedIds,_Body),
226		ord_intersection(IntroducedIds,SortedIds,Clash),
227		Clash \= [],
228		% TO DO?: check if we really use a corresponding LHS identifier in Body: extract_raw_identifiers(Body,UsedIds), maplist(get_lhs_id,Replaces,LHSIds),
229		%format('Quantifier ids: ~w~nIntroduced Ids: ~w~n',[SortedIds,IntroducedIds]),
230		arg(1,Expr,Pos),
231		functor(Expr,QKind,_),
232		ajoin(['Quantifier (',QKind,') inside DEFINITION ',DefName,
233		' may capture identifiers from arguments of definition call: '],Msg),
234		add_warning(definition_variable_capture,Msg,Clash,Pos).
235
236		% compute which ids are introduced by performing the replacements
237		get_introduced_ids(Replaces,Ids) :- maplist(get_rhs_ids,Replaces,ListOfList),
238		ord_union(ListOfList,Ids).
239		get_rhs_ids(replace(_,New),Ids) :- extract_raw_identifiers(New,Ids).
240		%get_lhs_id(replace(Id,_),Id).
241
242		raw_conjunct([],truth(none)).
243		raw_conjunct([H|T],R) :-
244		( T=[] -> H=R
245		;
246		R=conjunct(none,H,RT),
247		raw_conjunct(T,RT)
248		).
249
250		%raw_occurs(ID,Term) :- raw_id(Term,ID).
251		%raw_occurs(ID,Term) :- compound(Term), Term =.. [_Func,_Pos|Args],
252		% member(A,Args), raw_occurs(ID,A).
253
254
255		% create_fresh_identifier(+PreferredName,+Ast,-Name):
256		% Generates an identifier that does not occur in Ast
257		% PreferredName: An atom with the preferred name of the identifier
258		% Ast: An untyped AST
259		% Name: An identifier (an atom) that does not occur free in AST,
260		% If PreferredName does not occur free in AST, it's 'PreferredName',
261		% otherwise it's 'PreferredName_N' where N is a natural number
262		create_fresh_identifier(PreferredName,Ast,Name) :-
263		extract_raw_identifiers(Ast,UsedIds),
264		( memberchk(PreferredName,UsedIds) ->
265		% Allready in use, find a fresh one by adding a number
266		atom_codes(PreferredName,PreferredCodes),
267		create_fresh_identifier_aux(PreferredCodes,UsedIds,1,Name)
268		;
269		Name = PreferredName).
270		create_fresh_identifier_aux(PreferredCodes,UsedIds,I,Name) :-
271		number_codes(I,ICodes),append(PreferredCodes,[95|ICodes],Codes),
272		atom_codes(NewName,Codes),
273		( memberchk(NewName,UsedIds) ->
274		% Allready in use, try again with a higher number
275		I2 is I+1,
276		create_fresh_identifier_aux(PreferredCodes,UsedIds,I2,Name)
277		;
278		Name = NewName).
279
280		% map a predicate over the raw AST to transform it
281		% we suppose that if the predicate P succeeds the sub-arguments do not need to be transformed
282
283		map_over(P,RawExpr,Res) :- map_over_raw_expr(RawExpr,P,Res).
284
285		map_over_raw_expr(RawExpr,P,Res) :- call(P,RawExpr,NewRawExpr),!,
286		Res=NewRawExpr.
287		map_over_raw_expr(RawExpr,P,Res) :- recur_over_raw_expr(RawExpr,P,Res).
288
289		recur_over_raw_expr([A|T],P,[MA|MT]) :- !,
290		map_over_raw_expr(A,P,MA),
291		map_over_raw_expr(T,P,MT).
292		recur_over_raw_expr(conjunct(Pos,A,B),P,conjunct(Pos,MA,MB)) :- !,
293		map_over_raw_expr(A,P,MA),
294		map_over_raw_expr(B,P,MB).
295		recur_over_raw_expr(disjunct(Pos,A,B),P,disjunct(Pos,MA,MB)) :- !,
296		map_over_raw_expr(A,P,MA),
297		map_over_raw_expr(B,P,MB).
298		recur_over_raw_expr(equal(Pos,A,B),P,equal(Pos,MA,MB)) :- !,
299		map_over_raw_expr(A,P,MA),
300		map_over_raw_expr(B,P,MB).
301		recur_over_raw_expr(A,_,R) :- atomic(A),!,R=A.
302		recur_over_raw_expr(A,P,R) :- raw_syntax_traversion(A,Fixed,Args),!,
303		functor(A,F,N), functor(R,F,N),
304		raw_syntax_traversion(R,Fixed,NewArgs),
305		maplist(map_over(P),Args,NewArgs).
306		recur_over_raw_expr(F,P,MF) :- F =.. [Functor,Pos|Args], % default: arg1 is position, rest is sub-arguments
307		maplist(map_over(P),Args,NewArgs),
308		MF =.. [Functor,Pos|NewArgs].
309
310		raw_syntax_traversion(definitions(Pos,List),defs(Pos),List). % definitions section
311		raw_syntax_traversion(expression_definition(Pos,Name,Paras,Body),expression_definition(Pos,Name),[Body|Paras]).
312
313		raw_syntax_traversion(conjunct(Pos,List),con(Pos),List). % n-ary conjunct
314		raw_syntax_traversion(disjunct(Pos,List),disj(Pos),List). % n-ary disjunct
315		raw_syntax_traversion(comprehension_set(Pos,Ids,Body),cs(Pos,Ids),[Body]).
316		raw_syntax_traversion(event_b_comprehension_set(Pos,Ids,Pred,Body),cs(Pos,Ids),[Pred,Body]).
317		raw_syntax_traversion(lambda(Pos,Ids,Pred,Expr),lm(Pos,Ids),[Pred,Expr]).
318		raw_syntax_traversion(symbolic_comprehension_set(Pos,Ids,Body),sc(Pos,Ids),[Body]).
319		raw_syntax_traversion(symbolic_event_b_comprehension_set(Pos,Ids,Pred,Body),sc(Pos,Ids),[Pred,Body]).
320		raw_syntax_traversion(symbolic_lambda(Pos,Ids,Pred,Expr),symlam(Pos,Ids),[Pred,Expr]).
321		raw_syntax_traversion(function(Pos,Fun,List),fun(Pos),[Fun|List]). % function call
322		raw_syntax_traversion(sequence_extension(Pos,List),sqext(Pos),List).
323		raw_syntax_traversion(set_extension(Pos,List),sext(Pos),List).
324		raw_syntax_traversion(definition(Pos,Name,ParaList),defcall(Pos,Name),ParaList).
325		raw_syntax_traversion(rec(Pos,List),rec(Pos),List). % n-ary conjunct
326		% TODO: let_predicate, label, description, ....
327
328
329
330		% update file numbers to new numbers (e.g., useful when adding separately parsed .prob files to an existing machine)
331		% the NewNrs list gives the new numbers of files 1,2,3,... etc respectively
332
333		raw_update_file_nrs(RawExpr,NewNrs,NewRawExpr) :-
334		map_over_raw_expr(RawExpr,raw_update_file_nrs3(NewNrs),NewRawExpr).
335
336		:- use_module(library(lists),[nth1/3]).
337		raw_update_file_nrs3(NewNrs,OldRaw,NewRaw) :-
338		update_raw_position_info(OldRaw,Pos,UpdatedRaw,NewPos),
339		update_position_filenumber(Pos,OldNr,NewPos,NewNr),
340		(nth1(OldNr,NewNrs,NewNr) -> true ; write(unknown_file_nr(OldNr)),nl,fail),
341		!,
342		recur_over_raw_expr(UpdatedRaw,raw_update_file_nrs3(NewNrs),NewRaw).
343		raw_update_file_nrs3(NewNrs,OldRaw,NewRaw) :-
344		recur_over_raw_expr(OldRaw,raw_update_file_nrs3(NewNrs),NewRaw).
345
346		% ---------------------------------
347
348		% raw set_extension or comprehension_set or similar
349		raw_special_set_term(SymTerm) :- raw_symbolic_annotation(SymTerm,Term),!, raw_special_set_term(Term).
350		raw_special_set_term(comprehension_set(_,_,_)).
351		raw_special_set_term(event_b_comprehension_set(_,_,_,_)).
352		raw_special_set_term(lambda(_,_,_,_)).
353		raw_special_set_term(quantified_intersection(_,_,_,_)).
354		raw_special_set_term(quantified_union(_,_,_,_)).
355		raw_special_set_term(sequence_extension(_,_)).
356		raw_special_set_term(set_extension(_,_)).
357
358		% check if we have a symbolic annotation and transform into regular raw term without annotation:
359		raw_symbolic_annotation(symbolic_composition(A,B,C),composition(A,B,C)).
360		raw_symbolic_annotation(symbolic_comprehension_set(Pos,Ids,Body),
361		comprehension_set(Pos,Ids,Body)).
362		raw_symbolic_annotation(symbolic_event_b_comprehension_set(Pos,Ids,Pred,Body),
363		event_b_comprehension_set(Pos,Ids,Pred,Body)).
364		raw_symbolic_annotation(symbolic_lambda(Pos,Ids,Pred,Expr),
365		lambda(Pos,Ids,Pred,Expr)).
366		raw_symbolic_annotation(symbolic_quantified_union(A,B,C,D),quantified_union(A,B,C,D)).
367
368		% simple raw operators whose first argument is a position and all other are raw formulas
369		raw_operator(add).
370		raw_operator(add_real).
371		raw_operator(block).
372		raw_operator(card).
373		raw_operator(cartesian_product).
374		raw_operator(composition).
375		raw_operator(concat).
376		raw_operator(conjunct).
377		raw_operator(convert_bool).
378		raw_operator(convert_real).
379		raw_operator(convert_int_floor).
380		raw_operator(convert_int_ceiling).
381		%raw_operator(couple).
382		%raw_operator(definition).
383		raw_operator(description).
384		raw_operator(disjunct).
385		raw_operator(div).
386		raw_operator(div_real).
387		raw_operator(domain).
388		raw_operator(domain_restriction).
389		raw_operator(domain_subtraction).
390		raw_operator(equal).
391		raw_operator(equivalence).
392		raw_operator(first).
393		raw_operator(first_projection).
394		raw_operator(front).
395		raw_operator(general_concat).
396		raw_operator(general_union).
397		raw_operator(greater).
398		raw_operator(greater_equal).
399		raw_operator(identifier).
400		raw_operator(identity).
401		raw_operator(if_then_else).
402		raw_operator(image).
403		raw_operator(implication).
404		raw_operator(interval).
405		raw_operator(intersection).
406		raw_operator(last).
407		raw_operator(less).
408		raw_operator(less_equal).
409		raw_operator(less_real).
410		raw_operator(less_equal_real).
411		raw_operator(max).
412		raw_operator(member).
413		raw_operator(minus_or_set_subtract).
414		raw_operator(minus).
415		raw_operator(minus_real).
416		raw_operator(min).
417		raw_operator(multiplication).
418		raw_operator(multiplication_real).
419		raw_operator(mult_or_cart).
420		raw_operator(negation).
421		raw_operator(not_equal).
422		raw_operator(not_member).
423		raw_operator(not_subset_strict).
424		raw_operator(not_subset).
425		raw_operator(overwrite).
426		raw_operator(partial_function).
427		raw_operator(perm).
428		raw_operator(pow_subset).
429		raw_operator(power_of).
430		raw_operator(power_of_real).
431		raw_operator(range).
432		raw_operator(range_restriction).
433		raw_operator(range_subtraction).
434		raw_operator(rec_entry).
435		raw_operator(reverse).
436		raw_operator(seq).
437		raw_operator(size).
438		raw_operator(subset_strict).
439		raw_operator(subset).
440		raw_operator(tail).
441		raw_operator(total_injection).
442		raw_operator(total_function).
443		raw_operator(trans_function).
444		raw_operator(unary_minus).
445		raw_operator(unary_minus_real).
446		raw_operator(union).
447		% external_function_call, ... : treated in list_operator
448		%raw_operator(Op) :- print(uncovered_op(Op)),nl,fail.
449		% TO DO: add more operators
450
451		raw_operator_term(Term) :- functor(Term,Op,_), raw_operator(Op). % TODO: match arity
452
453		raw_literal_term(boolean_true(_)).
454		raw_literal_term(boolean_false(_)).
455		raw_literal_term(integer(_,_)).
456		raw_literal_term(multiline_template(_,_)).
457		raw_literal_term(real(_,_)).
458		raw_literal_term(string(_,_)).