Library OracleLanguages.Imp.Lang

Require Import Common.
Require Import Imp.SmallStep.
Require Import Imp.Syntax.

Require ProgrammingLanguage.

Module Type ImpProgrammingLanguage (Var_as_DT : UsualDecidableTypeOrig).
  Module SmallStep := SmallStep.Imp Var_as_DT.
  Export SmallStep.

  Property genv_eq_dec:
    ∀ (x y : unit), { x = y } + { x ≠ y }.

  Lemma state_final_no_step:
    ∀ genv S v,
      state_final S = Some v →
      step genv S = None.

  Definition imp_language : ProgrammingLanguage.language :=
    {|
      ProgrammingLanguage.return_type := unit;
      ProgrammingLanguage.genv_type := unit;
      ProgrammingLanguage.state := state;
      ProgrammingLanguage.step := step;
      ProgrammingLanguage.state_final := state_final;
      ProgrammingLanguage.state_final_no_step := state_final_no_step;

      
      ProgrammingLanguage.prog := cmd;
      ProgrammingLanguage.initial_state := λ c, (tt, (c::nil, M.empty Z));

      ProgrammingLanguage.genv_eq := eq;
      ProgrammingLanguage.genv_eq_refl := @eq_refl unit;
      ProgrammingLanguage.genv_eq_sym := @eq_sym unit;
      ProgrammingLanguage.genv_eq_trans := @eq_trans unit;
      ProgrammingLanguage.genv_eq_dec := genv_eq_dec;

      ProgrammingLanguage.state_eq := state_eq;
      ProgrammingLanguage.state_eq_dec := state_eq_dec;
      ProgrammingLanguage.state_eq_sym := state_eq_sym;
      ProgrammingLanguage.state_eq_refl := state_eq_refl;
      ProgrammingLanguage.state_eq_trans := state_eq_trans;

      ProgrammingLanguage.state_final_eq := state_final_eq;
      ProgrammingLanguage.step_eq := step_eq;
      ProgrammingLanguage.step_eq' := step_eq';
    |}.

  Definition υ : ProgrammingLanguage.genv_type imp_language := tt.


  Inductive finite_small_step_exec s : state → Prop :=
    | Halted : finite_small_step_exec s ([], s)
    | Step : ∀ S S',
      step υ 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.

  Lemma finite_small_step_exec_nsteps:
    ∀ S s',
      (∃ n, ProgrammingLanguage.nsteps υ n S = Some ([], s'))
        ↔ finite_small_step_exec s' S.

  Import ProgrammingLanguage.

  Lemma nsteps_imp_app_1:
    ∀ n s s' k₁ k₂,
      nsteps υ n (k₁, s) = Some ([], s') →
      nsteps υ n (k₁ ++ k₂, s) = Some (k₂, s').

  Lemma nsteps_compose:
    ∀ {n₁ n₂ k₁ k₂ k₃ s₀ s₂} s₁,
    nsteps υ n₁ (k₁, s₀) = Some ([], s₁) →
    nsteps υ n₂ (k₂, s₁) = Some (k₃, s₂) →
    nsteps υ (n₁ + n₂) (k₁ ++ k₂, s₀) = Some (k₃, s₂).
End ImpProgrammingLanguage.

Module Make (Var_as_DT : UsualDecidableTypeOrig) : (ImpProgrammingLanguage Var_as_DT).
  Include ImpProgrammingLanguage Var_as_DT.
End Make.