module CESH.Properties (Node : Set) where
open import GeneralLemmas hiding ([_])
open import MachineCode Node
open import Relation hiding ([_])
open import Data.List using ([_])
open import CESH Node
determinism-CESH : _⟶CESH_ is-deterministic
determinism-CESH (VAR x) (VAR y)
= cong (λ v → _ , _ , val v ∷ _ , _) (just-inj (trans (sym x) y))
determinism-CESH CLOSURE CLOSURE = refl
determinism-CESH (APPLY x) (APPLY y) = cong₂ (λ c e → c , _ ∷ e , _) c₁≡c₂ e'₁≡e'₂
where
c₁,e'₁≡c₂,e'₂ = just-inj (trans (sym x) y)
c₁≡c₂ = proj₁ (,-inj c₁,e'₁≡c₂,e'₂)
e'₁≡e'₂ = proj₂ (,-inj c₁,e'₁≡c₂,e'₂)
determinism-CESH RETURN RETURN = refl
determinism-CESH LIT LIT = refl
determinism-CESH PRIMOP PRIMOP = refl
determinism-CESH REMOTE REMOTE = refl
determinism-CESH COND-0 COND-0 = refl
determinism-CESH COND-suc COND-suc = refl
_⟶CESH*_ = _⟶CESH_ *
infix 5 _↓CESH_
_↓CESH_ : Config → Value → Set
cfg ↓CESH v = ∃ λ h → cfg ⟶CESH* (END , [] , [ val v ] , h)
_↓CESH : Config → Set
cfg ↓CESH = ∃ λ v → cfg ↓CESH v
_↑CESH : Config → Set
_↑CESH = ↑ _⟶CESH_
convergent-cfg-doesn't-diverge : ∀ cfg → cfg ↓CESH → ¬ (cfg ↑CESH)
convergent-cfg-doesn't-diverge cfg (v , h , cfg⟶*v) cfg↑ = lemma (cfg↑ (END , [] , val v ∷ [] , h) cfg⟶*v)
where
lemma : ∀ {v} → ¬ (∃ λ cfg → (END , [] , val v ∷ [] , h) ⟶CESH cfg)
lemma (cfg , ())
divergent-cfg-doesn't-converge : ∀ cfg → cfg ↑CESH → ¬ (cfg ↓CESH)
divergent-cfg-doesn't-converge cfg cfg↑ cfg↓ = convergent-cfg-doesn't-diverge cfg cfg↓ cfg↑