module stlc.run where

open import Data.Nat
open import Data.List

open import config
open import stlc.value public
open import stlc.inst public

Config = MakeConfig Inst MachineValue

data Result : Set where
  stuck : Config → Result
  notFinished : Config → Result
  done  : MachineValue → Result

run : ℕ → Config → Result
run _ ⟨ [] ∣ env ∣ [] ⟩ = done env
run zero c = notFinished c
run (suc n) ⟨ UNIT ∷ inst ∣ e ∣ stack ⟩ = run n ⟨ inst ∣ ⟨⟩ ∣ stack ⟩
run (suc n) ⟨ NAT x ∷ inst ∣ e ∣ stack ⟩ = run n ⟨ inst ∣ `nat x ∣ stack ⟩
run (suc n) ⟨ SKIP ∷ inst ∣ env ∣ stack ⟩ = run n ⟨ inst ∣ env ∣ stack ⟩
--- PRODUCT ---
run (suc n) ⟨ FST ∷ inst ∣ env , _ ∣ stack ⟩ = run n ⟨ inst ∣ env ∣ stack ⟩
run (suc n) ⟨ SND ∷ inst ∣ _ , env ∣ stack ⟩ = run n ⟨ inst ∣ env ∣ stack ⟩
run (suc n) ⟨ PUSH ∷ inst ∣ env ∣ stack ⟩ = run n ⟨ inst ∣ env ∣ env ∷ stack ⟩
run (suc n) ⟨ SWAP ∷ inst ∣ env ∣ s ∷ stack ⟩ = run n ⟨ inst ∣ s ∣ env ∷ stack ⟩
run (suc n) ⟨ PAIR ∷ inst ∣ env ∣ s ∷ stack ⟩ = run n ⟨ inst ∣ s , env ∣ stack ⟩
--- EXPONENTIAL ---
run (suc n) ⟨ APP ∷ inst ∣ cur i s , t ∣ stack ⟩ = run n ⟨ i ++ inst ∣ s , t ∣ stack ⟩
run (suc n) ⟨ CUR i ∷ inst ∣ env ∣ stack ⟩ = run n ⟨ inst ∣ cur i env ∣ stack ⟩
--- COPRODUCT ---
run (suc n) ⟨ CASE i₁ i₂ ∷ i ∣ e₁ , L e₂ ∣ s ⟩ = run n ⟨ i₁ ++ i ∣ e₁ , e₂ ∣ s ⟩
run (suc n) ⟨ CASE i₁ i₂ ∷ i ∣ e₁ , R e₂ ∣ s ⟩ = run n ⟨ i₂ ++ i ∣ e₁ , e₂ ∣ s ⟩
run (suc n) ⟨ INL ∷ i ∣ e ∣ s ⟩ = run n ⟨ i ∣ L e ∣ s ⟩
run (suc n) ⟨ INR ∷ i ∣ e ∣ s ⟩ = run n ⟨ i ∣ R e ∣ s ⟩
--- LIST OBJECT ---
run (suc n) ⟨ NIL ∷ inst ∣ env ∣ stack ⟩ = run n ⟨ inst ∣ [] ∣ stack ⟩
run (suc n) ⟨ C ∷ inst ∣ h , t ∣ stack ⟩ = run n ⟨ inst ∣ h ⦂ t ∣ stack ⟩
run (suc n) ⟨ IT x r ∷ inst ∣ p , [] ∣ stack ⟩ = run n ⟨ x ++ inst ∣ p ∣ stack ⟩
run (suc n) ⟨ IT x r ∷ inst ∣ p , h ⦂ t ∣ stack ⟩ = run n ⟨ IT x r ∷ PAIR ∷ PAIR ∷ r ++ inst ∣ p , t ∣ h ∷ p ∷ stack ⟩
run _ c = stuck c