%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% LITE Tcl/Tk interface
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% :- ensure_loaded('../Lite/lite').
:- ensure_loaded('../lite').

:- module(lite).

% :- use_module(library(tk)).
:- use_module(library(tcltk)).
:- verbose(off).

:- dynamic r_event/2.

:- abolish(show_state,2).
% Next command keep check event during verification
show_state(S,ITL) :-!,
%        (tcl_eval(I,update,_);true),!,
        (tk_do_one_event;true),
        nl,write('state('),write(S),  % (
        (verbose,write(' , '), write(ITL),write(')'),nl;write(')')),!.

event(verbose,'1') :- verbose(on).
event(verbose,'0') :- verbose(off).
event(X,Y) :- assertz(r_event(X,Y)).   % ,write((X,Y)),nl.
event(X) :-   assertz(r_event(X,[])).  % ,write((X)),nl.

next(X,Y) :- r_event(_,_),retract(r_event(X,Y)),!.
next(X,Y) :- tk_do_one_event,!,
	next(X,Y).
next(X,Y) :- next(X,Y).

display :-
	init_display(I),!,
	event_loop(run,I).

init_display(I) :-
	(retract(r_event(_,_)),fail;true),
%	tk_init('lite',[]),
	tk_new([],I),
%	tcl_eval('source disp.tcl'),
	tcl_eval(I,'source xf-disp',_),
        all_disable(I).
canvas_origin(20,20).

event_loop(quit,_I):-!.
event_loop(_,I) :-
	next(X,Y),execute(X,Y,I),!,event_loop(X,I).

execute(verify,X,I) :- !,
	verify(X,I).

% !,X=1 -> verbose(on); verbose(off). causes error
execute(verbose,X,_) :- X='1' -> verbose(on); verbose(off).
execute(map,X,I) :- !,name(X,L),name(X1,L),view_state(a,X1,I).
execute(execute,_,I) :- !,do_execute(I),!.
execute(generate,_,_) :- !,
	generate.
execute(counter,_,I) :- !,do_diagnosis(I),!.
execute(quit,_,I) :- !,
	tcl_eval(I,'destroy .',_),
	tcl_delete(I).
%	tcl_eval(I,'destroy .',_).
execute(prolog_call,X,_) :- !,prolog_call(X).
execute(tokio_call,X,_) :- !,tokio_call(X).
execute(X,_,_) :- !,write(event(X)),nl,ttyflush.

generate :-
	TOKIO = 'tmp.tokio',
	tell(TOKIO),tgen,told,
        user:com(TOKIO,'tmp.out').
gen(X) :- consult(X),specification(Y),ex(Y),flush_output,generate.
gen(X) :- 
	name(X,XL),append(XL,".lite",YL),name(X1,YL),
	consult(X1),specification(Y),ex(Y),flush_output,generate.

verify(X,I) :-
        all_disable(I),
	abolish(st,3),abolish(specification,1),abolish(st_variables,2),
	t2string(X,X0),s2terms(X0,X1),command(X1,X2,X3),
	display_contents(X3,I),
	ex(X2),!,
	ttyflush, display_statistics(I),
        all_enable(I).
verify(_,I) :-
        all_disable(I).
display_contents(X,I) :-
	ttyflush,t2strings(X,XS0),easy_pp(XS0,XS),
	tcl_eval(I,'$symbolicName(entry) delete 0.0 end',_),
	tcl_eval(I,['$symbolicName(entry) insert 0.0 {',chars(XS),'}'],_),
        display_update(I).

all_disable(I) :-
	tcl_eval(I,'$symbolicName(map) configure -state disabled',_),
	tcl_eval(I,'$symbolicName(execute) configure -state disabled',_),
	tcl_eval(I,'$symbolicName(diag) configure -state disabled',_),
	display_update(I).
all_enable(I) :-
	tcl_eval(I,'$symbolicName(map) configure -state normal',_),
	tcl_eval(I,'$symbolicName(execute) configure -state normal',_),
	tcl_eval(I,'$symbolicName(diag) configure -state normal',_),
	display_update(I).

% Backtrack Control of example/counter example

do_execute(I) :- display_exe('.',I),next(X,Y),do_execute(X,Y,I),!.
do_execute(_I).

do_execute(execute,_,_) :-!,
	fail.
do_execute(X,Y,I) :- execute(X,Y,I),!.

do_diagnosis(I) :- display_diag(',',I),next(X,Y),do_diagnosis(X,Y,I),!.
do_diagnosis(_).

do_diagnosis(diag,_,_) :-!,
	fail.
do_diagnosis(X,Y,I) :- execute(X,Y,I),!.

% :- dynamic specification/1.

% Text Based Commnad

command([st(X,Y,Z)|T],Term,[st(X,Y,Z)|T1]):-!,
	assertz(st(X,Y,Z)),!,
	command(T,Term,T1).
command([specification(X)|T],X,[specification(X)|T1]):-!,
	command(T,X,T1).
command([st_variables(X,Y)|T],Term,[st_variables(X,Y)|T1]):-!,
	assertz(st_variables(X,Y)),
	command(T,Term,T1).
command([],true,[]) :-!.
command([],_,[]) :-!.
command([H],Term,[Term1]) :-!,
	command(H,Term),!,Term=Term1.
command([H|T],(Term1,Terms),[Term1|T1]) :-
	command(H,Term1),!,command(T,Terms,T1).

command(demo(X),Term):-!,lite:demo(X,Term).   % predefined examples
command(ex(X),Term):-!,ex(X,Term).
command(prolog(X,P),X):-!,safe_call(P).
command(prolog(P),true):-!,safe_call(P).
command(tokio(P),true):-!,safe_call(tokio(P)).
command(consult(P),Term):-!,
	command(file(P),Term).
command(file(P),Term):-
	on_exception(Er,(consult(P),specification(Term)),
           read_error(Term,Er,user,user)).
command(A,A) :- atomic(A),!.
command(P,R) :- functor(P,H,N),functor(R,H,N),
        command_arg(N,P,R).
command_arg(0,_P,_R):-!.
command_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
        N1 is N-1,command(PA,RA),command_arg(N1,P,R).

prolog_call(X) :- 
	t2string(X,X0),s2terms(X0,[X1|_]),safe_call(X1).
tokio_call(X) :- 
	t2string(X,X0),s2terms(X0,[X1|_]),safe_call(tokio(X1)).

safe_call(X) :-
	on_exception(Er,user:call(X),
           read_error(X,Er,user,user)),!.
safe_call(_).

:-dynamic font/2.

small :- (retract(font(_,_));true),assert(font("7x14",14)).
large :- (retract(font(_,_));true),assert(font("12x24",24)).

:-small.
% font("7x14",14).

width(W,H):-
   font(_,Fs),
   W is integer(1000/24*Fs), H is integer(500/24*Fs).

display_statistics(I) :-
        itl_state_number(S), % number of state
        itl_transition(L),!, % number of transition
        name(S,Ss),name(L,Ls),
        append("State: ",Ss,S0),append(S0," Edge:",S1),append(S1,Ls,S2),
        tcl_eval(I,['$symbolicName(states) configure -text {',chars(S2),'}'],_),!.
display_statistics(I) :-
        itl_state_number(S), % number of state
        itl_transition(L),!, % number of transition
        name(S,Ss),name(L,Ls),
        append("State: ",Ss,S0),append(S0," Edge:",S1),append(S1,Ls,S2),
        tcl_eval(I,['$symbolicName(states) configure -text {',chars(S2),'}'],_),!.

%%---------------------------------------------------------------------
% display_diagnosis
display_diag(View,I) :- diag(X),
	write_display_diag(X,View,I).

% display_execution exapmle.
display_exe(View,I) :- exe(Z),
	write_display_diag(Z,View,I).

write_display_diag(counter_example(Hist),View,I) :-!,display_ce(Hist,View,I).
write_display_diag(execution(Hist),View,I) :-!,display_ce(Hist,View,I).
write_display_diag(R,_View,I):-!,
	atomic(R),
	clear_display(I),
	tcl_eval(I,['$symbolicName(canvas) create text 0 0 -text "',R,'"'],_).

append([],X,X):-!.
append([H|X],Y,[H|Z]) :- append(X,Y,Z).

clear_display(I) :-
	tcl_eval(I,'$symbolicName(canvas) delete all',_).
display_ce(Hist,View,I) :-
	canvas_origin(OX,OY),
	font(_,Fs),
	clear_display(I),
	X is OX+Fs/2,Y=OY,W is integer(60/24*Fs),H is integer(60/24*Fs),
	(variable_list(L);L=[]),append(L,['Time'],L1),!,
	display_var(['State'|L1],View,X,Y,H,X,X1,I),
	X2 is X1+X,
	display_ce(Hist,L,View,X2,Y,W,H,0,I). % ,View=>batchmodeoff.
display_var([],_,_,_,_,X,X,_):-!.
display_var([Var|L],View,X,Y,H,X1,X2,I):-
	Y1 is Y+H, font(_Fn,Fs),
	name(Var,VarText),length(VarText,Len0),Len is Len0*Fs,
	% View=>stringlength(VarText,Len),
	(X1>X+Len,X3=X1;X3 is X+Len),!,
	display_string(X,Y,VarText,I),
	display_var(L,View,X,Y1,H,X3,X2,I).

display_string(X,Y,Text,I) :-
	font(Fn,_),
        tcl_eval(I,['$symbolicName(canvas) create text ',X,' ',Y,' -font ',chars(Fn),
                  ' -text "', chars(Text),'"'
        ],_).
display_ce([],_,_,_,_,_,_,_,_):-!.
display_ce([(S->[_|Cond])|Hist],L,View,X,Y,W,H,T,I) :-
	X1 is X+W,Y1 is Y+H,T1 is T+1,
	name(S,SText),display_string(X1,Y,SText,I),
	display_now(L,Cond,View,X1,Y1,W,H,T,I),
	display_ce(Hist,L,View,X1,Y,W,H,T1,I).

display_now([],_,_View,X,Y,_,_,T,I):-!,
	name(T,SText),display_string(X,Y,SText,I).
display_now([V|Vr],Cond,View,X,Y,W,H,T,I):-
	XS is X-H/2,YS is Y-H/2,
	display_state(Cond,V,View,XS,YS,W,H,I),
	Y1 is Y+H,
	display_now(Vr,Cond,View,X,Y1,W,H,T,I).

rectangle(1,X,Y,X2,Y2,I) :-!,
        tcl_eval(I,['$symbolicName(canvas) create rectangle ',
                  X,' ',Y,' ', X2,' ',Y2,' ',
                 '-stipple gray50 -fill black'
        ],_).
rectangle(0,X,Y,X2,Y2,I) :-
        tcl_eval(I,['$symbolicName(canvas) create rectangle ',
                  X,' ',Y,' ', X2,' ',Y2
        ],_).
display_state([V|_],V,_View,X,Y,W,H,I) :-!, % true
	X2 is X+W,Y2 is Y+H,
	rectangle(1,X,Y,X2,Y2,I).
display_state([not(V)|_],V,_View,X,Y,W,H,I) :-!, % false
	X2 is X+W,Y2 is Y+H,
	rectangle(0,X,Y,X2,Y2,I).
display_state([_|T],V,View,X,Y,W,H,I) :-!,
	display_state(T,V,View,X,Y,W,H,I).
display_state([],_,_View,X,Y,W,H,I) :-!,    % unknown
	X2 is X+W,Y2 is Y+H/2,Y3 is Y2+3,
	rectangle(0,X,Y2,X2,Y3,I).

display_update(I) :- tcl_eval(I,'update',_).

view_state(View,W,I) :-
   itl_state_number(S),
   clear_display(I),
   canvas_origin(OX,OY),
   calc_view_size(W,S,D,W0),
%   write(calc_view_size(W,S,D,W0)),nl,
   W1 is OX + W0 + D, H1 is OY + W0 + D,
   rectangle(0,OX,OY,W1,H1,I),
   view_state_write(View,W0,S,D,I).

calc_view_size(W,S,D,W1) :-
   D0 is integer(W/(S+1)),(D0<2,D=2;D=D0),!,
   W0 is D*(S+1),(W0=<W,!,W1 = W0; W1 is integer(W)),!.

view_state_write(_View,W,S,D,I) :- 
   canvas_origin(OX,OY),
   links(X,Y), link_translate(X,Y,X1,Y1,W,S),
   X2 is OX+X1+D,Y2 is OY+Y1+D,
   X11 is OX+X1,Y11 is OY+Y1,
   rectangle(1,X11,Y11,X2,Y2,I),
   display_update(I),
   fail.
view_state_write(_View,_,_,_,_):-true. 

link_translate(false,Y,X1,Y1,W,S) :- !,
    link_translate(S,Y,X1,Y1,W,S).
link_translate(X,false,X1,Y1,W,S) :- !,
    link_translate(X,S,X1,Y1,W,S).
link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!,
    X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)).
link_translate(X,_,X1,0,W,S) :- number(X),!,
    X1 is integer(X*W/(S+1)).
link_translate(_,Y,0,Y1,W,S) :- number(Y),!,
    Y1 is integer(Y*W/(S+1)).
link_translate(_,_,0,0,_,_).

%%

s2term("",true):-!.
s2term(Text,Term) :-
	telling(O),
	tell(tmp),format("~s.~n",[Text]),told,tell(O),
	seeing(I),
	see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)),
	see(tmp),seen,see(I),!.
s2term(_,true):-tell(tmp),told,see(tmp),seen.

s2terms("",true):-!.
s2terms(Text,Terms) :-
	check_period(Text,0,Text1),
	telling(O),
	tell(tmp),format("~s~n",[Text1]),told,tell(O),
	seeing(I),
	see(tmp),on_exception(Er,s2terms0(Terms),read_error(Terms,Er,I,O)),
	see(tmp),seen,see(I),!.
s2terms(_,true):-tell(tmp),told,see(tmp),seen.

s2terms0(Terms) :-read(X),s2terms0(X,Terms).
s2terms0(end_of_file,[]):-!.
s2terms0(H,[H|T]):-read(X),s2terms0(X,T).

read_error(true,Er,I,O) :- 
	tell(tmp),told,see(tmp),seen,
	see(I),tell(O),    %   unix(system('rm tmp')),
	write('read error:'),write(Er),nl.

t2string(Term,Text) :-
	telling(O),
	tell(tmp),write(Term),told,tell(O),
	seeing(I),
	see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
t2string(_,true):-tell(tmp),told,see(tmp),seen.

t2strings(Terms,Text):-!,
	telling(O),
        t2strings(Terms),
        told,tell(O),
	seeing(I),
	see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
t2strings(_,true):-tell(tmp),told,see(tmp),seen.

t2strings([]):-!.
t2strings([Term|T]):-!,
	tell(tmp),write(Term),put("."),put(10),t2strings(T).

read_string(-1,[]) :- !.
read_string(C,[C|T]) :- 
	get0(C1),read_string(C1,T).

check_period([],0,[32,46]):-!.
check_period([],1,[]):-!.
check_period([46],_,[46]):-!.
check_period([46,X|T],_,[46,X|T1]):-(X=32;X=10;X=37),!,
	check_period(T,1,T1).
check_period([37|T],X,[37|T1]):-
	skip_line(T,X,T1).
check_period([X|T],P,[X|T1]):-(X=32;X=10),!,
	check_period(T,P,T1).
check_period([X|T],_,[X|T1]):-
	check_period(T,0,T1).

skip_line([],X,[]):-!,
	check_period([],X,_).
skip_line([10|T],X,[10|T1]):-!,
	check_period(T,X,T1).
skip_line([_|T],X,T1):-skip_line(T,X,T1).

easy_pp(X,X1) :- easy_pp(X,X1,0).
easy_pp([],[10],_) :- !.
easy_pp([C|T],[C1,10|T0],_) :- C is ".",!,C1 = C,
	easy_pp(T,T0,0).
easy_pp([C|T],[C1,10|T0],N) :- C is ",",!,C1 = C,
	easy_tab(N,T0,T1),easy_pp(T,T1,N).
easy_pp([C|T],[C1,10|T0],N) :- C is ";",!,C1 = C,
	easy_tab(N,T0,T1),easy_pp(T,T1,N).
easy_pp([C,C|T],[C1,C1,10|T0],N) :- C is "&",!,C1 = C, % &&
	easy_tab(N,T0,T1),easy_pp(T,T1,N).
easy_pp([C|T],[C1,10|T0],N) :- C is "&",!,C1 = C,      % &
	easy_tab(N,T0,T1),easy_pp(T,T1,N).
easy_pp([10|T],[10|T0],N) :- !,
	easy_tab(N,T0,T1),easy_pp(T,T1,N).
easy_pp([Par|T],[Par1|T0],N) :- Par is "(",!,Par1 = Par,
	N1 is N+1,easy_pp(T,T0,N1).
easy_pp([Par|T],[Par1|T0],N) :- Par is ")",!,Par1 = Par,
	N1 is N-1,easy_pp(T,T0,N1).
easy_pp([H|T],[H|T0],N) :- 
	easy_pp(T,T0,N).

easy_tab(N,T,T1):-N =< 0,!,T=T1.
easy_tab(N,[32,32|T],T1) :-
	N1 is N-1,easy_tab(N1,T,T1).

% end %