module CESH.Simulation (Node : Set) where

open import GeneralLemmas
open import CES             Node as CES
open import CESH            Node as CESH
open import CESH.Properties Node
open import Heap
open import MachineCode Node
open import Relation

-- * Definition of the relation
R-code : Rel Code Code
R-code c₁ c₂ = c₁  c₂

R-env      : ClosHeap  Rel CES.Env CESH.Env

R-closure  :  ClosHeap  Rel CES.Closure CESH.Closure
R-closure h (c₁ , e₁) (c₂ , e₂) = R-code c₁ c₂ × R-env h e₁ e₂

lookup-clptr :  ClosHeap  ClosPtr 
                (CESH.Closure  Set)  Set
lookup-clptr h ptr P =  λ c  h ! ptr  just c × P c

lookup-clptr-fmap :  h ptr {P Q}  (∀ {c}  P c  Q c)  lookup-clptr h ptr P  lookup-clptr h ptr Q
lookup-clptr-fmap hs ptr f (c , lucl , Pcs) = c , lucl , f Pcs

R-val : ClosHeap  Rel CES.Value CESH.Value
R-val h (nat n₁)   (nat n₂)    = n₁  n₂
R-val h (nat _)    (clos _)    = 
R-val h (clos _)   (nat _)     = 
R-val h (clos c₁)  (clos ptr)  =  λ c₂ 
  h ! ptr  just c₂ × R-closure h c₁ c₂

R-env h []         []         = 
R-env h []         (x₂  e₂)  = 
R-env h (x₁  e₁)  []         = 
R-env h (x₁  e₁)  (x₂  e₂)  = R-val h x₁ x₂ × R-env h e₁ e₂

R-stackelem :  ClosHeap  Rel CES.StackElem CESH.StackElem
R-stackelem h (val v₁)   (val v₂)   = R-val h v₁ v₂
R-stackelem h (val _)    (cont _)   = 
R-stackelem h (cont _)   (val _)    = 
R-stackelem h (cont c₁)  (cont c₂)  = R-closure h c₁ c₂

R-stack : ClosHeap  Rel CES.Stack CESH.Stack
R-stack h []          []          = 
R-stack h []          (x₂  s₂)   = 
R-stack h (x₁  s₁)   []          = 
R-stack h (x₁  s₁)   (x₂  s₂)  = R-stackelem h x₁ x₂ × R-stack h s₁ s₂

R-config : Rel CES.Config CESH.Config
R-config (c₁ , e₁ , s₁) (c₂ , e₂ , s₂ , h₂) =
  R-code c₁ c₂ × R-env h₂ e₁ e₂ × R-stack h₂ s₁ s₂

-- * The relation is preserved when updating the heap
module HeapUpdate (h h' : ClosHeap)(h⊆h' : h  h') where
  lu-clptr :  ptr {P}  lookup-clptr h ptr P  lookup-clptr h' ptr P
  lu-clptr ptr ((c , e) , h!ptr≡c,e , p) = (c , e) , h⊆h' ptr h!ptr≡c,e , p

  env :  e he  R-env h e he  R-env h' e he

  closure :  cl hcl  R-closure h cl hcl  R-closure h' cl hcl
  closure (c₁ , e₁) (c₂ , e₂) (Rc₁c₂ , Re₁e₂) = Rc₁c₂ , env e₁ e₂ Re₁e₂

  value :  v hv  R-val h v hv  R-val h' v hv
  value (nat n₁) (nat n₂) Rvhv = Rvhv
  value (nat _) (clos _) ()
  value (clos _) (nat _) ()
  value (clos cl) (clos ptr) Rvhv = lookup-clptr-fmap h' ptr (closure cl _) (lu-clptr ptr Rvhv)

  env [] [] Rehe = tt
  env [] (hv  he) ()
  env (v  e) [] ()
  env (v  e) (hv  he) (Rvhv , Rehe) = value v hv Rvhv , env e he Rehe

  stackelem :  e he  R-stackelem h e he  R-stackelem h' e he
  stackelem (val v) (val hv) Rehe = value v hv Rehe
  stackelem (val _) (cont _) ()
  stackelem (cont _) (val _) ()
  stackelem (cont cl) (cont hcl) Rehe = closure cl hcl Rehe

  stack :  s hs  R-stack h s hs  R-stack h' s hs
  stack [] [] tt = tt
  stack [] (x  hs) ()
  stack (x  s) [] ()
  stack (x  s) (hx  hs) (Rxhx , Rshs) = stackelem x hx Rxhx , stack s hs Rshs

  config :  cfg c e s   R-config cfg (c , e , s , h)  R-config cfg (c , e , s , h')
  config (c , e , s) hc he hs (Rchc , Rehe , Rshs) = Rchc , env e he Rehe , stack s hs Rshs

lookup-var :  {h v} e e' x  R-env h e e'  lookup x e  just v   λ v'  lookup x e'  just v' × R-val h v v'
lookup-var [] e' zero Ree' ()
lookup-var (v  e) [] zero () look
lookup-var (v  e) (v'  e') zero (Rvv' , _) refl = v' , refl , Rvv'
lookup-var [] e' (suc x) Ree' ()
lookup-var (v  e) [] (suc _) () look
lookup-var (_  e) (_  e') (suc x) Ree' look = lookup-var e e' x (proj₂ Ree') look

-- | The proof.
simulation : Simulation _⟶CES_ _⟶CESH_ R-config
simulation (VAR n SEQ c , e , s)
           .(c , e , val v  s)
           (.(VAR n SEQ c) , he , hs , h)
           (VAR {v = v} x)
           (refl , Rehe , Rshs)
  = let
      (hv , y , Rvhv) = lookup-var e he n Rehe x
     in (c , he , val hv  hs , h)
       , VAR y
       , refl , Rehe , Rvhv , Rshs
simulation (CLOSURE c' SEQ c , e , s)
           .(c , e , val (clos (c' , e))  s)
           (.(CLOSURE c' SEQ c) , he , hs , h)
           CLOSURE
           (refl , Rehe , Rshs)
  = let
      (h' , ptr) = h  (c' , he)
      h⊆h' : h  h'
      h⊆h'  = h⊆h▸x h
      Rehe'  = HeapUpdate.env h h' h⊆h' e he Rehe
      Rshs'  = HeapUpdate.stack h h' h⊆h' s hs Rshs
      Rclptr : R-stackelem h' (val (clos (c' , e))) (val (clos ptr))
      Rclptr = (c' , he) , !-▸ h (c' , he) , refl , Rehe'
     in (c , he , val (clos ptr)  hs , h')
       , CLOSURE
       , (refl , Rehe' , Rclptr , Rshs')
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , [] , h)
           APPLY
           (refl , Rehe , ())
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , cont _  hs , h)
           APPLY
           (refl , Rehe , () , Rshs)
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , val hv  [] , h)
           APPLY
           (refl , Rehe , Rvhv , ())
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , val hv  cont _  hs , h)
           APPLY
           (refl , Rehe , Rvhv , () , Rshs)
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , val hv  val (nat _)  hs , h)
           APPLY
           (refl , Rehe , Rvhv , () , Rshs)
simulation (APPLY SEQ c , e , val v  val (clos (c' , e'))  s)
           .(c' , v  e' , cont (c , e)  s)
           (.(APPLY SEQ c) , he , val hv  val (clos ptr)  hs , h)
           APPLY
           (refl , Rehe , Rvhv , ((.c' , he') , h!ptr≡c',e₁ , refl , Re'he') , Rshs)
  = (c' , hv  he' , cont (c , he)  hs , h)
  , APPLY h!ptr≡c',e₁
  , refl , (Rvhv , Re'he') , (refl , Rehe) , Rshs
simulation (RETURN , e , val v  cont (c , e')  s)
           .(c , e' , val v  s)
           (.RETURN , he , [] , h)
           RETURN (refl , Rehe , ())
simulation (RETURN , e , val v  cont (c , e')  s)
           .(c , e' , val v  s)
           (.RETURN , he , cont _  hs , h)
           RETURN (refl , Rehe , () , Rshs)
simulation (RETURN , e , val v  cont (c , e')  s)
           .(c , e' , val v  s)
           (.RETURN , he , val hv  [] , h)
           RETURN (refl , Rehe , Rvhv , ())
simulation (RETURN , e , val v  cont (c , e')  s)
           .(c , e' , val v  s)
           (.RETURN , he , val hv  val _  hs , h)
           RETURN (refl , Rehe , Rvhv , () , Rshs)
simulation (RETURN , e , val v  cont (c , e')  s)
           .(c , e' , val v  s)
           (.RETURN , he , val hv  cont (hc , he')  hs , h)
           RETURN
           (refl , Rehe , Rvhv , (Rchc , Re'he') , Rshs)
  = (hc , he' , val hv  hs , h)
  , RETURN
  , Rchc , Re'he' , Rvhv , Rshs
simulation (LIT l SEQ c , e , s)
           .(c , e , val (nat l)  s)
           (.(LIT l SEQ c) , he , hs , h)
           LIT
           (refl , Rehe , Rshs)
   = (c , he , val (nat l)  hs , h)
   , LIT
   , refl , Rehe , refl , Rshs
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , [] , h)
           PRIMOP
           (refl , Rehe , ())
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , cont _  hs , h)
           PRIMOP
           (refl , Rehe , () , Rshs)
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , val (clos _)  hs , h)
           PRIMOP
           (refl , Rehe , () , Rshs)
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , val (nat .l₁)  [] , h)
           PRIMOP
           (refl , Rehe , refl , ())
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , val (nat .l₁)  cont _  hs , h)
           PRIMOP
           (refl , Rehe , refl , () , Rshs)
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , val (nat .l₁)  val (clos _)  hs , h)
           PRIMOP
           (refl , Rehe , refl , () , Rshs)
simulation (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
           .(c , e , val (nat (f l₁ l₂))  s)
           (.(PRIMOP f SEQ c) , he , val (nat .l₁)  val (nat .l₂)  hs , h)
           PRIMOP
           (refl , Rehe , refl , refl , Rshs)
  = (c , he , val (nat (f l₁ l₂))  hs , h)
  , PRIMOP
  , refl , Rehe , refl , Rshs
simulation (COND c c' , e , val (nat 0)  s)
           .(c , e , s)
           (.(COND c c') , he , [] , h)
           COND-0
           (refl , Rehe , ())
simulation (COND c c' , e , val (nat 0)  s)
           .(c , e , s)
           (.(COND c c') , he , cont _  hs , h)
           COND-0
           (refl , Rehe , () , Rshs)
simulation (COND c c' , e , val (nat 0)  s)
           .(c , e , s)
           (.(COND c c') , he , val (clos _)  hs , h)
           COND-0
           (refl , Rehe , () , Rshs)
simulation (COND c c' , e , val (nat 0)  s)
           .(c , e , s)
           (.(COND c c') , he , val (nat .0)  hs , h)
           COND-0
           (refl , Rehe , refl , Rshs)
  = (c , he , hs , h)
  , COND-0
  , refl , Rehe , Rshs
simulation (COND c c' , e , val (nat (suc n))  s)
           .(c' , e , s)
           (.(COND c c') , he , [] , h)
           COND-suc
           (refl , Rehe , ())
simulation (COND c c' , e , val (nat (suc n))  s)
           .(c' , e , s)
           (.(COND c c') , he , cont _  hs , h)
           COND-suc
           (refl , Rehe , () , Rshs)
simulation (COND c c' , e , val (nat (suc n))  s)
           .(c' , e , s)
           (.(COND c c') , he , val (clos _)  hs , h)
           COND-suc
           (refl , Rehe , () , Rshs)
simulation (COND c c' , e , val (nat (suc n))  s)
           .(c' , e , s)
           (.(COND c c') , he , val (nat .(suc n))  hs , h)
           COND-suc
           (refl , Rehe , refl , Rshs)
  = (c' , he , hs , h)
  , COND-suc
  , refl , Rehe , Rshs
simulation .(REMOTE c' i SEQ c , e , s)
           .(c' , [] , cont (c , e)  s)
           (.(REMOTE c' i SEQ c) , he , hs , h)
           (REMOTE {c'} {i} {c} {e} {s})
           (refl , Rehe , Rshs)
  = (c' , [] , cont (c , he)  hs , h)
  , REMOTE
  , refl , tt , (refl , Rehe) , Rshs