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
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₂
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
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