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)