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

% :- ensure_loaded('../tableau/lite').
:- module(lite).
:- 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(update);true),!,
	bdt2itl(ITL,ITL1),
        nl,write('state('),write(S),  % (
        (verbose,write(' , '), write(ITL1),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(0),!,
	next(X,Y).

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

tcl_exit :-
    tcl(X),tcl_delete(X),retract(tcl(X)).

tcl_name(L,Name) :-
	concatenate(L,L1),
	name(Name,L1).

concatenate([],[]).
concatenate([H|T],X) :- atomic(H),!,
	name(H,List),concatenate(T,X1),append(List,X1,X).
concatenate([H|T],X) :-  H=[_|_],
	concatenate(T,X1),append(H,X1,X).

tcl_eval(E) :- atomic(E),!,
	tcl(Tcl),tcl_eval(Tcl,E,_).
tcl_eval(E) :- E=[_|_],tcl_name(E,N),
	tcl(Tcl),tcl_eval(Tcl,N,_).

init_display :-
	(retract(r_event(_,_)),fail;true),
         tk_new([name('Lite Verifier')], Tcl),
	assert(tcl(Tcl)),
%	tcl_eval('source disp.tcl'),
	tcl_eval('source xf-disp'),
        all_disable.
canvas_origin(20,20).

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

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

% !,X=1 -> verbose(on); verbose(off). causes error
execute(verbose,X) :- X='1' -> verbose(on); verbose(off).
execute(map,X) :- !,name(X,L),name(X1,L),view_state(a,X1).
execute(execute,_) :- !,do_execute,!.
execute(generate,_) :- !,
	generate.
execute(counter,_) :- !,do_diagnosis,!.
execute(quit,_) :- !. % ,tcl_eval('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),generate.
gen(X) :- 
	name(X,XL),append(XL,".lite",YL),name(X1,YL),
	consult(X1),specification(Y),ex(Y),generate.

verify(X) :-
        all_disable,
	abolish(st,3),abolish(specification,1),abolish(st_variables,2),
	t2string(X,X0),s2terms(X0,X1),command(X1,X2,X3),
	display_contents(X3),
	ex(X2),!,
	ttyflush, display_statistics,
        all_enable.
verify(_) :-
        all_disable.

display_contents(X) :-
	ttyflush,t2string(X,XS0),easy_pp(XS0,XS),
	tcl_eval('$symbolicName(entry) delete 0.0 end'),
	tcl_eval(['$symbolicName(entry) insert 0.0 {',XS,'}']),
        display_update.

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

% Backtrack Control of example/counter example

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

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

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

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

% :- 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 :-
        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(["$symbolicName(states) configure -text {",S2,"}"]),!.

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

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

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

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

clear_display :-
	tcl_eval('$symbolicName(canvas) delete all').
display_ce(Hist,View) :-
	canvas_origin(OX,OY),
	font(_,Fs),
	clear_display,
	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),
	X2 is X1+X,
	display_ce(Hist,L,View,X2,Y,W,H,0). % ,View=>batchmodeoff.
display_var([],_,_,_,_,X,X):-!.
display_var([Var|L],View,X,Y,H,X1,X2):- atomic(Var),!,
	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),
	display_var(L,View,X,Y1,H,X3,X2).
display_var([Var|L],View,X,Y,H,X1,X2):- 
	functor(Var,VarH,2),member(VarH,[(^)]),!,
	arg(1,Var,VarA),arg(2,Var,VarB),
	% infix operator
	Y1 is Y+H, font(_Fn,Fs),
	name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB),
	append(VarTextA,VarTextH,VarText0),
	append(VarText0,VarTextB,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),
	display_var(L,View,X,Y1,H,X3,X2).
display_var([Var|L],View,X,Y,H,X1,X2):- 
	functor(Var,VarH,2),
	arg(1,Var,VarA),arg(2,Var,VarB),
	Y1 is Y+H, font(_Fn,Fs),
	name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB),
	CB is "(",CE is ")",CC is ",",
	append(VarTextH,[CB|VarTextA],VarText0),
	append(VarText0,[CC|VarTextB],VarText1),
	append(VarText1,[CE],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),
	display_var(L,View,X,Y1,H,X3,X2).

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

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

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

display_update :- tcl_eval('update').

view_state(View,W) :-
   itl_state_number(S),
   clear_display,
   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),
   view_state_write(View,W0,S,D).

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) :- 
   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),
   display_update,
   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).

% sicstus dependent 
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([C,C1,C2,CB|T],C3,N) :- [C,_,C2,CB]="[a](",!,  % quote '[a]'
	CQ is "'", C3 = [CQ,C,C1,C2,CQ,CB|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 %