Library OracleLanguages.Imp.BigStep

Require Import Common.
Require Import Imp.Lang.
Require Import ProgrammingLanguage.

Module Type ImpBigStep
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT).

  Reserved Notation "S ⊢ c ⇓ S'" (at level 50, no associativity).
  Inductive big_step : store → cmd → store → Prop :=
    | j_skip: ∀ {s},
      s ⊢ Skip ⇓ s
    | j_seq: ∀ {s₀ s₂ c₁ c₂} (s₁ : store),
      s₀ ⊢ c₁ ⇓ s₁ →
      s₁ ⊢ c₂ ⇓ s₂ →
      s₀ ⊢ (Seq c₁ c₂) ⇓ s₂
    | j_assign: ∀ {s s' x e} v,
      eval_exp s e = Some v →
      M.add x v s = s' →
      s ⊢ (Assign x e) ⇓ s'
    | j_if_then: ∀ {s s' b c₁ c₂},
      eval_bexp s b = Some true →
      s ⊢ c₁ ⇓ s' →
      s ⊢ ITE b c₁ c₂ ⇓ s'
    | j_if_else: ∀ {s s' b c₁ c₂},
      eval_bexp s b = Some false →
      s ⊢ c₂ ⇓ s' →
      s ⊢ ITE b c₁ c₂ ⇓ s'
    | j_while_iter: ∀ {s s' b c} s₁,
      eval_bexp s b = Some true →
      s ⊢ c ⇓ s₁ →
      s₁ ⊢ While b c ⇓ s' →
      s ⊢ While b c ⇓ s'
    | j_while_end: ∀ {s b c},
      eval_bexp s b = Some false →
      s ⊢ While b c ⇓ s
    | j_assert_true: ∀ {s b},
      eval_bexp s b = Some true →
      s ⊢ Assert b ⇓ s
  where "S ⊢ c ⇓ S'" := (big_step S c S').

  Hint Constructors big_step.

  Reserved Notation "S ⊢ c ⇒ '∞'" (at level 50, no associativity).
  Inductive big_step_div : store → cmd → Prop :=
    | j_seq₁: ∀ {s₀ c₁ c₂},
      s₀ ⊢ c₁ ⇒ ∞ →
      s₀ ⊢ (Seq c₁ c₂) ⇒ ∞
    | j_seq₂: ∀ {s₀ c₁ c₂} (s₁ : store),
      s₀ ⊢ c₁ ⇓ s₁ →
      s₁ ⊢ c₂ ⇒ ∞ →
      s₀ ⊢ (Seq c₁ c₂) ⇒ ∞
    | j_if_then_inf: ∀ {s b c₁ c₂},
      eval_bexp s b = Some true →
      s ⊢ c₁ ⇒ ∞ →
      s ⊢ ITE b c₁ c₂ ⇒ ∞
    | j_if_else_inf: ∀ {s b c₁ c₂},
      eval_bexp s b = Some false →
      s ⊢ c₂ ⇒ ∞ →
      s ⊢ ITE b c₁ c₂ ⇒ ∞
    | j_while₁: ∀ {s b c},
      eval_bexp s b = Some true →
      s ⊢ c ⇒ ∞ →
      s ⊢ While b c ⇒ ∞
    | j_while₂: ∀ {s b c} s₁,
      eval_bexp s b = Some true →
      s ⊢ c ⇓ s₁ →
      s₁ ⊢ While b c ⇒ ∞ →
      s ⊢ While b c ⇒ ∞
  where "S ⊢ c ⇒ '∞'" := (big_step_div S c).

  Hint Constructors big_step_div.

  Theorem big_implies_small:
    ∀ c s s',
    s ⊢ c ⇓ s' →
    ∃ n, @nsteps imp_language tt n ([c], s) = Some ([], s').

  Lemma seq_assoc:
    ∀ s c₁ c₂ c₃ s',
    s ⊢ Seq (Seq c₁ c₂) c₃ ⇓ s' ↔
    s ⊢ Seq c₁ (Seq c₂ c₃) ⇓ s'.

  Inductive big_step_cont (S : store) : store → cont → Prop :=
    | Halted :
      big_step_cont S S []
    | OneBigStep : ∀ s c s' k,
      s ⊢ c ⇓ s' →
      big_step_cont S s' k →
      big_step_cont S s (c::k).

  Inductive big_step_cont_div : store → cont → Prop :=
    | Diverges : ∀ s c k,
      s ⊢ c ⇒ ∞ →
      big_step_cont_div s (c::k)
    | OneBigStep' : ∀ s c s' k,
      s ⊢ c ⇓ s' →
      big_step_cont_div s' k →
      big_step_cont_div s (c::k).

  Hint Constructors big_step_cont.
  Hint Constructors big_step_cont_div.

  Theorem big_step_determinist:
    ∀ c s s' s'',
    s ⊢ c ⇓ s' →
    s ⊢ c ⇓ s'' →
    s' = s''.

  Theorem big_div_implies_small_div_helper:
    ∀ c s,
    s ⊢ c ⇒ ∞ →
    ∃ c' k' s', step tt ([c], s) = Some (c'::k', s') ∧ big_step_cont_div s' (c'::k').

  Theorem big_implies_small_helper:
    ∀ c s s'',
    s ⊢ c ⇓ s'' →
    ∃ k' s', step tt ([c], s) = Some (k', s') ∧ big_step_cont s'' s' k'.

  Theorem big_div_implies_small_div_helper':
    ∀ k s,
    big_step_cont_div s k →
    ∃ c' k' s', step tt (k, s) = Some (c'::k', s') ∧ big_step_cont_div s' (c'::k').
  Theorem big_cont_div_implies_small_div:
    ∀ k s,
    big_step_cont_div s k →
    infinite_small_step_exec (k, s).

  Theorem big_div_implies_small_div:
    ∀ c s,
    s ⊢ c ⇒ ∞ →
    infinite_small_step_exec ([c], s).

  Lemma small_implies_big_helper:
    ∀ S s',
    finite_small_step_exec s' S →
    big_step_cont s' (snd S) (fst S).

  Lemma small_implies_big:
    ∀ c s s',
    (∃ n, @nsteps imp_language tt n ([c], s) = Some ([], s')) →
    s ⊢ c ⇓ s'.

  Theorem small_equiv_big:
    ∀ c s s',
    (∃ n, @nsteps imp_language tt n ([c], s) = Some ([], s')) ↔ s ⊢ c ⇓ s'.
End ImpBigStep.

Module Make (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT)
  : ImpBigStep Var_as_DT Lang.
  Include (ImpBigStep Var_as_DT Lang).
End Make.