module CES.Properties (Node : Set) where
open import GeneralLemmas

open import MachineCode Node
open import CES Node
open import Relation

determinism-CES : _⟶CES_ is-deterministic
determinism-CES (VAR x) (VAR y)
  = cong  v  _ , _ , val v  _) (just-inj (trans (sym x) y))
determinism-CES CLOSURE  CLOSURE   = refl
determinism-CES APPLY    APPLY     = refl
determinism-CES RETURN   RETURN    = refl
determinism-CES REMOTE   REMOTE    = refl
determinism-CES LIT      LIT       = refl
determinism-CES PRIMOP   PRIMOP    = refl
determinism-CES COND-0   COND-0    = refl
determinism-CES COND-suc COND-suc  = refl

⟶CES-is-decidable : _⟶CES_ is-decidable
⟶CES-is-decidable (VAR n SEQ c , e , s) with lookup n e | inspect (lookup n) e
⟶CES-is-decidable (VAR n SEQ c , e , s) | just v | [ lu ] = yes ((c , e , val v  s) , VAR lu)
⟶CES-is-decidable (VAR n SEQ c , e , s) | nothing | [ lu ] = no (lemma lu)
  where lemma :  {n c e s}  lookup n e  nothing    cfg  (VAR n SEQ c , e , s) ⟶CES cfg)  
        lemma lu ((c , e , val .v  s) , VAR {v = v} lu') = nothing≠just (trans (sym lu) lu')
⟶CES-is-decidable (CLOSURE c' SEQ c , e , s) = yes ((c , e , val (clos (c' , e))  s) , CLOSURE)
⟶CES-is-decidable (APPLY SEQ c , e , []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (APPLY SEQ c , e , x  []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (APPLY SEQ c , e , val v  val (nat x)  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (APPLY SEQ c , e , val v  val (clos (c' , e'))  s) = yes ((c' , v  e' , cont (c , e)  s) , APPLY)
⟶CES-is-decidable (APPLY SEQ c , e , val v  cont c'  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (APPLY SEQ c , e , cont c'  val v  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (APPLY SEQ c , e , cont c'  cont c''  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (REMOTE c' i SEQ c , e , s) = yes ((c' , [] , cont (c , e)  s) , REMOTE)
⟶CES-is-decidable (END , e , s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (RETURN , e , []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (RETURN , e , x  []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (RETURN , e , val v  val v'  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (RETURN , e , val v  cont (c , e')  s) = yes ((c , e' , val v  s) , RETURN)
⟶CES-is-decidable (RETURN , e , cont c  val v  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (RETURN , e , cont c  cont c'  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (LIT l SEQ c , e , s) = yes ((c , e , val (nat l)  s) , LIT)
⟶CES-is-decidable (PRIMOP f SEQ c , e , []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , cont x  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , val (clos cl)  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , val (nat l₁)  []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , val (nat l₁)  cont x  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , val (nat l₁)  val (clos cl)  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (PRIMOP f SEQ c , e , val (nat l₁)  val (nat l₂)  s)
  = yes ((c , e , val (nat (f l₁ l₂))  s) , PRIMOP)
⟶CES-is-decidable (COND c c' , e , []) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (COND c c' , e , cont _  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (COND c c' , e , val (clos _)  s) = no lemma
  where lemma :   cfg  _ ⟶CES cfg)  
        lemma (cfg , ())
⟶CES-is-decidable (COND c c' , e , val (nat 0)  s) = yes ((c , e , s) , COND-0)
⟶CES-is-decidable (COND c c' , e , val (nat (suc n))  s) = yes ((c' , e , s) , COND-suc)
_⟶CES*_ = _⟶CES_ *

infix 5 _↓CES_

-- * Termination and divergence
_↓CES_ : Config  Value  Set
cfg ↓CES v = cfg ⟶CES* (END , [] , val v  [])

_↓CES : Config  Set
cfg ↓CES =  λ v  cfg ↓CES v

_↑CES : Config  Set
_↑CES =  _⟶CES_

convergent-cfg-doesn't-diverge :  cfg  cfg ↓CES  ¬ (cfg ↑CES)
convergent-cfg-doesn't-diverge cfg (v , cfg⟶*v) cfg↑ = lemma (cfg↑ (END , [] , val v  []) cfg⟶*v)
  where
    lemma :  {v}  ¬ ( λ cfg  (END , [] , val v  []) ⟶CES cfg)
    lemma (cfg , ())

divergent-cfg-doesn't-converge :  cfg  cfg ↑CES  ¬ (cfg ↓CES)
divergent-cfg-doesn't-converge cfg cfg↑ cfg↓ = convergent-cfg-doesn't-diverge cfg cfg↓ cfg↑