-- Richard Fontana

-- Note:  implementation of type-checking was not completed -- 
-- types of channels can be specified in initial restrictions, for example, 
-- but nothing is done with them (I can probably complete this quickly
-- and can submit an updated version)


module Pi where

data Process = Null      -- Process with no observable behavior
             | Event (IO ())  -- Process causing an observable Haskell IO event
             | Channel :! Value -- Sender process (send signal along channel);
             | Channel :? (Pattern, Process) -- Receiver process 
             | Process :|: Process -- Process execution in parallel
             deriving Show
              
type Channel = String
type Variable = String

data Value =   Chan Channel
             | Tup [Value]
             | String String  -- special value for output, not used here
             deriving (Eq, Show)

data Pattern = Var Variable
             | Pat [Pattern]
             deriving (Eq, Show)

-- Determines if a value and a pattern are functionally equivalent 
-- (symmetric)
pveq :: Value -> Pattern -> Bool
pveq v p =
 case p of 
   Var s -> 
    case v of
      Chan s -> True      
      _      -> False   
   Pat (p':ps) ->
    case v of
      Tup (v':vs) ->
        (v' `pveq` p') && (Tup vs `pveq` Pat ps)
      _           -> False
   Pat [] -> 
    case v of 
      Tup [] -> True
      _      -> False       

-- Produces a pattern functionally equivalent (symmetric) to a value
v2p :: Value -> Pattern
v2p v =
  case v of
    Chan ch -> Var ch
    Tup []  -> Pat []
    Tup (t:ts) -> Pat (p:ps)
      where p = v2p t
            Pat ps = v2p (Tup ts)

data Type = Uncertain
            | Comp [Type]
            | Carries Type
            deriving Show

signal = Comp []

-- Assume for now that programmer is responsible for using a fresh 
-- variable name
-- This is designed to build up a list of new variables with type
-- bindings at the outset of execution of a process
new :: Channel -> Type -> [(Channel, Type)] -> [(Channel, Type)]
new ch t tpl = ((ch, t):tpl)

-- This maps values in a sender process to their corresponding
-- patterns in a receiver process (if it doesn't work, the program
-- fails
bind :: Value -> Pattern -> [(Pattern, Value)]
bind v (Var x) = [(Var x, v)]
bind (Tup []) (Pat []) = []
bind (Tup vs) (Pat ps) =
  if (length vs) == (length ps)
  then (bind (head vs) (head ps)) ++ (bind (Tup (tail vs)) (Pat (tail ps)))
  else error "binding failure" 
bind _ _ = error "binding failure"
  

-- This will be used when the type checking is integrated in the 
-- module 
getType :: Value -> [(Channel, Type)] -> (Type, [(Channel, Type)])
getType (Chan ch) cts =
  let r = lookup ch cts
  in
    case r of 
      (Just rt) -> (rt, cts)
      _         -> (Carries Uncertain, ((ch, Carries Uncertain):cts))
getType (Tup []) cts  = (signal, cts)
getType (Tup (v:vs)) cts =
  let (t, ucts) = getType v cts 
  in 
    let (Comp u, vcts) = getType (Tup vs) ucts
    in
      (Comp (t:u), vcts)
   

-- Used to execute a process (and a list of new channel/type bindings, 
-- if present (but currently this is not yet used functionally)
superrun :: [(Channel, Type)] -> Process ->  IO ()
superrun tpl p = fst (runlist (flatten p) tpl)
    
-- Lower-level process processing functions

run :: Process -> (IO (), [Process])
run Null = (return (), [])
run (Event e) = (e, [])
run (ch:?bp) = (return (), [ch:?bp]) 
run (ch:!v) = (return (), [ch:!v])
run _ = error "uninterpretable process expression"

runlist :: [Process] -> [(Channel, Type)] -> (IO (), [Process])
runlist [] tpl = (return (), [])
runlist ps tpl  =
  let (ml, nml) = match ps [] ([],[]) tpl 
  in
    case ml of
      [] -> runpevs nml
      _  -> 
           let (es, gpl) = runpevs nml
           in 
              let (es', gpl') = runml ml gpl tpl
              in
                let (res, ugpl) = runlist gpl' tpl
                in
                  (do {es; es'; res}, ugpl)


-- Make list of 'atomic' processes to scan, so that matches can be culled 
flatten :: Process -> [Process]
flatten (p :|: q) = pl ++ ql
  where pl = flatten p
        ql = flatten q
flatten p = [p]


runpair :: (Process, Process) -> [Process] -> [(Channel, Type)] 
 -> (IO (), [Process])
runpair (ml, mr) gpl tpl =
  let (ch :! snd, ch' :? rcv) = order ml mr
  in
    let (es, ps) = run (inst rcv snd)
    in
      (do {es}, ps ++ gpl)

-- Auxiliary function used in the inst function, used for
-- instantiating values within a receiver process expression
-- when it is matched with a sender expression
instval :: Value -> [(Pattern, Value)] -> Value
instval v pvs =
  case v of
    Chan ch ->
      let r = lookup (v2p (Chan ch)) pvs 
      in
         case r of
           Just rt -> rt
           _       -> v
    Tup (t:ts)  -> 
      let (Tup rts) = instval (Tup ts) pvs
      in     
        let r = lookup (v2p t) pvs
        in 
          case r of
            Just rt -> Tup (rt:rts)
            _       -> Tup (t:rts)

-- Instantiates bound names in a receiver process with the sent names 
-- from the sender process
inst :: (Pattern, Process) -> Value -> Process
inst (pat, proc) val =
  case proc of
    (p1 :|: p2) ->
       ((inst (pat, p1) val) :|: (inst (pat, p2) val))
    (ch :! v) ->
       case pat of 
          Var x ->
            case val of
               Chan c ->
                 case v of 
                   Chan d ->
                     if ch == x
                     then 
                       if d == x
                       then (c :! val)
                       else (c :! v)
                     else
                       if d == x
                       then (ch :! val)
                       else (ch :! v)
                   Tup [] ->
                     if ch == x
                     then (c :! v)
                     else (ch :! v)
                   Tup (vv:vvs) ->
                     let nvs = instval v (bind val pat)
                     in  
                       if ch == x
                       then (c :! nvs)
                       else (ch :! nvs)
               Tup t ->
                 case v of 
                   Chan d ->
                     if d == x
                     then (ch :! val)
                     else (ch :! v)
                   Tup (vv:vvs) ->
                      let nvs = instval v (bind val pat)
                      in (ch :! nvs)         
          Pat (p:ps) ->
            let bindv = bind val pat
            in
             let nvs = instval v bindv
             in 
               let (Chan dv) = instval (Chan ch) bindv
               in (dv :! nvs)
    (ch :? (pat', proc')) ->
     case pat of 
       Var x ->
        let proc'' = inst (pat, proc') val
        in 
          case val of 
           Chan c ->
             if ch == x 
             then (c :? (pat', proc''))
             else (ch :? (pat', proc''))  
           Tup t -> (ch :? (pat', proc''))
       Pat (p:ps) ->     
         let proc'' = inst (pat', proc'') val
         in
          let bindv = bind val pat
          in
            let (Chan dv) = instval (Chan ch) bindv
            in (dv :? (pat', proc'')) 
    _ -> proc             


-- Additional lower-level process-running functions

runml :: [(Process, Process)] -> [Process] -> [(Channel, Type)] 
  -> (IO (), [Process])
runml [] gpl tpl = (return (), gpl)
runml (pr:prs) gpl tpl =
  let (e, ugpl) = runpair pr gpl tpl 
  in 
     let (es, vgpl) = runml prs ugpl tpl
     in 
       (do {e; es}, vgpl)


runev :: Process -> (IO (), [Process])
runev p =
  case p of 
    Event e -> (e, [])
    _       -> (return (), [p])


-- Run pending events
runpevs :: [Process] -> (IO (), [Process])
runpevs [] = (return (), [])
runpevs (p:ps) = 
  let (e, r) = runev p
  in 
    let (es, rs) = runpevs ps 
      in 
        (do {e; es}, r++rs)


-- Put a matched pair of processes in a 'normal' order
order :: Process -> Process -> (Process, Process)
order ml mr =
  case ml of
    (ch :? v) -> (mr, ml)
    _         -> (ml, mr)


-- Matches sender and receiver processes in the list of flattened
-- process expressions.  This should also do type-checking when 
-- that is integrated
match :: [Process] -> [Process] -> ([(Process, Process)], [Process]) 
 -> [(Channel, Type)] ->  ([(Process, Process)], [Process])
match [] [] t tpl = t
match [] civ t tpl = match civ [] t tpl
match (a:as) civ t tpl =
  case a of
    Null -> match (as++civ) [] t tpl
    Event e -> match (as++civ) [] (ml, (a:nml)) tpl
       where (ml, nml) = t
    p -> 
       case as of 
         [] -> 
           let (ml, nml) = t
           in
             match civ [] (ml, (a:nml)) tpl       
         _ ->
           let (q:ttas) = as          
           in
             if p `matches` q 
             then let (ml, nml) = t
                  in match (ttas++civ) [] (((p, q):ml), nml) tpl
             else match (p:ttas) (q:civ) t tpl


-- Determines whether a sender and receiver "match"
matches :: Process -> Process -> Bool
p `matches` q =
  case p of 
    (ch :! v) -> 
      case q of 
         (ch' :? bp) -> (ch == ch')
         _ -> False
    (ch :? bp) ->
      case q of
         (ch' :! v) -> (ch == ch')
         _ -> False


-- Some simple examples discussed in the paper

test1 = superrun []
          (Event (putStr "peering\n") :|: Event (putStr "absorbing\n") :|: 
            Event (putStr "translating\n"))


test2 = superrun []
          (("x" :? (Pat [], Event (putStr "Got it!\n"))) :|: ("x" :! (Tup [])))


test3 = superrun []
          (("x":! (Chan "y")) :|: 
           ("x" :? (Var "z", ("z" :! (Chan "u")))) :|:
           ("y" :? (Var "w", Event (putStr "Got it!\n"))))

test4 = superrun []
          (("x" :! (Chan "y")) :|:
           ("x" :? (Var "z", ("a" :! (Chan "z")))) :|:
           ("a" :? (Var "w", Event (putStr "Got it!\n"))))


test5 = superrun 
         ( (new "b" (Carries (Comp [(Carries signal),(Carries signal)])) []) ++
          (new "t" (Carries signal) []) ++ (new "f" (Carries signal) []) )

                (
                  -- Encodes the Boolean value "False"
                 ("b":?(Pat[(Var"t"),(Var"f")],("f":!(Tup[]))))  :|:
                (
                  -- The testing process
                     ("b":!(Tup[(Chan"t"),(Chan"f")]))   :|:
                     ("t":?(Pat[],(Event (putStr"It's true\n")))) :|:
                     ("f":?(Pat[],(Event (putStr"It's false\n")))) ) ) 
                    
           -- Output should be:  "It's false"


test6 = superrun 
         ( (new "b" (Carries (Comp [(Carries signal),(Carries signal)])) []) ++
          (new "t" (Carries signal) []) ++ (new "f" (Carries signal) []) )

                (
                  -- Encodes the Boolean value "True"
                 ("b":?(Pat[(Var"t"),(Var"f")],("t":!(Tup[]))))  :|:
                (
                  -- The testing process
                     ("b":!(Tup[(Chan"t"),(Chan"f")]))   :|:
                     ("t":?(Pat[],(Event (putStr"It's true\n")))) :|:
                     ("f":?(Pat[],(Event (putStr"It's false\n")))) ) ) 
                    
           -- Output should be:  "It's true"