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

-- | Lemmas for different kinds of tagged messages
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

-- | The main theorem
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