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_
_↓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↑