{- Process Calculus:
   - Process, Spawn, Execute.
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module process where
import proto
import list

storage: U -> U = list

-- Type Former
process : U
        = (protocol state: U)             -- Process Signature
        * (current: prod protocol state)  -- In-Memory State
        * (act: id (prod protocol state)) -- Monoidal Action
        * (storage (prod protocol state)) -- In-Storage Signed Chain

-- Intruduction Rule
spawn (protocol state: U) (init: prod protocol state)
      (action: id (prod protocol state)) : process
    = (protocol,state,init,action,nil)

-- Accessors
protocol  (p: process): U = p.1
context   (p: process): U = p.2.1
signature (p: process): U = prod p.1 p.2.1
current   (p: process):          signature p  = p.2.2.1
action    (p: process):      id (signature p) = p.2.2.2.1
trace     (p: process): storage (signature p) = p.2.2.2.2

-- Isomorphic Signatures

-- P x S -> S      -- semigroup
-- P x S -> P x S  -- monoid

-- Eliminators
send    (p: process) (message: protocol p) : unit = undefined
receive (p: process) : protocol p = undefined
execute (p: process) (message: protocol p) : process
      = let step: signature p = (action p) (message, (current p).2)
         in (protocol p, context p, step, action p, cons step (trace p))

-- > run simple ping
data PING  = ping | pong
data STATE = init | stop | run
simple : process = spawn PING STATE (ping,init) (\(_:prod PING STATE)->(pong,run))
run (p : process) (start: protocol p) : process
  = let a : process = execute p start
        b : process = execute a (current a).1
        c : process = execute b (current b).1
     in c