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
| Id ⇒ Logic.True
| RecMod _ _ ⇒ Logic.True
| LeafMod _ ⇒ Logic.False
end.
Definition left_mod {A : Type} (m : cmd_mod A) : cmd_mod A :=
match m with
| Id ⇒ Id
| LeafMod m ⇒
LeafMod m
| RecMod m₁ _ ⇒ m₁
end.
Definition right_mod {A : Type} (m : cmd_mod A) : cmd_mod A :=
match m with
| Id ⇒ Id
| 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, None ⇒ Some 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.