(*************************************************)
(*     Software for the CONCUR submission        *)
(*************************************************)
(*    Pierre-Malo Deniélou, Nobuko Yoshida       *)
(*           Imperial College London             *)
(*************************************************)

(*-------*)
(* DEBUG *)
(*-------*)

let debug_bool = false
 
let gen_debug d =
  if d then
    (fun modul msg -> begin
      print_string ("["^modul^"] ");
      print_string (msg);
      print_newline ();
      flush stdout
    end)
  else fun _ _ -> ()

let debug = gen_debug debug_bool "Buffer"

(*------------*)
(* DATA TYPES *)
(*------------*)

type prin = string
type chan = int
type var = string

type global =
  | GMsg of prin * prin * chan * global
  | GRec of var * global
  | GVar of var
  | GEnd

let rec gprint = function
  | GMsg(a,b,c,g) -> a ^ " -> " ^ b ^ " : k" ^(string_of_int c)^ " ; " ^ (gprint g)
  | GRec(x,g) -> "mu " ^ x ^ ". " ^ gprint g
  | GVar x -> x
  | GEnd -> "End"

type nodeid = int

type named =
  | NGMsg of int * prin * prin * chan * named
  | NGRec of var * named
  | NGVar of var
  | NGEnd of int

let rec ngprint = function
  | NGMsg(n,a,b,c,g) -> "n" ^(string_of_int n)^ ": " ^ a ^ " -> " ^ b ^ " : k" ^(string_of_int c)^ " ; " ^ (ngprint g)
  | NGRec(x,g) -> "mu " ^ x ^ ". " ^ ngprint g
  | NGVar x -> x
  | NGEnd n -> "n" ^(string_of_int n)^ ":End"

type node = {id:nodeid ; sender:prin ; recver:prin ; label:string ; chan:chan}
type nodes = (nodeid * node) list
type edge = nodeid * nodeid
type graph = {vl: (var * nodeid) list; nl: (nodeid * node) list; edges: edge list}


let grprint gr = 
  let rec aux = function
      [] -> ""
    | (n,n')::l -> 
        let node = List.assoc n gr.nl in
        "n" ^(string_of_int n)^ ": " ^ node.sender ^ " -> " ^ node.recver 
        ^ " : k" ^(string_of_int node.chan)^ " . n"^(string_of_int n') ^" \n" ^ (aux l)
  in
  aux gr.edges

let edprint gr edges =
  let rec aux = function
      [] -> ""
    | (n,n')::l -> 
        let node = List.assoc n gr.nl in
        "n" ^(string_of_int n)^ ": " ^ node.sender ^ " -> " ^ node.recver 
        ^ " : k" ^(string_of_int node.chan)^ " . n"^(string_of_int n') ^" \n" ^ (aux l)
  in
  aux edges

(*---------------*)
(* AUX FUNCTIONS *)
(*---------------*)

let rec subset_assoc x = function
    [] -> []
  | (a,b)::q -> if a = x then b::(subset_assoc x q) else subset_assoc x q

let remove_duplicates l = 
  let rec aux acc = function 
    | [] -> List.rev acc
    | a::q -> if List.mem a acc then aux acc q else aux (a::acc) q
  in
  aux [] l
  
let rec cut x = function
      [] -> []
    | a::q -> 
        if x=a 
        then [a] 
        else a::(cut x q)

let rec skip x = function
      [] -> []
    | a::q -> 
        if x=a 
        then a::q 
        else skip x q


(*---------------------*)
(* CONVERSION TO GRAPH *)
(*---------------------*)

let name g = 
  let next = 
    let c = ref (-1) in
    (fun () -> incr c ; !c)
  in
  let rec aux = function
    | GMsg(a,b,c,g) -> let n = next () in NGMsg (n,a,b,c,aux g)
    | GRec(x,g) -> NGRec(x,aux g) 
    | GVar x -> NGVar x 
    | GEnd -> NGEnd (next())
  in
  aux g

let rec nameof nl = function
  | NGMsg(n,a,b,c,g) -> n
  | NGRec(x,g) -> nameof nl g
  | NGVar x -> List.assoc x nl
  | NGEnd n -> n
    
let named_to_graph ng =
  let rec getnodes = function
    | NGMsg(n,a,b,c,g) -> (n,{id=n;sender=a;recver=b;label="";chan=c})::(getnodes g)
    | NGRec(x,g) -> getnodes g
    | NGVar x -> []
    | NGEnd n -> []
  in
  let rec getvar = function
    | NGMsg(n,a,b,c,g) -> (getvar g)
    | NGRec(x,g) -> (x,nameof [] g)::(getvar g) (*Warning unsafe use of nameof here*)
    | NGVar x -> []
    | NGEnd n -> []
  in
  let rec aux nl = function
    | NGMsg(n,a,b,c,g) -> (n,nameof nl g)::(aux nl g)
    | NGRec(x,g) -> (aux nl g)
    | NGVar x -> []
    | NGEnd n -> []
  in  
  let vl = getvar ng in
  let nl = getnodes ng in
  {vl=vl;nl=nl;edges=aux vl ng}


let globex1 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GVar "x"))))
let grglobex1 = named_to_graph (name globex1)


let () = print_string (gprint globex1 ^ "\n")
let () = print_string (ngprint (name globex1) ^ "\n")
let () = print_string (grprint grglobex1 ^ "\n")




(*-------------------*)
(* INFINITE CHANNELS *)
(*-------------------*)

let iorel g =
  let rec aux path nid = 
    if List.mem_assoc nid g.nl then 
      let node = List.assoc nid g.nl in
      let io = List.map (function (n,_) -> (n,nid))
      (List.filter (function (n,(recver,chan)) ->
                      (node.sender = recver && node.chan <> chan)
                   )
         path) in
      let lnode = subset_assoc nid g.edges in
      if (List.mem_assoc nid path) then
        io@(List.flatten (List.map (fun n -> auxloop path [] n) lnode))
      else
        let newpath = (nid,(node.recver,node.chan))::path in
        io@(List.flatten (List.map (fun n -> aux newpath n) lnode))
    else
      []
  and auxloop path loop nid = 
    if (not (List.mem nid loop) && List.mem_assoc nid g.nl) then 
      let node = List.assoc nid g.nl in
      let io = List.map (function (n,_) -> (n,nid))
      (List.filter (function (n,(recver,chan)) ->
                      (node.sender = recver && node.chan <> chan)
                   )
         path) in
      let newloop = (nid)::loop in
      let lnode = subset_assoc nid g.edges in
      io@(List.flatten (List.map (fun n -> auxloop path newloop n) lnode))
    else
      []
  in
  remove_duplicates (aux [] 0)

let () = print_string (edprint grglobex1 (iorel grglobex1)^ "\n")

let loops g = 
  let init = List.map snd g.vl in
  let rec purge = function
      [] -> []
    | ([])::q-> purge q
    | a::q -> a::(purge q)
  in
  let rec loop path n = 
    Printf.printf "node %i\n" n;
    if List.mem n path 
    then begin
      [cut n (path)]
    end
    else
      let ln = subset_assoc n g.edges in
      let res = List.map (fun nid -> loop (n::path) nid) ln in
      purge (List.flatten res)
  in
  List.map List.rev (loop [] 0)

let infinite g =
  let io = iorel g in
  let loops = loops g in
  let rec find loop seen n = function
      [] -> None
    | nid::q ->
        Printf.printf "find node %i\n" nid;
        if nid = n 
        then Some seen
        else
          if ((List.mem nid seen) || not (List.mem nid loop))
          then find loop seen n q
          else 
            if List.mem_assoc nid io
            then 
              (Printf.printf "Next ...\n";
              let nio = subset_assoc nid io in
              (match find loop (nid::seen) n nio with
                   None -> find loop seen n q
                 | Some l -> Some l
              ))
            else
              find loop seen n q
  in
  let rec aux loop seen = function
      [] -> []
    | n::path -> 
        Printf.printf "aux node %i\n" n;
        if List.mem n seen 
        then aux loop seen path
        else 
          if List.mem_assoc n io
          then 
            let nio = subset_assoc n io in
            (match find loop [] n nio with
                 None -> n::(aux loop seen path)
               | Some l -> (aux loop (l@seen) path))
          else 
            (n::(aux loop seen path))
  in
  List.map (function l -> aux l [] l) loops

let globex2 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",2,GVar "x")))
let grglobex2 = named_to_graph (name globex2)
let () = print_string (gprint globex2 ^ "\n")
let () = print_string (ngprint (name globex2) ^ "\n")
let () = print_string (grprint grglobex2 ^ "\n")
let () = print_string (edprint grglobex2 (iorel grglobex2)^ "\n")

(*-------------------------*)
(* BUFFER SIZE COMPUTATION *)
(*-------------------------*)

let reset g oi n seq =
  let chan = (List.assoc n g.nl).chan in
  
  Printf.printf "Trying reset channel k%d from node %d\n" chan n;
  (* _ = List.iter (fun x -> Printf.printf "Seq is %i\n" x) seq in*)
  let rec aux = function
      [] -> false
    | a::q -> 
        Printf.printf "... look node %i\n" a;
        if (List.assoc a g.nl).chan = chan 
        then 
          let _ = Printf.printf "... right channel!\n" in true
        else
          let _ = Printf.printf "... wrong channel\n" in
          from_node a q (*
          if List.mem_assoc a oi
          then 
            let noi = subset_assoc a oi in
            List.fold_right (fun x b -> 
                               let _ = Printf.printf "... ... io pred node %i\n"
                                 x in b || 
                                        (if List.mem x q 
                                         then 
                                           let _ = Printf.printf "... ... going to node %i \n" x
                                           in aux (skip x q) 
                                         else 
                                           let _ = Printf.printf "... ... stopping \n" 
                                           in false))
              noi false
          else 
            false*)
  and from_node a q =
    if List.mem_assoc a oi
    then 
      let noi = subset_assoc a oi in
      List.fold_right (fun x b -> 
                         let _ = Printf.printf "... ... io pred node %i\n"
                           x in b || 
                                  (if List.mem x q 
                                   then 
                                     let _ = Printf.printf "... ... going to node %i \n" x
                                     in aux (skip x q) 
                                   else 
                                     let _ = Printf.printf "... ... stopping \n" 
                                     in false))
        noi false
    else 
      false
  in
  from_node n seq
    (*aux seq*)


let bounds g =
  let oi = List.map (function (x,y) -> (y,x)) (iorel g) in
  let max = Hashtbl.create 9 in
  let size = Hashtbl.create 9 in
  let add_chan chan = 
    if Hashtbl.mem size chan
    then let v = Hashtbl.find size chan in
    begin 
      Hashtbl.replace size chan (v+1);
      if (v+1)>Hashtbl.find max chan 
      then Hashtbl.replace max chan (v+1)
      else()
    end
    else (
      Hashtbl.add size chan 1;
      Hashtbl.add max chan 1
    )
  in
  let reset_chan chan = 
    Hashtbl.replace size chan 1
  in
  let rec addelement chan x = function
      [] -> []
    | (c,r)::q -> (if c=chan then (c,x::r) else (c,r))
        ::(addelement chan x q)
  in
  let rec rplcelement chan x = function
      [] -> []
    | (c,r)::q -> (if c=chan then (c,[x]) else (c,x::r))
        ::(rplcelement chan x q)
  in
  let rec addallelement x = function
      [] -> []
    | (c,r)::q -> (c,x::r)::(addallelement x q)
  in
  let rec aux seens paths n = 
    Printf.printf "Bounds node %i\n" n;
    if List.mem_assoc n g.nl then
      let chan = (List.assoc n g.nl).chan in
      let path,nextpathn,nextpath = 
        if List.mem_assoc chan paths 
        then (List.assoc chan paths,
              (rplcelement chan n paths (*(chan,[n])::(List.remove_assoc chan paths) *) ),
              (addallelement n paths)) 
        else ([],((chan,[n])::(addallelement n paths)),((chan,[n])::(addallelement n paths)))
      in
      let seen,next =
        if List.mem_assoc chan seens 
        then (List.assoc chan seens,addelement chan path seens) 
        else ([],(chan,[])::seens)
      in
      if List.mem path seen
      then (Printf.printf "Path already seen\n";)
      else
        if List.mem_assoc n g.edges 
        then 
          if reset g oi n path 
          then (Printf.printf "Reset!\n";
                reset_chan (chan);
                List.iter (aux next nextpathn) (subset_assoc n g.edges)
               )
          else (Printf.printf "No reset ...\n";
                add_chan ((List.assoc n g.nl).chan);
                List.iter (aux next nextpath) (subset_assoc n g.edges)
               )
        else ()
    else ()
  in
  aux [] [] 0;
  max
    
      
      
let print_size h =
  Hashtbl.iter (fun ch s -> Printf.printf "Channel k%d = %d\n" ch s) h



let _ = print_size  (bounds grglobex1) 



let globex3 = GRec("x",GMsg ("A","B",0,GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GVar "x")))))
let grglobex3 = named_to_graph (name globex3)
let () = print_string (ngprint (name globex3) ^ "\n")
let () = print_size  (bounds grglobex3) 

let globex31 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GMsg ("A","C",1,GVar "x")))))
let grglobex31 = named_to_graph (name globex31)
let () = print_string (ngprint (name globex31) ^ "\n")
let () = print_size  (bounds grglobex31)


let globex451 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",2,GMsg ("A","B",3,GMsg ("A","C",4,GMsg ("C","B",5,GMsg ("B","C",6,GMsg ("B","C",7,GEnd))))))))
let grglobex451 = named_to_graph (name globex451)
let () = print_string (ngprint (name globex451) ^ "\n")
let () = print_size  (bounds grglobex451)



let globex452 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg ("A","B",0,GMsg ("A","C",2,GMsg ("C","B",3,GMsg ("B","C",4,GMsg ("B","C",4,GEnd))))))))
let grglobex452 = named_to_graph (name globex452)
let () = print_string (ngprint (name globex452) ^ "\n")
let () = print_size  (bounds grglobex452)



let globex453 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg ("A","B",0,GMsg ("A","C",2,GMsg ("C","B",1,GMsg ("B","C",2,GMsg ("B","C",2,GEnd))))))))
let grglobex453 = named_to_graph (name globex453)
let () = print_string (ngprint (name globex453) ^ "\n")
let () = print_size  (bounds grglobex453)




let globex454 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg ("A","B",1,GMsg ("A","C",2,GMsg ("C","B",3,GMsg ("B","C",1,GMsg ("B","C",2,GEnd))))))))
let grglobex454 = named_to_graph (name globex454)
let () = print_string (ngprint (name globex454) ^ "\n")
let () = print_size  (bounds grglobex454)




let globex511 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("A","B",0,GMsg ("B","C",2,GMsg ("C","A",1,GVar "x"))))))
let grglobex511 = named_to_graph (name globex511)
let () = print_string (ngprint (name globex511) ^ "\n")
let () = print_size  (bounds grglobex511) 



let globex512 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("B","A",2,GMsg ("A","C",3,GVar "x")))))))
let grglobex512 = named_to_graph (name globex512)
let () = print_string (ngprint (name globex512) ^ "\n")
let () = print_size  (bounds grglobex512) 

 
(*============================================================================*)
(*                                   OLD STUFF                                *)
(*============================================================================*)

(*
let globex1 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GVar "x"))))

let () = print_string (gprint globex1 ^ "\n")

let rec subst v gg = function
  | GMsg(a,b,c,g) -> GMsg(a,b,c,subst v gg g)
  | GRec(x,g) -> if x = v then GRec(x,g) else GRec(x,subst v gg g)
  | GVar x -> if x = v then gg else GVar x
  | GEnd -> GEnd

let rec unfold = function
  | GMsg(a,b,c,g) -> GMsg(a,b,c,unfold g) 
  | GRec(x,g) -> subst x (GRec(x,g)) (unfold g) 
  | GVar x -> GVar x
  | GEnd -> GEnd

let () = print_string (gprint (unfold globex1) ^ "\n")

let reset ch sender g = 
  let () = debug ("reset of k"^(string_of_int ch)^ " : " ^ (gprint g) ^ " =>") in
  let rec rest fut = function
    | GMsg(a,b,c,g) -> begin
        match (c=ch,List.mem_assoc b fut) with
          | true,true -> 
            let ll = subset_assoc b fut in
            if List.exists (fun cc -> cc<>c) ll
            then let () = debug (" true ") in true
            else  rest fut g (* let () = debug (" false ") in false *)
          | false,true ->
              let ll = subset_assoc b fut in
              if List.exists (fun cc -> cc<>c) ll
              then  rest ((a,c)::fut) g  
              else rest fut g
          | true,false -> rest fut g (* let () = debug (" false ") in false *)
          | false,false -> rest fut g
      end
    | GRec(x,g) -> rest fut g
    | GVar x -> let () = debug (" false ") in false
    | GEnd -> let () = debug (" false ") in false
  in
  rest [(sender,ch)] g

let bounds nk g =
  let upb = Array.make nk 0 in
  let pil = Array.make nk 0 in
  let pat = Array.make nk GEnd in
  let g = unfold g in
  let up i = 
    pil.(i) <- pil.(i) + 1;
    if pil.(i) > upb.(i) 
    then upb.(i) <- pil.(i) 
    else ()
  in
  let rec bound = function
    | GMsg(a,b,c,g) -> 
        let acc = pat.(c) in
        for i = 0 to (nk-1) do
          pat.(i) <- GMsg(a,b,c,pat.(i))
        done ;
        (if reset c a acc then (
           pil.(c) <- 1 ; pat.(c) <- GMsg(a,b,c,GEnd) )
         else
           up c ) ; 
        bound g
    | GRec(x,g) -> bound g
    | GVar x -> ()
    | GEnd -> ()
  in
  bound g;
  Array.to_list upb

let test n g = 
  print_string (gprint g ^ "\n");
  List.iter (function i -> 
               print_int i ;
               print_string (" ") )
  (bounds n g); print_newline()

let globex2 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GMsg ("A","B",0,GVar "x")))))

let () = test 3 globex2

let globex3 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("B","C",2,GVar "x"))))))

let () = test 3 globex3

let globex31 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("B","C",2,GVar "x"))))

let () = test 3 globex31
let () = test 3 (unfold globex31)
let () = test 3 (unfold (unfold globex31))


let globex4 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","A",2,GMsg ("A","C",1,GVar "x")))))

let () = test 3 globex4

let globex41 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",2,GMsg("A","B",3,GMsg("A","C",4,GMsg("C","B",5,GMsg("B","C",6,GMsg("B","C",7,GEnd)))))))) 
let globex42 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg("A","B",1,GMsg("A","C",2,GMsg("C","B",3,GMsg("B","C",4,GMsg("B","C",4,GEnd)))))))) 
let globex43 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg("A","B",1,GMsg("A","C",2,GMsg("C","B",1,GMsg("B","C",2,GMsg("B","C",2,GEnd)))))))) 
let globex44 = GMsg ("A","B",0,GMsg ("B","A",1,GMsg ("A","B",0,GMsg("A","B",1,GMsg("A","C",2,GMsg("C","B",3,GMsg("B","C",1,GMsg("B","C",2,GEnd))))))))

let () = test 8 globex41
let () = test 8 globex42
let () = test 8 globex43
let () = test 8 globex44


let globex51 = GRec("x",GMsg ("A","B",1,GMsg ("C","A",2,GMsg ("A","B",1,GMsg ("B","C",3,GMsg ("C","A",2,GVar "x"))))))
let globex52 = GRec("x",GMsg ("A","B",1,GMsg ("C","A",2,GMsg ("A","B",1,GMsg ("C","A",2,GMsg ("B","A",3,GMsg ("A","C",4,GVar "x")))))))
let globex53 = GRec("x",GMsg ("A","B",1,GMsg ("C","A",2,GMsg ("A","B",1,GMsg ("C","A",2,GMsg ("B","C",3,GVar "x"))))))

let () = test 5 globex51
let () = test 5 globex52
let () = test 5 globex53
let () = test 5 (unfold globex51)
let () = test 5 (unfold globex52)
let () = test 5 (unfold globex53)

(*
let globex61 = GRec("x",GMsg ("A","B",0,GMsg ("C","A",1,GMsg ("D","C",2,GMsg ("B","D",3,GVar "x")))))

let () = test 5 globex61
let () = test 5 (unfold globex61)
let () = test 5 (unfold (unfold globex61))

let globex7 = GRec("x",GMsg ("A","B",0,GMsg ("B","C",1,GMsg ("C","B",2,GMsg ("B","D",0,GMsg ("D","A",3,GVar "x"))))))

let () = test 5 globex7
let () = test 5 (unfold globex7)
let () = test 5 (unfold (unfold globex7))
*)



  *)