open import GeneralLemmas using (_≡_; Dec)
module DCESH.Presimulation-CESH(Node : Set)(_≟_ : (n n' : Node) → Dec (n ≡ n')) where
open import Heap
open import CESH Node
open import DCESH Node _≟_
open import DCESH.Properties Node _≟_
open import DCESH.Simulation-CESH Node _≟_
open import GeneralLemmas
open import MachineCode Node
open import Relation
open import Tagged
lookup-var' : ∀ {h hs v} e de x → (∀ n → R-env n h hs e de) → lookup x de ≡ just v → ∃ λ v' → lookup x e ≡ just v'
lookup-var' e [] zero Rede ()
lookup-var' e [] (suc x) Rede ()
lookup-var' [] (x ∷ de) zero Rede look = ⊥-elim (Rede 0)
lookup-var' (x ∷ e) (dx ∷ de) zero Rede look = x , refl
lookup-var' [] (x ∷ de) (suc x₁) Rede look = ⊥-elim (Rede 0)
lookup-var' (x ∷ e) (x₁ ∷ de) (suc x₂) Rede look = lookup-var' e de x₂ (proj₂ ∘ Rede) look
presimulation-sync-<silent> : ∀ thread {n heaps hs hs' dcfg'} cfg
→ n ⊢ (just thread , hs) ⟶Machine< silent > (dcfg' , hs')
→ R-machine heaps cfg (just thread) → ∃ λ cfg' → cfg ⟶CESH cfg'
presimulation-sync-<silent> (VAR var SEQ dc , de , ds , r)
(.(VAR var SEQ dc) , e , s , h)
(VAR x)
(refl , Rede , Rsds)
= let (v' , y) = lookup-var' e de var Rede x
in (dc , e , val v' ∷ s , h) , VAR y
presimulation-sync-<silent> (CLOSURE dc' SEQ dc , de , ds , r)
(.(CLOSURE dc' SEQ dc) , e , s , h)
CLOSURE (refl , Rede , Rsds)
= let (h' , closptr) = h ▸ (dc' , e)
in (dc , e , val (clos closptr) ∷ s , h') , CLOSURE
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(c , e , [] , h)
(APPLY p)
(Rcdc , Rede , ())
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(c , e , cont x ∷ s , h)
(APPLY p)
(Rcdc , Rede , () , Rsds)
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(c , e , val v' ∷ [] , h)
(APPLY p)
(Rcdc , Rede , Rvdv , ())
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(c , e , val v' ∷ cont _ ∷ s , h)
(APPLY p)
(Rcdc , Rede , Rvdv , () , Rsds)
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(c , e , val v' ∷ val (nat n) ∷ s , h)
(APPLY p)
(Rcdc , Rede , Rvdv , Rv'dv' , Rsds) = ⊥-elim (Rv'dv' 0)
presimulation-sync-<silent> (APPLY SEQ dc , de , val dv ∷ val (clos (dc' , de')) ∷ ds , r)
(.(APPLY SEQ dc) , e , val v' ∷ val (clos closptr) ∷ s , h)
(APPLY p)
(refl , Rede , Rvdv , Rcldcl , Rsds) with Rcldcl 1
... | ((c' , e') , _ , lu , _) = (c' , v' ∷ e' , cont (dc , e) ∷ s , h) , APPLY lu
presimulation-sync-<silent> (.RETURN , de , (val dv ∷ cont (dc , de') ∷ ds , r))
(.RETURN , e , [] , h)
RETURN
(refl , Rede , ())
presimulation-sync-<silent> (.RETURN , de , (val dv ∷ cont (dc , de') ∷ ds , r))
(.RETURN , e , cont _ ∷ s , h)
RETURN
(refl , Rede , () , Rsds)
presimulation-sync-<silent> (.RETURN , de , (val dv ∷ cont (dc , de') ∷ ds , r))
(.RETURN , e , val v ∷ [] , h)
RETURN
(refl , Rede , Rvdv , ())
presimulation-sync-<silent> (.RETURN , de , (val dv ∷ cont (dc , de') ∷ ds , r))
(.RETURN , e , val v ∷ val _ ∷ s , h)
RETURN
(refl , Rede , Rvdv , () , Rsds)
presimulation-sync-<silent> (.RETURN , de , (val dv ∷ cont (dc , de') ∷ ds , r))
(.RETURN , e , val v ∷ cont (c , e') ∷ s , h)
RETURN
(refl , Rede , Rvdv , Rcont , Rsds)
= (c , e' , val v ∷ s , h) , RETURN
presimulation-sync-<silent> (LIT n SEQ dc , de , (ds , r))
(.(LIT n SEQ dc) , e , s , h)
LIT
(refl , Rede , Rsds)
= (dc , e , val (nat n) ∷ s , h) , LIT
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , [] , h)
PRIMOP
(refl , Rede , ())
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , cont _ ∷ s , h)
PRIMOP
(refl , Rede , () , Rsds)
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , val (clos c) ∷ s , h)
PRIMOP
(refl , Rede , Rvdv , Rsds) = ⊥-elim (Rvdv 0)
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , val (nat l₁') ∷ [] , h)
PRIMOP
(refl , Rede , Rvdv , ())
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , val (nat l₁') ∷ cont _ ∷ s , h)
PRIMOP
(refl , Rede , Rvdv , () , Rsds)
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , val (nat l₁') ∷ val (clos _) ∷ s , h)
PRIMOP
(refl , Rede , Rvdv , Rvdv' , Rsds) = ⊥-elim (Rvdv' 0)
presimulation-sync-<silent> (PRIMOP f SEQ dc , de , (val (nat l₁) ∷ val (nat l₂) ∷ ds , r))
(.(PRIMOP f SEQ dc) , e , val (nat l₁') ∷ val (nat l₂') ∷ s , h)
PRIMOP
(refl , Rede , Rvdv , Rvdv' , Rsds)
= (dc , e , val (nat (f l₁' l₂')) ∷ s , h) , PRIMOP
presimulation-sync-<silent> (COND c c' , de , (val (nat .0) ∷ ds , r))
(.(COND c c') , e , [] , h)
COND-0
(refl , Rede , ())
presimulation-sync-<silent> (COND c c' , de , (val (nat .0) ∷ ds , r))
(.(COND c c') , e , cont _ ∷ s , h)
COND-0
(refl , Rede , () , Rsds)
presimulation-sync-<silent> (COND c c' , de , (val (nat .0) ∷ ds , r))
(.(COND c c') , e , val (clos _) ∷ s , h)
COND-0
(refl , Rede , Rvdv , Rsds) = ⊥-elim (Rvdv 0)
presimulation-sync-<silent> (COND c c' , de , (val (nat .0) ∷ ds , r))
(.(COND c c') , e , val (nat n) ∷ s , h)
COND-0
(refl , Rede , Rvdv , Rsds) with Rvdv 0
presimulation-sync-<silent> (COND c c' , de , val (nat ._) ∷ ds , r)
(.(COND c c') , e , val (nat .0) ∷ s , h)
COND-0
(refl , Rede , Rvdv , Rsds) | refl = (c , e , s , h) , COND-0
presimulation-sync-<silent> (COND c c' , de , (val (nat (suc l)) ∷ ds , r))
(.(COND c c') , e , [] , h)
COND-suc
(refl , Rede , ())
presimulation-sync-<silent> (COND c c' , de , (val (nat (suc l)) ∷ ds , r))
(.(COND c c') , e , cont _ ∷ s , h)
COND-suc
(refl , Rede , () , Rsds)
presimulation-sync-<silent> (COND c c' , de , (val (nat (suc l)) ∷ ds , r))
(.(COND c c') , e , val (clos _) ∷ s , h)
COND-suc
(refl , Rede , Rvdv , Rsds) = ⊥-elim (Rvdv 0)
presimulation-sync-<silent> (COND c c' , de , (val (nat (suc l)) ∷ ds , r))
(.(COND c c') , e , val (nat l') ∷ s , h)
COND-suc
(refl , Rede , Rvdv , Rsds) with Rvdv 0
presimulation-sync-<silent> (COND c c' , de , val (nat (suc l)) ∷ ds , r)
(.(COND c c') , e , val (nat .(suc l)) ∷ s , h)
COND-suc
(refl , Rede , Rvdv , Rsds) | refl
= (c' , e , s , h) , COND-suc
presimulation-sync-<send> : ∀ thread {n heaps hs hs' dcfg' msg} cfg
→ n ⊢ (just thread , hs) ⟶Machine< send msg > (dcfg' , hs')
→ R-machine heaps cfg (just thread) → ∃ λ cfg' → cfg ⟶CESH cfg'
presimulation-sync-<send> (REMOTE c' i' SEQ c , de , ds)
(.(REMOTE c' i' SEQ c) , e , s , h)
REMOTE-send
(refl , Rede , Rsds)
= (c' , [] , cont (c , e) ∷ s , h) , REMOTE
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , [] , h)
(APPLY-send p)
(refl , Rede , ())
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , el ∷ [] , h)
(APPLY-send p)
(refl , Rede , Rvdv , ())
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , cont _ ∷ s , h)
(APPLY-send p)
(refl , Rede , () , Rsds)
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , val v ∷ cont _ ∷ s , h)
(APPLY-send p)
(refl , Rede , Rvdv , () , Rsds)
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , val v ∷ val (nat _) ∷ s , h)
(APPLY-send p)
(refl , Rede , Rvdv , Rv'dv' , Rsds) = ⊥-elim (Rv'dv' 0)
presimulation-sync-<send> (APPLY SEQ c , de , (val dv ∷ val (clos (ptr , loc)) ∷ ds , r))
(.(APPLY SEQ c) , e , val v ∷ val (clos closptr) ∷ s , h)
(APPLY-send p)
(refl , Rede , Rvdv , Rv'cl , Rsds) with Rv'cl 1
... | ((c' , e') , _ , lu , _) = (c' , v ∷ e' , cont (c , e) ∷ s , h) , APPLY lu
presimulation-sync-<send> (.RETURN , de , (val dv ∷ [] , just cptr))
(.RETURN , e , [] , h)
RETURN-send
(refl , Rede , ())
presimulation-sync-<send> (.RETURN , de , (val dv ∷ [] , just cptr))
(.RETURN , e , cont _ ∷ s , h)
RETURN-send
(refl , Rede , () , Rsds)
presimulation-sync-<send> (.RETURN , de , (val dv ∷ [] , just cptr))
(.RETURN , e , val v ∷ [] , h)
RETURN-send
(refl , Rede , Rvdv , ())
presimulation-sync-<send> (.RETURN , de , (val dv ∷ [] , just cptr))
(.RETURN , e , val v ∷ val _ ∷ s , h)
RETURN-send
(refl , Rede , Rvdv , _ , _ , _ , () , _)
presimulation-sync-<send> (.RETURN , de , (val dv ∷ [] , just cptr))
(.RETURN , e , val v ∷ cont (c , e') ∷ s , h)
RETURN-send
(refl , Rede , Rvdv , Rsds)
= (c , e' , val v ∷ s , h) , RETURN
presimulation-sync : Presimulation _⟶Sync_ _⟶CESH_ (R-sync ⁻¹)
presimulation-sync nodes ._ (c , e , s) (silent-step {n} x) (n' , ia , Rmachine)
with all-except-find-⟶<silent> nodes n' n ia x | nodes n' | inspect nodes n'
presimulation-sync nodes ._ (c , e , s , h) (silent-step x) (n , ia , ()) | refl | nothing , hs | [ eq ]
presimulation-sync nodes ._ (c , e , s , h) (silent-step x) (n , ia , Rmachine) | refl | just (dc , de , ds) , hs | [ eq ]
= presimulation-sync-<silent> (dc , de , ds) (c , e , s , h) (subst (λ p → n ⊢ p ⟶Machine< silent > _) eq x) Rmachine
presimulation-sync nodes ._ (c , e , s , h) (comm-step {sender} {receiver} {sender' = sender'} {receiver'} x y) (n , ia , Rmachine)
with all-except-find-⟶<send> nodes n sender ia x | nodes n | inspect nodes n
presimulation-sync nodes ._ (c , e , s , h) (comm-step x y) (n , ia , ()) | refl | nothing , hs | [ eq ]
presimulation-sync nodes ._ (c , e , s , h) (comm-step {sender} x y) (.sender , ia , Rmachine) | refl | just (dc , de , ds) , hs | [ eq ]
= presimulation-sync-<send> (dc , de , ds) (c , e , s , h) (subst (λ p → sender ⊢ p ⟶Machine< send _ > _) eq x) Rmachine