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_

-- | Termination and divergence
_↓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↑