module Krivine (Node : Set) where
open import GeneralLemmas

open import Lambda Node
open import Relation

mutual
  Closure = Term × Env     -- lambda term x environment
  data EnvElem : Set where   -- environment element (avoid circularity)
    clos : Closure  EnvElem
  Env      = List EnvElem

data StackElem : Set where  -- continuation stack
  arg : Closure             StackElem
  if0 : Closure  Closure   StackElem
  op₂ : (    )  Closure  StackElem
  op₁ : (  )  StackElem

Stack = List StackElem

Config = Term × Env × Stack

data _⟶Krivine_ : Rel Config Config where
  POPARG   :  {t e c s}  (ƛ t , e , arg c  s) ⟶Krivine (t , clos c  e , s)
  PUSHARG  :  {t t' e s}  ((t $ t') , e , s) ⟶Krivine (t , e , arg (t' , e)  s)
  VAR      :  {n e t e' s}  lookup n e  just (clos (t , e'))  (var n , e , s) ⟶Krivine (t , e' , s)
  COND     :  {b t f e s}  (if0 b then t else f , e , s) ⟶Krivine (b , e , if0 (t , e) (f , e)  s)
  COND-0   :  {e t e' f s}  (lit 0 , e , if0 (t , e') f  s) ⟶Krivine (t , e' , s)
  COND-suc :  {n e t f e' s}  (lit (suc n) , e , if0 t (f , e')  s) ⟶Krivine (f , e' , s)

  OP       :  {f t t' e s}  (op f t t' , e , s) ⟶Krivine (t , e , op₂ f (t' , e)  s)
  OP₂      :  {n e f t e' s}   (lit n , e , op₂ f (t , e')  s) ⟶Krivine (t , e' , op₁ (f n)  s)
  OP₁      :  {n e f s}  (lit n , e , op₁ f  s) ⟶Krivine (lit (f n) , [] , s)

  REMOTE   :  {t i e s}  (t at i , e , s) ⟶Krivine (t , [] , s) -- degenerate; t is closed; empty the environment