module Krivine (Node : Set) where
open import GeneralLemmas
open import Lambda Node
open import Relation
mutual
Closure = Term × Env
data EnvElem : Set where
clos : Closure → EnvElem
Env = List EnvElem
data StackElem : Set where
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)