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