Library DomainsSign
This file contains the definitions of the lattices used in the
abstract semantics of the example language.
Require Export Ascii.
Require Export String.
Require Export Containers.OrderedType Containers.Tactics.
Set Implicit Arguments.
Require Export ConcreteWhile.
Require Export LibHeap.
Section Domains.
Require Export sign.
Require Export otherlattices.
Definition aVal := Sign.t.
Definition gamma_aVal : aVal → ℘ Val := Sign.gamma.
Instance var_OrderedType : OrderedType.OrderedType var.
Admitted.
Lemma var_eq_eq : ∀ v1 v2 : var,
v1 === v2 → v1 = v2.
Admitted.
Definition aErr := PowerSet.t error.
Global Instance aErrPoset : PosetDec.t aErr.
apply PowerSet.Poset with (fun f ⇒ f Err).
introv. iff I; repeat intros (); apply I.
apply make_comparable.
intros () (). apply decidable_make with true. fold_bool. rew_refl¬.
Defined.
Global Instance aErrLat : LatticeDec.t aErr.
apply PowerSet.Lattice with (fun f ⇒ f Err).
introv. iff I; repeat intros (); apply I.
apply make_comparable.
intros () (). apply decidable_make with true. fold_bool. rew_refl¬.
Defined.
Global Instance aErrTop : TopDec.t aErr.
typeclass.
Defined.
Definition gamma_aErr : aErr → ℘ error := PowerSet.gamma _.
Definition UndefLat := LiftBot.t UnitLattice.t.
Global Instance UndefLat_lattice : LatticeDec.t UndefLat.
Proof. apply LiftBot.Lat. typeclass. Defined.
Definition aValVar := SumLattice.t aVal UndefLat.
Definition gamma_aValVar : aValVar → ℘ (Val + unit) :=
SumLattice.gamma _ _ _ (LiftBot.Lat _ UnitLattice.Lat) _ _
gamma_aVal (LiftBot.gamma _ _ UnitLattice.gamma).
Definition aUndef : aValVar := SumLattice.make2 _ _ (Some tt).
Definition aEnv :=
MapDefault.t var aValVar _ (SumLattice.Lattice _ _ _ (LiftBot.Lat _ UnitLattice.Lat)).
Global Instance : LatticeDec.t aEnv.
apply MapDefault.Lattice. apply SumLattice.Top.
Defined.
Definition gamma_aEnv : aEnv → ℘ Env :=
immerse_gamma _ _ (MapDefault.gammaf _ _ _ _ _ gamma_aValVar) _
(fun E x ⇒
match read_option E x with
| Some v ⇒ inl v
| None ⇒ inr tt
end).
Definition aCtxEnv := Extend.t aVal (fun A ⇒ option (var × A)).
Global Instance aCtxEnv_Lat : LatticeDec.t aCtxEnv.
apply Extend.Lat with (param := var)
(ext := fun _ x v ⇒ Some (x, v))
(extr := fun _ ⇒ option_map (fun xv ⇒ (snd xv, fst xv)));
try typeclass.
intros A [[x1 v1]|] [[x2 v2]|] E1 E2; simpls; tryfalse.
applys decidable_make true. fold_bool. rew_refl¬.
Defined.
Global Instance : EquivDec.t aCtxEnv. typeclass. Defined.
Global Instance : PosetDec.t aCtxEnv. typeclass. Defined.
Definition gamma_aCtxEnv : aCtxEnv → CtxEnv → Prop :=
Extend.gamma aVal (fun A ⇒ option (var × A)) var
(fun _ ⇒ option_map (fun xv ⇒ (snd xv, fst xv)))
(fun _ _ C1 C2 ⇒
match C1, C2 with
| None, None ⇒ true
| _, _ ⇒ false
end) _ gamma_aVal.
Global Instance : Gamma.t _ _ gamma_aCtxEnv.
Proof.
apply¬ @Extend.Gamma.
intros ? ? ? [?|] [?|] [?|] E1 E2 E3 C1 C2; tryfalse; auto¬.
intros ? [?|] [?|] E1 E2 C; tryfalse; auto¬.
Qed.
Definition aEnvV := (aEnv × aCtxEnv)%type.
Definition gamma_aEnvV : aEnvV → EnvV → Prop :=
productProdGamma _ _ _ _ gamma_aEnv gamma_aCtxEnv.
Global Instance : Gamma.t _ _ gamma_aEnvV.
apply ProductProdGamma; typeclass.
Defined.
Definition aEnvF := @FlatLatticeDec.TB EnvF.
Global Instance : EquivDec.t EnvF.
apply Comparable_EquivDec. apply heap_comparable; typeclass.
Defined.
Definition gamma_aEnvF : aEnvF → EnvF → Prop := flatGamma _ _.
Definition aOute := (aVal × aErr)%type.
Definition gamma_aOute : aOute → ℘ oute :=
immerse_gamma _ _ (productSumGamma _ _ _ _ gamma_aVal gamma_aErr) _
(fun o ⇒
match o return Val + error with
| oute_val v ⇒ inl v
| oute_error err ⇒ inr err
end).
Definition aOuts := (aEnv × aErr)%type.
Definition gamma_aOuts : aOuts → ℘ outs :=
immerse_gamma _ _ (productSumGamma _ _ _ _ gamma_aEnv gamma_aErr) _
(fun o ⇒
match o return Env + error with
| outs_normal E ⇒ inl E
| outs_error err ⇒ inr err
end).
Global Instance : Gamma.t _ _ gamma_aOuts.
Proof. apply immerseGamma. apply ProductSumGamma; typeclass.
Defined.
Definition read_env (E : aEnv) x :=
MapDefault.read _ _ _ _ E x.
Definition write_env (E : aEnv) x v : aEnv :=
MapDefault.write _ _ _ _ E x (Some (inl v)).
Definition get_value : aValVar → aVal :=
fun v ⇒
match v with
| Some (inl v) ⇒ v
| Some (inr undef) ⇒ ⊥♯
| None ⇒ ⊤♯
end.
Definition aFun := @FlatLatticeDec.TB (option (var × stat)).
Global Instance : LatticeDec.t aFun.
apply FlatLatticeDec.t. apply Comparable_EquivDec. typeclass.
Defined.
Definition readF_env (E : aEnvF) f : aFun :=
match E with
| FlatLatticeDec.TB_Top ⇒ FlatLatticeDec.TB_Top
| FlatLatticeDec.TB_Bot ⇒ FlatLatticeDec.TB_Bot
| FlatLatticeDec.TB_Elem Ef ⇒ FlatLatticeDec.TB_Elem (read_option Ef f)
end.
Definition writeF_env (E : aEnvF) f x s : aEnvF :=
match E with
| FlatLatticeDec.TB_Top ⇒ FlatLatticeDec.TB_Top
| FlatLatticeDec.TB_Bot ⇒ FlatLatticeDec.TB_Bot
| FlatLatticeDec.TB_Elem Ef ⇒ FlatLatticeDec.TB_Elem (write Ef f (x, s))
end.
Some lemmae about these lattices.
Lemma gamma_aEnv_awrite : ∀ E aE x av,
gamma_aEnv (write_env aE x av) E →
∃ v,
binds E x v ∧
gamma_aVal av v.
Proof.
introv G. unfold write_env in G.
set (R := MapDefault.read_write_eq var aValVar var_OrderedType _
aE x x (Some (inl av)) (Equivalence_Reflexive _)). clearbody R.
do 3 unfolds in G. rename G into G'.
set (G := G' x). clearbody G. clear G'.
rewrite Heap.read_option_def in G. cases_if as I.
inverts G as G G'.
rewrite <- G' in R. clear G'. inverts R as R. eexists. splits.
apply× @read_binds.
clear - G R. set (G' := Gamma_eq _ _ _ _ gamma_aVal _ _ _ R). clearbody G'. clear R.
apply¬ G'.
rewrite <- G in R. inverts R.
inverts G.
set (Er := Gamma_eq _ _ _ _ gamma_aValVar _ _ _ R). clearbody Er. clear R.
set (Er' := proj1 (Er (inr tt))). clearbody Er'. clear Er. apply Er' in G. clear Er'.
inverts G as G. simpl in G. destruct G.
Qed.
End Domains.
Extract Constant var_OrderedType ⇒ "(fun s1 s2 -> if s1 = s2 then Eq else if s1 < s2 then Lt else Gt)".