/*
 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: exdev.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
*/

% develop Local ITL formula into state diagram
%
% Mon May 20 17:24:23 BST 1991
% require([chop]).

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

:-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,
	r_abolish(state,3),
	asserta(state(true,[more],true)),
	asserta(state(true,[empty],0)),
        r_abolish(itl_state,2),
        r_abolish(stay,3),asserta(stay(0,0,0)),
        asserta(itl_state(false,false)),
        asserta(itl_state(empty,0)),
        asserta(itl_state(true,true)),
	r_abolish(links,2),asserta(links(true,true)),
	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),!.

%init_var(X,_) :- recorded(X,_,Ref),erase(Ref),fail.
%init_var(X,V) :- recorda(X,V,_).
%inc_var(Name,X1) :- 
%	recorded(Name,X,Ref),X1 is X+1,
%	erase(Ref),recorda(Name,X1,_).

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 */