data Code : Set  where
   C_putdown_rfork : Code
   C_putdown_lfork : Code
   C_thinking : Code
   C_pickup_rfork : Code
   C_pickup_lfork : Code
   C_eating : Code

record Phi : Set where
  field
    pid : ℕ
    right-hand : Bool
    left-hand : Bool
    next-code : Code
open Phi

record Env : Set where
  field
    table : List ℕ
    ph : List Phi
open Env

init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t
init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where
  init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t
  init-table-loop zero ind env exit = exit env
  init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{
    table = 0 ∷ (table env)
    ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit

code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
code_table C_putdown_rfork = putdown-rfork-c
code_table C_putdown_lfork = putdown-lfork-c
code_table C_thinking = thinking-c
code_table C_pickup_rfork = pickup-rfork-c
code_table C_pickup_lfork = pickup-lfork-c
code_table C_eating = thinking-c

pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
  pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  pickup-lfork-p zero f [] p env exit with table env
  ... | [] = exit env
  ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)}
  ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])}
  pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))}
  pickup-lfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])}
  pickup-lfork-p (suc ind) f [] p env exit = exit env
  pickup-lfork-p (suc ind) f (x ∷ ts) p env exit = pickup-lfork-p ind (f ++ (x ∷ [])) ts p env exit