/*
 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
                                  The University, Newcastle upton Tyne

 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@csl.sony.co.jp
 $Id$
*/

:-dynamic verbose/0,state/2,links/2.
:-dynamic stay/3.
:-dynamic regular_limit/1.

% itl decomposition for DST

% requires [chop]
% itl(Predicate,Next,Empty,ConditionLists)

itl(P) :- expand(P,P0),
	moref(Ev),itl(P0,Next,Ev,[],C),
	write(([Ev|C]->Next)),nl,fail.
itl(_).
itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C).

moref(empty).
moref(more).

itl(true,true,_,C,C):-!.
itl(false,false,_,C,C):-!.
itl(more,false,empty,C,C).
itl(more,true,E,C,C):-!,E = more.
% next two rule determines descrete time
itl(empty,true,empty,C,C).      
itl(empty,false,E,C,C):-!,E = more.  % no succeeding more interval
itl(N,F,E,C,C1):-number(N),!,
        sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
itl(?(Cond,T,F),N,E,C,C1):-!,
        itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1).
itl_cond(true,T,_,N,E,C,C1) :-!,
        itl(T,N,E,C,C1).
itl_cond(false,_,F,N,E,C,C1) :-!,
        itl(F,N,E,C,C1).
itl_cond(CN,T,F,N,E,C,C1) :-!,
        itl(T,TN,E,C,C0),
        itl(F,FN,E,C0,C1), negate(CN,NCN),
        and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).

itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1).
    local(true,P,C,C1):- true(C,P,C,C1).
       true([],P,C,[P|C]):-!.
       true([P|_],P,C,C):-!.
       true([not(P)|_],P,_,_):-!,fail.
       true([_|T],P,C,C1):-true(T,P,C,C1).
    local(false,P,C,C1):- false(C,P,C,C1).
       false([],P,C,[not(P)|C]):-!.
       false([P|_],P,_,_):-!,fail.
       false([not(P)|_],P,C,C):-!.
       false([_|T],P,C,C1):-false(T,P,C,C1).
itl(@(P),P,more,C,C).		   % strong next
itl(@(_),false,E,C,C):-!,E=empty.

% Regular Variable
itl(^(R),F,empty,C,C1):-
    local(F0,up(R),C,C0),
    local(F1,down(R,0),C0,C1),and(F0,F1,F).
itl(^(R),F1,E,C,C1):-!, E=more,
    local(F,up(R),C,C1),and(F,^(R,0),F1).

itl(^(_R,S),false,_,C,C):-
	regular_limit(X),S>X,!.
itl(^(R,S),F,empty,C,C1):-
    local(F,down(R,S),C,C1).
itl(^(R,S),^(R,S1),E,C,C):-!, E=more, S1 is S+1.

% Quantifier
itl(exists(P,Q),F,E,C,C0) :-!,
	itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
    itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1).
    itl_ex(false,Q,E,P,F,C,C0):-  !,remove_p(C,P,C1),
    	itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F).
    itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1),
    	itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0),
        or(QT,QF,TF),exists(TF,P,F).
    % constant order optimzation for quantifier
    exists(P,P,true):-!.
    exists(P,_,P):-atomic(P),!.
    exists(Q,P,exists(P,Q)).
    remove_p([],_,[]):-!.
    remove_p([not(P)|T],P,T):-!.
    remove_p([P|T],P,T):-!.
    remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1).
itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1).
itl(*(P),F,E,C,C1):-!,E=more,
	itl(P,PX,more,C,C1),
	closure(PX,P,F).
    closure(false,_,false):-!.
    closure(PX,P,(PX & *(P))).              %% infinite clousre (strong)
%%    closure(PX,P,(PX & (*(P);empty))).    %% finite closure (weak)
%% external state diagram (determinization)
itl(st(N),F,E,C,C1):-!,
	setof((Cond=>X),st(N,Cond,X),L),
	itl_transition(L,F,E,C,C1).
    itl_transition([],false,_,C,C):-!.
    itl_transition([(Cond=>true)|T],F,E,C,C1):-!,
    	itl((Cond),F0,E,C,C0),
        itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
    itl_transition([(Cond=>empty)|T],F,E,C,C1):-!,
    	itl((empty,Cond),F0,E,C,C0),
        itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
    itl_transition([(Cond=>X)|T],F,E,C,C1):-
    	itl((more,Cond),F0,E,C,C0),
        itl_transition1(F0,X,T,F,E,C0,C1).
    itl_transition1(false,_,T,F,E,C,C1):-!,
        itl_transition(T,F,E,C,C1).
    itl_transition1(true,X,T,F1,E,C,C1):-!,
        itl_transition(T,F,E,C,C1),or(F,st(X),F1).
%% ignore last state to check non stop predicate
itl(free_fin(_),F,empty,C,C):-!,F=true.
itl(free_fin(L),F1,more,C,C1):-!,
    itl(L,F,more,C,C1),free_fin(F,F1).
    free_fin(true,true):-!.
    free_fin(false,false):-!.
    free_fin(X,free_fin(X)):-!.
%%
itl((P,Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
itland(false,_,false,_,C0,C0):-!.
itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
itland(PN,Q,N,E,C0,C1):-
	itl(Q,QN,E,C0,C1),and(PN,QN,N).		%% and/3 in chop.pl
itl((P;Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
itlor(true,_,true,_,C0,C0):-!.
itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
itlor(PN,Q,N,E,C0,C1):-
	itl(Q,QN,E,C0,C1),or(PN,QN,N).		%% or/3 in chop.pl
itl(not(P),NN,E,X,X1) :- !,
	itl(P,N,E,X,X1),
	negate(N,NN).				%% negate/2 in chop.pl
% F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q)
itl((P&Q),F,empty,C,C1) :-!,
	itl((P,Q),F,empty,C,C1).
itl((P&Q),F,more,C,C2) :-!,
	itl(P,PE,empty,C,C0),
	C0 = C0R,
	itl(P,PM,more,C0R,C1),
	chop(PM,PE,F,Q,C1,C2).

chop(false,false,false,_,C,C):-!.
chop(PM,false,(PM & Q),Q,C,C):-!.
chop(PM,true,F,Q,C,C1):-!,
    itl(Q,QF,more,C,C1),
    chop1(PM,QF,Q,F).
chop(PM,PE,F,Q,C,C):-!,
	write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
	fail.

chop1(false,QF,_,QF):-!.
chop1(false,false,_,false):-!.
chop1(PM,false,Q,(PM&Q)):-!.
chop1(_,true,_,true):-!.
chop1(PM,QF,Q,(QF;(PM&Q))):-!.

itl(proj(_,Q),F,empty,C,C1) :-!,
	itl(Q,F,empty,C,C1).
itl(proj(P,Q),F,more,C,C1) :-!,
	itl(P,PM,more,C,C0),
	itl(Q,QM,more,C0,C1),
	prj(PM,QM,P,F).
prj(false,_,_,false):-!.
prj(_,false,_,false):-!.
prj(PM,QM,P,(PM&proj(P,QM))).

itl(prefix(P),F,empty,C,C1) :-!,
	itl(P,PE,empty,C,C0),
	itl(P,PM,more,C0,C1),    % this must be satistifiable
	prefix(PM,PE,F).
itl(prefix(P),F,more,C,C1) :-!,
	itl(P,PM,more,C,C1),
	prefix(PM,F).

prefix(true,true):-!.
prefix(false,false):-!.
prefix(PM,prefix(PM)):-!.

prefix(true,_,true):-!.
prefix(_,true,true):-!.
prefix(false,false,false):-!.
prefix(_,false,true):-!.

itl(Def,_,_,_,_) :-
    write('error: '),write(Def),nl,!,fail.

itl_statistics :- nl,
        itl_state_number(X),write(X),write(' states'),nl,fail.
itl_statistics :- 
        sbn(X),write(X),write(' subterms'),nl,fail.
itl_statistics :- 
        init_var(tmp,0),
        ((links(_,_),inc_var(tmp,_),fail);true),
        tmp(N),
%       init_var(tmp,0),
%       ((state(_,_,_),inc_var(tmp,_),fail);true),
%       recorded(tmp,L,_),
        itl_transition(L),
        write(N),put(47),  % "/"
        write(L),write(' state transitions'),nl,fail.
itl_statistics.


:-assert(verbose).
verbose(off) :- retract(verbose),fail;true.
verbose(on) :- asserta(verbose).

deve(ITL) :-
	init,!,
	expand(ITL,ITL0),		% chop standard form
	itlstd(ITL0,StdNOW),		% BDT
	assert(itl_state(StdNOW,1)),!,  % Initial State
	deve0((1,ITL0)).

deve0((S,ITL)) :-
%        increment_state(ITL,ITL_1,S),
        show_state(S,ITL),
%	setof(Next,itldecomp(ITL,Next,S),
	bagof(Next,itldecomp(ITL,Next,S),
	    Nexts),!,
	deve1(Nexts).
deve0(_).

deve1([]).
deve1([H|T]) :- deve0(H),deve1(T).

itldecomp(ITL,(NextS,Next),From) :-
	init_var(current,From),
	itl(ITL,Next,Cond),
	%% showing
	itlshow(Next,NextS,Cond,From).

itlshow(Next,S,Cond,From):-
	itlstd(Next,StdNext),
	check_state(StdNext,Cond,New,S),
	inc_var(itl_transition,_),
	assertz(state(From,Cond,S)),
	(links(S,From),!;assertz(links(S,From))),
	!,
	itlshow0(S,Cond,Next,New).

itlshow0(S,Cond,Next,New) :- verbose,!,
	itlshow1(S,Cond,Next,New),nl,!,New=1.
itlshow0(0,_,_,0):- !,put(101),!,fail.   % "e"
itlshow0(false,_,_,0):- !,put(102),!,fail.  % "f"
itlshow0(true,_,_,0):- !,put(116),!,fail.  % "t"
itlshow0(_,_,_,0):- !,put(46),!,fail.    % "."
itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!.  % "."

itlshow1(0,Cond,_,_):-!,
	write(Cond),write('->'),write(empty).
itlshow1(true,Cond,_,_):-!,
	write(Cond),write('->'),write(true).
itlshow1(false,Cond,_,_):-!,
	write(Cond),write('->'),write(false).
itlshow1(S,Cond,_,0):-!,
	write(Cond),write('->'),write(S).
itlshow1(S,Cond,Org,1):-
	write(Cond),write('->'),write(S),
	put(9),write(Org),!.

init :-
	subterm_init,
	abolish(state,3),
	asserta(state(true,[more],true)),
	asserta(state(true,[empty],0)),
        abolish(itl_state,2),
        abolish(stay,3),asserta(stay(0,0,0)),
        asserta(itl_state(false,false)),
        asserta(itl_state(empty,0)),
        asserta(itl_state(true,true)),
        init_var(regular_limit,5),
	abolish(links,2),asserta(links(true,true)),
	init_var(current,0),
	init_var(itl_transition,1),
	init_var(itl_state_number,1),!.

show_state(S,ITL) :-
	nl,write('state('),write(S),  % (
	(verbose,write(' , '), write(ITL),write(')'),nl;write(')')),!.

check_state(true,[more |_],0,true):-!.
check_state(true,[empty|_],0,0):-!.
check_state(false,_,0,false):-!.
check_state(STD,_,0,S):-
	itl_state(STD,S),!.
check_state(STD,_,1,S):-
	inc_var(itl_state_number,S),
	assert(itl_state(STD,S)),!.

init_var(X,_) :- functor(F,X,1),assert(F),fail.
init_var(X,_) :- functor(F,X,1),retract(F),fail.
init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!.
inc_var(Name,X1) :- 
        functor(F,Name,1),retract(F),arg(1,F,X),
        X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
        asserta(F1),!.
set_var(Name,X,X1) :-
        functor(F,Name,1),retract(F),!,arg(1,F,X),
        functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
set_var(Name,X,_) :- init_var(Name,X).

increment_state(stay(P,now),stay(P,S),S) :- !,
      (stay(P,F,S);assertz(stay(P,F,S))),!.
increment_state(N,N,_) :- atomic(N),!.
increment_state(P,R,S) :- functor(P,H,N),functor(R,H,N),
      increment_state_arg(N,P,R,S).
increment_state_arg(0,_P,_R,_):-!.
increment_state_arg(N,P,R,S):-arg(N,P,PA),arg(N,R,RA),
      N1 is N-1,increment_state(PA,RA,S),
      increment_state_arg(N1,P,R,S).

%% end %%