import TsmLean.Core.Syntax

namespace TsmLean.Core

/-! # Small-step operational semantics for TSM.

State = `(Code, PC, Stack)`. The stack is `List Value` (top-of-stack at
the head). Step is a *function* `State → Option State`:
  * `some s'` : the next state.
  * `none`    : halted, OOB, or stuck (type error).

Compare with TGC/TOC's big-step `Env → Term → Value → Env → Prop`:
TSM uses small-step because instructions are atomic. The reflexive-
transitive closure (`MultiStep`) is the analogue of big-step. -/

structure State where
  code  : Code
  pc    : Nat
  stack : List Value
  deriving Repr, Inhabited

def step (s : State) : Option State :=
  if h : s.pc < s.code.size then
    match s.code[s.pc] with
    | .push n  => some { s with pc := s.pc + 1, stack := .vInt n  :: s.stack }
    | .pushB b => some { s with pc := s.pc + 1, stack := .vBool b :: s.stack }
    | .pop =>
        match s.stack with
        | _ :: rest => some { s with pc := s.pc + 1, stack := rest }
        | []        => none
    | .dup =>
        match s.stack with
        | v :: rest => some { s with pc := s.pc + 1, stack := v :: v :: rest }
        | []        => none
    | .swap =>
        match s.stack with
        | a :: b :: rest => some { s with pc := s.pc + 1, stack := b :: a :: rest }
        | _              => none
    | .add =>
        match s.stack with
        | .vInt a :: .vInt b :: rest =>
            some { s with pc := s.pc + 1, stack := .vInt (b + a) :: rest }
        | _ => none
    | .sub =>
        match s.stack with
        | .vInt a :: .vInt b :: rest =>
            some { s with pc := s.pc + 1, stack := .vInt (b - a) :: rest }
        | _ => none
    | .mul =>
        match s.stack with
        | .vInt a :: .vInt b :: rest =>
            some { s with pc := s.pc + 1, stack := .vInt (b * a) :: rest }
        | _ => none
    | .eq =>
        match s.stack with
        | .vInt a :: .vInt b :: rest =>
            some { s with pc := s.pc + 1, stack := .vBool (b == a) :: rest }
        | _ => none
    | .lt =>
        match s.stack with
        | .vInt a :: .vInt b :: rest =>
            some { s with pc := s.pc + 1, stack := .vBool (b < a) :: rest }
        | _ => none
    | .jmp k => some { s with pc := k }
    | .jmpFalse k =>
        match s.stack with
        | .vBool false :: rest => some { s with pc := k,         stack := rest }
        | .vBool true  :: rest => some { s with pc := s.pc + 1,  stack := rest }
        | _                    => none
    | .halt => none
  else none

/-- Reflexive-transitive closure of `step`. -/
inductive MultiStep : State → State → Prop where
  | refl (s : State) : MultiStep s s
  | cons {s s' s'' : State}
         (h₁ : step s = some s') (h₂ : MultiStep s' s'') :
      MultiStep s s''

end TsmLean.Core