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.Tree.Binary
-- 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
      anid : ℕ
      value : ℕ

--
-- single process implemenation
--

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

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

pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t

-- pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → goto C_pickup_lfork record p { right = f } next )

pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next )
pickup_lfork p next = f_set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next )
eating p next = putdown_rfork p next
putdown_rfork p next = f_set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
putdown_lfork p next = f_set (Phils.left p) 0 ( λ f → thinking record p { left = f } next )
thinking p next = next p

run : Phils
run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p

--
-- goto version
--

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 

--
-- all possible arguments in APIs
--
record AtomicNatAPI : Set where
   field
      next : Code
      value : ℕ
      old : ℕ
      impl : AtomicNat

record PhilsAPI : Set  where
   field 
      next : Code
      impl : Phils

data Data : Set where
   D_AtomicNat :  AtomicNat → Data
   D_Phils :      Phils → Data
   A_AtomicNat :  AtomicNatAPI → Data
   A_Phils :      PhilsAPI → Data

data Error : Set where
   E_cas_fail : Error

open import hoareBinaryTree

record Context  : Set  where
   field
      next :      Code 
      fail :      Code
      phil :      PhilsAPI
      atomicNat : AtomicNatAPI
      mbase :     ℕ
      memory :    bt Data
      error :     Data
      fail_next :      Code

alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t
alloc-data {n} {t} c next = next record c { mbase = ( suc ( Context.mbase c ) ) } ( suc ( Context.mbase c ) ) 

update-data : {n : Level} {t : Set n} → ( c : Context ) → ℕ →  Data → ( Context → t ) → t
update-data  c n x next  = insertTree (Context.memory c) n x ( λ bt → next record c { memory = bt } )

f_cas : {n : Level} {t : Set n} → AtomicNat → (old now new : ℕ ) → ( Error  → t) → ( AtomicNat → t ) → t
f_cas a old now new error next with <-cmp old now 
... | tri≈ ¬a b ¬c = next record a { value = new }
... | tri< a₁ ¬b ¬c = error E_cas_fail
... | tri> ¬a ¬b _ = error E_cas_fail

--
-- second level stub
--
g_set : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
g_set {_} {t} c a next = f_set a ( AtomicNatAPI.value api   ) 
         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
    api : AtomicNatAPI
    api = Context.atomicNat c

g_cas : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
g_cas {n} {t} c a next = f_cas a ( AtomicNatAPI.old api   )( AtomicNat.value a ) ( AtomicNatAPI.value api   ) ( λ e →  next (Context.fail_next c) c )
         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
    api : AtomicNatAPI
    api = Context.atomicNat c

g_putdown_rfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_putdown_rfork c p next = next C_set record c { 
    atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value =  Phils.pid p ; old = AtomicNat.value (Phils.right p ) ; next = C_putdown_lfork } }

g_putdown_lfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_putdown_lfork c p next = next C_set record c { 
    atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value =  Phils.pid p ; old = AtomicNat.value (Phils.left p ) ; next = C_thinking } }

g_thinking : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_thinking c p next = next C_pickup_rfork c  

g_pickup_rfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_pickup_rfork c p next = next C_set record c {
    atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value = 0 ; old = AtomicNat.value (Phils.right p ) ; next = C_pickup_lfork } }

g_pickup_lfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_pickup_lfork c p next = next C_set record c {
    atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = 0 ; old = AtomicNat.value (Phils.left p ) ; next = C_eating } }

g_eating : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_eating c p next =  next C_putdown_rfork c 

set_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
set_stub c next = f_cas (AtomicNatAPI.impl api)  (AtomicNatAPI.old api) {!!} (AtomicNatAPI.value  api) {!!} ( λ ai → next {!!} ) where
     api : AtomicNatAPI
     api = Context.atomicNat c
     ai : {!!}
     ai = updateTree {!!} {!!} {!!} {!!} {!!}

putdown_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
putdown_rfork_stub p next = {!!} -- g_putdown_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

putdown_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
putdown_lfork_stub p next = {!!} -- g_putdown_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_thinking } )

thinking_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
thinking_stub p next = {!!} -- g_thinking ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_rfork } )

pickup_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
pickup_rfork_stub p next = {!!} -- g_pickup_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_lfork } )

pickup_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
pickup_lfork_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_eating } )

eating_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
eating_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_rfork } )

code_table :  {n : Level} {t : Set n} → Code → Context → ( Context → t) → t
code_table C_set  = set_stub
code_table C_putdown_rfork = putdown_rfork_stub
code_table C_putdown_lfork = putdown_lfork_stub
code_table C_thinking = thinking_stub
code_table C_pickup_rfork = pickup_rfork_stub
code_table C_pickup_lfork = pickup_lfork_stub
code_table C_eating = eating_stub

open Context

step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
step {n} {t} [] next0 = next0 []
step {n} {t} (p ∷ ps) next0 = code_table {!!} p ( λ np → next0 (ps ++ ( np ∷ [] ) )) 

test : List Context
test = step {!!} ( λ ps → ps )

test1 : List Context
test1 = step {!!}
  $ λ ps → step ps $ λ ps → ps

-- loop exexution

-- concurrnt execution

-- state db ( binary tree of processes )

-- depth first ececution

-- verify temporal logic poroerries