Library OracleLanguages.Imp.SmallStep

Require Import Common.
Require Import Imp.Syntax.
Require Import List.
Import ListNotations.

Module Imp (Var_as_DT : UsualDecidableTypeOrig).
  Module Syntax := Imp.Syntax.Imp Var_as_DT.
  Export Syntax.

  Definition cont := list cmd.
  Definition state := prod cont store.

  Definition state_eq (S₁ S₂ : state) : Prop :=
    let '(k₁, s₁) := S₁ in
    let '(k₂, s₂) := S₂ in
    k₁ = k₂ ∧ M.Equal s₁ s₂.

  Lemma state_eq_dec:
    ∀ S₁ S₂, {state_eq S₁ S₂} + {¬ state_eq S₁ S₂}.

  Definition beq_state (S₁ S₂ : state) :=
    if state_eq_dec S₁ S₂ then true else false.

  Lemma state_eq_sym:
    ∀ S₁ S₂,
    state_eq S₁ S₂ → state_eq S₂ S₁.

  Lemma state_eq_refl:
    ∀ S,
    state_eq S S.

  Lemma state_eq_trans:
    ∀ S₁ S₂ S₃,
    state_eq S₁ S₂ →
    state_eq S₂ S₃ →
    state_eq S₁ S₃.

  Definition state_final (S : state) :=
    match S with
      | ([], _) ⇒ Some tt
      | _ ⇒ None
    end.

  Lemma state_final_eq:
    ∀ S S',
      state_eq S S' →
      state_final S = state_final S'.

  Definition step (_ : unit) (S : state) : option state :=
    let '(k, s) := S in
    match k with
    | [] ⇒ None
    | Skip::k' ⇒ ret (k', s)
    | (Seq c₁ c₂)::k' ⇒ ret (c₁::c₂::k', s)
    | (Assign x e)::k' ⇒ eval_exp s e >>= λ v,
      ret (k', M.add x v s)
    | (ITE b c₁ c₂)::k' ⇒ eval_bexp s b >>= λ v,
      ret ((if v then c₁ else c₂)::k', s)
    | (While b c')::k' ⇒ eval_bexp s b >>= λ v,
      ret (if v then (c'::(While b c')::k', s) else (k', s))
    | (Assert b)::k' ⇒
      eval_bexp s b >>= λ v,
      if v then ret (k', s)
      else None
    end.

  Lemma step_app:
    ∀ k k' k₂ s s', step tt (k, s) = Some (k', s') →
    step tt (k ++ k₂, s) = Some (k' ++ k₂, s').

  Lemma step_eq:
    ∀ genv₁ genv₂ S₁ S₂ S₁' S₂',
      genv₁ = genv₂ →
      state_eq S₁ S₂ →
      step genv₁ S₁ = Some S₁' →
      step genv₂ S₂ = Some S₂' →
      state_eq S₁' S₂'.

  Lemma step_eq':
    ∀ genv₁ genv₂ S₁ S₂,
      genv₁ = genv₂ →
      state_eq S₁ S₂ →
      step genv₁ S₁ = None ↔ step genv₂ S₂ = None.

  Inductive finite_small_step_exec s : state → Prop :=
    | Halted : finite_small_step_exec s ([], s)
    | Step : ∀ S S',
      step tt S = Some S' →
      finite_small_step_exec s S' →
      finite_small_step_exec s S.

  Hint Constructors finite_small_step_exec.

  CoInductive infinite_small_step_exec : state → Prop :=
    | InfStep : ∀ S S',
      step tt S = Some S' →
      infinite_small_step_exec S' →
      infinite_small_step_exec S.
End Imp.