% Sdda3		5-Oct-86 
% For use on simulator

%% To do:  (look for '%%')
%%	recursion - keep list of call procedures, ignore recursive calls
%%	   	problem: doesn't work for typical procedure working on a list,
%%			 since the list is smaller (different) each time.
%%		possible optimization: "recognize" base case & skip to it
%%	follow atoms, g is 'any atom', all others unique,  does it work?
%%	stats - write heapused, cputime to files (as comments)
%%	worst_case - handle ground terms (copy unify, modify atomic)
%%	handle disjunction - needs worst_case
%%	add cuts where possible to save space
%%	fill in rest of built-ins
%% 	how to handle op?
%%	Handle assert/retract?  call?  (If given ground terms- ok, vars- no)
%%		must have ground functor, definite number of args!

% Front end for simulator use
top :-
	do_sdda(test,A,B,C).

% Does the sdda on FileName, instantiates Exitmodes to list of exit modes,
% ExitModes structure: [[Funtor/Arity, Activation, Exit], ... ],
% e.g. [[a/2, [g,X], [g,g]]
do_sdda(FileName, ExitModes, BackList, PredList) :-
	%%see(FileName),
	read_procedures(Procs, ExitModes, Entries),	% collect all procedures
	%%seen,
%	write('Procedures '), nl, write_list(Procs), nl,
%	write('Entry points '), nl, write_list(Entries), nl,
%	(nonvar(ExitModes) ->				% Don't mention there
%		(write('Declared exit modes '), nl, 	% aren't any
%		 write_list(ExitModes), nl) ;
%		true),
	entry_exit_modes_list(Procs, ExitModes, Entries).
%	write('Exit modes '), nl, write_list(ExitModes), nl.

%%%  !!! Hard code in read for test:
%	sdda_entry(c(A,B,C)).
%	a(X, Y).
%	a(X, X).
%	c(A,B,C) :- a(A,B).

read_procedures([[a/2,a(_109,_110),a(_148,_148)|_184],
		 [c/3,(c(_191,_192,_193):-a(_191,_192))|_238]|_239],
		 _68,[c(_76,_77,_78)|_102]) :- !.

% For each entry point in Entries do sdda, building Known, an unbound-tail list
% Known structure: [[Name/Arity, ActivationModes, ExitModes], ...|_],
% where ActivationModes and ExitModes are lists of variables and the atom 'g'.
% 'g' represents a ground element and variables represent equivalence classes.
entry_exit_modes_list(_, _, Entries) :-			% Done
	var(Entries).
entry_exit_modes_list(ProcList, Known, [Entry|Entries]) :-
	Entry =.. [Functor|Act],		% Get functor/arity & activation
	length(Act, Arity),			% from entry declaration
	proc_exit_mode(ProcList, Known, [], Functor/Arity, Act, _),  % No invoc.
	entry_exit_modes_list(ProcList, Known, Entries).

% Do sdda on procedure Functor/Arity, given activation mode Act.  Instantiates
% Known to known exit modes and Act to exit modes for Functor/Arity under Act
proc_exit_mode(_, _, _, Functor/Arity, Act, Exit) :-
	built_in(Functor/Arity, Act, Exit).		    % This is a built-in
proc_exit_mode(_, Known, _, Functor/Arity, Act, Exit) :-
	look_up_act([Functor/Arity, Act, Exit], Known).       % Already did this
proc_exit_mode(ProcList, Known, Invocations, Functor/Arity, Act, Exit) :-
	umember([Functor/Arity|Clauses], ProcList),	% Look up definition
	dup(Clauses, ClausesCopy),			% Don't munge original 
	clause_exit_modes_list(ProcList, Known, Invocations, 
			       ClausesCopy, Act, Exits),
	(Exits=[] -> fail ; true),		       % didn't find any => fail
	worst_case(Exits, Exit),			% assume the worst
	dup(Act, ActCopy),				% Need copy because Body
	add_to_list([Functor/Arity, ActCopy, Exit], Known).   % binds Act & Exit
proc_exit_mode(_, Known, _, Functor/Arity, Act, Exit) :-
%	write('No such procedure at compile time '),
	Activation=..[Functor|Act],
%	write(Activation), nl,
	all_shared(Act, Exit),     	   % return worst possible - all shared 
	add_to_list([Functor/Arity, Act, Exit], Known).

% Analyze all clauses for this procedure, instantiate Exits to all exit modes
clause_exit_modes_list(_, _, _, Clauses, _, []) :-
	var(Clauses), !.			       % No more clauses => done
clause_exit_modes_list(ProcList, Known, Invocations, 
		       [Clause|Clauses], Act, Exits) :-
	eqmember([Clause, Act], Invocations), 		% This is a recursive 
%    write('skipping clause exit mode for '), 
%    write(Clause), write(' '), write(Act), nl,
	clause_exit_modes_list(ProcList, Known, Invocations,	% call, ignore
			       Clauses, Act, Exits).		% it
clause_exit_modes_list(ProcList, Known, Invocations, 
		       [Clause|Clauses], Act, [Exit|Exits]) :-
	dup(Act, Exit),					% We'll bind Exit
	clause_exit_mode(ProcList, Known, [[Clause, Act]|Invocations], 
		 	 Clause, Exit),			% Record invocation
	clause_exit_modes_list(ProcList, Known, Invocations, 
		     	       Clauses, Act, Exits).
clause_exit_modes_list(ProcList, Known, Invocations, 
		       [Clause|Clauses], Act, Exits) :- 	% Unify failed
	clause_exit_modes_list(ProcList, Known, Invocations, 
			       Clauses, Act, Exits).   

% Given activation modes for this clause, return its exit modes
clause_exit_mode(ProcList, Known, Invocations, Clause, Act) :-
	(Clause = ':-'(Head, Body) ; Clause=Head, Body=true),	% Decompose it
	Head =.. [_|Args],					% Bind the head
	unify(Args, Act),					% to activation
	body_exit_mode(ProcList, Known, Invocations, Body). 	% do the body

body_exit_mode(ProcList, Known, Invocations, ','(Goal, Goals)) :-  % Conjunction
	body_exit_mode(ProcList, Known, Invocations, Goal),	% Do 1st
	body_exit_mode(ProcList, Known, Invocations, Goals).	% & rest
body_exit_mode(ProcList, Known, Invocation, Goal) :-
	functor(Goal, Functor, Arity),
	Goal =.. [Functor|Act],
	proc_exit_mode(ProcList, Known, Invocation, Functor/Arity, Act, Exit),
	unify(Act, Exit).	

% Unifies Left and Right with the special case that the atom 'g' matches
% any atom (except [])
unify(Left, Left) :- !.				% Try standard unify first
unify(Left, g) :-				% else, is it special case
	atomic(Left), !,			
	\+ Left=[].
unify(g, Right) :-				
	atomic(Right), !,
	\+ Right=[].
unify([LeftHead|LeftTail], [RightHead|RightTail]) :-	% or list
	!, unify(LeftHead, RightHead),
	unify(LeftTail, RightTail).
unify(Left, Right) :-					% or structure
	Left =.. [Functor|LeftArgs],
	Right =.. [Functor|RightArgs],
	unify(LeftArgs, RightArgs).
	
% Succeed if Left and Right are equivalent, i.e. they are the exact same 
% with variables renamed
equiv(Left, Right) :- 
	equiv(Left, Right, _).
equiv(Left, Right, _) :-		
	Left==Right, !.			
equiv(g, Right, _) :-		
	atomic(Right), !,
	\+ Right=[].			
equiv(Left, g, _) :-
	atomic(Left), !,
	\+ Left=[].			
equiv(Left, Right, Bindings) :-
	var(Left), !,
	var(Right), 
	equiv_vars(Left, Right, Bindings).
equiv(Left, Right, Bindings) :-
	var(Right), !,
	var(Left), 
	equiv_vars(Left, Right, Bindings).
equiv([LeftHead|LeftTail], [RightHead|RightTail], Bindings) :-
	!, equiv(LeftHead, RightHead, Bindings),
	equiv(LeftTail, RightTail, Bindings).
equiv(Left, Right, Bindings) :-
	Left=..[Functor|LeftArgs],
	Right=..[Functor|RightArgs],
	equiv(LeftArgs, RightArgs, Bindings).

equiv_vars(Left, Right, Bindings) :-
	var(Bindings), !,
	Bindings=[[Left, Right]|_].
equiv_vars(Left, Right, [[AnyVar, AnyBinding]|_]) :-
	Left==AnyVar, !,
	Right==AnyBinding.
equiv_vars(Left, Right, [[AnyVar, AnyBinding]|_]) :-
	Right==AnyBinding, !,
	Left==AnyVar.
equiv_vars(Left, Right, [ _|Bindings]) :-
	equiv_vars(Left, Right, Bindings).

% Make a copy of Orig with new vars.  Copy must be a variable.
% E.g. dup([A,s(A,B),[B,C]], New) binds New to [X,s(X,Y),[Y,Z]]
dup(Orig, Copy) :-
	dup(Orig, Copy, _).
dup(Orig, Copy, Bindings) :-
	var(Orig), !,
	dup_var(Orig, Copy, Bindings).
dup(Orig, Orig, _) :-				% Atoms, including []
	atomic(Orig), !.
dup([OrigHead|OrigTail], [CopyHead|CopyTail], Bindings) :-
	!, dup(OrigHead, CopyHead, Bindings),
	dup(OrigTail, CopyTail, Bindings).
dup(Orig, Copy, Bindings) :-
	Orig=..[Functor|OrigArgs],
	dup(OrigArgs, CopyArgs, Bindings),
	Copy=..[Functor|CopyArgs].

dup_var(Orig, Copy, Bindings) :-
	var(Bindings), !,
	Bindings=[[Orig, Copy]|_].
dup_var(Orig, Copy, [[AnyVar, Copy]|_]) :-
	Orig==AnyVar, !.
dup_var(Orig, Copy, [_|Bindings]) :-
	dup_var(Orig, Copy, Bindings).

% ----- Built-ins ----- %

built_in(true/0, [], []).			% No change 
built_in(fail/0, [], []).			% No change 
built_in('='/2, [X, Y], [g, g]) :- 
	(atomic(X) ; atomic(Y)). 		% Ground both if either atomic
built_in('='/2, [X, Y], [X, X]).		% else bind them 
built_in(/('+',2), [X, Y], [X, Y]).		% No change 
built_in(/('-',2), [X, Y], [X, Y]).		% No change 
built_in(/('*',2), [X, Y], [X, Y]).		% No change 
built_in(/('/',2), [X, Y], [X, Y]).		% No change 
built_in(/('>=',2), [X, Y], [X, Y]).		% No change 
built_in(/('<',2), [X, Y], [X, Y]).		% No change 
built_in(is/2, [X, Y], [g, Y]).			% Ground result 

% ----- Utilities ----- %

worst_case([], _).				%% Doesn't work if any Exits
worst_case([Exit|Exits], Worst) :-		%% fail to match, e.g.
	unify(Exit, Worst),			%% [[s(1)], [f(1)]].
	worst_case(Exits, Worst).

look_up_act(_, Known) :-
	var(Known), 
	!, fail.    
look_up_act([Functor/Arity, Act, Exit], [[Functor/Arity, KnownAct, Exit]|_]) :-
	equiv(Act, KnownAct).    
look_up_act([Functor/Arity, Act, Exit], [_|Known]) :-
	look_up_act([Functor/Arity, Act, Exit], Known).

all_shared(Act, Exit) :-			%% Wrong
	unify(Act, _, VarModesList),
	bind_all(_, VarModesList),
	unify(Act, Exit, VarModesList).

bind_all(_, VarModesList) :-
	var(VarModesList).
bind_all(Mode, [[Var, Mode]|VarModesList]) :-
	var(Mode),
	bind_all(Mode, VarModesList).
bind_all(Mode, [[_, _]|VarModesList]) :-
	bind_all(Mode, VarModesList).


% Adds Element to the tail of List, an unbound-tail list
add_to_list(Element, List) :-
	var(List),
	List=[Element|_].
add_to_list(Element, [_|List]) :-
	add_to_list(Element, List).

% Membership relation for unbound-tail lists
umember(_, List) :- 
	var(List), !, fail.
umember(Element, [Element|_]).
umember(Element, [_|Tail]) :- umember(Element, Tail).

% Strict membership relation for unbound-tail lists
sumember(_, List) :- 
	var(List), !, fail.
sumember(Element, [AnyElement|_]) :- Element==AnyElement.
sumember(Element, [_|Tail]) :- sumember(Element, Tail).

% Membership relation for standard nil-tail lists
member(X, [X|_]).
member(X, [_|T]) :- member(X, T).

% Strict membership relation for standard nil-tail lists
smember(X, [Y|_]) :- X==Y.
smember(X, [_|T]) :- smember(X, T).

% Equiv membership relation for standard nil-tail lists
eqmember(X, [Y|_]) :- equiv(X, Y).
eqmember(X, [_|T]) :- eqmember(X, T).

% Our old favorite
concat([], L, L).
concat([X|L1], L2, [X|L3]) :- concat(L1, L2, L3).

% Pretty prints unbound-tail lists -- dies on NIL tail lists
%write_list(List) :-
%	dup(List, NewList),
%	(var(NewList) -> (name_vars(NewList, 0, _));
%			  write(NewList)) ; 
%		         (write('['), 
%		      	  write_list2(NewList, 0, _), 
%		          write('|_].'))), 	% write('].') to write nil tails
	nl.				
write_list2([H|T], NextName, NewNextName) :- 
	name_vars(H, NextName, TempNextName),
	write(H),
	(nonvar(T) -> (write(','), nl, 
		       write(' '), 
		       write_list2(T, TempNextName, NewNextName)) ; 
		      NewNextName = TempNextName).

name_vars(Term, NextName, NewNextName) :-
	var(Term), !,
	make_name(NextName, Term),
	NewNextName is NextName + 1.
name_vars(Term, NextName, NextName) :-
	atom(Term), !.
name_vars([TermHead|TermTail], NextName, NewNextName) :-
	!, name_vars(TermHead, NextName, TempNextName),
	name_vars(TermTail, TempNextName, NewNextName).
name_vars(Term, NextName, NewNextName) :-
	Term =.. [_|TermArgs],
	name_vars(TermArgs, NextName, NewNextName).

make_name(IntName, Variable) :-
	Count is IntName // 26,
	NewIntName is IntName mod 26 + "A",
	build_name(Count, NewIntName, Name),
	name(Variable, Name).

build_name(0, IntName, [IntName]) :- !.
build_name(Count, IntName, [IntName|Rest]) :- Count>0,
	NewCount is Count - 1,
	build_name(NewCount, IntName, Rest).