/**********************************************************************************
"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:-
	assert(num_type(0,bot)),
	assert(type_num(bot,0)),
 %@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(_,_)).



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

:- use_module(library(lists)).

:- dynamic num_of_types/1.

:- dynamic prime/2,hprime/4.
:- dynamic primefailure/2.
:- dynamic pseudoprime/3,hpsprime/3.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Phase 1: 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),

  ord_union(Types1,Types2,Union),
  
  length(Union,NPlus1),
  pseudo_saturated(Union),
  detstatus(Union,Status),
  iterate_act(Status,NPlus1,Union),
  fail.

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

iterate_act(det(Join),NPlus1,Union) :- add_prime(NPlus1,Union,Join).
iterate_act(cons,NPlus1,Union) :- add_pseudoprime(NPlus1,Union).
iterate_act(fail,NPlus1,Union) :- add_primefailure(NPlus1,Union).

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

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

detstatus([],Row,Status) :-
  map_minimal_indices(Row,Mins),
  length(Mins,N),               
  ( N == 0 -> (Status = fail)
  ; N == 1 -> (Status = det(Join),arg(1,Mins,Join))
  ; N > 1, (Status = cons)
  ).
detstatus([N|Rest],Row,Status) :-
  clause(stmatrix_num(N,NRow),true),
  ord_intersection(NRow,Row,NewRow),
  ( NewRow == [] -> Status = fail
  ; detstatus(Rest,NewRow,Status)
  ).

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

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

add_prime2(X,Y,Z) :-
	unify_type(X,Y,Z),
	(
          (sub_type(X,Y);sub_type(Y,X)) -> true
	   ;(
		(clause(num_type(N1,X),true)),
		(clause(num_type(N2,Y),true)),
		(clause(num_type(JoinNum,Z),true)),
		((N1<N2)->P2=[N1,N2];P2=[N2,N1]),
                term_hash(P2,H),
		\+ hprime(_,2,P2,_),
		assert(prime(2,P2)),
                assert(hprime(H,2,P2,JoinNum))
            )
	),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,clause(hpsprime(N,_H,_Set),true),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,OrdNum),
		( clause(suffix(0,OrdNum,X),true) -> true
   			; asserta(suffix(0,OrdNum,OrdNum))
  		),
		add_first_redexes(OrdNum,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),
	( clause(suffix(0,Join,Join),true)
		 -> asserta(redex(XOrdNum,Join,C))
   		;(
			asserta(suffix(0,Join,Join)),
			asserta(redex(XOrdNum,Join,C))
		 )
  	),	
	fail.
add_first_redexes_all(_X,_XOrdNum,_,_).


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

First we add all the suffix edges of level>1 (add_edge_level_1Plus)
And then we check on what states that was just created we could jump and
add the corresponding redex edge(add_redex_if_any):


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 suffix 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,clause(hpsprime(Size,_,TopoSet),true),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 finds such PS
------------------------------------------------------------------------*/
add_redex_if_any(TS,TSEnd):-
	clause(hpsprime(_,_,TS),true),
	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(_,_).

%%%%%%%%%%%%%%%%%%%%% 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)->
	 (
	   write(H)	
	)
	;(
	   num_type(H,Name),
	   write('\''),
           write(Name),
           write('\'')	
	   
	)).

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


write_topo_type(TypeNum):-
	(topo_ind(yes)-> write(TypeNum)
	 ;(num_type(TypeNum,Name),
	   write('\''),
           write(Name),
           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(_,_,_):-!.
