/*
 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
 $Header$
*/
:-dynamic define/2.
% ITL chop standard form
% requires ndcomp

def(~(P),not(P)).				% not
def((P->Q),(not(P);Q)).				% imply
def(P<->Q,((not(P);Q),(P; not(Q)))).		% equiv
def(P=Q,((not(P);Q),(P; not(Q)))).		% equiv 
def((P && Q),((not(empty),P) & Q)).		% strong chop
def('<>'(Q),(true & Q)).			% sometime
def('#'(Q), not(true & not(Q))).		% always
def('[]'(Q), not(true & not(Q))).		% always
def('[a]'(Q), not(true & not(Q) & true)).	% always with arbitary fin
def('<a>'(Q), (true & Q & true)).	% sometime with arbitary fin
def(fin(Q),(true & (empty,Q))).			% final state in the interval
def(keep(Q), not(true & not((empty ; Q)))).	% except final state
def(halt(Q), '[]'(empty=Q)).	
def(more, not(empty)).				% non empty interval
% discrete stuff
def(skip, @(empty)).				% 1 length interval
def(infinite, (true & false)).			% 
def(finite, ~((true & false))).			% 
def(length(I), X):- I>=0 ,def_length(I,X).	% length operator
def(less(I), X):- I>=0 ,def_less(I,X).		% less than N length
def(next(P),(empty; @(P))).
% temporal assignments
def(gets(A,B),keep(@A<->B)).
def(stable(A),keep(@A<->A)).
def(state(A),(share(A),'[]'(L))):- def_state(A,L).
% def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R)))).
%   easier one
% def(Q=>P,(Q & (empty,P); ~Q & (empty, ~P))).
% def(P<=Q,Q=>P).
% loop stuff and quantifiers
def(+A ,(A & *((empty;A)))).  % weak closure
def(while(Cond,Do), *(((Cond->Do) , (~Cond->empty)))).
def(repeat(Do,until,Cond), (*((Do;empty)) ,@ halt(Cond))).
def(all(P,Q),not(exists(P,not(Q)))):-!,
	atomic(P).  % more check is necessary
def(local(P), (P = (P&true))):- !.
% test predicates
def(trace(X,List),L) :- !,make_trace(List,X,L).
def(even(P),
	exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P))))).
def(evenp(P),(
	*(((P,skip) & skip;empty,P)) & (empty;skip)
)). 
def(phil(L,R),
       +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )).
def(X,Y) :- define(X,Y).

def_length(I,empty):-I=<0,!.
def_length(I,@ X):-I1 is I-1,def_length(I1,X).
def_less(I,false):-I=<0,!.
def_less(I,next(X)):-I1 is I-1,def_less(I1,X).
def_state([H],H):-!.
def_state([H|L],(H;L1)):-def_state(L,L1).
make_trace([],_,true):-!.
make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L).
make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L).
make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L).
make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L).

:-dynamic variable/1.

expand(X,Y) :- init_variable,expand1(X,Y).

expand1(V,V) :- var(V),!.
expand1((P,Q),R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
expand1(st(R),st(R)) :- !,
	st_variables(In,Out),add_variable(In),add_variable(Out).
% expand1([P|Q],R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
expand1((P;Q),R) :- !,expand1(P,P1),expand1(Q,Q1),or(P1,Q1,R).
expand1((P&Q),R) :- !,expand1(P,P1),expand1(Q,Q1),chop_expand1(P1,Q1,R).
expand1(not(Q),NQ):-!,expand1(Q,Q1),negate(Q1,NQ).
expand1(exists(P,Q),exists(P,Q1)):-
	nonvar(P),name(P,[X|_]),X = 95,!, % "_"  % reuse it...
	expand1(Q,Q1).
expand1(exists(P,Q),exists(P,Q1)):-var(P),!,
	new_var(P), 
	expand1(Q,Q1).
expand1(exists(P,Q),exists(P,Q1)):-!,
	expand1(Q,Q1).
expand1([],[]):-!.
expand1([H|L],?(And,true,?(NAnd,false,true_false))):-!, 
        % non-deterministic selection
	expand_list([H|L],L1),
	all_and(L1,And),
	all_not(L1,NAnd).
expand1(^(R),^(R)):-!,           % 2nd order variable
	add_2var(R).
expand1(P,R) :- def(P,Q),!,expand1(Q,R).
expand1(P,P) :- atomic(P),!,     % for empty or skip
	check_atomic(P).
expand1(P,R) :- functor(P,H,N),functor(R,H,N),
	expand_arg(N,P,R).
expand_arg(0,_P,_R):-!.
expand_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
	N1 is N-1,expand1(PA,RA),expand_arg(N1,P,R).

chop_expand1(false,_,false):-!.
%   chop_expand1(_,false,false):-!.
chop_expand1(true,true,true):-!.
chop_expand1(P,Q,(P&Q)):-!.
expand_list([],[]) :-!.
expand_list([H|L],[H1|L1]) :-
    expand1(H,H1), expand_list(L,L1).
all_and([],true):-!.
all_and([H|L],F):- all_and(L,F1),and(H,F1,F).
all_not([],true):-!.
all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F).
check_atomic(empty):-!.
check_atomic(more):-!.
check_atomic(true):-!.
check_atomic(false):-!.
check_atomic(true_false):-!.
check_atomic(P) :- name(P,PL),PL=[95|_],!.
check_atomic(P) :- add_variable(P). % "_"

% do not use abolish here to avoid erase dynamic property of variable/1
init_variable :- retract(variable(_)),fail;true.
add_variable([]):-!.
add_variable([X|T]) :- !,add_variable(X),add_variable(T).
add_variable(X) :- variable(X),!.
add_variable(X) :- assertz(variable(X)),!.
variable_list(L) :- setof(X,variable(X),L).

new_var(P) :-
	(retract(sbn(N));N=1),N1 is N+1,asserta(sbn(N1)),!,
	name(N1,X),S = 95,name(P,[S|X]). % "_"

add_2var(R) :- length_limit(N),!,
	add_variable(over(R,N)),
	add_2var(N,R).
add_2var(R) :-
	add_variable(^(R)).
add_2var(0,R):-!,
	add_variable(^(R,0)).
add_2var(N,R):- N1 is N-1,
	add_variable(^(R,N)),
	add_2var(N1,R).

and(false,_,false):-!.
and(_,false,false):-!.
and(true,T,T):-!.
and(T,true,T):-!.
and(T,T,T):-!.
and(A,B,(A,B)):-!.

or(true,_,true):-!.
or(_,true,true):-!.
or(false,T,T):-!.
or(T,false,T):-!.
or(T,T,T):-!.
or(A,B,(A;B)):-!. 

negate(true,false):-!.
negate(false,true):-!.
negate(true_false,true_false):-!.
negate(not(N),N):-!.
negate(N,not(N)):-!.

/* */