1% BEGIN LICENSE BLOCK
2% Version: CMPL 1.1
3%
4% The contents of this file are subject to the Cisco-style Mozilla Public
5% License Version 1.1 (the "License"); you may not use this file except
6% in compliance with the License.  You may obtain a copy of the License
7% at www.eclipse-clp.org/license.
8% 
9% Software distributed under the License is distributed on an "AS IS"
10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
11% the License for the specific language governing rights and limitations
12% under the License. 
13% 
14% The Original Code is  The ECLiPSe Constraint Logic Programming System. 
15% The Initial Developer of the Original Code is  Cisco Systems, Inc. 
16% Portions created by the Initial Developer are
17% Copyright (C) 2006 Cisco Systems, Inc.  All Rights Reserved.
18% 
19% Contributor(s): Joachim Schimpf.
20% 
21% END LICENSE BLOCK
22% ----------------------------------------------------------------------
23% System:	ECLiPSe Constraint Logic Programming System
24% Component:	ECLiPSe III compiler
25% Version:	$Id: compiler_normalise.ecl,v 1.24 2013/02/26 01:21:20 jschimpf Exp $
26% ----------------------------------------------------------------------
27
28:- module(compiler_normalise).
29
30:- comment(summary, "ECLiPSe III compiler - source code normaliser").
31:- comment(copyright, "Cisco Technology Inc").
32:- comment(author, "Joachim Schimpf, Kish Shen").
33:- comment(date, "$Date: 2013/02/26 01:21:20 $").
34
35:- comment(desc, html("
36	This module creates the normalised form of the source predicate on
37	which the subsequent compiler passes do their work.
38	<P>
39	The clause structure is destroyed and replaced by inline disjunction.
40	The idea being that the compiler will treat disjunctions such that
41	we don't lose anything by doing so.
42	<P>
43	The decision to treat disjunctions directly implies that the bodies
44	have forks and joins of control flow, which makes everything much
45	more complicated compared to a conjunction-only clause compiler.
46	The upside is that there is more scope for optimization, e.g.
47	more sharing of the same environment, less data movement.
48	<P>
49	In the normalised form, the code is generally put in to a form that
50	is more convenient for later processing:
51	<UL>
52	<LI>wrappers identify type of item
53	<LI>lists of goals rather than comma/semicolon structures
54	</UL>
55	The constituents of a normalised source are:
56	<PRE>
57	Pred ::=	Conjunction
58
59	Conjunction ::=	[Goal|...]
60
61	Goal ::=	SimpleGoal
62		|	Disjunction
63
64	SimpleGoal ::=	goal{Term, ...}		% also used for head
65
66	Disjunction ::=	disjunction{Branches, ...}
67
68	Branches ::=	[Conjunction|...]
69
70	Term ::=	variable{...}
71		|	structure{...}
72		|	ground_structure{...}	% not yet done
73		|	[Term|...]		% list
74		|	AtomicTerm		% atomic terms literally
75	</PRE>
76
77")).
78
79:- lib(hash).
80
81:- use_module(compiler_common).
82
83:- import print_goal_state/3 from compiler_analysis.
84
85:- import
86	meta_index/2,
87	get_attribute/3
88   from sepia_kernel.
89
90
91% Utilities to deal with (optionally uninstantiated) annotated terms
92:- local op(700, xfx, =:).
93Var =: _Template :- var(Var), !.
94%Term =: Term2 :- verify instance(Term, Term2), Term = Term2.	% SLOW!
95Term =: Term.
96
97varg(I, T, A) :- ( var(T) -> true ; arg(I, T, A) ).
98
99ann_update_term(_NewTermAnn, Ann, _NewAnn) :- var(Ann), !.
100ann_update_term(NewTermAnn, Ann, NewAnn) :-
101	type_of(NewTermAnn, Type),
102	update_struct(annotated_term, [term:NewTermAnn,type:Type], Ann, NewAnn).
103
104ann_location(Ann, '', 0, 0, 0) :- var(Ann), !.
105ann_location(annotated_term{file:File,line:Line,from:From,to:To}, File, Line, From, To).
106		
107
108%----------------------------------------------------------------------
109
110:- export normalize_clauses_annotated/6.
111:- comment(normalize_clauses_annotated/6, [
112    summary:"Transforms a list of clauses into the normalised predicate representation",
113    args:[
114	"Clauses":"A list of clauses for a single predicate",
115	"AnnClauses":"A corresponding list of annotated clauses (or uninstantated)",
116	"Normalised":"The normalised, ground form of the predicate",
117	"VarCount":"Number of distinct variables in the normalised code",
118	"Options":"Options",
119	"Module":"Context module"
120    ],
121    amode:normalize_clauses_annotated(+,+,-,-,+,+),
122    desc:ascii("
123	Build the ground representation of a single predicate (clause list).
124
125	This deals with:
126	    -	replacing variables with descriptors (struct variable())
127	    	and assigning an integer variable identifier.
128		There is a fresh descriptor for every occurrence!
129	    -	wrapping structures into descriptors (struct structure())
130	    -	flattening conjunctions and disjunctions
131	    -	modules (lookup and context), including tool->tool_body
132	    -	variable goals -> metacall
133	    -	classifying goals as simple or regular
134
135	A normalised body or any other conjunction is a list of subgoals.
136	A normalised disjunction is a struct disjunction()
137	A normalised other subgoal is a struct goal()
138    ")
139]).
140
141normalize_clauses_annotated(Clauses, AnnClauses, NormClauses, VarCount, Options, Module) :-
142	normalize_clause_list(Clauses, AnnClauses, NormClauses, VarCount, Options, Module).
143%	reorder_goals(NormClauses0, NormClauses).
144
145
146%----------------------------------------------------------------------
147% Method for dealing with variables:
148% In the normalised representation, variables are replaced by
149% variable{} descriptors, initially with uninstantiated varid-fields.
150% A list of these descriptors is collected, and used at the end by
151% assign_varids/3 to fill in the varid-fields.
152%
153% Handling of cuts in control constructs:
154%	call(!)		local effect
155%	once(!)		local effect
156%	not(!)		local effect
157%	(! -> ...)	local effect (was error in ECLiPSe I)
158%	(... -> !)	global effect
159%	(! ; ...)	global effect
160%	(... ; !)	global effect
161%
162% Handling of 'true':
163%	true/0 should really be removed completely in this step. However,
164%	historically true/0 has been a regular goal in ECLiPSe, and
165%	is used to force waking before cuts, etc.  So removing it completely
166%	would break old code in subtle ways. We therefore remove it only if
167%	it is followed by a regular goal (including disjunction and cut),
168%	or if it occurs at the end of a branch.
169%
170% Disjunctions:
171%	Disjunctions are flattened as much as possible.
172%----------------------------------------------------------------------
173
174:- mode normalize_body(?,?,+,+,-,+,+,-,-,+,+,+,+).
175normalize_body(Var, AnnVar, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, _Last) :-
176	var(Var), !,
177	ann_update_term(call(AnnVar), AnnVar, AnnCall),
178	normalize_goal(call(Var), AnnCall, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM).
179
180normalize_body(true, _Ann, _Branch, CallNr, CallNr, _Cut, Vs, Vs, Goals, Goals, _LMP, _CM, last) :- !.
181	% remove true/0 at end of branches
182
183%normalize_body(call(G), Ann, Branch, CallNr0, CallNr, _Cut, Vs0, Vs, Goals0, Goals, _LMP, CM, Last) :-
184%	nonvar(G), !,
185%	Goals0 = [SavecutGoal|Goals1],
186%	same_call_pos(Branch, CallNr0, CallNr1, CallPos0),
187%	savecut_goal(CallPos0, Vs0, Vs1, LocalCut, SavecutGoal),
188%	% cuts have local effect!
189%        Ann =: annotated_term{term:call(AnnG)},
190%        normalize_body(G, AnnG, Branch, CallNr1, CallNr, LocalCut, Vs1, Vs, Goals1, Goals, CM-any, CM, Last).
191
192normalize_body(once(G), Ann, Branch, CallNr0, CallNr, _Cut, Vs0, Vs, Goals0, Goals, _LMP, CM, _Last) :- !,
193	Goals0 = [SavecutGoal|Goals1],
194	same_call_pos(Branch, CallNr0, CallNr1, CallPos0),
195	savecut_goal(CallPos0, Vs0, Vs1, LocalCut, SavecutGoal),
196	% cuts have local effect!
197        Ann =: annotated_term{term:once(AG)},
198        normalize_body(G, AG, Branch, CallNr1, CallNr2, LocalCut, Vs1, Vs2, Goals1, Goals2, CM-any, CM, any),
199	Goals2 = [CuttoGoal|Goals],
200	same_call_pos(Branch, CallNr2, CallNr, CallPos1),
201	cutto_goal(CallPos1, Vs2, Vs, LocalCut, CuttoGoal).
202
203normalize_body(not(G), Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals0, Goals, LMP, CM, Last) :-
204	LMP=LM-_, get_flag((not)/1, definition_module, sepia_kernel)@LM,
205	!,
206        Ann =: annotated_term{term:not(AG)},
207        ann_update_term(\+AG, Ann, Ann0),
208        normalize_body(\+G, Ann0, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals0, Goals, LMP, CM, Last).
209
210normalize_body(\+G, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals0, Goals, LMP, CM, Last) :- !,
211        Ann =: annotated_term{term:(\+AG)},
212        ann_update_term(fail, Ann, AnnFail),
213        ann_update_term(true, Ann, AnnTrue),
214        ann_update_term((AG->AnnFail), Ann, AnnCond),
215        ann_update_term((AnnCond;AnnTrue), Ann, AnnITE),
216        normalize_body((G->fail;true), AnnITE, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals0, Goals, LMP, CM, Last).
217
218normalize_body((G1->G2), Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals0, Goals, _LMP, CM, _Last) :- !,
219	% this is a ->/2 that's _not_ inside a ;/2
220	Goals0 = [SavecutGoal|Goals1],
221	same_call_pos(Branch, CallNr0, CallNr1, CallPos0),
222	savecut_goal(CallPos0, Vs0, Vs1, LocalCut, SavecutGoal),
223	% cuts have local effect!
224        Ann =: annotated_term{term:(AG1->AG2)},
225        normalize_body(G1, AG1, Branch, CallNr1, CallNr2, LocalCut, Vs1, Vs2, Goals1, Goals2, CM-any, CM, any),
226	Goals2 = [CuttoGoal|Goals3],
227	same_call_pos(Branch, CallNr2, CallNr3, CallPos1),
228	cutto_goal(CallPos1, Vs2, Vs3, LocalCut, CuttoGoal),
229	normalize_body(G2, AG2, Branch, CallNr3, CallNr, Cut, Vs3, Vs, Goals3, Goals, CM-any, CM, last).
230
231	% TODO: compile softcut!  Preliminary: metacall it.
232normalize_body((G1*->G2;G3), Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, Last) ?-
233	LMP=LM-_, get_flag((*->)/2, definition_module, sepia_kernel)@LM,
234	!,
235	ann_update_term(call(Ann), Ann, AnnCall),
236	normalize_body(call(G1*->G2;G3), AnnCall, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, Last).
237
238normalize_body((G1;G2), Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, _LMP, CM, _Last) :- !,
239	Goals = [SavecutGoal,disjunction{callpos:CallPos,branches:Branches}|Goals0],
240	same_call_pos(Branch, CallNr0, CallNr1, CallPos0),
241	savecut_goal(CallPos0, Vs0, Vs1, DisjCut, SavecutGoal),
242	new_call_pos(Branch, CallNr1, CallNr2, _CallPos),
243	new_call_pos(Branch, CallNr2, CallNr, CallPos),
244        Ann =: annotated_term{term:(AG1;AG2)},
245	normalize_left_branch(G1, AG1, CallPos, 1, BranchNr1, Cut, DisjCut, Vs1, Vs2, Branches, Branches1, CM-any, CM),
246	normalize_right_branch(G2, AG2, CallPos, BranchNr1, _NBranches, Cut, DisjCut, Vs2, Vs, Branches1, [], CM-any, CM).
247
248normalize_body((G1,G2), Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, _LMP, CM, Last) :- !,
249	% this could be changed such that the lookup module propagates
250	% through the comma (would be incompatible with Eclipse =< 5)
251	Ann =: annotated_term{term:(AG1,AG2)},
252	( G1 == true, starts_regular(G2, CM) ->
253	    % a true followed by a regular goal: eliminate the true/0
254	    normalize_body(G2, AG2, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, CM-any, CM, Last)
255	;
256	    normalize_body(G1, AG1, Branch, CallNr0, CallNr1, Cut, Vs0, Vs1, Goals, Goals1, CM-any, CM, any),
257	    normalize_body(G2, AG2, Branch, CallNr1, CallNr, Cut, Vs1, Vs, Goals1, Goals0, CM-any, CM, Last)
258	).
259
260normalize_body(G@M, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, _CM, Last) :-
261	LMP=LM-_, get_flag((@)/2, definition_module, sepia_kernel)@LM,
262        !,
263	% this could be changed such that the lookup module propagates
264	% through the @ (would be incompatible with Eclipse =< 5)
265	Ann =: annotated_term{term:(AG@_AM)},
266        ( atom(M) ->
267            normalize_body(G, AG, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, M, Last)
268	; var(G) ->
269	    ann_update_term(call(AG), Ann, AnnCall),
270	    normalize_goal(call(G), AnnCall, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, M)
271	;
272	    normalize_goal(G, AG, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, M)
273	).
274
275normalize_body(LM:G, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, Last) :-
276	atom(LM), nonvar(G),
277	LMP=LMC-_, get_flag((:)/2, definition_module, sepia_kernel)@LMC,
278	!,
279        Ann =: annotated_term{term:(_ALM:AG)},
280        normalize_body(G, AG, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LM-exported, CM, Last).
281
282normalize_body(!, _Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, _LMP, _CM, _Last) :- !,
283	Goals = [CuttoGoal|Goals0],
284	same_call_pos(Branch, CallNr0, CallNr, CallPos),
285	cutto_goal(CallPos, Vs0, Vs, Cut, CuttoGoal).
286
287normalize_body(X=Y, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, _Last) :- !,
288        simplify_unification(X=Y, Ann, UnifGoals, AnnUnifGoals),
289	(
290	    foreach(UnifGoal, UnifGoals),
291	    foreach(AnnUnifGoal, AnnUnifGoals),
292	    fromto(CallNr0,CallNr1,CallNr2,CallNr),
293	    fromto(Vs0,Vs1,Vs2,Vs),
294	    fromto(Goals,Goals1,Goals2,Goals0),
295	    param(Branch,Cut,LMP,CM)
296	do
297	    normalize_goal(UnifGoal, AnnUnifGoal, Branch, CallNr1, CallNr2, Cut, Vs1, Vs2, Goals1, Goals2, LMP, CM)
298	).
299
300normalize_body(G, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM, _Last) :-
301        normalize_goal(G, Ann, Branch, CallNr0, CallNr, Cut, Vs0, Vs, Goals, Goals0, LMP, CM).
302
303
304normalize_goal(G, AnnG, Branch, CallNr0, CallNr, _Cut, Vs0, Vs, [Goal|Goals], Goals, LM-Vis, CM) :-
305	callable(G),
306	!,
307	AnnG =: annotated_term{term:GAnn},
308	ann_location(AnnG, File, Line, From, To),
309	Goal = goal{
310	    kind:Kind,
311	    callpos:CallPos,
312	    definition_module:DM,
313	    lookup_module:LM1,
314	    functor:N1/A1,
315	    args:NormArgs,
316            path:File,
317            line:Line,
318            from:From,
319            to:To
320	},
321	functor(G, N, A),
322	get_pred_info(Vis, LM, N/A, DM, ToolBody, CallType),
323	( ToolBody = N1/A1 -> 			% replace tool with tool body
324	    LM1=DM,
325	    ann_update_term(CM, AnnG, AnnCM),
326	    normalize_term(CM, AnnCM, NormCM, Vs0, Vs1, =),	% CM may be a variable
327	    ModuleArg = [NormCM]
328	;
329	    N1=N, A1=A, LM1=LM,
330	    Vs1=Vs0, ModuleArg = []
331	),
332	( CallType = external ->
333	    same_call_pos(Branch, CallNr0, CallNr, CallPos),
334	    Kind = simple
335	;
336	    new_call_pos(Branch, CallNr0, CallNr, CallPos),
337	    Kind = regular
338	),
339	(					% normalize arguments
340	    for(I,1,A),
341	    fromto(NormArgs,[NormArg|MoreArgs],MoreArgs,ModuleArg),
342	    fromto(Vs1,Vs2,Vs3,Vs),
343	    param(G,GAnn)
344	do
345	    arg(I, G, Arg),
346	    varg(I, GAnn, AnnArg),
347	    normalize_term(Arg, AnnArg, NormArg, Vs2, Vs3, =)
348	    % ( Vs2==Vs3 -> term is ground ; true )
349	).
350normalize_goal(G, AnnG, _, _, _, _, _, _, _, _, LM, _) :-
351	compiler_event(#illegal_goal, term, AnnG, G, LM).
352%	compiler_error(AnnG, term, "Illegal goal: %QVw", [G]).
353
354
355    % Hack: check whether a preceding true/0 can be eliminated
356    % Fail for simple goals, control constructs, and when in doubt.
357    starts_regular((G,_), LM) ?- !, starts_regular(G, LM).
358    starts_regular(LM:G, _LM) ?- !, ( var(LM) -> true ; starts_regular(G, LM) ).
359    starts_regular(G@CM, LM) ?- !, ( var(CM) -> true ; starts_regular(G, LM) ).
360    starts_regular(!, _) ?- !, fail.
361    starts_regular(cut_to(_), _) ?- !, fail.
362    starts_regular((_;_), _) ?- !, fail.
363    starts_regular((_->_), _) ?- !, fail.
364    starts_regular(not(_), _) ?- !, fail.
365    starts_regular(\+(_), _) ?- !, fail.
366    starts_regular(once(_), _) ?- !, fail.
367    starts_regular(Goal, LM) :-
368	callable(Goal),
369	current_module(LM),
370	functor(Goal, F, N),
371	% also succeeds if F/N not defined yet
372	\+ get_flag(F/N, call_type, external)@LM.
373
374
375    % Look up relevant properties of the called predicate.
376    % If it is not known yet, assume defaults (regular, non-tool, []-module).
377    get_pred_info(ReqVis, LM, Pred0, DM, ToolBody, CallType) :-
378	(
379	    current_module(LM),
380            virtual_pred(Pred0, Pred, Extra),
381	    get_flag(Pred, visibility, Vis)@LM,
382	    required_visibility(ReqVis, Vis)
383	->
384
385	    ( get_flag(Pred, tool, on)@LM ->
386		tool_body(Pred, Body/N, DM)@LM,
387                N1 is N+Extra,
388                ToolBody = Body/N1
389	    ;
390		ToolBody = none,
391		get_flag(Pred, definition_module, DM)@LM
392	    ),
393	    get_flag(Pred, call_type, CallType)@LM
394	;
395	    % Nothing known about Pred, assume defaults
396	    DM = [], ToolBody = none, CallType = prolog
397	).
398
399    required_visibility(any, _) :- !.
400    required_visibility(exported, exported) :- !.
401    required_visibility(exported, reexported).
402
403    % Pretend existence of call/Any and :/Any
404    virtual_pred(Pred, Pred, 0).
405    virtual_pred(call/N, call/1, Extra) :- N>1, Extra is N-1.
406    virtual_pred((:)/N, (:)/2, Extra) :- N>2, Extra is N-2.
407
408
409normalize_left_branch((G1->G2), Ann, DisjCallPos, BranchNr0, BranchNr, Cut, DisjCut, Vs0, Vs, Branches, Branches0, _LM, CM) ?- !,
410	% we have an if-then-else (a branch of the disjunction that gets cut)
411	Branches = [[SavecutGoal|Goals]|Branches0],
412	new_branch(DisjCallPos, BranchNr0, BranchNr, BranchPos),
413	same_call_pos(BranchPos, 1, CallNr1, CallPos1),
414	savecut_goal(CallPos1, Vs0, Vs1, LocalCut, SavecutGoal),
415        Ann =: annotated_term{term:(AG1->AG2)},
416	normalize_body(G1, AG1, BranchPos, CallNr1, CallNr2, LocalCut, Vs1, Vs2, Goals, Goals1, CM-any, CM, any),
417	Goals1 = [CuttoGoal|Goals2],
418	same_call_pos(BranchPos, CallNr2, CallNr3, CallPos2),
419	cutto_goal(CallPos2, Vs2, Vs3, DisjCut, CuttoGoal),
420	normalize_body(G2, AG2, BranchPos, CallNr3, _CallNr, Cut, Vs3, Vs, Goals2, [], CM-any, CM, last).
421normalize_left_branch((G1;G2), Ann, DisjCallPos, BranchNr0, BranchNr, Cut, DisjCut, Vs0, Vs, Branches, Branches0, _LM, CM) ?-
422	% An if-then-else in the left alternative needs its own choicepoint!
423	nonvar(G1), G1 \= (_ -> _),
424	!,
425	% This disjunction can be merged with the parent one
426        Ann =: annotated_term{term:(AG1;AG2)},
427        normalize_left_branch(G1, AG1, DisjCallPos, BranchNr0, BranchNr1, Cut, DisjCut, Vs0, Vs1, Branches, Branches1, CM-any, CM),
428	normalize_right_branch(G2, AG2, DisjCallPos, BranchNr1, BranchNr, Cut, DisjCut, Vs1, Vs, Branches1, Branches0, CM-any, CM).
429normalize_left_branch(G1, Ann, DisjCallPos, BranchNr0, BranchNr, Cut, _DisjCut, Vs0, Vs, [Goals|Branches], Branches, LM, CM) :-
430	% A normal (uncut) branch of the disjunction
431	new_branch(DisjCallPos, BranchNr0, BranchNr, BranchPos),
432	normalize_body(G1, Ann, BranchPos, 1, _CallNr, Cut, Vs0, Vs, Goals, [], LM, CM, last).
433
434
435normalize_right_branch((G1;G2), Ann, DisjCallPos, BranchNr0, BranchNr, Cut, LocalCut, Vs0, Vs, Branches, Branches0, _LM, CM) ?- !,
436	% This disjunction can be merged with the parent one
437        Ann =: annotated_term{term:(AG1;AG2)},
438        normalize_left_branch(G1, AG1, DisjCallPos, BranchNr0, BranchNr1, Cut, LocalCut, Vs0, Vs1, Branches, Branches1, CM-any, CM),
439	normalize_right_branch(G2, AG2, DisjCallPos, BranchNr1, BranchNr, Cut, LocalCut, Vs1, Vs, Branches1, Branches0, CM-any, CM).
440normalize_right_branch(G1, Ann, DisjCallPos, BranchNr0, BranchNr, Cut, _LocalCut, Vs0, Vs, [Goals|Goals0], Goals0, LM, CM) :-
441	new_branch(DisjCallPos, BranchNr0, BranchNr, Branch),
442	normalize_body(G1, Ann, Branch, 1, _CallNr, Cut, Vs0, Vs, Goals, [], LM, CM, last).
443
444
445% Normalise a list of standard clauses, facts, etc
446
447% normalize_clause_list(+Clauses, ?AnnClauses, -NormClause, -VarCount, +Options, +CM)
448normalize_clause_list([Clause], [AnnClause], NormClause, VarCount, Options, CM) :- !,
449	NormClause = [HeadMarker, SavecutGoal |NormClause1],
450	same_call_pos([], 1, _CallNr, CallPos),
451	head_marker(Clause, CM, CallPos, HeadMarker, Arity),
452	savecut_goal(CallPos, Vs, Vs1, Cut, SavecutGoal),
453	normalize_clause(Clause, AnnClause, [], NormClause1, CM, Cut, Vs1, []),
454	assign_varids(Vs, Arity, VarCount, Options).
455normalize_clause_list(Clauses, AnnClauses, NormClauses, VarCount, Options, CM) :-
456	Clauses = [SomeClause|_],
457	NormClauses = [
458	    HeadMarker,
459	    SavecutGoal, 
460	    disjunction{callpos:CallPos,branches:NormBranches}
461	],
462	same_call_pos([], 1, CallNr1, CallPos0),
463	head_marker(SomeClause, CM, CallPos0, HeadMarker, Arity),
464	savecut_goal(CallPos0, Vs0, [], Cut, SavecutGoal),
465	new_call_pos([], CallNr1, CallNr2, _CallPos),
466	new_call_pos([], CallNr2, _CallNr, CallPos),
467%	new_call_pos([], CallNr1, _CallNr, CallPos),
468	(
469	    foreach(Clause,Clauses),
470            foreach(AnnClause,AnnClauses),
471	    foreach(Goals,NormBranches),
472	    fromto(1,BranchNr1,BranchNr2,_BranchNr),
473	    fromto(Arity,VarId1,VarId2,VarCount),
474	    param(CallPos,CM,Cut,Vs0,Options)
475	do
476	    new_branch(CallPos, BranchNr1, BranchNr2, ClauseBranch),
477	    normalize_clause(Clause, AnnClause, ClauseBranch, Goals, CM, Cut, Vs, Vs0),
478	    assign_varids(Vs, VarId1, VarId2, Options)
479	).
480
481    normalize_clause(Clause, AnnClause, Branch, Goals, CM, Cut, Vs, Vs0) :-
482	clause_head_body(Clause, AnnClause, Head, Body, AnnHead, AnnBody, HeadType, CM),
483	same_call_pos(Branch, 1, CallNr, CallPos),
484	normalize_head(HeadType, Head, AnnHead, CallPos, Goals, Goals1, Vs, Vs1),
485	normalize_body(Body, AnnBody, Branch, CallNr, _CallNr, Cut, Vs1, Vs0, Goals1, [], CM-any, CM, last).
486
487    :- mode clause_head_body(+,?,-,-,-,-,-,+).
488    clause_head_body((H0:- -?->B0), Ann, H, B, AH, AB, HeadType, CM) ?-
489	get_flag((?-)/2, definition_module, sepia_kernel)@CM,
490	!,
491        Ann =: annotated_term{term:(AH:-AnnMatch)},
492        AnnMatch =: annotated_term{term:(-?->AB)},
493	H=H0, B=B0, HeadType = (?=).
494    clause_head_body((H0:-B0), Ann, H, B, AH, AB, HeadType, _CM) ?- !,
495        Ann =: annotated_term{term:(AH:-AB)},
496	H=H0, B=B0, HeadType = (=).
497    clause_head_body((H0?-B0), Ann, H, B, AH, AB, HeadType, CM) ?-
498	get_flag((?-)/2, definition_module, sepia_kernel)@CM,
499	!,
500        Ann =: annotated_term{term:(AH?-AB)},
501	H=H0, B=B0, HeadType = (?=).
502    clause_head_body(H, AH, H, true, AH, AnnTrue, =, _CM) :-
503        ann_update_term(true, AH, AnnTrue).
504
505
506head_marker(Clause, CM, CallPos, Goal, Arity) :-
507	Goal = goal{
508	    kind:head, callpos:CallPos,
509	    lookup_module:CM, definition_module:CM,
510	    functor:N/Arity, args:HeadArgs},
511    	clause_head_body(Clause, _, H, _, _, _, _, CM),
512	functor(H, N, Arity),
513	(
514	    for(I,1,Arity),
515	    foreach(HeadArg,HeadArgs)
516	do
517	    new_vardesc(I, HeadArg)
518	).
519
520
521% Create a goal to save the cut position in a new variable
522% This will be optimized away later if the variable remains unused
523
524savecut_goal(CallPos, Vs0, Vs1, CutVar, Goal) :-
525	Goal = goal{
526	    kind:simple,
527	    callpos:CallPos,
528	    definition_module:sepia_kernel,
529	    lookup_module:sepia_kernel,
530	    functor:get_cut/1,
531	    args:[NormCutVar]
532	},
533	new_aux_variable(CutVar, NormCutVar, Vs0, Vs1).
534
535
536cutto_goal(CallPos, Vs0, Vs1, CutVar, Goal) :-
537	Goal = goal{
538	    kind:simple,
539	    callpos:CallPos,
540	    definition_module:sepia_kernel,
541	    lookup_module:sepia_kernel,
542	    functor:cut_to/1,
543	    args:[NormCutVar]
544	},
545	normalize_term(CutVar, _, NormCutVar, Vs0, Vs1, =).
546
547
548
549% Normalised term representation:
550%
551%	variables	struct(variable)
552%	attr.variables	struct(attrvar) - only if AttrFlag == (?=) !
553%	atomic		as such
554%	lists		as such
555%	structs		structure(structure)
556%	ground struct	ground_structure(ground)   TODO
557
558:- mode normalize_term(?,?,-,-,+,+).
559normalize_term(X, AnnX, Desc, Vs, Vs0, AttrFlag) :-
560	var(X), !,
561	normalize_var(X, AnnX, Desc, Vs, Vs0, AttrFlag, _VarId).
562normalize_term([X|Xs], Ann, [Y|Ys], Vs, Vs0, AttrFlag) :- !,
563	Ann =: annotated_term{term:[AnnX|AnnXs]},
564	normalize_term(X, AnnX, Y, Vs, Vs1, AttrFlag),
565	normalize_term(Xs, AnnXs, Ys, Vs1, Vs0, AttrFlag).
566normalize_term(X, Ann, structure{name:N,arity:A,args:Args}, Vs, Vs0, AttrFlag) :-
567	compound(X), !,
568	Ann =: annotated_term{term:AnnX},
569	functor(X, N, A),
570	(
571	    for(I,1,A),
572	    foreach(NormArg,Args),
573	    fromto(Vs,Vs2,Vs1,Vs0),
574	    param(X,AnnX,AttrFlag)
575	do
576	    arg(I, X, Arg),
577	    varg(I, AnnX, AnnArg),
578	    normalize_term(Arg, AnnArg, NormArg, Vs2, Vs1, AttrFlag)
579	).
580normalize_term(X, _Ann, X, Vs, Vs, _AttrFlag) :- atom(X), !.
581normalize_term(X, _Ann, X, Vs, Vs, _AttrFlag) :- number(X), !.
582normalize_term(X, _Ann, X, Vs, Vs, _AttrFlag) :- string(X), !.
583normalize_term(X, Ann, _, _, _, _) :-
584	( nonvar(Ann) ->
585	    Ann =: annotated_term{file:File,line:Line},
586	    printf(error, "File %w, line %d: ", [File,Line])
587	;
588	    true
589	),
590	type_of(X, Type),
591	printf(error, "Cannot compile term of type %w: %w%n", [Type,X]),
592	exit_block(abort_compile_predicate).
593
594
595normalize_var(X, AnnX, Desc, [X-VarDesc|Vs1], Vs0, AttrFlag, VarId) :-
596	( nonvar(AnnX) ->
597	    VarDesc = variable{source_info:AnnX,varid:VarId}
598	;
599	    VarDesc = variable{source_info:none,varid:VarId}
600	),
601	( meta(X), AttrFlag = (?=) ->
602	    Desc = attrvar{variable:VarDesc,meta:NormMeta},
603	    meta_attr_struct(X, Meta),
604	    normalize_term(Meta, _Ann, NormMeta, Vs1, Vs0, AttrFlag)
605	;
606	    % treat as plain variable when not in matching-clause head
607	    Desc = VarDesc, Vs1 = Vs0
608	).
609
610
611% Build a structure meta/N with all attributes of X
612meta_attr_struct(X, Meta) :-
613	meta_attributes(X, 1, Attrs),
614	Meta =.. [meta|Attrs].
615
616    meta_attributes(X, I, Attrs) :-
617	( meta_index(_Name,I) ->
618	    get_attribute(X, Attr, I),
619	    Attrs = [Attr|Attrs1],
620	    I1 is I+1,
621	    meta_attributes(X, I1, Attrs1)
622	;
623	    Attrs = []
624	).
625
626
627% Introduce a new, auxiliary source variable that was not in the
628% original source, or an additional occurrence of a source variable.
629% Treat occurrences like normal source variables.
630new_aux_variable(X, VarDesc, [X-VarDesc|Vs], Vs) :-
631	VarDesc = variable{source_info:none}.
632
633
634
635% Fill in the variable{varid:} fields with a unique integer >= 1
636% for every distinct variable.  Variables that occur in argument positions
637% will already have numbers assigned - simply copy that to every
638% descriptor for that variable.  Note that we have not yet separated
639% identical variables that occur in parallel branches of a disjunction,
640% that is taken care of in the variable classification pass.
641
642assign_varids(Vs, N0, N, Options) :-
643	keysort(Vs, SortedVs),
644	(
645	    foreach(X-variable{varid:VarId,source_info:Source},SortedVs),
646	    fromto(_OtherVar,X0,X,_),
647	    fromto(0,VarId0,VarId,VarIdN),
648	    fromto(none,Source0,Source,SourceN),
649	    fromto(multi,Occ0,Occ,OccN),
650	    fromto(N0,N1,N2,N3),
651	    param(Options)
652	do
653	    ( X == X0 ->	% same variable, unify IDs
654		N2 = N1,
655		VarId = VarId0,
656		Occ = multi
657	    ; var(VarId0) ->
658		N2 is N1+1,
659		VarId0 = N2,	% assign next number
660		Occ = single
661	    ;
662		head_singleton_check(Occ0, Source0, Options),
663		N2 = N1,	% was already numbered
664		Occ = single
665	    )
666	),
667	( var(VarIdN) ->
668	    N is N3+1,
669	    VarIdN = N		% assign next number
670	;
671	    head_singleton_check(OccN, SourceN, Options),
672	    N = N3		% was already numbered
673	).
674
675
676    % Report only singleton head arguments here (because this is the
677    % last time we have the necessary information).
678    % Other singletons are reported in the variable classification phase.
679    head_singleton_check(single, Source, Options) ?-
680	singleton_warning(Source, Options).
681    head_singleton_check(multi, _, _).
682
683
684
685% From a head, construct a normalised head, which is a pseudo
686% goal of kind:head. The normalised head contains distinct variables
687% these already get their VarIds (1..Arity) assigned here.
688% Head unifications get flattened into a sequence of =/2 goals.
689%
690% p(a) :- ...	is normalised into p(T) :- T?=a, ...
691% p(X,X) :- ...	is normalised into p(X,T) :- X=T, ...
692% p(X,X) ?- ...	is normalised into p(X,T) :- X==T, ...
693% p(X{A}) ?- ... is normalised into into p(X) :- X?=X{A}, ...
694% p(X{A},X{A}) ?- ... is normalised into p(X,T) :- X?=X{A}, T==X, ...
695%
696% attrvar{} descriptors are only created on the rhs of ?=/2, in all other
697% locations, we use simple variable{} descriptors for attributed variables.
698
699normalize_head(HeadType, Head, AnnHead, CallPos, Goals1, Goals, Vs0, Vs) :-
700	AnnHead =: annotated_term{term:HeadAnn},
701	(
702	    foreacharg(Arg,Head,I),
703	    fromto(Vs0,Vs1,Vs3,Vs),
704	    fromto([],Seen1,Seen2,_),
705	    fromto(Goals1,Goals2,Goals3,Goals),
706	    param(HeadType,HeadAnn,CallPos)
707	do
708	    Goal = goal{
709		    kind:simple,
710		    path:File,
711		    line:Line,
712		    from:From,
713		    to:To,
714		    callpos:CallPos,
715		    definition_module:sepia_kernel,
716		    lookup_module:sepia_kernel,
717		    functor:Op/2,
718		    args:[HeadArg,NormArg]
719		},
720	    varg(I, HeadAnn, AnnArg),
721	    ann_location(AnnArg, File, Line, From, To),
722	    ( nonvar(Arg) ->
723		% p(nonvar) :-  becomes  p(T) :- T=nonvar
724		% p(nonvar) ?-  becomes  p(T) :- T?=nonvar
725		Goals2 = [Goal|Goals3],
726		normalize_term(Arg, AnnArg, NormArg, Vs1, Vs3, HeadType),
727		Seen2 = Seen1,
728		Op = HeadType,
729		new_vardesc(I, HeadArg)
730	    ; varnonmember(Arg,Seen1) ->
731		Seen2 = [Arg|Seen1],
732		( meta(Arg), HeadType = (?=) ->
733		    % p(X{A}) ?-  becomes  p(X) :- X?=X{A}
734		    Goals2 = [Goal|Goals3],
735		    Op = HeadType,
736		    normalize_var(Arg, AnnArg, NormArg, Vs1, Vs3, ?=, I),
737		    NormArg = attrvar{variable:HeadArg}
738		;
739		    % Don't create a new variable for the first occurrence.
740		    % p(X) :- ...  remains  p(X) :- ...
741		    normalize_var(Arg, AnnArg, HeadArg, Vs1, Vs3, =, I),
742		    Goals2 = Goals3
743		)
744	    ;
745		% repeat occurrence: T=X (or T==X for matching)
746		Goals2 = [Goal|Goals3],
747		normalize_var(Arg, AnnArg, NormArg, Vs1, Vs3, =, _VarId),
748		Seen2 = Seen1,
749		headtype_varop(HeadType, Op),
750		new_vardesc(I, HeadArg)
751	    )
752	).
753
754headtype_varop(=, =).
755headtype_varop(?=, ==).
756
757varnonmember(_X, []).
758varnonmember(X, [Y|Ys]) :-
759	X \== Y,
760	varnonmember(X, Ys).
761
762
763% Flatten unifications and normalise them such that there is always
764% a variable on the left hand side. The sub-unifications inherit the
765% source annotation from the original unification goal.
766simplify_unification(X=Y, Ann, UnifGoals, AnnUnifGoals) ?-
767	Ann =: annotated_term{term:(AnnX=AnnY)},
768	simplify_unification(X, Y, AnnX, AnnY, Ann, UnifGoals, [], AnnUnifGoals, []).
769
770
771%:- mode simplify_unification(?,?,?,?,?,-,?,-,?).
772simplify_unification(X, Y, AnnX, AnnY, Ann, [X=Y|T], T, [AnnEq|AT], AT) :-
773	var(X), !,
774	ann_update_term(AnnX=AnnY, Ann, AnnEq).
775simplify_unification(X, Y, AnnX, AnnY, Ann, Us, Us0, AnnUs, AnnUs0) :-
776	var(Y), !,
777	simplify_unification(Y, X, AnnY, AnnX, Ann, Us, Us0, AnnUs, AnnUs0).
778simplify_unification(X, Y, _AnnX, _AnnY, _Ann, Us, Us, AnnUs, AnnUs) :-
779	X == Y, !.
780simplify_unification(X, Y, AnnX, AnnY, Ann, L, L0, AnnL, AnnL0) :-
781	functor(X, F, N), functor(Y, F, N), !,
782	AnnX =: annotated_term{term:XAnn},
783	AnnY =: annotated_term{term:YAnn},
784	(
785	    for(I,1,N),
786	    fromto(L,L1,L2,L0),
787	    fromto(AnnL,AnnL1,AnnL2,AnnL0),
788	    param(X,Y,XAnn,YAnn,Ann)
789	do
790	    arg(I, X, AX),
791	    arg(I, Y, AY),
792	    varg(I, XAnn, AnnAX),
793	    varg(I, YAnn, AnnAY),
794	    simplify_unification(AX, AY, AnnAX, AnnAY, Ann, L1, L2, AnnL1, AnnL2)
795	).
796simplify_unification(_X, _Y, _AnnX, _AnnY, Ann, [fail|T], T, [AnnF|AT], AT) :-
797	ann_update_term(fail, Ann, AnnF).
798
799
800/*
801%----------------------------------------------------------------------
802% Reorder a simple basic block prefix
803% - bring indexable tests to the front
804% - bring Var=Var unifications together
805%----------------------------------------------------------------------
806
807reorder_goals([], []).
808reorder_goals(Goals, RGoals) :- Goals = [_|_],
809	reorder_prefix(Goals, RGoals).
810reorder_goals(disjunction{branches:Branches}, disjunction{branches:RBranches}) :-
811	(
812	    foreach(Branch,Branches),
813	    foreach(RBranch,RBranches)
814	do
815	    reorder_goals(Branch, RBranch)
816		
817	).
818
819
820reorder_prefix(Goals, ReorderedGoals) :-
821	extract_and_prioritize_simple_prefix(Goals, KeyPrefix, Rest),
822	keysort(KeyPrefix, SortedKeyPrefix),
823	strip_key(SortedKeyPrefix, SortedPrefix),
824	append(SortedPrefix, Rest, ReorderedGoals).
825
826    strip_key([], []).
827    strip_key([_K-X|KXs], [X|Xs]) :-
828	strip_key(KXs, Xs).
829	
830extract_and_prioritize_simple_prefix([], [], []).
831extract_and_prioritize_simple_prefix([Goal|Goals], Prefix, Rest) :-
832	normalize_unif(Goal, Goal1),
833	( prefix_goal(Goal1, Prio) ->
834	    Prefix = [Prio-Goal1|Prefix0],
835	    extract_and_prioritize_simple_prefix(Goals, Prefix0, Rest)
836	;
837	    Prefix = [],
838	    Rest = [Goal1|Goals]
839	).
840
841:- mode prefix_goal(+,-).
842%prefix_goal(goal{functor:atom/1}, 1) :- !.
843%prefix_goal(goal{functor:atomic/1}, 1) :- !.
844%prefix_goal(goal{functor:number/1}, 1) :- !.
845%prefix_goal(goal{functor:var/1}, 1) :- !.
846%prefix_goal(goal{functor:nonvar/1}, 1) :- !.
847%prefix_goal(goal{functor:integer/1}, 1) :- !.
848%prefix_goal(goal{functor:real/1}, 1) :- !.
849%prefix_goal(goal{functor:rational/1}, 1) :- !.
850%prefix_goal(goal{functor:breal/1}, 1) :- !.
851%prefix_goal(goal{functor:free/1}, 1) :- !.
852%prefix_goal(goal{functor:string/1}, 1) :- !.
853%prefix_goal(goal{functor:meta/1}, 1) :- !.
854%prefix_goal(goal{functor:is_handle/1}, 1) :- !.
855%prefix_goal(goal{functor:is_suspension/1}, 1) :- !.
856prefix_goal(goal{functor:(=)/2,args:[_,Y]}, 1) :- atomic(Y), !.
857prefix_goal(goal{functor:(=)/2,args:[_,[_|_]]}, 2) :- !.
858prefix_goal(goal{functor:(=)/2,args:[_,structure{}]}, 2) :- !.
859prefix_goal(goal{functor:(=)/2,args:[variable{},variable{}]}, 3) :- !.
860prefix_goal(goal{functor:(=)/2,args:[X,Y]}, 4) :- !,
861	printf(warning_output, "Unclassified unification %w%n", [X=Y]).
862
863
864normalize_unif(Goal, NormUnif) :-
865	Goal = goal{functor:(=)/2,args:[X,Y]},
866	Y = variable{},
867	X \= variable{},
868	!,
869	update_struct(goal, args:[Y,X], Goal, NormUnif).
870normalize_unif(Goal, Goal).
871*/
872
873%----------------------------------------------------------------------
874% 
875%----------------------------------------------------------------------
876
877:- export print_normalized_clause/2.
878
879print_normalized_clause(Stream, Clause) :-
880	writeln(Stream, "------ Normalized Source ------"),
881	print_normalized_goal(Stream, 0, Clause).
882
883
884print_normalized_goal(_Stream, _Indent, []).
885print_normalized_goal(Stream, Indent, [Goal|Goals]) :-
886	print_normalized_goal(Stream, Indent, Goal),
887	print_normalized_goal(Stream, Indent, Goals).
888print_normalized_goal(Stream, Indent, disjunction{determinism:BranchDets,arity:A,
889		args:Args,indexvars:IndexVars,callpos:P,branches:Bs,branchheadargs:BHA}) :-
890	indent(Stream, Indent),
891	( foreacharg(BrDet,BranchDets), fromto(semidet,Det1,Det2,Det) do
892	    ( (BrDet==det;BrDet==failure) -> Det2=Det1 ; Det2=nondet )
893	),
894	printf(Stream, "DISJ/%w  (%w, callpos:", [A,Det]),
895	print_call_pos(Stream, P),
896	writeln(Stream, ")"),
897	ArgIndent is Indent+1,
898	( foreach(Arg,Args), param(Stream,ArgIndent) do
899	    indent(Stream, ArgIndent), writeln(Stream, Arg)
900	),
901	indent(Stream, Indent),
902	writeln(Stream, "INDEXES:"),
903	( foreach(Arg,IndexVars), param(Stream,ArgIndent) do
904	    indent(Stream, ArgIndent), writeln(Stream, Arg)
905	),
906	arity(BranchDets, NBranches),
907	( foreach(Branch,Bs), count(BranchI,1,_), param(Stream,Indent,P,A,BHA,BranchDets,NBranches) do
908	    Indent1 is Indent+1,
909	    indent(Stream, Indent),
910	    arg(BranchI, BranchDets, BranchDet),
911	    printf(Stream, "BRANCH/%w (%d of %d, %w, callpos:", [A,BranchI,NBranches,BranchDet]),
912	    append(P, [BranchI], PB),
913	    print_call_pos(Stream, PB),
914	    writeln(Stream, ")"),
915	    ArgIndent is Indent1+1,
916	    ( integer(A), A>0 ->
917		arg(BranchI, BHA, Args),
918		( foreach(Arg,Args), param(Stream,ArgIndent) do
919		    indent(Stream, ArgIndent), writeln(Stream, Arg)
920		)
921	    ;
922		true
923	    ),
924	    print_normalized_goal(Stream, Indent1, Branch)
925	),
926	indent(Stream, Indent),
927	write(Stream, "JOIN  (callpos:"),
928	print_call_pos(Stream, P),
929	writeln(Stream, ")").
930print_normalized_goal(Stream, Indent, goal{kind:K,callpos:P,state:State,
931		lookup_module:LM, functor:F,args:Args,envmap:EAM,envsize:ESize,
932                path:Path,line:Line}) :-
933	indent(Stream, Indent),
934	( K == head -> write(Stream, "HEAD") ; write(Stream, "GOAL") ),
935        printf(Stream, "  %w  (lm:%w, kind:%w, path:%w, line:%w callpos:", [F,LM,K,Path,Line]),
936	print_call_pos(Stream, P),
937	decode_activity_map(EAM,Env),
938	printf(Stream, ", env:%w@%w)%n", [ESize,Env]),
939	ArgIndent is Indent+1,
940	( foreach(Arg,Args), param(Stream,ArgIndent) do
941	    indent(Stream, ArgIndent), writeln(Stream, Arg)
942	),
943	print_goal_state(Stream, Indent, State).
944
945
946%----------------------------------------------------------------------
947% Denormalize (obtain a source suitable for inlining)
948% TODO: with annotations
949% TODO: Catch simple cases of recursion
950% TODO: if local predicates from the compilation module are called,
951%	they can only be called via :/2 if they are exported.
952% TODO: purge redundant get_cuts?
953% Note: context modules are handled correctly, since the tool
954%	calls are already expanded at this point!
955% Note: Unfortunately, we can only restore the annotations partially
956%	(per goal, not per term), but enough for tracing
957%----------------------------------------------------------------------
958
959:- export denormalize_pred/3.
960denormalize_pred([NormHead|NormBody], VarCount, (Head:-Body)) :-
961	dim(Vars, [VarCount]),
962	certainly_once denormalize_head(NormHead, Vars, Head),
963	denormalize_conj(NormBody, Vars, Body).
964
965%denormalize_head(goal{kind:head,functor:F/A,args:NormArgs}, Vars, Head) :-
966%	functor(Head, F, A),
967%	( foreach(NormArg,NormArgs), foreacharg(Arg,Head), param(Vars) do
968%	    denormalize_term(NormArg, Vars, Arg)
969%	).
970
971denormalize_conj([], _Vars, true).
972denormalize_conj([NormGoal|NormGoals], Vars, Conj) :-
973	denormalize_goal(NormGoal, Vars, Goal1),
974	(
975	    foreach(NormGoal,NormGoals),
976	    fromto(Goal1,PrevGoal,Goal,LastGoal),
977	    fromto(Conj,(PrevGoal,Conj2),Conj2,LastGoal),
978	    param(Vars)
979	do
980	    denormalize_goal(NormGoal, Vars, Goal)
981	).
982
983denormalize_goal(disjunction{branches:NormBranches}, Vars, Disj) ?-
984	certainly_once NormBranches = [NormBranch1|NormBranches1],
985	denormalize_conj(NormBranch1, Vars, Alt1),
986	(
987	    foreach(NormBranch,NormBranches1),
988	    fromto(Alt1,PrevAlt,Alt,LastAlt),
989	    fromto(Disj,(PrevAlt;Disj2),Disj2,LastAlt),
990	    param(Vars)
991	do
992	    denormalize_conj(NormBranch, Vars, Alt)
993	).
994denormalize_goal(goal{kind:Kind,functor:F/A,args:NormArgs,lookup_module:LM,definition_module:DM}, Vars, QGoal) ?-
995	verify Kind \== head,
996	( DM==[] -> QGoal=LM:Goal ; QGoal=DM:Goal ),
997	functor(Goal, F, A),
998	( foreach(NormArg,NormArgs), foreacharg(Arg,Goal), param(Vars) do
999	    denormalize_term(NormArg, Vars, Arg)
1000	).
1001
1002%denormalize_term(variable{varid:VarId}, Vars, Var) :-
1003%	arg(VarId, Vars, Var).
1004%denormalize_term(structure{name:F,arity:A,args:NormArgs}, Vars, Term) :-
1005%	functor(Term, F, A),
1006%	( foreach(NormArg,NormArgs), foreacharg(Arg,Term), param(Vars) do
1007%	    denormalize_term(NormArg, Vars, Arg)
1008%	).
1009%denormalize_term([NormArg|NormArgs], Vars, [Arg|Args]) :-
1010%	denormalize_term(NormArg, Vars, Arg),
1011%	denormalize_term(NormArgs, Vars, Args).
1012%denormalize_term(NormTerm, _Vars, Term) :- atomic(NormTerm),
1013%	Term=NormTerm.
1014
1015
1016%----------------------------------------------------------------------
1017% This will leave goal arguments unannotated!
1018% Problem: goal without source location are intermixed!
1019
1020
1021:- export denormalize_pred/5.
1022denormalize_pred([NormHead|NormBody], VarCount, Head, Body, AnnBody) :-
1023	dim(Vars, [VarCount]),
1024	certainly_once denormalize_head(NormHead, Vars, Head),
1025	denormalize_conj(NormBody, Vars, Body, AnnBody).
1026
1027denormalize_head(goal{kind:head,functor:F/A,args:NormArgs}, Vars, Head) :-
1028	functor(Head, F, A),
1029	( foreach(NormArg,NormArgs), foreacharg(Arg,Head), param(Vars) do
1030	    denormalize_term(NormArg, Vars, Arg)
1031	).
1032
1033denormalize_conj([], _Vars, true, _AnnMissing).
1034denormalize_conj([NormGoal|NormGoals], Vars, Conj, AnnConj) :-
1035	denormalize_goal(NormGoal, Vars, Goal1, AnnGoal1),
1036	(
1037	    foreach(NormGoal,NormGoals),
1038	    fromto(Goal1,PrevGoal,Goal,LastGoal),
1039	    fromto(AnnGoal1,AnnPrevGoal,AnnGoal,AnnLastGoal),
1040	    fromto(Conj,(PrevGoal,Conj2),Conj2,LastGoal),
1041	    fromto(AnnConj,AnnConj1,AnnConj2,AnnLastGoal),
1042	    param(Vars)
1043	do
1044	    inherit_annotation((AnnPrevGoal,AnnConj2), AnnPrevGoal, AnnConj1),
1045	    denormalize_goal(NormGoal, Vars, Goal, AnnGoal)
1046	).
1047
1048denormalize_goal(disjunction{branches:NormBranches}, Vars, Disj, AnnDisj) ?-
1049	certainly_once NormBranches = [NormBranch1|NormBranches1],
1050	denormalize_conj(NormBranch1, Vars, Alt1, AnnAlt1),
1051	(
1052	    foreach(NormBranch,NormBranches1),
1053	    fromto(Alt1,PrevAlt,Alt,LastAlt),
1054	    fromto(AnnAlt1,AnnPrevAlt,AnnAlt,AnnLastAlt),
1055	    fromto(Disj,(PrevAlt;Disj2),Disj2,LastAlt),
1056	    fromto(AnnDisj,AnnDisj1,AnnDisj2,AnnLastAlt),
1057	    param(Vars)
1058	do
1059	    inherit_annotation((AnnPrevAlt;AnnDisj2), AnnPrevAlt, AnnDisj1),
1060	    denormalize_conj(NormBranch, Vars, Alt, AnnAlt)
1061	).
1062denormalize_goal(NormGoal, Vars, QGoal, AnnQGoal) ?-
1063	NormGoal = goal{kind:Kind,functor:F/A,args:NormArgs,lookup_module:LM,definition_module:DM},
1064	verify Kind \== head,
1065	( DM==[] -> LDM=LM ; LDM=DM ),
1066	QGoal=LDM:Goal,
1067	functor(Goal, F, A),
1068	annotate_from_norm_goal(Goal, NormGoal, AnnGoal),
1069	inherit_annotation(LDM, AnnGoal, AnnLDM),
1070	inherit_annotation(AnnLDM:AnnGoal, AnnGoal, AnnQGoal),
1071	( foreach(NormArg,NormArgs), foreacharg(Arg,Goal), param(Vars) do
1072	    denormalize_term(NormArg, Vars, Arg)
1073	).
1074
1075denormalize_term(variable{varid:VarId}, Vars, Var) :-
1076	arg(VarId, Vars, Var).
1077denormalize_term(structure{name:F,arity:A,args:NormArgs}, Vars, Term) :-
1078	functor(Term, F, A),
1079	( foreach(NormArg,NormArgs), foreacharg(Arg,Term), param(Vars) do
1080	    denormalize_term(NormArg, Vars, Arg)
1081	).
1082denormalize_term([NormArg|NormArgs], Vars, [Arg|Args]) :-
1083	denormalize_term(NormArg, Vars, Arg),
1084	denormalize_term(NormArgs, Vars, Args).
1085denormalize_term(NormTerm, _Vars, Term) :- atomic(NormTerm),
1086	Term=NormTerm.
1087
1088
1089annotate_from_norm_goal(Term, goal{path:P,line:L,from:F,to:T}, Ann) :-
1090	( var(P) ->
1091	    Ann=annotated_term{term:TermAnn,type:Type,file:'',line:0,from:0,to:0}
1092	;
1093	    Ann=annotated_term{term:TermAnn,type:Type,file:P,line:L,from:F,to:T}
1094	),
1095	functor(Term, N, A),
1096	functor(TermAnn, N, A),	% annotated arguments remain uninstantiated!
1097	type_of(Term, Type).
1098
1099inherit_annotation(_Term, AnnTmpl, _AnnTerm) :- var(AnnTmpl), !.
1100inherit_annotation(Term, AnnTmpl,  AnnTerm) :-
1101	update_struct(annotated_term, [term:Term,type:Type], AnnTmpl, AnnTerm),
1102	type_of(Term, Type).