/*

	tokio interpreter on tokio
		Thu Sep  4 11:06:06 GMT+9:00 1986

*/


% main parts
solve((A,B)):- solve(A),solve(B).
solve(A):- t_clause(A,B),solve(B).

%% temporal operators
solve((A && B)):-
	solve(A) && solve(B).
solve(#A):-
	#solve(A).
solve(@A):-
	@solve(A).
solve(next(A)):-
	next(solve(A)).
solve(keep(A)):-
	keep(solve(A)).
solve(length(N)):-
	length(N).

%% functions
solve(A=B) :- eval(A,V),eval(B,V1),!,V=V1.
eval(V1,V) :- atomic(V1),!,V=V1.
eval(V1,V) :- var(V1),!,V=V1.
eval(@A,V) :- next(eval(A,V1)), V = @V1.
eval(A+B,V) :- eval(A,AA),eval(B,BB), V=AA+BB.

%% system predicates
solve(A):- sys(A),prolog(A).

sys(write(_)).
sys(nl).
sys(true).

%% assertions
t_clause( counter(A) , (@A=A+1, next(counter(A)))).

t_clause( ap([],A,A) , true).
t_clause( ap([H|X],Y,[H|Z]), ap(X,Y,Z)).

%% tester
test1 :- solve((
	length(5),#write(1)
    )).

test2 :- solve((
	length(3),#write(0) &&
	length(2),#write(1)
    )).

test3 :- solve((    % this does not work
	length(5),A=1, #(@A=A+1), #write(A)
    )).

test4 :- solve((
	length(5),A=1,counter(A),#write(A)
    )).

test5 :- solve((
	ap(A,B,[1,2,3]),write((A,B)),nl,fail
    )).

%%