module CESH.Presimulation (Node : Set) where

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

lookup-var' :  {h v} e he x  R-env h e he  lookup x he  just v   λ v'  lookup x e  just v'
lookup-var' e [] zero Rede ()
lookup-var' [] (x  de) zero () lu
lookup-var' (x  e) (x₁  de) zero Rede lu = x , refl
lookup-var' e [] (suc x) Rede ()
lookup-var' [] (x  de) (suc x₁) () lu
lookup-var' (x  e) (x₁  de) (suc x₂) Rede lu = lookup-var' e de x₂ (proj₂ Rede) lu

presimulation : Presimulation  _⟶CESH_ _⟶CES_
                               (R-config ⁻¹)
presimulation (VAR n SEQ c , he , hs , h)
              .(c , he , val v  hs , h)
              (.(VAR n SEQ c) , e , s)
              (VAR {v = v} x)
              (refl , Rehe , Rshs)
   = let
       (v' , lu) = lookup-var' e he n Rehe x
      in (c , e , val v'  s)
       , VAR lu
presimulation (CLOSURE c' SEQ c , he , hs , h)
              .(c , he , val (clos (proj₂ (h  (c' , he))))  hs , proj₁ (h  (c' , he)))
              (.(CLOSURE c' SEQ c) , e , s)
              CLOSURE
              (refl , Rehe , Rshs)
  = (c , e , val (clos (c' , e))  s)
  , CLOSURE
presimulation (APPLY SEQ c , he , val v  val (clos clptr)  hs , h)
              .(c' , v  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , [])
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , ())
presimulation (APPLY SEQ c , he , val v  val (clos clptr)  hs , h)
              .(c' , v  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , cont _  s)
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , () , Rshs)
presimulation (APPLY SEQ c , he , val hv  val (clos clptr)  hs , h)
              .(c' , hv  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , val v  [])
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , Rvhv , ())
presimulation (APPLY SEQ c , he , val hv  val (clos clptr)  hs , h)
              .(c' , hv  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , val v  cont _  s)
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , Rvhv , () , Rshs)
presimulation (APPLY SEQ c , he , val hv  val (clos clptr)  hs , h)
              .(c' , hv  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , val v  val (nat _)  s)
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , Rvhv , () , Rshs)
presimulation (APPLY SEQ c , he , val hv  val (clos clptr)  hs , h)
              .(c' , hv  he' , cont (c , he)  hs , h)
              (.(APPLY SEQ c) , e , val v  val (clos (c'' , e'))  s)
              (APPLY {c' = c'} {e' = he'} x)
              (refl , Rehe , Rvhv , Rclclptr , Rshs)
  = (c'' , v  e' , cont (c , e)  s)
  , APPLY
presimulation (RETURN , he , (val hv  cont (c , he')  hs) , h)
              .(c , he' , val hv  hs , h)
              (.RETURN , e , [])
              RETURN
              (refl , Rehe , ())
presimulation (RETURN , he , (val hv  cont (c , he')  hs) , h)
              .(c , he' , val hv  hs , h)
              (.RETURN , e , cont _  s)
              RETURN
              (refl , Rehe , () , Rshs)
presimulation (RETURN , he , (val hv  cont (c , he')  hs) , h)
              .(c , he' , val hv  hs , h)
              (.RETURN , e , val v  [])
              RETURN
              (refl , Rehe , Rvhv , ())
presimulation (RETURN , he , (val hv  cont (c , he')  hs) , h)
              .(c , he' , val hv  hs , h)
              (.RETURN , e , val v  val _  s)
              RETURN
              (refl , Rehe , Rvhv , () , Rshs)
presimulation (RETURN , he , (val hv  cont (c , he')  hs) , h)
              .(c , he' , val hv  hs , h)
              (.RETURN , e , val v  cont (.c , e')  s)
              RETURN
              (refl , Rehe , Rvhv , (refl , Re'he') , Rshs)
  = (c , e' , val v  s)
  , RETURN
presimulation ((LIT l SEQ c) , he , hs , h)
              .(c , he , val (nat l)  hs , h)
              (.(LIT l SEQ c) , e , s)
              LIT
              (refl , Rehe , Rshs)
  = (c , e , val (nat l)  s)
  , LIT
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , [])
              PRIMOP
              (refl , Rehe , ())
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , cont _  s)
              PRIMOP
              (refl , Rehe , () , Rshs)
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , val (clos _)  s)
              PRIMOP
              (refl , Rehe , () , Rshs)
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , val (nat .l₁)  [])
              PRIMOP
              (refl , Rehe , refl , ())
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , val (nat .l₁)  cont _  s)
              PRIMOP
              (refl , Rehe , refl , () , Rshs)
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , val (nat .l₁)  val (clos _)  s)
              PRIMOP
              (refl , Rehe , refl , () , Rshs)
presimulation (PRIMOP f SEQ c , he , val (nat l₁)  val (nat l₂)  hs , h)
              .(c , he , val (nat (f l₁ l₂))  hs , h)
              (.(PRIMOP f SEQ c) , e , val (nat .l₁)  val (nat .l₂)  s)
              PRIMOP
              (refl , Rehe , refl , refl , Rshs)
  = (c , e , val (nat (f l₁ l₂))  s)
  , PRIMOP
presimulation (COND c c' , he , val (nat 0)  hs , h)
              .(c , he , hs , h)
              (.(COND c c') , e , [])
              COND-0
              (refl , Rehe , ())
presimulation (COND c c' , he , val (nat 0)  hs , h)
              .(c , he , hs , h)
              (.(COND c c') , e , cont _  s)
              COND-0
              (refl , Rehe , () , Rshs)
presimulation (COND c c' , he , val (nat 0)  hs , h)
              .(c , he , hs , h)
              (.(COND c c') , e , val (clos _)  s)
              COND-0
              (refl , Rehe , () , Rshs)
presimulation (COND c c' , he , val (nat 0)  hs , h)
              .(c , he , hs , h)
              (.(COND c c') , e , val (nat .0)  s)
              COND-0
              (refl , Rehe , refl , Rshs)
  = (c , e , s)
  , COND-0
presimulation (COND c c' , he , val (nat (suc n))  hs , h)
              .(c' , he , hs , h)
              (.(COND c c') , e , [])
              COND-suc
              (refl , Rehe , ())
presimulation (COND c c' , he , val (nat (suc n))  hs , h)
              .(c' , he , hs , h)
              (.(COND c c') , e , cont _  s)
              COND-suc
              (refl , Rehe , () , Rshs)
presimulation (COND c c' , he , val (nat (suc n))  hs , h)
              .(c' , he , hs , h)
              (.(COND c c') , e , val (clos _)  s)
              COND-suc
              (refl , Rehe , () , Rshs)
presimulation (COND c c' , he , val (nat (suc n))  hs , h)
              .(c' , he , hs , h)
              (.(COND c c') , e , val (nat .(suc n))  s)
              COND-suc
              (refl , Rehe , refl , Rshs)
  = (c' , e , s)
  , COND-suc
presimulation (.(REMOTE c' i SEQ c) , he , hs , h)
              .(c' , [] , cont (c , he)  hs , h)
              (.(REMOTE c' i SEQ c) , e , s)
              (REMOTE {c'} {i} {c})
              (refl , Rehe , Rshs)
  = (c' , [] , cont (c , e)  s)
  , REMOTE