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 : ℕ       -- memory pointer ( unique id of DataGear )
      value : ℕ

init-AtomicNat : AtomicNat
init-AtomicNat = record { anid = 0 ; value = 0 }

--
-- 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 Phil  : Set  where
   field 
      pid : ℕ
      left right : AtomicNat

init-Phil : Phil
init-Phil = record { pid = 0 ; left = init-AtomicNat ; right = init-AtomicNat }

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

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

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

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

--
-- Coda Gear
--

data Code : Set  where
   C_nop : Code
   C_cas_int : 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 AtomicNat-API : Set where
   field
      next : Code
      fail : Code
      value : ℕ
      impl : AtomicNat

record Phil-API : Set  where
   field 
      next : Code
      impl : Phil

data Error : Set where
   E_panic : Error
   E_cas_fail : Error

--
-- Data Gear
--
data Data : Set where
   D_AtomicNat :  AtomicNat → Data
   D_Phil :      Phil → Data
   D_Error :      Error → Data

   -- A_AtomicNat :  AtomicNat-API → Data
   -- A_Phil :      Phil-API → Data

open import hoareBinaryTree

record Context  : Set  where
   field
      next :      Code 
      fail :      Code

      --  -API list (frame in Gears Agda )
      c_Phil-API :     Phil-API
      c_AtomicNat-API : AtomicNat-API

      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 } )

--
-- second level stub
--
AtomicInt_cas_stub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.anid ai) ( D_AtomicNat (record ai { value = AtomicNat.value ai } ))
     ( λ bt → next ( Context.fail c ) c  ) -- segmentation fault ( null pointer )
     $ λ now bt → f_cas ai  (AtomicNat.value ai) now bt  where
    api : AtomicNat-API
    api = Context.c_AtomicNat-API c
    ai : AtomicNat
    ai = AtomicNat-API.impl api
    f_cas : AtomicNat → (old : ℕ ) → Data  → bt Data  → t
    f_cas a old (D_AtomicNat now) bt with <-cmp old ( AtomicNat.value now )
    ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.fail api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = a } }  ) -- update memory
    ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c
    ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
    f_cas a old _ bt    = next ( Context.fail c ) c       -- type error


Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
Phil_putdown_rfork_sub c next = next C_cas_int record c { 
    c_AtomicNat-API = record { impl = Phil.right phil ; value =  Phil.pid phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
    phil : Phil
    phil = Phil-API.impl ( Context.c_Phil-API c )

Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
Phil_putdown_lfork_sub c next = next C_cas_int record c { 
    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_thinking ; next = C_thinking } }  where
    phil : Phil
    phil = Phil-API.impl ( Context.c_Phil-API c )

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

Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
Phil_pickup_lfork_sub c next = next C_cas_int record c { 
    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_pickup_rfork ; next = C_pickup_lfork } }  where
    phil : Phil
    phil = Phil-API.impl ( Context.c_Phil-API c )

Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
Phil_pickup_rfork_sub c next = next C_cas_int record c { 
    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_pickup_lfork ; next = C_eating } }  where
    phil : Phil
    phil = Phil-API.impl ( Context.c_Phil-API c )

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

code_table :  {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
code_table C_nop  = λ c  next  → next C_nop c
code_table C_cas_int  = AtomicInt_cas_stub
code_table C_putdown_rfork = Phil_putdown_rfork_sub
code_table C_putdown_lfork = Phil_putdown_lfork_sub
code_table C_thinking = Phil_thiking
code_table C_pickup_rfork = Phil_pickup_lfork_sub
code_table C_pickup_lfork = Phil_pickup_rfork_sub
code_table C_eating = Phil_eating_sub

open Context

new :   {n : Level} {t : Set n} →  ( c : Context ) → Data → ( Context → ℕ → t ) → t
new c1 d next =  alloc-data c1 ( λ c1 n → update-data c1  n d (λ c2 → next c2 n ))

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 (Context.next p) p ( λ code np → next0 (ps ++ ( record np { next = code } ∷ [] ))) 

init-context : Context
init-context = record {
      next = C_nop
    ; fail = C_nop
    ; c_Phil-API = record { next = C_nop ; impl = init-Phil } 
    ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat } 
    ; mbase = 0
    ; memory = leaf
    ; error = D_Error E_panic
    ; fail_next = C_nop
  }

init-phil-1 : (pid : ℕ ) → (left right : AtomicNat ) → List Context
init-phil-1 pid left right = c ∷ [] where
   c : Context
   c = record init-context { c_Phil-API = record { next = C_thinking ; impl = record  init-Phil { pid = pid ; left = left ; right = right }  } } 

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