module stlc.step where

open import Data.List
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

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

Config = MakeConfig Inst MachineValue

data CAM→ : Config → Config → Set where
  unit-step : ∀ {i e s} →            CAM→ ⟨ UNIT ∷ i ∣ e ∣ s ⟩               ⟨ i ∣ ⟨⟩ ∣ s ⟩
  nat-step  : ∀ {i e s x} →          CAM→ ⟨ (NAT x) ∷ i ∣ e ∣ s ⟩            ⟨ i ∣ `nat x ∣ s ⟩
  skip-step : ∀ {i e s} →            CAM→ ⟨ SKIP ∷ i ∣ e ∣ s ⟩               ⟨ i ∣ e ∣ s ⟩
  fst-step  : ∀ {i e₁ e₂ s} →        CAM→ ⟨ FST ∷ i ∣ e₁ , e₂ ∣ s ⟩          ⟨ i ∣ e₁ ∣ s ⟩
  snd-step  : ∀ {i e₁ e₂ s} →        CAM→ ⟨ SND ∷ i ∣ e₁ , e₂ ∣ s ⟩          ⟨ i ∣ e₂ ∣ s ⟩
  push-step : ∀ {i e s} →            CAM→ ⟨ PUSH ∷ i ∣ e ∣ s ⟩               ⟨ i ∣ e ∣ e ∷ s ⟩
  swap-step : ∀ {i e₁ e₂ s} →        CAM→ ⟨ SWAP ∷ i ∣ e₁ ∣ e₂ ∷ s ⟩         ⟨ i ∣ e₂ ∣ e₁ ∷ s ⟩
  pair-step : ∀ {i e₁ e₂ s} →        CAM→ ⟨ PAIR ∷ i ∣ e₂ ∣ e₁ ∷ s ⟩         ⟨ i ∣ e₁ , e₂ ∣ s ⟩
  cur-step  : ∀ {i₁ i₂ e s} →        CAM→ ⟨ CUR i₁ ∷ i₂ ∣ e ∣ s ⟩            ⟨ i₂ ∣ cur i₁ e ∣ s ⟩
  app-step  : ∀ {i₁ i₂ e₁ e₂ s} →    CAM→ ⟨ APP ∷ i₁ ∣ cur i₂ e₁ , e₂ ∣ s ⟩  ⟨ i₂ ++ i₁ ∣ e₁ , e₂ ∣ s ⟩
--- COPRODUCT ---
  inl-step  : ∀ {i e s} →            CAM→ ⟨ INL ∷ i ∣ e ∣ s ⟩                ⟨ i ∣ L e ∣ s ⟩
  inr-step  : ∀ {i e s} →            CAM→ ⟨ INR ∷ i ∣ e ∣ s ⟩                ⟨ i ∣ R e ∣ s ⟩
  case1-step : ∀ {i₁ i₂ i e₁ e₂ s} → CAM→ ⟨ CASE i₁ i₂ ∷ i ∣ e₁ , L e₂ ∣ s ⟩ ⟨ i₁ ++ i ∣ e₁ , e₂ ∣ s ⟩
  case2-step : ∀ {i₁ i₂ i e₁ e₂ s} → CAM→ ⟨ CASE i₁ i₂ ∷ i ∣ e₁ , R e₂ ∣ s ⟩ ⟨ i₂ ++ i ∣ e₁ , e₂ ∣ s ⟩
--- LIST OBJECT ---
  nil-step  : ∀ {i e s} →            CAM→ ⟨ NIL ∷ i ∣ e ∣ s ⟩                ⟨ i ∣ [] ∣ s ⟩
  c-step    : ∀ {i h t s} →          CAM→ ⟨ C ∷ i ∣ h , t ∣ s ⟩              ⟨ i ∣ h ⦂ t ∣ s ⟩
  it1-step  : ∀ {i e s x r} →        CAM→ ⟨ IT x r ∷ i ∣ e , [] ∣ s ⟩        ⟨ x ++ i ∣ e ∣ s ⟩
  it2-step  : ∀ {i e s x r h t} →    CAM→ ⟨ IT x r ∷ i ∣ e , h ⦂ t ∣ s ⟩      ⟨ IT x r ∷ PAIR ∷ PAIR ∷ r ++ i ∣ e , t ∣ h ∷ e ∷ s ⟩

deterministicStep : ∀ {a b c : Config} →  CAM→ a b → CAM→ a c → b ≡ c
deterministicStep unit-step unit-step = refl
deterministicStep nat-step nat-step = refl
deterministicStep skip-step skip-step = refl
deterministicStep fst-step fst-step = refl
deterministicStep snd-step snd-step = refl
deterministicStep push-step push-step = refl
deterministicStep swap-step swap-step = refl
deterministicStep pair-step pair-step = refl
deterministicStep cur-step cur-step = refl
deterministicStep app-step app-step = refl
--- COPRODUCT ---
deterministicStep inl-step inl-step = refl
deterministicStep inr-step inr-step = refl
deterministicStep case1-step case1-step = refl
deterministicStep case2-step case2-step = refl
--- LIST OBJECT ---
deterministicStep nil-step nil-step = refl
deterministicStep c-step c-step = refl
deterministicStep it1-step it1-step = refl
deterministicStep it2-step it2-step = refl