module Krivine.Properties (Node : Set) where open import GeneralLemmas open import Krivine Node open import Lambda Node open import Relation clos-inj : ∀ {c₁ c₂} → clos c₁ ≡ clos c₂ → c₁ ≡ c₂ clos-inj refl = refl determinism-Krivine : _⟶Krivine_ is-deterministic determinism-Krivine POPARG POPARG = refl determinism-Krivine PUSHARG PUSHARG = refl determinism-Krivine (VAR x) (VAR y) = cong₂ (λ p q → p , q , _) (proj₁ (,-inj p)) (proj₂ (,-inj p)) where p = clos-inj (just-inj (trans (sym x) y)) determinism-Krivine COND COND = refl determinism-Krivine COND-0 COND-0 = refl determinism-Krivine COND-suc COND-suc = refl determinism-Krivine OP OP = refl determinism-Krivine OP₂ OP₂ = refl determinism-Krivine OP₁ OP₁ = refl determinism-Krivine REMOTE REMOTE = refl _⟶Krivine*_ = _⟶Krivine_ * infix 5 _↓Krivine_ _↓Krivine_ : Config → Value → Set cfg ↓Krivine v = ∃ λ env → cfg ⟶Krivine* (value v , env , []) _↓Krivine : Config → Set cfg ↓Krivine = ∃ λ v → cfg ↓Krivine v _↑Krivine : Config → Set _↑Krivine = ↑ _⟶Krivine_ decidable-lookup : ∀ n e → Dec (∃ λ c → lookup n e ≡ just (clos c)) decidable-lookup zero [] = no lem where lem : ∄ λ c → nothing ≡ just (clos c) lem (cfg' , ()) decidable-lookup zero (clos c ∷ e) = yes (c , refl) decidable-lookup (suc n) [] = no lem where lem : ∄ λ c → nothing ≡ just (clos c) lem (cfg' , ()) decidable-lookup (suc n) (_ ∷ e) = decidable-lookup n e decidable-Krivine : _⟶Krivine_ is-decidable decidable-Krivine (ƛ t , e , []) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine (ƛ t , e , arg x ∷ s) = yes ((t , clos x ∷ e , s) , POPARG) decidable-Krivine (ƛ t , e , if0 x x₁ ∷ s) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine (ƛ t , e , op₂ x x₁ ∷ s) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine (ƛ t , e , op₁ x ∷ s) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine ((t $ t') , e , s) = yes ((t , e , arg (t' , e) ∷ s) , PUSHARG) decidable-Krivine (var n , e , s) with decidable-lookup n e decidable-Krivine (var n , e , s) | yes ((t , e') , lu) = yes ((t , e' , s) , VAR lu) decidable-Krivine (var n , e , s) | no ¬p = no lem where lem : ∄ λ cfg' → (var n , e , s) ⟶Krivine cfg' lem (._ , VAR lu) = ¬p (_ , lu) decidable-Krivine (lit n , e , []) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine (lit n , e , arg x ∷ s) = no lem where lem : ∄ λ cfg' → _ ⟶Krivine cfg' lem (cfg' , ()) decidable-Krivine (lit zero , e , if0 (t₁ , e₁) (t₂ , e₂) ∷ s) = yes ((t₁ , e₁ , s) , COND-0) decidable-Krivine (lit (suc n) , e , if0 (t₁ , e₁) (t₂ , e₂) ∷ s) = yes ((t₂ , e₂ , s) , COND-suc) decidable-Krivine (lit n , e , op₂ f (t₁ , e₂) ∷ s) = yes ((t₁ , e₂ , op₁ (f n) ∷ s) , OP₂) decidable-Krivine (lit n , e , op₁ f ∷ s) = yes ((lit (f n) , [] , s) , OP₁) decidable-Krivine (op f t₁ t₂ , e , s) = yes ((t₁ , e , op₂ f (t₂ , e) ∷ s) , OP) decidable-Krivine (if0 t then t₁ else t₂ , e , s) = yes ((t , e , if0 (t₁ , e) (t₂ , e) ∷ s) , COND) decidable-Krivine (t at x , e , s) = yes ((t , [] , s) , REMOTE)