
% ----------------------------------------------------------------------

/*
	TOY PICT
	A very small and incomplete version of the Pict core language.
	NB: when backtracking, still seems to find the same transitions
	in more than one way => still some redundancy in rules.
*/

% ----------------------------------------------------------------------

% Meta-ops:
:- op(1000,fx,run).
:- op(900,xfx,==>).	% action
:- op(900,xfx,===>).	% actions till stop
:- op(900,xfx,--->).	% reduction of application
:- op(850,xfx,@).	% substitution
:- op(900,xfx,:=).	% definition

% Ops:
:- op(700,xfy,&).	% concurrent composition
:- op(700,xfy,?).	% input
:- op(700,xfy,?*).	% repeated input
:- op(700,xfy,>).	% abstraction
:- op(600,xfy,!).	% output
% :- op(200,xfy,\).	% new (not used)

% ----------------------------------------------------------------------

run(P)				:-	print(P), nl, P ===> _ .

P ===> End			:-	act(P,Comm,R),
						print('	'), print(Comm), nl,
						print('=> '), print(R), nl,
					R ===> End.

P ===> P			:-	dead(P).

% ----------------------------------------------------------------------

Process ==> NewProcess		:-	act(Process, _, NewProcess).

% ----------------------------------------------------------------------

act(P1&Q1, Comm, P2&Q2)			:-	out(P1,Comm,P2),
						in(Q1,Comm,Q2).

act(P1&Q1, Comm, P2&Q2)			:-	in(P1,Comm,P2),
						out(Q1,Comm,Q2).

act(P&Process, Comm, P&NewProcess)	:-	act(Process, Comm, NewProcess) .
act(Process&P, Comm, NewProcess&P)	:-	act(Process, Comm, NewProcess) .
act(N, Comm, R)				:-	N := P, !,
						act(P, Comm, R).

dead(P)					:-	act(P,_,_), !, fail.
dead(_).

% ----------------------------------------------------------------------

out(Channel!Message, Channel!Message, nil).

out(P & Q, Comm, P & R)		:- out(Q, Comm, R).
out(P & Q, Comm, R & Q)		:- out(P, Comm, R).
out(N, Comm, R)			:- N := P, !, out(P, Comm, R).

/*
out(N\P, Comm, R)			:- gensym(N,UN),
						P @ {[UN]/[N]} ---> P1,
						out(P1, Comm, R).
*/

% ----------------------------------------------------------------------

in(Channel?Pattern>AbsProcess, Channel!Message, NewProcess)
		:-	AbsProcess @ {Message/Pattern} ---> NewProcess .

in(Channel?*Pattern>AbsProcess,
		Channel!Message,
	(Channel?*Pattern>AbsProcess) & NewProcess)
		:-	AbsProcess @ {Message/Pattern} ---> NewProcess .

in(P & Q, Comm, P & R)		:- in(Q, Comm, R).
in(P & Q, Comm, R & Q)		:- in(P, Comm, R).
in(N, Comm, R)			:- N := P, !, in(P, Comm, R).

/*
in(N\P, Comm, R)			:- gensym(N,UN),
						P @ {[UN]/[N]} ---> P1,
						in(P1, Comm, R).
*/

% ----------------------------------------------------------------------

/*
	AbsExpr @ {Value/Pattern} ---> Expr .
	Need rules for every possible subexpression.
*/

D @ {XL/NL} ---> E			:-	D := P, !,
						P @ {XL/NL} ---> E .

M @ {[_]/[N]} ---> M			:-	atom(M), M \== N, !.
Expr @ {[]/[]} ---> Expr .

N @ {[X]/[N]} ---> X			:-	!.
[N] @ {[X]/[N]} ---> [X] .

CE?AProc @ {XL/NL} ---> C?Proc		:-	CE @ {XL/NL} ---> C,
						AProc @ {XL/NL} ---> Proc.

CE?*AProc @ {XL/NL} ---> C?*Proc	:-	CE @ {XL/NL} ---> C,
						AProc @ {XL/NL} ---> Proc.

CE!AMsg @ {XL/NL} ---> C!Msg		:-	CE @ {XL/NL} ---> C,
						AMsg @ {XL/NL} ---> Msg.

P&Q @ {XL/NL} ---> PR & QR		:-	P @ {XL/NL} ---> PR,
						Q @ {XL/NL} ---> QR.

Pat>Abs @ {XL/NL} ---> PatR>AbsR	:-	Pat @ {XL/NL} ---> PatR,
						Abs @ {XL/NL} ---> AbsR.

% ----------------------------------------------------------------------

