module ModelChecking where

open import Level renaming (zero to Z ; suc to succ)

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product
open import Function as F hiding (const)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic
open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
open import Relation.Binary.Definitions

record AtomicNat : Set where
   field
      value : ℕ

set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
set a v next = next record { value = v }

record Phils  : Set  where
   field 
      pid : ℕ
      left right : AtomicNat

putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } )

putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } )

thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
thinking p next = next p 

pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } )

pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )

eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
eating p next = next  p 

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

record Process : Set  where
   field
      phil : Phils
      next : Code 

putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next = C_putdown_lfork } )

code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
code_table C_set  = {!!}
code_table C_putdown_rfork = putdown_rfork_stub
code_table C_putdown_lfork = {!!}
code_table C_thinking = {!!}
code_table C_pickup_rfork = {!!}
code_table C_pickup_lfork = {!!}
code_table C_eating = {!!}

step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
step = {!!}