Library HeapAlgebraImplem_fs
Require Export AlgebraType.
Section R.
Variable R O:Set.
Variable PR:LatticeAtom R.
Variable PO:Lattice O.
Section gamma.
Variable gR : GammaBestTop Location PR.
Variable gO : Gamma (PowPoset ClassInst) PO.
Definition gammaHeap : Gamma (PowPoset Heap) (ArrayLattice PO WordSize).
refine (gamma_constr _ _
(fun H h =>
forall loc o p,
h loc = Some o ->
gR (best PR p) loc ->
gO (applyArray PO H p) o) _).
intros H1 H2 H h H' loc o p H1' H2'.
apply (gamma_monotone gO (applyArray PO H1 p)).
apply applyArray_monotone; auto.
eauto.
Defined.
End gamma.
Definition HeapConnect : Heap.Connect PR PO.
refine (Heap.Build_Connect
gammaHeap _
(fun f r o =>
modify_set PO
f (to_set PR r)
(fun o' => join PO o' o)) _ _
(fun f r => (apply_set PO f (to_set PR r))) _
(bottom (ArrayLattice PO WordSize)) _
).
intros.
intros HH h H1 loc o p H2 H3.
apply H0.
apply (H1 loc o); auto.
apply H; auto.
intros gR gO Hp Loc Obj h H.
inversion_clear H as [h' loc].
inversion_clear H0 in H1 H2.
intros loc' o' p; intros.
generalize dependent H.
unfold substHeap; case Location_dec; intro; subst; intros.
injection H; clear H; intros; subst.
apply (gamma_monotone gO (join PO (applyArray PO Hp p) Obj)).
apply apply_modify_set1 with (f:=(fun o'0 : O => join PO o'0 Obj)).
apply gamma_best with Location gR loc; auto.
apply (gamma_monotone gO Obj); auto.
CaseEq (in_set p (to_set PR Loc)); intros.
apply (gamma_monotone gO (join PO (applyArray PO Hp p) Obj)).
apply apply_modify_set1 with (f:=(fun o'0 : O => join PO o'0 Obj)); auto.
apply (gamma_monotone gO (applyArray PO Hp p)); auto.
apply (H1 _ _ p H); auto.
elim (gamma_best_exist gR _ _ H2); intros.
rewrite apply_modify_set2; auto.
apply (H1 _ _ p H); auto.
red; intros H5; rewrite H5 in H4; simpl in H4; discriminate H4.
intros gR1 gR2 gO Hp Loc Obj h loc o h' H.
inversion_clear H.
intros H1 H2 H3 H4 loc' o' p; intros.
generalize dependent H.
unfold substHeap; case Location_dec; intro; subst; intros.
injection H; clear H; intros; subst.
apply (gamma_monotone gO (join PO (applyArray PO Hp p) Obj)).
apply apply_modify_set1 with (f:=(fun o'0 : O => join PO o'0 Obj)).
apply gamma_best with Location gR2 loc; auto.
apply (gamma_monotone gO Obj); auto.
CaseEq (in_set p (to_set PR Loc)); intros.
apply (gamma_monotone gO (join PO (applyArray PO Hp p) Obj)).
apply apply_modify_set1 with (f:=(fun o'0 : O => join PO o'0 Obj)); auto.
apply (gamma_monotone gO (applyArray PO Hp p)); auto.
apply (H1 _ _ p H); auto.
apply H4; auto.
rewrite H; discriminate.
rewrite apply_modify_set2; auto.
apply (H1 _ _ p H); auto.
apply H4; auto.
rewrite H; discriminate.
simpl; intros.
inversion_clear H as [h' loc].
inversion_clear H0.
CaseEq (to_set PR r); intros.
elim (gamma_best_exist gR _ _ H2); intros.
apply (gamma_monotone gO (applyArray PO h x0)).
apply apply_set_in.
rewrite <- H0.
apply gamma_best with Location gR loc; auto.
apply H1 with loc; auto.
rewrite H0; discriminate.
destruct h; simpl.
apply (gamma_top gO (fun _ => True)); auto.
apply (gamma_top gO (fun _ => True)); auto.
intros.
intros h H loc o p.
rewrite H; intros H'; discriminate H'.
Defined.
End R.
Implicit Arguments HeapConnect [R O].
Index
This page has been generated by coqdoc