/**********************************************************************************
"Thus one portion of being is the Prolific, the other the Devouring:
 to the devourer it seems as if the producer was in his chains, 
 but it is not so, he only takes portions of existence and fancies that the whole."
	From "The Marriage of Heaven and Hell" by William Blake
***********************************************************************************/

/*>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
 BUILDING THE AUTOMATON:
it is done in three phases:
@pahse1: finding the prime and psuedo-prime sets
@pahse2: building the automaton (the devourer)
@pahse3: generating the prolog code that implements the automaton 
<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<*/
:- dynamic topo_ind/1,multi_hash/1.

% gen_flag(<-MultiHash:yes/no>,<-TopoOrd:yes/no>)
gen_flag(MultiHash,TopoOrd):-
	retractall(multi_hash(_)),
	retractall(topo_ind(_)),
	assert(multi_hash(MultiHash)),
	assert(topo_ind(TopoOrd)).

go:-
 %@pahse1
	statistics(walltime, [Phase1Start,_]),
	start,
	statistics(walltime, [Phase1End,_]),

%@pahse2
	statistics(walltime, [Phase2Start,_]),
	build_aut, 
	statistics(walltime, [Phase2End,_]),

%@pahse3
	statistics(walltime, [Phase3Start,_]),
	gen_code,
	statistics(walltime, [Phase3End,_]),

	Phase1Time is Phase1End - Phase1Start,
	Phase2Time is Phase2End - Phase2Start,
	Phase3Time is Phase3End - Phase3Start,
	TotalTime is (Phase1Time + Phase2Time + Phase3Time), 
	nl,nl,
	write('Phase 1 completed in < '),write(Phase1Time),write(' > msec'),nl,
	write('Phase 2 completed in < '),write(Phase2Time),write(' > msec'),nl,
	write('Phase 3 completed in < '),write(Phase3Time),write(' > msec'),nl,
	write('>>>>>>>>>>>>>>>>>>>>TOTAL Time: '),write(TotalTime),write(' msec'),nl,

	write('automaton Stats:'),nl,
	next_vertex(NumOfStates),
	write('Number of States:'),write(NumOfStates),nl,
	findall(1,suffix(_,_,_),Ss),length(Ss,NumOfSuffixEdges),
	write('Number Of Suffix Edges:'),write(NumOfSuffixEdges),nl,
	findall(1,redex(_,_,_),Rs),length(Rs,NumOfRedexEdges),
	write('Number Of Redex Edges:'),write(NumOfRedexEdges),nl,
	TotalEdges is NumOfRedexEdges + NumOfSuffixEdges,
	write('Total Number Of Edges:'),write(TotalEdges),nl,
	cleanup,
	nl.

cleanup :-
	%stuff from phase-1
	retractall(prime(_,_)),
	retractall(hprime(_,_,_,_,_)),
	retractall(primefailure(_,_)),
	retractall(hpsprime(_,_,_,_)),
	%stuff from phase-2
	retractall(suffix(_,_,_)),
	retractall(redex(_,_,_)),
	retractall(last_vertex_added(_)),
	%stuff from phase-3
	retractall(visited(_)),
	retractall(wroteb(_,_,_)),
	retractall(wrote(_,_)).
	%retractall(multi_hash(_)),
	%retractall(topo_ind(_)).


%%%%%%%%%%%%%%%%%%%%% PHASE 1 %%%%%%%%%%%%%%%%%%%%%%%%%

:- use_module(library(lists)).
:- dynamic num_of_types/1.
:- dynamic prime/2,hprime/5.
:- dynamic primefailure/2.
:- dynamic pseudoprime/3,hpsprime/4.

%%%%%%%%%%%%%%%%%%%% MISC/UTILS %%%%%%%%%%%%%%%%%%%%%%%
% using my_union instead of ord_union, since
% ord_union wants sets in prolog standard
% order which is not always the case here!
my_union([X|Y],Z,W) :- member(X,Z),  my_union(Y,Z,W).
my_union([X|Y],Z,[X|W]) :- \+ member(X,Z), my_union(Y,Z,W).
my_union([],Z,Z).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% topo_ord(+Set,-TopoOrdSet)
%
topo_ord([T],[T]):-!.
topo_ord(Set,TopoOrdSet):-
	% NOTE: Assuming that num_of_types/1 is asserted in the
	% the PHASE 2 of compile_sub_type in ale.pl
	num_of_types(NumOfTypes),
	topo_key(NumOfTypes,Set,TKeySet),
	keysort(TKeySet,SortedTKeySet),
	dekey_list(SortedTKeySet,TopoOrdSet).

topo_key(_,[],[]).
topo_key(NumOfTypes,[Entry|RestOfSet],[OrdNum-Entry|TKeySet]):-

	% type_nums were asserted during compile_sub_type 
	% those generated ones are apparently 
	% based on the reverse topological order
	% so instead of reversing the types and 
	% doing the topo sort all over again 
	% simply reverse the ordinal number 
	% and keysort will take care of the rest

	type_num(Entry,RevOrdNum),
 	OrdNum is NumOfTypes - RevOrdNum, 
	topo_key(NumOfTypes,RestOfSet,TKeySet).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% topo_ord_rev(+Set,-TopoRevOrdSet)
%
topo_ord_rev([T],[T]):-!.
topo_ord_rev(Set,TopoRevOrdSet):-
	num_of_types(NumOfTypes),
	topo_rev_key(NumOfTypes,Set,TKeySet),
	keysort(TKeySet,SortedTKeySet),
	dekey_list(SortedTKeySet,TopoRevOrdSet).

topo_rev_key(_,[],[]).
topo_rev_key(NumOfTypes,[Entry|RestOfSet],[RevOrdNum-Entry|TKeySet]):-
	type_num(Entry,RevOrdNum),
	topo_rev_key(NumOfTypes,RestOfSet,TKeySet).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% finds an assert the prime and psuedo-prime sets
% Before calling start 'ale.pl' must be loaded 
% as well as the subtype file(eg. 'sub.pl')

start:-
	retractall(num_of_types(_)),
	retractall(prime(_,_)),
	retractall(hprime(_,_,_,_,_)),
	retractall(primefailure(_,_)),
	retractall(hpsprime(_,_,_,_)),
	compile_sub_type,
	iterate(2),
	add_prime2(_,_,_).

iterate(N) :-
  write(N),nl,	
  NPlus1 is N + 1,
  pseudoprime(_,Types1,_N),
  pseudoprime(_,Types2,_AlsoN),
  my_union(Types1,Types2,Union),
  length(Union,NPlus1),
  pseudo_saturated(Union),
  detstatus(Union,Status,Join),
  ( Status == det -> add_prime(NPlus1,Union,Join)
  ; Status == cons -> add_pseudoprime(NPlus1,Union)
  ; Status == fail, add_primefailure(NPlus1,Union)
  ),
  fail.

iterate(N) :-
  NPlus1 is N + 1,
  retractall(pseudoprime(_,_,N)),
  ( clause(pseudoprime(_,_,NPlus1),true) -> iterate(NPlus1)
  	; (true,write('no psuedoprime with size='),write(NPlus1) )
  ).

pseudo_saturated(Set) :-
  select(_,Set,SubSet),
  term_hash(SubSet,H),
  \+ pseudoprime(H,SubSet,_N),
  !,fail.
  pseudo_saturated(_).

detstatus([T|Rest],Status,Join) :-
  clause(type_num(T,N),true),
  clause(stmatrix_num(N,Row),true),
  detstatus(Rest,Row,Status,Join).

detstatus([],Row,Status,Join) :-
  map_minimal(Row,Mins),		
  length(Mins,N),
  ( N == 0 -> (Status = fail,Join=no)
  ; N == 1 -> (Status = det,[Join] = Mins)
  ; N > 1, (Status = cons,Join=no)
  ).

detstatus([T|Rest],Row,Status,Join) :-
  clause(type_num(T,N),true),
  clause(stmatrix_num(N,TRow),true),
  ord_intersection(TRow,Row,NewRow),
  ( NewRow == [] -> Status = fail
  ; detstatus(Rest,NewRow,Status,Join)
  ).

add_prime(N,Set,Join) :-
   term_hash(Set,H),
   topo_ord(Set,TopoOrdSet),
   ( clause(prime(N,Set),true) -> true
   ; (assert(prime(N,Set)),assert(hprime(H,N,Set,TopoOrdSet,Join)))
   ).

add_pseudoprime(N,Set) :-
   term_hash(Set,H),
   topo_ord(Set,TopoOrdSet),
   ( clause(pseudoprime(H,Set,N),true) -> true
   ; (assert(hpsprime(H,N,Set,TopoOrdSet)),assert(pseudoprime(H,Set,N)))
   ).

add_prime2(X,Y,Z) :-
	unify_type(X,Y,Z),
	(
          (sub_type(X,Y);sub_type(Y,X)) -> true
	   ;(
		append([X],[Y],P2),
                term_hash(P2,H),
		topo_ord(P2,TopoOrdSet),
		\+ hprime(_,2,_,TopoOrdSet,_),
		assert(prime(2,P2)),
                assert(hprime(H,2,P2,TopoOrdSet,Z))
            )
	),fail.
add_prime2(_,_,_).


add_primefailure(N,Set) :-
   ( clause(primefailure(N,Set),true) -> true
   ; assert(primefailure(N,Set))
   ).


%%%%%%%%%%%%%%%%%%%%% PHASE 2:  Building the automaton %%%%%%%%%%%%%%%%%%%%%%
/* +++++++++++++++++++++++++++++++++++++++++++++++++++
Here we are building the suffix tree and along the way
add the extra redex edges, alltogether is our automaton
+++++++++++++++++++++++++++++++++++++++++++++++++++++*/

:- dynamic suffix/3,redex/3,last_vertex_added/1.

next_vertex(N):-
	last_vertex_added(Old),
	N is Old + 1,
	retract(last_vertex_added(Old)),
	assert(last_vertex_added(N)).

update_vertex(N):-
	retractall(last_vertex_added(_)),
	assert(last_vertex_added(N)).


build_aut :-
	findall(N,hpsprime(_,N,_Set,_),PSSizeSet),
	remove_duplicates(PSSizeSet,PSSizes),
	add_edge_level_1,
	num_of_types(NumOfTypes),
	update_vertex(NumOfTypes),
	add_edge_level_1Plus(PSSizes),
	add_redex_if_any(_,_),

	write('****************************************'),nl,
	write('automaton Stats Before prunning:'),nl,
	next_vertex(NumOfStates),
	write('Number of States:'),write(NumOfStates),nl,
	findall(1,suffix(_,_,_),Ss),length(Ss,NumOfSuffixEdges),
	write('Number Of Suffix Edges:'),write(NumOfSuffixEdges),nl,
	findall(1,redex(_,_,_),Rs),length(Rs,NumOfRedexEdges),
	write('Number Of Redex Edges:'),write(NumOfRedexEdges),nl,
	TotalEdges is NumOfRedexEdges + NumOfSuffixEdges,
	write('Total Number Of Edges:'),write(TotalEdges),nl,
	write('****************************************'),nl,

	prune.


/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*
@Level1: At this level, initially there is no edge, so
First we add suffix edges for every type from
 0 to the topological oridnal number (representing the initial states) 

for example : 
suffix(0,3,z) 
... 
suffix(0,4,h),
suffix(0,8,c)

and then we check if we should add any redex edge 

for example suppose there is a prime set [c,d] -> h
so we should add a redex edge redex(8,4,d)
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/

add_edge_level_1:-
	add_first_suffixes(_).
add_first_suffixes(X):-
	type(X),
	ground(X),
	(X == bot -> true 
	;(
		type_num(X,RevOrdNum),
		num_of_types(NumOfTypes),
 		OrdNum is NumOfTypes - RevOrdNum,
		( clause(suffix(0,OrdNum,X),true) -> true
   		   ; asserta(suffix(0,OrdNum,X))
  		),
		add_first_redexes(X,OrdNum)	
	 )
	),
	fail.
add_first_suffixes(_).


add_first_redexes(X,XOrdNum):-
     add_first_redexes_all(X,XOrdNum,_,_).


add_first_redexes_all(X,XOrdNum,C,Join) :-
	hprime(_,2,_,[X,C],Join),
	type_num(Join,RevOrdNum),
	num_of_types(NumOfTypes),
 	JoinOrdNum is NumOfTypes - RevOrdNum,
	( clause(suffix(0,JoinOrdNum,Join),true)
		 -> asserta(redex(XOrdNum,JoinOrdNum,C))
   		;(
			asserta(suffix(0,JoinOrdNum,Join)),
			asserta(redex(XOrdNum,JoinOrdNum,C))
		 )
  	),	
	fail.
add_first_redexes_all(_X,_XOrdNum,_,_).


/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*
@Levels >2: 
This will add suffix edges for psuedo-prime sets 
of size, N, and after it add the suffix edges
it will check if in any path that was constructed so far, 
can we jump to somewhere else by a redex edge, if yes it will
that redex edge:

It will use two facts:

1) For any pseudo-prime set, say PS, of size N which is topologically ordered, 
   there exist another pseudo-prime set of size N-1 which is the prefix
   of PS.

by this fact we first find the prefix of PS with size N-1, and then look for
the path that was constructed in one level before and find the last state,
now we add another suufix edge from that state to the newly created state with
its weigth being the last element of PS in hand.	

2) For any prime set,P, of size N which is topologically ordered, 
   there exist a pseudo-prime,PS, set of size N-1 which is the prefix
   of P.

by this, after adding the new suffix edge and extending the path we are in it,
we look for a prime a set of size N+1, in which some suffix of this PS, would
be the prefix of it, after finding such prime(if any) we find its join and 
add the proper redex to that Join, This is done in add_redex_if_any

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/

add_edge_level_1Plus([]).
add_edge_level_1Plus([Size|PSSizes]):-
	%first find all the psuedo-primes of this size
	findall(TopoSet,hpsprime(_,Size,_,TopoSet),TSs),
	add_edges_for(TSs),
	add_edge_level_1Plus(PSSizes).


add_edges_for([]).
add_edges_for([TS|TSs]):-
	length(TS,N),
	PN is N - 1,
	prefix(Prefix,TS),
	length(Prefix,PN),
	(find_last_hop_for(Prefix,0,From)->true
	 ; (write('BAD ERROR!!!!: there is no Prefix path for PS='),write(TS),nl)
	),
	last(TS,Weight),
	next_vertex(To),
	( clause(suffix(From,To,Weight),true) -> true
   	 ; asserta(suffix(From,To,Weight))
  	), 
	add_edges_for(TSs).


/*---------------------------------------------------------------------*
<+TS> is the Pseudo-prime that all of its element are on some path
whose last element took it to <+TSEnd> state

Side effect: adds the redex if it find such PS, fails if it could not!
%Ver. 3 make sure you add all: so put it failure driven loop!
------------------------------------------------------------------------*/
add_redex_if_any(TS,TSEnd):-
	hpsprime(_,_,_,TS),
	find_last_hop_for(TS,0,TSEnd),
	suffix(Suffix,TS),
	length(Suffix,N),
	NP is N+1,
	hprime(_,NP,_,PrimeTopo,Join), 
	prefix(Suffix,PrimeTopo),
	append(X,Suffix,TS),
	append(X,[Join],Look),
	find_last_hop_for(Look,0,RedexTo),
	last(PrimeTopo,Weight),
	(clause(redex(TSEnd,RedexTo,Weight),true) -> true
   	 ; asserta(redex(TSEnd,RedexTo,Weight))
  	),
	fail.
add_redex_if_any(_,_).


find_last_hop_for([],Last,Last).
find_last_hop_for([W|Ws],From,Last):-
	suffix(From,NextHop,W),
	find_last_hop_for(Ws,NextHop,Last).

/*----------------------------------------------------*
For suffix edges: if there is no outgoing suffix edge 
or (incoming or outgoing) redex edge get rid of it.
------------------------------------------------------*/
prune :- prune_s(_,_).
prune_s(To,W):-
	suffix(0,To,W),
	( suffix(To,_,_)-> fail
		;((redex(_,To,_);redex(To,_,_))-> fail
			; retract(suffix(0,To,W))
		)
	),fail.
prune_s(_,_).


print_aut:-
	put_all_suffix(_,_,_),
	put_all_redex(_,_,_).	

put_all_suffix(From,To,Weight):-
	suffix(From,To,Weight),
	write('suffix('),
	write(From),write(','),
	write(To),write(','),
	write(Weight),write(')'),
	nl,
	fail.
put_all_suffix(_,_,_).


put_all_redex(From,To,Weight):-
	redex(From,To,Weight),
	write('redex('),
	write(From),write(','),
	write(To),write(','),
	write(Weight),write(')'),
	nl,
	fail.
put_all_redex(_,_,_).


%%%%%%%%%%%%%%%%%%%%% PHASE 3: Generating IR code %%%%%%%%%%%%%%%%%	
:- dynamic visited/1,wroteb/3,wrote/2.
:- use_module(library(system),[datime/1]).

gen_code :-
	datime(W),
	(multi_hash(yes)->
	(topo_ind(yes)->tell('aut_MultiHash_code_num.pl');tell('aut_MultiHash_code.pl')) 
	;(topo_ind(yes)->tell('aut_code_num.pl');tell('aut_code.pl'))
	),
	write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'),nl,
  	write('%This file was generated by ALE, (http://www.ale.cs.toronto.edu) '),nl,
   	write('% '),write(W),nl,
	write('% The following code implements the automaton-based index of the'),nl,
        write('% compiled subtype hierarchy,(for internal compiler use).'),nl,	
   	write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'),nl,
	nl,
	write('pp([L|R],Ans):-pp(0,L,R,Ans).'),nl,
	findall(NextState,suffix(0,NextState,_),Childs),nl,
	do_dfs(0,Childs,[]),
	gen_redex_code_for(_,_,_),
	told.

write_list_items([]).
write_list_items([H]):-
	(topo_ind(yes)->
	 (num_type(N,H),write(N))
	;(
	 write('\''),
         write(H),
         write('\'')
	)).

write_list_items([H|T]):-
	(topo_ind(yes)->
	 (clause(num_type(N,H),true),write(N))
	;
	(write('\''),
         write(H),
         write('\'')
	)),
	write(','),
	write_list_items(T).


write_topo_type(T):-
	(topo_ind(yes)->
	 (clause(num_type(N,T),true),write(N))
	 ;(write('\''),write(T),write('\''))
	).

do_dfs(State,Childs,Acc):-
        traverse(State,Childs,Acc).

traverse(State,[NextState|Rest],Acc):-
	suffix(State,NextState,W),
	findall(NextStateChilds,suffix(NextState,NextStateChilds,_),NSCs),
	NewAcc = [W|Acc],
	reverse(NewAcc,RevAcc),
	((NSCs == []) -> (
		write('pp('),write(State),write(','),write_topo_type(W),
		write(',[],'),write('['),write_list_items(RevAcc),write(']'),write(').'),nl
	);
	(
		write('pp('),write(State),write(','),write_topo_type(W),
		write(',[],'),write('['),write_list_items(RevAcc),write(']'),write(').'),nl,

		write('pp('),write(State),write(','),write_topo_type(W),
		write(',[N|R],A) :-'),
		( multi_hash(yes)->
		  (write(' pp_'),write(NextState),write('(N,R,A).'),nl)	
		 ;(write(' pp('),write(NextState),write(',N,R,A).'),nl)
		)
	)),
	do_dfs(NextState,NSCs,NewAcc),
	traverse(State,Rest,Acc).

traverse(_State,[],_Acc).

gen_redex_code_for(State,TO,With):-
	redex(State,TO,With),
	hprime(_,NP,_,PrimeTopo,Join),
	append(PSSet,[With],PrimeTopo),
	suffix(Suffix,PSSet),
	length(Suffix,N),
	NP is N+1,
	prefix(Suffix,PrimeTopo),
	suffix(From,TO,Join),	
	(wrote(State,With) -> true
	;(
	suffix(Branch,State,BranchWith),
	((wroteb(Branch,State,BranchWith);suffix(State,_,_) )-> true
	 ;(
        	write('pp('),write(Branch),write(','),write_topo_type(BranchWith),
	        write(',[N|R],A) :-'),
		( multi_hash(yes)->
			(write(' pp_'),write(State),write('(N,R,A).'),nl)
			;(write(' pp('),write(State),write(',N,R,A).'),nl)
		),

		assert(wroteb(Branch,State,BranchWith))
	 )
	),
	write('pp('),write(State),write(','),write_topo_type(With),
	write(',L,A) :-'),
	( multi_hash(yes)->
	(write(' pp_'),write(From),write('('),write_topo_type(Join),write(',L,A).'),nl)
	;(write(' pp('),write(From),write(','),write_topo_type(Join),write(',L,A).'),nl)
	)
	
	)),
	assert(wrote(State,With)),
	fail.
gen_redex_code_for(_,_,_):-!.
