(*********************************************************************
**********************************************************************

 File name: pi-calculator.ml

 Fresh O'Caml program to calculate the possible labelled transitions 
 from a process expression in the Milner-Parrow-Walker Pi-Calculus.

 Usage: see the section on HOW TO USE THIS FILE, below.

 Author: A.M.Pitts

 Date: 2003-08-08

 Reference:

 [SW] Davide Sangiorgi and David Walker, "The pi-calculus: a theory of
 mobile processes" (CUP, 2001).

*********************************************************************
*********************************************************************)

(**********************************************************************
 Some GENERAL FUNCTIONS
**********************************************************************)

let mapPartial (f : 'a -> 'b option) : 'a list -> 'b list =
  let rec map (xs : 'a list) : 'b list =
    match xs with
	[] -> []
      | x :: xs' -> 
	  (match f x with
	      None -> map xs'
	    | Some y -> y :: map xs')
  in map;;

(* (mapMatrixPartial f xs ys) returns a list containing all those z for 
which Some z = f x y, for some x in xs and y in ys *)
let mapMatrixPartial (f : 'a -> 'b -> 'c option) 
  (xs: 'a list) (ys : 'b list) : 'c list =
  let rec m (x : 'a) (ys : 'b list) (zs : 'c list) : 'c list =
    match ys with
	[] -> zs
      | y :: ys' -> 
	  (match f x y with
	      None -> m x ys' zs
	    | Some z -> m x ys' (z :: zs)) in
  let rec ms (xs : 'a list) (ys : 'b list) (zs : 'c list) : 'c list =
    match xs with
	[] -> zs
      | x :: xs' -> ms xs' ys (m x ys zs)
  in ms xs ys [];;

(* append lists without duplicating *)
let rec ( ++ ) (xs : 'a list) (ys : 'a list) : 'a list =
  match ys with
      [] -> xs
    | y :: ys' -> 
	if List.exists ((=) y) xs then xs ++ ys'
	else (y :: xs) ++ ys';;

(*********************************************************************
 SYNTAX

 We use the following grammar for pi-calculus processes:

          processes p ::= m             guarded sum              
                          p | p         composition
                          nu x(p)       restriction
                          !p            replication
       guarded sums m ::= 0             inaction
                          a             prefixed process
                          m + m         summation
 prefixed processes a ::= out c c. p    output prefix
                          in c(x). p    input prefix
                          tau. p        unobservable prefix
                          [c = c]a      match prefix

  where c,x range over names of channels.

 This grammar is equivalent to [SW, Definition 1.1.1], but corresponds 
 more closely to the datatype proc for processes declared below, 
 which uses use abstraction types, <<chan>>(-), when representing 
 operations that bind channel names.  

 Corresponding to the syntactic categories p, m, a given above are
 datatypes proc, gsum and prefix, declared below. This file does not
 give a parser for turning strings into values of these datatypes. It
 does contain print functions for displaying such values as strings
 obeying the above grammar.

*********************************************************************)

type t;;                                (* some type *)

type chan = t name;;			(* channel names, c,x *)

type proc =                             (* pi-caluclus processes *)
    Gd of gsum				(* m *)
  | Par of proc * proc			(* p1 | p2 *)    
  | Res of <<chan>>proc			(* nu x(p) *)
  | Rep of proc				(* !p *)
and gsum =				(* guarded sums, m *)
    Inact				(* 0 *)
  | Pre of prefix			(* a *)
  | Plus of gsum * gsum			(* m1 + m2 *)
and prefix =				(* prefixes, a *)
    Out of chan * chan * proc		(* out c1 c2. p *)
  | In of chan * (<<chan>>proc)		(* in c(x). p  *)
  | Tau of proc				(* tau. p *)
  | Match of chan * chan * prefix;;     (* [c1 = c2]a *)


(********************************************************************* 
 RENAMING FUNCTION

 (c |-> c')p gives the result of capture-avoiding substitution in
 p:proc of the channel name c':chan for all occurrences of c:chan that
 are not within the scope of a binder <<c''>>(-).

 Note: the definition of rename is remarkably simple! 
 (because of the way FreshML handles binding operations)
*********************************************************************)

let ( |-> ) (c : chan) (c' :chan) : proc -> proc =
  let rec rename (p : proc) : proc =
    match p with
	Gd m -> Gd(renameg m)
      | Par(p1, p2) -> Par(rename p1, rename p2)
      | Res(<<x>>p1) -> Res(<<x>>(rename p1))
      | Rep p1 -> Rep(rename p1)
  and renameg (m : gsum) : gsum =
    match m with
	Inact -> Inact
      | Pre a -> Pre(renamep a)
      | Plus(m1, m2) -> Plus(renameg m1, renameg m2)
  and renamep (a : prefix) : prefix =
    match a with 
	Out(c1, c2, p) -> Out(renamec c1, renamec c2, rename p)
      | In(c1, <<x>>p) -> In(renamec c1, <<x>>(rename p))
      | Tau p -> Tau(rename p)
      | Match(c1, c2, a) -> Match (renamec c1, renamec c2, renamep a)
  and renamec (c1 : chan ) : chan =
    if c1 = c then c' else c1
  in rename;;


(*********************************************************************
 LABELLED TRANSITION SYSTEM
  
  We are going to use the "late transition system" defined in [SW,
  Definition 4.3.1]. This is because it enables us to give a _finite_
  list of outcomes of one step of transition, relying on the "image
  finiteness" properties of the labelled transition system---see [SW,
  Corollary 1.4.6] (which refers to the "early" transition system) and
  [SW, Lemma 4.3.2] (which explains the close relationship between late
  and early transitions).

  According to [SW, Definition 4.3.1], transitions from a process P 
  take the form 
  
  p |---act---> p'

  where act is either the unobservable action (tau), free output (out
  c1 c2), bound output (out c1(c2)), or bound input (in c1(c2)). We
  collect act and the residual process p' into a pair and then use
  name-abstraction to take account of binding. Thus the results of a
  transition from a process p are given by the values of the datatype
  value declared below. Given p : proc, (next p) : (value list) returns
  a finite list of distinct values representing all the possible
  labelled transitions steps from
  p. 

*********************************************************************)

type value =	                       (* results of a transition *)
    TauVal of proc		       (* |---tau---------> p *)
  | FrOutVal of chan * chan * proc     (* |---out c1 c2---> p *)
  | BnOutVal of chan * (<<chan>>proc)  (* |---out c(x)----> p *)
  | InVal of chan * (<<chan>>proc);;   (* |---in c(x)-----> p *)

(* Helper function for the L-PAR-L rule [SW, Table 4.1] *)
let parlVal (p : proc) (v : value) : value =
  match v with
      TauVal p1 -> TauVal(Par(p1, p))
    | FrOutVal(c1, c2, p2) -> FrOutVal(c1, c2, Par(p2, p))
    | BnOutVal(c1, <<x>>p2) -> BnOutVal(c1, <<x>>(Par(p2, p)))
    | InVal(c1, <<x>>p2) -> InVal(c1, <<x>>(Par(p2, p)));; 
 
(* Helper function for the L-PAR-R rule [SW, Table 4.1] *) 
let parrVal (p : proc) (v : value) : value =
  match v with
      TauVal p1 -> TauVal(Par(p, p1))
    | FrOutVal(c1, c2, p2) -> FrOutVal(c1, c2, Par(p, p2))
    | BnOutVal(c1, <<x>>p2) -> BnOutVal(c1, <<x>>(Par(p, p2)))
    | InVal(c1, <<x>>p2) -> InVal(c1, <<x>>(Par(p, p2)));; 

(* Synchronised communication between two values 
using the COMM-L/R and CLOSE-L/R rules [SW, Table 4.1] *)
let syncVal (v : value) (v' : value) : value option =
  match v with
      FrOutVal(c1, c2, p) ->
	(match v' with
	    InVal(c1', <<x>>p') -> 
	      if c1 = c1' then Some(TauVal(Par(p, (x |-> c2)p')))
	      else None
	  | _ -> None)
    | BnOutVal(c, <<x>>p) ->
	(match v' with
	    InVal(c', <<x'>>p') ->
	      if c = c' then 
		Some(TauVal(Res(<<x>>(Par(p, swap x and x' in p')))))
	      else None
	  | _ -> None)
    | InVal(c, <<x>>p) ->
	(match v' with
	    FrOutVal(c1, c2, p') -> 
              if c = c1 then 
		Some(TauVal(Par((x |-> c2)p, p')))
	      else None
	  | BnOutVal(c', <<x'>>p') ->
              if c = c' then 
		Some(TauVal(Res(<<x'>>(Par((swap x' and x in p), p')))))
	      else None
	  | _ -> None)
    | _ -> None;;


(* Helper function for the L-RES rule [SW, Table 4.1] *)
let resVal (c : chan) (v : value) : value option =
  match v with
      TauVal p -> Some(TauVal(Res(<<c>>p)))
    | FrOutVal(c1, c2, p) -> 
	if c = c1 then None
	else if c = c2 then Some(BnOutVal(c1, <<c>>p))
	else Some(FrOutVal(c1, c2, Res(<<c>>p)))
    | BnOutVal(c1, <<x>>p) ->
	if c = c1 then None
	else Some(BnOutVal(c1, <<x>>(Res(<<c>>p))))
    | InVal(c1, <<x>>p) -> 
	if c = c1 then None
	else Some(InVal(c1, <<x>>(Res(<<c>>p))));;

(* Helper function for the L-OPEN rule  [SW, Table 4.1] *)
let resOpenVal (c :chan) (v : value) : value option =
  match v with
      FrOutVal(c1, c2, p) -> 
	if c = c1 then None
	else if c = c2 then Some(BnOutVal(c1, <<c>>p))
	else None
    | _ -> None;;

(* Compute the list of distinct values resulting from one step 
   of transition *)
let rec next (p : proc) : value list =
  match p with
      Gd(Inact) -> []
    | Gd(Pre(Out(c1, c2, p'))) -> [FrOutVal(c1, c2, p')]
    | Gd(Pre(In(c, abs))) -> [InVal(c, abs)] 
    | Gd(Pre(Tau p1)) -> [TauVal p1]
    | Gd(Pre(Match(c1, c2, pre))) -> 
	if c1 = c2 then next(Gd(Pre pre)) else [] 
    | Gd(Plus(m,m')) -> (next(Gd m)) ++ (next(Gd m')) 
    | Par(p1,p2) -> 
	let vs1 = next p1 in
	let vs2 = next p2 in
	(List.map (parlVal p2) vs1) 
	(* apply the PAR-L rule *) ++ 
	(List.map (parrVal p1) vs2) 
	(* apply the PAR-R rule *) ++ 
	(mapMatrixPartial syncVal vs1 vs2) 
	(* apply the COMM-L/R and CLOSE-L/R rules *)
  | Res(<<x1>>p1) -> 
      let vs = next p1 in
      (mapPartial (resVal x1) vs) 
      (* apply the RES rule *) ++
      (mapPartial (resOpenVal x1) vs) 
      (* apply the OPEN rule *)
  | Rep(p1) as p2 ->
      let vs = next p1 in
      (List.map (parlVal p2) vs) 
      (* apply the REP-ACT rule *) ++
      (List.map (parlVal p2) (mapMatrixPartial syncVal vs vs))
      (* apply the REP-COMM-L/R and REP-CLOSE-L/R rules *);;	 


(*********************************************************************
 DISPLAYING PROCESSES

 Recall that we use the following grammar for pi-calculus processes:

          processes p ::= m             guarded sum              
                          p | p         composition
                          nu x(p)       restriction
                          !p            replication
       guarded sums m ::= 0             inaction
                          a             prefixed process
                          m + m         summation
 prefixed processes a ::= out c c. p    output prefix
                          in c(x). p    input prefix
                          tau. p        unobservable prefix
                          [c = c]a      match prefix

  where c,x range over names of channels.

  Given p : proc, print_next p displays p and the possible labelled
  transitions from p. Free channel names are displayed using c0,
  c1,.... and bound ones using x0, x1, x2,... with bound names reused
  within local scopes.

  *********************************************************************)

(* global state to keep track of free channel names; the free
   component stores a list associating numbers with names; the fc
   component is intended to store the length of that list *)
type state = 
    { mutable free : (chan * int)list; mutable fc : int };;

let s : state = { free = []; fc = 0 };;


(* local environment to keep track of bound channel names; the free
   component is a list associating numbers with names; the bc
   component is intended to be the length of that list *)
type env = 
    { bound : (chan * int)list; bc : int };;

   (* print a channel in the given environment and current state *)
let print_chan (e : env) (c : chan) : unit = 
  try 
    let n = List.assoc c e.bound in
    print_string "x"; print_int n
      (* print bound names as xn, with n found from the environment *) 
  with Not_found ->
    (* if there is no entry in e, assume c is free *)
    let n =
      try List.assoc c s.free with Not_found ->
	(* a newly encountered free name, so update the state *)
      let { free = cs; fc = n } = s 
      in s.free <- (c,n) :: cs; s.fc <- n+1; n
	(* print free names as cn *)
    in print_string "c"; print_int n;;

(* helper functions for printing parentheses *)
let open_paren (prec : int) (op_prec : int) : unit =
    if prec > op_prec then print_string "(";;

let close_paren (prec : int) (op_prec : int) : unit =
    if prec > op_prec then print_string ")";;

(* the main display function *)
let print_next (p : proc) : unit =
  let rec pr (e : env) (prec : int ) (p : proc) : unit =
    (* print process p in current state with environment e and
       operator precedence prec *)
    match p with
	Gd m -> pr_g e 0 m;
      | Par(p1, p2) ->
	  open_paren prec 1;
	  pr e 1 p1; print_string " | "; pr e 1 p2;
	  close_paren prec 1
      | Res(<<x>>p1) ->
	  let { bound = cs; bc = n } = e in
	  let e' = { bound = (x, n) :: cs; bc = n+1 } in
	  open_paren prec 2;
	  print_string "nu x"; print_int n; print_string " "; 
	  pr e' 2 p1;
	  close_paren prec 2
      | Rep p1 ->
	  open_paren prec 2;
	  print_string "!"; pr e 2 p1;
          close_paren prec 2
  and pr_g (e : env) (prec : int ) (m : gsum) : unit =
    match m with 
	Inact -> print_string "0"
      | Pre a -> pr_p e 2 a;
      | Plus(m1, m2) ->
	  open_paren prec 0;
	  pr_g e 0 m1; print_string " + "; pr_g e 0 m2;
	  close_paren prec 0
  and pr_p  (e : env) (prec : int ) (a : prefix) : unit =
    match a with
	Out(c1, c2, p) ->
	  open_paren prec 2;
       	  print_string "out "; print_chan e c1;
	  print_string " "; print_chan e c2;
	  print_string ". "; pr e 2 p;
	  close_paren prec 2
      | In(c, <<x>>p) ->
	  let { bound = cs; bc = n } = e in
	  let e' = { bound = (x, n) :: cs; bc = n+1 } in
	  open_paren prec 2;
       	  print_string "in "; print_chan e c;
	  print_string "(x"; print_int n; 
	  print_string "). "; pr e' 2 p;
	  close_paren prec 2
      | Tau p ->
	  open_paren prec 2;
	  print_string "tau.  "; pr e 2 p;
	  close_paren prec 2
      | Match(c1, c2, a') ->
	  open_paren prec 2;
	  print_string "["; print_chan e c1; 
	  print_string " = "; print_chan e c2; 
	  print_string "]"; pr_p e 2 a';
	  close_paren prec 2
  and pr_v  (e : env) (v : value) : unit =
    match v with
	TauVal p -> 
	  print_string "|---tau---> "; pr e 0 p; print_string "\n\n"; 
      | FrOutVal(c1, c2, p) ->
	  print_string "|---out "; print_chan e c1;
	  print_string " "; print_chan e c2;
	  print_string "---> "; pr e 0 p; print_string "\n\n"
      | BnOutVal(c, <<x>>p) ->
	  let { bound = cs; bc = n } = e in
	  let e' = { bound = (x, n) :: cs; bc = n+1 } in
	  print_string "|---out "; print_chan e c;
	  print_string "(x"; print_int n;
	  print_string ")---> "; pr e' 0 p; print_string "\n\n"
      | InVal(c, <<x>>p) ->
	  let { bound = cs; bc = n } = e in
	  let e' = { bound = (x, n) :: cs; bc = n+1 } in
	  print_string "|---in "; print_chan e c;
	  print_string "(x"; print_int n;
	  print_string ")---> "; pr e' 0 p; print_string "\n\n"
  in 
  (* intialise the state *)
  s.free <- []; 
  s.fc <- 0;
  (* initial environment *)
  let e0 = { bound = []; bc = 0} in
  (* display p *)
  pr e0 0 p; 
  print_string "\ncan do the following transitions:\n";
  (* display the list of possible lsabelled transitions from p *)
  List.iter (pr_v e0) (next p);;   

(*********************************************************************
 HOW TO USE THIS FILE

  Start the Fresh O'Caml interactive system in the directory where
  this file is located. Then do
  
  #use "pi-calculator.ml";;

  at the Fresh O'Caml prompt. Now declare some values p of type proc
  (one example is given below) and use (printNext p) to display the
  possible late labelled transitions from the process represented by
  p.

*********************************************************************)
let example : proc =
  (* 

     (nu s (out x s.(out s a.(out s b.(0)))))
     |
     in x(w).( (in w(v).(in w(u).(out v u.(0)))) 
     | 
     in z(t).(0) )
     
     This process occurs on p40 of [SW]. *)
  let a = (fresh : chan) in
  let b = (fresh : chan) in  
  let s = (fresh : chan) in
  let t = (fresh : chan) in
  let u = (fresh : chan) in
  let v = (fresh : chan) in
  let w = (fresh : chan) in
  let x = (fresh : chan) in
  let z = (fresh : chan) in
  let p1 = Res(<<s>>(Gd(Pre(Out(x, s, Gd(Pre(Out(s, a, Gd(
    Pre(Out(s, b, Gd Inact))))))))))) in
  let p2 = Gd(Pre(In(w, <<v>>(Gd(Pre(In(w, <<u>>(
    Gd(Pre(Out(v, u, Gd Inact))))))))))) in
  Par(p1, Gd(Pre(In(x, <<w>>(Par(p2, Gd(
    Pre(In(z,<<t>>(Gd Inact))))))))));;
     
(*
print_next example;;
*)

(*********************************************************************
 END of pi-calculator.ml
*********************************************************************)