module Path where

open import Basics hiding (_==_)
open import Proc
import Graph

private open module G = Graph Nat

data Node : Set where
  node : Nat -> Node
  stop : Node

_==_ : Node -> Node -> Bool
stop         == stop         = true
node zero    == node zero    = true
node (suc n) == node (suc m) = node n == node m
_            == _            = false

data U : Set where
  int : U
  ext : U

data Name : Set where
  fwd-edge : Nat -> Nat  -> Name
  bwd-edge : Nat -> Node -> Name
  start    : Nat -> Name
  finish   : Nat -> Name

N : U -> Set
N int = Name
N ext = False

data Msg : Set where
  forward  : Node -> Node -> Msg
  backward : Node -> Msg

T : U -> Set
T int = Msg
T ext = Node

private
 module Impl where
  private module P = ProcDef U T N
  open P hiding (_!_)

  P = Proc int

  infixr 40 _!_
  _!_ : Msg -> P -> P
  m ! p = P._!_ (lift m) p

  fwd : Nat -> Nat -> Msg
  fwd from to = forward (node from) (node to)

  fwd-runner : Nat -> Nat -> P
  fwd-runner from to = > react
    where
      react : Msg -> P
      react (forward from' to') =
        if   to' == node from
        then fwd from to ! def (bwd-edge from from')
        else def (fwd-edge from to)
      react (backward _) = o

  bwd-runner : Nat -> Node -> P
  bwd-runner from w = > react
    where
      react : Msg -> P
      react (backward n) =
        if   n == w then o
        else if n == node from
        then backward w ! o
        else def (bwd-edge from w)
      react (forward _ _) = def (bwd-edge from w)

  pitcher : Nat -> P
  pitcher n = forward stop (node n) ! o 

  batter : Nat -> P
  batter n = > react
    where
      react : Msg -> P
      react (forward from to) =
        if   to == node n
        then backward from ! o
        else def (start n)
      react _ = def (start n)

  env : Env
  env int (fwd-edge from to) = fwd-runner from to
  env int (bwd-edge from w)  = bwd-runner from w
  env int (start n)          = batter n
  env int (finish n)         = pitcher n
  env ext ()

  edges : Graph -> P
  edges [] = o
  edges (edge x y :: G) = def (fwd-edge x y) || edges G

  φ : Tran ext int
  φ = record { upV = up; downV = down }
    where
      down : Node -> Lift Msg
      down x = lift (backward x)

      up : Msg -> Lift Node
      up (forward _ _) = bot
      up (backward x)  = lift x

  main : Graph -> Nat -> Nat -> Proc ext
  main G x y = φ /| def (finish y) || def (start x) || edges G

open Impl public

param : Param
param = record
        { U    = U
        ; T    = T
        ; Name = N
        ; env  = env
        }