/-!
# Common.Lang — cross-language abstraction.

A `BigStepLang` is a programming-language fragment with:
  * a syntactic class of terms,
  * a class of values,
  * a state type carrying everything else (env, heap, etc.),
  * a big-step relation `Eval : State → Term → Value → State → Prop`
    saying "starting in state `s`, evaluating term `t` produces value
    `v` and state `s'`",
  * a determinism property (the relation is functional in `(v, s')`).

This generalises TGC's `BigStep : Heap → Env → Term → Value → Heap`
(with State := Heap × Env) and TOC's `BigStep : Env → Term → Value →
Env` (with State := Env). TSM uses small-step semantics and fits a
different class — see `SmallStepLang`.

The point of the abstraction: theorems about *any* deterministic
big-step language are stated and proved once, and apply to all
instances. -/

namespace Common

class BigStepLang where
  Term  : Type
  Value : Type
  State : Type
  Eval  : State → Term → Value → State → Prop
  deterministic : ∀ {s : State} {t : Term} {v₁ v₂ : Value} {s₁ s₂ : State},
    Eval s t v₁ s₁ → Eval s t v₂ s₂ → v₁ = v₂ ∧ s₁ = s₂

namespace BigStepLang

variable [L : BigStepLang]

/-- Result of an evaluation, when it exists, is unique. -/
theorem unique_value
    {s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
    (h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
    v₁ = v₂ :=
  (L.deterministic h₁ h₂).1

theorem unique_state
    {s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
    (h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
    s₁ = s₂ :=
  (L.deterministic h₁ h₂).2

end BigStepLang

/-! ## SmallStepLang — small-step semantics (e.g., TSM).

A `SmallStepLang` is structurally simpler: a state type and a step
function. Determinism is automatic since `step` is a function. -/

class SmallStepLang where
  State : Type
  step  : State → Option State

namespace SmallStepLang

variable [L : SmallStepLang]

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

/-- Single-step is functional. -/
theorem step_deterministic {s s₁ s₂ : L.State}
    (h₁ : L.step s = some s₁) (h₂ : L.step s = some s₂) :
    s₁ = s₂ := by
  rw [h₁] at h₂; exact Option.some.inj h₂

end SmallStepLang

/-! ## Compilation correctness — the substrate-projection theorem.

If `Source` is a `BigStepLang`, `Target` is either kind, and `compile`
maps source specs to target specs preserving evaluation, then the
compilation pipeline inherits determinism.

This is the categorical kernel of CompCert-style theorems. -/

structure CompileCorrect
    (Source : BigStepLang)
    (Target : Type) (TargetEval : Target → Source.Value → Prop)
    (compile : Source.Term → Target) where
  /-- Compilation preserves evaluation: source `Eval` implies target
      `TargetEval` produces the same value. -/
  preservation :
    ∀ {s : Source.State} {t : Source.Term} {v : Source.Value} {s' : Source.State},
      Source.Eval s t v s' → TargetEval (compile t) v

end Common