%   Alone, this file specifies the piI-calculus of Davide Sangiori.
%
%   To get the specification of the late transitions for the pi-calculus,
%   use the file late.mod.  To get the specification of the early
%   transitions for the pi-calculus, use the file early.mod.
%
%   Notice that the clauses in this file are in L-lambda, while
%   adding either the late or early communication rules takes you 
%   outside L-lambda.
%
%   The specification of definitions or replication ! have been left
%   out (they are easy to treat too).
%
%   Dale Miller, 1 October 96

module core.

% pre
one (tauu P)     (pair  tau      P).       % tau-act
one (out X Y P)  (pair  (oo X Y) P).       % output-act
one (in X M)     (pairA (ii X)   M).       % input-act

one (plus P Q) R      :- one P R; one Q R. % sum
one (match X X P) R   :- one P R.          % match

% par - no dependency
one (par  P Q)  (pair A (par Px Q)) &
one (par  Q P)  (pair A (par Q Px)) :- one P (pair A Px).

% par - dependency
one (par  P Q)  (pairA A (n\(par (Px n) Q))) &
one (par  Q P)  (pairA A (n\(par Q (Px n)))) :- one P (pairA A Px).

% close
one (par P Q) (pair tau (nu n\(par (Px n) (Qx n)))) :-
  one P (pairA (oo X) Px),
  one Q (pairA (ii X) Qx).

% res
one (nu P) (pair  A (nu Px)) :-
  pi n\(one (P n) (pair  A (Px n))).

one (nu P) (pairA A m\(nu n\(Px n m))) :-
  pi n\(one (P n) (pairA A (Px n))).

% open
one (nu P) (pairA(oo X) Px) :-
  pi y\(one (P y) (pair (oo X y) (Px y))).