Library OracleLanguages.Imp.Oracles.OracleHelpers


Helpers for writing oracle languages on Imp

Require Import Common.
Require Import Imp.Lang.
Require Import ProgrammingLanguage.
Require Import OracleLanguage.
Require Omega.

Module Type ImpOracleHelpers
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT).
  Inductive cmd_mod (A : Type) :=
  | LeafMod : A cmd_mod A
  | Id : cmd_mod A
  | RecMod : cmd_mod A cmd_mod A cmd_mod A.


  Definition local_identity {A : Type} (m : cmd_mod A) : Prop :=
    match m with
    | IdLogic.True
    | RecMod _ _Logic.True
    | LeafMod _Logic.False
    end.

  Definition left_mod {A : Type} (m : cmd_mod A) : cmd_mod A :=
    match m with
    | IdId
    | LeafMod m
      
      LeafMod m
    | RecMod m₁ _m₁
    end.

  Definition right_mod {A : Type} (m : cmd_mod A) : cmd_mod A :=
    match m with
    | IdId
    | LeafMod m
      
      LeafMod m
    | RecMod _ m₂m₂
    end.

  Inductive cont_mod (A B : Type) :=
  | CmdMod : cmd_mod A cont_mod A B
  | ContMod : B cont_mod A B.


  Inductive step_helper_res (A B : Type) :=
  | GenericStep :
      state
      state
      list (cont_mod A B)
      step_helper_res A B
  | SpecialCmdStep :
      A
      list (cont_mod A B)
      step_helper_res A B
  | SpecialContStep :
      B
      list (cont_mod A B)
      step_helper_res A B
  | StuckStep :
      step_helper_res A B.


  Definition step_helper_id
            {A B : Type}
            (St₁ St₂ : state)
            (m : cmd_mod A)
            (km' : list (cont_mod A B)) :
    option (step_helper_res A B) :=
    match St₁, St₂ with
    | ([], _), ([], _)
      Some StuckStep
    | (Skip::_, _), (Skip::_, _)
    | (Assign _ _::_, _), (Assign _ _::_, _)
    | (Assert _::_, _), (Assert _::_, _)
      match step υ St₁, step υ St₂ with
      | None, NoneSome StuckStep
      | Some S₁', Some S₂'Some (GenericStep S₁' S₂' km')
      | _, _None
      end
    | (Seq c₁₁ c₁₂::k₁, s₁), (Seq c₂₁ c₂₂::k₂, s₂)
      Some (GenericStep
              (c₁₁::c₁₂::k₁, s₁)
              (c₂₁::c₂₂::k₂, s₂)
              (CmdMod (left_mod m)::CmdMod (right_mod m)::km'))
    | (ITE b₁ c₁₁ c₁₂::k₁, s₁), (ITE b₂ c₂₁ c₂₂::k₂, s₂)
      match eval_bexp s₁ b₁, eval_bexp s₂ b₂ with
      | Some true, Some true
        Some (GenericStep (c₁₁::k₁, s₁) (c₂₁::k₂, s₂) (CmdMod (left_mod m)::km'))
      | Some false, Some false
        Some (GenericStep (c₁₂::k₁, s₁) (c₂₂::k₂, s₂) (CmdMod (right_mod m)::km'))
      | None, None
        Some StuckStep
      | _, _None
      end
    | (While b₁ c₁::k₁, s₁), (While b₂ c₂::k₂, s₂)
      match eval_bexp s₁ b₁, eval_bexp s₂ b₂ with
      | Some true, Some true
        Some (GenericStep
                (c₁::While b₁ c₁::k₁, s₁)
                (c₂::While b₂ c₂::k₂, s₂)
                (CmdMod (left_mod m)::CmdMod m::km'))
      | Some false, Some false
        Some (GenericStep (k₁, s₁) (k₂, s₂) km')
      | None, None
        Some StuckStep
      | _, _None
      end
    | _, _
      None
    end.

  Definition step_helper
             {A B : Type}
             (St₁ St₂ : state)
             (km : list (cont_mod A B))
    : option (step_helper_res A B) :=
    match km with
    | (ContMod m)::km'
      Some (SpecialContStep m km')
    | (CmdMod m)::km'
      match m with
      | Id
      | RecMod _ _
        step_helper_id St₁ St₂ m km'
      | LeafMod m
        Some (SpecialCmdStep m km')
      end
    | []
      match St₁, St₂ with
      | ([], _), ([], _)
        Some StuckStep
      | _, _
        None
      end
    end.

  Lemma step_helper_special_cmd_step_inv:
     {A B : Type} S₁ S₂ (m : cont_mod A B) km m' km',
      step_helper S₁ S₂ (m::km) = Some (SpecialCmdStep m' km')
      m = CmdMod (LeafMod m') km = km'.

    Lemma step_helper_special_cont_step_inv:
     {A B : Type} S₁ S₂ (m : cont_mod A B) km m' km',
      step_helper S₁ S₂ (m::km) = Some (SpecialContStep m' km')
      m = ContMod m' km = km'.

  Lemma generic_step_bistep:
     {A B : Type} S₁ S₂ S₁' S₂' (km km' : list (cont_mod A B)),
      step_helper S₁ S₂ km = Some (GenericStep S₁' S₂' km')
      step υ S₁ = Some S₁' step υ S₂ = Some S₂'.

  Lemma generic_step_bicrash:
     {A B : Type} S₁ S₂ (km : list (cont_mod A B)),
      step_helper S₁ S₂ km = Some StuckStep
      step υ S₁ = None step υ S₂ = None.
End ImpOracleHelpers.

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