open import GeneralLemmas using (Dec; _≡_)
module DKrivine.Soundness
  (Node : Set)
  (_≟_ : (n n' : Node)  Dec (n  n'))
  where
open import DKrivine Node _≟_ as DKrivine
open import DKrivine.Properties Node _≟_
open import DKrivine.Simulation 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

¬suc-args' :  hs s' args srank  num-args s'  suc args  ¬ R-stack srank hs [] s'
¬suc-args' hs ([] , just x) args zero nargs ()
¬suc-args' hs ([] , nothing) args zero () R[]s'
¬suc-args' hs ([] , just ((contptr , j) , .(suc args) , drop)) args (suc rank) refl (s' , lu , d-s' , drop≡just , nargs≡sargs , R[]d-s')
  = ¬suc-args' hs d-s' args rank nargs≡sargs R[]d-s'
¬suc-args' hs ([] , nothing) args (suc rank) () R[]s'
¬suc-args' hs (x  xx , just x₁) args zero nargs ()
¬suc-args' hs (x  xx , just x₁) args (suc rank) nargs ()
¬suc-args' hs (x  xx , nothing) args zero nargs ()
¬suc-args' hs (x  xx , nothing) args (suc rank) nargs ()

termination-return :  n e' s' i nodes srank conth 
  let hs  = proj₂  nodes
   in all nodes except i are inactive 
      nodes i  just (lit n , e' , s') , conth 
      R-stack srank hs [] s'  nodes ↓Sync lit n
termination-return n e' ([] , just x) i nodes zero conth ia eq ()
termination-return n e' ([] , nothing) i nodes (suc srank) conth ia eq ()
termination-return n e' (x  s , just x₁) i nodes zero conth ia eq ()
termination-return n e' (x  s , just x₁) i nodes (suc srank) conth ia eq ()
termination-return n e' (x  s , nothing) i nodes zero conth ia eq ()
termination-return n e' (x  s , nothing) i nodes (suc srank) conth ia eq ()
termination-return n e' ([] , nothing) i nodes zero conth ia eq R[]s' = nodes , [] , i , ia , e' , conth , eq
termination-return n e' ([] , just ((contptr , j) , suc args , drop)) i nodes (suc srank) conth ia eq R[]s' =
  ⊥-elim (¬suc-args' (proj₂  nodes) ([] , just ((contptr , j) , suc args , drop)) args (suc srank) refl R[]s')
termination-return n e' ([] , just ((contptr , j) , zero , drop)) i nodes (suc srank) conth ia eq (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s') =
  let heaps = proj₂  nodes
      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) [] ds (s' , lu , d-s' , drop≡just , nargs≡args , Rsd-s')
      j-conth = heaps₁ j
      j-cfg₂ = just (lit n , [] , 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 [] d-s' Rsd-s'
      (nodes₃ , steps , Rcfgnodes₃)  = termination-return n [] d-s' j nodes₂ srank j-conth 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₃

termination-agrees-sync :  cfg nodes n  R-sync cfg nodes  cfg ↓Krivine lit n  nodes ↓Sync lit n
termination-agrees-sync ._  nodes n (i , ia , Rcfgnodes) (e' , []) with nodes i | inspect nodes i
termination-agrees-sync .(lit n , e , []) nodes n (i , ia , refl , Ree' , srank , R[]s') (e , [])
  | just (.(lit n) , e' , s') , ch | [ eq ] =
    termination-return n e' s' i nodes srank ch ia eq R[]s'
termination-agrees-sync .(lit n , e , []) nodes n (i , ia , ()) (e , []) | nothing , ch | [ eq ]
termination-agrees-sync cfg nodes n Rcfgnodes (e' , step₁  steps) =
  let (nodes₂ , step₂ , Rcfgnodes₂) = simulation-sync cfg _ nodes step₁ Rcfgnodes
      (nodes₃ , steps' , Rcfgnodes₃) = termination-agrees-sync _ nodes₂ n Rcfgnodes₂ (e' , steps)
   in nodes₃ , step₂ ⁺++* steps' , Rcfgnodes₃

divergence-agrees-sync :  cfg nodes  R-sync cfg nodes  cfg ↑Krivine  nodes ↑Sync
divergence-agrees-sync cfg nodes (i , ia , Rcfgnodes) =
  divergence-simulation-dec-det cfg nodes simulation-sync decidable-Krivine
    ⟶Sync-preserves-one-active  nodes' iia  determinism-Sync nodes' (proj₁ iia) (proj₂ iia)) (i , ia , Rcfgnodes) (i , ia)

initial-related-sync :  t root  R-sync (t , [] , []) (initial-network-sync t root)
initial-related-sync t root = root , ia , Rmachine
  where
    nodes = initial-network-sync t root
    heaps = proj₂  nodes
    ia : all nodes except root are inactive
    ia n n≠root with n  root
    ... | yes p = ⊥-elim (n≠root p)
    ... | no ¬p = refl
    Rmachine = subst  p  R-machine heaps (t , [] , []) (proj₁ p))
                     (sym (update-look
                              i'  (nothing , ))
                             root
                             (just (t , [] , [] , nothing) , )))
                     (refl , tt , 0 , tt)