open import GeneralLemmas using (Dec; _≡_)
module DKrivine.Simulation
(Node : Set)
(_≟_ : (n n' : Node) → Dec (n ≡ n'))
where
open import DKrivine Node _≟_ as DKrivine
open import DKrivine.Properties Node _≟_
open import GeneralLemmas
open import Heap
open import Krivine Node as Krivine
open import Krivine.Properties Node as KrivineProps
open import Lambda Node
open import Tagged
open import Relation
infix 7 _⊆s_
R-term : Rel Term Term
R-term t₁ t₂ = t₁ ≡ t₂
Heaps = Node → ContHeap
R-closure : Heaps → Rel Krivine.Closure DKrivine.Closure
stack-ext-pred : Heaps → ContPtr → (DKrivine.Stack → Set) → Set
stack-ext-pred hs (ptr , loc) P = ∃ λ s → hs loc ! ptr ≡ just s × P s
R-envelem : ℕ → Heaps → Rel Krivine.EnvElem DKrivine.EnvElem
R-envelem 0 hs (clos c₁) (local c₂) = R-closure hs c₁ c₂
R-envelem (suc rank) hs (clos c₁) (local c₂) = ⊥
R-envelem 0 hs (clos c₁) (remote contptr index) = ⊥
R-envelem (suc rank) hs (clos c₁) (remote contptr index) =
stack-ext-pred hs contptr
(λ s₂ → ∃ λ ee₂ → stack-index s₂ index ≡ just ee₂
× R-envelem rank hs (clos c₁) ee₂)
R-env : Heaps → Rel Krivine.Env DKrivine.Env
R-env hs [] [] = ⊤
R-env hs [] (x₂ ∷ e₂) = ⊥
R-env hs (x₁ ∷ e₁) [] = ⊥
R-env hs (x₁ ∷ e₁) (x₂ ∷ e₂) = (∃ λ rank → R-envelem rank hs x₁ x₂) × R-env hs e₁ e₂
R-closure hs (t₁ , e₁) (t₂ , e₂) = R-term t₁ t₂ × R-env hs e₁ e₂
R-stackelem : Heaps → Rel Krivine.StackElem DKrivine.StackElem
R-stackelem hs (arg c₁) (arg c₂) = R-closure hs c₁ c₂
R-stackelem hs (if0 c₁ c₁') (if0 c₂ c₂') = R-closure hs c₁ c₂ × R-closure hs c₁' c₂'
R-stackelem hs (op₂ f c₁) (op₂ g c₂) = f ≡ g × R-closure hs c₁ c₂
R-stackelem hs (op₁ f) (op₁ g) = f ≡ g
R-stackelem hs _ _ = ⊥
R-stack : ℕ → Heaps → Rel Krivine.Stack DKrivine.Stack
R-stack rank hs (x₁ ∷ s₁) ([] , nothing) = ⊥
R-stack rank hs [] (x₂ ∷ s₂ , r) = ⊥
R-stack rank hs (x₁ ∷ s₁) (x₂ ∷ s₂ , r) = R-stackelem hs x₁ x₂ × R-stack rank hs s₁ (s₂ , r)
R-stack 0 hs [] ([] , nothing) = ⊤
R-stack (suc rank) hs [] ([] , nothing) = ⊥
R-stack 0 hs s₁ ([] , just (contptr , args , drop)) = ⊥
R-stack (suc rank) hs s₁ ([] , just (contptr , args , drop)) =
stack-ext-pred hs contptr (λ s₂ →
∃ λ ds₂ → drop-stack s₂ drop ≡ just ds₂ × num-args ds₂ ≡ args × R-stack rank hs s₁ ds₂)
R-stack-must-have-arg : ∀ hs c s ptr drop → ¬ (∃ λ rank → R-stack rank hs (arg c ∷ s) ([] , just (ptr , 0 , drop)))
R-stack-must-have-arg hs c s (ptr , loc) drop (zero , ())
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , ([] , just (contptr , .0 , drop')) , dropds , refl , Rsds') = R-stack-must-have-arg hs c s contptr drop' (rank , Rsds')
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , ([] , nothing) , dropds , nargs , Rsds) = Rsds
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (arg _ ∷ ds , x₁) , dropds , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (if0 _ _ ∷ ds , x₂) , dropds , nargs , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (op₂ _ _ ∷ ds , x₂) , dropds , nargs , () , Rsds)
R-stack-must-have-arg hs c s (ptr , loc) drop (suc rank , s' , lu , (op₁ _ ∷ ds , x₁) , dropds , nargs , () , Rsds)
drop-stack-shift : ∀ s drop c ds r → drop-stack s drop ≡ just (arg c ∷ ds , r) → drop-stack s (suc drop) ≡ just (ds , r)
drop-stack-shift (.(arg c ∷ ds) , r') zero c ds .r' refl = refl
drop-stack-shift ([] , just (ptr , zero , drop')) (suc drop) c ds r ()
drop-stack-shift ([] , just (ptr , suc args , drop')) (suc drop) c ds r ass = drop-stack-shift ([] , just (ptr , args , suc drop')) drop c ds r ass
drop-stack-shift ([] , nothing) (suc drop) c ds r ()
drop-stack-shift (arg x ∷ s , r') (suc drop) c ds r ass = drop-stack-shift (s , r') drop c ds r ass
drop-stack-shift (if0 x x₁ ∷ s , r') (suc drop) c ds r ()
drop-stack-shift (op₂ x x₁ ∷ s , r') (suc drop) c ds r ()
drop-stack-shift (op₁ x ∷ s , r') (suc drop) c ds r ()
drop-stack-shift' : ∀ s drop ptr args drop' → drop-stack s drop ≡ just ([] , just (ptr , suc args , drop')) →
drop-stack s (suc drop) ≡ just ([] , just (ptr , args , suc drop'))
drop-stack-shift' (.[] , .(just (ptr , suc args , drop))) zero ptr args drop refl = refl
drop-stack-shift' ([] , just (ptr' , zero , drop'')) (suc drop) ptr args drop' ()
drop-stack-shift' ([] , just (ptr' , suc args' , drop'')) (suc drop) ptr args drop' ass = drop-stack-shift' ([] , just (ptr' , args' , suc drop'')) drop ptr args drop' ass
drop-stack-shift' ([] , nothing) (suc drop) ptr args drop' ()
drop-stack-shift' (arg x ∷ s , r) (suc drop) ptr args drop' ass = drop-stack-shift' (s , r) drop ptr args drop' ass
drop-stack-shift' (if0 x x₁ ∷ s , r) (suc drop) ptr args drop' ()
drop-stack-shift' (op₂ x x₁ ∷ s , r) (suc drop) ptr args drop' ()
drop-stack-shift' (op₁ x ∷ s , r) (suc drop) ptr args drop' ()
R-stack-shift : ∀ rank hs c s ptr args drop → R-stack rank hs (arg c ∷ s) ([] , just (ptr , suc args , drop)) →
R-stack rank hs s ([] , just (ptr , args , suc drop))
R-stack-shift zero hs c s ptr args drop ()
R-stack-shift (suc zero) hs c [] ptr args drop (s' , luptr , ([] , just (ptr' , args' , drop')) , drop≡just , nargs , ())
R-stack-shift (suc (suc rank)) hs c [] ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
s' , luptr , ([] , just (ptr' , args , suc drop'))
, drop-stack-shift' s' drop ptr' args drop' drop≡just , refl
, R-stack-shift (suc rank) hs c [] ptr' args drop' Rsds'
R-stack-shift (suc zero) hs c (x ∷ s) ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , ())
R-stack-shift (suc (suc rank)) hs c (x ∷ s) ptr args drop (s' , luptr , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
s' , luptr , ([] , just (ptr' , args , suc drop'))
, drop-stack-shift' s' drop ptr' args drop' drop≡just , refl
, R-stack-shift (suc rank) hs c (x ∷ s) ptr' args drop' Rsds'
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , ([] , nothing) , drop≡just , nargs , ())
R-stack-shift (suc rank) hs c [] ptr args drop (s' , luptr , (arg c' ∷ ds' , r) , drop≡just , nargs , Rcc' , Rsds') =
s' , luptr , (ds' , r) , drop-stack-shift s' drop c' ds' r drop≡just , suc-inj nargs , Rsds'
R-stack-shift (suc rank) hs c (x ∷ s) ptr args drop (s' , luptr , (arg c' ∷ ds' , r) , drop≡just , nargs , Rcc' , Rsds')
= s' , luptr , (ds' , r) , drop-stack-shift s' drop c' ds' r drop≡just , suc-inj nargs , Rsds'
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (if0 x x₁ ∷ ds' , r) , drop≡just , nargs , () , _)
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (op₂ x x₁ ∷ ds' , r) , drop≡just , nargs , () , _)
R-stack-shift (suc rank) hs c s ptr args drop (s' , luptr , (op₁ x ∷ ds' , r) , drop≡just , nargs , () , _)
stack-drop-index : ∀ s drop c xs r → drop-stack s drop ≡ just (arg c ∷ xs , r) → stack-index s drop ≡ just (local c)
stack-drop-index ([] , r') zero c xs r ()
stack-drop-index ([] , just (ptr , zero , drop')) (suc drop) c xs r ()
stack-drop-index ([] , just (ptr , suc args , drop')) (suc drop) c xs r drop≡just =
stack-drop-index ([] , just (ptr , args , suc drop')) drop c xs r drop≡just
stack-drop-index ([] , nothing) (suc drop) c xs r ()
stack-drop-index (arg x ∷ s , just x₁) zero .x .s .(just x₁) refl = refl
stack-drop-index (arg x ∷ s , just x₁) (suc drop) c xs r drop≡just = stack-drop-index (s , just x₁) drop c xs r drop≡just
stack-drop-index (arg x ∷ s , nothing) zero .x .s .nothing refl = refl
stack-drop-index (arg x ∷ s , nothing) (suc drop) c xs r drop≡just = stack-drop-index (s , nothing) drop c xs r drop≡just
stack-drop-index (if0 x x₁ ∷ s , just (ptr , args , drop')) zero c xs r ()
stack-drop-index (if0 x x₁ ∷ s , just (ptr , args , drop')) (suc drop) c xs r ()
stack-drop-index (if0 x x₁ ∷ s , nothing) zero c xs r ()
stack-drop-index (if0 x x₁ ∷ s , nothing) (suc drop) c xs r ()
stack-drop-index (op₂ x x₁ ∷ s , r') zero c xs r ()
stack-drop-index (op₂ x x₁ ∷ s , r') (suc drop) c xs r ()
stack-drop-index (op₁ x ∷ s , r') zero c xs r ()
stack-drop-index (op₁ x ∷ s , r') (suc drop) c xs r ()
stack-drop-index' : ∀ s drop ptr' args drop' → drop-stack s drop ≡ just ([] , just (ptr' , suc args , drop')) → stack-index s drop ≡ just (remote ptr' drop')
stack-drop-index' ([] , just .(ptr' , suc args , drop')) zero ptr' args drop' refl = refl
stack-drop-index' ([] , nothing) zero ptr' args drop' ()
stack-drop-index' ([] , just (ptr , zero , drop'')) (suc drop) ptr' args drop' ()
stack-drop-index' ([] , just (ptr , suc args' , drop'')) (suc drop) ptr' args drop' drop≡just =
stack-drop-index' ([] , just (ptr , args' , suc drop'')) drop ptr' args drop' drop≡just
stack-drop-index' ([] , nothing) (suc drop) ptr' args drop' ()
stack-drop-index' (arg x ∷ s , r) zero ptr' args drop' ()
stack-drop-index' (arg x ∷ s , r) (suc drop) ptr' args drop' drop≡just = stack-drop-index' (s , r) drop ptr' args drop' drop≡just
stack-drop-index' (if0 x x₁ ∷ s , r) zero ptr' args drop' ()
stack-drop-index' (if0 x x₁ ∷ s , r) (suc drop) ptr' args drop' ()
stack-drop-index' (op₂ x x₁ ∷ s , r) zero ptr' args drop' ()
stack-drop-index' (op₂ x x₁ ∷ s , r) (suc drop) ptr' args drop' ()
stack-drop-index' (op₁ x ∷ s , r) zero ptr' args drop' ()
stack-drop-index' (op₁ x ∷ s , r) (suc drop) ptr' args drop' ()
R-remote-pop-stack : ∀ rank hs c s ptr args drop → R-stack rank hs (arg c ∷ s) ([] , just (ptr , suc args , drop)) →
∃ λ rank' → R-envelem rank' hs (clos c) (remote ptr drop)
R-remote-pop-stack zero hs c s ptr args drop ()
R-remote-pop-stack (suc rank) hs c s ptr args zero ((.[] , .(just (ptr' , suc args , drop'))) , lus' , ([] , just (ptr' , .(suc args) , drop')) , refl , refl , Rsds') =
let s' = [] , just (ptr' , suc args , drop')
(rank' , Rcptr') = R-remote-pop-stack rank hs c s ptr' args drop' Rsds'
in suc rank' , s' , lus' , remote ptr' drop' , refl , Rcptr'
R-remote-pop-stack (suc zero) hs c s ptr args (suc drop) (s' , lus' , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , ())
R-remote-pop-stack (suc (suc rank)) hs c s ptr args (suc drop) (s' , lus' , ([] , just (ptr' , .(suc args) , drop')) , drop≡just , refl , Rsds') =
let (rank' , Rcptr') = R-remote-pop-stack (suc rank) hs c s ptr' args drop' Rsds'
in suc rank' , s' , lus' , remote ptr' drop' , stack-drop-index' s' (suc drop) ptr' args drop' drop≡just , Rcptr'
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , ([] , nothing) , drop≡just , nargs , ())
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (arg c' ∷ xs , r) , drop≡just , nargs , Rcc' , Rsds') =
1 , s' , lus' , local c' , stack-drop-index s' drop c' xs r drop≡just , Rcc'
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (if0 x x₁ ∷ _ , _) , drop≡just , nargs , () , Rsds')
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (op₂ x x₁ ∷ _ , _) , drop≡just , nargs , () , Rsds')
R-remote-pop-stack (suc rank) hs c s ptr args drop (s' , lus' , (op₁ x ∷ _ , _) , drop≡just , nargs , () , Rsds')
R-machine : Heaps → Rel Config (Maybe Thread)
R-machine hs (t₁ , e₁ , s₁) (just (t₂ , e₂ , s₂)) =
R-term t₁ t₂ × R-env hs e₁ e₂ × (∃ λ rank → R-stack rank hs s₁ s₂)
R-machine hs (t₁ , e₁ , s₁) nothing = ⊥
R-sync : Rel Config SyncNetwork
R-sync cfg nodes = ∃ λ i →
all nodes except i are inactive ×
R-machine (proj₂ ∘ nodes) cfg (proj₁ (nodes i))
_⊆s_ : (hs hs' : Heaps) → Set
hs ⊆s hs' = ∀ i → hs i ⊆ hs' i
⊆s-refl : (hs : Heaps) → hs ⊆s hs
⊆s-refl hs node = ⊆-refl (hs node)
⊆s-trans : {hs₁ hs₂ hs₃ : Heaps} → hs₁ ⊆s hs₂ → hs₂ ⊆s hs₃ → hs₁ ⊆s hs₃
⊆s-trans hs₁⊆shs₂ hs₂⊆shs₃ node = ⊆-trans (hs₁⊆shs₂ node) (hs₂⊆shs₃ node)
update-heaps-⊆s : ∀ (nodes : SyncNetwork) n {x' conth'}
→ let (_ , conth) = nodes n in
conth ⊆ conth' → proj₂ ∘ nodes ⊆s proj₂ ∘ update nodes n (x' , conth')
update-heaps-⊆s nodes n conth⊆conth' n' with n' ≟ n
update-heaps-⊆s nodes n conth⊆conth' .n | yes refl = conth⊆conth'
update-heaps-⊆s nodes n conth⊆conth' n' | no ¬p = ⊆-refl (proj₂ (nodes n'))
update-update-heaps-⊆s : ∀ (nodes : SyncNetwork) n {x x' conth conth'}
→ conth ⊆ conth' → proj₂ ∘ update nodes n (x , conth) ⊆s proj₂ ∘ update nodes n (x' , conth')
update-update-heaps-⊆s nodes n conth⊆conth' n' with n' ≟ n
update-update-heaps-⊆s nodes n conth⊆conth' .n | yes refl = conth⊆conth'
update-update-heaps-⊆s nodes n conth⊆conth' n' | no ¬p = ⊆-refl (proj₂ (nodes n'))
update-heaps-⊆s-same : ∀ (nodes : SyncNetwork) n {x y x'}
→ nodes n ≡ (x , y)
→ proj₂ ∘ nodes ⊆s proj₂ ∘ update nodes n (x' , y)
update-heaps-⊆s-same nodes n eq
= update-heaps-⊆s nodes n (subst (λ p → (proj₂ p) ⊆ _) (sym eq) (⊆-refl _))
module HeapUpdate (hs hs' : Heaps)(hs⊆shs' : hs ⊆s hs') where
s-ext-pred : ∀ contptr {P Q} → (∀ s → P s → Q s) → stack-ext-pred hs contptr P → stack-ext-pred hs' contptr Q
s-ext-pred (ptr , loc) f (s , lu , x) = s , hs⊆shs' loc ptr lu , f s x
closure : ∀ c c' → R-closure hs c c' → R-closure hs' c c'
envelem : ∀ rank el el' → R-envelem rank hs el el' → R-envelem rank hs' el el'
envelem zero (clos c) (local c') Rcc' = closure c c' Rcc'
envelem (suc rank) (clos c) (local c') Rcc' = Rcc'
envelem zero (clos c) (remote contptr index) Relel' = Relel'
envelem (suc rank) (clos c) (remote contptr index) Relel' = s-ext-pred contptr f Relel'
where
f : ∀ s →
(∃ λ ee' → stack-index s index ≡ just ee' × R-envelem rank hs (clos c) ee') →
∃ λ ee' → stack-index s index ≡ just ee' × R-envelem rank hs' (clos c) ee'
f s (ee' , si , Rcee') = ee' , si , envelem rank (clos c) ee' Rcee'
env : ∀ e e' → R-env hs e e' → R-env hs' e e'
env [] [] Ree' = Ree'
env [] (x ∷ e') Ree' = Ree'
env (x ∷ e) [] Ree' = Ree'
env (x ∷ e) (x' ∷ e') ((rank , Rxx') , Ree') = (rank , envelem rank x x' Rxx') , env e e' Ree'
closure (t , e) (t' , e') (Rtt' , Ree') = Rtt' , env e e' Ree'
stackelem : ∀ el el' → R-stackelem hs el el' → R-stackelem hs' el el'
stackelem (arg c) (arg c') Rcc' = closure c c' Rcc'
stackelem (if0 c₁ c₂) (if0 c₁' c₂') (Rc₁c₁' , Rc₂c₂') = closure c₁ c₁' Rc₁c₁' , closure c₂ c₂' Rc₂c₂'
stackelem (op₂ f c) (op₂ g c') (f≡g , Rcc') = f≡g , closure c c' Rcc'
stackelem (op₁ f) (op₁ g) f≡g = f≡g
stackelem (arg x) (if0 x₁ x₂) Relel' = Relel'
stackelem (arg x) (op₂ x₁ x₂) Relel' = Relel'
stackelem (arg x) (op₁ x₁) Relel' = Relel'
stackelem (if0 x x₁) (arg x₂) Relel' = Relel'
stackelem (if0 x x₁) (op₂ x₂ x₃) Relel' = Relel'
stackelem (if0 x x₁) (op₁ x₂) Relel' = Relel'
stackelem (op₂ x x₁) (arg x₂) Relel' = Relel'
stackelem (op₂ x x₁) (if0 x₂ x₃) Relel' = Relel'
stackelem (op₂ x x₁) (op₁ x₂) Relel' = Relel'
stackelem (op₁ x) (arg x₁) Relel' = Relel'
stackelem (op₁ x) (if0 x₁ x₂) Relel' = Relel'
stackelem (op₁ x) (op₂ x₁ x₂) Relel' = Relel'
stack : ∀ rank s s' → R-stack rank hs s s' → R-stack rank hs' s s'
stack zero [] ([] , nothing) Rss' = Rss'
stack (suc rank) [] ([] , nothing) Rss' = Rss'
stack zero [] (x ∷ s' , r) Rss' = Rss'
stack (suc rank) [] (x ∷ s' , r) Rss' = Rss'
stack zero (x ∷ s) ([] , nothing) Rss' = Rss'
stack (suc rank) (x ∷ s) ([] , nothing) Rss' = Rss'
stack zero (x ∷ s) (x' ∷ s' , r) (Rxx' , Rss') = stackelem x x' Rxx' , stack zero s (s' , r) Rss'
stack (suc rank) (x ∷ s) (x' ∷ s' , r) (Rxx' , Rss') = stackelem x x' Rxx' , stack (suc rank) s (s' , r) Rss'
stack zero [] ([] , just (contptr , args , drop)) Rss' = Rss'
stack zero (x ∷ s) ([] , just (contptr , args , drop)) Rss' = Rss'
stack (suc rank) [] ([] , just (contptr , args , drop)) Rss' = s-ext-pred contptr f Rss'
where
f : ∀ s' →
(∃ λ ds → drop-stack s' drop ≡ just ds × num-args ds ≡ args × R-stack rank hs [] ds) →
∃ λ ds → drop-stack s' drop ≡ just ds × num-args ds ≡ args × R-stack rank hs' [] ds
f s₁ (ds , drops , nargs , Rsds) = ds , drops , nargs , stack rank [] ds Rsds
stack (suc rank) (x ∷ s) ([] , just (contptr , args , drop)) Rss' = s-ext-pred contptr f Rss'
where
f : ∀ s' →
(∃ λ ds → drop-stack s' drop ≡ just ds × num-args ds ≡ args × R-stack rank hs (x ∷ s) ds) →
∃ λ ds → drop-stack s' drop ≡ just ds × num-args ds ≡ args × R-stack rank hs' (x ∷ s) ds
f s₁ (ds , drops , nargs , Rsds) = ds , drops , nargs , stack rank (x ∷ s) ds Rsds
machine : ∀ cfg m → R-machine hs cfg m → R-machine hs' cfg m
machine (t , e , s) (just (t' , e' , s')) (Rtt' , Ree' , rank , Rss') =
Rtt' , env e e' Ree' , rank , stack rank s s' Rss'
machine cfg nothing Rcfgm = Rcfgm
nodes-ia-update-ia : ∀ nodes n loc {hs} → all nodes except n are inactive
→ let nodes' = update nodes n (nothing , hs) in
let heaps' = proj₂ ∘ nodes'
in nothing , heaps' loc ≡ nodes' loc
nodes-ia-update-ia nodes n loc ia with loc ≟ n
... | yes p = refl
... | no ¬p = cong (λ p → p , proj₂ (nodes loc)) (sym (ia loc ¬p))
nodes-ia-update : ∀ nodes n loc {dcfg-loc hs} → all nodes except n are inactive
→ let nodes' = update nodes n (nothing , hs) in
let heaps' = proj₂ ∘ nodes' in
let nodes'' = update nodes' loc (just dcfg-loc , heaps' loc)
in all nodes'' except loc are inactive
nodes-ia-update nodes n loc ia n' ¬n'≡loc with n' ≟ loc
... | yes p = ⊥-elim (¬n'≡loc p)
... | no ¬p with n' ≟ n
... | yes q = refl
... | no ¬q = ia n' ¬q
lookup-var : ∀ hs e e' x el → R-env hs e e' → lookup x e ≡ just el → ∃ λ el' → lookup x e' ≡ just el' × ∃ λ rank → R-envelem rank hs el el'
lookup-var hs [] [] zero el Ree' ()
lookup-var hs [] [] (suc x) el Ree' ()
lookup-var hs [] (x ∷ e') n el () lu
lookup-var hs (x ∷ e) [] n el () lu
lookup-var hs (.el ∷ e) (el' ∷ e') zero el (Relel' , Ree') refl = el' , refl , Relel'
lookup-var hs (_ ∷ e) (_ ∷ e') (suc x) el (_ , Ree') lu = lookup-var hs e e' x el Ree' lu
R-machine-node-eq : ∀ nodes n {m} {node}
→ nodes n ≡ node
→ let heaps = proj₂ ∘ nodes
in R-machine heaps m (proj₁ node)
→ R-machine heaps m (proj₁ (nodes n))
R-machine-node-eq nodes n {m}{node} eq
= subst (R-machine (proj₂ ∘ nodes) m)
(proj₁ (,-inj (sym eq)))
R-machine-node : ∀ nodes n {m} {node}
→ let heaps = proj₂ ∘ update nodes n node
in R-machine heaps m (proj₁ node)
→ R-machine heaps m (proj₁ (update nodes n node n))
R-machine-node nodes n {m}{node}
= R-machine-node-eq (update nodes n node) n (update-look nodes n node)
node-step-silent : ∀ nodes n {hs thread machine}
→ nodes n ≡ just thread , hs
→ n ⊢ (just thread , hs) ⟶DKrivine< silent > machine
→ nodes ⟶Sync⁺ update nodes n machine
node-step-silent nodes n {hs}{thread}{machine} eq st
= [ silent-step (subst (λ p → n ⊢ p ⟶DKrivine< silent > machine) (sym eq) st) ]
node-step-silent-thread : ∀ nodes n {hs thread machine}
→ nodes n ≡ just thread , hs
→ n ⊢ (just thread , proj₂ (nodes n)) ⟶DKrivine< silent > machine
→ nodes ⟶Sync⁺ update nodes n machine
node-step-silent-thread nodes n {hs}{thread}{machine} eq st
= [ silent-step (subst (λ p → n ⊢ (p , proj₂ (nodes n)) ⟶DKrivine< silent > machine)
(sym (proj₁ (,-inj eq)))
st) ]
node-step-comm : ∀ nodes sender receiver {hs thread msg hs' receiver'}
→ all nodes except sender are inactive
→ nodes sender ≡ just thread , hs
→ sender ⊢ (just thread , proj₂ (nodes sender)) ⟶DKrivine< send msg > (nothing , hs')
→ let nodes' = update nodes sender (nothing , hs') in
let heaps' = proj₂ ∘ nodes'
in receiver ⊢ (nothing , heaps' receiver) ⟶DKrivine< receive msg > receiver'
→ nodes ⟶Sync update nodes' receiver receiver'
node-step-comm nodes sender receiver {hs}{thread}{msg}{hs'}{receiver'} ia eq sendstep receivestep
= comm-step (subst (λ p → sender ⊢ (p , proj₂ (nodes sender)) ⟶DKrivine< send msg > (nothing , hs'))
(sym (proj₁ (,-inj eq)))
sendstep)
(subst (λ p → receiver ⊢ p ⟶DKrivine< receive msg > receiver')
(nodes-ia-update-ia nodes sender receiver ia)
receivestep)
¬suc-args : ∀ hs x s s' args srank → num-args s' ≡ suc args → (∄ λ c → x ≡ arg c) → ¬ R-stack srank hs (x ∷ s) s'
¬suc-args hs x s ([] , just (contptr , .(suc args) , drop)) args zero refl ≠arg Rss' = Rss'
¬suc-args hs x s ([] , just (contptr , .(suc args) , drop)) args (suc srank) refl ≠arg (s' , lu , d-s' , drop≡just , nargs≡sargs , Rss') =
¬suc-args hs x s d-s' args srank nargs≡sargs ≠arg Rss'
¬suc-args hs x s ([] , nothing) args srank nargs≡suc ≠arg Rss' = Rss'
¬suc-args hs (arg x) s (x₁ ∷ s' , r) args srank nargs≡suc ≠arg Rss' = ≠arg (x , refl)
¬suc-args hs (if0 x x₁) s (arg x₂ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (if0 x x₁) s (if0 x₂ x₃ ∷ s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (if0 x x₁) s (op₂ x₂ x₃ ∷ s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (if0 x x₁) s (op₁ x₂ ∷ s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (op₂ x x₁) s (arg x₂ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₂ x x₁) s (if0 x₂ x₃ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₂ x x₁) s (op₂ x₂ x₃ ∷ s' , r) args srank () ≠arg (Relel' , Rss')
¬suc-args hs (op₂ x x₁) s (op₁ x₂ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (arg x₁ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (if0 x₁ x₂ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (op₂ x₁ x₂ ∷ s' , r) args srank nargs≡suc ≠arg (Relel' , Rss') = Relel'
¬suc-args hs (op₁ x) s (op₁ x₁ ∷ s' , r) args srank () ≠arg (Relel' , Rss')
R-stackcont : ∀ (nodes₁ nodes₂ : SyncNetwork) s s' i (x : Maybe Thread) rank →
let hs₁ = proj₂ ∘ nodes₁
conth = hs₁ i
(conth' , ptr) = i ⊢ hs₁ i ▸ s'
nodes₁' = update nodes₁ i (x , conth')
hs₁' = proj₂ ∘ nodes₁'
hs₂ = proj₂ ∘ nodes₂
in hs₁' ⊆s hs₂ → R-stack rank hs₁ s s' → R-stack (suc rank) hs₂ s ([] , just (ptr , num-args s' , 0))
R-stackcont nodes₁ nodes₂ [] s' i x rank hs₁'⊆shs₂ Rss' =
let hs₁ = proj₂ ∘ nodes₁
(conth' , ptr , loc) = i ⊢ hs₁ i ▸ s'
nodes₁' = update nodes₁ i (x , conth')
ul : nodes₁' i ≡ (x , conth')
ul = update-look nodes₁ i (x , conth')
hs₁' = proj₂ ∘ nodes₁'
hs₁⊆shs₁' : hs₁ ⊆s hs₁'
hs₁⊆shs₁' = update-heaps-⊆s nodes₁ i (h⊆h▸x (hs₁ i))
hs₂ = proj₂ ∘ nodes₂
hs₁⊆shs₂ = ⊆s-trans hs₁⊆shs₁' hs₁'⊆shs₂
Rss'₂ = HeapUpdate.stack hs₁ hs₂ hs₁⊆shs₂ rank [] s' Rss'
p : hs₁' i ≡ conth'
p = cong proj₂ ul
in s' , hs₁'⊆shs₂ i ptr (subst (λ p → p ! ptr ≡ just s') (sym p) (!-▸ (hs₁ i) s')) , s' , drop-stack0 s' , refl , Rss'₂
R-stackcont nodes₁ nodes₂ (e ∷ s) s' i x rank hs₁'⊆shs₂ Rss' =
let hs₁ = proj₂ ∘ nodes₁
(conth' , ptr , loc) = i ⊢ hs₁ i ▸ s'
nodes₁' = update nodes₁ i (x , conth')
ul : nodes₁' i ≡ (x , conth')
ul = update-look nodes₁ i (x , conth')
hs₁' = proj₂ ∘ nodes₁'
hs₁⊆shs₁' : hs₁ ⊆s hs₁'
hs₁⊆shs₁' = update-heaps-⊆s nodes₁ i (h⊆h▸x (hs₁ i))
hs₂ = proj₂ ∘ nodes₂
hs₁⊆shs₂ = ⊆s-trans hs₁⊆shs₁' hs₁'⊆shs₂
Rss'₂ = HeapUpdate.stack hs₁ hs₂ hs₁⊆shs₂ rank (e ∷ s) s' Rss'
p : hs₁' i ≡ conth'
p = cong proj₂ ul
in s' , hs₁'⊆shs₂ i ptr (subst (λ p → p ! ptr ≡ just s') (sym p) (!-▸ (hs₁ i) s')) , s' , drop-stack0 s' , refl , Rss'₂
simulation-var : ∀ t e s n e' s' nodes i conth el → let hs = proj₂ ∘ nodes in
(∃ λ rank → R-envelem rank hs (clos (t , e)) el) → (∃ λ rank → R-stack rank hs s s') →
all nodes except i are inactive → nodes i ≡ just (var n , e' , s') , conth → lookup n e' ≡ just el →
∃ λ nodes' → nodes ⟶Sync⁺ nodes' × R-sync (t , e , s) nodes'
simulation-var t e s n e' s' nodes i conth el (erank , Reel) Rss' ia nodesi≡just lu with nodes i | inspect nodes i
simulation-var t e s n e' s' nodes i conth (remote x x₁) (zero , ()) Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ]
simulation-var t e s n e' s' nodes i conth (local x) (suc erank , ()) Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ]
simulation-var t e s n e' s' nodes i conth (local (.t , e'')) (zero , refl , Ree') Rss' ia refl lu | .(just (var n , e' , s') , conth) | [ eq ] =
let dcfg' = just (t , e'' , s') , conth
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , e , s) (proj₁ dcfg')
(refl , Ree' , Rss')
in nodes' , node-step-silent nodes i eq (VAR lu)
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-var t e s n e' s' nodes i conth (remote (ptr , j) index) (suc erank , j-s , j-lu , j-el , stack-index≡just , Relj-el) (srank , Rss') ia refl lu | .(just (var n , e' , s') , conth) | [ eq ] =
let heaps = proj₂ ∘ nodes
i-conth = heaps i
(conth₁ , i-contptr) = i ⊢ i-conth ▸ s'
i-cfg₁ = nothing , conth₁
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
heaps⊆sheaps₁ : heaps ⊆s heaps₁
heaps⊆sheaps₁ = update-heaps-⊆s nodes i (h⊆h▸x i-conth)
j-conth = heaps₁ j
j-cfg₂ = just (var 0 , j-el ∷ [] , [] , just (i-contptr , num-args s' , 0)) , j-conth
(j-s₁ , j-lu₁ , j-el₁ , stack-index≡just₁ , Relj-el₁) =
HeapUpdate.envelem heaps heaps₁ heaps⊆sheaps₁ (suc erank)
(clos (t , e)) (remote (ptr , j) index)
(j-s , j-lu , j-el , stack-index≡just , Relj-el)
nodes₂ = update nodes₁ j j-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
Relj-el₂ = HeapUpdate.envelem heaps heaps₂ heaps⊆sheaps₂ erank (clos (t , e)) j-el Relj-el
ia' = nodes-ia-update nodes i j ia
(nodes₃ , steps , Rcfgnodes₃) =
simulation-var t e s 0 (j-el ∷ []) ([] , just (i-contptr , num-args s' , 0))
nodes₂ j j-conth j-el (erank , Relj-el₂)
(suc srank , R-stackcont nodes nodes₂ s s' i nothing srank heaps₁⊆sheaps₂ Rss')
ia' (update-look nodes₁ j j-cfg₂) refl
in nodes₃ , (node-step-comm nodes i j ia eq (VAR-send lu) (VAR-receive j-lu₁ stack-index≡just) ∷ steps) , Rcfgnodes₃
simulation-return : ∀ n e s cfg' e' s' i nodes srank conth →
let cfg = (lit n , e , s)
hs = proj₂ ∘ nodes
in cfg ⟶Krivine cfg' →
all nodes except i are inactive →
nodes i ≡ just (lit n , e' , s') , conth →
R-stack srank hs s s' → ∃ λ nodes' → nodes ⟶Sync⁺ nodes' × R-sync cfg' nodes'
simulation-return .0 e ._ ._ e' ([] , just x) i nodes zero conth COND-0 ia eq ()
simulation-return .0 e ._ ._ e' ([] , nothing) i nodes srank conth COND-0 ia eq ()
simulation-return .0 e ._ ._ e' (arg x ∷ s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e ._ ._ e' (op₂ x x₁ ∷ s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e ._ ._ e' (op₁ x ∷ s' , r) i nodes srank conth COND-0 ia eq (() , Rss')
simulation-return .0 e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' (if0 (.t₁ , e₁') (.t₂ , e₂') ∷ s' , r) i nodes srank conth COND-0 ia eq (((refl , Re₁e₁'),(refl , Re₂e₂')) , Rss') =
let dcfg' = just (t₁ , e₁' , s' , r) , conth
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t₁ , e₁ , s) (proj₁ dcfg')
(refl , Re₁e₁' , srank , Rss')
in nodes' , node-step-silent nodes i eq COND-0
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-return .0 e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth COND-0 ia eq Rss' =
⊥-elim (¬suc-args (proj₂ ∘ nodes) (if0 (t₁ , e₁) (t₂ , e₂)) s ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl lem Rss')
where
lem : ∄ (λ c → if0 _ _ ≡ arg c)
lem (c , ())
simulation-return .0 e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' ([] , just ((contptr , j) , 0 , drop)) i nodes (suc srank) conth COND-0 ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
let heaps = proj₂ ∘ nodes
ks = if0 (t₁ , e₁) (t₂ , e₂) ∷ s
ds = ([] , just ((contptr , j) , 0 , drop))
i-conth = heaps i
i-cfg₁ = nothing , i-conth
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
heaps⊆sheaps₁ : heaps ⊆s heaps₁
heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
(_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
j-conth = heaps₁ j
j-cfg₂ = just (lit 0 , [] , d-s') , j-conth
nodes₂ = update nodes₁ j j-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
ia' = nodes-ia-update nodes i j ia
Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
(nodes₃ , steps , Rcfgnodes₃) = simulation-return 0 [] ks _ [] d-s' j nodes₂ srank j-conth COND-0 ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁) ∷ steps , Rcfgnodes₃
simulation-return ._ e ._ ._ e' ([] , just x) i nodes zero conth COND-suc ia eq ()
simulation-return ._ e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth COND-suc ia eq Rss' =
⊥-elim (¬suc-args (proj₂ ∘ nodes) (if0 _ _) s ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl lem Rss')
where
lem : ∄ (λ c → if0 _ _ ≡ arg c)
lem (c , ())
simulation-return ._ e ._ ._ e' ([] , nothing) i nodes srank conth COND-suc ia eq ()
simulation-return ._ e ._ ._ e' (arg x ∷ s' , r) i nodes srank conth COND-suc ia eq (() , Rss')
simulation-return ._ e ._ ._ e' (op₂ x x₁ ∷ s' , r) i nodes srank conth COND-suc ia eq (() , Rss')
simulation-return ._ e ._ ._ e' (op₁ x ∷ s' , r) i nodes srank conth (COND-suc {t = proj₁ , proj₂}) ia eq (() , Rss')
simulation-return ._ e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' (if0 (.t₁ , e₁') (.t₂ , e₂') ∷ s' , r) i nodes srank conth COND-suc ia eq (((refl , Re₁e₁'),(refl , Re₂e₂')), Rss') =
let dcfg' = just (t₂ , e₂' , s' , r) , conth
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t₂ , e₂ , s) (proj₁ dcfg')
(refl , Re₂e₂' , srank , Rss')
in nodes' , node-step-silent nodes i eq COND-suc
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-return ._ e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth COND-suc ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
let heaps = proj₂ ∘ nodes
ks = if0 (t₁ , e₁) (t₂ , e₂) ∷ s
ds = ([] , just ((contptr , j) , 0 , drop))
i-conth = heaps i
i-cfg₁ = nothing , i-conth
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
heaps⊆sheaps₁ : heaps ⊆s heaps₁
heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
(_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
j-conth = heaps₁ j
j-cfg₂ = just (lit _ , [] , d-s') , j-conth
nodes₂ = update nodes₁ j j-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
ia' = nodes-ia-update nodes i j ia
Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
(nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth COND-suc ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁) ∷ steps , Rcfgnodes₃
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' ([] , just ((contptr , j) , suc args , drop)) i nodes srank conth OP₂ ia eq Rss' =
⊥-elim (¬suc-args (proj₂ ∘ nodes) (op₂ f (t₁ , e₁)) s ([] , just ((contptr , j) , suc args , drop)) args srank refl lem Rss')
where
lem : ∄ (λ c → op₂ _ _ ≡ arg c)
lem (c , ())
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' ([] , nothing) i nodes srank conth OP₂ ia eq ()
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' (arg x ∷ s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' (if0 x x₁ ∷ s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' (op₁ x ∷ s' , r) i nodes srank conth OP₂ ia eq (() , Rss')
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' (op₂ .f (.t₁ , e₁') ∷ s' , r) i nodes srank conth OP₂ ia eq ((refl , refl , Re₁e₁') , Rss') =
let dcfg' = just (t₁ , e₁' , op₁ (f n) ∷ s' , r) , conth
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t₁ , e₁ , op₁ (f n) ∷ s) (proj₁ dcfg')
(refl , Re₁e₁' , srank , refl , Rss')
in nodes' , node-step-silent nodes i eq OP₂
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' ([] , just ((contptr , j) , zero , drop)) i nodes zero conth OP₂ ia eq ()
simulation-return n e (op₂ f (t₁ , e₁) ∷ s) .(t₁ , e₁ , op₁ (f n) ∷ s) e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth OP₂ ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
let heaps = proj₂ ∘ nodes
ks = op₂ f (t₁ , e₁) ∷ s
ds = ([] , just ((contptr , j) , 0 , drop))
i-conth = heaps i
i-cfg₁ = nothing , i-conth
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
heaps⊆sheaps₁ : heaps ⊆s heaps₁
heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
(_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
j-conth = heaps₁ j
j-cfg₂ = just (lit _ , [] , d-s') , j-conth
nodes₂ = update nodes₁ j j-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
ia' = nodes-ia-update nodes i j ia
Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
(nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth OP₂ ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁) ∷ steps , Rcfgnodes₃
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , suc args , drop)) i nodes srank conth OP₁ ia eq Rss' =
⊥-elim (¬suc-args (proj₂ ∘ nodes) (op₁ f) s ([] , just ((contptr , j) , suc args , drop)) args srank refl lem Rss')
where
lem : ∄ (λ c → op₁ f ≡ arg c)
lem (c , ())
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , zero , drop)) i nodes zero conth OP₁ ia eq ()
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' ([] , nothing) i nodes srank conth OP₁ ia eq ()
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' (arg x ∷ s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' (if0 x x₁ ∷ s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' (op₂ x x₁ ∷ s' , r) i nodes srank conth OP₁ ia eq (() , Rss')
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' (op₁ .f ∷ s' , r) i nodes srank conth OP₁ ia eq (refl , Rss') =
let dcfg' = just (lit (f n) , [] , s' , r) , conth
nodes' = update nodes i dcfg'
heaps = proj₂ ∘ nodes
heaps' = proj₂ ∘ nodes'
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (lit (f n) , [] , s) (proj₁ dcfg')
(refl , tt , srank , Rss')
in nodes' , node-step-silent nodes i eq OP₁
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-return n e (op₁ f ∷ s) .(lit (f n) , [] , s) e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth OP₁ ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
let heaps = proj₂ ∘ nodes
ks = op₁ f ∷ s
ds = ([] , just ((contptr , j) , 0 , drop))
i-conth = heaps i
i-cfg₁ = nothing , i-conth
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
heaps⊆sheaps₁ : heaps ⊆s heaps₁
heaps⊆sheaps₁ = update-heaps-⊆s-same nodes i refl
(_ , lu₁ , _ , drop≡just₁ , _ ) = HeapUpdate.stack heaps heaps₁ heaps⊆sheaps₁ (suc srank) ks ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
j-conth = heaps₁ j
j-cfg₂ = just (lit _ , [] , d-s') , j-conth
nodes₂ = update nodes₁ j j-cfg₂
heaps₂ = proj₂ ∘ nodes₂
heaps₁⊆sheaps₂ : heaps₁ ⊆s heaps₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
heaps⊆sheaps₂ = ⊆s-trans heaps⊆sheaps₁ heaps₁⊆sheaps₂
ia' = nodes-ia-update nodes i j ia
Rsd-s'₂ = HeapUpdate.stack heaps heaps₂ heaps⊆sheaps₂ srank ks d-s' Rsd-s'
(nodes₃ , steps , Rcfgnodes₃) = simulation-return _ [] ks _ [] d-s' j nodes₂ srank j-conth OP₁ ia' (update-look nodes₁ j j-cfg₂) Rsd-s'₂
in nodes₃ , node-step-comm nodes i j ia eq RETURN-send (RETURN-receive lu₁ drop≡just₁) ∷ steps , Rcfgnodes₃
simulation-sync : Simulation _⟶Krivine_ _⟶Sync⁺_ R-sync
simulation-sync cfg cfg' nodes st (i , ia , Rcfgn) with nodes i | inspect nodes i
simulation-sync cfg cfg' nodes st (i , ia , ()) | nothing , conth | [ eq ]
simulation-sync (.(lit 0) , e , if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ nodes COND-0 (i , ia , refl , _ , srank , Rss') | just (.(lit 0) , e' , s') , conth | [ eq ] =
simulation-return 0 e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) (t₁ , e₁ , s) e' s' i nodes srank conth COND-0 ia eq Rss'
simulation-sync (._ , e , if0 (t₁ , e₁) (t₂ , e₂) ∷ s) ._ nodes COND-suc (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
simulation-return _ e (if0 (t₁ , e₁) (t₂ , e₂) ∷ s) (t₂ , e₂ , s) e' s' i nodes srank conth COND-suc ia eq Rss'
simulation-sync (._ , e , op₂ f (t₁ , e₁) ∷ s) ._ nodes OP₂ (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
simulation-return _ e (op₂ f (t₁ , e₁) ∷ s) (t₁ , e₁ , op₁ (f _) ∷ s) e' s' i nodes srank conth OP₂ ia eq Rss'
simulation-sync (._ , e , op₁ f ∷ s) ._ nodes OP₁ (i , ia , refl , _ , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
simulation-return _ e (op₁ f ∷ s) (lit (f _) , [] , s) e' s' i nodes srank conth OP₁ ia eq Rss'
simulation-sync (._ , e , ._) ._ nodes POPARG (i , ia , refl , Rede , rank , ()) | just (._ , e' , [] , nothing) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , if0 x x₁ ∷ s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , op₂ x x₁ ∷ s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , rank , () , Rss') | just (._ , e' , op₁ x ∷ s' , r) , conth | [ eq ]
simulation-sync (ƛ t , e , arg c ∷ s) ._ nodes POPARG (i , ia , refl , Ree' , rank , Rcc' , Rss') | just (._ , e' , arg c' ∷ s' , r) , conth | [ eq ] =
let dcfg' = just (t , local c' ∷ e' , s' , r) , conth
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl conth
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , clos c ∷ e , s) (proj₁ dcfg')
(refl , ((0 , Rcc') , Ree') , rank , Rss')
in nodes' , node-step-silent nodes i eq POPARG
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (._ , e , ._) ._ nodes POPARG (i , ia , refl , Ree' , Rss') | just (._ , e' , [] , just (ptr , 0 , drop)) , conth | [ eq ] =
⊥-elim (R-stack-must-have-arg (proj₂ ∘ nodes) _ _ ptr drop Rss')
simulation-sync (ƛ t , e , arg c ∷ s) ._ nodes POPARG (i , ia , refl , Ree' , 0 , ()) | just (._ , e' , [] , just (ptr , suc args , drop)) , conth | [ eq ]
simulation-sync (ƛ t , e , arg c ∷ s) ._ nodes POPARG (i , ia , refl , Ree' , suc rank , Rss') | just (._ , e' , [] , just (ptr , suc args , drop)) , conth | [ eq ] =
let dcfg' = just (t , remote ptr drop ∷ e' , [] , just (ptr , args , suc drop)) , conth
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl conth
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , clos c ∷ e , s) (proj₁ dcfg')
(refl , (R-remote-pop-stack (suc rank) heaps c s ptr args drop Rss' , Ree') , suc rank , R-stack-shift (suc rank) heaps c s ptr args drop Rss')
in nodes' , node-step-silent nodes i eq POPARG-remote
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync ((t $ t') , e , s) ._ nodes PUSHARG (i , ia , refl , Ree' , rank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
let dcfg' = just (t , e' , arg (t' , e') ∷ s' , r) , conth
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl conth
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , e , arg (t' , e) ∷ s) (proj₁ dcfg')
(refl , Ree' , rank , (refl , Ree') , Rss')
in nodes' , node-step-silent nodes i eq PUSHARG
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (var n , e , s) ._ nodes (VAR {t = t}{e' = e₁} lun) (i , ia , refl , Ree' , Rss') | just (._ , e' , s') , conth | [ eq ] =
let heaps = proj₂ ∘ nodes
el' , lun' , Relel' = lookup-var heaps e e' n (clos (t , e₁)) Ree' lun
in simulation-var t e₁ s n e' s' nodes i conth el' Relel' Rss' ia eq lun'
simulation-sync (if0 b then t else f , e , s) ._ nodes COND (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
let dcfg' = just (b , e' , if0 (t , e') (f , e') ∷ s' , r) , conth
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl conth
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (b , e , if0 (t , e) (f , e) ∷ s) (proj₁ dcfg')
(refl , Ree' , srank , ((refl , Ree') , refl , Ree') , Rss')
in nodes' , node-step-silent nodes i eq COND
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (op f t t' , e , s) ._ nodes OP (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s' , r) , conth | [ eq ] =
let dcfg' = just (t , e' , op₂ f (t' , e') ∷ s' , r) , conth
heaps = proj₂ ∘ nodes
nodes' = update nodes i dcfg'
heaps' = proj₂ ∘ nodes'
h⊆h = ⊆-refl conth
heaps⊆sheaps' = update-heaps-⊆s-same nodes i eq
Rmachine' = HeapUpdate.machine heaps heaps' heaps⊆sheaps' (t , e , op₂ f (t' , e) ∷ s) (proj₁ dcfg')
(refl , Ree' , srank , (refl , (refl , Ree')) , Rss')
in nodes' , node-step-silent nodes i eq OP
, i , (λ i' i'≠i → update-others nodes inactive i dcfg' i' i'≠i (ia i' i'≠i))
, R-machine-node nodes i Rmachine'
simulation-sync (t at j , e , s) ._ nodes REMOTE (i , ia , refl , Ree' , srank , Rss') | just (._ , e' , s') , conth | [ eq ] =
let heaps = proj₂ ∘ nodes
(conth₁ , contptr) = i ⊢ heaps i ▸ s'
i-cfg₁ = nothing , conth₁
nodes₁ = update nodes i i-cfg₁
heaps₁ = proj₂ ∘ nodes₁
j-cfg₂ = just (t , [] , [] , just (contptr , num-args s' , 0)) , heaps₁ j
nodes₂ = update nodes₁ j j-cfg₂
heaps₁⊆sheaps₂ = update-heaps-⊆s-same nodes₁ j refl
Rcfgnodes₂ = refl , tt , suc srank , R-stackcont nodes nodes₂ s s' i nothing srank heaps₁⊆sheaps₂ Rss'
in nodes₂ , [ node-step-comm nodes i j ia eq REMOTE-send REMOTE-receive ]
, j , nodes-ia-update nodes i j ia , R-machine-node-eq nodes₂ j (update-look nodes₁ j j-cfg₂) Rcfgnodes₂